| Age | Commit message (Collapse) | Author |
|
|
|
Also adding more comments and getting the ml files built in the build process
|
|
|
|
|
|
Now when mode.track_values is true, on every register read, the returned value is tainted with the register it came from. This tracking is followed through every operation the interperter touches (except library functions, to be completed next).
One a memory operation involving a tracked value, there is optionally list of registers that value arose from in the memory request (i.e. maybe (list reg_name)).
|
|
Need to add cases for tracking a taint past a conditional check where possible; and then to actually generate them from reading registers.
|
|
|
|
Catch interp_inter_imp up with interp.
WARNING: This commit triggers an exponential performance bug in Lem. To alleviate this bug, I am running with a locally modified Lem that has line 1321 of lem/src/typed_ast.ml commented out
(On my laptop, I gave up trying to compile after about 900 seconds; beefier computers May be able to run unmodified, I don't know)
|
|
under two minutes
|
|
Check point where Lem will compile interpreter in under 2 minutes
|
|
|
|
This introduced a bug in vector.sail, commented out and needs to be fixed.
|
|
|
|
Also allows register writing functions to be on the left hand side of an assignment in the same way.
The last parameter to a writing function is the value to be written, and should appear on the right hand side of an assignment expression.
|
|
|
|
remember why) for ppcmem integration.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
interpreter.
An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter.
|
|
as a pattern is matched without using an unknown; also causes full expansion on function calls with unknowns matched in patterns, however the local state is not reset.
|
|
|
|
|
|
|
|
|
|
|
|
(plus a few other small related corrections)
|
|
constraint solving (instead of hardcoding 64 as the default).
|
|
|
|
|
|
|
|
|
|
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
|