replaced NIA_LR/CTR/register with NIA_indirect;

removed IK_cond_branch, and added IK_branch

1 files changed, 12 insertions, 29 deletions

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)