summaryrefslogtreecommitdiff
path: root/src/value.ml
AgeCommit message (Collapse)Author
2018-01-12Interpreter can now pass local values by referenceAlasdair Armstrong
2018-01-12OCaml interactive mode can now run full aarch64 examples, and ocaml test cases.Alasdair Armstrong
2018-01-11Ocaml semantics can now run aarch64 hello world example using octapodAlasdair Armstrong
New testcase for bitfield syntax Updated to work with latest lem and linksem
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
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-13Use big_nums from LemAlasdair 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.