summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2019-05-17SMT: Finish adding all memory builtins from lib/regfp.sailAlasdair Armstrong
2019-05-15Coq: constraint solving for aarch64Brian Campbell
Also split out main solver tactic to make debugging a little easier.
2019-05-14Various bugfixesAlasdair Armstrong
Since we have __deref to desugar *x in this file (as it's the one file everything includes) we might as well add a __bitfield_deref here too, for the bitfield setters. Make sure undefined_nat can be used in C Both -memo_z3 and -no_memo_z3 were listed as default options, now only -no_memo_z3 is listed as the default.
2019-05-14Merge branch 'smt_experiments' into sail2Alasdair Armstrong
2019-05-14Add feature that allows functions to require type variables are constantAlasdair Armstrong
can now write e.g. forall (constant 'n : Int) rather than forall ('n: Int) which requires 'n to be a constant integer value whenever the function is called. I added this to the 'addrsize variable on memory reads/writes to absolutely guarantee in the SMT generation that we don't have to worry about the address being a variable length bitvector.
2019-05-13Merge branch 'sail2' into smt_experimentsAlasdair
2019-05-13Parse dereferences in orderinary expressionsAlasdair
2019-05-13fix typo in excl_res externJon French
2019-05-10SMT: Experiment with symbolic memory reads and writesAlasdair Armstrong
2019-05-09SMT: Make path conditionals more preciseAlasdair Armstrong
Previously path conditionals for a node were defined as the path conditional of the immediate dominator (+ a guard for explicit guard nodes after conditional branches), whereas now they are the path conditional of the immediate dominator plus an expression encapsulating all the guards between the immediate dominator and the node. This is needed as the previous method was incorrect for certain control flow graphs. This slows down the generated SMT massively, because it causes the path conditionals to become huge when the immediate dominator is far away from the node in question. It also changes computing path conditionals from O(n) to O(n^2) which is not ideal as our inlined graphs can become massive. Need to figure out a better way to generate minimal path conditionals between the immediate dominator and the node. I upped the timeout for the SMT tests from 20s to 300s each but this may still cause a failure in Jenkins because that machine is slow.
2019-05-08Remove generated TeX fileThomas Bauereiss
2019-05-07Merge branch 'sail2' into smt_experimentsAlasdair Armstrong
2019-05-07Patch up a couple of Isabelle proofs due to memory interface changesBrian Campbell
2019-05-05C: Add option to compile using __int128 rather than GMPAlasdair
Only requires a very small change to c_backend.ml. Most of this commit is duplication of the builtins and runtime in lib/int128. But the actual differences in those files is also fairly minor could be handled by some simple ifdefs for the integer builtins.
2019-05-03Jib: Optimize set_slice for ARM v8.5Alasdair Armstrong
2019-05-03Jib: Fix optimizations for SMT IR changesAlasdair Armstrong
Fixes C backend optimizations that were disabled due to changes in the IR while working on the SMT generation. Also add a -Oaarch64_fast option that optimizes any integer within a struct to be an int64_t, which is safe for the ARM v8.5 spec and improves performance significantly (reduces Linux boot times by 4-5 minutes). Eventually this should probably be a directive that can be attached to any arbitrary struct/type. Fixes the -c_specialize option for ARM v8.5. However this only gives a very small performance improvment for a very large increase in compilation time however.
2019-04-27Merge branch 'sail2' into smt_experimentsAlasdair
2019-04-26Fix some broken interpreter testsAlasdair Armstrong
2019-04-25Update coq read_mem/write_mem.Prashanth Mundkur
2019-04-25More read/write function updatesBrian Campbell
2019-04-24SMT: Make sure we clear overflow checks between generating propertiesAlasdair Armstrong
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-17now without memory leaksJon French
2019-04-17add unimplemented C platform definitions for platform_read_mem etcJon French
2019-04-17SMT: Unroll simple foreach loopsAlasdair Armstrong
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-15Merge branch 'sail2' of github.com:rems-project/sail into sail2Jon French
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
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-12lib/regfp.sail: add explicit C binding for memory access functionsJon French
2019-04-10Coq: update prompt monad to match the Lem, and port the state monad/liftingBrian Campbell
NB: requires minor changes in the models
2019-04-05Coq: termination measures for mutually recursive functionsBrian Campbell
2019-04-04Coq: improve solver on conjunctions, Euclidean division/moduloBrian Campbell
2019-03-27Coq: add a little knowledge about ZEuclid.divBrian Campbell
2019-03-27Coq: replace firstorder with less expensive tacticsBrian Campbell
2019-03-22Tidy up of div and mod operators (C implementation was previously ↵Robert Norton
inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one.
2019-03-19Coq: more test workBrian Campbell
- add dummy print_bits function - support int(1) like types in axioms
2019-03-19Coq: more work on testsBrian Campbell
- skip a few more that aren't supported yet - produce better debugging information (in particular, in the right order) - avoid some autocasts that aren't supported yet and are usually unnecessary - Handle more constraints like `8 * n = 8 * ?Goal`
2019-03-18Add non-negative constraints for zeros/onesBrian Campbell
2019-03-15Various monomorphisation tweaks and fixesThomas Bauereiss
2019-03-15Make mono_rewrites less dependant on ASL preludeThomas Bauereiss
... so that it can be more easily used for other specs. Also add some functions to vector_dec.sail to support this.
2019-03-15Coq: some progress on the test suiteBrian Campbell
Rewrite <> true/false in goals. Correct implicits in record and variant types. Use expanded valspecs from the type checker in axioms. Allow list notations in type definitions. Skip some not-yet-supported tests.
2019-03-15Coq: better loop handling, discharge some related proof obligationsBrian Campbell
2019-03-14Merge branch 'sail2' into rmem_interpreterJon French
2019-03-13lib/regfp.sail: new standard intrinsics for triggering memory effectsJon French
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 11:50:33 +0000