summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-08-14Coq library work for proofs:Brian Campbell
* rename state fields to avoid clash with regstate type * use rewriting to automate some proofs
2019-08-13Coq: definitions for cheri128 modelBrian Campbell
Add count_leading_zeros, and correct a precedence error in min/max.
2019-08-13Coq: fix non-exhaustive pattern match failure in riscv duopodBrian Campbell
2019-08-08Fix machine words againAlasdair Armstrong
2019-08-08Update machine wordsAlasdair Armstrong
2019-08-08Fix bitvectorToFromInterpAlasdair Armstrong
2019-08-08Use bitToFromInterp in bitvectorToFromInterpAlasdair Armstrong
2019-08-08Add same to bitlist representationAlasdair Armstrong
2019-08-08Add bitvectorToFromInterpAlasdair Armstrong
2019-08-05Print effect sets in alphabetical orderAlasdair Armstrong
2019-08-05Remove escape/pure effect restriction for mappingAlasdair Armstrong
2019-08-02Fix all warnings (except for two lem warnings)Alasdair Armstrong
Remove P_record as it's never been implemented in parser/typechecker/rewriter, and is not likely to be. This also means we can get rid of some ugliness with the fpat and mfpat types. Stubs for P_or and P_not are left as they still may get added to ASL and we might want to support them, although there are good reasons to keep our patterns simple. The lem warning for while -> while0 for ocaml doesn't matter because it's only used in lem, and the 32-bit number warning is just noise.
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-31Coq: Update barrier definitionsBrian Campbell
2019-07-31Coq: tweak Hoare proofs a littleBrian Campbell
2019-07-31Coq: reasoning for until loopsBrian Campbell
Loops measures are now abstracted over the variables so that they can be used in proofs. Add total Hoare logic rules for until.
2019-07-31Fix failing SMT testAlasdair Armstrong
2019-07-31Revert "Need to separate out the 0.10 lem library from upcoming 0.11"Alasdair Armstrong
This reverts commit 3fb4cf236c0d4b15831576faa45c763853632568.
2019-07-31Merge branch 'sail2' into union_barrierAlasdair Armstrong
2019-07-31Updates to function unfolding to support scattered definitionsAlasdair Armstrong
2019-07-31Remove redundant ifdef and run SMT tests by defaultAlasdair Armstrong
2019-07-31Change platform_barrier so it doesn't care about it's argument typeAlasdair Armstrong
2019-07-29Coq: add state monad version of while/until loops and lifting resultsBrian Campbell
2019-07-29Add type check after descattering to keep type environments up to dateBrian Campbell
2019-07-25Some documentation of mappings and string matchingJon French
2019-07-25Update Coq barrier definitionBrian Campbell
2019-07-25Basic port of proof machinery to CoqBrian Campbell
2019-07-18Need to separate out the 0.10 lem library from upcoming 0.11Alasdair Armstrong
Unlike the prompt-monad change I don't see a way to do this easily purely on the model side Make sure a64_barrier_type and domain aren't visible for RISC-V isabelle build
2019-07-18Add a option to check for a feature symbolAlasdair Armstrong
2019-07-18Add a feature flag for barrier type changeAlasdair Armstrong
Fix SMT mem_builtin test case
2019-07-18Update aarch64_small to build with new barriersAlasdair Armstrong
Make sure barrier changes don't affect other models for now
2019-07-18Support DMB/DSB domainsShaked Flur
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-07-15Add a fast path to speed up platform_read_ram: use fast_read_ram if read is ↵Robert Norton
8 bytes or less to avoid cost of using GMP integers (including free/malloc).
2019-07-11Make sure we do constant-fold primitives howeverAlasdair Armstrong
Previous change would stop all things defined externally from being folded, which was overly strict. We do want to allow folding for shared primitives, and can use the set of safe_primops in the interpreter for this.
2019-07-11Make sure constant folding won't fold external definitions that also have ↵Alasdair Armstrong
sail definitions Definitions can be made external on a per-backend basis, so we need to make sure constant folding doesn't inline external functions that have sail definitions for backends other than the ones we are currently targetting
2019-07-04Add coq builtin for concat_str (copied from mips prelude).Robert Norton
2019-07-04Bump opam version.Robert Norton
2019-07-03Consider references in topological sortingThomas Bauereiss
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-28Monomorphisation: add some alternative names for ones and zero_extend as ↵Robert Norton
used in risc-v spec.
2019-06-28ToFromInterp backend: always wrap typ arg values in a function, fixes option ↵Jon French
types in riscv
2019-06-28Add a warning for potentially unsafe castsAlasdair
2019-06-27SMT: Add a reverse endianness function and fix some bugsAlasdair Armstrong
2019-06-27Coq: less constrained version of slice for ARM modelBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 08:48:25 +0000