summaryrefslogtreecommitdiff
path: root/src/lem_interp/sail_impl_base.lem
AgeCommit message (Collapse)Author
2017-09-29fix deep_shallow_convert, stop using interp_interface.instruction for most ↵Christopher Pulte
things, SF and CP bugfixing
2017-09-21added a comment to the x86 lock'd read and writeShaked Flur
2017-09-20add support for x86 lock prefix (also remove unused Read/Write_tag kind in ↵Robert Norton
etc/regfp.sail.
2017-09-15reinstate deep/shallow conversionChristopher Pulte
2017-09-03added RISC-V strong-acquire/releaseShaked Flur
2017-08-31add EnumerationType type class: if a type is a member you get Ord membership ↵Christopher Pulte
and Set membership for free
2017-08-31added RISC-V AMOsShaked Flur
2017-08-30typeclass instance Ord(opcode)Christopher Pulte
2017-08-24typoShaked Flur
2017-08-24typoShaked Flur
2017-08-24added barrier-kind for x86 MFENCE;Shaked Flur
fixed some compare functions;
2017-08-22added RISC-V "fence w,w" and "fence.i";Shaked Flur
fixed the interpreter nias analysis;
2017-08-19RISC-V store-releaseShaked Flur
2017-08-17added RISC-V load-acquireShaked Flur
2017-08-17fixed the RISC-V fences (3 types: "rw,rw"/"r,rw"/"rw,w")Shaked 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-05-02docPeter Sewell
2017-04-24added register_value_for_regShaked Flur
2017-04-18added transactional memory supportShaked Flur
2017-03-24fixed endiannessShaked Flur
2017-03-23the interpreter/shallow expects little-endian memory-valuesShaked Flur
2017-02-08put back the header into Sail_impl_baseChristopher Pulte
2017-02-08pull in Shaked's type class instance changes, fix Ord and Eq instancesChristopher Pulte
2017-02-03fix headersPeter 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-11-05fixesChristopher Pulte
2016-10-25shallow embedding fixesChristopher Pulte
2016-10-24fixes, check in Shaked's sail_impl_base changesChristopher Pulte
2016-10-21shallow embedding progressChristopher Pulte
2016-10-19remove effect list from instruction typeChristopher Pulte
2016-10-08type class instance fixesChristopher 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 21:07:31 +0000