replaced NIA_LR/CTR/register with NIA_indirect;

removed IK_cond_branch, and added IK_branch

4 files changed, 33 insertions, 68 deletions

diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem
index 76880dbd..7fea0409 100644
--- a/src/gen_lib/deep_shallow_convert.lem
+++ b/src/gen_lib/deep_shallow_convert.lem
@@ -532,7 +532,7 @@ let instruction_kindToInterpValue = function
   | 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_branch -> V_ctor (Id_aux (Id "IK_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
@@ -541,7 +541,7 @@ let rec instruction_kindFromInterpValue v = match v with
   | 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_branch") _) _ _ v -> IK_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
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 121f6cc8..ffccaa7e 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -912,9 +912,7 @@ type regfp =
 type niafp = 
   | NIAFP_successor
   | NIAFP_concrete_address of vector bitU
-  | NIAFP_LR
-  | NIAFP_CTR
-  | NIAFP_register of regfp
+  | NIAFP_indirect_address
 
 (* only for MIPS *)
 type diafp = 
@@ -946,9 +944,7 @@ end
 let niafp_to_nia reginfo = function
   | NIAFP_successor -> NIA_successor
   | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v)
-  | NIAFP_LR -> NIA_LR
-  | NIAFP_CTR -> NIA_CTR
-  | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r)
+  | NIAFP_indirect_address -> NIA_indirect_address
 end
 
 let diafp_to_dia reginfo = function
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 2b754e25..9603b9fe 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -571,13 +571,11 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
          | Interp_ast.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) 
          | _ -> failwith "Register footprint analysis did not return dia of expected type" end in
        let nia_to_nia = function
-         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor
+         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _ -> NIA_successor
          | Interp_ast.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address ->
             NIA_concrete_address (get_addr address)
-         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR
-         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR
-         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg ->
-            NIA_register (reg_to_reg_name reg)
+         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_indirect_address") _) _ _ _ ->
+            NIA_indirect_address
          | _ -> failwith "Register footprint analysis did not return nia of expected type" end in
        let readk_to_readk = function
                          | "Read_plain" ->             Read_plain
@@ -634,8 +632,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
            (Interp_ast.V_tuple [(Interp_ast.V_ctor (Id_aux (Id readk) _) _ _ _) ;
                                 (Interp_ast.V_ctor (Id_aux (Id writek) _) _ _ _)]) ->
             IK_mem_rmw(readk_to_readk readk, writek_to_writek writek)
-         | Interp_ast.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ ->
-            IK_cond_branch
+         | Interp_ast.V_ctor (Id_aux (Id "IK_branch") _) _ _ _ ->
+            IK_branch
          | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ ->
             IK_simple
          | _ -> failwith "Analysis returned unexpected instruction kind"
@@ -1157,7 +1155,7 @@ let rr_interp_exhaustive mode i_state events =
 *)
 
 
-let instruction_kind_of_event : event -> maybe instruction_kind = function
+let instruction_kind_of_event nia_reg : event -> maybe instruction_kind = function
   (* this is a hack to avoid adding special events for AArch64 transactional-memory *)
   | E_read_reg (Reg "TMStartEffect" 63 64 D_decreasing) -> Just (IK_trans Transaction_start)
   | E_write_reg (Reg "TMAbortEffect" 63 64 D_decreasing) _ -> Just (IK_trans Transaction_abort)
@@ -1173,7 +1171,9 @@ let instruction_kind_of_event : event -> maybe instruction_kind = function
   | E_barrier bk -> Just (IK_barrier bk)
   | E_footprint -> Nothing
   | E_read_reg _ -> Nothing
-  | E_write_reg _ _ -> Nothing
+  | E_write_reg reg _ ->
+      if register_base_name reg = register_base_name nia_reg then Just IK_branch
+      else Nothing
   | E_error s -> failwith ("instruction_kind_of_event error: "^s)
   | E_escape -> Nothing (*failwith ("instruction_kind_of_event escape")*)
  end
@@ -1252,8 +1252,8 @@ let interp_instruction_analysis
       (interp_exhaustive : ((list (reg_name * register_value)) -> list event))
       instruction 
       nia_reg 
-      (nias_function : (list (maybe address) -> list reg_name -> list nia))
-      ism environment = 
+      (nias_function : (list (maybe address) -> list nia))
+      ism environment =
     
     let es = interp_exhaustive environment in
 
@@ -1263,19 +1263,15 @@ let interp_instruction_analysis
     let regs_feeding_address = List.concatMap regs_feeding_memory_access_address_of_event es in
 
     let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in
-
-    let nias = nias_function nia_address regs_in in
+    let nias = nias_function nia_address in
 
     let dia = DIA_none in (* FIX THIS! *)
 
-
     let inst_kind =
-      match List.mapMaybe instruction_kind_of_event es with
-      | [] -> if List.length nias > 1 then IK_cond_branch else IK_simple
+      match List.mapMaybe (instruction_kind_of_event nia_reg) es with
+      | [] -> IK_simple
+      | inst_kind :: [] -> inst_kind
       | inst_kind :: inst_kinds ->
-          let () = ensure (List.length nias > 1 --> inst_kind = IK_cond_branch)
-                      "multiple NIAs must be IK_cond_branch" in
-
           if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then
             inst_kind
 
@@ -1286,19 +1282,9 @@ let interp_instruction_analysis
                 | IK_mem_write _ -> true
                 | IK_mem_rmw _   -> false
                 | IK_barrier _   -> false
-                | IK_cond_branch -> false
+                | IK_branch      -> false
                 | IK_trans _     -> false
                 | IK_simple      -> false
-                end) &&
-            (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
-                match inst_kind' with
-                | IK_mem_read _  -> true
-                | _              -> false
-                end) &&
-            (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
-                match inst_kind' with
-                | IK_mem_write _ -> true
-                | _              -> false
                 end)
           then
             match
@@ -1355,7 +1341,7 @@ let interp_compare_analyses
       interp_exhaustive
       (instruction : Interp_ast.value)
       nia_reg
-      (nias_function : (list (maybe address) -> list reg_name -> list nia))
+      (nias_function : (list (maybe address) -> list nia))
       ism
       environment
       analysis_function
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index de3ba319..c7e01815 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -559,10 +559,9 @@ type instruction_kind =
   | IK_mem_read  of read_kind
   | IK_mem_write of write_kind
   | IK_mem_rmw   of (read_kind * write_kind)
-  | IK_cond_branch
-  (* unconditional branches are not distinguished in the instruction_kind;
-  they just have particular nias (and will be IK_simple *)
-  (* | IK_uncond_branch *)
+  | IK_branch (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address),
+  indirect/computed-branch (single nia of kind NIA_indirect_address)
+  and branch/jump (single nia of kind NIA_concrete_address) *)
   | IK_trans     of trans_kind
   | IK_simple
 
@@ -573,7 +572,7 @@ instance (Show instruction_kind)
     | IK_mem_read read_kind   -> "IK_mem_read " ^ (show read_kind)
     | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind)
     | IK_mem_rmw (r, w)       -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w)
-    | IK_cond_branch          -> "IK_cond_branch"
+    | IK_branch               -> "IK_branch"
     | IK_trans trans_kind     -> "IK_trans " ^ (show trans_kind)
     | IK_simple               -> "IK_simple"
   end
@@ -1232,32 +1231,18 @@ end
 type nia = 
   | NIA_successor
   | NIA_concrete_address of address
-  | NIA_LR   (* "LR0:61 || 0b00" in Power pseudocode *)
-  | NIA_CTR  (* "CTR0:61 || 0b00" in Power pseudocode *)
-  | NIA_register of reg_name (* the address will be in a register,
-                                corresponds to AArch64 BLR, BR, RET
-                                instructions *)
+  | NIA_indirect_address
 
 let niaCompare n1 n2 = match (n1,n2) with
   | (NIA_successor, NIA_successor) -> EQ
   | (NIA_successor, _) -> LT
-  | (NIA_concrete_address _, NIA_successor) -> GT
+  | (_, NIA_successor) -> GT
   | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2
   | (NIA_concrete_address _, _) -> LT
-  | (NIA_LR, NIA_successor) -> GT
-  | (NIA_LR, NIA_concrete_address _) -> GT
-  | (NIA_LR, NIA_LR) -> EQ
-  | (NIA_LR, _) -> LT
-  | (NIA_CTR, NIA_successor) -> GT
-  | (NIA_CTR, NIA_concrete_address _) -> GT
-  | (NIA_CTR, NIA_LR) -> GT
-  | (NIA_CTR, NIA_CTR) -> EQ
-  | (NIA_CTR, NIA_register _) -> LT
-  | (NIA_register _, NIA_successor) -> GT
-  | (NIA_register _, NIA_concrete_address _) -> GT
-  | (NIA_register _, NIA_LR) -> GT
-  | (NIA_register _, NIA_CTR) -> GT
-  | (NIA_register r1, NIA_register r2) -> compare r1 r2
+  | (_, NIA_concrete_address _) -> GT
+  | (NIA_indirect_address, NIA_indirect_address) -> EQ
+  (* | (NIA_indirect_address, _) -> LT
+  | (_, NIA_indirect_address) -> GT *)
   end
 
 instance (Ord nia)
@@ -1269,11 +1254,9 @@ instance (Ord nia)
 end
 
 let stringFromNia = function
-  | NIA_successor -> "NIA_successor"
+  | NIA_successor          -> "NIA_successor"
   | NIA_concrete_address a -> "NIA_concrete_address " ^ show a
-  | NIA_LR -> "NIA_LR"
-  | NIA_CTR -> "NIA_CTR"
-  | NIA_register r -> "NIA_register " ^ show r
+  | NIA_indirect_address   -> "NIA_indirect_address"
 end
 
 instance (Show nia)