summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_inter_imp.lem
AgeCommit message (Collapse)Author
2017-04-18added transactional memory supportShaked Flur
2017-04-03Rename TranslateAddress to TranslatePC and remove the accessType argument -- ↵Robert Norton
it is only ever used for translating the PC.
2017-03-24Print tracking information for V_track, hopefully fix extern_vector_value, ↵Christopher Pulte
fix sail_values bug.
2017-03-23the interpreter/shallow expects little-endian memory-valuesShaked Flur
2017-02-03fix headersPeter Sewell
2017-01-26christopher, kathy, peter: hacky experiment on nias_of_instructionPeter Sewell
2017-01-24functionality for comparing handwritten analysis function with exhaustive ↵Christopher Pulte
interpreter
2017-01-14changes to enable interpreter exhaustive analysis in ppcmem againChristopher Pulte
2016-12-09sail changes for making lem embedding Isabelle-friendlierChristopher Pulte
2016-12-01move interpreter-specific types from Sail_impl_base to Interp_interfaceChristopher Pulte
2016-11-30add new barrier kind for MIPS (only one for now).Robert Norton
2016-11-27make outcome_s contain the instruction state pretty print rather than the ↵Christopher Pulte
instruction state, factor out interpreter/shallow embedding value conversion
2016-11-09move decode_error type back to Sail_impl_base for nowChristopher Pulte
2016-11-08fixesChristopher Pulte
2016-11-07factor out regfp analysis types into etc/regfp.sailChristopher Pulte
2016-10-25fix my decode_to_istate bugChristopher Pulte
2016-10-21shallow embedding progressChristopher Pulte
2016-10-20factor out instr_external_to_interp_valueChristopher Pulte
2016-10-20fix previous FromToInterpValue typeclass issue, factor out intpreter's ↵Christopher Pulte
interp_value_to_instr_external
2016-10-19fixChristopher Pulte
2016-10-19remove effect list from instruction typeChristopher Pulte
2016-10-06move type definitions that both interpreter and shallow embedding use to ↵Christopher Pulte
sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome
2016-09-30fixes, update isntruction_analysis for NIAs and DIAChristopher Pulte
2016-09-21fixesChristopher Pulte
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-14 01:24:19 +0000