AST: support for more expressive memory variable representation

Author: sipma

chb/app/CHVersion.py

@@ -1 +1 @@
-chbversion: str = "0.3.0-20240805"
+chbversion: str = "0.3.0-20240829"

chb/arm/opcodes/ARMLoadRegister.py

@@ -207,8 +207,8 @@ def ast_prov(
                 annotations=annotations)
             ll_assigns: List[AST.ASTInstruction] = [ll_assign, ll_addr_assign]
 
-            basereg = xdata.vars[1]
-            newaddr = xdata.xprs[4]
+            basereg = xdata.vars[2]
+            newaddr = xdata.xprs[5]
             hl_addr_lhs = XU.xvariable_to_ast_lval(basereg, xdata, iaddr, astree)
             hl_addr_rhs = XU.xxpr_to_ast_def_expr(newaddr, xdata, iaddr, astree)
 
@@ -220,6 +220,9 @@ def ast_prov(
                 annotations=annotations)
             hl_assigns: List[AST.ASTInstruction] = [hl_assign, hl_addr_assign]
 
+            # Note: work-around for deficiency in def-use propagation
+            astree.add_expose_instruction(hl_addr_assign.instrid)
+
             astree.add_instr_mapping(hl_addr_assign, ll_addr_assign)
             astree.add_instr_address(hl_addr_assign, [iaddr])
             astree.add_expr_mapping(hl_addr_rhs, ll_addr_rhs)

chb/invariants/VMemoryBase.py

@@ -85,6 +85,10 @@ def is_basevar(self) -> bool:
     def is_basearray(self) -> bool:
         return False
 
+    @property
+    def is_basestruct(self) -> bool:
+        return False
+
     @property
     def is_global(self) -> bool:
         return False
@@ -249,6 +253,46 @@ def __str__(self) -> str:
         return str(self.basearray)
 
 
+@varregistry.register_tag("s", VMemoryBase)
+class VMemoryBaseBaseStruct(VMemoryBase):
+    """Base struct address.
+
+    args[0]: index of variable in xprdictionary
+    args[1]: index of struct type in bcdictionary
+    """
+
+    def __init__(
+            self,
+            vd: "FnVarDictionary",
+            ixval: IndexedTableValue) -> None:
+        VMemoryBase.__init__(self, vd, ixval)
+
+    @property
+    def is_basestruct(self) -> bool:
+        return True
+
+    @property
+    def basestruct(self) -> "XVariable":
+        return self.xd.variable(self.args[0])
+
+    @property
+    def basetyp(self) -> "BCTyp":
+        return self.bcd.typ(self.args[1])
+
+    def to_json_result(self) -> JSONResult:
+        ptrvar = self.basestruct.to_json_result()
+        if ptrvar.is_ok:
+            content: Dict[str, Any] = {}
+            content["ptrvar"] = ptrvar.content
+            return JSONResult("memorybase", content, "ok")
+        else:
+            return JSONResult(
+                "memorybase", {}, "fail", "memorybase: " + str(ptrvar.reason))
+
+    def __str__(self) -> str:
+        return str(self.basestruct)
+
+
 @varregistry.register_tag("g", VMemoryBase)
 class VMemoryBaseGlobal(VMemoryBase):
 

chb/invariants/XXprUtil.py

@@ -49,7 +49,8 @@
     from chb.invariants.VConstantValueVariable import (
         VInitialRegisterValue, VInitialMemoryValue, VFunctionReturnValue,
         SymbolicValue, MemoryAddress)
-    from chb.invariants.VMemoryBase import VMemoryBaseBaseArray
+    from chb.invariants.VMemoryBase import (
+        VMemoryBase, VMemoryBaseBaseArray, VMemoryBaseBaseStruct)
     from chb.invariants.VMemoryOffset import (
         VMemoryOffset,
         VMemoryOffsetConstantOffset,
@@ -59,6 +60,16 @@
     from chb.mips.MIPSRegister import MIPSRegister
 
 
+def prdebug(
+        s: str, iaddr: Optional[str] = None, iaddrs: List[str] = []) -> None:
+    if iaddr is None:
+        print("DEBUG: " + s)
+    elif iaddr in iaddrs:
+        print("DEBUG: " + iaddr + ": " + s)
+    else:
+        None
+
+
 def is_struct_field_address(xpr: X.XXpr, astree: ASTInterface) -> bool:
     """Return true if the expression is the address of a known struct."""
 
@@ -254,6 +265,37 @@ def vreturn_deref_value_to_ast_lval_expression(
     return astree.mk_temp_lval_expression()
 
 
+def memory_variable_to_lval_expression(
+        base: "VMemoryBase",
+        offset: "VMemoryOffset",
+        xdata: "InstrXData",
+        iaddr: str,
+        astree: ASTInterface,
+        size: int = 4) -> AST.ASTExpr:
+
+    name = str(base)
+
+    if not astree.globalsymboltable.has_symbol(name):
+        chklogger.logger.error(
+            "AST conversion of memory variable %s not in global symbol "
+            + "table not yet supported at address %s",
+            name, iaddr)
+        return astree.mk_temp_lval_expression()
+
+    vinfo = astree.globalsymboltable.get_symbol(name)
+    if offset.is_field_offset:
+        offset = cast("VMemoryOffsetFieldOffset", offset)
+        astoffset = field_offset_to_ast_offset(offset, xdata, iaddr, astree)
+        return astree.mk_vinfo_lval_expression(vinfo, astoffset)
+
+    chklogger.logger.error(
+        "AST conversion of memory variable %s with other offset not yet "
+        + "supported at address %s",
+        name, iaddr)
+
+    return astree.mk_temp_lval_expression()
+
+
 def global_variable_to_lval_expression(
         offset: "VMemoryOffset",
         xdata: "InstrXData",
@@ -565,6 +607,11 @@ def xvariable_to_ast_def_lval_expression(
         return global_variable_to_lval_expression(
             memvar.offset, xdata, iaddr, astree)
 
+    if xvar.is_memory_variable:
+        memvar = cast("VMemoryVariable", xvar.denotation)
+        return memory_variable_to_lval_expression(
+            memvar.base, memvar.offset, xdata, iaddr, astree)
+
     if xvar.is_local_stack_variable:
         stackvar = cast("VMemoryVariable", xvar.denotation)
         offset = stackvar.offset.offsetvalue()
@@ -826,6 +873,7 @@ def default() -> AST.ASTExpr:
 
     if hl_addr.is_ast_lval_expr:
         hl_addr_type = hl_addr.ctype(astree.ctyper)
+
         if hl_addr_type is None:
             return default()
 
@@ -845,6 +893,11 @@ def default() -> AST.ASTExpr:
         else:
             return default()
 
+    if hl_addr.is_ast_addressof:
+        hl_addr = cast(AST.ASTAddressOf, hl_addr)
+        hl_lval = hl_addr.lval
+        return astree.mk_lval_expr(hl_lval)
+
     if hl_addr.is_ast_binary_op:
         hl_addr = cast(AST.ASTBinaryOp, hl_addr)
 
@@ -980,7 +1033,6 @@ def stack_variable_to_ast_lval(
 
 
 def array_offset_to_ast_offset(
-        elementtyp: AST.ASTTyp,
         offset: "VMemoryOffsetArrayIndexOffset",
         xdata: "InstrXData",
         iaddr: str,
@@ -1001,7 +1053,36 @@ def to_ast_offset(suboffset: "VMemoryOffset") -> AST.ASTOffset:
         else:
             return nooffset
 
-    return astree.mk_expr_index_offset(indexxpr, offset=to_ast_offset(offset.offset))
+    return astree.mk_expr_index_offset(
+        indexxpr, offset=to_ast_offset(offset.offset))
+
+
+def field_offset_to_ast_offset(
+        offset: "VMemoryOffsetFieldOffset",
+        xdata: "InstrXData",
+        iaddr: str,
+        astree: ASTInterface) -> AST.ASTOffset:
+
+    if offset.has_no_offset():
+        return astree.mk_field_offset(offset.fieldname, offset.ckey)
+
+    if offset.offset.is_field_offset:
+        fieldoffset = cast("VMemoryOffsetFieldOffset", offset.offset)
+        suboffset = field_offset_to_ast_offset(
+            fieldoffset, xdata, iaddr, astree)
+    elif offset.offset.is_array_index_offset:
+        arrayindexoffset = cast("VMemoryOffsetArrayIndexOffset", offset.offset)
+        suboffset = array_offset_to_ast_offset(
+            arrayindexoffset, xdata, iaddr, astree)
+    elif offset.offset.is_constant_value_offset:
+        suboffset = astree.mk_scalar_index_offset(offset.offset.offsetvalue())
+    else:
+        suboffset = nooffset
+
+    return astree.mk_field_offset(
+        offset.fieldname, offset.ckey, offset=suboffset)
+
+
 
 def array_variable_to_ast_lval(
         base: "MemoryAddress",
@@ -1035,7 +1116,6 @@ def array_variable_to_ast_lval(
         return astree.mk_temp_lval()
 
     astoffset = array_offset_to_ast_offset(
-        elementtyp,
         cast("VMemoryOffsetArrayIndexOffset", offset),
         xdata,
         iaddr,
@@ -1050,6 +1130,46 @@ def array_variable_to_ast_lval(
     return astree.mk_temp_lval()
 
 
+def struct_variable_to_ast_lval(
+        base: "MemoryAddress",
+        structtyp: AST.ASTTypComp,
+        offset: "VMemoryOffset",
+        xdata: "InstrXData",
+        iaddr: str,
+        astree: ASTInterface) -> AST.ASTLval:
+
+    name = base.name
+    if name is None:
+        chklogger.logger.error(
+            "AST conversion of struct variable at %s encountered nameless "
+            + "base %s",
+            str(iaddr), str(base))
+        return astree.mk_temp_lval()
+
+    if not astree.globalsymboltable.has_symbol(name):
+        chklogger.logger.error(
+            "AST conversion of memory address value %s not in global symbol "
+            + " table not yet supported at address %s",
+            str(name), iaddr)
+        return astree.mk_temp_lval()
+
+    vinfo = astree.globalsymboltable.get_symbol(name)
+    if not offset.is_field_offset:
+        chklogger.logger.error(
+            "AST conversion of struct variable expected to find field offset "
+            + "but found %s at address %s",
+            str(offset), iaddr)
+        return astree.mk_temp_lval()
+
+    astoffset = field_offset_to_ast_offset(
+        cast("VMemoryOffsetFieldOffset", offset),
+        xdata,
+        iaddr,
+        astree)
+
+    return astree.mk_vinfo_lval(vinfo, offset=astoffset)
+
+
 def global_variable_to_ast_lval(
         offset: "VMemoryOffset",
         xdata: "InstrXData",
@@ -1190,8 +1310,8 @@ def xvariable_to_ast_lval(
 
     elif (
             xv.is_memory_variable
-            and cast ("VMemoryVariable",
-                      xv.denotation).base.is_basearray):
+            and cast("VMemoryVariable",
+                     xv.denotation).base.is_basearray):
         xvmem = cast("VMemoryVariable", xv.denotation)
         base = cast("VMemoryBaseBaseArray", xvmem.base).basearray
         if not base.is_memory_address_value:
@@ -1209,6 +1329,27 @@ def xvariable_to_ast_lval(
             iaddr,
             astree)
 
+    elif (
+            xv.is_memory_variable
+            and cast("VMemoryVariable",
+                     xv.denotation).base.is_basestruct):
+        xvmem = cast ("VMemoryVariable", xv.denotation)
+        base = cast("VMemoryBaseBaseStruct", xvmem.base).basestruct
+        if not base.is_memory_address_value:
+            chklogger.logger.error(
+                "AST conversion of lval %s encountered invalie BaseStruct at %s",
+                str(xv), iaddr)
+            return astree.mk_temp_lval()
+        basevar = cast("MemoryAddress", base.denotation.auxvar)
+        basetyp = cast("VMemoryBaseBaseStruct", xvmem.base).basetyp.convert(astree.typconverter)
+        return struct_variable_to_ast_lval(
+            basevar,
+            cast(AST.ASTTypComp, basetyp),
+            xvmem.offset,
+            xdata,
+            iaddr,
+            astree)
+
     else:
         chklogger.logger.error(
             "AST conversion of lval %s at address %s not yet supported",