summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2019-06-13Add AST for greater-than and less-than constraintsBrian Campbell
Mostly to make constraints sent to the SMT solver and Coq nicer, but also makes it easy to remove uninformative constraints in the Coq back-end.
2019-06-12Handle partial matches in guarded pattern rewriteThomas Bauereiss
Add a fallthrough case that fails to potentially partial pattern matches. This also helps to preserve any guard in the final match case, which might be needed for flow typing (see the discussion on issue #51). TODO: Merge with the MakeExhaustive rewrite, which currently does not support guarded patterns.
2019-06-12SMT: Fix missing case for append builtinAlasdair Armstrong
2019-06-11Coq: improve readability of types filesBrian Campbell
Also get rid of the notation warnings for single element records.
2019-06-10Add well-formedness check for type schemes in valspecs.Brian Campbell
Fixes #47. Also adjust the nexp substitution so that the error message points to a useful location, and replace the empty environment with the initial environment in a few functions that do type checking to ensure that the prover is set up (which may be needed for the wf check).
2019-06-08Workaround for OCaml bytecode memory bugBrian Campbell
See <https://github.com/ocaml/ocaml/issues/8699#issuecomment-499108873>, tested on 4.07.1 and 4.08+rc2.
2019-06-06SMT: Rename some functions to make usage clearerAlasdair Armstrong
2019-06-06Fix tdiv_int and tmod_int bindings for LemThomas Bauereiss
Also rename them for uniformity with other backends.
2019-06-06Add arith_shiftr to C and OCaml librariesThomas Bauereiss
2019-06-06SMT: Add function to de-serialise serialised modelAlasdair Armstrong
2019-06-06Add an option to pre-compile the axiomatic model for SMTAlasdair Armstrong
2019-06-06Update aarch64_small hgen filesAlasdair Armstrong
2019-06-05Add some regression testsAlasdair
2019-06-05Fix: Make sure we check Jib types match for operators before optimizingAlasdair Armstrong
Insert coercions for AV_cval if neccessary Simplify any n in 2 ^ n, to make sure we can always evaluate 2 ^ n when n is a constant before passing it to the SMT solver.
2019-06-05Coq: fix type alias expansion in constraintsBrian Campbell
2019-06-04Make sure aarch64_small can generate Jib for SMTAlasdair Armstrong
Add a test case for this
2019-06-04Remove unused AST constructorAlasdair Armstrong
Clean up ott grammar a bit
2019-06-04SMT: Add a fuzzing tool for the SMT builtinsAlasdair Armstrong
2019-06-03Coq: support non-exhaustive pattern rewrite for exception handlingBrian Campbell
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-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-28Coq: don't output complex bool types at let expressionsBrian Campbell
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-23Coq: support loops which update richly typed variablesBrian 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-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: 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-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: remove unhelpful type printing restriction on early returnsBrian Campbell
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-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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 14:39:35 +0000