| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-28 | Coq: merge some implicit variables from axioms with arguments | Brian Campbell | |
| (Similar to the proper translation for function definitions) | |||
| 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 | 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-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: record conditionals in the context for constraint solving | Brian Campbell | |
| 2018-05-23 | Coq: Implement the most basic merging of type- and term-level parameters | Brian Campbell | |
| 2018-05-23 | riscv decode now uses mapping-decode and passes tests | Jon French | |
| 2018-05-23 | fix typo in error message in type_check.ml | Jon French | |
| 2018-05-22 | Fix one part of cast introduction, leave another for later | Brian Campbell | |
| 2018-05-22 | Fix for E_cons not being compiled correctly into OCaml | Alasdair Armstrong | |
| 2018-05-21 | Add an -ocaml-nobuild option to avoid building the generated ocaml by ↵ | Prashanth Mundkur | |
| default (off by default). | |||
| 2018-05-21 | further RISCV mapping: all extant non-compressed instructions done | Jon French | |
| 2018-05-21 | fix bug in rewrite_defs_mapping_patterns where pattern-uses of mappings with ↵ | Jon French | |
| multiple arguments weren't type-checking correctly | |||
| 2018-05-18 | Make named theorem collections of state monad more fine-grained | Thomas Bauereiss | |
| 2018-05-18 | Fix bug in rewriting variable updates | Thomas Bauereiss | |
| 2018-05-18 | temporary HACK for aarch64: make rewrite_defs_pat_lits ignore strings | Jon French | |
| 2018-05-18 | more riscv mappings; riscv now builds successfully to lem which builds to ↵ | Jon French | |
| isabelle (but isabelle almost certainly broken) | |||
| 2018-05-18 | Avoid split_on_char function that was introduced in OCaml 4.04. Use Util ↵ | Robert Norton | |
| version instead and make sure to install util and copy it to ocaml build directory. | |||
| 2018-05-17 | changes to for testing FreeBSD boot on MIPS: allowing loading raw file in ↵ | Robert Norton | |
| ocaml main so that we can have simboot + kernel. Support UART output only. | |||
| 2018-05-17 | Merge branch 'cheri-mono' into sail2 | Brian Campbell | |
| 2018-05-17 | fix bug in rewrite_defs_pat_string_append -- make it pass types through ↵ | Jon French | |
| correctly | |||
| 2018-05-17 | Remove sequential code again | Brian Campbell | |
| 2018-05-17 | Use an intermediate base_monad type alias in Lem, | Brian Campbell | |
| resolving the difference in type parameters between the prompt and state monads, and allowing a single output file to be used with either. Normally, the type alias is to the prompt monad, but for HOL4 we use the state monad. | |||
| 2018-05-16 | fix a couple warnings in type_check.ml | Jon French | |
| 2018-05-16 | Declare hol automatic termination in sail_values | Ramana Kumar | |
| 2018-05-16 | Add support for inline val-spec declaration for mappings | Jon French | |
| This means that a mapping which formerly had to be pre-declared like val name : a <-> b ... mapping name { x <-> y, ... } can now be shortened to mapping name : a <-> b { x <-> y, ... } | |||
| 2018-05-15 | Merge branch 'sail2' into mappings | Jon French | |
| 2018-05-15 | reorder lem rewrite passes and explicitly remove mapping valspecs; string ↵ | Jon French | |
| stuff now compiles to Lem | |||
| 2018-05-15 | rewrite_defs_guarded_pats: guards deserve rewriting too | Jon French | |
| 2018-05-14 | make debug printing of realised mappings both optional and lazy | Jon French | |
| 2018-05-12 | Fix bug in handling of registers with option type | Thomas Bauereiss | |
| Also add test cases and Isabelle lemmas | |||
| 2018-05-11 | More builtin names in constant propagation | Brian Campbell | |
| 2018-05-11 | Make nexp simplification a little smarter | Brian Campbell | |
| (should really make the Lem pretty printer use the solver properly, but this is a useful stopgap) | |||
| 2018-05-11 | Actually use the correct type for singleton rewriting this time | Brian Campbell | |
| 2018-05-11 | Be much more careful to introduce the right bitvector casts to the right sizes | Brian Campbell | |
| 2018-05-11 | Handle automatic existential unpacking in function application in mono analysis | Brian Campbell | |
| 2018-05-11 | Use type from funcl in singleton rewriting | Brian Campbell | |
| The pattern types may be subtypes, using those caused it to try rewriting int parameters and failing | |||
| 2018-05-11 | further riscv mapping | Jon French | |
| 2018-05-11 | support for mapping-patterns inside (should be) all other pattern types | Jon French | |
| 2018-05-11 | Add Boolean short-circuiting to state monad | Thomas Bauereiss | |
| 2018-05-11 | Merge branch 'sail2' into cheri-mono | Thomas Bauereiss | |
| In order to use up-to-date sequential CHERI model for test suite | |||
| 2018-05-11 | Remove buggy bit list comparison functions from Lem library | Thomas Bauereiss | |
| Found bugs by running CHERI test suite on Isabelle-exported model: signed less-than for bit lists was missing negations for the two's complement, and unsigned less-than compared the reverse lists. Since all other backends implement this in Sail, it seems best to just remove this code. Also add support for infix operators to Lem backend, by z-encoding their identifiers like the other backends do. | |||
| 2018-05-11 | Remove unneeded _sail suffix from latex files. | Robert Norton | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |