Documentation

chb/api/XXPredicate.py

@@ -26,7 +26,7 @@
 # ------------------------------------------------------------------------------
 
 
-from typing import List, TYPE_CHECKING
+from typing import List, Optional, TYPE_CHECKING
 
 from chb.api.InterfaceDictionaryRecord import (
     InterfaceDictionaryRecord, apiregistry)
@@ -925,6 +925,35 @@ def __str__(self) -> str:
         return "tainted(" + str(self.term) + ")"
 
 
+@apiregistry.register_tag("tfs", XXPredicate)
+class XXPTrustedOsCmdFmtString(XXPredicate):
+
+    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 fmt(self) -> "BTerm":
+        return self.id.bterm(self.args[0])
+
+    @property
+    def fmtkind(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.fmtkind + ", " + str(self.optlen) + ")"
+
+
 @apiregistry.register_tag("v", XXPredicate)
 class XXPValidMem(XXPredicate):
     """Term points to valid memory

chb/app/FnProofObligations.py

@@ -47,13 +47,20 @@
     "o": "open",
     "dis": "safe",
     "del": "delegated",
+    "local": "delegated-local",
     "v": "violation"
 }
 
 class POStatus:
 
-    def __init__(self, tag: str) -> None:
-        self._tag = tag
+    def __init__(self, xpod: "FnXPODictionary", node: ET.Element) -> None:
+        self.node = node
+        self._xpod = xpod
+        self._tag = self.node.get("s", "none")
+
+    @property
+    def xpod(self) -> "FnXPODictionary":
+        return self._xpod
 
     @property
     def tag(self) -> str:
@@ -71,11 +78,20 @@ def is_discharged(self) -> bool:
     def is_delegated(self) -> bool:
         return self.tag == "del"
 
+    @property
+    def is_delegated_local(self) -> bool:
+        return self.tag == "local"
+
     @property
     def is_violated(self) -> bool:
         return self.tag == "v"
 
+    def get_iaddr(self) -> str:
+        return self.node.get("iaddr", "?")
+
     def __str__(self) -> str:
+        if self.is_delegated_local:
+            return "delegated-local: " + self.get_iaddr()
         return po_status_strings.get(self.tag, "?")
 
 
@@ -173,11 +189,12 @@ def proofobligations(self) -> Dict[str, List[ProofObligation]]:
                     self._store[iaddr] = []
                     for xxpo in xloc.findall("po"):
                         xpo = self.xpod.read_xml_xpo_predicate(xxpo)
-                        statustag = xxpo.get("s", "o")
-                        status = POStatus(statustag)
-                        msg = xxpo.get("m", "none")
-                        po = ProofObligation(iaddr, xpo, status, msg)
-                        self._store[iaddr].append(po)
+                        xstatus = xxpo.find("status")
+                        if xstatus is not None:
+                            status = POStatus(self.xpod, xstatus)
+                            msg = xxpo.get("m", "none")
+                            po = ProofObligation(iaddr, xpo, status, msg)
+                            self._store[iaddr].append(po)
         return self._store
 
     def open_proofobligations(self) -> Dict[str, List[ProofObligation]]:

chb/app/FnXPODictionary.py

@@ -28,9 +28,9 @@
 
 import xml.etree.ElementTree as ET
 
-from typing import List, TYPE_CHECKING
+from typing import List, Optional, TYPE_CHECKING
 
-from chb.app.FnXPODictionaryRecord import xporegistry
+from chb.app.FnXPODictionaryRecord import xporegistry, FnXPODictionaryRecord
 from chb.app.XPOPredicate import XPOPredicate
 
 import chb.util.IndexedTable as IT
@@ -41,6 +41,28 @@
     from chb.app.Function import Function
     from chb.bctypes.BCDictionary import BCDictionary
     from chb.invariants.FnXprDictionary import FnXprDictionary
+    from chb.invariants.XXpr import XXpr
+
+
+class XPOFormatArgument(FnXPODictionaryRecord):
+
+    def __init__(self, xpod: "FnXPODictionary", ixval: IT.IndexedTableValue) -> None:
+        FnXPODictionaryRecord.__init__(self, xpod, ixval)
+
+    @property
+    def argument(self) -> "XXpr":
+        return self.xd.xpr(self.args[0])
+
+    @property
+    def converter(self) -> str:
+        return self.tags[0]
+
+    @property
+    def fieldwidth(self) -> Optional[int]:
+        return None if self.tags[1] == "other" else int(self.tags[1])
+
+    def __str__(self) -> str:
+        return "(" + self.converter + ", " + str(self.argument) + ")"
 
 
 class FnXPODictionary:
@@ -50,8 +72,10 @@ def __init__(
             fn: "Function",
             xnode: ET.Element) -> None:
         self._fn = fn
+        self.format_arg_table = IT.IndexedTable("format-arg-table")
         self.xpo_predicate_table = IT.IndexedTable("xpo-predicate-table")
         self.tables: List[IT.IndexedTable] = [
+            self.format_arg_table,
             self.xpo_predicate_table
         ]
         self.initialize(xnode)
@@ -82,6 +106,10 @@ def xpo_predicate(self, ix: int) -> XPOPredicate:
             raise UF.CHBError(
                 "Illegal xpo predicate index value: " + str(ix))
 
+    def format_arg(self, ix: int) -> XPOFormatArgument:
+        return XPOFormatArgument(self, self.format_arg_table.retrieve(ix))
+
+
     # ------------------------------------- initialize dictionary from file ---
 
     def read_xml_xpo_predicate(self, xnode: ET.Element) -> XPOPredicate:

chb/app/Function.py

@@ -531,7 +531,7 @@ def rdef_location_partition(self) -> Dict[str, List[List[str]]]:
         result: Dict[str, List[List[str]]] = {}
 
         for (iaddr, instr) in self.instructions.items():
-            irdefs = instr.rdef_locations()
+            irdefs = instr.rdef_register_locations()
             for (reg, rdeflist) in irdefs.items():
                 result.setdefault(reg, [])
                 for rrlist in result[reg]:

chb/app/Instruction.py

@@ -341,8 +341,15 @@ def ast_switch_condition_prov(
             Optional[AST.ASTExpr], Optional[AST.ASTExpr]]:
         raise UF.CHBError("ast-switch-condition-prov not defined")
 
-    def rdef_locations(self) -> Dict[str, List[str]]:
-        """Returns for each register, which locations must be combined."""
+    def rdef_register_locations(self) -> Dict[str, List[str]]:
+        """Returns for each register, which locations must be combined.
+
+        Note that there may be rdefs (reaching definitions) for other
+        variables. In particular, stack variables that get initialized
+        as part of a function side effect create a definition for that
+        variable, which may be retrieved via a reaching definition later.
+        Those variables are not returned by this method.
+        """
 
         return {}