summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-02-01Fix missing typedef cases in OCaml outputAlasdair
2019-02-01Add test cases for integer synonymsAlasdair
2019-02-01Expand integer synonymsAlasdair Armstrong
2019-02-01Add tracing instrumention for SMTAlasdair Armstrong
Fix pretty printer bug
2019-02-01Use same license as Sail for emacs modeAlasdair Armstrong
2019-02-01Merge pull request #29 from thoughtpolice/patch-1Alasdair Armstrong
sail-mode: add ELPA metadata
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-31sail-mode: add ELPA metadataAustin Seipp
This adds ELPA metadata, which should allow authorship of MELPA packages for Sail mode. Signed-off-by: Austin Seipp <aseipp@pobox.com>
2019-01-31Fix an unnecessary cast insertion on assignmentsBrian Campbell
2019-01-31Turn on cast insertion for -lem_mwords and revert b826df25Brian Campbell
now that cast insertion can handle RISC-V Also inserts specs for casts in they're not present
2019-01-31Drop type annotations in top-level nexp rewriting in favour of valspecsBrian Campbell
otherwise the valspec rewriting will be inconsistent with the type annotation. Note that the type checker will have introduced valspecs where necessary.
2019-01-31Make cast insertion handle more complex nexps and pushing casts into blocksBrian Campbell
# Conflicts: # src/monomorphise.ml
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-31Further restrict attention to Int kidsThomas Bauereiss
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-30Cache compilation results to improve build times for repeated buildsAlasdair
2019-01-29Fixes for full v8.5Alasdair Armstrong
2019-01-29Add an option to crudely slice a function out of a Sail modelBrian Campbell
Not ideal because it keeps everything that's not a function, but good enough for quick tests extracted from arm.
2019-01-29Monomorphisation: add missing tyvar substitution during constrant propagationBrian Campbell
2019-01-29Add a few more type annotations after mono rewritesThomas Bauereiss
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
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-29Monomorphisation: restrict our attention to Int kidsBrian Campbell
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-25Coq: add enough to generate some output for arm-v8.5-aBrian Campbell
Now supports mutual recursion, configuration registers (in the same way as Lem), boolean constraints (but produces some ugly stuff that the solver can't handle).
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-24Make recheck_defs_without_effects restore old flag properlyBrian 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-23Make rewriting of E_assign a bit more robustThomas Bauereiss
2019-01-23Add another flow-typing case for E_internal_pletThomas Bauereiss
Copied from a corresponding case for E_block, so that this flow typing still gets picked up after E_block has been rewritten away.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 15:13:42 +0000