summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-06Make CHERI spec type-check againThomas Bauereiss
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-05Merge branch 'master' into experimentsAlasdair Armstrong
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-12-04Merge remote-tracking branch 'origin/master' into experimentsAlasdair Armstrong
2017-12-04added the Power modelShaked Flur
2017-12-04match what rmem expects from sail/armShaked Flur
2017-12-04renamed hgen to genShaked Flur
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-30match what rmem (ppcmem2) expects from ISA MakefilesShaked Flur
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-27Added test for short-circuiting of boolean operationsAlasdair 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-24Attempt to document intermediate language used by Sail in ott.Alasdair Armstrong
2017-11-23renamingShaked Flur
2017-11-23added RISCV_ prefix to some values to stop Lem from renaming themShaked Flur
2017-11-21Expose entry point in elf_loader for Sail modelAlasdair Armstrong
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 03:46:12 +0000