summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-01-27failing test with c128Robert Norton
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-25Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sailKathy Gray
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 cheri 256 and 128 together factoring out differing parts into separate ↵Robert Norton
cheri_prelude files.
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-24Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sailChristopher Pulte
2017-01-24functionality for comparing handwritten analysis function with exhaustive ↵Christopher Pulte
interpreter
2017-01-24first pass at cheri128 sail.Robert Norton
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-14update pretty printing to actually reflect lem ast changesKathy Gray
2017-01-14changes to enable interpreter exhaustive analysis in ppcmem againChristopher Pulte
2017-01-12Adding sample generated power fileKathy Gray
2017-01-07Turn back on resolving branch nexp unification more than once. This is the ↵Kathy Gray
right thing to do because otherwise the order of the resolution of branch constraints matters, and that's not easily controllable. This will require figuring out why it's infinite looping for ASL's checking rather than just turning it off.
2016-12-12pp fixChristopher Pulte
2016-12-12cheri sail export progressChristopher Pulte
2016-12-09sail changes for making lem embedding Isabelle-friendlierChristopher Pulte
2016-12-08add target for building cheri_notlb.lemRobert Norton
2016-12-02fix interpreter build following refactoringRobert Norton
2016-12-01move interpreter-specific types from Sail_impl_base to Interp_interfaceChristopher Pulte
2016-11-30shallow embedding fix, rename 'copy' to 'reset_vector_start', don't print ↵Christopher Pulte
shallow/deep ast conversion type class instances anymore, add herdtools ast / shallow ast conversion functions, add mips ImplementationDefinedStopFetching instruction
2016-11-30add new barrier kind for MIPS (only one for now).Robert Norton
2016-11-28make sail produce prompt and state version of shallow embedding files at the ↵Christopher Pulte
same time with the types both have in common factored out into separate file, rename one mips shallow embedding _extras file as required by this
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-23Make type checker not run to fix point on resolving case-split type ↵Kathy Gray
variables; modern implementation of nexp unification seems not to need it
2016-11-23Add new type checking file. Small changes to type inference, temporary ↵Kathy Gray
change to printing
2016-11-22fix mips MakefileChristopher Pulte
2016-11-15wrap state monad into list monoad for non-deterministic write exclusive ↵Christopher Pulte
operations
2016-11-14add option -lem_sequential for producing shallow embedding that refers to ↵Christopher Pulte
state monad, library fixes
2016-11-10rewrite state.lemChristopher Pulte
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-05Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sailChristopher Pulte
2016-11-05fixesChristopher Pulte
2016-11-03split out RI node so that ppcmem model does not implement reserved ↵Robert Norton
instruction exception behaviour but sequential model does (for test suite).
2016-11-02shallow embedding library fixes, logfile pp fixesChristopher Pulte
2016-10-28shallow embedding progressChristopher Pulte
2016-10-27more shallow embedding fixesChristopher Pulte
2016-10-26Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sailChristopher Pulte
2016-10-26shallow embedding 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 04:12:23 +0000