summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
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
2019-01-31Merge branch 'monads' into asl_flow2Thomas Bauereiss
2019-01-29Fixes for full v8.5Alasdair Armstrong
2019-01-29Add a few more type annotations after mono rewritesThomas Bauereiss
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-23Don't let "make" fail unnecessarily in lib/isabelleThomas Bauereiss
Only check for availability of Lem library if actually trying to build an Isabelle heap image.
2019-01-22Don't hardcode location of BBV libraryThomas Bauereiss
2019-01-22Make sure we optimize constrained union constructorsAlasdair
2019-01-21The RISCV environment variable collides with common usage by the RISC-V ↵Prashanth Mundkur
toolchain; use SAIL_RISCV instead to refer to sail-riscv.
2019-01-21Pass Lem library path to IsabelleThomas Bauereiss
2019-01-21Don't require manual set up of Isabelle session directoriesThomas Bauereiss
Since Isabelle 2018, specifying the same directory both on the command line and persistently in the user's ROOTS file is allowed, so we don't have to choose between one or the other any more.
2019-01-21Fix build of Isabelle documentationThomas Bauereiss
2019-01-14Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-10Fixes so 8.5 with vector instructions compiles to CAlasdair Armstrong
2019-01-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Merge sail2 into monadsThomas Bauereiss
2019-01-09Coq: add truncateLSB and import Zeuclid by defaultBrian Campbell
2019-01-04Add a few helper lemmasThomas Bauereiss
2019-01-04C library: fix fprintf warnings in lib/elf.cAlastair Reid
2019-01-01Coq: update instr_kinds from LemBrian Campbell
2018-12-29Coq: ensure that recursive functions computeBrian Campbell
2018-12-28Remove opt_spc_matches_prefix from sail.h (fixes C tests)Jon French
2018-12-28Merge branch 'sail2' into rmem_interpreterJon French
2018-12-27Coq: make solver try hints before stripping away existentialsBrian Campbell
(which allows us to avoid a Coq bug where the proof isn't recorded correctly)
2018-12-22Added RISC-V fence.tsoShaked Flur
2018-12-19Coq: add zeros library function (used by MIPS)Brian Campbell
2018-12-19Coq: handle existentials in hypotheses during solving, add max_nat, better castsBrian Campbell
2018-12-18Fix rewriter issuesAlasdair Armstrong
Fixes some re-writer issues that was preventing RISC-V from building with new flow-typing constraints. Unfortunately because the flow typing now understands slightly more about boolean variables, the very large nested case statements with matches predicates produced by the string-matching end up causing a huge blowup in the overall compilation time.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 23:09:30 +0000