summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2019-05-15Coq: constraint solving for aarch64Brian Campbell
Also split out main solver tactic to make debugging a little easier.
2019-05-14SMT: Allow printing SMT with an optional variable prefixAlasdair Armstrong
Allows us to mix generated SMT for two separate threads without name clashes, however we do want to be able to share datatypes so they are not prefixed. Currently the pretty-printer adds the prefix but we may want a smt_def -> smt_def renaming function instead.
2019-05-14Fix test case for previous commitAlasdair Armstrong
Previous commit changed the bitfield desugaring very slightly which this test case relied upon.
2019-05-14Various bugfixesAlasdair Armstrong
Since we have __deref to desugar *x in this file (as it's the one file everything includes) we might as well add a __bitfield_deref here too, for the bitfield setters. Make sure undefined_nat can be used in C Both -memo_z3 and -no_memo_z3 were listed as default options, now only -no_memo_z3 is listed as the default.
2019-05-14Merge branch 'smt_experiments' into sail2Alasdair Armstrong
2019-05-14SMT: Add comment explaining path conditionalsAlasdair Armstrong
2019-05-14Fix: Issue a warning for any unrecognised directiveAlasdair Armstrong
Fixes #46
2019-05-14Add feature that allows functions to require type variables are constantAlasdair Armstrong
can now write e.g. forall (constant 'n : Int) rather than forall ('n: Int) which requires 'n to be a constant integer value whenever the function is called. I added this to the 'addrsize variable on memory reads/writes to absolutely guarantee in the SMT generation that we don't have to worry about the address being a variable length bitvector.
2019-05-13Merge branch 'sail2' into smt_experimentsAlasdair
2019-05-13Parse dereferences in orderinary expressionsAlasdair
2019-05-13aarch64_small: correct cast_bool_bit/cast_bit_bool functionsJon French
Fixes issue with spurious alignment faults etc.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 16:59:10 +0000