Skip to content

Commit 90b7b2f

Browse files
sipmasipma
committed
ARM: convert astprov to handle result types
1 parent 266ea8c commit 90b7b2f

File tree

9 files changed

+362
-108
lines changed

9 files changed

+362
-108
lines changed

‎chb/arm/opcodes/ARMArithmeticShiftRight.py‎

Lines changed: 57 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
# ------------------------------------------------------------------------------
55
# The MIT License (MIT)
66
#
7-
# Copyright (c) 2021-2024 Aarno Labs LLC
7+
# Copyright (c) 2021-2025 Aarno Labs LLC
88
#
99
# Permission is hereby granted, free of charge, to any person obtaining a copy
1010
# of this software and associated documentation files (the "Software"), to deal
@@ -30,7 +30,7 @@
3030
from chb.app.InstrXData import InstrXData
3131

3232
from chb.arm.ARMDictionaryRecord import armregistry
33-
from chb.arm.ARMOpcode import ARMOpcode, simplify_result
33+
from chb.arm.ARMOpcode import ARMOpcode, ARMOpcodeXData, simplify_result
3434
from chb.arm.ARMOperand import ARMOperand
3535

3636
import chb.ast.ASTNode as AST
@@ -39,11 +39,49 @@
3939
import chb.invariants.XXprUtil as XU
4040

4141
import chb.util.fileutil as UF
42-
4342
from chb.util.IndexedTable import IndexedTableValue
43+
from chb.util.loggingutil import chklogger
4444

4545
if TYPE_CHECKING:
46-
import chb.arm.ARMDictionary
46+
from chb.arm.ARMDictionary import ARMDictionary
47+
from chb.invariants.XVariable import XVariable
48+
from chb.invariants.XXpr import XXpr
49+
50+
51+
class ARMArithmeticShiftRightXData(ARMOpcodeXData):
52+
53+
def __init__(self, xdata: InstrXData) -> None:
54+
ARMOpcodeXData.__init__(self, xdata)
55+
56+
@property
57+
def vrd(self) -> "XVariable":
58+
return self.var(0, "vrd")
59+
60+
@property
61+
def xrn(self) -> "XXpr":
62+
return self.xpr(0, "xrn")
63+
64+
@property
65+
def xrm(self) -> "XXpr":
66+
return self.xpr(1, "xrm")
67+
68+
@property
69+
def result(self) -> "XXpr":
70+
return self.xpr(2, "result")
71+
72+
@property
73+
def rresult(self) -> "XXpr":
74+
return self.xpr(3, "rresult")
75+
76+
@property
77+
def result_simplified(self) -> str:
78+
return simplify_result(
79+
self.xdata.args[3], self.xdata.args[4], self.result, self.rresult)
80+
81+
@property
82+
def annotation(self) -> str:
83+
assignment = str(self.vrd) + " := " + self.result_simplified
84+
return self.add_instruction_condition(assignment)
4785

4886

4987
@armregistry.register_tag("ASR", ARMOpcode)
@@ -74,10 +112,7 @@ class ARMArithmeticShiftRight(ARMOpcode):
74112
useshigh[0]: lhs
75113
"""
76114

77-
def __init__(
78-
self,
79-
d: "chb.arm.ARMDictionary.ARMDictionary",
80-
ixval: IndexedTableValue) -> None:
115+
def __init__(self, d: "ARMDictionary", ixval: IndexedTableValue) -> None:
81116
ARMOpcode.__init__(self, d, ixval)
82117
self.check_key(2, 5, "ArithmeticShiftRight")
83118

@@ -100,18 +135,11 @@ def mnemonic_extension(self) -> str:
100135
return wb + cc + wide
101136

102137
def annotation(self, xdata: InstrXData) -> str:
103-
lhs = str(xdata.vars[0])
104-
result = xdata.xprs[1]
105-
rresult = xdata.xprs[2]
106-
xresult = simplify_result(xdata.args[3], xdata.args[4], result, rresult)
107-
assignment = lhs + " := " + xresult
108-
if xdata.has_unknown_instruction_condition():
109-
return "if ? then " + assignment
110-
elif xdata.has_instruction_condition():
111-
c = str(xdata.xprs[1])
112-
return "if " + c + " then " + assignment
138+
xd = ARMArithmeticShiftRightXData(xdata)
139+
if xd.is_ok:
140+
return xd.annotation
113141
else:
114-
return assignment
142+
return "Error value"
115143

116144
def ast_prov(
117145
self,
@@ -139,10 +167,16 @@ def ast_prov(
139167

140168
# high-level assignment
141169

142-
lhs = xdata.vars[0]
143-
rhs1 = xdata.xprs[0]
144-
rhs2 = xdata.xprs[1]
145-
rhs3 = xdata.xprs[3]
170+
xd = ARMArithmeticShiftRightXData(xdata)
171+
if not xd.is_ok:
172+
chklogger.logger.error(
173+
"Encountered error value at address %s", iaddr)
174+
return ([], [])
175+
176+
lhs = xd.vrd
177+
rhs1 = xd.xrn
178+
rhs2 = xd.xrm
179+
rhs3 = xd.rresult
146180
rdefs = xdata.reachingdefs
147181
defuses = xdata.defuses
148182
defuseshigh = xdata.defuseshigh

‎chb/arm/opcodes/ARMCompareBranchNonzero.py‎

Lines changed: 51 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
# ------------------------------------------------------------------------------
55
# The MIT License (MIT)
66
#
7-
# Copyright (c) 2021-2024 Aarno Labs LLC
7+
# Copyright (c) 2021-2025 Aarno Labs LLC
88
#
99
# Permission is hereby granted, free of charge, to any person obtaining a copy
1010
# of this software and associated documentation files (the "Software"), to deal
@@ -30,7 +30,7 @@
3030
from chb.app.InstrXData import InstrXData
3131

3232
from chb.arm.ARMDictionaryRecord import armregistry
33-
from chb.arm.ARMOpcode import ARMOpcode, simplify_result
33+
from chb.arm.ARMOpcode import ARMOpcode, ARMOpcodeXData, simplify_result
3434
from chb.arm.ARMOperand import ARMOperand
3535

3636
import chb.ast.ASTNode as AST
@@ -48,10 +48,46 @@
4848

4949
if TYPE_CHECKING:
5050
from chb.arm.ARMDictionary import ARMDictionary
51+
from chb.invariants.XXpr import XXpr
52+
53+
54+
class ARMCompareBranchNonZeroXData(ARMOpcodeXData):
55+
56+
def __init__(self, xdata: InstrXData) -> None:
57+
ARMOpcodeXData.__init__(self, xdata)
58+
59+
@property
60+
def xrn(self) -> "XXpr":
61+
return self.xpr(0, "xrn")
62+
63+
@property
64+
def txpr(self) -> "XXpr":
65+
return self.xpr(1, "txpr")
66+
67+
@property
68+
def fxpr(self) -> "XXpr":
69+
return self.xpr(2, "fxpr")
70+
71+
@property
72+
def tcond(self) -> "XXpr":
73+
return self.xpr(3, "tcond")
74+
75+
@property
76+
def fcond(self) -> "XXpr":
77+
return self.xpr(4, "fcond")
78+
79+
@property
80+
def xtgt(self) -> "XXpr":
81+
return self.xpr(5, "xtgt")
82+
83+
@property
84+
def annotation(self) -> str:
85+
return "if " + str(self.tcond) + " goto " + str(self.xtgt)
86+
5187

5288

5389
@armregistry.register_tag("CBNZ", ARMOpcode)
54-
class ARMCompareBranchZero(ARMOpcode):
90+
class ARMCompareBranchNonZero(ARMOpcode):
5591
"""Compares the value in a register with zero and conditionally branches forward.
5692
5793
CBNZ <Rn>, <label>
@@ -69,10 +105,7 @@ class ARMCompareBranchZero(ARMOpcode):
69105
xprs[5]: target
70106
"""
71107

72-
def __init__(
73-
self,
74-
d: "ARMDictionary",
75-
ixval: IndexedTableValue) -> None:
108+
def __init__(self, d: "ARMDictionary", ixval: IndexedTableValue) -> None:
76109
ARMOpcode.__init__(self, d, ixval)
77110
self.check_key(1, 2, "CompareBranchNonzero")
78111

@@ -86,14 +119,21 @@ def opargs(self) -> List[ARMOperand]:
86119

87120
def ft_conditions(self, xdata: InstrXData) -> Sequence[XXpr]:
88121
if xdata.has_branch_conditions():
89-
return [xdata.xprs[4], xdata.xprs[3]]
122+
xd = ARMCompareBranchNonZeroXData(xdata)
123+
if xd.is_ok:
124+
return [xd.fcond, xd.tcond]
125+
else:
126+
chklogger.logger.warning("CBNZ: Encountered error condition")
127+
return []
90128
else:
91129
return []
92130

93131
def annotation(self, xdata: InstrXData) -> str:
94-
xpr = str(xdata.xprs[3])
95-
tgt = str(xdata.xprs[5])
96-
return "if " + xpr + " != 0 goto " + tgt
132+
xd = ARMCompareBranchNonZeroXData(xdata)
133+
if xd.is_ok:
134+
return xd.annotation
135+
else:
136+
return "Error value"
97137

98138
def ast_prov(
99139
self,

‎chb/arm/opcodes/ARMCompareBranchZero.py‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -120,8 +120,7 @@ def ft_conditions(self, xdata: InstrXData) -> Sequence[XXpr]:
120120
if xd.is_ok:
121121
return [xd.fcond, xd.tcond]
122122
else:
123-
chklogger.logger.warning(
124-
"CBZ: Encountered error condition at address")
123+
chklogger.logger.warning("CBZ: Encountered error condition")
125124
return []
126125
else:
127126
return []

‎chb/arm/opcodes/ARMReverseSubtract.py‎

Lines changed: 56 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
# ------------------------------------------------------------------------------
55
# The MIT License (MIT)
66
#
7-
# Copyright (c) 2021-2024 Aarno Labs LLC
7+
# Copyright (c) 2021-2025 Aarno Labs LLC
88
#
99
# Permission is hereby granted, free of charge, to any person obtaining a copy
1010
# of this software and associated documentation files (the "Software"), to deal
@@ -30,7 +30,7 @@
3030
from chb.app.InstrXData import InstrXData
3131

3232
from chb.arm.ARMDictionaryRecord import armregistry
33-
from chb.arm.ARMOpcode import ARMOpcode, simplify_result
33+
from chb.arm.ARMOpcode import ARMOpcode, ARMOpcodeXData, simplify_result
3434
from chb.arm.ARMOperand import ARMOperand
3535

3636
import chb.ast.ASTNode as AST
@@ -39,12 +39,50 @@
3939
import chb.invariants.XXprUtil as XU
4040

4141
import chb.util.fileutil as UF
42-
4342
from chb.util.IndexedTable import IndexedTableValue
43+
from chb.util.loggingutil import chklogger
4444

4545
if TYPE_CHECKING:
4646
from chb.arm.ARMDictionary import ARMDictionary
4747
from chb.arm.ARMOperandKind import ARMShiftedRegisterOp
48+
from chb.invariants.XVariable import XVariable
49+
from chb.invariants.XXpr import XXpr
50+
51+
52+
class ARMReverseSubtractXData(ARMOpcodeXData):
53+
54+
def __init__(self, xdata: InstrXData) -> None:
55+
ARMOpcodeXData.__init__(self, xdata)
56+
57+
@property
58+
def vrd(self) -> "XVariable":
59+
return self.var(0, "vrd")
60+
61+
@property
62+
def xrn(self) -> "XXpr":
63+
return self.xpr(0, "xrn")
64+
65+
@property
66+
def xrm(self) -> "XXpr":
67+
return self.xpr(1, "xrm")
68+
69+
@property
70+
def result(self) -> "XXpr":
71+
return self.xpr(2, "result")
72+
73+
@property
74+
def rresult(self) -> "XXpr":
75+
return self.xpr(3, "rresult")
76+
77+
@property
78+
def result_simplified(self) -> str:
79+
return simplify_result(
80+
self.xdata.args[3], self.xdata.args[4], self.result, self.rresult)
81+
82+
@property
83+
def annotation(self) -> str:
84+
assignment = str(self.vrd) + " := " + self.result_simplified
85+
return self.add_instruction_condition(assignment)
4886

4987

5088
@armregistry.register_tag("RSB", ARMOpcode)
@@ -102,11 +140,11 @@ def is_writeback(self) -> bool:
102140
return self.args[0] == 1
103141

104142
def annotation(self, xdata: InstrXData) -> str:
105-
lhs = str(xdata.vars[0])
106-
result = xdata.xprs[2]
107-
rresult = xdata.xprs[3]
108-
xresult = simplify_result(xdata.args[3], xdata.args[4], result, rresult)
109-
return lhs + " := " + xresult
143+
xd = ARMReverseSubtractXData(xdata)
144+
if xd.is_ok:
145+
return xd.annotation
146+
else:
147+
return "Error value"
110148

111149
def ast_prov(
112150
self,
@@ -139,10 +177,16 @@ def ast_prov(
139177

140178
# high-level assignment
141179

142-
lhs = xdata.vars[0]
143-
rhs1 = xdata.xprs[0]
144-
rhs2 = xdata.xprs[1]
145-
rhs3 = xdata.xprs[3]
180+
xd = ARMReverseSubtractXData(xdata)
181+
if not xd.is_ok:
182+
chklogger.logger.error(
183+
"Encountered error value at address %s", iaddr)
184+
return ([], [])
185+
186+
lhs = xd.vrd
187+
rhs1 = xd.xrn
188+
rhs2 = xd.xrm
189+
rhs3 = xd.rresult
146190

147191
defuses = xdata.defuses
148192
defuseshigh = xdata.defuseshigh

0 commit comments

Comments
 (0)