summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-07-08Extend language to support register aliases and to support interrupts, traps ↵Kathy Gray
and the like.
2014-07-08add additional cases for nexp normalisationKathy Gray
2014-07-04Relax constraints for quot_vecGabriel Kerneis
2014-07-04Correct error of forgetting type information that was allowing more programs ↵Kathy Gray
than it should have
2014-07-04Update power.sailGabriel Kerneis
2014-07-04Fix pretty printer for verbose printingKathy Gray
2014-07-04Force end-of-input when parsing expression listGabriel Kerneis
2014-07-03Parse list of expressions in Sail_libGabriel Kerneis
2014-07-03Introduce a Sail libraryGabriel Kerneis
Used by the Power XML extraction tool.
2014-07-03Adjust behavior on Unknown values in pattern match to stop matching as soon ↵Kathy Gray
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.
2014-07-02Support implicit parameters, to get the length of an expected vector into ↵Kathy Gray
functions like exts
2014-07-02Update Power exampleGabriel Kerneis
2014-07-02Fix ordering issue in vector-concat pattern matchingGabriel Kerneis
2014-07-01Better pretty-printing for vectorsGabriel Kerneis
2014-07-01Update case of EXTSGabriel Kerneis
2014-06-30Support for nondeterministic blocksKathy Gray
2014-06-27Update type conformance for overloading resolution on order arguments.Kathy Gray
Also, correctly type check nondet blocks
2014-06-26range -> vector coerces only on constants and explicit castsKathy Gray
2014-06-26Remove .native in make cleanGabriel Kerneis
2014-06-26Adding better support for unspecified values in indexed vectorsKathy Gray
Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches
2014-06-25Add support for memory barrierKathy Gray
2014-06-25Add support for actions that read just a slice or single bit of a registerKathy Gray
2014-06-24Get enumerations working in interpreterKathy Gray
(plus a few other small related corrections)
2014-06-24Get vector length for to_inc_vec and to_dec_vec from the type system after ↵Kathy Gray
constraint solving (instead of hardcoding 64 as the default).
2014-06-23Get indexed vectors, particularly with default values, workingKathy Gray
2014-06-19Add mod:vec->range->vecGabriel Kerneis
2014-06-18reinstate range to vector coercionsKathy Gray
2014-06-18Fix mod_vec in libraryGabriel Kerneis
2014-06-18Correct effect matching bug; and print out effect listsKathy Gray
2014-06-18Add definition of mod to libKathy Gray
2014-06-18Make hex constants work; improve utility of casts for selecting overloaded ↵Kathy Gray
functions
2014-06-12Overloaded multiplicationGabriel Kerneis
Hopefully I got the constraints right again.
2014-06-12Interpret when an unknown is inserted into the program by interp_exhaustiveKathy Gray
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.
2014-06-12Add uint* to default type names for lexerGabriel Kerneis
This is necessary to avoid a parse error. It might make sense to merge this list and the one in type_internal.ml somehow, to avoid duplication and similar bugs in the future.
2014-06-11power.sail: store mode64bit in a bool registerGabriel Kerneis
This is now possible because we handle coercions better.
2014-06-11Update power.sail: remove some hacksGabriel Kerneis
2014-06-11Equality between range and bit vectorGabriel Kerneis
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.
2014-06-11Improve error message for missing library functionsGabriel Kerneis
2014-06-10Minor color and build tweaksGabriel Kerneis
2014-06-10More colorsGabriel Kerneis
2014-06-10More robust build systemGabriel Kerneis
2014-06-09Better, colored holeGabriel Kerneis
2014-06-09Improve interaction after chat with PeterGabriel Kerneis
- 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"
2014-06-09Support deinfix pretty-printingGabriel Kerneis
2014-06-09Add more stops in interpreter (stopping just at the point of each internal ↵Kathy Gray
function call) Also turning off an annoying printf I left in.
2014-06-09Working towards evaluating with interp_exhaustiveKathy Gray
2014-06-09Add "continuation" command in interpreterGabriel Kerneis
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.
2014-06-09Add switch to show/hide casts in interpreterGabriel Kerneis
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).
2014-06-09Add explicit flag -r to rebuild in demo.shGabriel Kerneis
./demo.sh now jumps straight into the interpreter. ./demo.sh -r does the fancy "rebuild step-by-step with comments" show
2014-06-09Merge branch 'for-dagstuhl' into masterGabriel Kerneis
Conflicts: src/lem_interp/interp_lib.lem src/lem_interp/run_interp.ml Remove "to_vec_safe" work-around
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 19:14:34 +0000