Begin refactoring Sail library

- Add back support for bit list representation of bit vectors, for backwards
  compatibility in order to ease integration with the interpreter.  For this
purpose, split out a file sail_operators.lem from sail_values.lem, and add a
variant sail_operators_mwords.lem for the machine word representation of
bitvectors.  Currently, Sail is hardcoded to use machine words for the
sequential state monad, and bit lists for the free monad, but this could be
turned into a command line flag.

- Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem
  library.  The wrappers make use of sizeof expressions to extract type
information from bitvectors (length, start index) in order to pass it to the
Lem functions.

- Add early return support to the free monad, using a new constructor "Return
  of 'r".  As with the sequential monad, functions with early return are
wrapped into "catch_early_return", which extracts the return value at the end
of the function execution.

1 files changed, 13 insertions, 10 deletions

diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 0cdeb414..167e7de9 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -779,32 +779,35 @@ end
 
 (* the address_lifted types should go away here and be replaced by address *)
 type with_aux 'o = 'o * maybe ((unit -> (string * string)) * ((list (reg_name * register_value)) -> list event))
-type outcome 'a =
+type outcome_r 'a 'r =
   (* Request to read memory, value is location to read, integer is size to read,
      followed by registers that were used in computing that size *)
-  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome 'a))
+  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome_r 'a 'r))
   (* Tell the system a write is imminent, at address lifted, of size nat *)
-  | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome 'a))
+  | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome_r 'a 'r))
   (* Request the result of store-exclusive *)
-  | Excl_res of (bool -> with_aux (outcome 'a))
+  | Excl_res of (bool -> with_aux (outcome_r 'a 'r))
   (* Request to write memory at last signalled address. Memory value should be 8
      times the size given in ea signal *)
-  | Write_memv of memory_value * (bool -> with_aux (outcome 'a))
+  | Write_memv of memory_value * (bool -> with_aux (outcome_r 'a 'r))
   (* Request a memory barrier *)
-  | Barrier of barrier_kind * with_aux (outcome 'a)
+  | Barrier of barrier_kind * with_aux (outcome_r 'a 'r)
   (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint of with_aux (outcome 'a)
+  | Footprint of with_aux (outcome_r 'a 'r)
   (* Request to read register, will track dependency when mode.track_values *)
-  | Read_reg of reg_name * (register_value -> with_aux (outcome 'a))
+  | Read_reg of reg_name * (register_value -> with_aux (outcome_r 'a 'r))
   (* Request to write register *)
-  | Write_reg of (reg_name * register_value) * with_aux (outcome 'a)
+  | Write_reg of (reg_name * register_value) * with_aux (outcome_r 'a 'r)
   | Escape of maybe string
   (*Result of a failed assert with possible error message to report*)
   | Fail of maybe string
-  | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome 'a)
+  (* Early return with value of type 'r *)
+  | Return of 'r
+  | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome_r 'a 'r)
   | Done of 'a
   | Error of string
 
+type outcome 'a = outcome_r 'a unit
 type outcome_s 'a = with_aux (outcome 'a)
 (* first string : output of instruction_stack_to_string
    second string: output of local_variables_to_string *)