summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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-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-17Allow generating C that doesn't hard code any librariesAlasdair Armstrong
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-12Remove unnecessary copies of non-existant files in ocaml backend.Robert Norton
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-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-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-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: 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-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-29Add type check after descattering to keep type environments up to dateBrian 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-18Support DMB/DSB domainsShaked Flur
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-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-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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 12:01:01 +0000