allow for conditional return instructions

Author: sipma

chb/app/BasicBlock.py

@@ -95,6 +95,10 @@ def last_instruction(self) -> Instruction:
     def has_return(self) -> bool:
         return self.last_instruction.is_return_instruction
 
+    @property
+    def has_conditional_return(self) -> bool:
+        return self.last_instruction.is_conditional_return_instruction
+
     @property
     @abstractmethod
     def instructions(self) -> Mapping[str, Instruction]:

chb/app/CHVersion.py

@@ -1 +1 @@
-chbversion: str = "0.3.0-20250608"
+chbversion: str = "0.3.0-20250624"

chb/app/Cfg.py

@@ -682,10 +682,32 @@ def ast(self,
         for n in self.rpo_sorted_nodes:
             astblock = astfn.astblock(n)
             blocknode = astblock.ast(astree)
-            if astblock.has_return:
+
+            if astblock.has_conditional_return:
+                succ = self.successors(n)[0]
                 instr = astblock.last_instruction
                 rv = instr.return_value()
                 astexpr: Optional[AST.ASTExpr] = None
+                if rv is not None and not astree.returns_void():
+                    astexpr = XU.xxpr_to_ast_def_expr(
+                        rv, instr.xdata, instr.iaddr, astree)
+                    rtnstmt = astree.mk_return_stmt(
+                        astexpr, instr.iaddr, instr.bytestring)
+                    rvcondition = instr.ast_condition(astree)
+                    if rvcondition is not None:
+                        elsebr = astree.mk_instr_sequence([])
+                        brstmt = cast(AST.ASTBranch, astree.mk_branch(
+                            rvcondition, rtnstmt, elsebr, succ))
+                        blockstmts[n] = [blocknode, brstmt]
+                    else:
+                        blockstmts[n] = [blocknode, rtnstmt]
+                else:
+                    blockstmts[n] = [blocknode]
+
+            elif astblock.has_return:
+                instr = astblock.last_instruction
+                rv = instr.return_value()
+                astexpr = None
                 if rv is not None and not astree.returns_void():
                     astexpr = XU.xxpr_to_ast_def_expr(
                         rv, instr.xdata, instr.iaddr, astree)

chb/app/InstrXData.py

@@ -526,6 +526,26 @@ def get_instruction_condition(self) -> XXpr:
         else:
             raise UF.CHBError("No instruction condition index found")
 
+    def get_instruction_c_condition(self) -> XXpr:
+        for t in self.tags:
+            if t.startswith("icc:"):
+                index = int(t[4:])
+                argval = self.args[index]
+                if argval == -2:
+                    raise UF.CHBError(
+                        "Error value in instruction c condition")
+                return self.xprdictionary.xpr(argval)
+        else:
+            raise UF.CHBError("No instruction c_condition index found")
+
+    def has_valid_instruction_c_condition(self) -> bool:
+        for t in self.tags:
+            if t.startswith("icc:"):
+                index = int(t[4:])
+                argval = self.args[index]
+                return argval >= 0
+        return False
+
     def has_condition_block_condition(self) -> bool:
         return "TF" in self.tags
 
@@ -576,6 +596,17 @@ def has_return_cxpr(self) -> bool:
         else:
             return False
 
+    @property
+    def is_return_xpr_ok(self) -> bool:
+        if not self.has_return_xpr():
+            return False
+        rvtag = next(t for t in self.tags if t.startswith("return:"))
+        rvix = int(rvtag[7:])
+        rval = self.args[rvix]
+        if rval == -2:
+            return False
+        return True
+
     def get_return_xpr(self) -> XXpr:
         rvtag = next(t for t in self.tags if t.startswith("return:"))
         rvix = int(rvtag[7:])
@@ -584,6 +615,17 @@ def get_return_xpr(self) -> XXpr:
             raise UF.CHBError("Unexpected error in return value")
         return self.xprdictionary.xpr(rval)
 
+    @property
+    def is_return_xxpr_ok(self) -> bool:
+        if not self.has_return_xpr():
+            return False
+        rvtag = next(t for t in self.tags if t.startswith("return:"))
+        rvix = int(rvtag[7:])
+        rval = self.args[rvix + 1]
+        if rval == -2:
+            return False
+        return True
+
     def get_return_xxpr(self) -> XXpr:
         rvtag = next(t for t in self.tags if t.startswith("return:"))
         rvix = int(rvtag[7:])

chb/app/Instruction.py

@@ -206,6 +206,10 @@ def is_store_instruction(self) -> bool:
     def is_return_instruction(self) -> bool:
         ...
 
+    @property
+    def is_conditional_return_instruction(self) -> bool:
+        return False
+
     @property
     def is_nop_instruction(self) -> bool:
         return False

chb/arm/opcodes/ARMBranchExchange.py

@@ -38,7 +38,7 @@
 from chb.astinterface.ASTInterface import ASTInterface
 
 from chb.invariants.XXpr import XXpr
-
+import chb.invariants.XXprUtil as XU
 
 import chb.util.fileutil as UF
 from chb.util.loggingutil import chklogger
@@ -69,6 +69,14 @@ def xxtgt(self) -> "XXpr":
     def has_return_xpr(self) -> bool:
         return self.xdata.has_return_xpr()
 
+    @property
+    def is_return_xpr_ok(self) -> bool:
+        return self.xdata.is_return_xpr_ok
+
+    @property
+    def is_return_xxpr_ok(self) -> bool:
+        return self.xdata.is_return_xxpr_ok
+
     def returnval(self) -> "XXpr":
         return self.xdata.get_return_xpr()
 
@@ -81,6 +89,18 @@ def has_creturnval(self) -> bool:
     def creturnval(self) -> "XXpr":
         return self.xdata.get_return_cxpr()
 
+    def has_instruction_condition(self) -> bool:
+        return self.xdata.has_instruction_condition()
+
+    def get_instruction_condition(self) -> "XXpr":
+        return self.xdata.get_instruction_condition()
+
+    def has_valid_instruction_c_condition(self) -> bool:
+        return self.xdata.has_valid_instruction_c_condition()
+
+    def get_instruction_c_condition(self) -> "XXpr":
+        return self.xdata.get_instruction_c_condition()
+
     @property
     def annotation(self) -> str:
         if self.xdata.is_bx_call:
@@ -89,8 +109,10 @@ def annotation(self) -> str:
             cx = (" (C: "
                   + (str(self.creturnval()) if self.has_creturnval() else "None")
                   + ")")
-            if self.is_ok:
+            if self.is_return_xxpr_ok:
                 return "return " + str(self.rreturnval()) + cx
+            elif self.is_return_xpr_ok:
+                return "return " + str(self.returnval()) + cx
             else:
                 return "Error value"
         else:
@@ -126,11 +148,20 @@ def is_return_instruction(self, xdata: InstrXData) -> bool:
         else:
             return False
 
+    def is_conditional_return_instruction(self, xdata: InstrXData) -> bool:
+        if self.is_return_instruction(xdata):
+            return xdata.has_instruction_condition()
+        return False
+
     def return_value(self, xdata: InstrXData) -> Optional[XXpr]:
         xd = ARMBranchExchangeXData(xdata)
-        if xd.has_creturnval():
-            if xd.is_ok:
+        if xd.has_return_xpr():
+            if xd.has_creturnval():
                 return xd.creturnval()
+            elif xd.is_return_xxpr_ok:
+                return xd.rreturnval()
+            elif xd.is_return_xpr_ok:
+                return xd.returnval()
             else:
                 chklogger.logger.warning(
                     "Return value is an error value")
@@ -174,6 +205,38 @@ def assembly_ast(
         """Need check for branch on LR, which should emit a return statement."""
         return []
 
+    def ast_condition_prov(
+            self,
+            astree: ASTInterface,
+            iaddr: str,
+            bytestring: str,
+            xdata: InstrXData,
+            reverse: bool
+    ) -> Tuple[Optional[AST.ASTExpr], Optional[AST.ASTExpr]]:
+
+        ll_astcond = self.ast_cc_expr(astree)
+
+        if xdata.has_instruction_condition():
+            xd = ARMBranchExchangeXData(xdata)
+            if xd.has_valid_instruction_c_condition():
+                pcond = xd.get_instruction_c_condition()
+            else:
+                pcond = xd.get_instruction_condition()
+            hl_astcond = XU.xxpr_to_ast_def_expr(pcond, xdata, iaddr, astree)
+
+            astree.add_expr_mapping(hl_astcond, ll_astcond)
+            astree.add_expr_reachingdefs(hl_astcond, xdata.reachingdefs)
+            astree.add_flag_expr_reachingdefs(ll_astcond, xdata.flag_reachingdefs)
+            astree.add_condition_address(ll_astcond, [iaddr])
+
+            return (hl_astcond, ll_astcond)
+
+        else:
+            chklogger.logger.error(
+                "No condition found at address %s", iaddr)
+            hl_astcond = astree.mk_temp_lval_expression()
+            return (hl_astcond, ll_astcond)
+
     def ast_prov(
             self,
             astree: ASTInterface,