summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
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.
2019-02-28Coq: more for informative booleansBrian Campbell
Make internal_plet produce annotations (with code to replace unusable type variables) Add mappings for bool kids at bindings Add version of and_bool that proves a property
2019-02-28Coq: some work on bool simplificationBrian Campbell
This introduces some simplification of informative booleans, but tries too hard to eliminate all of the existentials resulting in difficulties in and/or trees.
2019-02-25Fix some builtins, and make mod_int return naturalAlasdair Armstrong
2019-02-25Merge branch 'sail2' into rmem_interpreterJon French
2019-02-21Allow monomorphisation with C generationAlasdair
Run C tests with -O -Oconstant_fold -auto_mono
2019-02-13Merge branch 'sail2' into rmem_interpreterJon French
2019-02-08Add missing functions to HOL monad wrapperThomas Bauereiss
Also make the rewriter keep failed assertions in output when pruning blocks.
2019-02-07Monomorphisation tweaks for v8.5Thomas Bauereiss
Various tweaks to the monomorphisation rewrites. Disable old sizeof rewriting for Lem backend and rely on the type checker rewriting implicit arguments. Also avoid unifying nexps with sums, as this can easily fail due to commutativity and associativity.
2019-02-06Fix some testsAlasdair Armstrong
2019-02-06Remove all sizeof rewriting from C compilationAlasdair
All sizeof expressions now removed by the type-checker, so it's now properly a type error if they cannot be removed rather than a bizarre re-write error. This also greatly improves compilation speed overall, at the expense of the first type-checking pass.
2019-02-04Fix some warningsAlasdair Armstrong
2019-02-03Merge branch 'sail2' into rmem_interpreterJon French
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-02-01Tweak HOL LEM_DIR to match riscv makefileBrian Campbell
2019-02-01Make hol libraries use opam Lem library by defaultBrian Campbell
2019-01-31Build Isabelle heap image instead of just running sessionThomas Bauereiss
2019-01-31Adapt HOL library to monad changesThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 14:43:01 +0000