summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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-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-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
2017-11-27Case splitting on boolsBrian Campbell
(mostly to make test cases easier)
2017-11-24Use unbound precision big_ints throughout sail.Alasdair Armstrong
Alastair's test cases revealed that using regular ints causes issues throughout sail, where all kinds of things can internally overflow in edge cases. This either causes crashes (e.g. int_of_string fails for big ints) or bizarre inexplicable behaviour. This patch switches the sail AST to use big_int rather than int, and updates everything accordingly. This touches everything and there may be bugs where I mistranslated things, and also n = m will still typecheck with big_ints but fail at runtime (ocaml seems to have decided that static typing is unnecessary for equality...), as it needs to be changed to eq_big_int. I also got rid of the old unused ocaml backend while I was updating things, so as to not have to fix it.
2017-11-21Check non-constraint liftable assertions in blocks correctlyAlasdair Armstrong
2017-11-21Merge Thomas' suggested changesBrian Campbell
Use overloading to find eq/neq Track range/atom split Missing type expansion
2017-11-20Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-11-20Fix a bug with constraint generation in flow typing.Alasdair Armstrong
This bug manifested as the ARM example elf executable printing the wrong characters... but otherwise doing not failing and exiting cleanly. It didn't trigger the test suite at all. I tracked it down to this line using git-bisect, and while returning nc_true is a bit suspect I'm still not 100% sure how this caused such a subtle and annoying bug in the generated ocaml code - it took several hours to track down the breakage to this line.
2017-11-20Tidy last upBrian Campbell
2017-11-20Constant propagation in guardsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 03:21:50 +0000