replaced NIA_LR/CTR/register with NIA_indirect;

removed IK_cond_branch, and added IK_branch

13 files changed, 90 insertions, 113 deletions

diff --git a/Makefile b/Makefile
index 97e42f7e..2b5e867c 100644
--- a/Makefile
+++ b/Makefile
@@ -1,24 +1,35 @@
-.PHONY: all sail language clean archs isabelle-lib apply_header
+ARCHS += power
+ARCHS += arm
+ARCHS += risc-v
+# ARCHS += mips
+# ARCHS += cheri
+ARCHS += x86
 
 all: sail interpreter
+.PHONY: all
 
 sail:
 	$(MAKE) -C src
 	ln -f -s src/sail.native sail
+.PHONY: sail
 
 language:
 	$(MAKE) -C language
+.PHONY: language
 
-interpreter: 
+interpreter:
 	$(MAKE) -C src interpreter
+.PHONY: interpreter
 
 archs:
-	for arch in arm mips cheri; do\
+	for arch in $(ARCHS); do\
 	  $(MAKE) -C "$$arch" || exit;\
 	done
+.PHONY: archs
 
 isabelle-lib:
 	$(MAKE) -C isabelle-lib
+.PHONY: isabelle-lib
 
 apply_header:
 	$(MAKE) clean
@@ -29,9 +40,17 @@ apply_header:
 	headache -c etc/headache_config -h src/LICENCE `ls src/lem_interp/*.ml`
 	headache -c etc/headache_config -h src/LICENCE `ls src/lem_interp/*.lem`
 	$(MAKE) -C arm apply_header
+.PHONY: apply_header
 
 clean:
 	for subdir in src arm ; do\
 	  $(MAKE) -C "$$subdir" clean;\
 	done
 	-rm sail
+.PHONY: clean
+
+clean_archs:
+	for arch in $(ARCHS); do\
+	  $(MAKE) -C "$$arch" clean;\
+	done
+.PHONY: clean_archs
diff --git a/arm/Makefile b/arm/Makefile
index d7124df6..c597f714 100644
--- a/arm/Makefile
+++ b/arm/Makefile
@@ -38,7 +38,7 @@ apply_header:
 .PHONY: apply_header
 
 ######################################################################
-IDLARM=../../../rsem/idlarm
+IDLARM=../../rsem/idlarm
 
 pull_from_idlarm:
 	$(MAKE) -C $(IDLARM) clean
diff --git a/arm/aarch64_regfp.sail b/arm/aarch64_regfp.sail
index 148f9646..60aa48d1 100644
--- a/arm/aarch64_regfp.sail
+++ b/arm/aarch64_regfp.sail
@@ -168,7 +168,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) effect pure initia
       let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o};
       (bit[64]) nia' := rPC() + offset;
       Nias := [|| NIAFP_successor, NIAFP_concrete_address(nia') ||];
-      ik := IK_cond_branch;
+      ik := IK_branch;
     }
     case (BranchConditional(offset,condition)) -> {
       iR := append(iR,ConditionHoldsIFP(condition));
@@ -176,7 +176,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) effect pure initia
          ConditionHolds(condition) *)
       let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o};
       Nias := [|| NIAFP_successor, NIAFP_concrete_address(rPC() + offset) ||];
-      ik := IK_cond_branch;
+      ik := IK_branch;
     }
     case (GenerateExceptionEL1(imm)) -> not_implemented("GenerateExceptionEL1")
     case (GenerateExceptionEL2(imm)) -> not_implemented("GenerateExceptionEL2")
@@ -271,14 +271,14 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) effect pure initia
          operand[bit_pos] == bit_val *)
       let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o}; 
       Nias := [|| NIAFP_successor, NIAFP_concrete_address(rPC() + offset) ||];
-      ik := IK_cond_branch;
+      ik := IK_branch;
     }
     case (BranchImmediate(branch_type,offset)) -> {
       if branch_type == BranchType_CALL
         then {iR := _PCfp :: iR; oR := append(xFP(30),oR)};
       let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o}; 
       Nias := [|| NIAFP_concrete_address(rPC() + offset) ||];
-      ik := IK_simple (* IK_uncond_branch *)
+      ik := IK_branch
     }
     case (BranchRegister(n,branch_type)) -> {
       iR := append(iR,xFP(n));
@@ -287,8 +287,8 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) effect pure initia
       let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o};
       Nias := if n ==31
               then [|| NIAFP_concrete_address(0) ||]
-              else [|| NIAFP_register(RFull(_Rs[n]))||];
-      ik := IK_simple (* IK_uncond_branch *)
+              else [|| NIAFP_indirect_address ||];
+      ik := IK_branch
     }
     case (ExceptionReturn) -> not_implemented("ExceptionReturn")
     case (DebugRestorePState) -> not_implemented("DebugRestorePState")
diff --git a/arm/armV8.sail b/arm/armV8.sail
index cfdb94f9..4a62bda6 100644
--- a/arm/armV8.sail
+++ b/arm/armV8.sail
@@ -642,7 +642,7 @@ function clause execute (BranchRegister(n,branch_type)) =
   (bit[64]) target := rX(n);
 
   if branch_type == BranchType_CALL then wX(30) := rPC() + 4;
-    BranchTo(target, branch_type);
+  BranchTo(target, branch_type);
 }
 
 (* ERET *)
diff --git a/etc/regfp.sail b/etc/regfp.sail
index cc057f2e..9a6172a9 100644
--- a/etc/regfp.sail
+++ b/etc/regfp.sail
@@ -16,9 +16,7 @@ typedef regfps = list <regfp>
 typedef niafp = const union {
   NIAFP_successor;
   (bit[64]) NIAFP_concrete_address;
-  NIAFP_LR;
-  NIAFP_CTR;
-  (regfp) NIAFP_register;
+  NIAFP_indirect_address;
 }
 
 typedef niafps = list <niafp>
@@ -90,7 +88,7 @@ typedef instruction_kind = const union {
   (read_kind) IK_mem_read;
   (write_kind) IK_mem_write;
   (read_kind, write_kind) IK_mem_rmw;
-  IK_cond_branch;
+  IK_branch;
   (trans_kind) IK_trans;
   IK_simple
 }
diff --git a/mips/mips_regfp.sail b/mips/mips_regfp.sail
index 36750583..13165f67 100644
--- a/mips/mips_regfp.sail
+++ b/mips/mips_regfp.sail
@@ -322,38 +322,34 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
       oR := RFull("HI") :: RFull ("LO") :: oR;
     }
     case (J(offset)) -> {
-      (* XXX actually unconditional jump *)
-      (*ik := IK_cond_branch;*)
+      ik := IK_branch;
       Dia := DIAFP_concrete((PC + 4)[63..28] : offset : 0b00);
     }
     case (JAL(offset)) -> {
-      (* XXX actually unconditional jump *)
-      (*ik := IK_cond_branch;*)
+      ik := IK_branch;
       oR := RFull("GPR31") :: oR;
       Dia := DIAFP_concrete((PC + 4)[63..28] : offset : 0b00);
     }
     case (JR(rs)) -> {
-      (* XXX actually unconditional jump *)
-      (*ik := IK_cond_branch;*)
+      ik := IK_branch;
       iR := RFull(GPRs[rs]) :: iR;
       Dia := DIAFP_reg(RFull(GPRs[rs]));
     }
     case (JALR(rs, rd)) -> {
-      (* XXX actually unconditional jump *)
-      (*ik := IK_cond_branch;*)
+      ik := IK_branch;
       iR := RFull(GPRs[rs]) :: iR;
       oR := RFull("GPR31") :: oR;
       Dia := DIAFP_reg(RFull(GPRs[rs]));
     }
     case (BEQ(rs, rd, imm, ne, likely)) -> {
-      ik := IK_cond_branch;
+      ik := IK_branch;
       if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
       if rd == 0 then () else iR := RFull(GPRs[rd]) :: iR;
       let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in
       Dia := DIAFP_concrete (PC + offset);
     }
     case (BCMPZ(rs, imm, cmp, link, likely)) -> {
-      ik := IK_cond_branch;
+      ik := IK_branch;
       if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
       if link then
         oR := RFull("GPR31") :: oR;
diff --git a/power/power_regfp.sail b/power/power_regfp.sail
index 35ecb37b..1f421186 100644
--- a/power/power_regfp.sail
+++ b/power/power_regfp.sail
@@ -76,7 +76,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
       if LK then oR := RFull("LR") :: oR;
       (bit[64]) nia' := if AA then EXTS(LI : 0b00) else CIA + EXTS(LI : 0b00);
       Nias := [|| NIAFP_concrete_address(nia') ||];
-      ik := IK_simple (* IK_uncond_branch *);
+      ik := IK_branch
     }
     case (Bc (BO, BI, BD, AA, LK)) -> {
       iR := mode64bit_fp :: iR;
@@ -89,7 +89,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
       if AA then iR := CIA_fp :: iR; 
       Nias := [|| NIAFP_successor, NIAFP_concrete_address(if AA then EXTS(BD : 0b00) else CIA + EXTS(BD : 0b00)) ||];
       if LK then {oR := RFull("LR") :: oR; iR := CIA_fp :: iR};
-      ik := IK_cond_branch
+      ik := IK_branch
     }
     case (Bclr (BO, BI, BH, LK)) -> {
       iR := mode64bit_fp :: iR;
@@ -99,18 +99,18 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
       (* TODO: actually whether LR is read, NIA written depends on runtime data *)
       (* if ctr_ok .. *) iR := RSlice("LR",0,61) :: iR;
       oR := NIA_fp :: oR;
-      Nias := [|| NIAFP_successor, NIAFP_LR ||];
+      Nias := [|| NIAFP_successor, NIAFP_indirect_address ||];
       if LK then {oR := RFull("LR") :: oR; iR := CIA_fp :: iR;};
-      ik := IK_cond_branch;
+      ik := IK_branch;
     }
     case (Bcctr (BO, BI, BH, LK)) -> {
       iR := RSliceBit("CR",BI + 32) :: iR;
       (* TODO: actually whether CTR is read and NIA written depends on runtime data *)
       (* if cond_ok *) iR := RSlice("CTR",0,61) :: iR;
       oR := NIA_fp :: oR;
-      Nias := [|| NIAFP_successor, NIAFP_CTR ||];
+      Nias := [|| NIAFP_successor, NIAFP_indirect_address ||];
       if LK then {oR := RFull("LR") :: oR; iR := CIA_fp :: iR;};
-      ik := IK_cond_branch;
+      ik := IK_branch;
     }
     case (Crand (BT, BA, BB)) -> {
       iR := RSliceBit("CR",BA + 32) :: RSliceBit("CR",BB + 32) :: iR;
@@ -150,7 +150,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
     }
     case (Sc (LEV)) -> {
       (* fake test end instruction *)
-      Nias := if LEV==63 then [|| ||] else [|| NIAFP_successor ||]; 
+      ();
     }
     case (Scv (LEV)) -> ()
     case (Lbz (RT, RA, D)) -> {
@@ -1480,4 +1480,4 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) recalculate_stswx_
   };
   ik := IK_mem_write(Write_plain);
   (iR,oR,aR,Nias,Dia,ik)}
-}
\ No newline at end of file
+}
diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail
index dee9cc8e..5bbcf044 100644
--- a/risc-v/riscv_regfp.sail
+++ b/risc-v/riscv_regfp.sail
@@ -23,20 +23,22 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
      case (RISCV_JAL ( imm, rd)) -> {
             if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
             let (bit[64]) offset = EXTS(imm) in
-            Nias := [|| NIAFP_concrete_address (PC + offset) ||]
+            Nias := [|| NIAFP_concrete_address (PC + offset) ||];
+            ik := IK_branch;
      }
      case (RISCV_JALR ( imm, rs, rd)) -> {
             if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
             if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
             let (bit[64]) offset = EXTS(imm) in
-            Nias := [|| NIAFP_register (RFull(GPRstr[rs])) ||];
+            Nias := [|| NIAFP_indirect_address ||];
+            ik := IK_branch;
      }
      case (BTYPE ( imm, rs2, rs1, op)) -> {
             if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR;
             if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR;
-            ik := IK_cond_branch;
+            ik := IK_branch;
             let (bit[64]) offset = EXTS(imm) in
-            Nias := NIAFP_concrete_address(PC + offset) :: Nias;
+            Nias := [|| NIAFP_concrete_address(PC + offset), NIAFP_successor ||];
      }
      case (ITYPE ( imm, rs, rd, op)) -> {
             if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
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)
diff --git a/x86/x64.sail b/x86/x64.sail
index 9fa0b838..3549b123 100644
--- a/x86/x64.sail
+++ b/x86/x64.sail
@@ -1457,8 +1457,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
           oR := RFull("RSP") :: oR;
           aR := ars;
           Nias := switch irm {
-          (* XXX register name is not important here -- just indicates we don't know the destination yet. *)
-            case (Rm (v))  -> NIAFP_register(RFull("RAX"))
+            case (Rm (v))  -> NIAFP_indirect_address
             case (Imm (v)) -> NIAFP_concrete_address(RIP + v)
           } :: Nias;
       }
@@ -1486,7 +1485,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
     case(HLT                          ) -> ()
     case(Jcc     (c, imm64)           ) -> 
       let flags = regfp_cond(c) in {
-        ik := IK_cond_branch;
+        ik := IK_branch;
         iR := RFull("RIP") :: flags;
         Nias :=  NIAFP_concrete_address(RIP + imm64) :: Nias;
       }
@@ -1495,8 +1494,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
         ik := if m then IK_mem_read(Read_plain) else IK_simple;
         iR := RFull("RIP")::append(rs, ars);
         aR := ars;
-        (* XXX register name is not important here -- just indicates we don't know the destination yet. *)
-        Nias := NIAFP_register(RFull("RAX")) :: Nias;
+        Nias := NIAFP_indirect_address :: Nias;
       }
     case(LEA     (sz, ds)             ) ->
       let (_, irs, ors, ars) = regfp_dest_src (ds) in {
@@ -1512,7 +1510,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
     }
     case(LOOP    (c, imm64)           ) -> 
       let flags = regfp_cond(c) in {
-          ik := IK_cond_branch;
+          ik := IK_branch;
           iR := RFull("RCX") :: flags;
           oR := RFull("RCX") :: oR;
           Nias := NIAFP_concrete_address(RIP + imm64) :: Nias;
@@ -1578,8 +1576,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
       iR := RFull("RSP") :: iR;
       oR := RFull("RSP") :: oR;
       aR := RFull("RSP") :: aR;
-      (* XXX register name is not important here -- just indicates we don't know the destination yet. *)
-      Nias := NIAFP_register(RFull("RAX")) :: Nias;
+      Nias := NIAFP_indirect_address :: Nias;
     }
     case(SET     (c, b, r_m)          ) -> 
       let flags = regfp_cond(c) in