| Age | Commit message (Collapse) | Author |
|---|
|
Rename l2.ott to sail.ott
|
|
node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node
|
|
|
|
fix Makefile clean
|
|
|
|
|
|
|
|
Not working yet
|
|
|
|
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
|
|
|
|
well as items of kind Type.
Syntax for the feature is:
def Nat id = nexp
Note: some useful nexps may not parse properly.
All typedef forms can also be used as def Type ... if desired, but this is not required.
|
|
Improve printing for asl to sail readability;
Add -o option for selecting the name of file generation;
Add additional initial check module for turning generated ast nodes into ready-to-type-check ast nodes
|
|
This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error.
WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified.
|
|
|
|
|
|
Close #20
|
|
|
|
|
|
|
|
|
|
Add a new internal node for moving assignments into scope-preserving expressions that more explicitly define the scope
|
|
unknown conditions.
Does not merge if one path has resulted in an exit
|
|
|
|
Events are eamem to signal the memory address to write to and wmv to pass the value to write
|
|
|
|
being very power-specific.
Note: slight interface change to instruction_extractor
|
|
Also fix type checker bug in not reporting modifications to parameter values
|
|
|
|
of type nat (at least not without a >= 0 check)
|
|
Fix up parsing on 2** precedence
Fix errors on type variables in function definition
|
|
Split out specification specific memory and external functions
Reduce the presence of big_int
Reduce the use of inc direction, instead using a default from the spec. Still a few places need to be parameterised over direction
Also some bug fixes exposed by above and running ARM second instruction
|
|
Also stop rewriting code in the pretty printer, instead move it all into a new general rewriting pass
|
|
|
|
function-clause
|
|
temporarily use other version of Lem
|
|
will be reflected in short hand type syntax, inc is still the default if undeclared
So:
default order dec
register bit[32] t (* Declares t as a decreasing vector, starting at 31 on the left and decreasing to 0 *)
default order inc
register bit[32] o (* Declares o as an increasing vector, starting at 0 on the left and increasing to 31 *)
It is presently possible to change the default mid-file; this is almost certainly bad and I will turn it into an error soon.
|
|
|
|
interpreter.
An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter.
|
|
and the like.
|
|
Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches
|
|
|
|
Short version of below; ready to hook interp_exhaustive up to something to test, but haven't yet.
If an unknown value influences a pattern match within an expression, each passing pattern is found and the bodies strung together into a block with let expressions to bind the variables.
In a function call, the cases are all collected but the support is not in place at the moment to evaluate them.
If an unknown is the result of the cond expression in an if, the then and else case become a block.
Unknowns within the interpreter propagate to more Unknowns; also for some but not all library functions yet.
|
|
Reduce the number of implicit coercions we're doing, expanding overloading and fixing up types of functions.
Warning: test_power does not run as not all overloaded funcitons are implemented
Warning: vector concatenation does not pretty print to sail source yet
|
|
to support 2**64.
Note: now nat (short hand for range<0,infinity>) should only be used if you really mean a nat instead of a bounded number (i.e. range<0,2**32>)
|
|
functions for connecting the interpreter to a memory model)
Also adding default values to index vectors for supporting sparse vectors/maps
|
|
|
|
constraints. Clean up Lem output a little for readability while debugging.
|
|
to_num and to_vec probably still need to be fixed
|
|
|
