astprov conversion for result types

Author: sipma

chb/app/CHVersion.py

@@ -1 +1 @@
-chbversion: str = "0.3.0-20250210"
+chbversion: str = "0.3.0-20250308"

chb/arm/ARMCallOpcode.py

@@ -240,7 +240,12 @@ def ast_call_prov(
             ctinfo = finfo.call_target_info(iaddr)
             ftype = ctinfo.target_interface.bctype
             if ftype is not None:
-                astfntype = ftype.convert(astree.typconverter)
+                try:
+                    astfntype = ftype.convert(astree.typconverter)
+                except UF.CHBError as e:
+                    chklogger.logger.warning(
+                        "Type conversion of function type was unsuccessful: %s",
+                        str(e))
 
             if xdata.is_bx_call:
                 # indirect call

chb/arm/opcodes/ARMBranch.py

@@ -90,14 +90,29 @@ def xtgt(self) -> "XXpr":
         index = 1 if self.is_unconditional else 4
         return self.xpr(index, "xtgt")
 
+    @property
+    def is_xtgt_known(self) -> bool:
+        index = 1 if self.is_unconditional else 4
+        return self.xdata.xprs_r[index] is not None
+
     @property
     def annotation(self) -> str:
-        if self._xdata.has_branch_conditions():
-            return "if " + str(self.tcond) + " then goto " + str(self.xtgt)
-        elif self.is_unconditional:
-            return "goto " + str(self.xtgt)
+        if self.is_ok:
+            if self._xdata.has_branch_conditions():
+                return "if " + str(self.tcond) + " then goto " + str(self.xtgt)
+            elif self.is_unconditional:
+                return "goto " + str(self.xtgt)
+            else:
+                return "?"
+        elif self.is_xtgt_known:
+            if self._xdata.has_branch_conditions():
+                return "if " + str(self.txpr) + " then goto " + str(self.xtgt)
+            elif self.is_unconditional:
+                return "goto " + str(self.xtgt)
+            else:
+                return "?"
         else:
-            return "?"
+            return "Error value"
 
 
 @armregistry.register_tag("B", ARMOpcode)
@@ -151,7 +166,10 @@ def ft_conditions_basic(self, xdata: InstrXData) -> Sequence[XXpr]:
     def ft_conditions(self, xdata: InstrXData) -> Sequence[XXpr]:
         xd = ARMBranchXData(xdata)
         if xdata.has_branch_conditions():
-            return [xd.fcond, xd.tcond]
+            if xd.is_ok:
+                return [xd.fcond, xd.tcond]
+            else:
+                return [xd.fxpr, xd.txpr]
         else:
             return []
 
@@ -191,7 +209,7 @@ def annotation(self, xdata: InstrXData) -> str:
             else:
                 return xd.annotation
         else:
-            return "Error value"
+            return xd.annotation
 
     def target_expr_ast(
             self,
@@ -264,6 +282,8 @@ def default(condition: XXpr) -> AST.ASTExpr:
         # case there are no rewritten variables, but this still has to be
         # validated with more instances.
 
+        xd = ARMBranchXData(xdata)
+
         ftconds_basic = self.ft_conditions(xdata)
         ftconds = self.ft_conditions(xdata)
 

chb/arm/opcodes/ARMCompare.py

@@ -78,7 +78,8 @@ def result(self) -> "XXpr":
     @property
     def annotation(self) -> str:
         ann = "compare " + str(self.xrn) + " and " + str(self.xrm)
-        ann += " (" + str(self.result) + ")"
+        if self.is_ok:
+            ann += " (" + str(self.result) + ")"
         return self.add_instruction_condition(ann)
 
 
@@ -118,10 +119,7 @@ def opargs(self) -> List[ARMOperand]:
 
     def annotation(self, xdata: InstrXData) -> str:
         xd = ARMCompareXData(xdata)
-        if xd.is_ok:
-            return xd.annotation
-        else:
-            return "Error value"
+        return xd.annotation
 
     def ast_prov(
             self,
@@ -149,16 +147,17 @@ def ast_prov(
 
         # high-level assignment
 
-        xd = ARMCompareXData(xdata)
-        if not xd.is_ok:
-            chklogger.logger.error(
-                "Error value encountered at address %s", iaddr)
-            return ([], [])
-
-        rhs = xd.result
         rdefs = xdata.reachingdefs
-
-        hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree)
+        xd = ARMCompareXData(xdata)
+        if xd.is_ok:
+            rhs = xd.result
+            hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree)
+        else:
+            rhs1 = xd.xrn
+            rhs2 = xd.xrm
+            hl_rhs1 = XU.xxpr_to_ast_def_expr(rhs1, xdata, iaddr, astree)
+            hl_rhs2 = XU.xxpr_to_ast_def_expr(rhs2, xdata, iaddr, astree)
+            hl_rhs = astree.mk_binary_op("minus", hl_rhs1, hl_rhs2)
 
         hl_assign = astree.mk_assign(
             astree.ignoredlhs,

chb/arm/opcodes/ARMStoreMultipleIncrementAfter.py

@@ -104,6 +104,26 @@ def copysize(self) -> int:
         else:
             raise UF.CHBError("Not an ldmstm aggregate")
 
+    @property
+    def regcount(self) -> int:
+        return len(self.xdata.vars_r) - 1
+
+    @property
+    def baselhs(self) -> "XVariable":
+        return self.var(0, "baselhs")
+
+    @property
+    def is_baselhs_known(self) -> bool:
+        return self.xdata.vars_r[0] is not None
+
+    @property
+    def memlhss(self) -> List["XVariable"]:
+        return [self.var(i, "memlhs-" + str(i)) for i in range(1, self.regcount + 1)]
+
+    @property
+    def rhss(self) -> List["XXpr"]:
+        return [self.xpr(i, "rhs-" + str(i)) for i in range(3, self.regcount + 3)]
+
     @property
     def annotation(self) -> str:
         if self.is_ok:
@@ -117,7 +137,10 @@ def annotation(self) -> str:
                     + str(self.copysize)
                     + ")")
             else:
-                return "not yet supported"
+                assigns = []
+                for (memlhs, rhs) in zip(self.memlhss, self.rhss):
+                    assigns.append(str(memlhs) + " := " + str(rhs))
+                return "; ".join(assigns)
         else:
             if self.is_ldmstm_aggregate:
                 if self.is_xxdst_unknown and self.is_xxsrc_unknown:

chb/arm/opcodes/ARMStoreRegisterHalfword.py

@@ -97,7 +97,7 @@ def annotation(self) -> str:
         if self.is_ok:
             assignment = str(self.vmem) + " := " + str(self.xxrt)
         elif not self.is_xxrt_known:
-            assignment = "(*" + str(self.xaddr) + ") := Error value"
+            assignment = "(*" + str(self.xaddr) + ") := " + str(self.xrt)
         elif self.is_vmem_unknown and self.is_address_known:
             assignment = "*(" + str(self.xaddr) + ") := " + str(self.xxrt)
         else:

chb/invariants/XXprUtil.py

@@ -659,10 +659,11 @@ def vargument_deref_value_to_ast_lval_expression(
             elif tgttype.is_scalar and coff == 0:
                 return astree.mk_memref_expr(xinitarg, anonymous=anonymous)
 
-    chklogger.logger.error(
-        "AST conversion of argument deref value: %s with offset %s and type %s "
-        + "not yet handled at %s",
-        str(basevar), str(offset), str(argtype), iaddr)
+    if not anonymous:
+        chklogger.logger.error(
+            "AST conversion of argument deref value: %s with offset %s and type %s "
+            + "not yet handled at %s",
+            str(basevar), str(offset), str(argtype), iaddr)
 
     return astree.mk_temp_lval_expression()