summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_interface.lem
AgeCommit message (Collapse)Author
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-09-29fix deep_shallow_convert, stop using interp_interface.instruction for most ↵Christopher Pulte
things, SF and CP bugfixing
2017-08-02fix sail library test interpreter glue for API change. Also fix ↵Robert Norton
build_context val spec which was out of dated although lem did not complain for some reason...
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-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-03-23the interpreter/shallow expects little-endian memory-valuesShaked Flur
2017-03-02tweak commentsPeter Sewell
2017-02-03fix headersPeter Sewell
2017-01-14changes to enable interpreter exhaustive analysis in ppcmem againChristopher Pulte
2016-12-01move interpreter-specific types from Sail_impl_base to Interp_interfaceChristopher Pulte
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-05fixesChristopher Pulte
2016-10-21shallow embedding progressChristopher 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-30add Robert's DIA typeclass instancesChristopher Pulte
2016-09-30fixes, update isntruction_analysis for NIAs and DIAChristopher Pulte
2016-09-19remove conflict messageChristopher Pulte
2016-09-16make vector concatenation pattern removal deal with vector patterns of ↵Christopher Pulte
unknown length (in the last item)
2016-09-14Add memory kind for concurrent tag reads and writesKathy Gray
2016-09-13Add optional address to memv eventsKathy Gray
2016-09-13add show functions, fixChristopher Pulte
2016-09-09minor fixesKathy 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-18move register_base_name and slice_of_reg_name from ppcmem thread semantics ↵Christopher
to interp_interface, fix reg_name comparison and equality
2016-08-06Add duplicate_bits to libKathy Gray
Pull Peter's changes to interp_interface back into the primary repo
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-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-03-08Return undefined value on reads of uninitialised memoryKathy Gray
2016-03-08Start task of setting up tagged memory in sequential interpreterKathy Gray
2016-02-02add translate_address functionalityKathy Gray
2016-01-29fix typo in kathy's last commit.Robert Norton
2016-01-29Put correct tags on to_vec callsKathy Gray
2016-01-28Support exit and assert better in sequential interpreter and general ↵Kathy Gray
interpreter interface
2016-01-26Fix some bugs in writing registers with slices in the sequential interpreterKathy Gray
2015-11-10Make first half of sequential interpreter driver compile againKathy Gray
2015-07-24Merge branch 'master' of bitbucket.org:Peter_Sewell/l2Shaked Flur
2015-07-24added signed_integerShaked Flur
2015-07-24Begin doing better analysis on case splits over unknownsKathy Gray
2015-07-19abbreviate printing of memory values <=9Peter Sewell
2015-07-01Go on despite the presence of an exit in exhaustive modeKathy Gray
2015-06-24Add new outcomes/events separating effective address and value for memory writesKathy Gray
2015-06-19one more end flag for memory_value functionsKathy Gray
2015-06-18Add more end_flag parametersKathy Gray
2015-06-17Extend mode and external memory functions with endian flagKathy Gray
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:40:38 +0000