Put in type for instruction form for models; remove extra information from Bytevectors; add place holder for memory size dependency tracking

7 files changed, 64 insertions, 132 deletions

diff --git a/src/lem_interp/extract.mllib b/src/lem_interp/extract.mllib
index 6230c0e8..ebca3114 100644
--- a/src/lem_interp/extract.mllib
+++ b/src/lem_interp/extract.mllib
@@ -1,9 +1,10 @@
 Interp_ast
+Interp_utilities
+Instruction_extractor
 Interp
 Interp_lib
 Interp_interface
 Interp_inter_imp
-Instruction_extractor
 
 Pretty_interp
 Run_interp
diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index 5474566d..e47a5252 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -1,6 +1,6 @@
 open import Interp_ast
+open import Interp_utilities
 open import Pervasives
-import Interp
 
 type typ = 
 | Bit
@@ -11,7 +11,7 @@ type instruction =
 |  Instr of string * list (string * typ) * list base_effect
 |  Skipped 
 
-val extract_instructions : string -> string -> defs Interp.tannot -> list instruction
+val extract_instructions : string -> string -> defs tannot -> list instruction
 
 let extract_parm (E_aux e (_,tannot)) =
   match e with
@@ -54,8 +54,8 @@ let rec extract_effects instrs execute =
 end
 
 let extract_instructions decode_name execute_name defs = 
-  let (Just decoder) = Interp.find_function defs (Id_aux (Id decode_name) Unknown) in
-  let (Just executer) = Interp.find_function defs (Id_aux (Id execute_name) Unknown) in
+  let (Just decoder) = find_function defs (Id_aux (Id decode_name) Unknown) in
+  let (Just executer) = find_function defs (Id_aux (Id execute_name) Unknown) in
   let instr_no_effects = extract_from_decode decoder in
   let instructions = extract_effects instr_no_effects executer in
   instructions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 6edebc49..a436d652 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -5,14 +5,9 @@ import List_extra (* For 'nth' and 'head' where we know that they cannot fail *)
 open import String_extra (* for 'show' to convert nat to string) *)
 
 open import Interp_ast
+open import Interp_utilities
 
-type tannot = maybe (t * tag * list nec * effect)
-
-let get_exp_l (E_aux e (l,annot)) = l
-
-val pure : effect
-let pure = Effect_aux(Effect_set []) Unknown
-let unit_t = Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown
+type tannot = Interp_utilities.tannot
 
 val intern_annot : tannot -> tannot
 let intern_annot annot =
@@ -24,38 +19,10 @@ let intern_annot annot =
 
 let val_annot typ = Just(typ,Tag_empty,[],pure)
 
-(* Workaround Lem's inability to scrap my (type classes) boilerplate.
- * Implementing only Eq, and only for literals - hopefully this will
- * be enough, but we should in principle implement ordering for everything in
- * Interp_ast *)
-
-val lit_eq: lit -> lit -> bool
-let lit_eq (L_aux left _) (L_aux right _) =
-   match (left, right) with
-   | (L_unit, L_unit) -> true
-   | (L_zero, L_zero) -> true
-   | (L_one, L_one) -> true
-   | (L_true, L_true) -> true
-   | (L_false, L_false) -> true
-   | (L_num n, L_num m) -> n = m
-   | (L_hex h, L_hex h') -> h = h'
-   | (L_bin b, L_bin b') -> b = b'
-   | (L_undef, L_undef) -> true
-   | (L_string s, L_string s') -> s = s'
-   | (_, _) -> false
-end
-
-instance (Eq lit)
-  let (=) = lit_eq
-  let (<>) n1 n2 = not (lit_eq n1 n2)
-end
-
 (* This is different from OCaml: it will drop elements from the longest list. *)
 let foldr2 f x l l' = List.foldr (Tuple.uncurry f) x (List.zip l l')
 let map2 f l l' = List.map (Tuple.uncurry f) (List.zip l l')
 
-let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end
-
 type reg_form =
  | Reg of id * tannot
  | SubReg of id * reg_form * index_range
@@ -76,12 +43,6 @@ type value =
  | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *)
  | V_track of value * (list reg_form) (* Used when memory system wants to track what register(s) a value came from *)
 
-let rec list_to_string format sep lst = match lst with 
-  | [] -> ""
-  | [last] -> format last
-  | one::rest -> (format one) ^ sep ^ (list_to_string format sep rest)
-end
-
 let rec string_of_value v = match v with
   | V_boxref nat t -> "$#" ^ (show nat) ^ "$"
   | V_lit (L_aux lit _) -> 
@@ -228,36 +189,6 @@ let rec to_aliases (Defs defs) =
       end 
     end
 
-val has_rmem_effect : list base_effect -> bool
-val has_barr_effect : list base_effect -> bool
-val has_wmem_effect : list base_effect -> bool
-let rec has_effect which efcts =
-  match efcts with
-  | [] -> false
-  | (BE_aux e _)::efcts ->
-    match (which,e) with
-    | (BE_rreg,BE_rreg)    -> true 
-    | (BE_wreg,BE_wreg)    -> true 
-    | (BE_rmem,BE_rmem)    -> true 
-    | (BE_wmem,BE_wmem)    -> true 
-    | (BE_barr,BE_barr)    -> true 
-    | (BE_undef,BE_undef)  -> true 
-    | (BE_unspec,BE_unspec) -> true 
-    | (BE_nondet,BE_nondet) -> true 
-    | _ -> has_effect which efcts
-    end 
-  end
-let has_rmem_effect = has_effect BE_rmem
-let has_barr_effect = has_effect BE_barr
-let has_wmem_effect = has_effect BE_wmem
-
-let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
-let get_effects (Typ_aux t _) =
-  match t with
-    | Typ_fn a r (Effect_aux (Effect_set eff) _) -> eff
-    | _ -> []
-  end
-
 val to_data_constructors : defs tannot -> list (id * typ)
 let rec to_data_constructors (Defs defs) =
   match defs with
@@ -760,23 +691,6 @@ let env_to_let mode (LEnv _ env) (E_aux e annot) =
 	           annot
 end
 
-val find_type_def : defs tannot -> id -> maybe (type_def tannot)
-val find_function : defs tannot -> id -> maybe (list (funcl tannot))
-
-let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
-  List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls
-
-let rec find_function (Defs defs) id =
-  match defs with 
-  | [] -> Nothing
-  | def::defs -> 
-    match def with
-    | DEF_fundef f -> match get_funcls id f with
-      | [] -> find_function (Defs defs) id
-      | funcs -> Just funcs end
-    | _ -> find_function (Defs defs) id
-    end end
-
 (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
 val match_pattern : pat tannot -> value -> bool * bool * lenv
 let rec match_pattern (P_aux p _) value_whole =
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 14a286cb..a69ea430 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -27,7 +27,7 @@ end
 		   
 let intern_value v = match v with
   | Bitvector bs inc fst   -> Interp.V_vector fst inc  (to_bits bs)
-  | Bytevector bys inc fst -> Interp.V_vector fst inc 
+  | Bytevector bys -> Interp.V_vector 0 true 
     (to_bits (List.reverse
 		(List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys))))
   | Unknown -> Interp.V_unknown
@@ -43,11 +43,11 @@ end
 let extern_value mode for_mem v = match v with
   | Interp.V_vector fst inc bits ->
     if for_mem 
-    then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, Nothing)
+    then (Bytevector (List.reverse (to_bytes (from_bits bits))), Nothing)
     else (Bitvector (from_bits bits) inc fst, Nothing)
   | Interp.V_track (Interp.V_vector fst inc bits) regs -> 
     if for_mem
-    then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, 
+    then (Bytevector (List.reverse (to_bytes (from_bits bits))), 
           if (mode.Interp.track_values) 
           then (Just (List.map (fun r -> extern_reg r Nothing) regs))
           else Nothing)
@@ -103,7 +103,7 @@ let rec interp_to_value_helper thunk =
       end 
     | Interp.Action (Interp.Exit (E_aux e _)) _ ->
       match e with
-	| E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just Unsupported_instruction_error)
+	| E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just (Unsupported_instruction_error ("",[],[])))
 	| E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just Not_an_instruction_error)
       end 
     | _ -> (Nothing, Just (Internal_error "Memory or register requested in decode"))
@@ -133,6 +133,7 @@ let decode_to_istate top_level value =
 	  Instr (Interp.Thunk_frame
 		   (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
 		   top_level Interp.eenv Interp.emem Interp.Top)
+	        ("",[],[])
 	| (Nothing, Just err) -> err
       end 
     | (Nothing, Just err) -> err
@@ -156,7 +157,7 @@ let rec interp_to_outcome mode thunk =
       match List.lookup i memory_functions with
       | (Just (Just read_k,_,f)) -> 
         let (location, length, tracking) = (f mode value) in
-        Read_mem read_k location length tracking (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
+        Read_mem read_k location tracking length Nothing (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
       | _ -> Error ("Memory " ^ i ^ " function with read kind not found")
       end
     | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
@@ -164,7 +165,7 @@ let rec interp_to_outcome mode thunk =
       | (Just (_,Just write_k,f)) -> 
         let (location, length, tracking) = (f mode loc_val) in
         let (value, val_tracking) = (extern_value mode true write_val) in
-        Write_mem write_k location length tracking value val_tracking (fun b -> next_state) 
+        Write_mem write_k location tracking length Nothing value val_tracking (fun b -> next_state) 
       | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
       end 
     | Interp.Barrier (Id_aux (Id i) _) lval ->
@@ -200,10 +201,10 @@ let rec ie_loop mode i_state =
       (E_read_reg reg)::(ie_loop mode (i_state_fun Unknown))
     | Write_reg reg value i_state->
       (E_write_reg reg value)::(ie_loop mode i_state)
-    | Read_mem read_k loc length tracking i_state_fun ->
-      (E_read_mem read_k loc length tracking)::(ie_loop mode (i_state_fun Unknown))
-    | Write_mem write_k loc length l_track value v_track i_state_fun ->
-      (E_write_mem write_k loc length l_track value v_track)::(ie_loop mode (i_state_fun true))
+    | Read_mem read_k loc tracking length ltracking i_state_fun ->
+      (E_read_mem read_k loc tracking length ltracking)::(ie_loop mode (i_state_fun Unknown))
+    | Write_mem write_k loc track length l_track value v_track i_state_fun ->
+      (E_write_mem write_k loc track length l_track value v_track)::(ie_loop mode (i_state_fun true))
     | Internal _ _ next -> (ie_loop mode next)
      end ;;
   
@@ -219,12 +220,12 @@ let rec rr_ie_loop mode i_state =
     | Write_reg reg value i_state->
       let (events,outcome) = (rr_ie_loop mode i_state) in
       (((E_write_reg reg value)::events), outcome)
-    | Read_mem read_k loc length tracking i_state_fun ->
+    | Read_mem read_k loc tracking  length ltracking i_state_fun ->
       let (events,outcome) = (rr_ie_loop mode (i_state_fun Unknown)) in 
-      (((E_read_mem read_k loc length tracking)::events),outcome)
-    | Write_mem write_k loc length l_track value v_track i_state_fun ->
+      (((E_read_mem read_k loc tracking length ltracking)::events),outcome)
+    | Write_mem write_k loc track length l_track value v_track i_state_fun ->
       let (events,outcome) = (rr_ie_loop mode (i_state_fun true)) in
-      (((E_write_mem write_k loc length l_track value v_track)::events),outcome)
+      (((E_write_mem write_k loc track length l_track value v_track)::events),outcome)
     | Internal _ _ next -> (rr_ie_loop mode next)
      end ;;
 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 2051233d..68e57b47 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -1,4 +1,5 @@
 import Interp
+open import Interp_ast
 open import Pervasives
 open import Num
 
@@ -22,7 +23,7 @@ type value =
   some special registers, with no clear mapping to bits. Should
   we permit Record of (string * Bitvector) values as well?
 *)
-| Bytevector of list word8 * bool * integer (* For memory accesses : see above *)
+| Bytevector of list word8 (* For memory accesses *)
 | Unknown
 (*To add: an abstract value representing an unknown but named memory address?*)
 
@@ -35,10 +36,11 @@ type reg_name =
 | Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *)
 
 type outcome =
-(* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values *)
-| Read_mem of read_kind * value * integer * maybe (list reg_name) *  (value -> instruction_state)
+(* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values,
+   integer is size to read, followed by registers that were used in computing that size *)
+| Read_mem of read_kind * value * maybe (list reg_name) * integer * maybe (list reg_name) *  (value -> instruction_state)
 (* Request to write memory, first value and dependent registers is location, second is the value to write *)
-| Write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state)
+| Write_mem of write_kind * value * maybe (list reg_name) * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state)
 (* Request a memory barrier *)
 | Barrier of barrier_kind * instruction_state
 (* Request to read register, will track dependency when mode.track_values *)
@@ -49,16 +51,19 @@ type outcome =
 | Nondet_choice of list instruction_state * instruction_state
 (* Stop for incremental stepping, function can be used to display function call data *)
 | Internal of maybe string * maybe (unit -> string) * instruction_state
+(* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally provide a handler *)
+| Escape of maybe instruction_state
 | Done
 | Error of string
 
 type event = 
-| E_read_mem of read_kind * value * integer * maybe (list reg_name) 
-| E_write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name)
+| E_read_mem of read_kind * value * maybe (list reg_name) * integer * maybe (list reg_name)
+| E_write_mem of write_kind * value * maybe (list reg_name) * integer * maybe (list reg_name) * value * maybe (list reg_name)
 | E_barrier of barrier_kind
 | 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 there be a representation for escape down here?*)
 (*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 *)
@@ -66,9 +71,20 @@ val build_context : Interp_ast.defs Interp.tannot -> context (*defs should come
 val initial_instruction_state : context -> string -> list value -> instruction_state 
   (* string is a function name, list of value are the parameters to that function *)
 
+(*Type representint the constructor parameters in instruction_form, other is a type not representable externally*)
+type instr_parm_typ = 
+  | Bit (*A single bit, represented as a one element Bitvector as a value*)
+  | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
+  | Bvector of maybe integer (* A bitvector type, with length when statically known *)
+
+(*A representation of the AST node for each instruction in the spec, with concrete values from this call, and the potential static effects from the funcl clause for this instruction 
+Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
+*)
+type instruction_form = (string * list (string * instr_parm_typ * value) * list base_effect)
+
 type i_state_or_error =
-  | Instr of instruction_state
-  | Unsupported_instruction_error
+  | Instr of instruction_state * instruction_form
+  | Unsupported_instruction_error of instruction_form
   | Not_an_instruction_error
   | Internal_error of string
 
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index a9c22b6c..a54dc6e1 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -49,7 +49,7 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
 
 let val_to_string v = match v with
   | Bitvector(bools, _, _) -> "0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))
-  | Bytevector(words, _, _)->
+  | Bytevector words->
     "0x" ^ (String.concat ""
 	    (List.map (function 
 	      | 10 -> "A"
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index fbb06eed..60258504 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -50,7 +50,7 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
 let val_to_string v = match v with
   | Bitvector(bools, inc, fst)-> let l = List.length bools in
     (string_of_int l) ^ " bits -- 0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))
-  | Bytevector(words, inc, fst)->
+  | Bytevector words ->
     let l = List.length words in
     (string_of_int l) ^ " bytes --" ^
       (String.concat ""
@@ -191,7 +191,7 @@ module Mem = struct
     add key valu m
 
   let to_string loc v =
-    sprintf "[%s] -> %x" (val_to_string (Bytevector(loc, true, zero_big_int))) v
+    sprintf "[%s] -> %x" (val_to_string (Bytevector loc)) v
 end ;;
 
 let rec slice bitvector (start,stop) = 
@@ -202,8 +202,8 @@ let rec slice bitvector (start,stop) =
                  inc,
                  (if inc then zero_big_int else (add_big_int (sub_big_int stop start) unit_big_int)))
                 
-    | Bytevector(bytes, inc, fst) -> 
-      Bytevector((Interp.from_n_to_n start stop bytes),inc,fst) (*This is wrong, need to explode and re-encode, but maybe never happens?*)
+    | Bytevector bytes -> 
+      Bytevector((Interp.from_n_to_n start stop bytes)) (*This is wrong, need to explode and re-encode, but maybe never happens?*)
     | Unknown0 -> Unknown0
 ;;
 
@@ -245,12 +245,12 @@ let fupdate_slice original e (start,stop) =
                                     (if inc then (sub_big_int start fst) else (sub_big_int fst start))
                                     (if inc then (sub_big_int stop fst) else (sub_big_int fst stop)) bs bools), inc, fst)
       | _ -> Unknown0)
-    | Bytevector(bytes,inc,fst) -> (*Can this happen?*)
+    | Bytevector bytes -> (*Can this happen?*)
       (match e with
-      | Bytevector([byte],_,_) -> 
-        Bytevector((list_update zero_big_int start stop byte bytes),inc,fst)
-      | Bytevector(bs,_,_) ->
-        Bytevector((list_update_list zero_big_int start stop bs bytes),inc,fst)
+      | Bytevector [byte] -> 
+        Bytevector (list_update zero_big_int start stop byte bytes)
+      | Bytevector bs ->
+        Bytevector (list_update_list zero_big_int start stop bs bytes)
       | _ -> Unknown0)
     | Unknown0 -> Unknown0
 ;;
@@ -272,10 +272,10 @@ let rec format_events = function
     "     Failed with message : " ^ s ^ "\n"
   | (E_error s)::events ->
     "     Failed with message : " ^ s ^ " but continued on erroneously\n"
-  | (E_read_mem(read_kind, location, length, dep))::events ->
+  | (E_read_mem(read_kind, location,depl, length, dep))::events ->
     "     Read_mem at " ^ (val_to_string location) ^ " for " ^ (string_of_big_int length) ^ " bytes \n" ^
     (format_events events)
-  | (E_write_mem(write_kind,location, length, dep, value, vdep))::events ->
+  | (E_write_mem(write_kind,location,depl, length, dep, value, vdep))::events ->
     "     Write_mem at " ^ (val_to_string location) ^ " writing " ^ (val_to_string value) ^ " across " ^ (string_of_big_int length) ^ " bytes\n" ^
     (format_events events)
   | ((E_barrier b_kind)::events) ->
@@ -306,13 +306,13 @@ let rec perform_action ((reg, mem) as env) = function
    let old_val = Reg.find id reg in
    let new_val = fupdate_slice old_val value (combine_slices range mini_range) in
    (None,(Reg.add id new_val reg,mem))
- | Read_mem0(_,Bytevector(location,_,_), length, _,_) ->
+ | Read_mem0(_,(Bytevector location),_, length, _,_) ->
    let rec reading location length = 
      if eq_big_int length zero_big_int 
      then []
      else (Mem.find location mem)::(reading (increment location) (sub_big_int length unit_big_int)) in
-   (Some (Bytevector((List.rev (reading location length)), true, zero_big_int)), env) (*TODO: how to get order back here? *)
- | Write_mem0(_,(Bytevector(location,_,_)), length, _, (Bytevector(bytes,_,_)),_,_) ->
+   (Some (Bytevector((List.rev (reading location length)))), env)
+ | Write_mem0(_,(Bytevector location),_, length, _, (Bytevector bytes),_,_) ->
    let rec writing location length bytes mem = 
      if eq_big_int length zero_big_int
      then mem
@@ -440,7 +440,7 @@ let run
 	| Write_reg0(reg,value,next) ->
 	  show "write_reg" (reg_name_to_string reg) left (val_to_string value);
 	  (step next, env', next)
-	| Read_mem0(kind, location, length, dependencies, next_thunk) ->
+	| Read_mem0(kind, location, ldeps, length, dependencies, next_thunk) ->
 	  (match return with
 	    | Some(value) -> 
 	      show "read_mem" (val_to_string location) right (val_to_string value);
@@ -451,7 +451,7 @@ let run
 	      let next = next_thunk value in
 	      (step next, env', next)
 	    | None -> assert false)
-	| Write_mem0(kind,location, length, dependencies, value, val_dependencies, next_thunk) ->
+	| Write_mem0(kind,location, ldeps, length, dependencies, value, val_dependencies, next_thunk) ->
 	  show "write_mem" (val_to_string location) left (val_to_string value);
           (match (dependencies,val_dependencies) with
           | (None,None) -> ();