summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
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-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-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.
2018-12-18Merge branch 'sail2' into monadsThomas Bauereiss
2018-12-17Changes for ASL parserAlasdair Armstrong
2018-12-17Adapt Coq and termination measure support to typechecker changesBrian Campbell
Also output termination measures in Sail printer
2018-12-14Add truncateLSB builtin useful for implementing Cheri Concentrate. Also add ↵Robert Norton
bool_of_bit and bit_of_bool in sail_lib
2018-12-13Remove redundant zero extensions more aggressively in mono rewritesThomas Bauereiss
subrange_subrange_concat does a zero extension internally, so another zero extension of its result is redundant and can lead to a type error in Lem (because Lem's type system cannot calculate the length of the intermediate result of subrange_subrange_concat).
2018-12-13Fix issue with sizeof-rewriting and monomorphisationAlasdair Armstrong
Sizeof-rewriting could introduce extra arguments to functions that instantiate_simple_equations could fill in with overly complicated types, causing unification to fail when building lem.
2018-12-13Merge remote-tracking branch 'origin/sail2' into asl_flowAlasdair
2018-12-12Move much of recursive function termination to a rewriteBrian Campbell
It now includes updating the effects so that morally pure recursive functions can be turned into this impure termination-by-assertion form.
2018-12-11Fix all tests with type checking changesAlasdair Armstrong
2018-12-11Initial attempt at using termination measures in CoqBrian Campbell
This only applies to recursive functions and uses the termination measure merely as a limit to the recursive call depth, rather than proving the measure correct.
2018-12-11Fix most remaining tests on branchAlasdair
2018-12-10Various changes:Alasdair Armstrong
* Improve type inference for numeric if statements (if_infer test) * Correctly handle constraints for existentially quantified constructors (constraint_ctor test) * Canonicalise all numeric types in function arguments, which triggers some weird edge cases between parametric polymorphism and subtyping of numeric arguments * Because of this eq_int, eq_range, and eq_atom etc become identical * Avoid duplicating destruct_exist in Env * Handle some odd subtyping cases better
2018-12-03Add Write_mem event/outcome without tagThomas Bauereiss
The inter-instruction semantics is responsible for correctly handling memory writes without tags; the lifting to the state monad handles it as writing a value with a zero tag bit.
2018-12-03Make names of memory r/w events more consistentThomas Bauereiss
Use E_read_memt for reading tagged memory, as in sail2_impl_base.lem, and rename E_write_mem to E_write_memt, since it always writes a tag.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:02:35 +0000