TYP: infrastructure for importing and displaying type constraints

Author: sipma

chb/app/BasicBlock.py

@@ -336,6 +336,7 @@ def to_string(
             bytes: bool = False,
             opcodetxt: bool = True,
             opcodewidth: int = 25,
+            typingrules: bool = False,
             sp: bool = True) -> str:
         ...
 

chb/app/CHVersion.py

@@ -1 +1 @@
-chbversion: str = "0.3.0-20250714"
+chbversion: str = "0.3.0-20250721"

chb/app/Function.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
@@ -604,6 +604,7 @@ def to_string(
             opcodewidth: int = 25,        # alignment width for opcode text
             sp: bool = True,
             proofobligations: bool = False,
+            typingrules: bool = False,
             stacklayout: bool = False) -> str:
         ...
 

chb/app/Instruction.py

@@ -345,6 +345,7 @@ def to_string(
             bytes: bool = False,
             opcodetxt: bool = True,
             opcodewidth: int = 25,
+            typingrules: bool = False,
             sp: bool = True) -> str:
         ...
 

chb/arm/ARMBlock.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
@@ -41,6 +41,7 @@
 from chb.invariants.XXpr import XXpr
 
 if TYPE_CHECKING:
+    from chb.app.AppAccess import AppAccess
     from chb.arm.ARMFunction import ARMFunction
 
 
@@ -55,6 +56,10 @@ def __init__(self, armf: "ARMFunction", xnode: ET.Element) -> None:
     def armfunction(self) -> "ARMFunction":
         return self._armf
 
+    @property
+    def app(self) -> "AppAccess":
+        return self.armfunction.app
+
     @property
     def armdictionary(self) -> ARMDictionary:
         return self.armfunction.armdictionary
@@ -74,13 +79,15 @@ def to_string(
             bytes: bool = False,
             opcodetxt: bool = True,
             opcodewidth: int = 40,
+            typingrules: bool = False,
             sp: bool = True) -> str:
         lines: List[str] = []
         for (ia, instr) in sorted(self.instructions.items()):
             pinstr = instr.to_string(
                 bytes=bytes,
                 opcodetxt=opcodetxt,
                 opcodewidth=opcodewidth,
+                typingrules=typingrules,
                 sp=sp)
             lines.append(str(ia).rjust(10) + "  " + pinstr)
         return "\n".join(lines)

chb/arm/ARMFunction.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
@@ -59,6 +59,7 @@
 import chb.util.fileutil as UF
 
 if TYPE_CHECKING:
+    from chb.app.AppAccess import AppAccess
     from chb.cmdline.PatchResults import PatchEvent
 
 
@@ -93,6 +94,10 @@ def __init__(
     def armdictionary(self) -> ARMDictionary:
         return self._armd
 
+    @property
+    def app(self) -> "AppAccess":
+        return self.armdictionary.app
+
     @property
     def armfunctiondictionary(self) -> FunctionDictionary:
         if self._armfnd is None:
@@ -289,6 +294,7 @@ def to_string(
             opcodewidth: int = 40,
             sp: bool = True,
             proofobligations: bool = False,
+            typingrules: bool = False,
             stacklayout: bool = False) -> str:
         lines: List[str] = []
         if stacklayout:
@@ -311,6 +317,7 @@ def to_string(
                     bytes=bytes,
                     opcodetxt=opcodetxt,
                     opcodewidth=opcodewidth,
+                    typingrules=typingrules,
                     sp=sp))
             lines.append("-" * 80)
             if self.has_jumptable(self.blocks[b].lastaddr):

chb/arm/ARMInstruction.py

@@ -61,6 +61,7 @@
 
 
 if TYPE_CHECKING:
+    from chb.app.AppAccess import AppAccess
     from chb.arm.ARMBlock import ARMBlock
     from chb.arm.ARMFunction import ARMFunction
     from chb.arm.ARMJumpTable import ARMJumpTable
@@ -88,6 +89,10 @@ def armfunction(self) -> "ARMFunction":
     def armdictionary(self) -> ARMDictionary:
         return self.armblock.armdictionary
 
+    @property
+    def app(self) -> "AppAccess":
+        return self.armfunction.app
+
     @property
     def armfunctiondictionary(self) -> "FunctionDictionary":
         return self.armfunction.armfunctiondictionary
@@ -434,13 +439,24 @@ def to_string(
             bytes: bool = False,
             opcodetxt: bool = True,
             opcodewidth: int = 40,
+            typingrules: bool = False,
             sp: bool = False) -> str:
+        if typingrules:
+            lines: List[str] = []
+            rulesapplied = self.app.type_constraints.rules_applied_to_instruction(
+                self.armfunction.faddr, self.iaddr)
+            for r in sorted(str(r) for r in rulesapplied):
+                lines.append("   " + str(r))
         try:
             pbytes = self.bytestring.ljust(10) + "  " if bytes else ""
             pesp = str(self.stackpointer_offset) + "  " if sp else ""
             popcode = (
                 self.opcodetext.ljust(opcodewidth) if opcodetxt else "")
-            return pesp + pbytes + popcode + self.annotation
+            codeline = pesp + pbytes + popcode + self.annotation
+            if len(lines) > 0:
+                return codeline + "\n  " + "\n  ".join(lines)
+            else:
+                return codeline
         except Exception as e:
             print(
                 "Error in instruction: "

chb/bctypes/TypeConstraintStore.py

@@ -24,11 +24,14 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 # ------------------------------------------------------------------------------
+import xml.etree.ElementTree as ET
 
 from typing import cast, Dict, List, Optional, Set, TYPE_CHECKING
 
 import chb.bctypes.TypeConstraint as TC
 
+import chb.util.fileutil as UF
+
 if TYPE_CHECKING:
     from chb.app.AppAccess import AppAccess
 
@@ -231,18 +234,96 @@ def __str__(self) -> str:
         return "\n".join(lines)
 
 
+class TypingRule:
+
+    def __init__(self, tcstore: "TypeConstraintStore", xr: ET.Element) -> None:
+        self._tcstore = tcstore
+        self._xr = xr
+
+    @property
+    def tcstore(self) -> "TypeConstraintStore":
+        return self._tcstore
+
+    @property
+    def app(self) -> "AppAccess":
+        return self.tcstore.app
+
+    @property
+    def iaddr(self) -> str:
+        return self._xr.get("loc", "0x0")
+
+    @property
+    def rulename(self) -> str:
+        return self._xr.get("rule", "?")
+
+    @property
+    def typeconstraint(self) -> TC.TypeConstraint:
+        ix = self._xr.get("tc-ix")
+        if ix is not None:
+            return self.app.tcdictionary.type_constraint(int(ix))
+        else:
+            raise UF.CHBError("Type constraint without tc index")
+
+    def __str__(self) -> str:
+        ix = self._xr.get("tc-ix")
+        return self.rulename + " " + str(ix) + ":" + str(self.typeconstraint)
+
+
 class TypeConstraintStore:
+    """Global store for type constraints.
+
+    Note: The use of this object is currently somewhat conflicted. It was
+    originally intended for global use, to recover function signatures for
+    an entire binary. More recently, however, it has been mainly used to
+    perform type construction for all local variables (registers and stack)
+    within individual functions to support lifting. This latest use in its
+    present form does not scale to an entire binary. For now the scaling
+    issue is solved by resetting the store after each function, which
+    essentially means that the store, when saved, only holds the constraints
+    for a single function (the latest processed).
+    """
 
     def __init__(self, app: "AppAccess") -> None:
         self._app = app
         self._constraints: Optional[List[TC.TypeConstraint]] = None
         self._functionconstraints: Dict[str, FunctionTypeConstraints] = {}
         self._functionregconstraints: Dict[str, FunctionRegisterConstraints] = {}
+        self._rules_applied: Optional[Dict[str, Dict[str, List[TypingRule]]]] = None
 
     @property
     def app(self) -> "AppAccess":
         return self._app
 
+    @property
+    def rules_applied(self) -> Dict[str, Dict[str, List[TypingRule]]]:
+        if self._rules_applied is None:
+            self._rules_applied = {}
+            tcstore = UF.get_typeconstraint_store_xnode(
+                self.app.path, self.app.filename)
+            if tcstore is not None:
+                rules = tcstore.find("rules-applied")
+                if rules is not None:
+                    for xf in rules.findall("function"):
+                        faddr = xf.get("faddr", "0x0")
+                        self._rules_applied[faddr] = {}
+                        for xr in xf.findall("rule"):
+                            rule = TypingRule(self, xr)
+                            self._rules_applied[faddr].setdefault(rule.iaddr, [])
+                            self._rules_applied[faddr][rule.iaddr].append(rule)
+
+        return self._rules_applied
+
+    def rules_applied_to_instruction(
+            self, faddr: str, iaddr: str) -> List[TypingRule]:
+        result: List[TypingRule] = []
+        if faddr in self.rules_applied:
+            if iaddr in self.rules_applied[faddr]:
+                for r in self.rules_applied[faddr][iaddr]:
+                    if r.typeconstraint.is_var_constraint:
+                        continue
+                    result.append(r)
+        return result
+
     @property
     def constraints(self) -> List[TC.TypeConstraint]:
         if self._constraints is None:

chb/cmdline/chkx

@@ -953,6 +953,10 @@ def parse() -> argparse.Namespace:
         "--proofobligations",
         action="store_true",
         help="include proofobligations at the top of the function")
+    resultsfunction.add_argument(
+        "--typingrules",
+        action="store_true",
+        help="include typing rules applied after each instruction")
     resultsfunction.add_argument(
         "--loglevel", "-log",
         choices=UL.LogLevel.options(),

chb/cmdline/commandutil.py

@@ -1099,6 +1099,7 @@ def results_function(args: argparse.Namespace) -> NoReturn:
     txtoutput: bool = not xjson
     stacklayout: bool = args.stacklayout
     proofobligations: bool = args.proofobligations
+    typingrules: bool = args.typingrules
     loglevel: str = args.loglevel
     logfilename: Optional[str] = args.logfilename
     logfilemode: str = args.logfilemode
@@ -1161,6 +1162,7 @@ def results_function(args: argparse.Namespace) -> NoReturn:
                 sp=True,
                 opcodetxt=True,
                 proofobligations=proofobligations,
+                typingrules=typingrules,
                 stacklayout=stacklayout,
                 opcodewidth=opcodewidth))
         except UF.CHBError as e: