| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-18 | Update mono test script | Brian Campbell | |
| 2018-04-18 | Add first draft of Isabelle library documentation | Thomas Bauereiss | |
| 2018-04-18 | Add a simple Hoare logic for sequential reasoning to the library | Thomas Bauereiss | |
| 2018-04-18 | Fix bug in pretty-printing loops to Lem | Thomas Bauereiss | |
| 2018-04-18 | Add some lemmas about bitvectors | Thomas Bauereiss | |
| Also clean up some library functions a bit, and add some missing failure handling variants of division operations on bitvectors. | |||
| 2018-04-18 | Move a few printing functions to sail_values.lem | Thomas Bauereiss | |
| They are used in various specs and test cases. | |||
| 2018-04-18 | Fix another reference to BK_nat | Alastair Reid | |
| 2018-04-18 | Add a test case for using enum to number function as a cast | Alasdair Armstrong | |
| 2018-04-18 | Fix build on linux | Alasdair Armstrong | |
| Turns out that BSD sed is not a subset of GNU sed, GNU sed doesn't allow a space after the -i option. | |||
| 2018-04-18 | Port to Mac: BSD sed != GNU sed | Alastair Reid | |
| For GNU sed, the extension is optional in sed -i ... But in BSD sed, the extension is mandatory sed -i .bak ... | |||
| 2018-04-18 | Move Lem shl_int, shr_int implementations from aarch64_extras to sail lib | Brian Campbell | |
| (note that they're already declared in lib/arith.sail) | |||
| 2018-04-18 | Rename BK_nat to BK_int to be consistent with source syntax | Alasdair Armstrong | |
| 2018-04-18 | Updates to latex mode for documentation | Alasdair Armstrong | |
| 2018-04-18 | Merge branch 'sail2' of github.com:rems-project/sail into sail2 | Robert Norton | |
| 2018-04-18 | fix bug in permissions test of ctestsubset. | Robert Norton | |
| 2018-04-17 | Implement sret. | Prashanth Mundkur | |
| 2018-04-17 | Hook in the delegated trap handler and remove the old one. | Prashanth Mundkur | |
| 2018-04-17 | Add platform initialization for the new bits of machine state. | Prashanth Mundkur | |
| 2018-04-17 | Separate out the trap handler, and make it use the delegatee privilege. | Prashanth Mundkur | |
| 2018-04-17 | Define exception handler delegation. | Prashanth Mundkur | |
| 2018-04-17 | Enable mono builtins test, tweak test output | Brian Campbell | |
| 2018-04-17 | Fix slicing in constant propagation | Brian Campbell | |
| 2018-04-17 | Move some Lem library vector operations so that we also have mword versions | Brian Campbell | |
| 2018-04-16 | Implement the s-mode views of mie/mip, and their legalizers. | Prashanth Mundkur | |
| 2018-04-16 | Add the satp legalizer. | Prashanth Mundkur | |
| 2018-04-13 | Add <=_u to riscv prelude. | Prashanth Mundkur | |
| 2018-04-13 | Add some checks of current state, and use for the xepc write legalizer. | Prashanth Mundkur | |
| 2018-04-13 | Some initial legalizers for writes to S-mode CSRs. | Prashanth Mundkur | |
| 2018-04-13 | Define legalizers for writes to M-mode CSRs, and hook these writes to use them. | Prashanth Mundkur | |
| 2018-04-13 | Move riscv memory definitions into a separate file. | Prashanth Mundkur | |
| 2018-04-13 | Fix access checks to riscv CSRs. | Prashanth Mundkur | |
| 2018-04-13 | Add a few more generated file to gitignore | Brian Campbell | |
| 2018-04-13 | Update aarch64 no vector monomorphisation source for current type checker | Brian Campbell | |
| 2018-04-13 | Check all patterns inside functions with -dsanity | Brian Campbell | |
| 2018-04-12 | Fill in some minor missing cases in monomorphisation | Brian Campbell | |
| 2018-04-12 | remove cheri128 backwards compatibility hack that extended ↵ | Robert Norton | |
| access_system_regs perm into bits 14-11 -- it looks like spec is heading that way. | |||
| 2018-04-12 | implement new permit_unseal used for CUnseal instead of permit_seal. | Robert Norton | |
| 2018-04-12 | add a cheri_trace target for conveniently building a debug build. | Robert Norton | |
| 2018-04-12 | Add implementations of CReadHwr and CWriteHwr | Robert Norton | |
| 2018-04-12 | Add missing read of UserLocal register using dmtc0 4, sel 2. Write was ↵ | Robert Norton | |
| present but read was missing except via rdhwr. | |||
| 2018-04-11 | Initial bits of supervisor state. | Prashanth Mundkur | |
| 2018-04-11 | Add some misc informational m-mode registers that are used in a test. | Prashanth Mundkur | |
| 2018-04-11 | More structured riscv trap vector handling. | Prashanth Mundkur | |
| 2018-04-11 | Fix test prelude | Brian Campbell | |
| 2018-04-11 | Avoid unnecessary rechecking in remove numeral pats rewrite | Brian Campbell | |
| (especially as the environment previously used was a bit dodgy) | |||
| 2018-04-11 | Use more robust method of finding deps of new tyvars in mono analysis | Brian Campbell | |
| 2018-04-11 | Make the atom to singleton type rewriter replace literals with guards | Brian Campbell | |
| (previously the typechecker did this for all literal patterns, but now it's only necessary for the rewritten arguments) | |||
| 2018-04-11 | Fix neq_range in flow.sail | Alasdair Armstrong | |
| 2018-04-10 | Porting some minisail changes to sail2 branch | Alasdair Armstrong | |
| This commit primarily changes how existential types are bound in letbindings. Essentially, the constraints on both numeric and existentially quantified types are lifted into the surrounding type context automatically, so in ``` val f : nat -> nat let x = f(3) ``` whereas x would have had type nat by default before, it'll now have type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh type variable). This has several advantages: x can be passed to functions expecting an atom argument, such as a vector indexing operation without any clunky cast functions - ex_int, ex_nat, and ex_range are no longer required. The let 'x = something() syntax is also less needed, and is now only really required when we specifically want a name to refer to x's type. This changes slightly the nature of the type pattern syntax---whereas previously it was used to cause an existential to be destructured, it now just provides names for an automatically destructured binding. Usually however, this just works the same. Also: - Fixed an issue where the rewrite_split_fun_constr_pats rewriting pass didn't add type paramemters for newly added type variables in generated function parameters. - Updated string_of_ functions in ast_util to reflect syntax changes - Fixed a C compilation issue where elements of union type constructors were not being coerced between big integers and 64-bit integers where appropriate - Type annotations in patterns now generalise, rather than restrict the type of the pattern. This should be safer and easier to handle in the various backends. I don't think any code we had was relying on this behaviour anyway. - Add inequality operator to lib/flow.sail - Fix an issue whereby top-level let bindings with annotations were checked incorrectly | |||
| 2018-04-10 | Avoid rejecting reasonable pattern matches in monomorphisation | Brian Campbell | |
| (when they're not relevant) | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |