From 043ea8ec3faecadf34ef9010bdd539f595f9c6da Mon Sep 17 00:00:00 2001
From: Shaked Flur
Date: Thu, 8 Feb 2018 12:06:00 +0000
Subject: replaced NIA_LR/CTR/register with NIA_indirect; removed
 IK_cond_branch, and added IK_branch

---
 arm/Makefile           |  2 +-
 arm/aarch64_regfp.sail | 12 ++++++------
 arm/armV8.sail         |  2 +-
 3 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'arm')

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 *)
-- 
cgit v1.2.3