summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2019-05-13fix typo in excl_res externJon French
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
2019-03-13C: Add missing update_lbits builtinAlasdair Armstrong
2019-03-12Coq: try non-linear nia solver tooBrian Campbell
2019-03-12Coq: fix some boolean issues seen in armBrian Campbell
Fixes bad precedence issues, removes an out-of-date special case that's not necessary, and solves more goals.
2019-03-08Fix the Coq mapping for eq_string in Sail lib.Prashanth Mundkur
2019-03-08Adds the DC and IC instructions to AArch64_small;Shaked Flur
Also, removes etc/regfp.sail and etc/regfp2.sail in favour of lib/regfp.sail
2019-03-07Fix bug in a mono rewrite helper functionThomas Bauereiss
2019-03-07Coq: apply a little brute force in some boolean goalsBrian Campbell
2019-03-05Coq: firstorder is better at the boolean goalsBrian Campbell
2019-03-05Coq: use setoid rewriting to apply under an existential binderBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-12 13:32:53 +0000