summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
2019-08-02Fix up some edge cases with the bitvector/polyvector splitBrian Campbell
Mostly in the Coq backend, plus a few testcases that use bitvector builtins on poly-vectors (which works on some backends, but not Coq). Also handle some additional list inclusion proofs in Coq.
2019-08-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-08-01Merge remote-tracking branch 'origin/rv_duopod_fix' into sail2Alasdair Armstrong
Fixes #53
2019-07-31Fix failing SMT testAlasdair Armstrong
2019-07-31Remove redundant ifdef and run SMT tests by defaultAlasdair Armstrong
2019-07-18Add a feature flag for barrier type changeAlasdair Armstrong
Fix SMT mem_builtin test case
2019-07-17Add another test caseAlasdair Armstrong
2019-07-16Fix all remaining tests for this branchAlasdair
2019-07-16Get monomorphisation tests working with separate bitvectorsAlasdair Armstrong
2019-07-16Merge remote-tracking branch 'origin/sail2' into separate_bvAlasdair Armstrong
2019-06-30Fix bug with toplevel pattern in RISC-V duopodAlasdair
Do this by making sure that generic pattern literal re-writing gets applied to top-level function clauses. This requires re-ordering the rewrites for most backends otherwise they break, which hopefully wo anything. After doing this re-ordering I had to turn off casting when rewriting bitvector patterns, otherwise insane things can happen.
2019-06-27SMT: Add a reverse endianness function and fix some bugsAlasdair Armstrong
2019-06-25SMT: Add another case to appendAlasdair Armstrong
2019-06-21Coq: add missing property derivation casts for effectful expressionsBrian Campbell
These don't appear much, but are now showing up in the sail-arm model due to an innocent change elsewhere.
2019-06-21Coq: be more careful when dealing with wildcard argument patternsBrian Campbell
If they're merged with a type variable then we still need to name the argument so that it can be used in other types.
2019-06-20Handle more uses of mutable variables during monomorphisation cast insertionBrian Campbell
In particular, bitvector subrange updates work with this version.
2019-06-19Make C emulator exit with failure for uncaught exception. Make special case ↵Robert Norton
for 'exception.sail' test that deliberately exits with uncaught exception.
2019-06-19Monomorphisation improvements for aarch64_smallBrian Campbell
- additional rewrites (signed extend of subrange@zeros, subrange assignment, variants with casts) - drop # from new top-level type variables (e.g., n_times_8) so that the rewriter knows that they're safe to include in casts - add casts in else-branches when only one possible value for a size is left - add casts when assertions force a size to be a particular value - don't use types to detect set constraints in analysis because we won't know which part of the assertion should be replaced - also use non-top-level type variables when simplifying sizes in analysis (useful when it can from pattern matching on an ast) - cope with repeated int('n) in a pattern match (!)
2019-06-18Fix two SMT test casesThomas Bauereiss
2019-06-18Update test casesThomas Bauereiss
2019-06-18Implement count_leading_zeros in LemThomas Bauereiss
2019-06-17Implement a count_leading_zeros builtin for ocaml and c. This may be a ↵Robert Norton
slight performance improvement and keeps compatibility with smt backend that already had a builtin for this because it can't handle the loop in the sail version. Will need implementations for prover backends.
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-06Fix aarch64_small testAlasdair Armstrong
2019-06-06Add arith_shiftr to C and OCaml librariesThomas Bauereiss
2019-06-05Add some regression testsAlasdair
2019-06-04Make sure aarch64_small can generate Jib for SMTAlasdair Armstrong
Add a test case for this
2019-06-04Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-06-04SMT: Add a fuzzing tool for the SMT builtinsAlasdair Armstrong
2019-06-03Test case for previous commitBrian 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-28Fix typechecking test expected errorAlasdair Armstrong
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-24Coq: support if-then-throw typechecking special caseBrian Campbell
2019-05-23Fix bug in slice_maskThomas Bauereiss
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-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-17Experiment with making vector and bitvector distinct typesAlasdair Armstrong
Only change that should be needed for 99.9% of uses is to change vector('n, 'ord, bit) to bitvector('n, 'ord), and adding $ifndef FEATURE_BITVECTOR_TYPE type bitvector('n, dec) = vector('n, dec, bit) $endif for to support any Sail before this Currently I have all C, Typechecking, and SMT tests passing, as well as the RISC-V spec building OCaml and C completely unmodified.
2019-05-17SMT: Finish adding all memory builtins from lib/regfp.sailAlasdair Armstrong
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-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-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-10SMT: Implement memory events for read_mem and write_memAlasdair
Generate SMT where the memory reads and writes are totally unconstrained, allowing additional constraints to be added that restrict the possible reads and writes based on some memory model.
2019-05-10SMT: Experiment with symbolic memory reads and writesAlasdair Armstrong
2019-05-10SMT: Fix error in get_pathcondAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 20:30:29 +0000