diff --git a/chb/api/XXPredicate.py b/chb/api/XXPredicate.py index 6fcdfe1b..77536b7f 100644 --- a/chb/api/XXPredicate.py +++ b/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 diff --git a/chb/app/FnProofObligations.py b/chb/app/FnProofObligations.py index 18189360..5cd8a204 100644 --- a/chb/app/FnProofObligations.py +++ b/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]]: diff --git a/chb/app/FnXPODictionary.py b/chb/app/FnXPODictionary.py index a035dbfb..2ebdb709 100644 --- a/chb/app/FnXPODictionary.py +++ b/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: diff --git a/chb/app/Function.py b/chb/app/Function.py index d64991bc..6d7c8899 100644 --- a/chb/app/Function.py +++ b/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]: diff --git a/chb/app/Instruction.py b/chb/app/Instruction.py index 03f96660..14642dd6 100644 --- a/chb/app/Instruction.py +++ b/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 {} diff --git a/chb/app/XPOPredicate.py b/chb/app/XPOPredicate.py index 189a8bb0..fa1b7998 100644 --- a/chb/app/XPOPredicate.py +++ b/chb/app/XPOPredicate.py @@ -26,7 +26,7 @@ # ------------------------------------------------------------------------------ """Predicate over expressions in a function context.""" -from typing import List, TYPE_CHECKING +from typing import List, Optional, TYPE_CHECKING from chb.app.FnXPODictionaryRecord import ( FnXPODictionaryRecord, xporegistry) @@ -37,7 +37,7 @@ if TYPE_CHECKING: from chb.api.BTerm import BTerm - from chb.app.FnXPODictionary import FnXPODictionary + from chb.app.FnXPODictionary import FnXPODictionary, XPOFormatArgument from chb.bctypes.BCTyp import BCTyp from chb.invariants.XXpr import XXpr @@ -171,7 +171,7 @@ def is_xpo_validmem(self) -> bool: @property def is_xpo_disjunction(self) -> bool: return False - + @xporegistry.register_tag("ab", XPOPredicate) class XPOAllocationBase(XPOPredicate): @@ -380,7 +380,7 @@ class XPOFunctionPointer(XPOPredicate): def __init__( self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: XPOPredicate.__init__(self, xpod, ixval) - + @property def is_xpo_function_pointer(self) -> bool: return True @@ -458,7 +458,7 @@ def __str__(self) -> str: + str(self.size) + ")") - + @xporegistry.register_tag("ifs", XPOPredicate) class XPOInputFormatString(XPOPredicate): """Expression points to a format string for input (scanf). @@ -531,8 +531,8 @@ def size(self) -> "XXpr": def __str__(self) -> str: return "new-memory(" + str(self.pointer) + ", " + str(self.size) + ")" - - + + @xporegistry.register_tag("sa", XPOPredicate) class XPOStackAddress(XPOPredicate): """Expression is a stack address. @@ -542,7 +542,7 @@ class XPOStackAddress(XPOPredicate): def __init__( self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: - XPOPredicate.__init__(self, xpod, ixval) + XPOPredicate.__init__(self, xpod, ixval) @property def is_xpo_stack_address(self) -> bool: @@ -565,7 +565,7 @@ class XPOHeapAddress(XPOPredicate): def __init__( self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: - XPOPredicate.__init__(self, xpod, ixval) + XPOPredicate.__init__(self, xpod, ixval) @property def is_xpo_heap_address(self) -> bool: @@ -577,7 +577,7 @@ def expr(self) -> "XXpr": def __str__(self) -> str: return "heap-address(" + str(self.expr) + ")" - + @xporegistry.register_tag("ga", XPOPredicate) class XPOGlobalAddress(XPOPredicate): @@ -588,7 +588,7 @@ class XPOGlobalAddress(XPOPredicate): def __init__( self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: - XPOPredicate.__init__(self, xpod, ixval) + XPOPredicate.__init__(self, xpod, ixval) @property def is_xpo_global_address(self) -> bool: @@ -600,7 +600,7 @@ def expr(self) -> "XXpr": def __str__(self) -> str: return "global-address(" + str(self.expr) + ")" - + @xporegistry.register_tag("no", XPOPredicate) class XPONoOverlap(XPOPredicate): @@ -629,7 +629,7 @@ def pointer2(self) -> "XXpr": def __str__(self) -> str: return ( "no-overlap(" + str(self.pointer1) + ", " + str(self.pointer2) + ")") - + @xporegistry.register_tag("nn", XPOPredicate) class XPONotNull(XPOPredicate): @@ -652,7 +652,7 @@ def pointer(self) -> "XXpr": def __str__(self) -> str: return "not-null(" + str(self.pointer) + ")" - + @xporegistry.register_tag("nu", XPOPredicate) class XPONull(XPOPredicate): @@ -675,7 +675,7 @@ def pointer(self) -> "XXpr": def __str__(self) -> str: return "null(" + str(self.pointer) + ")" - + @xporegistry.register_tag("nz", XPOPredicate) class XPONotZero(XPOPredicate): @@ -698,7 +698,7 @@ def expr(self) -> "XXpr": def __str__(self) -> str: return "not-zero(" + str(self.expr) + ")" - + @xporegistry.register_tag("nng", XPOPredicate) class XPONonNegative(XPOPredicate): @@ -721,8 +721,8 @@ def expr(self) -> "XXpr": def __str__(self) -> str: return "non-negative(" + str(self.expr) + ")" - - + + @xporegistry.register_tag("nt", XPOPredicate) class XPONullTerminated(XPOPredicate): """Pointer points to null-terminated string. @@ -767,7 +767,7 @@ def pointer(self) -> "XXpr": def __str__(self) -> str: return "output-format-string(" + str(self.pointer) + ")" - + @xporegistry.register_tag("pos", XPOPredicate) class XPOPositive(XPOPredicate): @@ -901,6 +901,101 @@ def __str__(self) -> str: return "tainted(" + str(self.expr) + ")" +@xporegistry.register_tag("ts", XPOPredicate) +class XPOTrustedString(XPOPredicate): + """Expression is trusted. + + args[0]: index of expression in xprdictionary + """ + + def __init__( + self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: + XPOPredicate.__init__(self, xpod, ixval) + + @property + def is_xpo_trusted_string(self) -> bool: + return True + + @property + def expr(self) -> "XXpr": + return self.xd.xpr(self.args[0]) + + def __str__(self) -> str: + return "trusted-string(" + str(self.expr) + ")" + + +@xporegistry.register_tag("tc", XPOPredicate) +class XPOTrustedOsCmdString(XPOPredicate): + """Expression is trusted os command string + + args[0]: index of expression in xprdictionary + """ + + def __init__( + self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: + XPOPredicate.__init__(self, xpod, ixval) + + @property + def is_xpo_trusted_os_cmd_string(self) -> bool: + return True + + @property + def expr(self) -> "XXpr": + return self.xd.xpr(self.args[0]) + + def __str__(self) -> str: + return "trusted-os-cmd-string(" + str(self.expr) + ")" + + +@xporegistry.register_tag("tfs", XPOPredicate) +class XPOTrustedOsCmdFmtString(XPOPredicate): + """Expression is trusted os command format string + + args[0]: index of expression in xprdictionary + """ + + def __init__( + self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: + XPOPredicate.__init__(self, xpod, ixval) + + @property + def is_xpo_trusted_os_cmd_fmt_string(self) -> bool: + return True + + @property + def expr(self) -> "XXpr": + return self.xd.xpr(self.args[0]) + + @property + def kind(self) -> str: + if self.tags[1] == "f": + return "FMT_ARGS" + else: + return "VA_LIST" + + @property + def optlen(self) -> Optional["XXpr"]: + if self.args[1] == -1: + return None + return self.xd.xpr(self.args[1]) + + @property + def format_arguments(self) -> List["XPOFormatArgument"]: + return [self.xpod.format_arg(i) for i in self.args[2:]] + + def __str__(self) -> str: + return ( + "trusted-os-cmd-fmt-string(" + + str(self.expr) + + ", " + + self.kind + + ", " + + (str(self.optlen) if self.optlen is not None else "_") + + ", " + + ", ".join(str(fmtarg) for fmtarg in self.format_arguments) + + ")") + + @xporegistry.register_tag("v", XPOPredicate) class XPOValidMem(XPOPredicate): """Expression points to valid memory. @@ -922,5 +1017,3 @@ def expr(self) -> "XXpr": def __str__(self) -> str: return "validmem(" + str(self.expr) + ")" - - diff --git a/chb/arm/ARMInstruction.py b/chb/arm/ARMInstruction.py index ec27b6bc..d135d690 100644 --- a/chb/arm/ARMInstruction.py +++ b/chb/arm/ARMInstruction.py @@ -412,11 +412,11 @@ def lhs_variables( def rhs_expressions(self, filter: Callable[[XXpr], bool]) -> List[XXpr]: return [x for x in self.opcode.rhs(self.xdata) if filter(x)] - def rdef_locations(self) -> Dict[str, List[str]]: + def rdef_register_locations(self) -> Dict[str, List[str]]: result: Dict[str, List[str]] = {} for rdef in self.xdata.reachingdefs: - if rdef is not None: + if rdef is not None and rdef.variable.is_register_variable: rdefvar = str(rdef.variable) rdeflocs = sorted([str(s) for s in rdef.valid_deflocations]) result[rdefvar] = rdeflocs diff --git a/chb/astinterface/ASTIProvenance.py b/chb/astinterface/ASTIProvenance.py index a092cd5c..29a20a56 100644 --- a/chb/astinterface/ASTIProvenance.py +++ b/chb/astinterface/ASTIProvenance.py @@ -453,7 +453,15 @@ def resolve_reaching_defs(self) -> None: v, str(instr.tgt), addr) self.add_reaching_definition(xid, instrid) else: - chklogger.logger.warning( + # Calls may have side effects, which will + # also produce reaching definitions. These + # are currently not included in the + # ASTCall data type, but probably should + # be added at some point. For now this + # warning is changed into an INFO msg until + # side effects are properly incorporated + # in the AST representation. + chklogger.logger.info( "Lhs variable names don't match: %s vs %s" + " to %s for reaching def address %s", str(instr.lhs), v, str(instr.tgt), addr) diff --git a/chb/cmdline/astcmds.py b/chb/cmdline/astcmds.py index d61e8337..df4a1292 100644 --- a/chb/cmdline/astcmds.py +++ b/chb/cmdline/astcmds.py @@ -468,7 +468,7 @@ def print_reachingdefs( dotpaths: List[Tuple[DotRdefPath, str, str]] = [] regspill = register + "_spill" for (iaddr, instr) in f.instructions.items(): - if register in instr.rdef_locations(): + if register in instr.rdef_register_locations(): register_o = app.bdictionary.register_by_name(register) cblock = f.containing_block(iaddr) rdefs = instr.reaching_definitions(register) diff --git a/chb/cmdline/commandutil.py b/chb/cmdline/commandutil.py index 7b509351..4cdf7761 100644 --- a/chb/cmdline/commandutil.py +++ b/chb/cmdline/commandutil.py @@ -475,6 +475,8 @@ def analyzecmd(args: argparse.Namespace) -> NoReturn: + ". Version found: " + chbversion) + doreset = True + try: userhints = prepare_executable( path, diff --git a/chb/summaries/bchsummaries.jar b/chb/summaries/bchsummaries.jar index 887d1243..26ca2467 100644 Binary files a/chb/summaries/bchsummaries.jar and b/chb/summaries/bchsummaries.jar differ