summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-01-14Support some more unification casesThomas Bauereiss
2019-01-14Make rewriting of foreach loops for Lem more robustThomas Bauereiss
Bind loop bounds to type variables, and don't pull existential variables out of context
2019-01-14Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-13update READMEPeter Sewell
2019-01-13update README with current model reposPeter Sewell
2019-01-11Updates for sail-arm releaseAlasdair Armstrong
We want to ensure that no_devices.sail and devices.sail have the same effect footprint, because with a snapshot-type release in sail-arm, we can't rebuild the spec with asl_to_sail every time we switch from running elf binaries to booting OS's. This commit allows registers to have arbitrary effects, so registers that are really representing memory-mapped devices don't have to have the wmem/rmem effect.
2019-01-10Fixes so 8.5 with vector instructions compiles to CAlasdair Armstrong
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-08Improvements for v85Alasdair Armstrong
2019-01-04C library: fix fprintf warnings in lib/elf.cAlastair Reid
2019-01-04Arm ElfMain: fix minor type errorsAlastair Reid
I guess that Sail became a bit more strict about typechecking variables in the last few months.
2019-01-03Make sure to close file handles when printing error messagesAlasdair Armstrong
2019-01-03Comment out bisect coverage in ocamlbuild filesAlasdair Armstrong
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-26More cleanupAlasdair Armstrong
Remove unused name schemes and DEF_kind
2018-12-26Some cleanupAlasdair Armstrong
2018-12-26Add makefile target for building with Bisect coverageAlasdair Armstrong
2018-12-26More error messages improvmentsAlasdair Armstrong
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-22Improve error messages and debuggingAlasdair Armstrong
Work on improving the formatting and quality of error messages When sail is invoked with sail -i, any type errors now drop the user down to the interactive prompt, with the interactive environment being the environment at the point the type error occurred, this means the typechecker state can be interactively queried in the interpreter to help diagnose type errors.
2018-12-21Simplify boolean existentialsAlasdair Armstrong
Remove redundant variables in boolean existentials. A situation can occur during re-writing when patterns are re-written into simpler guarded patterns, with the guard containing a large conjunction. Often those individual conjuncts have no meaning for flow typing, but we'll still generate a large conjunct bool('p & 'q & 'r & 's ...) for the guard. Now we can simplify that return type by combining all the type variables that don't give us any information into a single one, which improves performance as we can avoid passing all those variables to the constraint solver.
2018-12-21Expand synonyms in generated mapping val-specsAlasdair Armstrong
This ensures that mappings round-trip through the pretty-printer and parser unchanged Remove guarded_pats rewrite from C compilation. It causes a large increase in compilation time due to how it interacts with flow typing/pattern literal re-writing/and sizeof-rewriting
2018-12-20Make sure sail -v prints useful version infoAlasdair Armstrong
2018-12-20Fix monomorpisation tests with typechecker changesAlasdair Armstrong
Add an extra argument for Type_check.prove for the location of the prove call (as prove __POS__) to help debug SMT related issues
2018-12-20RISVC model is now at https://github.com/rems-project/sail-riscv . Remove it ↵Robert Norton
and tests.
2018-12-19Improve sizeof rewriting performanceAlasdair Armstrong
Simply constraints further before calling Z3 to improve performance of sizeof re-writing.
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-18Ensure type-variables have consistent namesAlasdair
Type variables can now be lexically scoped and shadow each other like normal variables, rather than being required to be unique. This means we can use identifier names to choose names for type variables in a way where we can assume they remain consistent between type-checker runs. This means that re-writer steps can lift types out of annotations in E_aux constructors and put them directly as syntactic annotations in the AST - this should enable more robust rewrite steps. Also fix RISC-V lem build w/ flow typing changes
2018-12-18Revert "Experiment with generating type variable names in a repeatable way"Alasdair
This reverts commit 4d8a4078990a00ffdc018bc8f5d4d5e3dcf6527d.
2018-12-18Experiment with generating type variable names in a repeatable wayAlasdair Armstrong
This results in much better error messages, as we can pick readable names that make sense, and should hopefully make the re-writer more robust.
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-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-18Store function instantiation information within annotations, so we don'tAlasdair
have to recompute it, which can be very expensive for very large specifications Also additional flow typing and fixes for boolean type variables
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 10:57:40 +0000