| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-07-31 | Remove old specs that have more up to date version | Alasdair | |
| Move outdated things into old subdirectory | |||
| 2018-09-21 | Remove cheri and mips specs -- they now have their own repository. | Robert Norton | |
| 2018-09-03 | Coq: rework generation of dependent pairs so that they are only | Brian Campbell | |
| constructed when a function call, cast, or binder demands them, removing some ambiguous corner cases. Also - Don't simplify nexps before printing (note that we usually end up needing a (8 * x) / 8 lemma as a result) - More extraction of properties in the goal - Splitting of conditionals/matches in goals (which can occur more often because of the new positions of build_ex in definitions) - Try simple solving first to improve speed / reduce proof sizes / help fill in metavariables (because manipulating the goal can interfere with instantiating them) - Update RISC-V patch | |||
| 2018-08-28 | Adapt theory imports for Isabelle 2018 | Thomas Bauereiss | |
| Requires a recent Lem version that supports generating session-qualified imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860 | |||
| 2018-08-16 | Add the type an expression was checked against to tannots, and use for Coq | Brian Campbell | |
| Tweak extra Coq files to match. Tweak early return rewrite to use declared return type, which can always be put into an E_cast. | |||
| 2018-08-02 | Coq mips: fix deprecation warning | Brian Campbell | |
| 2018-08-02 | Coq: remove type removal holdover from Lem backend, add MIPS lemma | Brian Campbell | |
| 2018-07-24 | Merge remote-tracking branch 'origin/sail2' into c_fixes | Alasdair Armstrong | |
| 2018-07-24 | Now builds mips spec again. | Alasdair | |
| Some more testing needed to make sure it runs FreeBSD properly and CHERI before merging | |||
| 2018-07-23 | Coq: faster MIPS extras without confusing message | Brian Campbell | |
| 2018-07-12 | Add missing builtins needed for cheri128 C. Still doesn't build possibly due ↵ | Robert Norton | |
| to code gen issue. | |||
| 2018-07-12 | update arm and mips models for new type of write_ram builtin. Also fix c and ↵ | Robert Norton | |
| interpreter implementations of same. | |||
| 2018-07-11 | Update CHERI code extraction from Isabelle | Thomas Bauereiss | |
| Also use zero-initialised memory. Apparently some tests access unitialised memory, and the default behaviour of the Lem shallow embedding is to fail in this case. | |||
| 2018-07-10 | Make HOL build properly again for all of the models | Brian Campbell | |
| 2018-07-09 | Tweak bit casting definitions in MIPS to avoid non-exhaustive patterns | Brian Campbell | |
| Recent change made them proper matches rather than conditionals, and Coq rejects incomplete matches. (Will need a proper solution later...) | |||
| 2018-07-09 | Simplify treating of undefined_bool in Lem library | Thomas Bauereiss | |
| Use nondeterministic choice by default instead of a deterministic bitstream generator in the state, which is slightly awkward to reason about, because every use of undefined_boolS changes the state. The previous behaviour can be implemented as Sail code, if desired. Also add a default implementation of internal_pick that nondeterministically chooses an element from a list. | |||
| 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-06 | changes to increase MIPS coverage -- remove optional/unused PREF instruction ↵ | Robert Norton | |
| and unused cases in ll/sc match | |||
| 2018-07-05 | mips: ignore unused functions warnings caused by making some functions static. | Robert Norton | |
| 2018-07-04 | mips: move rmem integration instructions into separate file (disabled for ↵ | Robert Norton | |
| now) to avoid coverage noise. | |||
| 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 | Fill in a few Coq functions for CHERI from the MIPS prelude | Brian Campbell | |
| 2018-07-02 | Coq modulus operation that fits the type | Brian Campbell | |
| 2018-07-02 | Coq building rule in MIPS makefile | Brian Campbell | |
| 2018-06-29 | Try to fix some tricky C compilation bugs, break everything instead | Alasdair Armstrong | |
| 2018-06-28 | Add tagged memory to C rts to cheri can be compiled to C | Alasdair Armstrong | |
| 2018-06-27 | Add a mips_c_gcov target that builds mips_c model with coverage reporting. | Robert Norton | |
| 2018-06-27 | Add a new function cycle_limit_reached that returns bool, allowing for ↵ | Robert Norton | |
| graceful exit on reaching cycle limit. This aids coverage and valgrind instrumentation. | |||
| 2018-06-26 | mips: fix duplication of cycle_count call that arose due to git merge. | Robert Norton | |
| 2018-06-26 | mips: comment out printing of EXCEPTION on every ISA exception. | Robert Norton | |
| 2018-06-26 | turn on warnings when compiling mips c then dial back ones that are ↵ | Robert Norton | |
| triggered by generated code (probably false positives). Fix some warnings in rts.c | |||
| 2018-06-25 | Support bitlist representation in Sail2_string | Thomas Bauereiss | |
| 2018-06-25 | Coq: add typeclass based comparison, and instantiate for enums | Brian Campbell | |
| 2018-06-25 | Use getopt rather than argp for Mac compatibility in C runtime | Alasdair Armstrong | |
| Also further tweaks to Sail library for C and include sail lib files for tracing | |||
| 2018-06-25 | add device tree file for mips. | Robert Norton | |
| 2018-06-25 | mips: add optional tracing of register writes (commented out). | Robert Norton | |
| 2018-06-25 | Fix bugs in mips ldl/ldr that were probably introduced in porting to sail2. | Robert Norton | |
| 2018-06-22 | Fix Lem build of MIPS/CHERI | Thomas Bauereiss | |
| 2018-06-22 | Add current state of mips_extras.v | Brian Campbell | |
| 2018-06-22 | Add bitvector size constraints in MIPS | Brian Campbell | |
| 2018-06-22 | Add coq builtins for MIPS | Brian Campbell | |
| 2018-06-22 | Add coq generation rule for mips | Brian Campbell | |
| 2018-06-22 | add support for new cycle_limit feature in mips. | Robert Norton | |
| 2018-06-21 | Remove loading kernel from mips main | Alasdair Armstrong | |
| 2018-06-21 | Merge branch 'tracing' into sail2 | Alasdair Armstrong | |
| 2018-06-21 | Fix MIPS wrt changes to C runtime | Alasdair Armstrong | |
| This plus changes to bitfield internals is enough to run some MIPS tests at 1Mhz. | |||
| 2018-06-18 | Add bitvector length constraints to mips inequalities | Brian Campbell | |
| to match new constraints in prelude | |||
| 2018-06-11 | More efficient bitfield implementation | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |