summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-04-27Cheri ISA change in CTestSubset -- ignore sealed bits when testing for ↵Robert Norton
subset (aids garbage collection).
2018-04-26Add riscv SV39 page-table walk.Prashanth Mundkur
2018-04-26Ensure riscv interrupt delegation does not reduce current privilege.Prashanth Mundkur
2018-04-26Fix bug introduced in alignment check.Prashanth Mundkur
2018-04-26Lem: Add Size class annotations for nested bitvector typesThomas Bauereiss
2018-04-26Initial support for faults of writes to physical addresses.Prashanth Mundkur
2018-04-26Initial support for faults of reads to physical addresses.Prashanth Mundkur
2018-04-26Fix bug in rewriting of loopsThomas Bauereiss
Take into account existential types when determining bounds for the loop variable
2018-04-26Avoid adding explicit type annotations with generated type variablesThomas Bauereiss
2018-04-26Make effect propagation in rewriter more efficientThomas Bauereiss
Use non-recursive fix_eff_exp instead of recursive propagate_exp_effect, assuming that the effects of subexpressions have already been fixed by the recursive calls of the rewriter.
2018-04-26Lazily evaluate debugging messagesThomas Bauereiss
This is meant to increase performance; for example, generating debug messages that include pretty-printed expressions can be very costly, if those expressions are complex (e.g. deeply nested E_internal_plet nodes representing a long sequence of monadic binds).
2018-04-26Add a new SHARE_DIR argument to use when doing opam build. For non-opam ↵Robert Norton
builds this defaults to git root.
2018-04-26Make ocamlbuild assume lem is in path instead of relative to current directory.Robert Norton
2018-04-26Fix apply_header target with location of LICENSE file.Robert Norton
2018-04-26Opam packaging: add install and uninstall targets and code to find various ↵Robert Norton
files in installed location.
2018-04-26Remove obsolete mips/cheri rules from sail makefile. These are now built in ↵Robert Norton
their respective subdirectories.
2018-04-25Simplify subtyping checkAlasdair Armstrong
This should make subtyping work better for tuples containing constrained types. Removes the intermediate type-normal-form representation from the subtyping check, and replaces it with Env.canonicalize from the canonical branch.
2018-04-25Start working on documentationAlasdair Armstrong
2018-04-24Add some explanations to free monad documentationThomas Bauereiss
2018-04-23Make riscv build depend on Makefile updates.Prashanth Mundkur
2018-04-23Add riscv PTE definitions and access control checks.Prashanth Mundkur
2018-04-23Merge branch 'rmn30_latex' into sail2Robert Norton
2018-04-23Add a cheri128_trace target.Robert Norton
2018-04-23Fix a discrepancy with spec. about which register number is reported for ↵Robert Norton
permissions failure in CBuildCap.
2018-04-23Fix a problem with 128-bit setCapBounds function revealed by CBuildCap test ↵Robert Norton
-- an assertion failure that new bounds are exact. The address of the new cap should have address=base (i.e. offset=0) but this was not being set. This was not previously visible because all other uses of setCapBounds already have address=newBase when calling.
2018-04-20Fix a typo.Prashanth Mundkur
2018-04-20Add a riscv instruction printer for the execution log.Prashanth Mundkur
2018-04-20Some cleanup and comments.Prashanth Mundkur
2018-04-20Make building of Isabelle heap image optionalThomas Bauereiss
2018-04-20Allow instantiation of type or order type variables without kind declarationBrian Campbell
2018-04-20Have sign_extend in common Sail Lem library, use it and zero_extend inBrian Campbell
mono rewrites
2018-04-20Fix combined sign-extend-slice operationBrian Campbell
2018-04-19Fix minor typo.Prashanth Mundkur
2018-04-19Gloss over UInt/unsigned name difference in monomorphisationBrian Campbell
2018-04-19Fix bug with function being applied to tuplesAlasdair Armstrong
For some reason there was a desugaring rule that mapped f((x, y)) to f(x, y) in initial_check.ml, this prevented functions and constructors from being applied to tuples.
2018-04-19more nuanced discussion of generating HOL4 and CoqPeter Sewell
2018-04-18Remove obsolete comment.Prashanth Mundkur
2018-04-18Add interrupt prioritization and delegation.Prashanth Mundkur
2018-04-18Fix mideleg semantics after spec clarification from Andrew Waterman.Prashanth Mundkur
2018-04-18Use the generated num_of_E function for enum E instead of defining one by hand.Prashanth Mundkur
2018-04-18Add generated PDF of documentation draft --- comments welcomeThomas Bauereiss
Placed in lib/isabelle/manual/document.pdf Also fixed a few typos.
2018-04-18Update mono test scriptBrian Campbell
2018-04-18Add first draft of Isabelle library documentationThomas Bauereiss
2018-04-18Add a simple Hoare logic for sequential reasoning to the libraryThomas Bauereiss
2018-04-18Fix bug in pretty-printing loops to LemThomas Bauereiss
2018-04-18Add some lemmas about bitvectorsThomas Bauereiss
Also clean up some library functions a bit, and add some missing failure handling variants of division operations on bitvectors.
2018-04-18Move a few printing functions to sail_values.lemThomas Bauereiss
They are used in various specs and test cases.
2018-04-18Fix another reference to BK_natAlastair Reid
2018-04-18Add a test case for using enum to number function as a castAlasdair Armstrong
2018-04-18Fix build on linuxAlasdair Armstrong
Turns out that BSD sed is not a subset of GNU sed, GNU sed doesn't allow a space after the -i option.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-16 11:13:16 +0000