diff options
| author | Shaked Flur | 2018-02-08 12:06:00 +0000 |
|---|---|---|
| committer | Shaked Flur | 2018-02-08 12:06:00 +0000 |
| commit | 043ea8ec3faecadf34ef9010bdd539f595f9c6da (patch) | |
| tree | eb44af3b9dec8e1a222872f56d4e32781596fa9e /arm | |
| parent | 151d86b911c9a266465638ee3514156dfb178e92 (diff) | |
replaced NIA_LR/CTR/register with NIA_indirect;
removed IK_cond_branch, and added IK_branch
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/Makefile | 2 | ||||
| -rw-r--r-- | arm/aarch64_regfp.sail | 12 | ||||
| -rw-r--r-- | arm/armV8.sail | 2 |
3 files changed, 8 insertions, 8 deletions
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 *) |