summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-28Coq: label fixpoint bodies, tweak spacingBrian Campbell
2019-10-28Some C backend refactoringAlasdair
Make it so that jib_compile.ml never relies on specific string encodings for various constructs in C. Previously this happened when monomorphisation occured for union constructors and fields, i.e. x.foo -> x.zfoo_bitsz632z7 Now identifiers that can be modified are represented as (id, ctyp list) tuples, so we can keep the types x.foo -> x.foo::<bits(32)> This then enables us to do jib IR -> jib IR rewrites that modify types In particular there is now a rewrite that removes tuples as an IR->IR pass rather than doing it ad-hoc in the C code generation, although this is not on by default Note that this change seems to have triggered an Ott bug so jib.lem is now checked in and not generated from Ott
2019-10-25Remove global symbol generatorAlasdair
Rather than having a global symbol generating function gensym used throughout the C backend, instead 'generate' them as needed like: let (gensym, reset_gensym_counter) = symbol_generator "gs" This just makes things a bit neater and means we can reset the counter between definitions in jib_compile without worrying about other modules relying on global uniqueness
2019-10-25Refactor Jib IR pretty printerAlasdair Armstrong
2019-10-25Some more interpreter tweaksAlasdair Armstrong
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 11:40:07 +0000