INV: add support for typecast values

Author: sipma

chb/arm/opcodes/ARMLoadRegister.py

@@ -230,13 +230,26 @@ def ast_prov(
         defuses = xdata.defuses
         defuseshigh = xdata.defuseshigh
 
+        def has_cast() -> bool:
+            return (
+                astree.has_register_variable_intro(iaddr)
+                and astree.get_register_variable_intro(iaddr).has_cast())
+
+        if has_cast():
+            lhstype = hl_lhs.ctype(astree.ctyper)
+            if lhstype is not None:
+                hl_rhs = astree.mk_cast_expr(lhstype, hl_rhs)
+
         hl_assign = astree.mk_assign(
             hl_lhs,
             hl_rhs,
             iaddr=iaddr,
             bytestring=bytestring,
             annotations=annotations)
 
+        if has_cast():
+            astree.add_expose_instruction(hl_assign.instrid)
+
         astree.add_instr_mapping(hl_assign, ll_assign)
         astree.add_instr_address(hl_assign, [iaddr])
         astree.add_expr_mapping(hl_rhs, ll_rhs)
@@ -316,6 +329,10 @@ def ast_prov(
             astree.add_lval_defuses(ll_addr_lhs, defuses[1])
             astree.add_lval_defuses_high(ll_addr_lhs, defuseshigh[1])
         else:
+            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)
             ll_assigns = [ll_assign]
             hl_assigns = [hl_assign]
 

chb/arm/opcodes/ARMLoadRegisterHalfword.py

@@ -199,6 +199,7 @@ def ast_prov(
 
         elif xd.is_xrmem_unknown and xd.is_address_known:
             xaddr = xd.xaddr
+            lhs = xd.vrt
             hl_lhs = XU.xvariable_to_ast_lval(lhs, xdata, iaddr, astree)
             hl_rhs = XU.xmemory_dereference_lval_expr(
                 xaddr, xdata, iaddr, astree, size=2)

chb/astinterface/ASTICodeTransformer.py

@@ -80,7 +80,9 @@ def transform_instruction_sequence_stmt(
         for instr in stmt.instructions:
             if instr.is_ast_assign:
                 instr = cast(AST.ASTAssign, instr)
-                if self.astinterface.has_ssa_value(str(instr.lhs)):
+                if (
+                        self.astinterface.has_ssa_value(str(instr.lhs))
+                        and not self.provenance.has_expose_instruction(instr.instrid)):
                     chklogger.logger.info(
                         "Remove [%s]: has ssa value", str(instr))
                     continue

chb/astinterface/ASTInterface.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# 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
@@ -62,6 +62,8 @@
 from chb.astinterface.ASTIProvenance import ASTIProvenance
 import chb.astinterface.ASTIUtil as AU
 
+from chb.userdata.UserHints import FunctionAnnotation, RegisterVarIntro
+
 import chb.util.fileutil as UF
 from chb.util.loggingutil import chklogger
 
@@ -98,6 +100,7 @@ def __init__(
             appsignature: Optional["AppFunctionSignature"] = None,
             rdeflocs: Dict[str, List[List[str]]] = {},
             varintros: Dict[str, str] = {},
+            functionannotation: Optional[FunctionAnnotation] = None,
             stackvarintros: Dict[int, str] = {},
             patchevents: Dict[str, "PatchEvent"] = {},
             verbose: bool = False) -> None:
@@ -106,6 +109,7 @@ def __init__(
         self._astprototype = astprototype
         self._appsignature = appsignature
         self._rdeflocs = rdeflocs
+        self._functionannotation = functionannotation
         self._varintros = varintros
         self._stackvarintros = stackvarintros
         self._patchevents = patchevents
@@ -152,10 +156,19 @@ def appsignature(self) -> Optional["AppFunctionSignature"]:
     def rdeflocs(self) -> Dict[str, List[List[str]]]:
         return self._rdeflocs
 
+    @property
+    def function_annotation(self) -> Optional[FunctionAnnotation]:
+        return self._functionannotation
+
+    def has_function_annotation(self) -> bool:
+        return self.function_annotation is not None
+
+    # deprecated
     @property
     def varintros(self) -> Dict[str, str]:
         return self._varintros
 
+    # deprecated
     @property
     def stackvarintros(self) -> Dict[int, str]:
         return self._stackvarintros
@@ -265,15 +278,29 @@ def add_local_vardefinition(
         self._localvardefinitions.setdefault(iaddr, {})
         self._localvardefinitions[iaddr][var] = expr
 
+    # deprecated
     def has_variable_intro(self, iaddr: str) -> bool:
         return iaddr in self.varintros
 
+    # deprecated
     def get_variable_intro(self, iaddr: str) -> str:
         if self.has_variable_intro(iaddr):
             return self.varintros[iaddr]
         else:
             raise UF.CHBError("No variable intro found for " + iaddr)
 
+    def has_register_variable_intro(self, iaddr: str) -> bool:
+        fnannotation = self.function_annotation
+        if fnannotation is not None:
+            return fnannotation.has_register_variable_introduction(iaddr)
+        return False
+
+    def get_register_variable_intro(self, iaddr: str) -> RegisterVarIntro:
+        fnannotation = self.function_annotation
+        if fnannotation is not None:
+            return fnannotation.get_register_variable_introduction(iaddr)
+        raise UF.CHBError("No function annotation found")
+
     def has_stack_variable_intro(self, offset: int) -> bool:
         return offset in self.stackvarintros
 
@@ -1014,8 +1041,8 @@ def mk_ssa_register_varinfo(
             return vinfo
 
         # create a new ssa variable
-        if iaddr in self.varintros:
-            vname = self.varintros[iaddr]
+        if self.has_register_variable_intro(iaddr):
+            vname = self.get_register_variable_intro(iaddr).name
         elif prefix is not None:
             self._ssa_prefix_counters.setdefault(prefix, 0)
             ssaid = self._ssa_prefix_counters[prefix]

chb/cmdline/astcmds.py

@@ -215,8 +215,8 @@ def buildast(args: argparse.Namespace) -> NoReturn:
     symbolicaddrs: Dict[str, str] = userhints.symbolic_addresses()
     revsymbolicaddrs = {v: k for (k, v) in symbolicaddrs.items()}
     revfunctionnames = userhints.rev_function_names()
-    varintros = userhints.variable_introductions()
-    stackvarintros = userhints.stack_variable_introductions()
+    varintros = userhints.variable_introductions()   # to be removed
+    stackvarintros = userhints.stack_variable_introductions()  # to be removed
 
     # library_targets = library_call_targets(app, functions)
 
@@ -324,6 +324,7 @@ def buildast(args: argparse.Namespace) -> NoReturn:
             fstackvarintros = {
                 -off: name
                 for (off, name) in stackvarintros.get(faddr, {}).items()}
+            functionannotation = userhints.function_annotation(faddr)
 
             astinterface = ASTInterface(
                 astree,
@@ -333,6 +334,7 @@ def buildast(args: argparse.Namespace) -> NoReturn:
                 astprototype=astprototype,
                 appsignature=appsignature,
                 varintros=varintros,
+                functionannotation=functionannotation,
                 stackvarintros=fstackvarintros,
                 patchevents=patchevents,
                 verbose=verbose)
@@ -341,7 +343,7 @@ def buildast(args: argparse.Namespace) -> NoReturn:
             # xdata records for all instructions in the function. Locations that
             # have a common user are merged. Types are provided by lhs_types.
             astinterface.introduce_ssa_variables(
-                f.rdef_locations(), f.lhs_types(), f.lhs_names)
+                f.rdef_locations(), f.register_lhs_types, f.lhs_names)
 
             # Introduce stack variables for all stack buffers with types
             astinterface.introduce_stack_variables(

chb/invariants/VConstantValueVariable.py

@@ -39,6 +39,11 @@
       * ctxt_iaddress_t
       * ctxt_iaddress_t
   | FunctionReturnValue  of ctxt_iaddress_t        "fr"       2      0
+  | TypeCastValue of                               "tc"       3      2
+     ctxt_iaddress_t
+     * string
+     * btype_t
+     * register_t
   | SyscallErrorReturnValue of ctxt_iaddress_t     "ev"       2      0
   | AugmentedValue of                              "av"       4      2
      variable_t
@@ -131,6 +136,10 @@ def is_global_value(self) -> bool:
     def is_function_return_value(self) -> bool:
         return False
 
+    @property
+    def is_typecast_value(self) -> bool:
+        return False
+
     @property
     def is_symbolic_value(self) -> bool:
         return False
@@ -549,6 +558,46 @@ def __str__(self) -> str:
             return "rtn_" + self.callsite
 
 
+@varregistry.register_tag("tc", VConstantValueVariable)
+class VTypeCastValue(VConstantValueVariable):
+    """Type cast of a register value.
+
+    tags[1]: address of cast
+    tags[2]: name of variable
+    args[0]: index of cast target type in bcdictionary
+    args[1]: index of register in bdictionary
+    """
+
+    def __init__(
+            self,
+            vd: "FnVarDictionary",
+            ixval: IndexedTableValue) -> None:
+        VConstantValueVariable.__init__(self, vd, ixval)
+
+    @property
+    def is_typecast_value(self) -> bool:
+        return True
+
+    @property
+    def iaddr(self) -> str:
+        return self.tags[1]
+
+    @property
+    def name(self) -> str:
+        return self.tags[2]
+
+    @property
+    def tgttype(self) -> "BCTyp":
+        return self.bcd.typ(self.args[0])
+
+    @property
+    def register(self) -> Register:
+        return self.bd.register(self.args[1])
+
+    def __str__(self) -> str:
+        return self.name
+
+
 @varregistry.register_tag("fp", VConstantValueVariable)
 class FunctionPointer(VConstantValueVariable):
     """Function pointer.

chb/invariants/XVariable.py

@@ -6,7 +6,7 @@
 #
 # Copyright (c) 2016-2020 Kestrel Technology LLC
 # Copyright (c) 2020-2021 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
@@ -116,6 +116,13 @@ def is_function_return_value(self) -> bool:
             and self.denotation.is_auxiliary_variable
             and self.denotation.auxvar.is_function_return_value)
 
+    @property
+    def is_typecast_value(self) -> bool:
+        return (
+            self.has_denotation()
+            and self.denotation.is_auxiliary_variable
+            and self.denotation.auxvar.is_typecast_value)
+
     @property
     def is_memory_address_value(self) -> bool:
         return (

chb/invariants/XXprUtil.py

@@ -55,7 +55,7 @@
         VMemoryVariable, VAuxiliaryVariable, VRegisterVariable)
     from chb.invariants.VConstantValueVariable import (
         VInitialRegisterValue, VInitialMemoryValue, VFunctionReturnValue,
-        SymbolicValue, MemoryAddress)
+        VTypeCastValue, SymbolicValue, MemoryAddress)
     from chb.invariants.VMemoryBase import (
         VMemoryBase,
         VMemoryBaseBaseVar,
@@ -889,6 +889,14 @@ def xvariable_to_ast_def_lval_expression(
         vinfo = astree.globalsymboltable.get_symbol(name)
         return astree.mk_vinfo_lval_expression(vinfo, anonymous=anonymous)
 
+    if xvar.is_typecast_value:
+        tcvar = cast("VTypeCastValue", xvar.denotation)
+        chklogger.logger.error(
+            "AST def conversion of typecast value %s to lval at address %s "
+            + "not yet supported",
+            str(tcvar), iaddr)
+        return astree.mk_temp_lval_expression()
+
     chklogger.logger.error(
         "AST def conversion of variable %s to lval-expression at address "
         + "%s not yet supported",
@@ -1553,12 +1561,17 @@ def global_variable_to_ast_lval(
             if fieldoffset.offset.is_no_offset:
                 subfieldastoffset: AST.ASTOffset = nooffset
             elif fieldoffset.offset.is_field_offset:
-                subfieldoffset = cast(
+                subfieldfldoffset = cast(
                     "VMemoryOffsetFieldOffset", fieldoffset.offset)
-                subfieldname = subfieldoffset.fieldname
-                subfieldkey = subfieldoffset.ckey
+                subfieldname = subfieldfldoffset.fieldname
+                subfieldkey = subfieldfldoffset.ckey
                 subfieldastoffset = astree.mk_field_offset(
                     subfieldname, subfieldkey)
+            elif fieldoffset.offset.is_array_index_offset:
+                subfieldarrayoffset = cast(
+                    "VMemoryOffsetArrayIndexOffset", fieldoffset.offset)
+                subfieldastoffset = array_offset_to_ast_offset(
+                    subfieldarrayoffset, xdata, iaddr, astree, anonymous=anonymous)
             else:
                 chklogger.logger.error(
                     "Index sub offset of global offset %s not yet handled at %s",
@@ -1741,10 +1754,26 @@ def vargument_deref_value_to_ast_lval(
         astree: ASTInterface,
         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 not offset.is_constant_value_offset:
         chklogger.logger.error(
-            "Non-constant offset: %s not yet supported at address %s",
-            str(offset), iaddr)
+            "Non-constant offset: %s with variable %s not yet supported at "
+            + "address %s",
+            str(offset), str(basevar), iaddr)
         return astree.mk_temp_lval()
 
     coff = offset.offsetvalue()
@@ -1844,6 +1873,39 @@ def vargument_deref_value_to_ast_lval(
             str(basevar), str(offset), iaddr)
         return astree.mk_temp_lval()
 
+    if basevar.is_typecast_value:
+        asmvar = cast("VAuxiliaryVariable", basevar.denotation)
+        vtcv = cast("VTypeCastValue", asmvar.auxvar)
+        bctype = vtcv.tgttype
+        vtype = bctype.convert(astree.typconverter)
+        if vtype is not None and vtype.is_pointer:
+            tgttype = cast(AST.ASTTypPtr, vtype).tgttyp
+            castaddr = vtcv.iaddr
+            if len(astree.ssa_intros[castaddr]) == 1:
+                vinfo = list(astree.ssa_intros[castaddr].values())[0]
+                vexpr = astree.mk_vinfo_lval_expression(
+                    vinfo, anonymous=anonymous)
+                if tgttype.is_compound:
+
+                    return field_pointer_to_ast_memref_lval(
+                        vexpr,
+                        tgttype,
+                        coff,
+                        iaddr,
+                        astree,
+                        anonymous=anonymous)
+
+            chklogger.logger.error(
+                "AST conversion of typecast value %s with type %s not yet handled "
+                + " at address %s",
+                str(basevar), str(tgttype), iaddr)
+            return astree.mk_temp_lval()
+
+        chklogger.logger.error(
+            "AST conversion of typecast value %s with type %s not yet handled at %s",
+            str(basevar), str(vtype), iaddr)
+        return astree.mk_temp_lval()
+
     chklogger.logger.error(
         "AST conversion of argument deref lvalue: %s with offset %s not yet "
         + "handled at %s (variable denotation type: %s)",