| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-03 | Flow typing and l-expression changes for ASL parser | Alasdair Armstrong | |
| 1. Experiment with allowing some flow typing on mutable variables for translating ASL in a more idiomatic way. I realise after updating some of the test cases that this could have some problematic side effects for lem translation, where mutable variables are translated into monadic code. We'd need to ensure that whatever flow typing happens for mutable variables also works for monadic code, including within transformed loops. If this doesn't work out some of these changes may need to be reverted. 2. Make the type inference for l-expressions a bit smarter. Splits the type checking rules for l-expressions into a inference part and a checking part like the other bi-directional rules. Should not be able to type check slightly more l-expresions, such as nested vector slices that may not have checked previously. The l-expression rules for vector patterns should be simpler now, but they are also more strict about bounds checking. Previously the bounds checks were derived from the corresponding operations that would appear on the RHS (i.e. LEXP_vector would get it's check from vector_access). This meant that the l-expression bounds checks could be weakend by weakening the checks on those operations. Now this is no longer possible, there is a -no_lexp_bounds_check option which turns of bounds checking in l-expressions. Currently this is on for the generated ARM spec, but this should only be temporary. 3. Add a LEXP_vector_concat which mirrors P_vector_concat except in l-expressions. Previously there was a hack that overloaded LEXP_tup for this to translate some ASL patterns, but that was fairly ugly. Adapt the rewriter and other parts of the code to handle this. The rewriter for lexp tuple vector assignments is now a rewriter for vector concat assignments. 4. Include a newly generated version of aarch64_no_vector 5. Update the Ocaml test suite to use builtins in lib/ | |||
| 2018-05-03 | Fix duopod with latest riscv prelude | Alasdair Armstrong | |
| 2018-05-03 | Add typing rule for checking tuples as well as inferring them | Alasdair Armstrong | |
| Removes some patches in ASL parser Allow immutable variables to shadow mutable ones. This is useful for translating ASL. | |||
| 2018-05-03 | Fix interpreter messages for failing asserts | Alasdair Armstrong | |
| 2018-05-03 | Hook in address translation for stores and atomics. | Prashanth Mundkur | |
| 2018-05-03 | Log csr writes in the execution log. | Prashanth Mundkur | |
| 2018-05-03 | Work in progress on the coq backend | Brian Campbell | |
| - originally based on the Lem backend - added externs to some of the library files and tests - added wildcard to extern valspecs in parser - added Type_check.get_val_spec_orig to return the valspec with the function's original names for bound type variables Note that most of the tests will fail currently | |||
| 2018-05-02 | Hook in address translation for loads. | Prashanth Mundkur | |
| 2018-05-02 | Finish up Sv39 address translation. | Prashanth Mundkur | |
| 2018-05-02 | Tick cycle counter in execute loop. | Prashanth Mundkur | |
| 2018-05-02 | Fix printing of csr immediates. | Prashanth Mundkur | |
| 2018-05-02 | Fix typo in riscv model. | Prashanth Mundkur | |
| 2018-05-01 | cheri128: remove unnecessary xor of E with 48. The zeroing of E in memory is ↵ | Robert Norton | |
| achieved by xoring with null_cap_bits so this was only affecting register representation. | |||
| 2018-05-01 | cheri256: minor optimisation -- factor out null_cap_bits as top level let. | Robert Norton | |
| 2018-05-01 | cheri256: switch to using absolute address (cursor) instead of offset ↵ | Robert Norton | |
| (relative) representation in capability registers, making register and memory format the same and slightly simplifying code. Next step: use struct representation in registers eliminating many conversions between struct and bits? | |||
| 2018-05-01 | remove unneeded commented out code. | Robert Norton | |
| 2018-05-01 | Implement new CGetAddr instruction. Note that we should possibly rename ↵ | Robert Norton | |
| function getCapCursor to getCapAddr. | |||
| 2018-04-30 | Make make uninstall a bit safer... | Robert Norton | |
| 2018-04-27 | Cheri ISA change in CTestSubset -- ignore sealed bits when testing for ↵ | Robert Norton | |
| subset (aids garbage collection). | |||
| 2018-04-26 | Add riscv SV39 page-table walk. | Prashanth Mundkur | |
| 2018-04-26 | Ensure riscv interrupt delegation does not reduce current privilege. | Prashanth Mundkur | |
| 2018-04-26 | Fix bug introduced in alignment check. | Prashanth Mundkur | |
| 2018-04-26 | Lem: Add Size class annotations for nested bitvector types | Thomas Bauereiss | |
| 2018-04-26 | Initial support for faults of writes to physical addresses. | Prashanth Mundkur | |
| 2018-04-26 | Initial support for faults of reads to physical addresses. | Prashanth Mundkur | |
| 2018-04-26 | Fix bug in rewriting of loops | Thomas Bauereiss | |
| Take into account existential types when determining bounds for the loop variable | |||
| 2018-04-26 | Avoid adding explicit type annotations with generated type variables | Thomas Bauereiss | |
| 2018-04-26 | Make effect propagation in rewriter more efficient | Thomas Bauereiss | |
| Use non-recursive fix_eff_exp instead of recursive propagate_exp_effect, assuming that the effects of subexpressions have already been fixed by the recursive calls of the rewriter. | |||
| 2018-04-26 | Lazily evaluate debugging messages | Thomas Bauereiss | |
| This is meant to increase performance; for example, generating debug messages that include pretty-printed expressions can be very costly, if those expressions are complex (e.g. deeply nested E_internal_plet nodes representing a long sequence of monadic binds). | |||
| 2018-04-26 | Add a new SHARE_DIR argument to use when doing opam build. For non-opam ↵ | Robert Norton | |
| builds this defaults to git root. | |||
| 2018-04-26 | Make ocamlbuild assume lem is in path instead of relative to current directory. | Robert Norton | |
| 2018-04-26 | Fix apply_header target with location of LICENSE file. | Robert Norton | |
| 2018-04-26 | Opam packaging: add install and uninstall targets and code to find various ↵ | Robert Norton | |
| files in installed location. | |||
| 2018-04-26 | Remove obsolete mips/cheri rules from sail makefile. These are now built in ↵ | Robert Norton | |
| their respective subdirectories. | |||
| 2018-04-25 | Simplify subtyping check | Alasdair Armstrong | |
| This should make subtyping work better for tuples containing constrained types. Removes the intermediate type-normal-form representation from the subtyping check, and replaces it with Env.canonicalize from the canonical branch. | |||
| 2018-04-25 | Start working on documentation | Alasdair Armstrong | |
| 2018-04-24 | Add some explanations to free monad documentation | Thomas Bauereiss | |
| 2018-04-23 | Make riscv build depend on Makefile updates. | Prashanth Mundkur | |
| 2018-04-23 | Add riscv PTE definitions and access control checks. | Prashanth Mundkur | |
| 2018-04-23 | Merge branch 'rmn30_latex' into sail2 | Robert Norton | |
| 2018-04-23 | Add a cheri128_trace target. | Robert Norton | |
| 2018-04-23 | Fix a discrepancy with spec. about which register number is reported for ↵ | Robert Norton | |
| permissions failure in CBuildCap. | |||
| 2018-04-23 | Fix a problem with 128-bit setCapBounds function revealed by CBuildCap test ↵ | Robert Norton | |
| -- an assertion failure that new bounds are exact. The address of the new cap should have address=base (i.e. offset=0) but this was not being set. This was not previously visible because all other uses of setCapBounds already have address=newBase when calling. | |||
| 2018-04-20 | Fix a typo. | Prashanth Mundkur | |
| 2018-04-20 | Add a riscv instruction printer for the execution log. | Prashanth Mundkur | |
| 2018-04-20 | Some cleanup and comments. | Prashanth Mundkur | |
| 2018-04-20 | Make building of Isabelle heap image optional | Thomas Bauereiss | |
| 2018-04-20 | Allow instantiation of type or order type variables without kind declaration | Brian Campbell | |
| 2018-04-20 | Have sign_extend in common Sail Lem library, use it and zero_extend in | Brian Campbell | |
| mono rewrites | |||
| 2018-04-20 | Fix combined sign-extend-slice operation | Brian Campbell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |