summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-21Tweak types of loop combinators for prover combinatorsThomas Bauereiss
Split the variable (tuple) type into an input and output type. They are meant to be the same, but due to the way function types are instantiated, unification can fail in the case of existential types, as in the added test case (when trying to generate Lem definitions from it). The output of the loop will be checked against the expected type, though, due to a type annotation outside the loop added by the rewrite pass for variable updates.
2020-04-21Save SMT cache when terminating with an exceptionThomas Bauereiss
2020-04-21Add more mono rewrites for bitvector subrangesThomas Bauereiss
2020-04-21Rewrite vector concat lexps to sequences of assignmentsThomas Bauereiss
... instead of a tuple assignment. This makes the rewrite independent of the tuple assignment rewrite and allows it to be moved after the latter (nesting vector concat lexps into tuple lexps is an idiom in ASL, but the other way around doesn't make sense).
2020-04-21Be more careful about type annotations in rewrites to LemThomas Bauereiss
In particular, don't add annotations for types with existentially quantified variables that only occur in constraints, not in the type, e.g. {'i1 'i2, 'i1 == div('i2, 8). int('i1)}. These seem to confuse the type checker when pulled out into the source AST.
2020-04-10Check more types in monomorphisation rewritesThomas Bauereiss
In the new version of the ASL-generated Sail, some vector operators are also overloaded for integers to match idioms of ASL (e.g. i[31:0], where i is an integer), so check in the monomorphisation rewrites that we use bitvector helper functions only for actual bitvectors.
2020-04-10Add test output to gitignoreThomas Bauereiss
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-10Update path for newer versions of BBV Coq libraryThomas Bauereiss
2020-04-10Make merlin know about pprintThomas Bauereiss
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-01Update INSTALL.mdAlasdair Armstrong
Mention robert's workaround for z3 on WSL
2020-04-01Report SMT solver stderr on unexpected return codeBrian Campbell
2020-03-29Implement set_slice_int in the interpreterAlasdair
2020-03-25Merge pull request #64 from arichardson/intellij-syntaxAlasdair Armstrong
Add documentation for CLion/PyCharm/IntelliJ syntax highlighting
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-18Add documentation for CLion/PyCharm/IntelliJ syntax highlightingAlex Richardson
Turns out the TextMate Bundles plugin can load the vscode extension and provide some basic syntax highlighting.
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-24Allow overloading of subrange builtins for non-bitvectorsThomas Bauereiss
2020-02-24Avoid generating assertions multiple times during typecheckingThomas Bauereiss
2020-02-23Merge branch 'sail2' of https://github.com/rems-project/sail into sail2jp
2020-02-23set vscode syntax highlighting extension up for publicationjp
2020-02-21Add barriers to regfp.sail for full ARMv8Alasdair Armstrong
Again use an $ifdef to avoid breaking RMEM. We can't use the same barrier_kind, because we *really* want a plain enumeration both for its simple SMT representation and a simple 1 to 1 mapping to the cat models used by herd. Technically for Isla, all the read_kind/write_kind/barrier_kind etc types can be defined separately on a per-architecture basis anyway, so maybe using this file at all is a bit of an anachronism.
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-14mention vscode mode in READMEjp
2020-02-12add vscode syntax highlighting modejp
2020-02-12made list of required ubuntu packages completejp
2020-02-12Merge branch 'sail2' of https://github.com/rems-project/sail into sail2jp
2020-02-12improve syntax highlightingjp
2020-02-06Make sure tdiv_int and tmod_int are recognised by sail -iAlasdair Armstrong
2020-02-05Tweak Coq scopes for 8.11Brian Campbell
2020-02-03Add an __instr_announce builtin in regfp.sailAlasdair Armstrong
Allows keeping track of which instructions actually get executed in a trace
2020-02-03Update regfp.sail with ifetch changes from poly_mapping branchAlasdair Armstrong
However, use an ifdef to make sure the ifetch changes only appear for the ARM spec, because otherwise the generated lem for RMEM will break.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 05:58:49 +0000