summaryrefslogtreecommitdiff
path: root/src/gen_lib
AgeCommit message (Collapse)Author
2017-04-07fix error in generated ocaml where writing single bit of register was not ↵Robert Norton
taking account of register direction.
2017-04-07implement quot and mod with truncation towards zero which is not the ocaml ↵Robert Norton
way but standard for C and most hw.
2017-04-07simplify xor using ocaml <> operator which also has the advantage of being ↵Robert Norton
more correct
2017-04-06minor changes in sail_values.ml to aid debuggingRobert Norton
2017-04-06fix incorrect use of == in eqRobert Norton
2017-04-06implement exts and extz as manipulations on bit vectors rather than ↵Robert Norton
converting to integers, allowing them to work on vectors containing undef.
2017-04-06Implement exit by raising Sail_exit exceptionRobert Norton
2017-03-30Make length function return big_intRobert Norton
2017-03-28temporary fix for problem duplicate (lack of direction) -- assume decreasing ↵Robert Norton
for mips compatibility.
2017-03-28Fix erroneous bitwise xor.Robert Norton
2017-03-27fix bitshift operators. I think these should be independent of vector order...Robert Norton
2017-03-27Fix broken to_vec of negative values. Old code was a bit confused. Probably ↵Robert Norton
possible to rewrite using arithmetic on big_int which might be faster.
2017-03-24Checkpoint work-in-progress mips sequential interpreter using ocaml shallow ↵Robert Norton
embedding.
2017-03-24changes to ocaml pp to allow mips->ocaml to compileRobert Norton
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-01-12Adding sample generated power fileKathy Gray
2016-12-09sail changes for making lem embedding Isabelle-friendlierChristopher 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-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-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-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-28shallow embedding progressChristopher Pulte
2016-10-27more shallow embedding fixesChristopher Pulte
2016-10-26shallow embedding fixesChristopher Pulte
2016-10-25shallow embedding fixesChristopher Pulte
2016-10-24fixes, check in Shaked's sail_impl_base changesChristopher Pulte
2016-10-22fixes, Interp.value printing for debuggingChristopher Pulte
2016-10-21shallow embedding progressChristopher Pulte
2016-10-19typeclass instances for converting between shallow and deep embeddingChristopher Pulte
2016-10-11move armv8_extras and power_extras to idl/power and idlarm, fixesChristopher Pulte
2016-10-10changed the way registers/register fields work, fixes, nicer names for new ↵Christopher Pulte
letbound variables
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-26minor changesChristopher Pulte
2016-09-26nicer lem output: fewer unnecessary letbinds, monad binds and returnsChristopher Pulte
2016-09-25nicer lem output: no more unecessary 'unit' returns if if-expressions, ↵Christopher Pulte
for-loops or case-expressions also return updated variables
2016-09-23sail-to-lem progressChristopher Pulte
2016-09-21fixesChristopher Pulte
2016-09-19sail-to-lem progressChristopher Pulte
2016-09-07push some lem pp changesChristopher Pulte
2016-07-12sail-to-lem and lem library fixesChristopher
2016-01-28Support exit and assert better in sequential interpreter and general ↵Kathy Gray
interpreter interface
2015-12-21fixes, pp progressChristopher