kathy,peter: making decode integration with ppcmem2 typecheck

4 files changed, 29 insertions, 29 deletions

diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index e47a5252..d4a52890 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -7,11 +7,11 @@ type typ =
 | Bitvector of maybe integer
 | Other
 
-type instruction = 
+type instruction_form = 
 |  Instr of string * list (string * typ) * list base_effect
 |  Skipped 
 
-val extract_instructions : string -> string -> defs tannot -> list instruction
+val extract_instructions : string -> string -> defs tannot -> list instruction_form
 
 let extract_parm (E_aux e (_,tannot)) =
   match e with
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 292552f4..27e5e17c 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -157,15 +157,15 @@ 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 tracking length Nothing (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
+        Read_mem read_k location length tracking (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 ->
       match List.lookup i memory_functions with
       | (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 tracking length Nothing value val_tracking (fun b -> next_state) 
+        let (value, v_tracking) = (extern_value mode true write_val) in
+        Write_mem write_k location length tracking value v_tracking (fun b -> next_state) 
       | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
       end 
     | Interp.Barrier (Id_aux (Id i) _) lval ->
@@ -201,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 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))
+    | 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 tracking value v_tracking i_state_fun ->
+      (E_write_mem write_k loc length tracking value v_tracking)::(ie_loop mode (i_state_fun true))
     | Internal _ _ next -> (ie_loop mode next)
      end ;;
   
@@ -220,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 tracking  length ltracking i_state_fun ->
+    | Read_mem read_k loc length tracking i_state_fun ->
       let (events,outcome) = (rr_ie_loop mode (i_state_fun Unknown)) in 
-      (((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 ->
+      (((E_read_mem read_k loc length tracking)::events),outcome)
+    | Write_mem write_k loc length tracking value v_tracking i_state_fun ->
       let (events,outcome) = (rr_ie_loop mode (i_state_fun true)) in
-      (((E_write_mem write_k loc track length l_track value v_track)::events),outcome)
+      (((E_write_mem write_k loc length tracking value v_tracking)::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 ec863a41..40c34480 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -38,9 +38,9 @@ type reg_name =
 type outcome =
 (* 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)
+| Read_mem of read_kind * value * 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 * maybe (list reg_name) * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state)
+| Write_mem of write_kind * value * 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 *)
@@ -57,8 +57,8 @@ type outcome =
 | Error of string
 
 type event = 
-| 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_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_barrier of barrier_kind
 | E_read_reg of reg_name
 | E_write_reg of reg_name * value
@@ -71,7 +71,7 @@ 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 representint the constructor parameters in instruction, 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 *)
@@ -80,15 +80,15 @@ type instr_parm_typ =
 (*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 instruction = (string * list (string * instr_parm_typ * value) * list base_effect)
 
 type decode_error = 
-  | Unsupported_instruction_error of instruction_form
+  | Unsupported_instruction_error of instruction
   | Not_an_instruction_error of value
   | Internal_error of string
 
 type i_state_or_error =
-  | Instr of instruction_form * instruction_state
+  | Instr of instruction * instruction_state
   | Decode_error of decode_error
 
 
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 60258504..f8c05085 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -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,depl, length, dep))::events ->
+  | (E_read_mem(read_kind, location, length, tracking))::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,depl, length, dep, value, vdep))::events ->
+  | (E_write_mem(write_kind,location, length, tracking, value, v_tracking))::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)))), env)
- | Write_mem0(_,(Bytevector location),_, length, _, (Bytevector bytes),_,_) ->
+ | 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,20 +440,20 @@ 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, ldeps, length, dependencies, next_thunk) ->
+	| Read_mem0(kind, location, length, tracking, next_thunk) ->
 	  (match return with
 	    | Some(value) -> 
 	      show "read_mem" (val_to_string location) right (val_to_string value);
-              (match dependencies with
+              (match tracking with
               | None -> ()
               | Some(deps) ->
                 show "read_mem address depended on" (dependencies_to_string deps) "" "");
 	      let next = next_thunk value in
 	      (step next, env', next)
 	    | None -> assert false)
-	| Write_mem0(kind,location, ldeps, length, dependencies, value, val_dependencies, next_thunk) ->
+	| Write_mem0(kind,location, length, tracking, value, v_tracking, next_thunk) ->
 	  show "write_mem" (val_to_string location) left (val_to_string value);
-          (match (dependencies,val_dependencies) with
+          (match (tracking,v_tracking) with
           | (None,None) -> ();
           | (Some(deps),None) ->
             show "write_mem address depended on" (dependencies_to_string deps) "" "";