Predicates

chb/api/XXPredicate.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2023  Aarno Labs LLC
+# Copyright (c) 2023-2026  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
@@ -165,14 +165,38 @@ def is_xp_starts_thread(self) -> bool:
     def is_xp_tainted(self) -> bool:
         return False
 
+    @property
+    def is_xp_trusted_string(self) -> bool:
+        return False
+
+    @property
+    def is_xp_trusted_os_cmd_string(self) -> bool:
+        return False
+
+    @property
+    def is_xp_trusted_os_cmd_fmt_string(self) -> bool:
+        return False
+
+    @property
+    def is_xp_trusted_os_cmd_fmt_arg_string(self) -> bool:
+        return False
+
     @property
     def is_xp_validmem(self) -> bool:
         return False
 
+    @property
+    def is_xp_writes_string_from_fmt_string(self) -> bool:
+        return False
+
     @property
     def is_xp_disjunction(self) -> bool:
         return False
 
+    @property
+    def is_xp_conditional(self) -> bool:
+        return False
+
 
 @apiregistry.register_tag("ab", XXPredicate)
 class XXPAllocationBase(XXPredicate):
@@ -925,15 +949,59 @@ def __str__(self) -> str:
         return "tainted(" + str(self.term) + ")"
 
 
+@apiregistry.register_tag("ts", XXPredicate)
+class XXTrustedString(XXPredicate):
+
+    def __init__(
+            self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None:
+        XXPredicate.__init__(self, ixd, ixval)
+
+    @property
+    def is_xp_trusted_string(self) -> bool:
+        return True
+
+    @property
+    def term(self) -> "BTerm":
+        return self.id.bterm(self.args[0])
+
+    def __str__(self) -> str:
+        return "trusted-string(" + str(self.term) + ")"
+
+
+@apiregistry.register_tag("tc", XXPredicate)
+class XXTrustedOsCmdString(XXPredicate):
+    """String is safe to pass as an argument to system or popen."""
+
+    def __init__(
+            self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None:
+        XXPredicate.__init__(self, ixd, ixval)
+
+    @property
+    def is_xp_trusted_os_cmd_string(self) -> bool:
+        return True
+
+    @property
+    def term(self) -> "BTerm":
+        return self.id.bterm(self.args[0])
+
+    def __str__(self) -> str:
+        return "trusted-os-cmd-string(" + str(self.term) + ")"
+
+
 @apiregistry.register_tag("tfs", XXPredicate)
 class XXPTrustedOsCmdFmtString(XXPredicate):
+    """The string constructed by the format string is safe to pass to system.
+
+    If a length is given, the string must evaluate to a value that has string
+    length less than the given length.
+    """
 
     def __init__(
             self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None:
         XXPredicate.__init__(self, ixd, ixval)
 
     @property
-    def is_xp_trusted_os_cmd_string(self) -> bool:
+    def is_xp_trusted_os_cmd_fmt_string(self) -> bool:
         return True
 
     @property
@@ -951,7 +1019,104 @@ def optlen(self) -> Optional["BTerm"]:
         return self.id.bterm(self.args[1])
 
     def __str__(self) -> str:
-        return "trusted-os-cmd-fmt-string(" + str(self.fmt) + ", " + self.fmtkind + ", " + str(self.optlen) + ")"
+        return (
+            "trusted-os-cmd-fmt-string("
+            + str(self.fmt)
+            + ", "
+            + self.fmtkind
+            + ", "
+            + str(self.optlen)
+            + ")")
+
+
+@apiregistry.register_tag("tfa", XXPredicate)
+class XXPTrustedOsCmdFmtArgString(XXPredicate):
+    """String is safe to pass as a format argument to a string passed to system.
+
+    It is safe if the format specifier associated with this argument is
+    enclosed in quotes according to the quotes property.
+
+    If a length is given the length of the argument string must be less than
+    or equal to the given length.
+    """
+
+    def __init__(
+            self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None:
+        XXPredicate.__init__(self, ixd, ixval)
+
+    @property
+    def is_xp_trusted_os_cmd_fmt_arg_string(self) -> bool:
+        return True
+
+    @property
+    def fmt(self) -> "BTerm":
+        return self.id.bterm(self.args[0])
+
+    @property
+    def quotes(self) -> str:
+        return self.tags[1]
+
+    @property
+    def optlen(self) -> Optional["BTerm"]:
+        if self.args[1] == -1:
+            return None
+        return self.id.bterm(self.args[1])
+
+    def __str__(self) -> str:
+        return (
+            "trusted-os-cmd-fmt-string("
+            + str(self.fmt)
+            + ", "
+            + self.quotes
+            + ", "
+            + str(self.optlen)
+            + ")")
+
+
+@apiregistry.register_tag("wfs", XXPredicate)
+class XXPWritesStringFromFmtString(XXPredicate):
+    """Side effect that asserts that a string is constructed from the given format string.
+
+    An optional length imposes a maximum length on the string being written.
+    """
+
+    def __init__(
+            self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None:
+        XXPredicate.__init__(self, ixd, ixval)
+
+    @property
+    def is_xp_writes_string_from_fmt_string(self) -> bool:
+        return True
+
+    @property
+    def destination(self) -> "BTerm":
+        return self.id.bterm(self.args[0])
+
+    @property
+    def fmt(self) -> "BTerm":
+        return self.id.bterm(self.args[1])
+
+    @property
+    def fmtkind(self) -> str:
+        return self.tags[1]
+
+    @property
+    def optlen(self) -> Optional["BTerm"]:
+        if self.args[2] == -1:
+            return None
+        return self.id.bterm(self.args[2])
+
+    def __str__(self) -> str:
+        return (
+            "writes-string-from-fmt-string("
+            + str(self.destination)
+            + ", "
+            + str(self.fmt)
+            + ", "
+            + self.fmtkind
+            + ", "
+            + str(self.optlen)
+            + ")")
 
 
 @apiregistry.register_tag("v", XXPredicate)

chb/app/CHVersion.py

@@ -1,3 +1,3 @@
 chbversion: str = "0.3.0-20260527"
 
-minimum_required_chb_version = "0.6.0_20260407"
+minimum_required_chb_version = "0.6.0_20260527"

chb/cmdline/AnalysisManager.py

@@ -75,6 +75,7 @@ def __init__(
             fns_no_lineq: List[str] = [],
             fns_exclude: List[str] = [],
             fns_include: List[str] = [],
+            fns_include_callees: bool = False,
             show_function_timing: bool = False,
             gc_compact: int = 0,
             lineq_instr_cutoff: int = 0,
@@ -114,6 +115,7 @@ def __init__(
         self.fns_no_lineq = fns_no_lineq
         self.fns_exclude = fns_exclude
         self.fns_include = fns_include
+        self.fns_include_callees = fns_include_callees
         self.show_function_timing = show_function_timing
         self.gc_compact = gc_compact
         self.lineq_instr_cutoff = lineq_instr_cutoff
@@ -483,6 +485,8 @@ def _analyze_until_stable(
             cmd.extend(["-fn_exclude", s])
         for s in self.fns_include:
             cmd.extend(["-fn_include", s])
+        if self.fns_include_callees:
+            cmd.append("-fn_include_callees")
         for s in self.specializations:
             cmd.extend(["-specialization", s])
         if analysisrepeats > 1:

chb/cmdline/chkx

@@ -476,6 +476,10 @@ def parse() -> argparse.Namespace:
         nargs="*",
         default=[],
         help="addresses of function to include in the analysis")
+    analyzecmd.add_argument(
+        "--fns_include_callees",
+        help="include callees of all fns_included",
+        action="store_true")
     analyzecmd.add_argument(
         "--analyze_all_named",
         help="include all functions named in userdata in the analysis",

chb/cmdline/commandutil.py

@@ -416,6 +416,7 @@ def analyzecmd(args: argparse.Namespace) -> NoReturn:
     fns_no_lineq: List[str] = args.fns_no_lineq  # function hex addresses
     fns_exclude: List[str] = args.fns_exclude  # function hex addresses
     fns_include: List[str] = args.fns_include  # function hex addresses
+    fns_include_callees: bool = args.fns_include_callees
     analyze_all_named: bool = args.analyze_all_named
     analyze_range_entry_points: List[str] = args.analyze_range_entry_points
     gc_compact: int = args.gc_compact
@@ -553,6 +554,7 @@ def analyzecmd(args: argparse.Namespace) -> NoReturn:
         fns_no_lineq=fns_no_lineq,
         fns_exclude=fns_exclude,
         fns_include=fns_include,
+        fns_include_callees=fns_include_callees,
         gc_compact=gc_compact,
         show_function_timing=show_function_timing,
         lineq_instr_cutoff=lineq_instr_cutoff,

chb/models/FunctionPrecondition.py

@@ -41,7 +41,7 @@
 
 from chb.models.BTerm import BTerm, btermregistry
 from chb.models.ModelsType import ModelsType, mk_type
-    
+
 
 import chb.util.fileutil as UF
 
@@ -347,3 +347,29 @@ def __str__(self) -> str:
             + ", "
             + str(self.arg2)
             + ")")
+
+
+@preconditionregistry.register_tag("trusted-os-cmd-string", FunctionPrecondition)
+class PreTrustedOsCmdString(FunctionPrecondition):
+
+    def __init__(
+            self,
+            fsem: "FunctionSemantics",
+            tag: str,
+            xnode: Optional[ET.Element] = None) -> None:
+        FunctionPrecondition.__init__(self, fsem, tag, xnode)
+        self._arg1: Optional[BTerm] = None
+
+    @property
+    def arg1(self) -> BTerm:
+        if self._arg1 is None:
+            self._arg1 = (
+                btermregistry.mk_instance(self.semantics, self.xterm(0), BTerm))
+        return self._arg1
+
+    def __str__(self) -> str:
+        return (
+            self.tag
+            + "("
+            + str(self.arg1)
+            + ")")

chb/models/ModelsAccess.py

@@ -6,7 +6,7 @@
 #
 # Copyright (c) 2016-2020 Kestrel Technology LLC
 # Copyright (c) 2020      Henny Sipma
-# Copyright (c) 2021-2023 Aarno Labs LLC
+# Copyright (c) 2021-2026 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