summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
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
2019-03-05Coq 8.9 compatibility fixBrian Campbell
2019-03-05Additional optimizations for C compilationAlasdair
2019-03-04Merge branch 'sail2' into rmem_interpreterJon French
2019-03-01Coq: some library compatibility changesBrian Campbell
2019-03-01Coq: add a little bit of boolean solvingBrian Campbell
Just enough for RISC-V to go through
2019-02-28Coq: remove unused library definitionsBrian Campbell
2019-02-28Coq: Clean up rich boolean handling in backendBrian Campbell
Now generates something vaguely sensible for RISC-V, although the solver needs a little work. Adds type annotations around effectful, rich and/or expressions.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 16:02:35 +0000