summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_inter_imp.lem
AgeCommit message (Collapse)Author
2017-11-17Fix interpreter to work with new typecheckerAlasdair Armstrong
Need to map sail type annotations to interpreter type annotations in lem_ast ouput. This doesn't seem too hard.
2017-07-24interpreter: optionally print debugging tracesJon French
2017-07-24move value type definitions to ott, and introduce new E_internal_value ast ↵Jon French
node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node
2017-05-28fixed exmemShaked Flur
2017-05-24Merge branch 'master' of bitbucket.org:Peter_Sewell/sailShaked Flur
# Conflicts: # src/lem_interp/interp.lem # src/lem_interp/interp_inter_imp.lem # src/lem_interp/interp_interface.lem # src/parser.mly # src/pretty_print_lem.ml
2017-05-24added the exmem effect for AArch64 store-exclusiveShaked Flur
2017-05-24Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from ↵Robert Norton
data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 14:35:40 +0000