summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_inter_imp.lem
AgeCommit message (Collapse)Author
2016-09-13Add optional address to memv eventsKathy Gray
2016-09-13add show functions, fixChristopher Pulte
2016-09-13extern slice for instruction analysisKathy Gray
2016-09-09update instruction_analysis to support nias and instruction kindChristopher Pulte
2016-09-02Extend type checking so that patterns with vector concatenation don't permit ↵Kathy Gray
under specified vector lengths (at least for function patterns) Extend interpreter interface to have a function for Christopher's instruction analysis
2016-08-17Fix pattern match bug in interp where vector accesses were using the wrong ↵Kathy Gray
start index
2016-07-25winKathy Gray
2016-07-25one more goKathy Gray
2016-07-25Actually fix stack for returnKathy Gray
2016-07-23Add a return exp form to Sail, supported in type checker and in interpreter.Kathy Gray
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
2016-06-07Fix issue in accessing fields and slices of registers during translate addressKathy Gray
2016-06-03Fix bug exposed/introduced by properly handling vector starts in the type ↵Kathy Gray
checker
2016-05-04Correct register field/slice reading for decreasing reads for ↵Kathy Gray
decode/translate_address/exhaustive. (Was previously correct for full register reads)
2016-05-03write all or part of fields out of translate_address (instead of just all)Kathy Gray
fix bug in interp_to_value_helper
2016-05-03Change decode and translate_address to support writing register events ↵Kathy Gray
(although decode isn't pushed through yet). Note: this will break all builds
2016-04-26Add more cases for translate_address to support enumsKathy Gray
2016-04-26print error case on translate addressKathy Gray
2016-04-25Make interpreter able to read registers during translate address and decode.Kathy Gray
This is not yet connected to any model and not yet tested. Also, reduce the number of parentheses needed by the parser. Namely, register declarations should no longer need parens around the types and let expressions should need fewer instances of parens around the expression (i.e. let a = exp ).
2016-04-18More fixes to interp with regards to warnings and debugging infoKathy Gray
2016-04-12Reduce warnings for interpreter. Removed all pattern match warnings for ↵Kathy Gray
interp_lib, interp_inter_imp, and printing_functions.
2016-03-08Start task of setting up tagged memory in sequential interpreterKathy Gray
2016-02-02Get mips stuff hooked up with translate address.Kathy Gray
Note: this support is rather mips centric at the moment
2016-02-02add translate_address functionalityKathy Gray
2016-01-28Support exit and assert better in sequential interpreter and general ↵Kathy Gray
interpreter interface
2016-01-27Make mips build againKathy Gray
Make quiet mode for sequential interpreter not print
2016-01-26Fix some bugs in writing registers with slices in the sequential interpreterKathy Gray
2016-01-20Decoding a mips instruction :)Kathy Gray
Not executing yet as some previous commit has broken the interpreter's local assignment
2016-01-11Interpreter interface now supports option<ast> result from decode and etc ↵Kathy Gray
instead of looking for exit calls
2015-10-08augment annot of interpreterKathy Gray
2015-08-06Update analysis to merge states and values after branches taken due to ↵Kathy Gray
unknown conditions. Does not merge if one path has resulted in an exit
2015-07-24Begin doing better analysis on case splits over unknownsKathy Gray
2015-07-01fix equality comparisonKathy Gray
2015-07-01Use set instead of list for tainted valuesKathy Gray
2015-07-01Go on despite the presence of an exit in exhaustive modeKathy Gray
2015-06-28Tag enumeration variables properly when introducing themKathy Gray
2015-06-26Better handling of literal true and false (turn them into the expected bit0 ↵Kathy Gray
and bit1); also fix some handling of wmv and eamem.
2015-06-24Support new write memory eventsKathy Gray
2015-06-24Add new outcomes/events separating effective address and value for memory writesKathy Gray
2015-06-22Fixes issue #12Kathy Gray
2015-06-18Consistent handling of constructors with no parametersKathy Gray
2015-06-17Extend mode and external memory functions with endian flagKathy Gray
2015-06-09Too hasty removal; still used by trans_sail.genKathy Gray
2015-06-09remove superfluous num_to_bits; replaced by bit_list_of_integerKathy Gray
2015-06-09support exit/escape out of the interfaceKathy Gray
2015-06-07Fix instruction extractorKathy Gray
2015-06-02Fix errors around ARM not being able to decode due to instruction_extractor ↵Kathy Gray
being very power-specific. Note: slight interface change to instruction_extractor
2015-05-13Add dynamic footprint dependency check event/outcomeKathy Gray
Also fix type checker bug in not reporting modifications to parameter values
2015-05-01Change interpreter interface to support ppcmem2's view of vectors as always ↵Kathy Gray
increasing while supporting inc and dec views to the interpreter and in printing Fix bugs exposed by running idlarm several instructions (after fixing above)
2015-04-22Fix some interpreter bugs preventing ARM instructions from making progressKathy Gray
2015-03-18Use boolean on write where applicableKathy Gray
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 21:51:13 +0000