| Age | Commit message (Collapse) | Author |
|---|
|
|
|
functions
|
|
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.
|
|
The type-constraints are inspired from those for (+). They seem to work
but I am not sure they make sense.
The vector is interpreted as unsigned.
|
|
|
|
|
|
|
|
|
|
- remember mode (run, step or next) between instructions
- display continuation by default in step mode
- start in step mode by default
- incompatible change: the shorthand for stack is now bt (=backtrace),
since s becomes the shorthand for step
- incompatible change: pressing enter now repeats the current mode,
instead of "step"
|
|
|
|
function call)
Also turning off an annoying printf I left in.
|
|
|
|
This displays the full continuation of the current breakpoint,
which is basically the closest that we have from the "context"
requested by Peter. Especially using it after the "execute" breakpoint
shows the code of the instruction to be executed.
|
|
Use "show_casts" and "hide_casts" in interactive interpreter to
display or show casts in expressions. Hidden by default (makes
things much less readable otherwise).
|
|
Conflicts:
src/lem_interp/interp_lib.lem
src/lem_interp/run_interp.ml
Remove "to_vec_safe" work-around
|
|
solving; get test_power running again by supporting the correct operations and bit operations
|
|
Update power.sail to new, pretty-printer-based version
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Default to 64 bit for vec + range
|
|
Copy-pasted with a few tweaks from Pretty_printer.
Should really make a functor instead, but not sure how to deal with
E_internal_cast yet.
Note that Interp_ast and Ast are *not* generated from the same ott file
(resp. l2.ott and l2_type.ott), but they are close enough that the code
almost "just works".
|
|
|
|
|
|
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>)
|
|
|
|
constraints
|
|
interpreter
|
|
|
|
|
|
|
|
|
|
|
|
functions for connecting the interpreter to a memory model)
Also adding default values to index vectors for supporting sparse vectors/maps
|
|
|
|
|
|
Change type of + on vectors to (bit vector,bit vector) -> bit vector
|
|
vectors) and make the test suite pass again
|
|
WARNING: vector test breaks due to not having implemented the full range of different + functions
In general, we need to decide whether vector + vector, vector + range and range + vector should all return ranges, vectors or a mixture
|
|
|
|
|
|
Does not properly bind variables (i.e. in the pattern 0b01:(bit[3]) a: 0b0001 subsequent uses of a will not be bound in the interpreter, though they are in the type checker), so until bug is fixed, treat all such identifiers as _
|
|
|
|
|
|
- Move FDE loop to the OCaml side of the Power model (avoid leaking
memory due to lack of TCO in interpreter)
- Display cycle count
- Check the value of CIA at the end of each cycle and stop if it is
equal to the initial value of LR, returning the value in GPR3.
|
|
|
