summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-25Coq: clean up some formattingBrian Campbell
2019-10-25Coq: make sure solver can't accidentally use recursive definitionsBrian Campbell
2019-10-25Allow interactive commands to be setup outside isail.mlAlasdair Armstrong
can use Interactive.register_command to set up a new interactive command, which allows commands to be set up near where the functionality they interact with is defined, e.g. the ast slicing commands are registered in Slice.ml. Also allows help messages to be generated in a consistent way.
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-12Remove unnecessary copies of non-existant files in ocaml backend.Robert Norton
2019-09-02Enable part of a test that's been fixed recently.Brian Campbell
2019-09-02Coq: add properly checked subrange update, reduce importsBrian Campbell
2019-08-30Add a couple of overlooked testsBrian Campbell
2019-08-29Clean up some mono testsBrian 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-22additional option to tweak Coq output to support user-defined monad:pes20
-coq_alt_modules2 <filename> provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default definitions of MR and M monads
2019-08-20Merge branch 'sail2' of github.com:rems-project/sail into sail2pes20
2019-08-20add -coq_alt_modules option to override the default imported modulespes20
2019-08-20add -coq_alt_modules option to override the default imported modulespes20
2019-08-20add -coq_alt_modules option to override the default imported modulespes20
2019-08-19Coq: add bools_of_bits_nondet and friends to libraryBrian Campbell
2019-08-14Update testsThomas Bauereiss
2019-08-14Add a mono rewrite for (ones(n) @ zeros(m))Thomas Bauereiss
2019-08-14Inline reg_deref in Lem outputThomas Bauereiss
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-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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 08:10:55 +0000