summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_lib.lem
AgeCommit message (Collapse)Author
2014-11-23coerce better between a single bit and a bit vector of one bitKathy Gray
2014-11-23maybe best not to die at the first sign of an undef...Kathy Gray
2014-11-23properly name division operators in libKathy Gray
2014-11-23make interpreter now buildsKathy Gray
and I *think* that I'm making vectors of unknowns in all the necessary places now.
2014-11-22signed multiplication and quotKathy Gray
2014-11-22add new function for overflow arithmetic instructionsKathy Gray
2014-11-21Support signed and unsigned arithmeticKathy Gray
2014-11-21Print out default values for underspecified vectors instead of leaving them ↵Kathy Gray
and letting them turn into undefineds
2014-11-20look for sub matches of registers on exhaustive modeKathy Gray
2014-11-18Fix various pattern match bugs; add a few functionsKathy Gray
2014-11-16Add some missing functionsKathy Gray
2014-11-16Add overflow checking arithmetic operations. Fix various bugs that this exposedKathy Gray
Of note: Interp_lib.to_num now takes an Unsigned or a Signed constructor, rather than a boolean
2014-11-05Correct bug treating unsigned values as signed in arith operationsKathy Gray
2014-10-30Add case to neg for interp_libKathy Gray
2014-10-28Allow tracking of unknowns in interp library, removing the P hacks.Kathy Gray
Add a function from instruction to istate
2014-10-28hacks on taint trackingPeter Sewell
2014-10-22Update printing for testing, fix some bugs found along the wayKathy Gray
2014-10-16bug fixes to run test from Christopher's testsKathy Gray
2014-10-14Iron out bugs in running new executable with branching; add new executable ↵Kathy Gray
as well.
2014-09-04Make exhaust run from the first breakpoint in the interactive interpreterKathy Gray
(I still think this is a silly place to run exhaust from, but it no longer finds errors or crashes)
2014-08-27Changes to get another (slightly larger) executable running;Kathy Gray
adding executable as a test as well
2014-08-20Add ability to track register dependencies in interactive stepper; thus ↵Kathy Gray
testing register tracking/tainting
2014-08-13Update library functionsKathy Gray
2014-07-30working dec vectorsKathy Gray
2014-07-01Update case of EXTSGabriel Kerneis
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-19Add mod:vec->range->vecGabriel Kerneis
2014-06-18Fix mod_vec in libraryGabriel Kerneis
2014-06-18Add definition of mod to libKathy Gray
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-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-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
2014-06-07Add optional overloading on expected return type to fix bug in constraint ↵Kathy Gray
solving; get test_power running again by supporting the correct operations and bit operations
2014-06-07exts returns bit[64] instead of natGabriel Kerneis
Update power.sail to new, pretty-printer-based version
2014-06-06Improve work-aroundGabriel Kerneis
Default to 64 bit for vec + range
2014-06-05Refactor to_vec and add work-around to avoid truncationGabriel Kerneis
2014-06-04Fixup type coercions and overloadingKathy Gray
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
2014-05-06Begin tie to ppcmem style actions/outcomesKathy Gray
Change type of + on vectors to (bit vector,bit vector) -> bit vector
2014-05-01Make an overloading type decision (all + operations return ranges, never ↵Kathy Gray
vectors) and make the test suite pass again
2014-04-30More support for overloading functions; primarily focusing on +Kathy Gray
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
2014-04-03Implement some arithmetic operationsGabriel Kerneis
2014-04-03Implement bitwise library operationsGabriel Kerneis
2014-04-03Typeclass Eq for valuesGabriel Kerneis
Again, this is necessary to compare big_int
2014-04-02Solve more constraints; fix up test suite bugs uncovered by solving more ↵Kathy Gray
constraints. Clean up Lem output a little for readability while debugging.
2014-04-02eq and neq return bit, not boolGabriel Kerneis
2014-04-02Fix EXTS and signedness of to_numGabriel Kerneis
2014-04-01Allow negative "nat" internallyGabriel Kerneis
to_num and to_vec probably still need to be fixed
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 07:27:32 +0000