XXPR: add support for baseptr array index offset

Author: sipma

chb/app/CHVersion.py

@@ -1 +1 @@
-chbversion: str = "0.3.0-20250329"
+chbversion: str = "0.3.0-20250401"

chb/arm/opcodes/ARMStoreRegisterByte.py

@@ -278,6 +278,7 @@ def ast_prov(
             rhs = xd.xxrt
         else:
             rhs = xd.xrt
+
         hl_rhs = XU.xxpr_to_ast_def_expr(rhs, xdata, iaddr, astree)
 
         rdefs = xdata.reachingdefs

chb/astinterface/ASTICodeTransformer.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
@@ -85,28 +85,29 @@ def transform_instruction_sequence_stmt(
                         and not self.provenance.has_expose_instruction(instr.instrid)):
                     chklogger.logger.info(
                         "Remove [%s]: has ssa value", str(instr))
-                    continue
-                if self.provenance.has_active_lval_defuse_high(instr.lhs.lvalid):
-                    chklogger.logger.debug(
+                elif self.provenance.has_active_lval_defuse_high(instr.lhs.lvalid):
+                    chklogger.logger.info(
                         "Transform [%s]: active lval_defuse_high: %s",
                         str(instr),
                         self.provenance.active_lval_defuse_high(instr.lhs.lvalid))
                     instrs.append(instr)
                 elif self.provenance.has_lval_store(instr.lhs.lvalid):
-                    chklogger.logger.debug(
+                    chklogger.logger.info(
                         "Transform [%s]: lval_store", str(instr))
                     instrs.append(instr)
                 elif self.provenance.has_expose_instruction(instr.instrid):
                     chklogger.logger.info(
                         "Transform [%s]: expose instruction", str(instr))
                     instrs.append(instr)
                 elif instr.lhs.lhost.is_global:
-                    chklogger.logger.debug(
-                        "Transfor [%s]: global lhs", str(instr))
+                    chklogger.logger.info(
+                        "Transform [%s]: global lhs", str(instr))
                     instrs.append(instr)
                 else:
                     chklogger.logger.info("Transform [%s]: remove", str(instr))
             else:
+                chklogger.logger.info(
+                    "Transform [%s]: include by default", str(instr))
                 instrs.append(instr)
         return self.astinterface.mk_instr_sequence(
             instrs,

chb/cmdline/commandutil.py

@@ -638,21 +638,22 @@ def results_stats(args: argparse.Namespace) -> NoReturn:
         mode=logfilemode,
         msg="results stats invoked")
 
-    tags: Dict[str, List[str]] = {}
+    tagdata: Dict[str, Any] = {}
     if tagfile is not None:
         with open(tagfile, "r") as fp:
             tagdata = json.load(fp)
-        for (key, flist) in tagdata["keys"].items():
-            for faddr in flist:
-                tags.setdefault(faddr, [])
-                if not key in tags[faddr]:
-                    tags[faddr].append(key)
+
+    functiontags: Dict[str, List[str]] = {}
+
+    if "function-tags" in tagdata:
+        functiontags = tagdata["function-tags"]
 
     maxlen = 0
-    for (faddr, keys) in tags.items():
-        taglen = 4 + len(",".join(keys))
+    for (faddr, keys) in functiontags.items():
+        taglen = len(",".join(keys))
         if taglen > maxlen:
             maxlen = taglen
+    maxlen = maxlen + 4 if maxlen > 0 else 0
 
     xinfo = XI.XInfo()
     xinfo.load(path, xfile)
@@ -672,8 +673,8 @@ def results_stats(args: argparse.Namespace) -> NoReturn:
     else:
         sortkey = lambda f: int(f.faddr, 16)
     for f in sorted(stats.get_function_results(), key=sortkey):
-        if f.faddr in tags:
-            fn_tags = tags[f.faddr]
+        if f.faddr in functiontags:
+            fn_tags = functiontags[f.faddr]
         else:
             fn_tags = []
         if "hide" in fn_tags:

chb/invariants/VMemoryOffset.py

@@ -36,6 +36,7 @@
   | FieldOffset of string * int * memory_offset_t        "f"      2      2
   | IndexOffset of variable_t * int * memory_offset_t    "i"      1      3
   | ArrayIndexOffset of xpr_t * memory_offset_t          "a"      1      2
+  | BasePtrArrayIndexOffset of xpr_t * memory_offset_t   "p"      1      2
   | UnknownOffset                                        "u"      1      0
 
 """
@@ -84,6 +85,10 @@ def is_index_offset(self) -> bool:
     def is_array_index_offset(self) -> bool:
         return False
 
+    @property
+    def is_baseptr_array_index_offset(self) -> bool:
+        return False
+
     @property
     def is_no_offset(self) -> bool:
         return False
@@ -388,6 +393,39 @@ def __str__(self) -> str:
         return "[" + str(self.index_expression) + "]" + str(self.offset)
 
 
+@varregistry.register_tag("p", VMemoryOffset)
+class VMemoryOffsetBasePtrArrayIndexOffset(VMemoryOffset):
+    """Array index offset
+
+    args[0]: index of index expression in xprdictionary
+    args[1]: index of next-level offset in vardictionary
+    """
+
+    def __init__(
+            self,
+            vd: "FnVarDictionary",
+            ixval: IndexedTableValue) -> None:
+        VMemoryOffset.__init__(self, vd, ixval)
+
+    @property
+    def index_expression(self) -> "XXpr":
+        return self.xd.xpr(self.args[0])
+
+    @property
+    def offset(self) -> VMemoryOffset:
+        return self.vd.memory_offset(self.args[1])
+
+    @property
+    def is_baseptr_array_index_offset(self) -> bool:
+        return True
+
+    def has_no_offset(self) -> bool:
+        return self.offset.is_no_offset
+
+    def __str__(self) -> str:
+        return "[" + str(self.index_expression) + "]" + str(self.offset)
+
+
 @varregistry.register_tag("u", VMemoryOffset)
 class VMemoryOffsetUnknown(VMemoryOffset):
 

chb/invariants/XXprUtil.py

@@ -122,6 +122,7 @@
         VMemoryOffsetConstantOffset,
         VMemoryOffsetFieldOffset,
         VMemoryOffsetArrayIndexOffset,
+        VMemoryOffsetBasePtrArrayIndexOffset,
         VMemoryOffsetIndexOffset)
     from chb.mips.MIPSRegister import MIPSRegister
 
@@ -437,7 +438,10 @@ def memory_variable_to_lval_expression(
             return astree.mk_memref_expr(
                 astbase, offset=astoffset, anonymous=anonymous)
 
-        else:
+        elif (
+                offset.is_field_offset
+                or offset.is_array_index_offset
+                or offset.is_constant_value_offset):
             astlval = xvariable_to_ast_def_lval_expression(
                 base.basevar, xdata, iaddr, astree, anonymous=anonymous)
             if offset.is_field_offset:
@@ -451,10 +455,27 @@ def memory_variable_to_lval_expression(
             elif offset.is_constant_value_offset:
                 astoffset = astree.mk_scalar_index_offset(offset.offsetvalue())
             else:
+                chklogger.logger.warning(
+                    "Offset %s not yet handled at address %s",
+                    str(offset), iaddr)
                 astoffset = nooffset
             return astree.mk_memref_expr(
                 astlval, offset=astoffset, anonymous=anonymous)
 
+        elif offset.is_baseptr_array_index_offset:
+            astlval = xvariable_to_ast_def_lval_expression(
+                base.basevar, xdata, iaddr, astree, anonymous=anonymous)
+            offset = cast("VMemoryOffsetBasePtrArrayIndexOffset", offset)
+            (ptroffset, astoffset) = base_ptr_array_offset_to_ast_offset(
+                offset, xdata, iaddr, astree, anonymous=anonymous)
+            if ptroffset.is_integer_constant_zero:
+                return astree.mk_memref_expr(
+                    astlval, offset=astoffset, anonymous=anonymous)
+            else:
+                ptrexpr = astree.mk_binary_op("plus", ptroffset, astlval)
+                return astree.mk_memref_expr(
+                    ptrexpr, offset=astoffset, anonymous=anonymous)
+
     name = str(base)
 
     if not astree.globalsymboltable.has_symbol(name):
@@ -1499,6 +1520,25 @@ def stack_variable_to_ast_lval(
     return astree.mk_temp_lval()
 
 
+def base_ptr_array_offset_to_ast_offset(
+        offset: "VMemoryOffsetBasePtrArrayIndexOffset",
+        xdata: "InstrXData",
+        iaddr: str,
+        astree: ASTInterface,
+        anonymous: bool = False) -> Tuple[AST.ASTExpr, AST.ASTOffset]:
+
+    indexxpr = xxpr_to_ast_def_expr(
+        offset.index_expression, xdata, iaddr, astree, anonymous=anonymous)
+
+    if offset.has_no_offset() and indexxpr.is_integer_constant:
+        return (indexxpr, nooffset)
+
+    chklogger.logger.error(
+        "Base ptr array offset %s not yet handled at address %s",
+        str(offset), iaddr)
+    return (astree.mk_integer_constant(0), nooffset)
+
+
 def array_offset_to_ast_offset(
         offset: "VMemoryOffsetArrayIndexOffset",
         xdata: "InstrXData",
@@ -1675,8 +1715,7 @@ def xvariable_to_ast_lval(
         if (
                 rhs is not None
                 and (rhs.is_constant
-                     or (rhs.is_constant_value_variable
-                         and not rhs.is_function_return_value))):
+                     or (rhs.is_constant_value_variable))):
             astrhs: Optional[AST.ASTExpr] = xxpr_to_ast_def_expr(
                 rhs, xdata, iaddr, astree, anonymous=anonymous)
         else: