summaryrefslogtreecommitdiff
path: root/src/lem_interp
AgeCommit message (Collapse)Author
2017-05-28fixed exmemShaked Flur
2017-05-26fix run_with builds after build_context gained an extra argument.Robert Norton
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-04-03Rename TranslateAddress to TranslatePC and remove the accessType argument -- ↵Robert Norton
it is only ever used for translating the PC.
2017-03-29change reqiured to work with little endian interpreter.Robert Norton
2017-03-25endianness fixShaked Flur
2017-03-24fixed endiannessShaked Flur
2017-03-24Christopher, Peter: make "run_interp_model.ml" build again (endianness)Peter Sewell
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-03-02tweak commentsPeter Sewell
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-27fix right shiftKathy Gray
2017-01-26c128: xor E with 48 when storing in memory so that null cap is all zeros but ↵Robert Norton
has non-zero E (latest spec.)
2017-01-26christopher, kathy, peter: hacky experiment on nias_of_instructionPeter Sewell
2017-01-25Make interpreter a little more flexible on the format of a register type to ↵Kathy Gray
match ASL; add missing functions/cases to library
2017-01-25Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sailKathy Gray
2017-01-25Make vector equality remember about the possibility of unknown valuesKathy Gray
2017-01-24functionality for comparing handwritten analysis function with exhaustive ↵Christopher Pulte
interpreter
2017-01-24Remember to pass through collapse argument in else case in bit_lifteds_to_stringRobert Norton
2017-01-23remove taint printingKathy Gray
2017-01-23Extend lib with min and maxKathy Gray
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-02fix interpreter build following refactoringRobert Norton
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-23Add new type checking file. Small changes to type inference, temporary ↵Kathy Gray
change to printing
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-11-02shallow embedding library fixes, logfile pp fixesChristopher Pulte
2016-10-25load all segments into prog_mem regardless of x flag (for running cheri ↵Robert Norton
tests all memory is equal
2016-10-25Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sailChristopher Pulte
2016-10-25fix my decode_to_istate bugChristopher Pulte
2016-10-25Improve pattern match failure error messagesKathy Gray
2016-10-25shallow embedding fixesChristopher Pulte
2016-10-24fixes, check in Shaked's sail_impl_base changesChristopher Pulte
2016-10-22Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sailChristopher Pulte
2016-10-22fixes, Interp.value printing for debuggingChristopher Pulte
2016-10-22fixes following interface changes (type of instruction, name of barrier)Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-15 19:09:21 +0000