Small tweaks to interp_interface interface

Also adding more comments and getting the ml files built in the build process

3 files changed, 74 insertions, 35 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 14745763..4e4ca4ab 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -10,6 +10,9 @@ val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name
 
 let build_context defs = Interp.to_top_env defs
 
+let make_mode eager_eval tracking_values = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values |>;;
+let tracking_dependencies mode = mode.Interp.track_values
+
 let to_bits l = (List.map (fun b -> match b with
                                | false -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) 
 			       | true ->  (Interp.V_lit (L_aux L_one Interp_ast.Unknown)) end) l)
@@ -64,7 +67,7 @@ type mem_function = (string *
   Should probably be expanded into a parameter to mode as with above
 *)
 let memory_functions =
-  [ ("MEM", (Just(Interp.Read_plain), Just(Interp.Write_plain), (fun mode v -> extern_value mode true v)));
+  [ ("MEM", (Just(Read_plain), Just(Write_plain), (fun mode v -> extern_value mode true v)));
   ]
 
 let rec interp_to_outcome mode thunk = 
@@ -97,7 +100,7 @@ let rec interp_to_outcome mode thunk =
       | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
       end 
     | Interp.Barrier (Id_aux (Id i) _) lval ->
-      Barrier Interp.Plain next_state (* TODO set up some barrier functions and see if the value would be anything needed *)
+      Barrier Plain next_state (* TODO set up some barrier functions and see if the value would be anything needed *)
     | Interp.Nondet exps -> 
       let nondet_states = List.map (Interp.set_in_context next_state) exps in
       Nondet_choice nondet_states next_state      
@@ -126,6 +129,4 @@ let rec ie_loop mode i_state =
     | Internal _ next -> (ie_loop mode next)
      end ;;
   
-let interp_exhaustive i_state = 
-  let mode = <| Interp.eager_eval = true; Interp.track_values = false; |> in
-  ie_loop mode i_state
+let interp_exhaustive mode i_state = ie_loop mode i_state
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index a1ddef88..b1275d14 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -2,19 +2,29 @@ import Interp
 open import Pervasives
 open import Num
 
-type read_kind = Interp.read_kind
-type write_kind = Interp.write_kind
-type barrier_kind = Interp.barrier_kind
-
 type word8 = nat (* bounded at a byte, for when lem supports it*)
 
+(* Abstract types, to be accessed only through this interface *)
+type instruction_state = Interp.stack
+type context = Interp.top_level
+type interp_mode = Interp.interp_mode
+val make_mode : bool -> bool -> interp_mode
+val tracking_dependencies : interp_mode -> bool
+
+(*Concrete types*)
+type read_kind = Read_plain | Read_reserve | Read_acquire
+type write_kind = Write_plain | Write_conditional | Write_release
+type barrier_kind = Plain | Sync | LwSync | Eieio | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD
+
 type value = 
-| Bitvector of list bool (* For register accesses *)
+| Bitvector of list bool   (* For register accesses *)
+(*To discuss:  ARM8 uses at least one abstract record form for 
+  some special registers, with no clear mapping to bits. Should
+  we permit Record of (string * Bitvector) values as well?
+*)
 | Bytevector of list word8 (* For memory accesses *)
 | Unknown
-
-type instruction_state = Interp.stack
-type context = Interp.top_level
+(*To add: an abstract value representing an unknown but named memory address?*)
 
 type slice = (integer * integer)
 
@@ -49,19 +59,25 @@ type event =
 | E_read_reg of reg_name
 | E_write_reg of reg_name * value
 | E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*)
-(*Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
+(*To discuss: Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
 
+(* Functions to build up the initial state for interpretation *)
+val build_context : Interp_ast.defs Interp.tannot -> context (*defs should come from a .lem file generated by Sail*)
+val initial_instruction_state : context -> string -> list value -> instruction_state 
+  (* string is a function name, list of value are the parameters to that function *)
 
-val build_context : Interp_ast.defs Interp.tannot -> context
-val initial_instruction_state : context -> string -> value -> instruction_state
-
-type interp_mode = Interp.interp_mode 
+(* Big step of the interpreter, to the next request for an external action *)
+(* When interp_mode has eager_eval false, interpreter is (close to) small step *)
 val interp : interp_mode -> instruction_state -> outcome
 
-val interp_exhaustive : instruction_state -> list event
+(* Run the interpreter without external interaction, feeding in Unknown on all reads *)
+val interp_exhaustive : interp_mode -> instruction_state -> list event
+
+(* As above, but will request register reads: outcome will only be rreg, done, or error *)
+val rr_interp_exhaustive : interp_mode -> instruction_state -> list event -> (outcome * (list event)) 
 
-val rr_interp_exhaustive : instruction_state -> list event -> (outcome * (list event)) (* Like interp_exhaustive but will read registers; the outcome will only ever be a rreg request, done, or error *)
 
+(*To discuss: Are these functions needed, since the memory requests carry the register dependencies for that request? *)
 val mem_read_analysis : instruction_state -> list event (*Should record all rreg events where the registers are involved in memory reads to compute the addressses in is*)
 
 val mem_write_analysis : instruction_state -> list event (*Should record all rreg events where the registers are involved in memory writes to compute the address (and value?, in a separate list?)*)
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index e5d916a3..91930974 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -2,6 +2,8 @@ open Printf ;;
 open Interp_ast ;;
 open Interp ;;
 open Interp_lib ;;
+open Interp_interface ;;
+open Interp_inter_imp ;;
 
 open Big_int ;;
 
@@ -45,33 +47,53 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
   | _ -> assert false) l))
 ;;
 
+let val_to_string v = match v with
+  | Bitvector bools -> "0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))
+  | Bytevector words ->
+    "0x" ^ (String.concat ""
+	    (List.map (function 
+	      | 10 -> "A"
+	      | 11 -> "B"
+	      | 12 -> "C"
+	      | 13 -> "D"
+	      | 14 -> "E"
+	      | 15 -> "F"
+	      | i  -> string_of_int i) words))		
+  | Unknown0 -> "Unknown"
+
+let reg_name_to_string = function
+  | Reg0 s -> s
+  | Reg_slice(s,(first,second)) -> s (*contemplate putting slice here*)
+  | Reg_field(s,f,_) -> s ^ "." ^ f
+  | Reg_f_slice(s,f,_,(first,second)) -> s ^ "." ^ f
+
 let rec reg_to_string = function
   | Reg (id,_) -> id_to_string id
   | SubReg (id,r,_) -> sprintf "%s.%s" (reg_to_string r) (id_to_string id)
 ;;
 
-let rec val_to_string = function
+let rec val_to_string_internal = function
  | V_boxref(n, t) -> sprintf "boxref %d" n
  | V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l)
  | V_tuple l ->
-     let repr = String.concat ", " (List.map val_to_string l) in
+     let repr = String.concat ", " (List.map val_to_string_internal l) in
      sprintf "(%s)" repr
  | V_list l ->
-     let repr = String.concat "; " (List.map val_to_string l) in
+     let repr = String.concat "; " (List.map val_to_string_internal l) in
      sprintf "[||%s||]" repr
  | V_vector (first_index, inc, l) ->
      let last_index = add_int_big_int (if inc then List.length l - 1 else 1 - List.length l) first_index  in
      let repr =
        try bitvec_to_string (* (if inc then l else List.rev l)*) l
        with Failure _ ->
-         sprintf "[%s]" (String.concat "; " (List.map val_to_string l)) in
+         sprintf "[%s]" (String.concat "; " (List.map val_to_string_internal l)) in
      sprintf "%s [%s..%s]" repr (string_of_big_int first_index) (string_of_big_int last_index)
  | V_record(_, l) ->
-     let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string value) in
+     let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal value) in
      let repr = String.concat "; " (List.map  pp l) in
      sprintf "{%s}" repr
  | V_ctor (id,_, value) ->
-     sprintf "%s %s" (id_to_string id) (val_to_string value)
+     sprintf "%s %s" (id_to_string id) (val_to_string_internal value)
  | V_register r ->
      sprintf "reg-as-value %s" (reg_to_string r)
  | V_unknown -> "unknown"
@@ -146,7 +168,7 @@ let id_compare i1 i2 =
 module Reg = struct
   include Map.Make(struct type t = id let compare = id_compare end)
   let to_string id v =
-    sprintf "%s -> %s" (id_to_string id) (val_to_string v)
+    sprintf "%s -> %s" (id_to_string id) (val_to_string_internal v)
   let find id m =
 (*    eprintf "reg_find called with %s\n" (id_to_string id);*)
     let v = find id m in
@@ -191,7 +213,7 @@ module Mem = struct
     v
   *)
   let to_string idx v =
-    sprintf "[%s] -> %s" (string_of_big_int idx) (val_to_string v)
+    sprintf "[%s] -> %s" (string_of_big_int idx) (val_to_string_internal v)
 end ;;
 
 
@@ -347,7 +369,7 @@ let run
   in
   let rec loop mode env = function
   | Value v ->
-      debugf "%s: %s %s\n" (grey name) (blue "return") (val_to_string v);
+      debugf "%s: %s %s\n" (grey name) (blue "return") (val_to_string_internal v);
       true, mode, env
   | Action (a, s) ->
       let top_exp = top_frame_exp s in
@@ -364,25 +386,25 @@ let run
       let left = "<-" and right = "->" in
       let (mode',env',s) = begin match a with
       | Read_reg (reg, sub) ->
-          show "read_reg" (reg_to_string reg ^ sub_to_string sub) right (val_to_string return);
+          show "read_reg" (reg_to_string reg ^ sub_to_string sub) right (val_to_string_internal return);
           step (),env',s
       | Write_reg (reg, sub, value) ->
           assert (return = unit_lit);
-          show "write_reg" (reg_to_string reg ^ sub_to_string sub) left (val_to_string value);
+          show "write_reg" (reg_to_string reg ^ sub_to_string sub) left (val_to_string_internal value);
           step (),env',s
       | Read_mem (id, args, sub) ->
-          show "read_mem" (id_to_string id ^ val_to_string args ^ sub_to_string sub) right (val_to_string return);
+          show "read_mem" (id_to_string id ^ val_to_string_internal args ^ sub_to_string sub) right (val_to_string_internal return);
           step (),env',s
       | Write_mem (id, args, sub, value) ->
           assert (return = unit_lit);
-          show "write_mem" (id_to_string id ^ val_to_string args ^ sub_to_string sub) left (val_to_string value);
+          show "write_mem" (id_to_string id ^ val_to_string_internal args ^ sub_to_string sub) left (val_to_string_internal value);
           step (),env',s
       (* distinguish single argument for pretty-printing *)
       | Call_extern (f, (V_tuple _ as args)) ->
-          show "call_lib" (f ^ val_to_string args) right (val_to_string return);
+          show "call_lib" (f ^ val_to_string_internal args) right (val_to_string_internal return);
           step (),env',s
       | Call_extern (f, arg) ->
-          show "call_lib" (sprintf "%s(%s)" f (val_to_string arg)) right (val_to_string return);
+          show "call_lib" (sprintf "%s(%s)" f (val_to_string_internal arg)) right (val_to_string_internal return);
           step (),env',s
       | Step _ ->
           assert (return = unit_lit);