summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.)
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-18Check more carefully for recursive functions when generating LemThomas Bauereiss
Annotating non-recursive functions as recursive in Lem output is allowed, but will make Lem use "fun"/"function" commands when generating Isabelle output, which is much slower to process than "definiton".
2018-12-17Adapt Coq and termination measure support to typechecker changesBrian Campbell
Also output termination measures in Sail printer
2018-12-14Add some experimental support for non-lexical flow-typing rulesAlasdair Armstrong
Add a file nl_flow.ml which can analyse a block of Sail expressions and insert constraints for flow-typing rules which do not follow the lexical structure of the code (and therefore the syntax-directed typing rules can't do any flow-typing for). A common case found in ASL translated Sail would be something like function decode(Rt: bits(4)) = { if Rt == 0xF then { throw(Error_see("instruction")); }; let t = unsigned(Rt); execute(t) } which would currently fail is execute has a 0 <= t <= 14 constraint for a register it writes to. However if we spot this pattern and add an assertion automatically: let t = unsigned(Rt); assert(t != 15); execute(t) Then everything works, because the assertion is in the correct place for regular flow typing. Currently it only works for this specific use-case, and is turned on using the -non_lexical_flow flag
2018-12-14Add a few more tests for JenkinsAlasdair Armstrong
Some of the output from the tests scripts is odd on Jenkins, try to fix this by flushing stdout more regularly in the test scripts
2018-12-14Prepare for new release.Robert Norton
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-14Get real number tests working in OCaml/InterpreterAlasdair
2018-12-14A few additional testsAlasdair
2018-12-13Fix typo in boolean constraint desugaringAlasdair Armstrong
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-13Fixing rationals in Sail interpreter and OCamlAlasdair Armstrong
2018-12-13Add hooks to call cgen stub file for RISC-VAlasdair Armstrong
2018-12-13Add a stub file for future cgen generationsAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 04:32:14 +0000