summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-04-21implement to_vec_big using zarith extract for some speedup.Robert Norton
2017-04-21suppress register field tracing if not enabled (missed in previous commit)Robert Norton
2017-04-21add make variable for setting ocaml compilation options (e.g. set to -p to ↵Robert Norton
enable gprof profiling)
2017-04-20more library optimisation. Implement int_of_bit_array using shift, avoiding ↵Robert Norton
need to use power.
2017-04-20implement vector subrange using Array.sub for approx 10% speedup.Robert Norton
2017-04-20remove unnecessary lemlib include in compile.Robert Norton
2017-04-20add support for cheri128 ocaml shallow embeddingRobert Norton
2017-04-20add brackets around integer literals so that ocaml parses them correctly and ↵Robert Norton
doesn't mistake the - for minus operator
2017-04-20build a single run_embed.native with mips and cheri models linked and choose ↵Robert Norton
between them using a command line switch.
2017-04-20attempt to optimise performance if not tracing writes.Robert Norton
2017-04-20add missing min and max functions, overriding built-in ocaml ones. Also ↵Robert Norton
neq_range.
2017-04-20add missing KD_nabbrev support in ocaml shallow embedding.Robert Norton
2017-04-20support assert in ocaml shallow embedding.Robert Norton
2017-04-20use mangled field name when accessing record field.Robert Norton
2017-04-20add name to register representation and print it on write.Robert Norton
2017-04-18make ocaml embedding of foreach use (now universal) big_ints.Robert Norton
2017-04-18fix definition of mask -- Vregister and VvectorR were swapped.Robert Norton
2017-04-18Implement return using an exception caught in the function body. Polymorphic ↵Robert Norton
exceptions are not permitted so a local mutable variable, ret, is used in ocaml to store the return value. This avoids having to define a new exception type for each function. Ocaml infers the type of the option when it is assigned at the return site.
2017-04-18Generate runtime error for L_undef. Existing code was broken except for type ↵Robert Norton
bit (specifically it caused generated ocaml to fail to type check for an undef number.
2017-04-18added transactional memory supportShaked Flur
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-06use set_register when writing element of vector of registers to avoid ↵Robert Norton
accidentally replacing Vregister with Vvalue or Vregister... Seems to work for MIPS but not sure if might encounter vector of something other than bit or register. A more specific value type would have made this a compile-time error rather than run-time.
2017-04-06add support for address translation and exit handling in mips ocaml shallow ↵Robert Norton
embedding test setup.
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-04-03Rename TranslateAddress to TranslatePC and remove the accessType argument -- ↵Robert Norton
it is only ever used for translating the PC.
2017-03-30Make length function return big_intRobert Norton
2017-03-29change reqiured to work with little endian interpreter.Robert Norton
2017-03-29Factor out pretty printers into separate files. Hopefully this will make ↵Robert Norton
searching easier.
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-25endianness fixShaked Flur
2017-03-24fixed endiannessShaked Flur
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-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-14remove the -i optionPeter Sewell
2017-02-14tidy command-line optionsPeter Sewell
2017-02-09wibPeter Sewell
2017-02-09group initial type environment into meaningful sections; pretty-print in ↵Peter Sewell
user-readable way
2017-02-09tweak pp of initial type environment and l2.ott commentsPeter Sewell