summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-25Update coq read_mem/write_mem.Prashanth Mundkur
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-25Update prelude in mono testsBrian Campbell
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-19Coq: more robust handling of unknown constraintsBrian Campbell
2019-04-18Parameterise memory read/write primitives by address lengthJon French
2019-04-17Add interpreter annots to vector_dec.Prashanth Mundkur
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-17now without memory leaksJon French
2019-04-17add unimplemented C platform definitions for platform_read_mem etcJon French
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-17Merge pull request #42 from crabtw/sail2Robert Norton
Add base64 package constraint
2019-04-17Add base64 package constraintJyun-Yan You
2019-04-17Remove obsolete generated files from .gitignore directory so they will show ↵Robert Norton
up in git status.
2019-04-17Allow libsail to be installed without the other things (for rmem)Shaked Flur
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-16Code for testing builtins with CoqBrian Campbell
Disabled by default because it's fairly resource heavy. Currently two failures: a minor bug affecting divmod.sail, and undefined values aren't set up for set_slice_bits.sail.
2019-04-16Coq: make bools_of_int (and hence get_slice_int) compute wellBrian Campbell
2019-04-16Coq: set_slice typoBrian Campbell
2019-04-16Coq: tdiv builtinsBrian Campbell
2019-04-16Coq: add specialised shiftsBrian Campbell
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 11:14:06 +0000