summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_inter_imp.lem
AgeCommit message (Collapse)Author
2019-07-31Revert "Need to separate out the 0.10 lem library from upcoming 0.11"Alasdair Armstrong
This reverts commit 3fb4cf236c0d4b15831576faa45c763853632568.
2019-07-18Need to separate out the 0.10 lem library from upcoming 0.11Alasdair Armstrong
Unlike the prompt-monad change I don't see a way to do this easily purely on the model side Make sure a64_barrier_type and domain aren't visible for RISC-V isabelle build
2019-07-18Support DMB/DSB domainsShaked Flur
2018-02-17Merge master branch into sail2 for OCaml 4.06 compatibilityThomas Bauereiss
2018-02-08replaced NIA_LR/CTR/register with NIA_indirect;Shaked Flur
removed IK_cond_branch, and added IK_branch
2017-12-05Update header files on masterAlasdair Armstrong
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-11-30Merge branch 'master' into experimentsAlasdair Armstrong
2017-11-29Better lem_ast tagging and interpreter tweaksAlasdair Armstrong
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-10-09add translations for missing read/write kinds.Robert Norton
2017-10-09add translation of IK_mem_rmw interp_inter_imp. TODO: could we get rid of ↵Robert Norton
this and use shallow embedding conversion?
2017-10-06move nias_of_instruction into RMEM so that it can use shallow embedding ast ↵Robert Norton
and not obsolete interp_interface one.
2017-09-29fix deep_shallow_convert, stop using interp_interface.instruction for most ↵Christopher Pulte
things, SF and CP bugfixing
2017-09-15x86: implement regfp analysis function (no control flow yet)Robert Norton
2017-08-31added RISC-V AMOsShaked Flur
2017-08-22added RISC-V "fence w,w" and "fence.i";Shaked Flur
fixed the interpreter nias analysis;
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:38:51 +0000