summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2019-04-29SMT: Refactor overflow checks into generic event checking systemAlasdair Armstrong
Have assert events for assertions and overflow events for potential integer overflow. Unclear how these should interact... The order in which such events are applied to the final assertion is potentially quite important. Overflow checks and assertions are now path sensitive, as they should be.
2019-04-29SMT: Support arbitrary tuple sizesAlasdair Armstrong
2019-04-27Merge branch 'sail2' into smt_experimentsAlasdair
2019-04-26Fix some broken interpreter testsAlasdair Armstrong
2019-04-26More constructor monomorphisation supportBrian Campbell
- handle multiple bitvector length variables - more fine-grained unnecessary cast insertion checks - add tuple matching support to constant propagation (for the test)
2019-04-25Fill in missing map_..._annot caseBrian Campbell
2019-04-25More read/write function updatesBrian Campbell
2019-04-25Get basic constructor monomorphisation working againBrian Campbell
- updates for type checking changes - handle a little more pattern matching in constant propagation - fix bug where false positive warnings were produced - ensure bitvectors in tuples are always monomorphised (to catch the case where the bitvectors only appear alone with a constant size)
2019-04-25Make constructor splitting in monomorphisation obey -dall_split_errorsBrian Campbell
2019-04-25Don't try to insert monomorphisation casts when the types are the sameBrian Campbell
2019-04-25lem gen_lib: update read/write functions to take (dummy) addrsize argument ↵Jon French
as in other places
2019-04-25SMT: Provide a more useful error message when topsort failsAlasdair
2019-04-24SMT: Make sure we clear overflow checks between generating propertiesAlasdair Armstrong
2019-04-24SMT: Can now recheck some simple models via the interpreterAlasdair
Probably need to clean-up the implementation and merge new_interpreter into this branch before supporting re-checking counterexamples with more things.
2019-04-23SMT: Add some commentsAlasdair
2019-04-23SMT: Only check counterexamples automatically with -smt_auto flagAlasdair Armstrong
2019-04-23SMT: Add parser for generated modelsAlasdair Armstrong
Simple parser-combinator style parser for generated models. It's actually quite tricky to reconstruct the models because we can have: let x = something $counterexample function prop(x: bits(32)) -> bool = ... where the function argument becomes zx/1 rather than zx/0, which is what we'd expect for the argument of a property. Might need to do something smarter with encoding locations into smt names to figure out what SMT variables correspond to which souce variables exactly. The above also previously generated incorrect SMT, which has now been fixed.
2019-04-23SMT: Add signed builtinThomas Bauereiss
2019-04-20SMT: Support writing to register referencesAlasdair Armstrong
Add a new AE_write_ref constructor in the ANF representation to make writes to register references explicit in Jib_compile
2019-04-20Fix: Reduce constant-fold time for ARM from 20min+ to 10sAlasdair Armstrong
With the new interpreter changes computing the initial state for the interpreter does some significant work. The existing code was re-computing the initial state for every subexpression in the specification (not even just the ones due to be constant-folded away). Now we just compute the initial state once and use it for all constant folds. Also reduce the time taken for the simple_assignments rewrite from 20s to under 1s for ARMv8.5, by skipping l-expressions that are already in the simplest form.
2019-04-19Coq: when replacing n_constraints in types allow for some rearrangementBrian Campbell
(in particular, to cope with Type_check.simp_typ)
2019-04-17SMT: Automatically get model when $counterexample is used rather than $propertyAlasdair Armstrong
2019-04-17Coq: support pure loops with termination measuresBrian Campbell
2019-04-17SMT: Support register referencesAlasdair Armstrong
2019-04-17SMT: Support generic vectors and handle lets between specs and functionsAlasdair Armstrong
If we have e.g. $property val prop : ... let X = 0 function prop(...) = X == ... then we need to ensure that let X is included when we generate the property.
2019-04-17SMT: Unroll simple foreach loopsAlasdair Armstrong
2019-04-17Build libsail again (removed Bytcode and Share_directory)Shaked Flur
2019-04-16Temporarily remove Makefile part that is making Jenkins failAlasdair Armstrong
Comment out some interpreter tests that go into infinite loops because those will cause issues for Jenkins.
2019-04-16Fix: Don't repeat ctyp_of_typ callAlasdair Armstrong
2019-04-16Remove unnecessary assertThomas Bauereiss
2019-04-16SMT: Support toplevel letbindingsAlasdair Armstrong
2019-04-16SMT: Fix inlining issuesAlasdair Armstrong
2019-04-16Coq: don't record assertions in the context if Sail doesn'tBrian Campbell
This can massively reduce Coq's typechecking time on assertion heavy code, such as the builtins tests.
2019-04-16Also allow "repeat" in loop termination measure syntaxBrian Campbell
2019-04-16BugfixingThomas Bauereiss
2019-04-16SMT: Take care to not generate duplicate labelsThomas Bauereiss
2019-04-16SMT: Add struct value literalsAlasdair
Generates much better SMT that assigning each field one-by-one starting with an undefined struct.
2019-04-15Add more SMT builtinsThomas Bauereiss
2019-04-15SMT: Allow partial specializationsAlasdair Armstrong
Change specialisation so we only specialize integer parameters when they are constant. This makes ensures that the integer-specialised code is always type-correct.
2019-04-15Merge branch 'sail2' of github.com:rems-project/sail into sail2Jon French
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
2019-04-15Fix: Allow zero-length vector literalsAlasdair Armstrong
2019-04-15Basic loop termination measures for CoqBrian Campbell
Currently only supports pure termination measures for loops with effects. The user syntax uses separate termination measure declarations, as in the previous recursive termination measures, which are rewritten into the loop AST nodes before type checking (because it would be rather difficult to calculate the correct environment to type check the separate declaration in).
2019-04-13SMT: Add count_leading_zeros and more builtinsAlasdair
2019-04-13SMT: More builtinsAlasdair
Add some tests for arithmetic operations. Some tests fail in either Z3 or CVC4 currently, due to how overflow is handled.
2019-04-12ToFromInterp_backend: print type annotations for abbrevs of unquantified ↵Jon French
types, to help out ocaml (hack)
2019-04-12ToFromInterp_backend: don't generate converters for cache_op_kindJon French
2019-04-12ToFromInterp_backend: better handling of nexpsJon French
2019-04-12Interpreter: remove debug printing (oops)Jon French
2019-04-12update libsail.mllib with more jib modulesJon French
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 15:40:26 +0000