summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2020-04-10Allow empty Sail source filesThomas Bauereiss
... instead of dying with "Syntax error".
2020-04-10Add Lem builtins for operations on realsThomas Bauereiss
... that match the names in lib/real.sail. Also fix the lem mapping for abs_int_atom and a Lem syntax error with nested record updates.
2020-04-10Make bounds check for vector subrange assignments stricterThomas Bauereiss
Check that indices are within bounds, not just in the right (increasing/decreasing) order.
2020-04-10Implement hex_str for LemThomas Bauereiss
2020-04-10Be more careful when flow-typing loopsThomas Bauereiss
Asserting constraints from the loop condition in the body is fine for while-loops, but doesn't make sense for until-loops.
2020-04-01Report SMT solver stderr on unexpected return codeBrian Campbell
2020-03-29Implement set_slice_int in the interpreterAlasdair
2020-03-25Fix a typo in write_mem for the interpreterAlasdair
2020-03-19Improve a particularly unhelpful type errorAlasdair
From: No type variable 'ex14# to: Type error: [../and_let_bool.sail]:6:19-50 6 | and_bool(let y : bool = x in not_bool(y), x) | ^-----------------------------^ | The type variable 'ex14# would leak into an outer scope. | | Try adding a type annotation to this expression. | This error was caused by: | [../and_let_bool.sail]:6:23-24 | 6 | and_bool(let y : bool = x in not_bool(y), x) | | ^ | | Type variable 'ex14# was introduced here |
2020-03-18Expose details of failed lexp bounds checksThomas Bauereiss
Allows ASL-to-Sail translation to automatically patch lexp bounds check errors.
2020-03-13SMT fixes for some corner cases of vector updatesThomas Bauereiss
2020-03-02Fix jenkinsAlasdair Armstrong
2020-03-02Add arith_shiftr to SMT and interpreterThomas Bauereiss
2020-02-25Implement count_leading_zeros for interpreterThomas Bauereiss
2020-02-24Avoid generating assertions multiple times during typecheckingThomas Bauereiss
2020-02-21Make sure we test that struct literals have a complete set of fields. Fixes #60Alasdair Armstrong
2020-02-21Distinguish type identifiers in topological sortingThomas Bauereiss
Fixes #61
2020-02-21Fix bug in last patch to topological sorting (e5ee087f)Thomas Bauereiss
2020-02-21SMT: Implement a few more primopsThomas Bauereiss
2020-02-21Nl_flow: Consider early returnsThomas Bauereiss
Tells the typechecker that, for example, in a block after if (i < 0) then { return (); } else { ... } the constraint not(i < 0) holds. This is a useful pattern when type-checking code generated from ASL.
2020-02-21Move topological sorting code to graph.mlThomas Bauereiss
2020-02-20More list C codegen fixes for issue #59Alasdair Armstrong
2020-02-20Fix missing code generation builtins for lists. Fixes #59Alasdair Armstrong
Also uncovered a few other issues w.r.t lists
2020-02-06Make sure tdiv_int and tmod_int are recognised by sail -iAlasdair Armstrong
2020-01-31Fix soundness bug found by MarkAlasdair
When returning a type from a letbinding we need to be careful that the type it returns does not refer to any type variable that only exists for the lifetime of the letbinding (because it was bound by it). Normally this fails because any type variable bound in the inner letbinding won't exist in the outer scope, but if it is shadowed this can cause an issue.
2020-01-30Make sure external pprint is listed as a dependency for sail when used as an ↵Alasdair Armstrong
OCaml library
2020-01-28Use external PPrintThomas Bauereiss
2020-01-28Fix a bug with lexp->exp conversion for register referencesAlasdair
2020-01-22Preserve effect annotation when realising mappingsThomas Bauereiss
2020-01-21Reduce the amount of unnecessary parentheses in Coq outputBrian Campbell
2020-01-21Use hex/bin literals in Coq backendBrian Campbell
Also be more careful to avoid pattern bindings with identifiers to avoid parsing clashes, eg `let 'bytes := ...` which is confused with the notation for binary literals.
2020-01-17Merge scattered mapping fixesJames Clarke
2020-01-17Merge branch 'coq-bool-props' into sail2Brian Campbell
2020-01-17Keep track of source locations for all IR branchesAlasdair
Useful for tracking down non-determinism
2020-01-16Allow effects on mappingsAlasdair Armstrong
2020-01-16Cleanup type-checking rule for LEXP_fieldAlasdair Armstrong
Was being overly conservative with nested structs and used an incorrect location for the error message
2020-01-16Keep track of (non-bit) vectors known to be fixed size in JibAlasdair Armstrong
This is useful because an arbitrary vector of a fixed size N can be represented symbolically as a vector of N symbolic values, whereas an arbitrary vector of arbitrary size cannot be easily represented.
2020-01-14Basic support to track uncaught exceptions in Sail->CAlasdair
2020-01-10Don't do any C specific name mangling for the cons operator in jib_compileAlasdair Armstrong
Instead handle it specially in c_backend, leaving the type information in the IR available for other consumers
2020-01-04Coq: change record field update notation to avoid duplicating termsBrian Campbell
(using match rather than let-and-projections because the latter would be reduced by tactics like unfold)
2020-01-03Add Sail pretty-printing of bitfieldsThomas Bauereiss
2019-12-18Make sure we generate literals of precisely the right length for symbolic ↵Alasdair Armstrong
execution
2019-12-13move ott pp to different Makefile rulePeter Sewell
2019-12-13experiment in ott-generated ppPeter Sewell
2019-12-12Fix a little bit of inconsistency in the command line argumentsAlasdair Armstrong
2019-12-10Introduce new bitfield syntax for ASL translationAlasdair Armstrong
Now we less desugared ASL we'd like to translate some notions more idiomatically, such as bitfields with names. However the current bitfield implementation in Sail is really ugly (entirely my fault) This commit introduces a new flag -new_bitfields which changes the behavior of bitfields as follows bitfield B : bits(32) = { Field: 7..0 } Is now treated as a struct with a single field called `bits` register R : B function main() -> unit = { R[Field] = 0xFF; assert(R[Field] == 0xFF) } then desugars as R.bits[7..0] = 0xFF and assert(R.bits[7..0] == 0xFF) which is much simpler, matches ASL and is probably how it should have worked all along
2019-12-06Don't introduce uneccesary control flow when compilingAlasdair Armstrong
2019-12-03Prover backends: Expand Int type synonyms in type definitionsThomas Bauereiss
... not just in type abbreviations. Fixes an error in the RV32 build of CHERI-RISC-V.
2019-12-01Coq: remove last use and definition of doc_nc_propBrian Campbell
(plus test, as it wasn't covered before)
2019-11-29Merge branch 'word-numerals' into sail2Thomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-15 12:58:17 +0000