summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-05-31Add SMT related things to libsail fileAlasdair Armstrong
2019-05-31Change specialization interface slightlyAlasdair Armstrong
2019-05-30Implement ones builtin in sail_lib and add to interpreter. However currently ↵Robert Norton
this is implemented in lib/vector_dec.sail as sail function that calls not_vec on sail_zeros.
2019-05-30Set interpreter builtin for truncateLSB.Robert Norton
2019-05-29Some minor grammar fixes in internals.mdAlasdair Armstrong
2019-05-29Fix some typosAlasdair Armstrong
2019-05-29Add some Sail internals documentationAlasdair Armstrong
2019-05-29Coq: more solver improvementsBrian Campbell
- don't clear boolean local definitions - we need those now - some boolean disjunction fixes
2019-05-29Coq: need a proof for _shr32Brian Campbell
2019-05-29SMT: Make bitvector equality work between vectors of different lengthsAlasdair Armstrong
2019-05-29SMT: Fix sail_truncate and sail_mask for unusual argument typesAlasdair Armstrong
2019-05-29Fix sail_truncate error message in SMTAlasdair Armstrong
2019-05-28Fix typechecking test expected errorAlasdair Armstrong
2019-05-28Coq: more constraint solvingBrian Campbell
- add division lemma - deal with some awkward \/ constraints from asl_parser - try simple integer comparison proofs before omega (which can blow up on trivial properties in large contexts)
2019-05-28Coq: don't output complex bool types at let expressionsBrian Campbell
2019-05-28Just build lem in aarch64_small testAlasdair Armstrong
2019-05-28SMT: Add min and max functionsAlasdair Armstrong
Allow conversion between int(n) and int in smt_conversion
2019-05-28Make sure single clause functions with top-level guards work correctlyAlasdair Armstrong
2019-05-24Add a :thin_slice command to isail to isolate a given set of functionsBrian Campbell
2019-05-24Coq: support if-then-throw typechecking special caseBrian Campbell
2019-05-24Coq: switch to computable versions of BBV shiftsBrian Campbell
2019-05-23Coq: support loops which update richly typed variablesBrian Campbell
2019-05-23Coq: solve some division constraintsBrian Campbell
2019-05-23Coq: define the names from the Sail real libraryBrian Campbell
2019-05-23Fix bug in slice_maskThomas Bauereiss
2019-05-22Coq: tweak disjunctions tactic with subst to support more constraintsBrian Campbell
2019-05-22Coq: replace inferrable integer arguments with _ at more typesBrian Campbell
Previously we only checked at atom, now use destruct_atom_nexp to pick up implicit too.
2019-05-22Use opam instructions in INSTALL.mdAlasdair Armstrong
Move the instructions to build everything from source to the wiki
2019-05-22Fix: Update INSTALL.md with opam switch instructionsAlasdair Armstrong
2019-05-22Move Util.warn to Reporting, and make it take the location as a parameterAlasdair Armstrong
Also add a $suppress_warnings directive that ensures that no warnings are generated for a specific file.
2019-05-21SMT: Use a separate constructor for memory read variablesAlasdair Armstrong
We want to ensure simplication can treat these separately so we don't accidentally simplify away dependencies between reads and write addresses.
2019-05-21Fix: undefined_nat test for interpreterAlasdair Armstrong
2019-05-21SMT: Add control flow node numbers to memory events to track program orderAlasdair Armstrong
Add path conditions to memory events Allow simplication of generated SMT based on constructor kinds
2019-05-21Lem: Fix bug in generation of val-specsThomas Bauereiss
Used to output duplicate type variables in some cases.
2019-05-21Coq: remove premature unfolding of local definitionsBrian Campbell
2019-05-21Coq: introduce autocasts at variablesBrian Campbell
Usually we do this at function applications and casts, but occasionally a variable is used at a different type.
2019-05-20Coq: fix property extraction bug, solve some constraints involving setsBrian Campbell
2019-05-20Revert "Add constraints to undefined vector functions to ensure that lengths ↵Brian Campbell
are" This reverts commit 8bed4e4ef414f93e02f28f0e5eb223a855ba3d14.
2019-05-20Filter termination measures during slicingBrian Campbell
2019-05-20Speed up graph construction by always keeping graph in normalized formBrian Campbell
Only checks the leaves that were added in each add_edge/add_edges call. Slicing bits of the 8.5 model went (for me) from intractable to about one second.
2019-05-20Coq: add some missing autocasts, avoid unnecessary patterns in letsBrian Campbell
The former is useful when a bitvector variable is cast to an equivalent length, and the latter is easier for Coq's unification to deal with.
2019-05-19Coq: add signed bitvector to integer function that doesn't need >0 constraintBrian Campbell
2019-05-19Coq: remove unhelpful type printing restriction on early returnsBrian Campbell
2019-05-19Coq: proper definitions for some undefined value functionsBrian Campbell
That is, undefined_bitvector, undefined_unit, internal_pick.
2019-05-19Add constraints to undefined vector functions to ensure that lengths areBrian Campbell
sane, and an incomplete check on undefined literals.
2019-05-17SMT: Finish adding all memory builtins from lib/regfp.sailAlasdair Armstrong
2019-05-16Fix: Add a feature symbol for new constant type variable syntaxAlasdair Armstrong
2019-05-16SMT: Tweak SMT generation interfaceAlasdair Armstrong
Expose AST -> Jib compilation function for SMT, and smt_header function Functorise the optimiser so it can output the SMT definitions to any data structure
2019-05-16SMT: Improve simplification for generated SMTAlasdair Armstrong
Generate addresses, kinds, and values separately for read and write events. Add an mli interface for jib_smt.ml
2019-05-1594f445 introduced a new name for _ref_deref, add it to the effect rewritingBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 19:31:19 +0000