| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-04 | Merge branch 'patch-1' of https://github.com/arichardson/sail into ↵ | Robert Norton | |
| arichardson-patch-1 | |||
| 2018-05-31 | Fix for Jenkins build | Alasdair Armstrong | |
| Looks like Jenkins is still on OCaml 4.02.3. We should probably upgrade to 4.05 at some point. | |||
| 2018-05-31 | Fixes to get ARM u-boot working in Sail. | Alasdair Armstrong | |
| Also fixes to C backend for compiling MIPS spec to C - Fix an issue with const correctness in internal_vector_update functions generated by C backend - Add builtins for MIPS to sail.h - Fix an issue where reg_deref didn't work when called on pointers to large bitvectors, i.e. vectors containing references to large bitfields as in the MIPS TLB code - Various bug fixes and changes for running U-boot on ARM model, including for interpreter and OCaml compilation. - Fix memory leak issues and incorrect shadowing for foreach loops - Update C header file. Fixes memory leak in memory read/write builtins. - Add aux constructor to ANF representation to hold environment information. - Fix undefined behavior caused by optimisation left shifting uint64_t vectors 64 or more times. Unfortunately there's more issues because the same happens for X >> 64 right shifts. It would make sense for this to be zero, because that would guarantee the property that ((X >> n) >> m) == (X >> (n + m)) but we probably need to do (X >> (n - 1) >> 1) in the optimisation to ensure that we don't cause UB. Shifting by 63 and then by 1 is well-defined, but shifting by 64 in one go isn't according to the C standard. This issue with right-shifts only occurs for zero-length vectors, so it's not a huge deal, but it's still annoying. - Add versions of print_bits and print_int that print to stderr. Follows OCaml convention of print/prerr. Should make things more explicit. Different backends had different ideas about where print should output to, not every backend needs to have this (e.g. theorem prover backends don't need to print) but having both stderr and stdout seperate and clear is useful for executable models (UART needs to be stdout, debug messages should be stderr). | |||
| 2018-05-31 | Some tweaks to ocaml compilation and sail_lib for ARM with system registers | Alasdair Armstrong | |
| 2018-05-31 | Add auxiliary script to Holmakefile | Ramana Kumar | |
| 2018-05-31 | Add some HOL4 termination proofs for state.lem | Ramana Kumar | |
| 2018-05-31 | Also dump the cap hwregs in dump_cp2_state | Alexander Richardson | |
| Dump format is the same as for the cap GPRs with DEBUG CAP HWREG as the prefix | |||
| 2018-05-30 | Fix typo in install instructions | Alasdair Armstrong | |
| 2018-05-30 | Update INSTALL.md | Alasdair Armstrong | |
| Some tweaks to installation instructions for latest OCaml versions (4.05 and 4.06) | |||
| 2018-05-28 | Coq: merge some implicit variables from axioms with arguments | Brian Campbell | |
| (Similar to the proper translation for function definitions) | |||
| 2018-05-28 | Coq: add back tests with undefined functions | Brian Campbell | |
| 2018-05-28 | Coq: prefer simple binders over patterns | Brian Campbell | |
| Otherwise it has occasional problems working out the return type | |||
| 2018-05-28 | Coq: add option to produce axioms for unimplemented functions | Brian Campbell | |
| Useful for partial test cases (e.g., some of the typechecking tests) Also a bonus warning for such functions in normal use | |||
| 2018-05-28 | Coq: proper printing of nexps | Brian Campbell | |
| 2018-05-25 | Coq: fill in some built-ins | Brian Campbell | |
| vector_access is a bit hacky at the moment - it expects a constraint to be shown between the index and the list size, but we don't track list sizes in general | |||
| 2018-05-25 | Use paged memory storage for ocaml backend memory. This is slightly slower ↵ | Robert Norton | |
| (<5% on a simple test) but dramatically reduces memory usage compared to having a hash table entry per byte! | |||
| 2018-05-25 | allow loading multiple raw files in ocaml main backend to allow kernel and ↵ | Robert Norton | |
| dtb to be mapped. | |||
| 2018-05-24 | Revert "Allow instantiation of type or order type variables without kind ↵ | Brian Campbell | |
| declaration" This reverts commit 895f868cd537277ba61dfc427fee0e288af7e226. These are actually treated as Ints (although you could pretend they weren't and it mostly worked). | |||
| 2018-05-24 | Check kinds of type variables while checking well-formedness of types | Brian Campbell | |
| Stops (e.g.) an Int being used as a Type, including when no kind was declared. The following commit will remove the test for the latter case. | |||
| 2018-05-24 | Coq: need None special case here, too | Brian Campbell | |
| 2018-05-24 | Coq: solve more constraints | Brian Campbell | |
| 2018-05-24 | Help launch coqide | Brian Campbell | |
| 2018-05-24 | Import (rather hacky) Coq Sail libraries | Brian Campbell | |
| 2018-05-24 | Coq: record conditionals in the context for constraint solving | Brian Campbell | |
| 2018-05-23 | Fix incorrect channel in dtc i/o. | Prashanth Mundkur | |
| 2018-05-23 | A couple of missing >= 0 constraints on vector handling functions | Brian Campbell | |
| 2018-05-23 | Coq: Implement the most basic merging of type- and term-level parameters | Brian Campbell | |
| 2018-05-23 | Fix riscv build for older versions of ocamlbuild (e.g. 4.02.3) by copying ↵ | Robert Norton | |
| platform ocaml files into _sbuild directory generated by sail and then running ocamlbuild there. | |||
| 2018-05-22 | Fix one part of cast introduction, leave another for later | Brian Campbell | |
| 2018-05-22 | Re-enable the RISC-V lem build, and switch the test-suite to use the ↵ | Prashanth Mundkur | |
| platform build. | |||
| 2018-05-22 | Fix for E_cons not being compiled correctly into OCaml | Alasdair Armstrong | |
| 2018-05-22 | Fix Lem build for RISC-V | Thomas Bauereiss | |
| 2018-05-21 | Fix a doc typo. | Prashanth Mundkur | |
| 2018-05-21 | Add the missed _tags file, and fix a typo. | Prashanth Mundkur | |
| 2018-05-21 | Start platform execution at the reset-vector in the rom. | Prashanth Mundkur | |
| 2018-05-21 | Add in the platform files and update the ocaml build. Disable the isabelle ↵ | Prashanth Mundkur | |
| build until we add suitable platform definitions/stubs. The platform bits are not yet hooked into the model, but only into the build, so are untested. | |||
| 2018-05-21 | Add an -ocaml-nobuild option to avoid building the generated ocaml by ↵ | Prashanth Mundkur | |
| default (off by default). | |||
| 2018-05-21 | Move the top-level loop from main to riscv_step, but remove elf bits. | Prashanth Mundkur | |
| 2018-05-21 | Move mem-op-result to _sys to be usable from _platform. | Prashanth Mundkur | |
| 2018-05-21 | Get Aarch64 exported to HOL4 | Brian Campbell | |
| Worked around problem with the model where it tries to use bound variables in patterns | |||
| 2018-05-21 | cheri: fix a bug in cfromptr: should give null result when value of rt is ↵ | Robert Norton | |
| zero not only when rt is the zero register (zr). | |||
| 2018-05-21 | Ignore src/share_directory.ml | Ramana Kumar | |
| src/Makefile suggests this is a generated file | |||
| 2018-05-18 | Make named theorem collections of state monad more fine-grained | Thomas Bauereiss | |
| 2018-05-18 | Add lemmas about monadic Boolean connectives | Thomas Bauereiss | |
| 2018-05-18 | Clean up aarch64_extras.lem | Thomas Bauereiss | |
| 2018-05-18 | Fix bug in rewriting variable updates | Thomas Bauereiss | |
| 2018-05-18 | mips: add support for CP0 Config0.K0 field because a test has appeared for ↵ | Robert Norton | |
| it. This concerns cache behaviour of kernel segment k0 but since we dont have a cache we just store the value. It could be relevant to RMEM if we ever want to support kernel mode there. | |||
| 2018-05-18 | cheri: add support for clc with big immediate (clcbi). This is quite easily ↵ | Robert Norton | |
| done by making it decode to same CLC ast node and extending length of immediate field to 16 bits. cscbi is not supported as the feeling is that it will not be needed. | |||
| 2018-05-18 | use correct inequality for strings. | Robert Norton | |
| 2018-05-18 | Add sail_valuesAuxiliary rw theorems to computeLib | Ramana Kumar | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |