ARM: astprov conversion for result types

Author: sipma

chb/app/CHVersion.py

@@ -1 +1 @@
-chbversion: str = "0.3.0-20241111"
+chbversion: str = "0.3.0-20250203"

chb/arm/opcodes/ARMAdd.py

@@ -353,8 +353,15 @@ def pointer_arithmetic_expr() -> AST.ASTExpr:
 
             chklogger.logger.error(
                 "Second operand pointer variable not yet supported for %s at "
-                + "address %s",
-                str(rhs3), iaddr)
+                + "address %s; rrhs1: %s; hl_rhs1: %s; hl_rhs2: %s; hl_rhs1_type: %s;"
+                + " hl_rhs2_type: %s",
+                str(rhs3),
+                iaddr,
+                str(rrhs1),
+                str(hl_rhs1),
+                str(hl_rhs2),
+                str(hl_rhs1_type),
+                str(hl_rhs2_type))
             return astree.mk_temp_lval_expression()
 
 
@@ -392,8 +399,14 @@ def pointer_arithmetic_expr() -> AST.ASTExpr:
 
         elif (hl_lhs_type is not None and hl_lhs_type.is_pointer):
             hl_rhs = pointer_arithmetic_expr()
-            if rhs3.is_constant_expression:
-                astree.set_ssa_value(str(hl_lhs), hl_rhs)
+            if str(hl_rhs).startswith("astmem_tmp"):
+                chklogger.logger.error(
+                    "Unable to compute pointer arithmetic expression for %s "
+                    "at address %s",
+                    str(rhs3), iaddr)
+            else:
+                if rhs3.is_constant_expression:
+                    astree.set_ssa_value(str(hl_lhs), hl_rhs)
 
         else:
             hl_rhs = XU.xxpr_to_ast_def_expr(rhs3, xdata, iaddr, astree)

chb/arm/opcodes/ARMStoreMultipleIncrementAfter.py

@@ -69,18 +69,34 @@ def ldmstm_xpr(self, index: int, msg: str) -> "XXpr":
     def xdst(self) -> "XXpr":
         return self.ldmstm_xpr(0, "xdst")
 
+    @property
+    def is_xdst_unknown(self) -> bool:
+        return self.xdata.xprs_r[0] is None
+
     @property
     def xsrc(self) -> "XXpr":
         return self.ldmstm_xpr(1, "xsrc")
 
+    @property
+    def is_xsrc_unknowns(self) -> bool:
+        return self.xdata.xprs_r[1] is None
+
     @property
     def xxdst(self) -> "XXpr":
         return self.ldmstm_xpr(2, "xxdst")
 
+    @property
+    def is_xxdst_unknown(self) -> bool:
+        return self.xdata.xprs_r[2] is None
+
     @property
     def xxsrc(self) -> "XXpr":
         return self.ldmstm_xpr(3, "xxsrc")
 
+    @property
+    def is_xxsrc_unknown(self) -> bool:
+        return self.xdata.xprs_r[3] is None
+
     @property
     def copysize(self) -> int:
         if self.is_ldmstm_aggregate:
@@ -90,17 +106,39 @@ def copysize(self) -> int:
 
     @property
     def annotation(self) -> str:
-        if self.is_ldmstm_aggregate:
-            return (
-                "memcpy(" +
-                str(self.xxdst)
-                + ", "
-                + str(self.xxsrc)
-                + ", "
-                + str(self.copysize)
-                + ")")
+        if self.is_ok:
+            if self.is_ldmstm_aggregate:
+                return (
+                    "memcpy(" +
+                    str(self.xxdst)
+                    + ", "
+                    + str(self.xxsrc)
+                    + ", "
+                    + str(self.copysize)
+                    + ")")
+            else:
+                return "not yet supported"
         else:
-            return "not yet supported"
+            if self.is_ldmstm_aggregate:
+                if self.is_xxdst_unknown and self.is_xxsrc_unknown:
+                    dst = str(self.xdst)
+                    src = str(self.xsrc)
+                elif self.is_xxdst_unknown:
+                    dst = str(self.xdst)
+                    src = str(self.xxsrc)
+                else:
+                    dst = str(self.xxdst)
+                    src = str(self.xsrc)
+                return (
+                        "memcpy("
+                        + dst
+                        + ", "
+                        + src
+                        + ", "
+                        + str(self.copysize)
+                        + ")")
+            else:
+                return "not yet supported"
 
 
 
@@ -166,10 +204,7 @@ def is_store_instruction(self, xdata: InstrXData) -> bool:
 
     def annotation(self, xdata: InstrXData) -> str:
         xd = ARMStoreMultipleIncrementAfterXData(xdata)
-        if xd.is_ok:
-            return xd.annotation
-        else:
-            return "Error value"
+        return xd.annotation
 
     def ast_prov_ldmstmcopy(
             self,
@@ -232,8 +267,13 @@ def ast_prov_ldmstmcopy(
 
         xd = ARMStoreMultipleIncrementAfterXData(xdata)
         if not xd.is_ok:
-            chklogger.logger.error(
-                "Encountered error value at address %s", iaddr)
+            if xd.is_xxsrc_unknown and xd.is_xxdst_unknown:
+                chklogger.logger.error(
+                    "LDM-STM-memcpy: (%s): src and dst unknown", iaddr)
+            elif xd.is_xxsrc_unknown:
+                chklogger.logger.error("LDM-STM-memcpy: (%s): src unknown", iaddr)
+            else:
+                chklogger.logger.error("LDM-STM-memcpy: (%s): dst unknown", iaddr)
             return ([], [])
 
         xdst = xd.xdst

chb/arm/opcodes/ARMUnsignedExtendHalfword.py

@@ -197,4 +197,9 @@ def ast_prov(
         astree.add_lval_defuses(hl_lhs, defuses[0])
         astree.add_lval_defuses_high(hl_lhs, defuseshigh[0])
 
+        if astree.has_register_variable_intro(iaddr):
+            rvintro = astree.get_register_variable_intro(iaddr)
+            if rvintro.has_cast():
+                astree.add_expose_instruction(hl_assign.instrid)
+
         return ([hl_assign], [ll_assign])

chb/astinterface/ASTICodeTransformer.py

@@ -105,7 +105,7 @@ def transform_instruction_sequence_stmt(
                         "Transfor [%s]: global lhs", str(instr))
                     instrs.append(instr)
                 else:
-                    chklogger.logger.debug("Transform [%s]: remove", str(instr))
+                    chklogger.logger.info("Transform [%s]: remove", str(instr))
             else:
                 instrs.append(instr)
         return self.astinterface.mk_instr_sequence(

chb/astinterface/ASTInterface.py

@@ -62,7 +62,8 @@
 from chb.astinterface.ASTIProvenance import ASTIProvenance
 import chb.astinterface.ASTIUtil as AU
 
-from chb.userdata.UserHints import FunctionAnnotation, RegisterVarIntro
+from chb.userdata.UserHints import (
+    FunctionAnnotation, RegisterVarIntro, StackVarIntro)
 
 import chb.util.fileutil as UF
 from chb.util.loggingutil import chklogger
@@ -302,13 +303,16 @@ def get_register_variable_intro(self, iaddr: str) -> RegisterVarIntro:
         raise UF.CHBError("No function annotation found")
 
     def has_stack_variable_intro(self, offset: int) -> bool:
-        return offset in self.stackvarintros
+        fnannotation = self.function_annotation
+        if fnannotation is not None:
+            return fnannotation.has_stack_variable_introduction(offset)
+        return False
 
-    def get_stack_variable_intro(self, offset: int) -> str:
-        if self.has_stack_variable_intro(offset):
-            return self.stackvarintros[offset]
-        else:
-            raise UF.CHBError("No stack-variable intro found for " + str(offset))
+    def get_stack_variable_intro(self, offset: int) -> StackVarIntro:
+        fnannotation = self.function_annotation
+        if fnannotation is not None:
+            return fnannotation.get_stack_variable_introduction(offset)
+        raise UF.CHBError("No function annotation found")
 
     def set_available_expressions(
             self, aexprs: Dict[str, Dict[str, Tuple[int, int, str]]]) -> None:
@@ -1095,13 +1099,15 @@ def mk_stack_variable_lval(
             return self.stack_variables[offset]
 
         # create a new stack variable
-        if offset in self.stackvarintros:
-            vname = self.stackvarintros[offset]
+        if self.has_stack_variable_intro(offset):
+            svintro = self.get_stack_variable_intro(offset)
+            vname = svintro.name
         else:
             if offset < 0:
                 vname = "localstackvar_" + str(-offset)
             else:
                 vname = "stack_" + str(offset)
+
         size: Optional[int] = None
         if vtype is not None:
             size = self.type_size_in_bytes(vtype)

chb/invariants/VAssemblyVariable.py

@@ -330,6 +330,8 @@ def __str__(self) -> str:
         elif self.is_realigned_stack_variable:
             offset = self.offset.offsetvalue()
             return 'varr.' + '{0:04d}'.format(offset)
+        elif self.offset.is_no_offset:
+            return "*" + str(self.base)
         return str(str(self.base)) + '[' + str(self.offset) + ']'
 
 

chb/invariants/VConstantValueVariable.py

@@ -6,7 +6,7 @@
 #
 # Copyright (c) 2016-2020 Kestrel Technology LLC
 # Copyright (c) 2020      Henny Sipma
-# Copyright (c) 2021-2024 Aarno Labs LLC
+# Copyright (c) 2021-2025 Aarno Labs LLC
 #
 # Permission is hereby granted, free of charge, to any person obtaining a copy
 # of this software and associated documentation files (the "Software"), to deal
@@ -197,7 +197,10 @@ def variable(self) -> "XVariable":
 
     @property
     def register(self) -> "Register":
-        raise UF.CHBError("Constant value is not an initial register value")
+        raise UF.CHBError(
+            "Constant value is not an initial register value: "
+            + str(self)
+            + " (" + self.tags[0] + ")")
 
     def argument_deref_arg_offset(self, inbytes: bool = False) -> Tuple[int, int]:
         raise UF.CHBError("argument_deref_arg_offset not supported on "
@@ -372,7 +375,9 @@ def is_function_return_deref_value(self) -> bool:
         if avar.is_memory_variable and avar.is_basevar_variable:
             xbasevar = avar.basevar
             offset = avar.offset
-            return xbasevar.is_function_return_value and offset.is_constant_offset
+            return (
+                xbasevar.is_function_return_value
+                and (offset.is_constant_offset or offset.is_no_offset))
         else:
             return False
 
@@ -595,7 +600,7 @@ def register(self) -> Register:
         return self.bd.register(self.args[1])
 
     def __str__(self) -> str:
-        return self.name
+        return self.name + "(" + self.iaddr + ", " + str(self.tgttype) + ")"
 
 
 @varregistry.register_tag("fp", VConstantValueVariable)

chb/invariants/XXprUtil.py

@@ -149,7 +149,7 @@ def xconstant_to_ast_expr(
             gvaddrtype = gvaddr.ctype(astree.ctyper)
             if gvaddrtype is not None and gvaddrtype.is_array:
                 # array already is an address
-                return astree.mk_lval_expr(lval)
+                return astree.mk_start_of(lval)
             else:
                 return astree.mk_address_of(lval)
         else:
@@ -259,7 +259,7 @@ def vreturn_deref_value_to_ast_lval_expression(
         astree: ASTInterface,
         anonymous: bool = False) -> AST.ASTExpr:
 
-    if not offset.is_constant_value_offset:
+    if not (offset.is_constant_value_offset or offset.is_no_offset):
         chklogger.logger.error(
             "Non-constant offset: %s not yet supported at address %s",
             str(offset), iaddr)
@@ -669,7 +669,7 @@ def vinitmemory_value_to_ast_lval_expression(
 
     if avar.is_memory_variable and avar.is_basevar_variable:
         avar = cast("VMemoryVariable", avar)
-        if not avar.offset.is_constant_value_offset:
+        if not (avar.offset.is_constant_value_offset or avar.offset.is_no_offset):
             chklogger.logger.error(
                 "Non-constant offset: %s not yet supported at address %s",
                 str(avar.offset), iaddr)
@@ -852,6 +852,8 @@ def xvariable_to_ast_def_lval_expression(
             return astree.mk_temp_lval_expression()
 
         else:
+            chklogger.logger.error(
+                "No rdefs found for %s at address %s", str(reg), iaddr)
             return astree.mk_temp_lval_expression()
 
     if xvar.is_global_variable:
@@ -890,7 +892,17 @@ def xvariable_to_ast_def_lval_expression(
         return astree.mk_vinfo_lval_expression(vinfo, anonymous=anonymous)
 
     if xvar.is_typecast_value:
-        tcvar = cast("VTypeCastValue", xvar.denotation)
+        tcvar = cast("VTypeCastValue", xvar.denotation.auxvar)
+        variaddr = tcvar.iaddr
+        varreg = tcvar.register
+        if variaddr in astree.ssa_intros and str(varreg) in astree.ssa_intros[variaddr]:
+            vinfo = astree.ssa_intros[variaddr][str(varreg)]
+            ssavalue = astree.get_ssa_value(vinfo.vname)
+            if ssavalue is not None:
+                return ssavalue
+            else:
+                return astree.mk_vinfo_lval_expression(
+                    vinfo, anonymous=anonymous)
         chklogger.logger.error(
             "AST def conversion of typecast value %s to lval at address %s "
             + "not yet supported",
@@ -1755,19 +1767,32 @@ def vargument_deref_value_to_ast_lval(
         anonymous: bool = False) -> AST.ASTLval:
 
     if offset.is_no_offset:
-        asmvar = cast("VAuxiliaryVariable", basevar.denotation)
-        vinitvar = cast("VInitialRegisterValue", asmvar.auxvar)
-        xinitarg = vinitregister_value_to_ast_lval_expression(
-            vinitvar, xdata, iaddr, astree, anonymous=anonymous)
-        argtype = xinitarg.ctype(astree.ctyper)
-        if argtype is None:
-            chklogger.logger.error(
-                "Untyped dereferenced argument value %s not yet supported at "
-                + "address %s",
-                str(xinitarg), iaddr)
-            return astree.mk_temp_lval()
-        else:
-            return astree.mk_memref_lval(xinitarg, anonymous=anonymous)
+        if basevar.is_initial_register_value:
+            asmvar = cast("VAuxiliaryVariable", basevar.denotation)
+            vinitvar = cast("VInitialRegisterValue", asmvar.auxvar)
+            xinitarg = vinitregister_value_to_ast_lval_expression(
+                vinitvar, xdata, iaddr, astree, anonymous=anonymous)
+            argtype = xinitarg.ctype(astree.ctyper)
+            if argtype is None:
+                chklogger.logger.error(
+                    "Untyped dereferenced argument value %s not yet supported at "
+                    + "address %s",
+                    str(xinitarg), iaddr)
+                return astree.mk_temp_lval()
+            else:
+                return astree.mk_memref_lval(xinitarg, anonymous=anonymous)
+
+        if basevar.is_function_return_value:
+            asmvar = cast("VAuxiliaryVariable", basevar.denotation)
+            frvinitrvar = cast("VFunctionReturnValue", asmvar.auxvar)
+            callsite = frvinitrvar.callsite
+            if callsite in astree.ssa_intros:
+                if len(astree.ssa_intros[callsite]) == 1:
+                    vinfo = list(astree.ssa_intros[callsite].values())[0]
+                    vtype = vinfo.vtype
+                    vexpr = astree.mk_vinfo_lval_expression(
+                        vinfo, anonymous=anonymous)
+                    return astree.mk_memref_lval(vexpr, anonymous=anonymous)
 
     if not offset.is_constant_value_offset:
         chklogger.logger.error(
@@ -1977,6 +2002,7 @@ def xmemory_dereference_lval(
         anonymous: bool = False) -> AST.ASTLval:
 
     xaddr = xxpr_to_ast_def_expr(address, xdata, iaddr, astree)
+
     if xaddr.is_ast_binary_op:
         xaddr = cast(AST.ASTBinaryOp, xaddr)
         if xaddr.exp1.is_ast_startof: