summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-08-28Eta expand lem for OCaml generationBrian Campbell
2017-08-28Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-08-28Correct indexing and equality for bitvectorsBrian Campbell
2017-08-28Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵Brian Campbell
mono-experiments # Conflicts: # src/gen_lib/sail_values.lem
2017-08-24Use relative path in MakefileThomas Bauereiss
2017-08-24Fix some bugs related to the CHERI specThomas Bauereiss
- Correctly pass exponentials to Z3 - Infer types of functional record updates - Support "def Nat"
2017-08-24Add Num identifiers to type environmentThomas Bauereiss
2017-08-24Improve and simplify handling of mutable local variablesThomas Bauereiss
2017-08-24Begin refactoring Sail libraryThomas Bauereiss
- Add back support for bit list representation of bit vectors, for backwards compatibility in order to ease integration with the interpreter. For this purpose, split out a file sail_operators.lem from sail_values.lem, and add a variant sail_operators_mwords.lem for the machine word representation of bitvectors. Currently, Sail is hardcoded to use machine words for the sequential state monad, and bit lists for the free monad, but this could be turned into a command line flag. - Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem library. The wrappers make use of sizeof expressions to extract type information from bitvectors (length, start index) in order to pass it to the Lem functions. - Add early return support to the free monad, using a new constructor "Return of 'r". As with the sequential monad, functions with early return are wrapped into "catch_early_return", which extracts the return value at the end of the function execution.
2017-08-24Avoid re-typechecking after rewriting passesThomas Bauereiss
Rewriting of sizeofs and constraints seems to lose or hide some information that the typechecker needs
2017-08-24Add some missing type annotationsThomas Bauereiss
2017-08-24Add a little cast handling to constant propagationBrian Campbell
2017-08-23Started work on an undefined literal removal pass for the ocamlAlasdair Armstrong
backed. Ocaml doesn't support undefined values, so we need a way to remove them from the specification in order to generate good ocaml code. There are more subtle issues to - like if we initialize a mutable variable with an undefined list, then the ocaml runtime has no way of telling what it's length should be (as this information is removed by the simple_types pass). We therefore rewrite undefined literals with calls to functions that create undefined types, e.g. (bool) undefined becomes undefined_bool () (vector<'n,'m,dec,bit>) undefined becomes undefined_vector(sizeof 'n, sizeof 'm, undefined_bit ()) We therefore have to generate undefined_X functions for any user defined datatype X. initial_check seems to be the logical place for this. This is straightforward provided the user defined types are not-recursive (and it shouldn't be too bad even if they are).
2017-08-23TypoBrian Campbell
2017-08-23Update monomorphisation test scriptBrian Campbell
2017-08-23Syntax updates in monomorphisationBrian Campbell
2017-08-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-08-22Type quantification elimination working for hexapod specAlasdair Armstrong
2017-08-22Added debugging output for E_record and E_record_update in ast_utilAlasdair Armstrong
2017-08-22Add option to dump monomorphised ast before (re-)typecheckingBrian Campbell
2017-08-22Adapt first part of union monomorphisation to existential typesBrian Campbell
2017-08-22Added basic support for pure record definitions and functional recordAlasdair Armstrong
updates to the new typechecker
2017-08-22More work on quantifier eliminationAlasdair Armstrong
2017-08-21More work on quantifier elimination passAlasdair Armstrong
Also added a rewriting pass that removes the cast annotations and operator overloading declarations from the AST because they arn't supported by the interpreter.
2017-08-21Modified sizeof rewriting pass so it can correctly deal with existentials.Alasdair Armstrong
Basically we needed to make the rewriting step for E_sizeof and E_constraint more aggressively try to rewrite those expressions from variables in scope, without adding new parameters to pass the type variables at runtime, as this can break in the presence of existential quantification. Still some cleanup to do in this code, but tests on the arm spec show that it now introduces the minimal amount of new parameters.
2017-08-21Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-08-18Correct indexing and equality for bitvectorsBrian Campbell
2017-08-18Fixed a bug where sizeof re-writing fail for aliased type argumentsAlasdair Armstrong
Also: Merge remote-tracking branch 'origin/sail_new_tc' into experiments
2017-08-17Work on E_constraint removal pass and diagnosing bugs in E_sizeof removal passAlasdair Armstrong
2017-08-17Add E_constraint support to re-writerAlasdair Armstrong
2017-08-17Add support for register types other than bitvector to state monadThomas Bauereiss
Make state monad parametric in register state, and generate a record with registers from the Sail spec
2017-08-17Various sail fixes for ASL hexapodAlasdair Armstrong
2017-08-17Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵Brian Campbell
mono-experiments
2017-08-17Merge remote-tracking branch 'origin' into mono-experimentsBrian Campbell
# Conflicts: # src/type_internal.ml
2017-08-17fixed the RISC-V fences (3 types: "rw,rw"/"r,rw"/"rw,w")Shaked Flur
2017-08-16Added the feature to bind type variables in patterns.Alasdair Armstrong
The reason you want this is to do something like (note new parser only): ********* default Order dec type bits 'n:Int = vector('n - 1, 'n, dec, bit) val zeros : forall 'n. atom('n) -> bits('n) val decode : bool -> unit function decode b = { let 'datasize: {|32, 64|} = if b then 32 else 64; let imm: bits('datasize) = zeros(datasize); () } ********* for the ASL decode functions, where the typechecker now knows that the datasize variable and the length of imm are the same.
2017-08-16Eta-expansion in sail_values to make OCaml happyBrian Campbell
2017-08-16lem_interp: remove broken val_to_string_internal functions, replace with ↵Jon French
string_of_value as used everywhere else
2017-08-15Merge remote-tracking branch 'origin/mono-experiments' into experimentsAlasdair Armstrong
2017-08-15Removed Typ_arg_effect - nobody used it and it isn't supported by the backends.Alasdair Armstrong
2017-08-15Export existential destructuring function in type_check.mli.Alasdair Armstrong
Also rename some functions for consistency.
2017-08-15Export utility functions from type_check.mlAlasdair Armstrong
2017-08-15Menhir parser support for try/catchAlasdair Armstrong
2017-08-15Improve and simplify handling of mutable local variablesThomas Bauereiss
2017-08-15Added exceptions and try/catch blocks to AST and typechecker in orderAlasdair Armstrong
to translate exceptions in ASL. See test/typecheck/pass/trycatch.sail.
2017-08-14Existentials in free type var functionsBrian Campbell
2017-08-14Some overloaded equality support in monomorphisationBrian Campbell
2017-08-14Merge remote-tracking branch 'origin/master' into experimentsAlasdair Armstrong
2017-08-14Merge remote-tracking branch 'origin/mono-experiments' into experimentsAlasdair Armstrong
2017-08-14More constructs in menhir parser, plus support for both left and right infix ↵Alasdair Armstrong
operators.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 16:29:14 +0000