summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_lib.lem
AgeCommit message (Collapse)Author
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
2014-03-20Remove work-around from interpreter, move it to power.sailGabriel Kerneis
Two bugs are worked-around here: - missing cast to nat when a vector is wrapped in exts (exts is a no-op currently anyway, so we are discarding it) - missing cast (due to limited type-inference) in one if branch: type given explicitly.
2014-03-20Workaround missing casts for external callsGabriel Kerneis
This patch should be reverted when the interpreter is fixed. The first instruction of main.bin is now executed. The second one fails, seemingly because of a similar missing cast issue (external function add receives register GPR1 as value).
2014-03-11More work on interpreter and Power modelGabriel Kerneis
2014-03-11Confusion between first index and vector lengthGabriel Kerneis
2014-03-04More polymorphism for additionGabriel Kerneis
2014-02-28Fix endiannessGabriel Kerneis
In fact, increasing order is big-endian, not little-endian. This is good news for us, because it means we do not need any switch for the POWER spec.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 14:38:24 +0000