From 5170d0a71125a377b89cbd5b4bd8fbd0bf0e3b2c Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 25 Jun 2026 18:53:01 -0700 Subject: [PATCH] add predicates and frozen variable --- chb/api/XXPredicate.py | 42 +++++++++++++++++++++++- chb/app/CHVersion.py | 2 +- chb/app/XPOPredicate.py | 11 ++++++- chb/invariants/VConstantValueVariable.py | 37 ++++++++++++++++++++- chb/invariants/XVariable.py | 7 ++++ chb/invariants/XXprUtil.py | 21 +++++++++++- chb/userdata/UserHints.py | 6 ++++ 7 files changed, 121 insertions(+), 5 deletions(-) diff --git a/chb/api/XXPredicate.py b/chb/api/XXPredicate.py index f782e11f..5d336416 100644 --- a/chb/api/XXPredicate.py +++ b/chb/api/XXPredicate.py @@ -141,6 +141,10 @@ def is_xp_null_terminated(self) -> bool: def is_xp_output_formatstring(self) -> bool: return False + @property + def is_xp_restricted_output_formatstring(self) -> bool: + return False + @property def is_xp_positive(self) -> bool: return False @@ -777,6 +781,42 @@ def __str__(self) -> str: return "output-formatstring(" + str(self.pointer) + ")" +@apiregistry.register_tag("rofs", XXPredicate) +class XXPRestrictedOutFormatString(XXPredicate): + """Term points to a restricted format string for output (printf) + + A restricted output format string is a format string with a specific sequence of + format specifiers. + + args[0]: index of pointer in interfacedictionary + """ + + def __init__( + self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None: + XXPredicate.__init__(self, ixd, ixval) + + @property + def is_xp_restricted_output_formatstring(self) -> bool: + return True + + @property + def pointer(self) -> "BTerm": + return self.id.bterm(self.args[0]) + + @property + def specifiers(self) -> List[str]: + return [self.bd.string(i) for i in self.args[1:]] + + def __str__(self) -> str: + return ( + "restricted-output-formatstring(" + + str(self.pointer) + + ", " + + ", ".join(self.specifiers) + + ")" + ) + + @apiregistry.register_tag("pos", XXPredicate) class XXPPositive(XXPredicate): """Term is positive. @@ -1008,7 +1048,7 @@ def optlen(self) -> Optional["BTerm"]: def __str__(self) -> str: return ( - "trusted-os-cmd-fmt-string(" + "trusted-os-cmd-fmt-arg-string(" + str(self.fmt) + ", " + self.quotes diff --git a/chb/app/CHVersion.py b/chb/app/CHVersion.py index f54d8706..45357d1a 100644 --- a/chb/app/CHVersion.py +++ b/chb/app/CHVersion.py @@ -1,3 +1,3 @@ -chbversion: str = "0.3.0-20260619" +chbversion: str = "0.3.0-20260625" minimum_required_chb_version = "0.6.0_20260617" diff --git a/chb/app/XPOPredicate.py b/chb/app/XPOPredicate.py index 89039d01..0b095b85 100644 --- a/chb/app/XPOPredicate.py +++ b/chb/app/XPOPredicate.py @@ -1004,6 +1004,10 @@ def is_xpo_trusted_os_cmd_fmt_arg_string(self) -> bool: def expr(self) -> "XXpr": return self.xd.xpr(self.args[0]) + @property + def quotes(self) -> str: + return self.tags[1] + @property def optlen(self) -> Optional["XXpr"]: if self.args[1] == -1: @@ -1013,7 +1017,12 @@ def optlen(self) -> Optional["XXpr"]: def __str__(self) -> str: return ( "trusted-os-cmd-fmt-arg-string(" - + str(self.expr)) + + str(self.expr) + + ", " + + str(self.quotes) + + ", " + + str(self.optlen) + + ")") @xporegistry.register_tag("v", XPOPredicate) diff --git a/chb/invariants/VConstantValueVariable.py b/chb/invariants/VConstantValueVariable.py index e998202b..6947f81f 100644 --- a/chb/invariants/VConstantValueVariable.py +++ b/chb/invariants/VConstantValueVariable.py @@ -6,7 +6,7 @@ # # Copyright (c) 2016-2020 Kestrel Technology LLC # Copyright (c) 2020 Henny Sipma -# Copyright (c) 2021-2025 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 @@ -139,6 +139,10 @@ def is_function_return_value(self) -> bool: def is_typecast_value(self) -> bool: return False + @property + def is_frozen_value(self) -> bool: + return False + @property def is_symbolic_value(self) -> bool: return False @@ -479,6 +483,37 @@ def __str__(self) -> str: + '_@_' + str(self.jump_addr)) +@varregistry.register_tag("frv", VConstantValueVariable) +class VFrozenValue(VConstantValueVariable): + """Value of a test at an earlier instruction. + + tags[1]: address of test instruction + tags[2]: address of conditional jump instruction + args[0]: index of variable in xprdictionary + """ + + def __init__( + self, + vd: "FnVarDictionary", + ixval: IndexedTableValue) -> None: + VConstantValueVariable.__init__(self, vd, ixval) + + @property + def is_frozen_value(self) -> bool: + return True + + @property + def variable(self) -> "XVariable": + return self.xd.variable(self.args[0]) + + @property + def iaddr(self) -> str: + return self.tags[1] + + def __str__(self) -> str: + return (str(self.variable) + '_@val_' + str(self.iaddr)) + + @varregistry.register_tag("bv", VConstantValueVariable) class VBridgeVariable(VConstantValueVariable): """Variable that represents a call argument. diff --git a/chb/invariants/XVariable.py b/chb/invariants/XVariable.py index 9b64304d..97cc93f1 100644 --- a/chb/invariants/XVariable.py +++ b/chb/invariants/XVariable.py @@ -134,6 +134,13 @@ def is_typecast_value(self) -> bool: and self.denotation.is_auxiliary_variable and self.denotation.auxvar.is_typecast_value) + @property + def is_frozen_value(self) -> bool: + return ( + self.has_denotation() + and self.denotation.is_auxiliary_variable + and self.denotation.auxvar.is_frozen_value) + @property def is_symbolic_expr_value(self) -> bool: return ( diff --git a/chb/invariants/XXprUtil.py b/chb/invariants/XXprUtil.py index 855efea8..a4c4e5fc 100644 --- a/chb/invariants/XXprUtil.py +++ b/chb/invariants/XXprUtil.py @@ -113,7 +113,7 @@ VMemoryVariable, VAuxiliaryVariable, VRegisterVariable) from chb.invariants.VConstantValueVariable import ( VInitialRegisterValue, VInitialMemoryValue, VFunctionReturnValue, - VTypeCastValue, SideEffectValue, SymbolicValue) + VFrozenValue, VTypeCastValue, SideEffectValue, SymbolicValue) from chb.invariants.VMemoryBase import ( VMemoryBase, VMemoryBaseBaseVar, @@ -1053,6 +1053,25 @@ def xvariable_to_ast_def_lval_expression( str(tcvar), iaddr) return astree.mk_temp_lval_expression() + if xvar.is_frozen_value: + frvar = cast("VFrozenValue", xvar.denotation.auxvar) + variaddr = frvar.iaddr + frvarreg = frvar.variable + if variaddr in astree.ssa_intros and str(frvarreg) in astree.ssa_intros[variaddr]: + vinfo = astree.ssa_intros[variaddr][str(frvarreg)] + ssavalue = astree.get_ssa_value(vinfo.vname) + if ssavalue is not None: + return ssavalue + else: + return astree.mk_vinfo_lval_expression( + vinfo, anonymous=anonymous) + if not anonymous: + chklogger.logger.error( + "AST def conversion of frozen value %s to lval at address %s " + + "not yet supported", + str(frvar), iaddr) + return astree.mk_temp_lval_expression() + if xvar.is_sideeffect_value: sevar = cast("SideEffectValue", xvar.denotation.auxvar) argloc = sevar.argument_location diff --git a/chb/userdata/UserHints.py b/chb/userdata/UserHints.py index cf2efe86..65f9ae33 100644 --- a/chb/userdata/UserHints.py +++ b/chb/userdata/UserHints.py @@ -486,6 +486,10 @@ def typename(self) -> Optional[str]: def ispointerto(self) -> bool: return "ptrto" in self.mods + @property + def isfreeze(self) -> bool: + return "freeze" in self.mods + @property def mods(self) -> List[str]: return cast(List[str], self.varintro.get("mods", [])) @@ -504,6 +508,8 @@ def to_xml(self, node: ET.Element) -> None: xvintro.set("ptrto", "yes") if self.has_cast(): xvintro.set("cast", "yes") + if self.isfreeze: + xvintro.set("freeze", "yes") def __str__(self) -> str: return (