diff --git a/chb/api/AppFunctionSemantics.py b/chb/api/AppFunctionSemantics.py index 8615fe74..f8050268 100644 --- a/chb/api/AppFunctionSemantics.py +++ b/chb/api/AppFunctionSemantics.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 @@ -35,6 +35,7 @@ from chb.util.IndexedTable import IndexedTableValue if TYPE_CHECKING: + from chb.api.FunctionQualifiers import FunctionQualifiers from chb.api.InterfaceDictionary import InterfaceDictionary from chb.api.XXPredicate import XXPredicate @@ -46,6 +47,8 @@ class AppFunctionSemantics(InterfaceDictionaryRecord): args[1]: index of postcondition list in interfacedictionary args[2]: index of error-postcondition list in interfacedictionary args[3]: index of side-effect list in interfacedictionary + args[4]: index of post requests in interfacedictionary + args[5]: index of function-qualifiers in interfacedictionary """ def __init__( @@ -68,6 +71,14 @@ def errorpostcondition_list(self) -> List["XXPredicate"]: def sideeffect_list(self) -> List["XXPredicate"]: return self.id.xpredicate_list(self.args[3]) + @property + def postrequest_list(self) -> List["XXPredicate"]: + return self.id.xpredicate_list(self.args[4]) + + @property + def qualifiers(self) -> "FunctionQualifiers": + return self.id.function_qualifiers(self.args[5]) + def __str__(self) -> str: lines: List[str] = [] if len(self.precondition_list) > 0: @@ -86,4 +97,5 @@ def __str__(self) -> str: lines.append("Side-effects") for p in self.sideeffect_list: lines.append(" " + str(p)) + lines.append("Qualifiers: " + str(self.qualifiers)) return "\n".join(lines) diff --git a/chb/api/AppFunctionSignature.py b/chb/api/AppFunctionSignature.py index 90cd8838..00b562e1 100644 --- a/chb/api/AppFunctionSignature.py +++ b/chb/api/AppFunctionSignature.py @@ -67,6 +67,10 @@ def calling_convention(self) -> str: def parameter_list(self) -> List["FtsParameter"]: return self.id.fts_parameter_list(self.args[0]) + @property + def is_vararg(self) -> bool: + return self.args[1] == 1 + @property def returntype(self) -> "BCTyp": return self.bcd.typ(self.args[3]) diff --git a/chb/api/FunctionQualifiers.py b/chb/api/FunctionQualifiers.py new file mode 100644 index 00000000..202e1066 --- /dev/null +++ b/chb/api/FunctionQualifiers.py @@ -0,0 +1,88 @@ +# ------------------------------------------------------------------------------ +# CodeHawk Binary Analyzer +# Author: Henny Sipma +# ------------------------------------------------------------------------------ +# The MIT License (MIT) +# +# 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 +# in the Software without restriction, including without limitation the rights +# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +# copies of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be included in all +# copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. +# ------------------------------------------------------------------------------ + + +from typing import List, Optional, TYPE_CHECKING + +from chb.api.InterfaceDictionaryRecord import InterfaceDictionaryRecord + +import chb.util.fileutil as UF + +from chb.util.IndexedTable import IndexedTableValue + +if TYPE_CHECKING: + from chb.api.InterfaceDictionary import InterfaceDictionary + from chb.api.XXPredicate import XXPredicate + + +class FunctionQualifiers(InterfaceDictionaryRecord): + + def __init__( + self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None: + InterfaceDictionaryRecord.__init__(self, ixd, ixval) + + def _optional_bool(self, index: int) -> Optional[bool]: + r = self.args[index] + if r == 2: + return True + elif r == 1: + return False + else: + return None + + @property + def fq_noreturn(self) -> Optional[bool]: + return self._optional_bool(0) + + @property + def fq_functional(self) -> Optional[str]: + r = self.args[1] + if r == 2: + return "FConst" + elif r == 1: + return "FPure" + else: + return None + + @property + def fq_sets_errno(self) -> Optional[bool]: + return self._optional_bool(2) + + @property + def fq_must_use_return(self) -> Optional[bool]: + return self._optional_bool(3) + + def __str__(self) -> str: + return ( + ("fq_noreturn: " + str(self.fq_noreturn) + "; " + if self.fq_noreturn is not None else "") + + ("fq_functional: " + str(self.fq_functional) + "; " + if self.fq_functional is not None else "") + + ("fq_sets_errno: " + str(self.fq_sets_errno) + "; " + if self.fq_sets_errno is not None else "") + + ("fq_must_use_return: " + str(self.fq_must_use_return) + ";" + if self.fq_must_use_return is not None else "")) diff --git a/chb/api/InterfaceDictionary.py b/chb/api/InterfaceDictionary.py index 15048605..30600a40 100644 --- a/chb/api/InterfaceDictionary.py +++ b/chb/api/InterfaceDictionary.py @@ -40,6 +40,7 @@ from chb.api.AppFunctionSignature import AppFunctionSignature from chb.api.CallTarget import CallTarget from chb.api.FunctionStub import FunctionStub +from chb.api.FunctionQualifiers import FunctionQualifiers from chb.api.XXPredicate import XXPredicate from chb.api.InterfaceDictionaryRecord import apiregistry @@ -67,6 +68,7 @@ def __init__( IT.IndexedTable("parameter-location-list-table")) self.fts_parameter_list_table = IT.IndexedTable("fts-parameter-list-table") self.fts_parameter_table = IT.IndexedTable("fts-parameter-table") + self.function_qualifiers_table = IT.IndexedTable("function-qualifiers-table") self.function_interface_table = IT.IndexedTable("function-interface-table") self.function_semantics_table = IT.IndexedTable("function-semantics-table") self.function_signature_table = IT.IndexedTable("function-signature-table") @@ -78,6 +80,7 @@ def __init__( self.parameter_location_list_table, self.function_stub_table, self.call_target_table, + self.function_qualifiers_table, self.function_interface_table, self.function_semantics_table, self.function_signature_table, @@ -119,6 +122,10 @@ def call_target(self, ix: int) -> CallTarget: return apiregistry.mk_instance( self, self.call_target_table.retrieve(ix), CallTarget) + def function_qualifiers(self, ix: int) -> FunctionQualifiers: + return FunctionQualifiers( + self, self.function_qualifiers_table.retrieve(ix)) + def function_interface(self, ix: int) -> AppFunctionInterface: return AppFunctionInterface( self, self.function_interface_table.retrieve(ix)) diff --git a/chb/api/XXPredicate.py b/chb/api/XXPredicate.py index 37cdca3f..f782e11f 100644 --- a/chb/api/XXPredicate.py +++ b/chb/api/XXPredicate.py @@ -65,10 +65,6 @@ def is_xp_buffer(self) -> bool: def is_xp_enum(self) -> bool: return False - @property - def is_xp_constant_false(self) -> bool: - return False - @property def is_xp_freed(self) -> bool: return False @@ -157,10 +153,6 @@ def is_xp_relational_expr(self) -> bool: def is_xp_sets_errno(self) -> bool: return False - @property - def is_xp_starts_thread(self) -> bool: - return False - @property def is_xp_tainted(self) -> bool: return False @@ -341,22 +333,6 @@ def __str__(self) -> str: + ")") -@apiregistry.register_tag("f", XXPredicate) -class XXPFalse(XXPredicate): - """Constant false predicate.""" - - def __init__( - self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None: - XXPredicate.__init__(self, ixd, ixval) - - @property - def is_xp_constant_false(self) -> bool: - return True - - def __str__(self) -> str: - return "false" - - @apiregistry.register_tag("fr", XXPredicate) class XXPFreed(XXPredicate): """Pointer to memory region has been freed. @@ -380,22 +356,6 @@ def __str__(self) -> str: return "freed(" + str(self.pointer) + ")" -@apiregistry.register_tag("fn", XXPredicate) -class XXPFunctional(XXPredicate): - """Function has no side effects.""" - - def __init__( - self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None: - XXPredicate.__init__(self, ixd, ixval) - - @property - def is_xp_functional(self) -> bool: - return True - - def __str__(self) -> str: - return "functional" - - @apiregistry.register_tag("fp", XXPredicate) class XXPFunctionPointer(XXPredicate): """Term is address of a function. @@ -878,22 +838,6 @@ def __str__(self) -> str: + str(self.term2)) -@apiregistry.register_tag("errno", XXPredicate) -class XXPSetsErrno(XXPredicate): - """Function sets errno.""" - - def __init__( - self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None: - XXPredicate.__init__(self, ixd, ixval) - - @property - def is_xp_sets_errno(self) -> bool: - return True - - def __str__(self) -> str: - return "sets-errno" - - @apiregistry.register_tag("st", XXPredicate) class XXPStartsThread(XXPredicate): """Starts thread indicated by pointer with given arguments. diff --git a/chb/app/CHVersion.py b/chb/app/CHVersion.py index 06af1529..f37f2cab 100644 --- a/chb/app/CHVersion.py +++ b/chb/app/CHVersion.py @@ -1,3 +1,3 @@ -chbversion: str = "0.3.0-20260603" +chbversion: str = "0.3.0-20260611" -minimum_required_chb_version = "0.6.0_20260527" +minimum_required_chb_version = "0.6.0_20260611" diff --git a/chb/app/FnProofObligations.py b/chb/app/FnProofObligations.py index 5cd8a204..bc661179 100644 --- a/chb/app/FnProofObligations.py +++ b/chb/app/FnProofObligations.py @@ -159,6 +159,7 @@ def __str__(self) -> str: + str(self.xpo) + " (" + str(self.status) + + m + ")") @@ -192,7 +193,7 @@ def proofobligations(self) -> Dict[str, List[ProofObligation]]: xstatus = xxpo.find("status") if xstatus is not None: status = POStatus(self.xpod, xstatus) - msg = xxpo.get("m", "none") + msg = xstatus.get("m", "none") po = ProofObligation(iaddr, xpo, status, msg) self._store[iaddr].append(po) return self._store diff --git a/chb/app/XPOPredicate.py b/chb/app/XPOPredicate.py index fa1b7998..58866ff5 100644 --- a/chb/app/XPOPredicate.py +++ b/chb/app/XPOPredicate.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 @@ -64,18 +64,10 @@ def is_xpo_buffer(self) -> bool: def is_xpo_enum(self) -> bool: return False - @property - def is_xpo_constant_false(self) -> bool: - return False - @property def is_xpo_freed(self) -> bool: return False - @property - def is_xpo_functional(self) -> bool: - return False - @property def is_xpo_function_pointer(self) -> bool: return False @@ -152,10 +144,6 @@ def is_xpo_positive(self) -> bool: def is_xpo_relational_expr(self) -> bool: return False - @property - def is_xpo_sets_errno(self) -> bool: - return False - @property def is_xpo_starts_thread(self) -> bool: return False @@ -316,22 +304,6 @@ def __str__(self) -> str: + ")") -@xporegistry.register_tag("f", XPOPredicate) -class XPOPFalse(XPOPredicate): - """Constant false predicate.""" - - def __init__( - self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: - XPOPredicate.__init__(self, xpod, ixval) - - @property - def is_xpo_constant_false(self) -> bool: - return True - - def __str__(self) -> str: - return "false" - - @xporegistry.register_tag("fr", XPOPredicate) class XPOFreed(XPOPredicate): """Pointer to memory region has been freed. @@ -355,21 +327,6 @@ def __str__(self) -> str: return "freed(" + str(self.pointer) + ")" -@xporegistry.register_tag("fn", XPOPredicate) -class XPOFunctional(XPOPredicate): - - def __init__( - self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: - XPOPredicate.__init__(self, xpod, ixval) - - @property - def is_xpo_functional(self) -> bool: - return True - - def __str__(self) -> str: - return "functional" - - @xporegistry.register_tag("fp", XPOPredicate) class XPOFunctionPointer(XPOPredicate): """Expression is address of a function. @@ -996,6 +953,37 @@ def __str__(self) -> str: + ")") +@xporegistry.register_tag("tfa", XPOPredicate) +class XPOTrustedOsCmdFmtArgString(XPOPredicate): + """Expression is trusted as argument for a format string-constructed command. + + 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_arg_string(self) -> bool: + return True + + @property + def expr(self) -> "XXpr": + return self.xd.xpr(self.args[0]) + + @property + def optlen(self) -> Optional["XXpr"]: + if self.args[1] == -1: + return None + return self.xd.xpr(self.args[1]) + + def __str__(self) -> str: + return ( + "trusted-os-cmd-fmt-arg-string(" + + str(self.expr)) + + @xporegistry.register_tag("v", XPOPredicate) class XPOValidMem(XPOPredicate): """Expression points to valid memory. diff --git a/chb/bctypes/TypeConstraint.py b/chb/bctypes/TypeConstraint.py index 911b9e90..817f12dc 100644 --- a/chb/bctypes/TypeConstraint.py +++ b/chb/bctypes/TypeConstraint.py @@ -389,6 +389,39 @@ def __str__(self) -> str: return "deref" +@tcdregistry.register_tag("fofs", TypeCapLabel) +class TypeCapLabelFOutputFormatString(TypeCapLabel): + + def __init__( + self, + tcd: "TypeConstraintDictionary", + ixval: IndexedTableValue) -> None: + TypeCapLabel.__init__(self, tcd, ixval) + + @property + def is_output_format_string(self) -> bool: + return True + + def __str__(self) -> str: + return "output-format-string" + + +@tcdregistry.register_tag("fifs", TypeCapLabel) +class TypeCapLabelFInputFormatString(TypeCapLabel): + + def __init__( + self, + tcd: "TypeConstraintDictionary", + ixval: IndexedTableValue) -> None: + TypeCapLabel.__init__(self, tcd, ixval) + + @property + def is_input_format_string(self) -> bool: + return True + + def __str__(self) -> str: + return "input-format-string" + @tcdregistry.register_tag("a", TypeCapLabel) class TypeCapLabelOffsetAccess(TypeCapLabel): @@ -463,7 +496,6 @@ def __str__(self) -> str: return "stackaddr_" + str(self.offset) - class TypeVariable(TypeConstraintDictionaryRecord): def __init__( diff --git a/chb/summaries/bchsummaries.jar b/chb/summaries/bchsummaries.jar index 0bf72b52..49259b27 100644 Binary files a/chb/summaries/bchsummaries.jar and b/chb/summaries/bchsummaries.jar differ