summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-11-10Fixed ocaml backend so it correctly compiles registers passed by name.Alasdair Armstrong
Added a test case for this behavior
2017-11-10Fixed some tricky typechecking bugsAlasdair Armstrong
2017-11-08Allow functions to be selectively declared external only for some backendsThomas Bauereiss
For example, val test = { ocaml: "test_ocaml" } : unit -> unit will only be external for OCaml. For other backends, it will have to be defined.
2017-11-08Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-11-08Allow for different extern names for different backendsAlasdair Armstrong
For example: val test = { ocaml: "test_ocaml", lem: "test_lem" } : unit -> unit val main : unit -> unit function main () = { test (); } for a backend not explicitly provided, the extern name would be simply "test" in this case, i.e. the string version of the id. Also fixed some bugs in the ocaml backend.
2017-11-07Fix typo in constraint rewriterThomas Bauereiss
2017-11-07Add builtin for reversing endiannessThomas Bauereiss
2017-11-07Declare prelude functions as externThomas Bauereiss
Also, rename a few functions for uniformity, e.g. bool_and -> and_bool
2017-11-07Fix vector_subrange typoBrian Campbell
2017-11-03Fix ocaml test suiteAlasdair Armstrong
2017-11-03Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-11-03Fixed a bug where true and false get mixed up in rewriterAlasdair Armstrong
2017-11-03Fix a bug where sail would throw an exception with empty file listAlasdair Armstrong
2017-11-03Make sure simple parameter sizes appear in Lem mwords outputBrian Campbell
2017-11-03Make nexp_simp a little smarterBrian Campbell
2017-11-02Added monomorphism restriction to undefined values.Alasdair Armstrong
What does this mean? Basically undefined values can't be created for types that contain free type variables, so for example: undefined : list(int) is good, but undefined : list('a) is bad. The reason we want to do this is because we can't compile them away statically, and this leads to situations where type-checkable code fails in the rewriter and gives horribly confusing error messages that don't relate to code the user wrote at all. As an example the following used to typecheck, but fail in the rewriter with a confusing error message, whereas now the typechecker should reject all cases which would trigger that failure in rewriting. val test : forall ('a:Type). list('a) -> unit effect {wreg, undef} function test xs = { xs_mut = xs; xs_mut = undefined; (* We don't know what kind of undefined 'a is *) () } There's a slight hitch, namely that in the undefined_type functions created by the -undefined_gen option, we do want to allow functions that have polymorphic undefined values, so that we can generate undefined generators for polymorphic datatypes such as: union option ('a:Type) = { Some : 'a, None } These functions are always have a specific form that allows the rewriter to succesfully remove the polymorphic undefined value for the 'a argument for Sone. As such there's a flag in the typechecking environment for polymorphic undefineds that is enabled when it sees a function with the undefined_ name prefix. Also: Fixed some test cases that were broken due to escape effect being added to assert.
2017-11-02Merge branch 'experiments'Thomas Bauereiss
2017-11-02Fix a few AST and parsing-related bugsThomas Bauereiss
2017-11-02Optionally generate an initial register state for the sequential Lem shallow ↵Thomas Bauereiss
embedding Checks for command-line flag -undefined_gen and uses the undefined value generator functions of the form undefined_typ to initialise registers
2017-11-02Fix translation of repeat-until loops to LemThomas Bauereiss
2017-11-02Handle "undefined" type-level sizes in monomorphisationBrian Campbell
2017-11-01Support bitvector-size-parametric functions in Lem outputBrian Campbell
Translates atom('n) types into itself('n) types that won't be erased Also exports more rewriting functions
2017-11-01Fix some missing nexp simplification in Lem outputBrian Campbell
2017-10-31Fixed wrong image for List-remove.svgAlasdair Armstrong
2017-10-31Added trace viewer application for traces produced by sail -ocaml_traceAlasdair Armstrong
See README file for how to set up and use
2017-10-31Improvements to register read tracing in ocaml backendAlasdair Armstrong
2017-10-31Pretty-print Sail assertions in LemThomas Bauereiss
Map to calls to monadic function assert_exp that throws an exception if the assertion is false
2017-10-31Fix bug in topological sorting of val-specsThomas Bauereiss
Put them before the function they declare
2017-10-31Remove redundant nexp simplification functionThomas Bauereiss
2017-10-27Fixed some ocaml backend related bugsAlasdair Armstrong
2017-10-26Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-10-26Unfold nexp abbreviations for pretty-printingThomas Bauereiss
2017-10-26Update val specs after rewriting functionsThomas Bauereiss
2017-10-26Experiment with pretty-printing non-atomic nexps in LemThomas Bauereiss
2017-10-26Updated ocaml backend so tracing instrumentation is optional.Alasdair Armstrong
Cleaned up the option list in sail.ml
2017-10-25Allow mutually recursive functionsThomas Bauereiss
2017-10-25Point sail/src makefile at ott file in language/Alasdair Armstrong
2017-10-25List.cons is too newBrian Campbell
2017-10-25Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-25Generate ast.ml from ott file and update makefile.Alasdair Armstrong
Fix until loop not being counted as sugar
2017-10-25Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-25Alternative low-memory version of barrier_kindCompareBrian Campbell
2017-10-25Avoid name clash in generated LemBrian Campbell
(complains due to added val spec)
2017-10-24Make nexp simplifier handle recursion properlyBrian Campbell
2017-10-24More succinct syntax in new parser for externed valspecs which shareAlasdair Armstrong
the same name between sail and the target
2017-10-24Print type annotations in Lem with type variablesBrian Campbell
(includes variables for bitvector sizes)
2017-10-24Limit quantifiers printed in Lem to type variables that actuallyBrian Campbell
appear in the output
2017-10-24Handle existential types in Lem backend by stripping them andBrian Campbell
checking that the type variables visible in the output aren't existential
2017-10-24Generate undefined_bitvector function when targeting machine wordsBrian Campbell
2017-10-24Produce debug message when an expression can't be converted to a constraintBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-16 20:07:12 +0000