summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-07Also remove impossible if-branchesThomas Bauereiss
2019-03-07Fix bug in a mono rewrite helper functionThomas Bauereiss
2019-03-07C: Make instrs_graph return just control flow graphAlasdair Armstrong
Previously instrs_graph would return the control-flow graph, as well as some data-flow by including reads and writes to variables represented as a node type in the graph (G_id). However, this was not particularly useful, and since the graph isn't in SSA form (so identifiers are non-unique) potentially inaccurate too. This simplifies the code so instrs_graph just returns control flow dependencies, which in turn simplifies the instr_reads and instr_writes functions.
2019-03-07Coq: apply a little brute force in some boolean goalsBrian Campbell
2019-03-07Add a rewrite to remove impossible cases on integer literalsBrian Campbell
(e.g., for the dual 32/64 bit RISC-V model) Apply this rewrite in Coq backend.
2019-03-07Simplify handling of referenced variables in constant propagationBrian Campbell
2019-03-07Git-ignore z3 cachesBrian Campbell
2019-03-07Extract constant propagation and related functions from monomorphisation.Brian Campbell
This shouldn't change any functionality.
2019-03-06Add an -ir option to print the intermediate representation of a fileAlasdair Armstrong
2019-03-06Improve AST slicingAlasdair Armstrong
2019-03-06Add option to slice out printing and tracing functions when generating CAlasdair Armstrong
Make instruction dependency graph use graph.ml Expose incremental graph building functions for performance in graph.mli
2019-03-05Fix missing case in specializationAlasdair
2019-03-05More optimizations and improvments for C generationAlasdair Armstrong
Add some comments in constant_fold.ml
2019-03-05Add missing comma in armV8.sailAlasdair Armstrong
2019-03-05Add forgotten recursive function testBrian Campbell
2019-03-05Add Unallocated to the gen filesBen Simner
Adds the Unallocated sail ast node to be tracked by all the transformation files, to track the change made to sail1.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 02:23:39 +0000