update instruction/istate decoding.

Use register size.
Printing again doesn't compile

2 files changed, 76 insertions, 35 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 65501b32..df47a75e 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -18,13 +18,23 @@ let build_context defs = match Interp.to_top_env defs with (_,context) -> contex
 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_bit = function 
+let to_ibit = function 
   | Bitl_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) 
   | Bitl_one ->  (Interp.V_lit (L_aux L_one Interp_ast.Unknown))
   | Bitl_undef -> (Interp.V_lit (L_aux L_undef Interp_ast.Unknown))
   | Bitl_unknown -> Interp.V_unknown 
 end
 
+let to_bit = function 
+  | Bitl_zero -> Bitc_zero 
+  | Bitl_one ->  Bitc_one
+end
+
+let to_lbit = function
+  | Bitc_zero -> Bitl_zero
+  | Bitc_one -> Bitl_one
+end
+
 let to_bool = function 
   | Bitl_zero -> false
   | Bitl_one ->  true
@@ -39,7 +49,7 @@ let is_bool = function
   | Bitl_unknown -> false
 end
 
-let to_bits l = List.map to_bit l
+let to_ibits l = List.map to_ibit l
 let from_bits l = List.map 
 		     (fun b -> match b with
                        | Interp.V_lit (L_aux L_zero _) -> Bitl_zero
@@ -59,14 +69,24 @@ let bits_to_byte b =
   if ((List.length b) = 8) && (all_known b)
   then natFromInteger (integerFromBoolList (false,(List.reverse (List.map to_bool b))))
   else Assert_extra.failwith "bits_to_byte given a non-8 list or one containing ? and u"
+
+let memval_to_regval v start dir = 
+  <| rv_bits=(List.concatMap (fun (Byte_lifted(bits)) -> bits) v);
+     rv_start=start; rv_dir = dir |>
+
+let opcode_to_regval (Opcode v) start dir =
+  (memval_to_regval (List.map (fun (Byte(bits)) -> Byte_lifted (List.map to_lbit bits)) v) start dir)
+
+let regval_to_ifield v = List.map to_bit v.rv_bits
+
 		   
 let intern_reg_value v = match v with
-  | <| rv_bits=[b] |> -> to_bit b
-  | _ -> Interp.V_vector (integerFromInt v.rv_start) (v.rv_dir = D_increasing) (to_bits v.rv_bits)
+  | <| rv_bits=[b] |> -> to_ibit b
+  | _ -> Interp.V_vector (integerFromInt v.rv_start) (v.rv_dir = D_increasing) (to_ibits v.rv_bits)
 end
 
 let intern_mem_value v = 
-  Interp.V_vector 0 true (*get a default here*) (List.concatMap (fun (Byte_lifted bits) -> to_bits bits) v)
+  Interp.V_vector 0 true (*get a default here*) (List.concatMap (fun (Byte_lifted bits) -> to_ibits bits) v)
 
 (*let byte_list_of_integer size num = 
   if (num < 0)
@@ -346,11 +366,12 @@ let migrate_typ = function
   | Instruction_extractor.IOther -> Other
 end
 
-let decode_to_istate top_level value = 
+let decode_to_istate top_level orig_value = 
+  let value = opcode_to_regval orig_value 0 D_increasing in
   let mode = make_mode true false in
   let (arg,_) = Interp.to_exp mode Interp.eenv (intern_reg_value value) in
   let (Interp.Env _ instructions _ _ _ _ _) = top_level in
-  let (instr_decoded,error) = interp_to_value_helper value ("",[],[])
+  let (instr_decoded,error) = interp_to_value_helper orig_value ("",[],[])
     (fun _ -> Interp.resume 
       (make_mode true false) 
       (Interp.Thunk_frame 
@@ -364,12 +385,13 @@ let decode_to_istate top_level value =
 	    | Just(Instruction_extractor.Instr_form name parms effects) -> 
 	      match (parm,parms) with
 		| (Interp.V_lit (L_aux L_unit _),[]) -> (name, [], effects)
-		| (value,[(p_name,ie_typ)]) -> (name, [(p_name,(migrate_typ ie_typ),(extern_reg_value Nothing value))], effects)
+		| (value,[(p_name,ie_typ)]) -> (name, [(p_name,(migrate_typ ie_typ),
+							(regval_to_ifield (extern_reg_value Nothing value)))], effects)
 		| (Interp.V_tuple vals,parms) -> 
-		  (name, (Interp.map2 (fun value (p_name,ie_typ) -> (p_name,(migrate_typ ie_typ),(extern_reg_value Nothing value))) vals parms), effects)
+		  (name, (Interp.map2 (fun value (p_name,ie_typ) -> (p_name,(migrate_typ ie_typ),(regval_to_ifield (extern_reg_value Nothing value)))) vals parms), effects)
           end end end in 
       let (arg,_) = Interp.to_exp mode Interp.eenv instr in
-      let (instr_decoded,error) = interp_to_value_helper value instr_external
+      let (instr_decoded,error) = interp_to_value_helper orig_value instr_external
 	(fun _ -> Interp.resume 
 	 (make_mode true false) 
 	 (Interp.Thunk_frame 
@@ -398,7 +420,9 @@ let decode_to_instruction top_level value =
 
 let instruction_to_istate top_level ((name, parms, _) as instr) = 
   let mode = make_mode true false in
-  let get_value (name,typ,v) = let (e,_) = Interp.to_exp mode Interp.eenv (intern_reg_value v) in e in
+  let get_value (name,typ,v) = 
+    let (e,_) = 
+      Interp.to_exp mode Interp.eenv (intern_reg_value (opcode_to_regval v 0 D_increasing)) in e in
 (*  (Instr instr*)
     (Interp.Thunk_frame
        (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) 
@@ -495,25 +519,32 @@ let rec find_reg_name reg = function
       | _ -> find_reg_name reg registers
 end end
 
+let reg_size = function
+  | Reg i size -> size
+  | Reg_slice i (p1,p2) -> if p1 < p2 then (p2-p1 +1) else (p1-p2 +1)
+  | Reg_field i f (p1,p2) -> if p1 < p2 then (p2-p1 +1) else (p1-p2 +1)
+  | Reg_f_slice i f _ (p1,p2) -> if p1 < p2 then p2-p1 +1 else p1-p2+1
+end
+
 let rec ie_loop mode register_values i_state = 
   let unknown_reg size =  
-    <| rv_bits = (List.replicate size Bitl_unknown); rv_start = 0; rv_dir = D_increasing |> in
-  let unknown_mem size = List.replicate size (Byte_lifted (List.replicate 8 Bitl_unknown)) in
+    <| rv_bits = (List.replicate (natFromInteger size) Bitl_unknown); rv_start = 0; rv_dir = D_increasing |> in
+  let unknown_mem size = List.replicate (natFromInteger size) (Byte_lifted (List.replicate 8 Bitl_unknown)) in
   match (interp mode i_state) with
     | Done -> []
     | Error msg -> [E_error msg]
     | Read_reg reg i_state_fun -> 
       let v =  match register_values with
-	| Nothing -> unknown_reg 64
+	| Nothing -> unknown_reg (reg_size reg)
 	| Just(registers) -> match find_reg_name reg registers with
-	    | Nothing -> unknown_reg 64 (*Wrong in some cases, need to look in reg and store full length of reg*)
+	    | Nothing -> unknown_reg (reg_size reg)
 	    | Just v -> v end end in
       (E_read_reg reg)::(ie_loop mode register_values (i_state_fun v))
     | Write_reg reg value i_state->
       (E_write_reg reg value)::(ie_loop mode register_values i_state)
     | Read_mem read_k loc length tracking i_state_fun ->
       (E_read_mem read_k loc length tracking)::
-	(ie_loop mode register_values (i_state_fun (unknown_mem (natFromInteger length))))
+	(ie_loop mode register_values (i_state_fun (unknown_mem length)))
     | 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 register_values (i_state_fun true))
     | Barrier barrier_k i_state ->
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index e84cb358..1e48e07b 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -22,6 +22,15 @@ open import Interp_ast
 open import Pervasives
 open import Num
 
+(* maybe isn't a member of type Ord - this should be in the Lem standard library*)
+instance forall 'a. Ord 'a => (Ord (maybe 'a))
+  let compare = maybeCompare compare
+  let (<)  r1 r2 = (maybeCompare compare r1 r2) = LT
+  let (<=) r1 r2 = (maybeCompare compare r1 r2) <> GT
+  let (>)  r1 r2 = (maybeCompare compare r1 r2) = GT
+  let (>=) r1 r2 = (maybeCompare compare r1 r2) <> LT
+end
+
 type word8 = nat (* bounded at a byte, for when lem supports it*)
 
 (* Abstract types, to be accessed only through this interface *)
@@ -188,9 +197,21 @@ type address = Address of list byte (* of length 8 *)
 
 type opcode = Opcode of list byte (* of length 4 *)
 
+instance (Ord register_value)
+  let compare = defaultCompare
+  let (<) = defaultLess
+  let (<=) = defaultLessEq
+  let (>) = defaultGreater
+  let (>=) = defaultGreaterEq
+end
 
-
-
+instance (Ord address_lifted)
+  let compare = defaultCompare
+  let (<) = defaultLess
+  let (<=) = defaultLessEq
+  let (>) = defaultGreater
+  let (>=) = defaultGreaterEq
+end
 
 type outcome =
 (* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values,
@@ -248,16 +269,6 @@ instance (Ord barrier_kind)
   let (>=) = defaultGreaterEq
 end
 
-(* maybe isn't a member of type Ord - this should be in the Lem standard library*)
-instance forall 'a. Ord 'a => (Ord (maybe 'a))
-  let compare = maybeCompare compare
-  let (<)  r1 r2 = (maybeCompare compare r1 r2) = LT
-  let (<=) r1 r2 = (maybeCompare compare r1 r2) <> GT
-  let (>)  r1 r2 = (maybeCompare compare r1 r2) = GT
-  let (>=) r1 r2 = (maybeCompare compare r1 r2) <> LT
-end
-
-
 (*let eventCompare e1 e2 = 
   match (e1,e2) with
   | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) -> compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
@@ -272,16 +283,15 @@ end
   | (E_read_reg _, _) -> LT
   | (E_write_reg _ _, _) -> LT
   | _ -> GT
-  end
+  end*)
+
 
-*)
 
 instance (SetType event)
   let setElemCompare = defaultCompare
 end
 
 
-
 (* 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 register_value -> instruction_state 
@@ -308,7 +318,7 @@ end
 (*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 = (string * list (string * instr_parm_typ * register_value) * list base_effect)
+type instruction = (string * list (string * instr_parm_typ * instruction_field_value) * list base_effect)
 
 let instructionEqual i1 i2 = match (i1,i2) with
   | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2
@@ -318,7 +328,7 @@ type v_kind = Bitv | Bytev
 
 type decode_error = 
   | Unsupported_instruction_error of instruction
-  | Not_an_instruction_error of register_value
+  | Not_an_instruction_error of opcode
   | Internal_error of string
 
 type instruction_or_decode_error =
@@ -332,11 +342,11 @@ type i_state_or_error =
 
 
 (** PS:I agree. propose to remove this: Function to decode an instruction and build the state to run it*)
-val decode_to_istate : context -> register_value -> i_state_or_error
+val decode_to_istate : context -> opcode -> i_state_or_error
 
 (** propose to add this, and then use instruction_to_istate on the result: Function to decode an instruction and build the state to run it*)
 (** PS made a placeholder in interp_inter_imp.lem, but it just uses decode_to_istate and throws away the istate; surely it's easy to just do what's necessary to get the instruction.   This sort-of works, but it crashes on ioid 10 after 167 steps - maybe instruction_to_istate (which I wasn't using directly before) isn't quite right? *)
-val decode_to_instruction : context -> register_value -> instruction_or_decode_error
+val decode_to_instruction : context -> opcode -> instruction_or_decode_error
 
 (*Function to generate the state to run from an instruction form; is always an Instr*)
 val instruction_to_istate : context -> instruction -> i_state_or_error