summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-05-07Preserve more pattern locations during type checkingBrian Campbell
(monomorphisation uses them to decide where to case split)
2019-05-07Patch up a couple of Isabelle proofs due to memory interface changesBrian Campbell
2019-05-06Handle type variables generated while inferring applications in monomorphisationBrian Campbell
Also handle any type variables from assignments and degrade gracefully during constant propagation when unification is not possible.
2019-05-06Avoid degenerate construction monomorphisation, use # in generated namesBrian Campbell
2019-05-06Apply constructor monomorphisation in preference to variable splitsBrian Campbell
Note that we might need to do both in future. Also report more information when constructor refinement fails.
2019-05-06Calculate some type variable substitutions during constant propagationBrian Campbell
Needed for constructor monomorphisation
2019-05-06Handle global constants in monomorphisationBrian Campbell
2019-05-06Cope with irrelevant existentials when monomorphising constructorsBrian Campbell
2019-05-06Don't initialise registers in interpreter when register accesses not allowedBrian Campbell
Avoids having to handle unexpected undefined values during constant propagation.
2019-05-06Expand constraints while looking for sets during monomorphisationBrian Campbell
2019-05-03Tidy of Sail Ott definition to allow valid Isabelle datatypes to be ↵Mark Wassell
generated for Sail AST
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-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-17Coq: support pure loops with termination measuresBrian Campbell
2019-04-17now without memory leaksJon French
2019-04-17add unimplemented C platform definitions for platform_read_mem etcJon French
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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 23:46:56 +0000