summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-13Finish toFromInterp backend, adding Lem modeJon French
2019-03-13Remove prover reference from typecheck env when marshalling out defsJon French
2019-03-13lib/regfp.sail: new standard intrinsics for triggering memory effectsJon French
2019-03-13package and install Sail as an ocamlfind libraryJon French
2019-03-04Type_check: functions env/typ_of_tannotJon French
2019-03-04Merge branch 'sail2' into rmem_interpreterJon French
2019-03-04Marshalling: remove prover before marshallingJon French
2019-03-04Interpreter: remove useless string-to-rk/wk/bk functions, they're much ↵Jon French
better suited in RMEM
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-04fix old extern type usage in SpecializeJon French
2019-03-04Merge branch 'sail2' into rmem_interpreterJon French
2019-03-04Type_check: make prover reference in env an option defaulting to NoneJon French
Also: * Rename add_prover to set_prover * Make set_prover public This is to support being able to marshal out typecheck envs. RMEM (or other users) can temporarily set the prover reference to None to avoid attempting to marshal a functional value, and then reset it to Some (Type_check.prove ...) on unmarshalling.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 17:36:01 +0000