summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-01-31Make cast insertion handle more complex nexps and pushing casts into blocksBrian Campbell
# Conflicts: # src/monomorphise.ml
2019-01-31Monomorphisation: improve cast insertion and nexp rewriting on variantsBrian Campbell
It now pushes casts into lets and constructor applications, and so supports the case needed for RISC-V.
2019-01-31Add missing cases to constraint comparisonBrian Campbell
2019-01-31Support case splitting on variables as well as sizeof in cast introductionBrian Campbell
2019-01-29Improve generation of initial register stateThomas Bauereiss
Define initial values for record types once instead of repeating them in the initial register state.
2019-01-28Lem: Be more careful about nexps occurring in the function signatureThomas Bauereiss
Don't ask Z3 to simplify them, as flow typing might lead to different results in different if-branches, for example, leading to type errors in Lem.
2019-01-25Monomorphisation: update a built-in nameBrian Campbell
2019-01-25Fix solution finding using SMT by looking for the right variableBrian Campbell
2019-01-23Minor opam release to fix #26. Also includes new unrolling pragma.Robert Norton
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-22Add some more test casesAlasdair Armstrong
2019-01-22Add a pragma for unrolling recursive functionsAlasdair Armstrong
For example in RISC-V for the translation table walk: $optimize unroll 2 val walk32 ... function walk32 ... would create two extra copies of the walk_32 function, walk_32_unroll_1 and walk_32_unroll_2, with only walk_32_unroll_2 being recursive. Currently we only support the case where we have $optimize unroll, directly followed by a valspec, then a function, but this should be generalised in future. This optimization nearly doubles the performance of RISC-V It is implemented using a new Optimize.recheck rewrite that replaces the ordinary recheck_defs pass. It uses a new typechecker check_with_envs function that allows re-writes to utilise intermediate typechecking environments to minimize the amount of AST checking that occurs, for performance reasons. Note that older Sail versions including the current OPAM release will complain about the optimize pragma, so this cannot be used until they become up to date with this change.
2019-01-22Bump opam version for release.Robert Norton
2019-01-22Build isabelle and hol files in lib from lem before opam install.Robert Norton
2019-01-22Don't hardcode location of BBV libraryThomas Bauereiss
2019-01-22Make sure there is an ocaml representation for optimized memory read forAlasdair
RISC-V
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 typo in install instructionsAlasdair Armstrong
2019-01-21Remove old emacs mode to avoid confusionAlasdair Armstrong
2019-01-21Update manual snapshot and add basic sail -latex documentationAlasdair Armstrong
2019-01-21Fix build of Isabelle documentationThomas Bauereiss
2019-01-21Add output directory option for generated Isabelle auxiliary theoriesThomas Bauereiss
2019-01-21Fix some issues with latex generation so manual builds againAlasdair Armstrong
since riscv is no longer in this repository, and we use the RISC-V duopod as an example, you need to build as: make RISCV=directory manual.pdf if directory is not equal to ../../sail-riscv (which is where it would be if sail and sail-riscv are checked out in the same respository together)
2019-01-21Fix a bug with type-checking and latex generationAlasdair Armstrong
We should maybe just make the -latex option behavior the default to avoid this kind of thing
2019-01-19wibShaked Flur
2019-01-16Latex: handle underscores when generating latex names.Prashanth Mundkur
2019-01-14Add options for output directories for the lem and coq backends.Prashanth Mundkur
2019-01-13update READMEPeter Sewell
2019-01-13update README with current model reposPeter Sewell
2019-01-09Update Coq snapshotsBrian Campbell
2019-01-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Coq: add parens around negative integer literalsBrian Campbell
2019-01-09Coq: add truncateLSB and import Zeuclid by defaultBrian Campbell
2019-01-02Coq: tweak recently introduced type check to ignore effectsBrian Campbell
2019-01-01Coq: update instr_kinds from LemBrian Campbell
2018-12-31Last rewrite reordering needs more typecheckingBrian Campbell
2018-12-31Coq: move function clause merging to keep measure argument intactBrian Campbell
2018-12-30Sort dependencies of termination measures properlyBrian Campbell
2018-12-29Coq: ensure that recursive functions computeBrian Campbell
2018-12-29Add separate termination_measure declarationsBrian Campbell
2018-12-27Coq: avoid putting ambiguous numeric literals in Coq outputBrian Campbell
There are situations when we really want a more refined expression, such as 8 * n instead of 64 (when we know n = 8 from a case split), but we might not be able to generate it. For now we generate an underscore and let Coq figure it out from the context.
2018-12-27Coq: fix name clashes and instantiation calculationBrian Campbell
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-23Remove a comment that breaks Isabelle buildThomas Bauereiss
With the new comment syntax, Isabelle seems to barf on that comment, apparently due to the backslashes.
2018-12-22Added RISC-V fence.tsoShaked Flur
2018-12-20RISVC model is now at https://github.com/rems-project/sail-riscv . Remove it ↵Robert Norton
and tests.
2018-12-19Coq: handle pairs of ranges (and other existential types) properlyBrian Campbell
(Needed for current CHERI.)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 11:11:08 +0000