summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2019-11-21Implement -cycle-limit option for OCaml emulator similar to one for C.Robert Norton
2019-11-20Coq: port a couple of definitions from Isabelle for address translation specBrian Campbell
2019-11-14Update location of sail2_instr_kinds.lemRobert Norton
2019-11-14Perform isabelle check only when heap-img rule is used to avoid calling opam ↵Robert Norton
(which might not be present).
2019-11-13Coq: more proof supportBrian Campbell
- add state versions of foreach combinators - support dependent sumbool pattern matching (i.e., those where the property is actually used) - add rewriting congruence rules, state monad lifting rules, and invariant proof rules for these
2019-11-04Coq: compatiblity with 8.10 as well as 8.9Brian Campbell
2019-10-25Coq: make sure solver can't accidentally use recursive definitionsBrian Campbell
2019-10-24Coq: use `abstract` to separate out proofs from definitionsBrian Campbell
- requires fixpoint definitions containing proofs to be processed in proof mode (due to a bug in Coq), so change libraries and pretty printing to do that - adjust some lemmas to avoid extra evars
2019-10-18Coq: tweak a state monad lifting rule to improve performanceBrian Campbell
2019-10-17Allow generating C that doesn't hard code any librariesAlasdair Armstrong
2019-10-16Now builds arm address translation with clang -target aarch64-none-eabiAlasdair Armstrong
Some builtins need properly implementing still Use modified spinlock implementation from hafnium with stdatomic, rather than assembly
2019-10-16Make nostd Sail arena allocator thread safe (maybe)Alasdair
2019-10-15More work on bare-metal SailAlasdair Armstrong
2019-10-14Add -Ofixed_int and -Ofixed_bits to assume fixed-precision ints and ↵Alasdair Armstrong
bitvectors in C Assumes a Sail C library that has functions with the right types to support this. Currently lib/int128 supports the -Ofixed_int option, which was previously -Oint128. Add a version of Sail C library that can be built with -nostdlib and -ffreestanding, assuming the above options. Currently just a header file without any implementation, but with the right types
2019-10-02Coq: generate decidable equality instances for variant typesBrian Campbell
It only produces them when necessary (because some types do not have decidable equality due to embedded proofs). Also add trivial instance for the unit type.
2019-10-02Coq: limited support for existentially-typed tuplesBrian Campbell
- in particular at monadic interfaces (i.e., sufficient for instruction ast types) - see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an example that's not currently supported - generate definitions for type-level Bool definitions (i.e., predicates)
2019-09-19Change Coq Hoare logic rules to produce nicer preconditionsBrian Campbell
In particular, shift state lambdas outside of if/match/let which avoids unnecessary abstraction/applications. Add more rules to the tactic.
2019-09-19Expand Coq Hoare logic and congruence rules to more operatorsBrian Campbell
Also tweak the informative and/or boolean definitions so that they use the same proofs in both monads.
2019-09-02Coq: add properly checked subrange update, reduce importsBrian Campbell
2019-08-29Turn the two abs_int declarations into overloadsBrian Campbell
(otherwise Sail uses the type from one and the extern from the other)
2019-08-22Coq: tactics to do rewrites under state monad, simple wp computationBrian Campbell
2019-08-19Coq: add bools_of_bits_nondet and friends to libraryBrian Campbell
2019-08-14Use bitvector type in mono rewritesThomas Bauereiss
Also don't require a previously declared default vector indexing order in vector_dec.sail.
2019-08-14Fix bug in mono rewritesThomas Bauereiss
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-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-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-31Merge branch 'sail2' into union_barrierAlasdair 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-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 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-16Fix all remaining tests for this branchAlasdair
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-04Add coq builtin for concat_str (copied from mips prelude).Robert Norton
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
2019-06-21Coq: even more robust handling of unknown goalsBrian Campbell
2019-06-21Coq: better handling of unknown constraintsBrian Campbell
Move the tactic forward so that preprocessing can't try silly things, simpl to get rid of embedded proofs.
2019-06-20Coq: avoid some unnecessary reduction in the constraint solverBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-16 00:37:47 +0000