ARM: additional astprov handling

Author: sipma

chb/app/CHVersion.py

@@ -1 +1 @@
-chbversion: str = "0.3.0-20250312"
+chbversion: str = "0.3.0-20250313"

chb/arm/opcodes/ARMMove.py

@@ -237,4 +237,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/ast/ASTCPrettyPrinter.py

@@ -185,7 +185,8 @@ def write_global_declarations(self) -> None:
                 continue
             self.ccode.newline(indent=self.indent)
             if vinfo.vtype is None:
-                self.ccode.write("? " + vinfo.vname + ";")
+                self.ccode.write("int " + vinfo.vname + ";")
+                self.ccode.write("  // no type available; int inserted here")
                 continue
 
             if vinfo.vtype.is_function:

chb/invariants/XXprUtil.py

@@ -656,9 +656,25 @@ def vargument_deref_value_to_ast_lval_expression(
                     astree,
                     anonymous=anonymous)
 
-            elif tgttype.is_scalar and coff == 0:
+            if tgttype.is_pointer:
+                ioff = coff // 4
+                aoff = astree.mk_scalar_index_offset(ioff)
+                if xinitarg.is_ast_lval_expr:
+                    xinitarg = cast(AST.ASTLvalExpr, xinitarg)
+                    lhost = xinitarg.lval.lhost
+                    lval = astree.mk_lval(lhost, offset=aoff, anonymous=anonymous)
+                    return astree.mk_lval_expression(lval, anonymous=anonymous)
+
+            if tgttype.is_scalar and coff == 0:
                 return astree.mk_memref_expr(xinitarg, anonymous=anonymous)
 
+        if not anonymous:
+            chklogger.logger.error(
+                "AST conversion of initial register deref value: %s with offset %s "
+                + "and type %s not yet handled at %s",
+                str(xinitarg), str(coff), str(argtype), iaddr)
+        return astree.mk_temp_lval_expression()
+
     if not anonymous:
         chklogger.logger.error(
             "AST conversion of argument deref value: %s with offset %s and type %s "
@@ -1122,17 +1138,15 @@ def default() -> AST.ASTExpr:
         astxpr2 = xxpr_to_ast_expr(xpr2, xdata, iaddr, astree, anonymous=anonymous)
         if operator in ["plus", "minus"]:
             ty1 = astxpr1.ctype(astree.ctyper)
-            if ty1 is not None:
-                if ty1.is_pointer:
-                    return mk_xpointer_expr(
-                        operator,
-                        astxpr1,
-                        cast(AST.ASTTypPtr, ty1),
-                        astxpr2,
-                        iaddr,
-                        astree,
-                        anonymous=anonymous)
-                return astree.mk_binary_expression(operator, astxpr1, astxpr2)
+            if ty1 is not None and ty1.is_pointer:
+                return mk_xpointer_expr(
+                    operator,
+                    astxpr1,
+                    cast(AST.ASTTypPtr, ty1),
+                    astxpr2,
+                    iaddr,
+                    astree,
+                    anonymous=anonymous)
             else:
                 return default()
         else: