| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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-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 | 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 | 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 | Declare hol automatic termination in sail_values | Ramana Kumar | |
| 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 | 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 | |
| 2018-05-11 | Avoid generating latex files that differ only by case because this causes ↵ | Robert Norton | |
| confusion on case insensitive file systems (e.g. mac). | |||
| 2018-05-10 | latex: don't include the prefix in the label. This means we have the option ↵ | Robert Norton | |
| of omitting valspec in documentation if it is deemed too verbose and still have hyperlinks work. The caveat is that it could result in multiply defined labels. | |||
| 2018-05-09 | Add language=sail option in listings command for latex output. This helps ↵ | Robert Norton | |
| with documents containing listings in multiple languages. | |||
| 2018-05-09 | Fix an issue with C compilation | Alasdair Armstrong | |
| 2018-05-09 | Fix printing of hex strings in Lem | Thomas Bauereiss | |
| 2018-05-09 | Add tests for Isabelle->OCaml generation for CHERI and AArch64 | Thomas Bauereiss | |
| 2018-05-09 | Add more annotations for loop bounds in Lem rewriting | Thomas Bauereiss | |
| Typechecking for-loops failed after the Lem rewriting passes in some cases: if the lower bound for the loop may be greater than the upper bound, the loop variable's type might be empty, and it cannot be initialised. This patch adds a guard "lower <= upper" around the loop body, and removes it again during pretty-printing. | |||
| 2018-05-09 | Run ARM built-in tests for Lem backend (via OCaml) | Thomas Bauereiss | |
| 2018-05-09 | Support short-circuiting of Boolean expressions in Lem | Thomas Bauereiss | |
| 2018-05-09 | Generate initial register state record | Thomas Bauereiss | |
| Filled with default values (e.g., 0) and used to initialise the state monad. There is already code to generate a Sail function "initialize_registers", but this is monadic itself, so it cannot be used to initialise the monad. | |||
| 2018-05-09 | Fix Byte_sequence errors due to linksem update | emersion | |
| 2018-05-04 | Add back purely sequential Lem generation | Thomas Bauereiss | |
| The datatype package of HOL4 does not support the prompt monad, so this patch restores the option to generate a model that only uses the state monad. Also add a Makefile target cheri_sequential.lem in the cheri/ directory. | |||
| 2018-05-04 | Checked that variable names in split_fun rewrites are really variables | Brian Campbell | |
| Otherwise some clauses disappear | |||
| 2018-05-04 | Fix missing nexp id rewriting | Brian Campbell | |
| 2018-05-04 | Rewrite constant nexps in specs | Brian Campbell | |
| (from Thomas) | |||
| 2018-05-04 | Add support for top-level values to monomorphisation singleton rewrite | Brian Campbell | |
| 2018-05-04 | Fix mono cast introduction to avoid a checking to inference change | Brian Campbell | |
| Adds return type to pattern so that the original function body is still type checked, rather than switching to type inference which may fail. | |||
| 2018-05-04 | Start updating monomorphisation | Brian Campbell | |
| + add additional lexp + update aarch64 mono demo source - still needs support for tyvars from assignments in dependency analysis | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |