AST: improve on memory variable resolution

Author: sipma

chb/app/CHVersion.py

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

chb/arm/opcodes/ARMAdd.py

@@ -407,7 +407,6 @@ def pointer_arithmetic_expr() -> AST.ASTExpr:
             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/ARMStoreRegister.py

@@ -69,6 +69,18 @@ def vmem(self) -> "XVariable":
     def is_vmem_unknown(self) -> bool:
         return self.xdata.vars_r[0] is None
 
+    @property
+    def lhsvar(self) -> "XVariable":
+        return self.var(1, "lhsvar")
+
+    @property
+    def is_lhsvar_unknown(self) -> bool:
+        return self.xdata.vars_r[1] is None
+
+    @property
+    def is_lhsvar_known(self) -> bool:
+        return self.xdata.vars_r[1] is not None
+
     @property
     def vrn(self) -> "XVariable":
         return self.var(1, "vrn")
@@ -234,6 +246,12 @@ def ast_prov(
             hl_lhs = XU.xvariable_to_ast_lval(
                 lhs, xdata, iaddr, astree, memaddr=memaddr)
 
+        elif xd.is_vmem_unknown and xd.is_lhsvar_known and xd.is_address_known:
+            memaddr = xd.xaddr
+            lhsvar = xd.lhsvar
+            hl_lhs = XU.xvariable_to_ast_lval(
+                lhsvar, xdata, iaddr, astree, memaddr=memaddr)
+
         elif xd.is_vmem_unknown and xd.is_address_known:
             memaddr = xd.xaddr
             hl_lhs = XU.xmemory_dereference_lval(memaddr, xdata, iaddr, astree)
@@ -245,6 +263,11 @@ def ast_prov(
                 iaddr)
             return ([], [])
 
+        if xd.is_vmem_unknown:
+            vmem = "unknown"
+        else:
+            vmem = str(xd.vmem)
+
         rhs = xd.xxrt
         rdefs = xdata.reachingdefs
         defuses = xdata.defuses

chb/arm/opcodes/ARMStoreRegisterByte.py

@@ -64,6 +64,18 @@ def vmem(self) -> "XVariable":
     def is_vmem_unknown(self) -> bool:
         return self.xdata.vars_r[0] is None
 
+    @property
+    def lhsvar(self) -> "XVariable":
+        return self.var(1, "lhsvar")
+
+    @property
+    def is_lhsvar_unknown(self) -> bool:
+        return self.xdata.vars_r[1] is None
+
+    @property
+    def is_lhsvar_known(self) -> bool:
+        return self.xdata.vars_r[1] is not None
+
     @property
     def xrn(self) -> "XXpr":
         return self.xpr(0, "xrn")
@@ -188,11 +200,17 @@ def ast_prov(
         xd = ARMStoreRegisterByteXData(xdata)
 
         if xd.is_ok:
-            lhs = xd.vmem
+            lhs = xd.lhsvar
             memaddr = xd.xaddr
             hl_lhs = XU.xvariable_to_ast_lval(
                 lhs, xdata, iaddr, astree, memaddr=memaddr)
 
+        elif xd.is_vmem_unknown and xd.is_lhsvar_known and xd.is_address_known:
+            memaddr = xd.xaddr
+            lhsvar = xd.lhsvar
+            hl_lhs = XU.xvariable_to_ast_lval(
+                lhsvar, xdata, iaddr, astree, memaddr=memaddr)
+
         elif xd.is_vmem_unknown and xd.is_address_known:
             memaddr = xd.xaddr
             hl_lhs = XU.xmemory_dereference_lval(memaddr, xdata, iaddr, astree)

chb/ast/ASTCPrettyPrinter.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2022-2024  Aarno Labs LLC
+# Copyright (c) 2022-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
@@ -463,7 +463,7 @@ def visit_asm_instr(self, instr: AST.ASTAsm) -> None:
     def visit_lval(self, lval: AST.ASTLval) -> None:
         if lval.lhost.is_memref:
             memexp = cast(AST.ASTMemRef, lval.lhost).memexp
-            if lval.offset.is_field_offset:
+            if lval.offset.is_field_offset and not memexp.is_ast_addressof:
                 fieldname = cast(AST.ASTFieldOffset, lval.offset).fieldname
                 suboffset = cast(AST.ASTFieldOffset, lval.offset).offset
                 memexp.accept(self)
@@ -488,9 +488,13 @@ def visit_variable(self, var: AST.ASTVariable) -> None:
         self.ccode.write(var.vname)
 
     def visit_memref(self, memref: AST.ASTMemRef) -> None:
-        self.ccode.write("(*(")
-        memref.memexp.accept(self)
-        self.ccode.write("))")
+        if memref.memexp.is_ast_addressof:
+            memexp = cast(AST.ASTAddressOf, memref.memexp)
+            memexp.lval.accept(self)
+        else:
+            self.ccode.write("(*(")
+            memref.memexp.accept(self)
+            self.ccode.write("))")
 
     def visit_no_offset(self, offset: AST.ASTNoOffset) -> None:
         pass

chb/cmdline/PatchResults.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2023-2024  Aarno Labs, LLC
+# Copyright (c) 2023-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
@@ -409,6 +409,8 @@ def events(self) -> List[PatchEvent]:
         if self._events is None:
             self._events = []
             for de in self._d["events"]:
+                if de["category"] == "failure":
+                    continue
                 self._events.append(PatchEvent(de))
         return self._events
 

chb/invariants/XXpr.py

@@ -6,7 +6,7 @@
 #
 # Copyright (c) 2016-2020 Kestrel Technology LLC
 # Copyright (c) 2020-2021 Henny B. 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
@@ -766,19 +766,28 @@ def is_stack_address(self) -> bool:
         args = self.operands
         if len(args) == 2:
             return (args[0].is_stack_base_address and args[1].is_constant)
+        elif self.is_addressof_var:
+            xvar = self.get_addressof_var
+            return xvar is not None and xvar.is_local_stack_variable
         else:
             return False
 
     def stack_address_offset(self) -> int:
-        if self.is_stack_address:
+        if self.is_stack_address and len(self.operands) == 2:
+            # explicit stack address
             stackoffset = self.operands[1]
             if self.operator == 'minus':
                 return stackoffset.negated_value()
             else:
                 return stackoffset.intvalue
-        else:
-            raise UF.CHBError(
-                "Expression is not a stack address: " + str(self))
+
+        elif self.is_stack_address and self.is_addressof_var:
+            xvar = self.get_addressof_var
+            if xvar is not None:
+                return xvar.denotation.offset.offsetvalue()
+
+        raise UF.CHBError(
+            "Expression is not a stack address: " + str(self))
 
     @property
     def is_heap_address(self) -> bool:

chb/invariants/XXprUtil.py

@@ -1035,7 +1035,7 @@ def default() -> AST.ASTExpr:
 
     cst2 = cast(AST.ASTIntegerConstant, axpr2).cvalue
 
-    if not axpr1.is_ast_lval_expr:
+    if not (axpr1.is_ast_lval_expr or axpr1.is_ast_addressof):
         chklogger.logger.warning(
             "AST def conversion of pointer expression encountered unexpected "
             + " base expression %s at address %s",