| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-07 | Cancel riscv reservation before i/o scheduling, tweak reservation tracing. | Prashanth Mundkur | |
| 2018-07-07 | Add the lrsc tests from riscv-tests. | Prashanth Mundkur | |
| 2018-07-07 | An initial fix to riscv lr/sc, needs a review. | Prashanth Mundkur | |
| This uses a stronger model than the version in Sail-1 in order to perform address alignment checks. The reservation is kept on virtual addresses, and maintained in the platform model, but now the lr/sc definitions need calls to externs to update this state. An alternative was to reserve physical addresses, but that appeared to be more complicated without a lot more changes. Ideally, the model should be parameterizable over both options. | |||
| 2018-07-07 | Add some tracing to riscv address translation. | Prashanth Mundkur | |
| 2018-07-07 | Coq: bbv have reorganised their repository | Brian Campbell | |
| 2018-07-07 | Coq: precise generic vectors | Brian Campbell | |
| (probably still some pattern matching to do, but I don't think the models use that) | |||
| 2018-07-07 | Coq: supply index constraint in for loops | Brian Campbell | |
| 2018-07-07 | Coq: eq_range should take proofs | Brian Campbell | |
| 2018-07-06 | Coq: support assertions inside and outside of blocks | Brian Campbell | |
| 2018-07-06 | Coq: avoid nexp simplification when deciding whether a cast is needed | Brian Campbell | |
| 2018-07-06 | Coq: Avoid clashes with the monad name, M | Brian Campbell | |
| 2018-07-06 | Coq: feed assertions into the context | Brian Campbell | |
| 2018-07-06 | Coq: use List.In predicates in constraint solving; make other bits robust | Brian Campbell | |
| 2018-07-06 | Coq: reduce use of sumbool_of_bool to relevant constraints | Brian Campbell | |
| 2018-07-06 | Coq: missing existential building for ranges | Brian Campbell | |
| 2018-07-06 | Coq: turn off partial support for dropping true constraints, fix strings | Brian Campbell | |
| 2018-07-06 | Change HighestSetBit into a form that can be handled by c backend. There are ↵ | Robert Norton | |
| still a few builtins missing before cheri128 will work. | |||
| 2018-07-06 | add gcov option for cheri_c. Add cheri128_c target. | Robert Norton | |
| 2018-07-06 | changes to increase MIPS coverage -- remove optional/unused PREF instruction ↵ | Robert Norton | |
| and unused cases in ll/sc match | |||
| 2018-07-05 | Fix printing of aq/rl flags in risc-v lr/sc. | Prashanth Mundkur | |
| 2018-07-05 | Fix equality comparisons for variants in C | Alasdair | |
| Makes sure equality comparisons for variants are compiled correctly. Needed for CHERI and mips, which have structs containing variants. Also make sure that struct equality works for structs containing other structs. | |||
| 2018-07-05 | Coq: get index_list right | Brian Campbell | |
| 2018-07-05 | Fix equality comparisons for structs | Alasdair | |
| Add a test case in test/c/eq_struct.sail. Ensure that the macro EQUAL(type) will always give a valid equality function for any builtin type in sail.h. | |||
| 2018-07-05 | Fix CHERI test that was failing when compiled to C | Alasdair Armstrong | |
| Non bitvector literals for decreasing vectors were not being reversed correctly, so the list of capability registers was effectively in reverse order. Added a test case to test/c/ based on this aspect of CHERI | |||
| 2018-07-05 | mips: ignore unused functions warnings caused by making some functions static. | Robert Norton | |
| 2018-07-05 | make many generated c functions static -- this gives the compiler a chance ↵ | Robert Norton | |
| to notice if they are dead or inline them if appropriate, cleaning up coverage reports and potentially improving execution speed. | |||
| 2018-07-05 | support acquire/release loads/stores in RISCV initial_analysis | Jon French | |
| 2018-07-05 | print to stdout not stderr to stop upsetting rmem regression tests | Jon French | |
| 2018-07-05 | restore missing RISC-V fence types in sail2; ignore io bits in fences more ↵ | Jon French | |
| cleanly | |||
| 2018-07-04 | mips: move rmem integration instructions into separate file (disabled for ↵ | Robert Norton | |
| now) to avoid coverage noise. | |||
| 2018-07-04 | AArch64 Prelude: Move cycle count primop to prelude | Alastair Reid | |
| 2018-07-03 | Add htif tohost to the riscv tracecmp tool. | Prashanth Mundkur | |
| 2018-07-03 | Allow the riscv htif_tohost mmio port to be readable, and ack writes to that ↵ | Prashanth Mundkur | |
| port. | |||
| 2018-07-03 | Fix a bug in foreach loops | Alasdair Armstrong | |
| We should test before the first iteration in case 'to' starts out as less than 'from'. | |||
| 2018-07-03 | cheri: refine lwl/lwr cap length checks to be exact. They were previously a ↵ | Robert Norton | |
| bit loose, but conservative. | |||
| 2018-07-03 | mips: just whitespace. | Robert Norton | |
| 2018-07-03 | Fix letbind_effects on LEXP_deref with an effectful subexpression | Brian Campbell | |
| 2018-07-03 | Fill in a few Coq functions for CHERI from the MIPS prelude | Brian Campbell | |
| 2018-07-03 | Main: fix SEE handling | Alastair Reid | |
| If a SEE exception is not caught within the decoder, it is an error in the Sail implementation or in the instruction set spec. This change ensures that we promptly detect and unambiguously report such errors. | |||
| 2018-07-03 | cheri: update to register file semantics. Most instructions now treat c0 as ↵ | Robert Norton | |
| null capability while some still refer to DDC. Special registers moved out of general capability register file. All capabilties initialised to null except those required for MIPS compatibility. | |||
| 2018-07-02 | Fix get_recursive_functions to not only pick up non-mutually recursive functions | Alasdair Armstrong | |
| The code to do this is rather ugly. It would be nice to have a generic callgraph representation we could just query and not use the rewriter in a weird way to extract this info. | |||
| 2018-07-02 | Coq: add some string functions | Brian Campbell | |
| 2018-07-02 | Coq: tidy up a bit of printing | Brian Campbell | |
| 2018-07-02 | Coq modulus operation that fits the type | Brian Campbell | |
| 2018-07-02 | Coq: replace simpl in a tactic with a more precise "change" | Brian Campbell | |
| Prevents partial unfolding of Z.pow. | |||
| 2018-07-02 | Coq: multiple record field updates | Brian Campbell | |
| Uses simple method of printing the entire record, in lieu of any decent record update syntax. | |||
| 2018-07-02 | Work around Coq issue with pattern binders | Brian Campbell | |
| 2018-07-02 | Coq building rule in MIPS makefile | Brian Campbell | |
| 2018-07-02 | cheri: the default cap for 256-bits no longer has reserved bits set. | Robert Norton | |
| 2018-07-02 | optimise cheri c build. | Robert Norton | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |