summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2019-01-31Further restrict attention to Int kidsThomas Bauereiss
2019-01-30Cache compilation results to improve build times for repeated buildsAlasdair
2019-01-29Fixes for full v8.5Alasdair Armstrong
2019-01-29Add an option to crudely slice a function out of a Sail modelBrian Campbell
Not ideal because it keeps everything that's not a function, but good enough for quick tests extracted from arm.
2019-01-29Monomorphisation: add missing tyvar substitution during constrant propagationBrian Campbell
2019-01-29Add a few more type annotations after mono rewritesThomas Bauereiss
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-29Improve generation of initial register stateThomas Bauereiss
Define initial values for record types once instead of repeating them in the initial register state.
2019-01-29Monomorphisation: restrict our attention to Int kidsBrian Campbell
2019-01-28Lem: Be more careful about nexps occurring in the function signatureThomas Bauereiss
Don't ask Z3 to simplify them, as flow typing might lead to different results in different if-branches, for example, leading to type errors in Lem.
2019-01-25Monomorphisation: update a built-in nameBrian Campbell
2019-01-25Fix solution finding using SMT by looking for the right variableBrian Campbell
2019-01-25Coq: add enough to generate some output for arm-v8.5-aBrian Campbell
Now supports mutual recursion, configuration registers (in the same way as Lem), boolean constraints (but produces some ugly stuff that the solver can't handle).
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-24Make recheck_defs_without_effects restore old flag properlyBrian Campbell
2019-01-23Make rewriting of E_assign a bit more robustThomas Bauereiss
2019-01-23Add another flow-typing case for E_internal_pletThomas Bauereiss
Copied from a corresponding case for E_block, so that this flow typing still gets picked up after E_block has been rewritten away.
2019-01-22Add a pragma for unrolling recursive functionsAlasdair Armstrong
For example in RISC-V for the translation table walk: $optimize unroll 2 val walk32 ... function walk32 ... would create two extra copies of the walk_32 function, walk_32_unroll_1 and walk_32_unroll_2, with only walk_32_unroll_2 being recursive. Currently we only support the case where we have $optimize unroll, directly followed by a valspec, then a function, but this should be generalised in future. This optimization nearly doubles the performance of RISC-V It is implemented using a new Optimize.recheck rewrite that replaces the ordinary recheck_defs pass. It uses a new typechecker check_with_envs function that allows re-writes to utilise intermediate typechecking environments to minimize the amount of AST checking that occurs, for performance reasons. Note that older Sail versions including the current OPAM release will complain about the optimize pragma, so this cannot be used until they become up to date with this change.
2019-01-22Make sure there is an ocaml representation for optimized memory read forAlasdair
RISC-V
2019-01-22Make sure we optimize constrained union constructorsAlasdair
2019-01-21Update manual snapshot and add basic sail -latex documentationAlasdair Armstrong
2019-01-21Add output directory option for generated Isabelle auxiliary theoriesThomas Bauereiss
2019-01-21Fix some issues with latex generation so manual builds againAlasdair Armstrong
since riscv is no longer in this repository, and we use the RISC-V duopod as an example, you need to build as: make RISCV=directory manual.pdf if directory is not equal to ../../sail-riscv (which is where it would be if sail and sail-riscv are checked out in the same respository together)
2019-01-21Fix a bug with type-checking and latex generationAlasdair Armstrong
We should maybe just make the -latex option behavior the default to avoid this kind of thing
2019-01-17Work around an issue with type abbreviations in HOLThomas Bauereiss
If we use the bitlist representation of bitvectors, the type argument in type abbreviations such as "bits('n)" becomes dead, which confuses HOL; as a workaround, expand type synonyms in this case.
2019-01-17Output configuration registers for LemThomas Bauereiss
Treat them as constants for now (with their initial value); in order to support updates, we would have to embed them properly into the monads.
2019-01-17Fix bug in letbind_effects rewriteThomas Bauereiss
Don't wrap effectful expressions in E_internal_return
2019-01-16Latex: handle underscores when generating latex names.Prashanth Mundkur
2019-01-14Add options for output directories for the lem and coq backends.Prashanth Mundkur
2019-01-14Add a function to perform re-writes in parallelAlasdair
rewrite_defs_base_parallel j is the same as rewrite_defs_base except it performs the re-writes in j parallel processes. Currently only the trivial_sizeof re-write is parallelised this way with a default of 4. This works on my machine (TM) but may fail elsewhere. Because 2019 OCaml concurrency support is lacking, we use Unix.fork and Marshal.to_channel to send the info from the child processes performing the re-write back to the parent. Also fix a missing case in pretty_print_lem
2019-01-14Support some more unification casesThomas Bauereiss
2019-01-14Make rewriting of foreach loops for Lem more robustThomas Bauereiss
Bind loop bounds to type variables, and don't pull existential variables out of context
2019-01-14Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-11Updates for sail-arm releaseAlasdair Armstrong
We want to ensure that no_devices.sail and devices.sail have the same effect footprint, because with a snapshot-type release in sail-arm, we can't rebuild the spec with asl_to_sail every time we switch from running elf binaries to booting OS's. This commit allows registers to have arbitrary effects, so registers that are really representing memory-mapped devices don't have to have the wmem/rmem effect.
2019-01-10Fixes so 8.5 with vector instructions compiles to CAlasdair Armstrong
2019-01-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Coq: add parens around negative integer literalsBrian Campbell
2019-01-08Improvements for v85Alasdair Armstrong
2019-01-03Make sure to close file handles when printing error messagesAlasdair Armstrong
2019-01-03Comment out bisect coverage in ocamlbuild filesAlasdair Armstrong
2019-01-02Coq: tweak recently introduced type check to ignore effectsBrian Campbell
2018-12-31Last rewrite reordering needs more typecheckingBrian Campbell
2018-12-31Coq: move function clause merging to keep measure argument intactBrian Campbell
2018-12-30Sort dependencies of termination measures properlyBrian Campbell
2018-12-29Coq: ensure that recursive functions computeBrian Campbell
2018-12-29Add separate termination_measure declarationsBrian Campbell
2018-12-27Coq: avoid putting ambiguous numeric literals in Coq outputBrian Campbell
There are situations when we really want a more refined expression, such as 8 * n instead of 64 (when we know n = 8 from a case split), but we might not be able to generate it. For now we generate an underscore and let Coq figure it out from the context.
2018-12-27Coq: fix name clashes and instantiation calculationBrian Campbell
2018-12-26More cleanupAlasdair Armstrong
Remove unused name schemes and DEF_kind
2018-12-26Some cleanupAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 18:06:37 +0000