summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2018-01-03Lots of experimental changes on this branchAlasdair Armstrong
* Changed comment syntax to C-style /* */ and // * References to registers and mutable variables are never created implicitly - a reference to a register or variable R is now created via the expression "ref R". References are assigned like "(*Y) = X", with "(*ref R) = X" being equivalent to "R = X". Everything is always explicit now, which simplifies the logic in the typechecker. There's also now an invariant that every id directly in a LEXP is mutable, which is actually required for our rewriter steps to be sound. * More flexible syntax for L-expressions to better support wierd power-idioms, some syntax sugar means that: X.GET(a, b, c) ==> _mod_GET(X, a, b, c) X->GET(a, b, c) ==> _mod_GET(ref X, a, b, c) for setters, this can be combined with the (still somewhat poorly named) LEXP_memory construct, such that: X->SET(a, b, c) = Y ==> _mod_SET(ref X, a, b, c, Y) Currently I use the _mod_ prefix for these 'modifier' functions, but we could omit that a la rust. * The register bits typedef construct no longer exists in the typechecker. This construct never worked consistently between backends and inc/dec vectors, and it can be easily replaced by structs with fancy setters/getters if need be. One can also use custom type operators to mimic the syntax, i.e. type operator ... ('n : Int) ('m : Int) = slice('n, 'm) struct cr = { CR0 : 32 ... 35, /* 32 : LT; 33 : GT; 34 : EQ; 35 : SO; */ CR1 : 36 ... 39, /* 36 : FX; 37 : FEX; 38 : VX; 39 : OX; */ CR2 : 40 ... 43, CR3 : 44 ... 47, CR4 : 48 ... 51, CR5 : 52 ... 55, CR6 : 56 ... 59, CR7 : 60 ... 63, } This greatly simplifies a lot of the logic in the typechecker, as it means that E_field is no longer ambiguously overloaded between records and register bit typedefs. This also makes writing semantics for these constructs much simpler.
2018-01-03Updates to interpreterAlasdair Armstrong
Experimenting with porting riscv model to new typechecker
2018-01-02Experimenting with power specAlasdair Armstrong
2017-12-14An experimental version of sail without bitvector start indexes.Alasdair Armstrong
Works with the vector branch of asl_parser
2017-12-14Merge remote-tracking branch 'origin/experiments' into interactiveAlasdair Armstrong
2017-12-14Fix all compiler warning except in lem pretty printer and monomorphisationAlasdair Armstrong
2017-12-13Cleanup code by fixing compiler warnings, and fix ocaml compilationAlasdair Armstrong
Add the ast.sed script we need to build sail. Currently we just need this to fix up the locations in the AST but it will be removed once we can share locations between ocaml and lem.
2017-12-13Merge remote-tracking branch 'origin/master' into interactiveAlasdair Armstrong
2017-12-13Use big_nums from LemAlasdair Armstrong
2017-12-13find zarith using ocamlfind instead of using the one in ocaml-lib which is ↵Shaked Flur
no longer there
2017-12-12Add a few helper functions for bit listsThomas Bauereiss
2017-12-12Make mono analysis fail properly on effectful functionsBrian Campbell
2017-12-11Allow stepping through code when evaluatingAlasdair Armstrong
2017-12-11Prototype interactive mode for sail.Alasdair Armstrong
Requires linenoise library (opam install linenoise) for readline support. Use 'make isail' to build sail with interactive support. Plain 'make sail' should work as before with no additional dependencies. Use 'sail -i <commands>' to run sail interactively, e.g. sail -new_parser -i test/ocaml/prelude.sail test/ocaml/trycatch/tc.sail then try some commands for typechecking and evaluation sail> :t main sail> main () Doesn't use the lem interpreter right now, instead has a small operational semantics in src/interpreter.ml, but this is not very complete and will be changed/removed.
2017-12-11Remove some duplication from monomorphisation analysis failure reportsBrian Campbell
2017-12-07More OCaml test casesAlasdair Armstrong
Improved handling of try/catch Better handling of unprovable constraints when the environment contains false
2017-12-07Fix boolean literal constraintsAlasdair Armstrong
2017-12-07Fix regressions in OCaml outputAlasdair Armstrong
Recent patches have made the rewriter more strict about performing type correct rewrites. This is mostly a good thing but did cause some problems with the ocaml backend. Currently the sizeof rewriter doesn't seem to preserve type correctness - I suspect this is because when it resolves the sizeofs, it generates constraints that are true, but not in a form where the typechecker can see that they are true. I disabled the re-check after the sizeof rewriting pass to fix this. Maybe we don't want to do this anyway because it's slow. Changes to function clauses with guards + monomorphisation changed how the typechecker handles literal patterns. I added a rewriting pass to rewrite literals to guarded equality checks, which is run before generating ocaml. The rewriter currently uses Env.empty in a view places. This can cause bugs because Env.empty is a totally unitialised environment that doesn't satisfy invariants we expect of an environment. This should be changed to initial_env and it shouldn't be exported, I fixed a few cases where this caused things to go wrong, but it should probably not be exported from Type_check.ml.
2017-12-07Support monomorphisation with set constrained integersBrian Campbell
Also, to support this, constant propagation for integer multiply, fix substitution of concrete values for nvars, size parameters in single argument functions, fix kind for itself, add eq_atom to prelude
2017-12-07Resolve function clause guard parsing ambiguity by requiring parenthesesBrian Campbell
2017-12-07Functions with guards changes in rewritesBrian Campbell
2017-12-06Add parsing for guards in function clausesBrian Campbell
Breaks parsing ambiguities by removing = as an identifier in the old parser and requiring parentheses for some expressions in the new parser
2017-12-06Remove filename mangling in monomorphisationBrian Campbell
Broke analysis a little
2017-12-06Rework case checking to only introduce guards when necessaryBrian Campbell
2017-12-06Add top-level pattern match guards internallyBrian Campbell
Also fix bug in mono analysis with generated variables Breaks lots of typechecking tests because it generates unnecessary equality tests on units (and the tests don't have generic equality), which I'll fix next.
2017-12-06Merge remote branch 'experiments' into experimentsThomas Bauereiss
2017-12-06Make AST after rewriting for Lem backend type-checkableThomas Bauereiss
- Add support for some internal nodes to type checker - Add more explicit type annotations during rewriting - Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer; these will be resolved by the type checker during rewriting now
2017-12-05Better support for exceptions in sail for ASL specs that need them.Alasdair Armstrong
2017-12-05add EdPeter Sewell
2017-12-05Update header files on masterAlasdair Armstrong
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-12-05Pretty printer now prints operator precedence correctly.Alasdair Armstrong
Also some simple rules to try to format if statements better based on contents while pretty printing.
2017-12-04Fix warnings in test suiteAlasdair Armstrong
2017-11-30Use doc_typdef_lem from experimentsAlasdair Armstrong
2017-11-30Merge branch 'master' into experimentsAlasdair Armstrong
2017-11-30Improvements to enable parsing and checking intermediate rewritingAlasdair Armstrong
steps Parser now has syntax for mutual recusion blocks mutual { ... fundefs ... } which is used for parsing and pretty printing DEF_internal_mutrec. It's stripped away by the initial_check, so the typechecker never sees DEF_internal_mutrec. Maybe this could change, as forcing mutual recursion to be explicit would probably be a good thing. Added record syntax to the new parser New option -dmagic_hash is similar to GHC's -XMagicHash in that it allows for identifiers to contain the special hash character, which is used to introduce new autogenerated variables in a way that doesn't clash with existing names. Option -sil compiles sail down to the intermediate language defined in sil.ott (not complete yet).
2017-11-29Better lem_ast tagging and interpreter tweaksAlasdair Armstrong
2017-11-29Switched to bytecode compiler for executing interpreter to avoid stack overflowAlasdair Armstrong
2017-11-29Fix lem_ast output bugsAlasdair Armstrong
2017-11-29Added location information for fixity and overloads in ast_util.mlAlasdair Armstrong
2017-11-28Make pretty printer able to print several internal constructs for debuggingAlasdair Armstrong
2017-11-28Small update to trivial sizeof rewrites so we can handle all cases inAlasdair Armstrong
aarch64 vector instructions. There's maybe a better more general way to do this but I'm not sure what that would be.
2017-11-28Fix issue where statements in blocks had incorrect environmentsAlasdair Armstrong
2017-11-27Utility functions in ast_util for asl_parserAlasdair Armstrong
2017-11-27Split rewriter into separate rewriting library and rewrite passesAlasdair Armstrong
As discussed previously, we wanted to start refactoring the re-writer to make it a bit less monolithic, and in the future potentially break it into separate files for backend-specific rewrites and stuff. - rewriter.ml now contains the generic re-writing code - rewrites.ml contains the rewriting passes themselves It would be nice if the generic rewriting code didn't depend on the typechecker, because then it could be used in ASL parser on untyped code.
2017-11-27Use guards from when patterns when typing casesBrian Campbell
2017-11-27Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-11-27Compile assertions into OCamlAlasdair Armstrong
and_bool and or_bool now are treated specially in the ocaml backend, so that they have the correct short-circuiting behaviour. This is required so that assertions don't fail for the ARM spec for predicates that shouldn't be tested in certain circumstances, for example things like: IsAArch32() && AArch32_specific_predicate Also fixed an issue in the sail library for ocaml where greater than or equal to was being mapped to greater than.
2017-11-27Fix bitvector pattern removal typoBrian Campbell
2017-11-27Replace bad generic comparisons in monoBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 17:04:10 +0000