summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_inter_imp.lem
AgeCommit message (Collapse)Author
2014-12-11Many fixes, primarily dealing with undefinedKathy Gray
Including: turn an undefined literal into a vector of undefined values of the correct length handle sparse vector unspecified default values as undefined literals allow global lets to call library functions
2014-12-10Fix mismatch errors in interpreter, mostly relating to taint/detaint behaviourKathy Gray
Also fixed for loop evaluation
2014-11-23make interpreter work better with unknowns, make interp_inter_imp do better ↵Kathy Gray
on coercions
2014-11-23Merge branch 'master' of bitbucket.org:Peter_Sewell/l2Peter Sewell
2014-11-23the properly named "git"Peter Sewell
2014-11-23extern single bit and single bool to instruction_fieldsKathy Gray
2014-11-23Fill in some of the basic coercionsKathy Gray
2014-11-23clean up interp interKathy Gray
2014-11-23more coercionsPeter Sewell
2014-11-23OCaml stubs for coercions and _to_istate OCamlPeter Sewell
2014-11-23wib (comment out to typecheck the rest...)Peter Sewell
2014-11-23fight with interface/impl mismatch. lose.Peter Sewell
2014-11-23update instruction/istate decoding.Kathy Gray
Use register size. Printing again doesn't compile
2014-11-22interp_interface happy again. printing functions now doesn't compileKathy Gray
2014-11-22Add size of register to register for making appropriate unknown register_valuesKathy Gray
2014-11-22Changing interface in step with Peter and ppcmem changesKathy Gray
2014-11-21Support signed and unsigned arithmeticKathy Gray
2014-11-21Fix bugs now documented in ppcmem notesKathy Gray
2014-11-20look for sub matches of registers on exhaustive modeKathy Gray
2014-11-19add byte_list_of_integerKathy Gray
2014-11-19Correct off-by-one bug in type checking vector slicesKathy Gray
Convert sparse vectors into full-fledged vectors more frequently and on export to memory system
2014-11-18Actually expect barriers to happenKathy Gray
2014-11-18Fix countLeadingZeroes typo (diff in number of es present)Kathy 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-13Catch more cases of registers for extern_regKathy Gray
2014-11-13Set start index on bits in extern_valueKathy Gray
2014-11-07Add integer_of_byte_list : list word8 -> integerKathy Gray
2014-11-07typoKathy Gray
2014-11-07more num_to_bitsKathy Gray
2014-11-07Put back old num_to_bits temporarily; add in a num_to_bits_correct that ↵Kathy Gray
treats the last argument as a big num
2014-11-07Fix types in num_to_bitsKathy Gray
2014-11-05Correct bug treating unsigned values as signed in arith operationsKathy Gray
2014-11-05fix(?) a Big_int/int type error wrt trans_sailPeter Sewell
2014-11-04Merge branch 'master' of bitbucket.org:Peter_Sewell/l2Peter Sewell
2014-11-04proposed split of decode into decode-to-instruction and ↵Peter Sewell
instruction-to-instructionstate
2014-11-04Read parts of a register, not always just the whole thingKathy Gray
2014-11-04K,P debuggingPeter Sewell
2014-11-04Fix setting of initial position in a vector after a sliceKathy Gray
2014-10-31Add a num to bits function; start hooking up the power.ml file to the ↵Kathy Gray
symbol/memory address list.
2014-10-30Fix type error that Lem didn't catch with the interpreter aloneKathy Gray
2014-10-30Add parameter to interp_exhaust with type maybe (list (reg_name,value)) for ↵Kathy Gray
registers we might read that we want values for (particularly the PC)
2014-10-28Allow tracking of unknowns in interp library, removing the P hacks.Kathy Gray
Add a function from instruction to istate
2014-10-28function in progress take 2Kathy Gray
2014-10-28hacks on taint trackingPeter Sewell
2014-10-28Function definition in progressKathy Gray
2014-10-28K,P fix constructor-as-variable errorPeter Sewell
2014-10-27Correct externally visible endianness bugsKathy Gray
2014-10-14Iron out bugs in running new executable with branching; add new executable ↵Kathy Gray
as well.
2014-10-10Functions for operating on bit and byte vectors from the interpreter interfaceKathy Gray