fix deep_shallow_convert, stop using interp_interface.instruction for most things, SF and CP bugfixing

5 files changed, 62 insertions, 36 deletions

diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem
index 86365b78..5a0dd99e 100644
--- a/src/gen_lib/deep_shallow_convert.lem
+++ b/src/gen_lib/deep_shallow_convert.lem
@@ -15,10 +15,10 @@ let toInterValueBool = function
   | false -> Interp_ast.V_lit (L_aux (L_zero) Unknown)
 end
 let rec fromInterpValueBool v = match v with
-  | Interp_ast.V_lit (L_aux (L_true) _)  -> true
-  | Interp_ast.V_lit (L_aux (L_false) _) -> false
   | Interp_ast.V_lit (L_aux (L_one) _)  -> true
+  | Interp_ast.V_lit (L_aux (L_true) _)  ->  true
   | Interp_ast.V_lit (L_aux (L_zero) _) -> false
+  | Interp_ast.V_lit (L_aux (L_false) _) -> false
   | Interp_ast.V_tuple [v] -> fromInterpValueBool v
   | v -> failwith ("fromInterpValue bool: unexpected value. " ^
                      Interp.debug_print_value v)
@@ -78,7 +78,7 @@ let rec fromInterpValueBitU v = match v with
   | Interp_ast.V_lit (L_aux (L_zero) _)  -> B0
   | Interp_ast.V_lit (L_aux (L_undef) _) -> BU
   | Interp_ast.V_lit (L_aux (L_true) _)   -> B1
-  | Interp_ast.V_lit (L_aux (L_false) _)  -> B0
+  | Interp_ast.V_lit (L_aux (L_false) _)  -> B0 
   | Interp_ast.V_tuple [v] -> fromInterpValueBitU v
   | v -> failwith ("fromInterpValue bitU: unexpected value. " ^
                      Interp.debug_print_value v)
@@ -506,18 +506,41 @@ instance (ToFromInterpValue barrier_kind)
 end
 
 
+let trans_kindToInterpValue = function
+  | Transaction_start -> V_ctor (Id_aux (Id "Transaction_start") Unknown) (T_id "trans_kind") (C_Enum 0) (toInterpValue ())
+  | Transaction_commit -> V_ctor (Id_aux (Id "Transaction_commit") Unknown) (T_id "trans_kind") (C_Enum 1) (toInterpValue ())
+  | Transaction_abort -> V_ctor (Id_aux (Id "Transaction_abort") Unknown) (T_id "trans_kind") (C_Enum 2) (toInterpValue ())
+  end
+let rec trans_kindFromInterpValue v = match v with
+  | V_ctor (Id_aux (Id "Transaction_start") _) _ _ v -> Transaction_start
+  | V_ctor (Id_aux (Id "Transaction_commit") _) _ _ v -> Transaction_commit
+  | V_ctor (Id_aux (Id "Transaction_abort") _) _ _ v -> Transaction_abort
+  | V_tuple [v] -> trans_kindFromInterpValue v
+  | v -> failwith ("fromInterpValue trans_kind: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance (ToFromInterpValue trans_kind)
+  let toInterpValue = trans_kindToInterpValue
+  let fromInterpValue = trans_kindFromInterpValue
+end
+
+
 let instruction_kindToInterpValue = function
   | IK_barrier v -> V_ctor (Id_aux (Id "IK_barrier") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
   | IK_mem_read v -> V_ctor (Id_aux (Id "IK_mem_read") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
   | IK_mem_write v -> V_ctor (Id_aux (Id "IK_mem_write") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
+  | IK_mem_rmw v -> V_ctor (Id_aux (Id "IK_mem_rmw") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
   | IK_cond_branch -> V_ctor (Id_aux (Id "IK_cond_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
+  | IK_trans v -> V_ctor (Id_aux (Id "IK_trans") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
   | IK_simple -> V_ctor (Id_aux (Id "IK_simple") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
   end
 let rec instruction_kindFromInterpValue v = match v with
   | V_ctor (Id_aux (Id "IK_barrier") _) _ _ v -> IK_barrier (fromInterpValue v)
   | V_ctor (Id_aux (Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v)
   | V_ctor (Id_aux (Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v)
+  | V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ v -> IK_mem_rmw (fromInterpValue v)
   | V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ v -> IK_cond_branch
+  | V_ctor (Id_aux (Id "IK_trans") _) _ _ v -> IK_trans (fromInterpValue v)
   | V_ctor (Id_aux (Id "IK_simple") _) _ _ v -> IK_simple
   | V_tuple [v] -> instruction_kindFromInterpValue v
   | v -> failwith ("fromInterpValue instruction_kind: unexpected value. " ^
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 58874fa6..f00458b7 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1424,8 +1424,8 @@ let rec match_pattern t_level (P_aux p (_, annot)) value_whole =
    | V_ctor (Id_aux cid _) t ckind v ->
      if id = cid
      then (match (pats,detaint v) with
-     | ([],(V_lit (L_aux L_unit _))) -> (true,true,eenv)
-     | ([P_aux (P_lit (L_aux L_unit _)) _],(V_lit (L_aux L_unit _))) -> (true,true,eenv)
+     | ([],(V_lit (L_aux L_unit _))) -> (true,false,eenv)
+     | ([P_aux (P_lit (L_aux L_unit _)) _],(V_lit (L_aux L_unit _))) -> (true,false,eenv)
      | ([p],_) -> match_pattern t_level p v
      | _ -> (false,false,eenv) end)
      else (false,false,eenv)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 6ee13d60..52acae1e 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -469,7 +469,7 @@ let translate_address top_level end_flag thunk_name registers address =
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (address_error,events) =
-    interp_to_value_helper debug (Just (Opcode bytes)) Ivh_translate val_str ("",[]) internal_direction
+    interp_to_value_helper debug (Just (Opcode bytes)) Ivh_translate val_str (V_list []) internal_direction
       registers [] false
       (fun _ -> Interp.resume 
         int_mode 
@@ -504,17 +504,16 @@ let intern_instruction direction (name,parms) =
   Interp_ast.V_ctor (Interp.id_of_string name) (T_id "ast") Interp_ast.C_Union
     (Interp_ast.V_tuple (List.map (value_of_instruction_param direction) parms))
 
-let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction =
+let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers (instruction : Interp_ast.value) =
   let (Context top_env direction _ _ _ _ _ _ _ _ _) = top_level in
   let (Interp.Env _ _ _ _ _ _ _ _ debug) = top_env in
   let mode = make_mode true false debug in
   let int_mode = mode.internal_mode in
-  let intern_val = intern_instruction direction instruction in
-  let val_str = Interp.string_of_value intern_val in
-  let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
+  let val_str = Interp.string_of_value instruction in
+  let (arg,_) = Interp.to_exp int_mode Interp.eenv instruction in
   let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (analysis_or_error,events) =
-    interp_to_value_helper debug Nothing Ivh_analysis val_str ("",[]) internal_direction
+    interp_to_value_helper debug Nothing Ivh_analysis val_str (V_list []) internal_direction
       registers [] false
       (fun _ -> Interp.resume 
         int_mode 
@@ -680,7 +679,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro
   let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (instr_decoded_error,events) =
-    interp_to_value_helper debug (Just value) Ivh_decode val_str ("",[]) internal_direction registers [] false
+    interp_to_value_helper debug (Just value) Ivh_decode val_str (V_list []) internal_direction registers [] false
       (fun _ -> Interp.resume 
           mode 
           (Interp.Thunk_frame 
@@ -688,9 +687,9 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro
              top_env Interp.eenv (Interp.emem "decode top level") Interp.Top) Nothing) in
   match (instr_decoded_error) with
     | Ivh_value instr -> 
-      let instr_external = interp_value_to_instr_external top_level instr in
+       (* let instr_external = interp_value_to_instr_external top_level instr in*) 
       let (instr_decoded_error,events) =
-        interp_to_value_helper debug (Just value) Ivh_unsupported val_str instr_external internal_direction
+        interp_to_value_helper debug (Just value) Ivh_unsupported val_str instr (*instr_external*) internal_direction
           registers [] false
         (fun _ -> Interp.resume 
             mode
@@ -699,7 +698,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro
                   (Interp_ast.Unknown, Nothing)) 
                top_env Interp.eenv (Interp.emem "decode second top level") Interp.Top) Nothing) in
       match (instr_decoded_error) with
-        | Ivh_value _ -> IDE_instr instr_external instr
+      | Ivh_value _ -> IDE_instr instr (*instr_external*)
         | Ivh_value_after_exn v ->
           Assert_extra.failwith "supported_instructions called exit, so support will be needed for that now"
         | Ivh_error err -> IDE_decode_error err
@@ -713,9 +712,9 @@ end
 let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_error = 
   let (Context top_env _ _ _ _ _ _ _ _ _ _) = top_level in
   match decode_to_instruction top_level registers value with
-  | IDE_instr instr instrv ->
+  | IDE_instr instr ->
      let mode = make_interpreter_mode true false in
-     let (arg,_) = Interp.to_exp mode Interp.eenv instrv in
+     let (arg,_) = Interp.to_exp mode Interp.eenv instr in
      Instr instr
            (IState (Interp.Thunk_frame
                       (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
@@ -750,11 +749,11 @@ let instr_external_to_interp_value top_level instr =
   Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id name) Interp_ast.Unknown) 
                 (T_id "ast") Interp_ast.C_Union parmsV
 
-val instruction_to_istate : context -> instruction -> instruction_state 
-let instruction_to_istate (top_level:context) (((name, parms) as instr):instruction) : instruction_state  = 
+val instruction_to_istate : context -> Interp_ast.value -> instruction_state 
+let instruction_to_istate (top_level:context) (instr:Interp_ast.value) : instruction_state  = 
   let mode = make_interpreter_mode true false in
   let (Context top_env _ _ _ _ _ _ _ _ _ _) = top_level in
-  let ast_node = fst (Interp.to_exp mode Interp.eenv (instr_external_to_interp_value top_level instr)) in
+  let ast_node = fst (Interp.to_exp mode Interp.eenv instr) in
   (IState
      (Interp.Thunk_frame
         (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [ast_node])
@@ -1092,7 +1091,7 @@ and state_to_outcome_s pp_instruction_state mode state =
          (fun env -> interp_exhaustive mode.internal_mode.Interp.debug (Just env) state))
   )
 
-val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit
+val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> Interp_ast.value -> Sail_impl_base.outcome_s unit
 let initial_outcome_s_of_instruction pp_instruction_state context mode instruction =
   let state = instruction_to_istate context instruction in
   state_to_outcome_s pp_instruction_state mode state
@@ -1222,14 +1221,15 @@ let nia_address_of_event nia_reg (event: event) : maybe (maybe address) =
   | _ -> Nothing
   end
 
-let nias_of_instruction 
+let nias_of_instruction
+      top_level
       thread_ism
     (nia_address: list (maybe address)) (* Nothing for unknown/undef*)
     (regs_in:     list reg_name)
-    (instruction: instruction)
+    (instruction: Interp_ast.value)
     : list nia
   =
-  let (instruction_name, instruction_fields) = instruction in
+  let (instruction_name, instruction_fields) = interp_value_to_instr_external top_level instruction in
 
   let unknown_nia_address = List.elem Nothing nia_address in
 
@@ -1390,7 +1390,9 @@ let nias_of_instruction
     | (s1, s2) -> failwith ("unexpected (thread_ism, instruction_name): (" ^ s1 ^ ", " ^ s2 ^ ")")
     end
 
+
 let interp_instruction_analysis 
+      top_level
       (interp_exhaustive : ((list (reg_name * register_value)) -> list event))
       instruction nia_reg ism environment = 
     
@@ -1403,7 +1405,7 @@ let interp_instruction_analysis
 
     let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in
 
-    let nias = nias_of_instruction ism nia_address regs_in instruction in
+    let nias = nias_of_instruction top_level ism nia_address regs_in instruction in
 
     let dia = DIA_none in (* FIX THIS! *)
 
@@ -1478,29 +1480,28 @@ val print_and_fail_of_inequal : forall 'a. Show 'a =>
                                 (instruction -> string) ->
                                 (string * 'a) -> (string * 'a) -> unit
 let print_and_fail_if_inequal 
-      (print_endline,pp_instruction,instruction)
+      (print_endline,instruction)
       (name1,xs1) (name2,xs2) =
   if xs1 = xs2 then ()
   else 
     let () = print_endline (name1^": "^show xs1) in
     let () = print_endline (name2^": "^show xs2) in
-    failwith (name1^" and "^ name2^" inequal for instruction " ^ pp_instruction instruction)
+    failwith (name1^" and "^ name2^" inequal for instruction: \n" ^ Interp.string_of_value instruction)
 
 let interp_compare_analyses 
       print_endline
-      pp_instruction
       (non_pseudo_registers : set reg_name -> set reg_name)
       context
       endianness
       interp_exhaustive
-      instruction
+      (instruction : Interp_ast.value)
       nia_reg
       ism
       environment
       analysis_function
       reg_info = 
   let (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1) = 
-    interp_instruction_analysis interp_exhaustive instruction nia_reg ism 
+    interp_instruction_analysis context interp_exhaustive instruction nia_reg ism 
                                 environment in
   let (regs_in1S,regs_out1S,regs_feeding_address1S,nias1S) =
     (Set.fromList regs_in1,
@@ -1525,7 +1526,7 @@ let interp_compare_analyses
      non_pseudo_registers regs_out2S,
      non_pseudo_registers regs_feeding_address2S) in
 
-  let aux = (print_endline,pp_instruction,instruction) in
+  let aux = (print_endline,instruction) in
   let () = (print_and_fail_if_inequal aux)
              ("regs_in exhaustive",regs_in1S) 
              ("regs_in hand",regs_in2S) in
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index dcc9f537..07d9e2b3 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -104,6 +104,10 @@ end
   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_field_value = list bit
+
 type instruction = (string * list (string * instr_parm_typ * instruction_field_value))
 
 let {coq} instructionEqual i1 i2 = match (i1,i2) with
@@ -117,7 +121,7 @@ let inline ~{coq} instructionInequal = unsafe_structural_inequality
 type v_kind = Bitv | Bytev
 
 type decode_error = 
-  | Unsupported_instruction_error of instruction
+  | Unsupported_instruction_error of Interp_ast.value
   | Not_an_instruction_error of opcode
   | Internal_error of string
 
@@ -264,12 +268,12 @@ val initial_instruction_state : context -> string -> list register_value -> inst
   (* string is a function name, list of value are the parameters to that function *)
 
 type instruction_or_decode_error =
-  | IDE_instr of instruction * Interp_ast.value
+  | IDE_instr of Interp_ast.value
   | IDE_decode_error of decode_error
 
 (** propose to remove the following type and use the above instead *)
 type i_state_or_error =
-  | Instr of instruction * instruction_state
+  | Instr of Interp_ast.value * instruction_state
   | Decode_error of decode_error
 
 
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 6957bb95..4f07f574 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -106,8 +106,6 @@ type register_value = <|
 
 type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *) (*MSB first everywhere*)
 
-type instruction_field_value = list bit
-
 type byte = Byte of list bit (* of length 8 *)  (*MSB first everywhere*) 
 
 type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*) * maybe integer