summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-05Coq: firstorder is better at the boolean goalsBrian Campbell
2019-03-05Coq: use setoid rewriting to apply under an existential binderBrian Campbell
2019-03-05Coq: use more local type information when constructing tuplesBrian Campbell
2019-03-05Coq: some debugging messagesBrian Campbell
2019-03-05Coq: output type-level Int definitionsBrian Campbell
2019-03-05Coq 8.9 compatibility fixBrian Campbell
2019-03-05Additional optimizations for C compilationAlasdair
2019-03-04Fix aarch64_small test XML for jenkinsAlasdair Armstrong
Rename rewrite_split_fun_constr_pats to rewrite_split_fun_ctor_pats as constr is commonly used as an abbreviation for constraint rather than constructor, and add a more descriptive comment.
2019-03-04Add test for building handwritten ARM to lem for JenkinsAlasdair Armstrong
2019-03-04Fix execute splitting to work when constructors have constraints.Alasdair Armstrong
Previously any constraints on constructors were just outright dropped when splitting the execute function in Lem generation. Now we get the constraints and type signature for each execute clause from the type given by Env.get_union_constructor, rather than by inferring the type of the pattern in each function clause. Currently this can still fail in the case where we have union U('x: Int), C1('x) = { ctor: {'y. C2('x, 'y), T('x, 'y)} } and val execute : forall 'z, C3('z). U('z) -> unit when C3 implies C1, and the body of an excute clause relies on the fact that C3 is stronger than C1, as each split function execute_ctor is only guaranteed to be constrained by some subset of C1. This seems unlikely to happen in practice though. Also fix a bug when binding P as int('T) against int('T) and similar cases, where the new type variable would cause the old type variable to become shadowed, but the constraint that the bound type variable and the old type variable are equal would not take this into account.
2019-03-04Merge branch 'sail2' of https://github.com/rems-project/sail into sail2Christopher Pulte
2019-03-04check in missing regfp2.sailChristopher Pulte
2019-03-04Do not store type synonyms as functions in the environmentAlasdair Armstrong
2019-03-04cleanupChristopher Pulte
2019-03-04Merge branch 'sail2' of https://github.com/rems-project/sail into sail2Christopher Pulte
2019-03-04last bit of sail1 to sail2 portingChristopher Pulte
2019-03-04Add location to warning in pattern completeness checkAlasdair Armstrong
2019-03-04more sail1-to-sail2 portingChristopher Pulte
2019-03-04more porting of armv8 from sail1 to sail2Christopher Pulte
2019-03-04moreChristopher Pulte
2019-03-02moreChristopher Pulte
2019-03-02moreChristopher Pulte
2019-03-02Merge branch 'sail2' of https://github.com/rems-project/sail into sail2Christopher Pulte
2019-03-02moreChristopher Pulte
2019-03-01WIP: Start working on being able to slice single instructions out of specsAlasdair Armstrong
2019-03-01Add some tricky test cases for quantified Sail AST typesAlasdair Armstrong
Fixes some bugs found by doing this
2019-03-01Coq: some library compatibility changesBrian Campbell
2019-03-01Add a test case for previous commitAlasdair Armstrong
Also make unifying int against int('n) work as expected for constructor applications.
2019-03-01Merge branch 'sail2' of https://github.com/rems-project/sail into sail2Christopher Pulte
2019-03-01Fix bug with naturals in quantified constructorsAlasdair Armstrong
2019-03-01Merge branch 'sail2' of https://github.com/rems-project/sail into sail2Christopher Pulte
2019-03-01Make Sail more flexible with existentials in union typesAlasdair Armstrong
Issues came up with Christophers translation of hand-written ARM into Sail2 where we were being overly pedantic about the exact position of existential quantifiers in constructors with multiple arguments. This commit generalises unify_typ and type_coercion_unify to be more flexible and support this. Should think at some point if unify_typ can be generalised further. This fix should fix the decode side of things, but may be some issues with the executes that still need looking into when existentials and multiple argument constructors are mixed.
2019-03-01Fill in some edge cases in monomorphisationBrian Campbell
2019-03-01more progressChristopher Pulte
2019-03-01Coq tidying: remove old definition, complete a pattern matchBrian Campbell
2019-03-01Coq: add a little bit of boolean solvingBrian Campbell
Just enough for RISC-V to go through
2019-03-01Coq: make iff `iff`Brian Campbell
Also drop unused implication function
2019-02-28Handle implicits in destruct_atom_nexpBrian Campbell
2019-02-28Coq: remove unused library definitionsBrian Campbell
2019-02-28Coq: Clean up rich boolean handling in backendBrian Campbell
Now generates something vaguely sensible for RISC-V, although the solver needs a little work. Adds type annotations around effectful, rich and/or expressions.
2019-02-28Coq: more for informative booleansBrian Campbell
Make internal_plet produce annotations (with code to replace unusable type variables) Add mappings for bool kids at bindings Add version of and_bool that proves a property
2019-02-28Coq: update tyvar merge information at other bindersBrian Campbell
2019-02-28Turn off some debugging messagesBrian Campbell
2019-02-28Coq: merge tyvars with corresponding variablesBrian Campbell
2019-02-28Coq: strip informative bools back to more uniform typesBrian Campbell
Also make pretty printing more keen on line breaking
2019-02-28Coq: some work on bool simplificationBrian Campbell
This introduces some simplification of informative booleans, but tries too hard to eliminate all of the existentials resulting in difficulties in and/or trees.
2019-02-28Allow user-specified state to be passed through generated CAlasdair Armstrong
For example: sail -c_extra_params "CPUMIPSState *env" -c_extra_args env would pass a QEMU MIPS cpu state to every non-builtin function call. Also add documentation for each C compilation option in C_backend.mli
2019-02-28more progressChristopher Pulte
2019-02-27Provide more access to the ELF symbols in the OCaml ELF-loader.Prashanth Mundkur
2019-02-27Tweaks to C compilation to make it more usable for embedding into other programsAlasdair Armstrong
Can now set a prefix for generated C functions with -c_prefix so -c_prefix sail_ would give sail_execute_CGetPerm over zexecute_CGetPerm. We still have to use our standard name-mangling scheme to avoid possible collisions within the name. Can build C that doesn't expect the standard runtime, which leaves operations like read_memory, write_memory etc to be stubbed in by another C program including the generated Sail. Things like letbindings are still an issue because we rely on a very small runtime to initialize global letbindings and similar. -c_separate_execute splits the execute function apart in the generated C
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 19:26:19 +0000