From cba47b228aff54569a3f923f99b52298cb65d921 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Fri, 24 Oct 2025 18:20:01 -0700 Subject: [PATCH 01/22] CMD: add command-line option to control status of system includes --- chc/app/CApplication.py | 15 +++++++++++ chc/app/CFile.py | 4 +++ chc/app/CFileGlobals.py | 14 +++++++++++ chc/app/CHVersion.py | 2 +- chc/cmdline/AnalysisManager.py | 21 ++++++++-------- chc/cmdline/ParseManager.py | 16 ++++++------ chc/cmdline/c_file/cfileutil.py | 36 ++++++++++++++++++++++----- chc/cmdline/c_project/cprojectutil.py | 15 +++++++---- chc/cmdline/chkc | 20 +++++++++++++++ 9 files changed, 112 insertions(+), 31 deletions(-) diff --git a/chc/app/CApplication.py b/chc/app/CApplication.py index 39e4fa9..6163c29 100644 --- a/chc/app/CApplication.py +++ b/chc/app/CApplication.py @@ -93,12 +93,14 @@ def __init__( targetpath: str, contractpath: str, singlefile: bool = False, + keep_system_includes: bool = False, excludefiles: List[str] = []) -> None: self._projectpath = projectpath self._projectname = projectname self._targetpath = targetpath self._contractpath = contractpath self._singlefile = singlefile + self._keep_system_includes = keep_system_includes self._excludefiles = excludefiles self._indexmanager = IndexManager(singlefile) self._globalcontract: Optional[CGlobalContract] = None @@ -138,6 +140,19 @@ def globalcontract(self) -> CGlobalContract: def is_singlefile(self) -> bool: return self._singlefile + @property + def keep_system_includes(self) -> bool: + """Returns true if functions from the system path ('/') must be included + + This property is false by default and must be enabled via a command-line + option. + + It is intended to, by default, filter out functions defined in header + files, that would otherwise be included in every source file. + """ + + return self._keep_system_includes + @property def excludefiles(self) -> List[str]: return self._excludefiles diff --git a/chc/app/CFile.py b/chc/app/CFile.py index 4a4e0a0..d70d40d 100644 --- a/chc/app/CFile.py +++ b/chc/app/CFile.py @@ -154,6 +154,10 @@ def name(self) -> str: def capp(self) -> "CApplication": return self._capp + @property + def keep_system_includes(self) -> bool: + return self.capp.keep_system_includes + @property def targetpath(self) -> str: return self.capp.targetpath diff --git a/chc/app/CFileGlobals.py b/chc/app/CFileGlobals.py index a908803..8ae7527 100644 --- a/chc/app/CFileGlobals.py +++ b/chc/app/CFileGlobals.py @@ -179,6 +179,10 @@ def __init__(self, cfile: "CFile", xnode: ET.Element) -> None: def cfile(self) -> "CFile": return self._cfile + @property + def keep_system_includes(self) -> bool: + return self.cfile.keep_system_includes + @property def declarations(self) -> "CFileDeclarations": return self.cfile.declarations @@ -284,6 +288,16 @@ def gfunctions(self) -> Dict[int, CGFunction]: xiloc = xf.get("iloc") if xivinfo is not None and xiloc is not None: vinfo = self.declarations.get_varinfo(int(xivinfo)) + if ( + not self.keep_system_includes + and vinfo.vdecl is not None + and vinfo.vdecl.file.startswith("/")): + chklogger.logger.info( + "%s: Skip system function %s defined in %s", + self.cfile.cfilename, + vinfo.vname, + vinfo.vdecl.file) + continue loc = self.declarations.get_location(int(xiloc)) gfun = CGFunction(loc, vinfo) self._gfunctions[vinfo.vid] = gfun diff --git a/chc/app/CHVersion.py b/chc/app/CHVersion.py index 61e0a46..ced4e23 100644 --- a/chc/app/CHVersion.py +++ b/chc/app/CHVersion.py @@ -1 +1 @@ -chcversion: str = "0.2.0-2024-11-04" +chcversion: str = "0.2.0-2025-10-24" diff --git a/chc/cmdline/AnalysisManager.py b/chc/cmdline/AnalysisManager.py index 7cc56a2..99c8d4e 100644 --- a/chc/cmdline/AnalysisManager.py +++ b/chc/cmdline/AnalysisManager.py @@ -54,7 +54,7 @@ def __init__( wordsize: int = 0, unreachability: bool = False, thirdpartysummaries: List[str] = [], - nofilter: bool = True, + keep_system_includes: bool = False, verbose: bool = False, ) -> None: """Initialize the analyzer location and target file location. @@ -72,13 +72,8 @@ def __init__( """ self._capp = capp - # self.contractpath = capp.contractpath self._config = Config() - # self.chsummaries = self.config.summaries - # self.path = self.capp.path - # self.canalyzer = self.config.canalyzer - # self.gui = self.config.chc_gui - self.nofilter = nofilter + self._keep_system_includes = keep_system_includes self.wordsize = wordsize self.thirdpartysummaries = thirdpartysummaries self.unreachability = unreachability @@ -88,6 +83,10 @@ def __init__( def capp(self) -> "CApplication": return self._capp + @property + def keep_system_includes(self) -> bool: + return self._keep_system_includes + @property def contractpath(self) -> Optional[str]: return self.capp.contractpath @@ -189,8 +188,8 @@ def _create_file_primary_proofobligations_cmd_partial(self) -> List[str]: cmd.extend(["-contractpath", self.contractpath]) cmd.extend(["-projectname", self.capp.projectname]) - if self.nofilter: - cmd.append("-nofilter") + if self.keep_system_includes: + cmd.append("-keep_system_includes") if self.wordsize > 0: cmd.extend(["-wordsize", str(self.wordsize)]) cmd.append(self.targetpath) @@ -283,8 +282,8 @@ def _generate_and_check_file_cmd_partial( if not (self.contractpath is None): cmd.extend(["-contractpath", self.contractpath]) cmd.extend(["-projectname", self.capp.projectname]) - if self.nofilter: - cmd.append("-nofilter") + if self.keep_system_includes: + cmd.append("-keep_system_includes") if self.wordsize > 0: cmd.extend(["-wordsize", str(self.wordsize)]) if self.unreachability: diff --git a/chc/cmdline/ParseManager.py b/chc/cmdline/ParseManager.py index f41df19..b082db3 100644 --- a/chc/cmdline/ParseManager.py +++ b/chc/cmdline/ParseManager.py @@ -72,7 +72,7 @@ def __init__( projectpath: str, projectname: str, targetpath: str, - filter: bool = False, + keep_system_includes: bool = False, posix: bool = False, verbose: bool = True, keepUnused: bool = False, @@ -96,7 +96,7 @@ def __init__( self._targetpath, self._projectname) self._analysisresultspath = UF.get_analysisresults_path( self._targetpath, self._projectname) - self._filter = filter + self._keep_system_includes = keep_system_includes self._posix = posix self._keepUnused = keepUnused self._verbose = verbose @@ -160,8 +160,8 @@ def tgtplatform(self) -> str: return self._tgtplatform @property - def filter(self) -> bool: - return self._filter + def keep_system_includes(self) -> bool: + return self._keep_system_includes @property def posix(self) -> bool: @@ -439,8 +439,8 @@ def parse_with_ccommands( "-targetdirectory", self.analysisresultspath ] - if not self.filter: - command.append("-nofilter") + if self.keep_system_includes: + command.append("-keep_system_includes") if self.keepUnused: command.append("-keepUnused") command.append(ifilename) @@ -533,8 +533,8 @@ def parse_ifile(self, ifilename: str) -> int: "-targetdirectory", self.analysisresultspath, ] - if not self.filter: - cmd.append("-nofilter") + if not self.keep_system_includes: + cmd.append("-keep_system_includes") if self.keepUnused: cmd.append("-keepUnused") cmd.append(ifilename) diff --git a/chc/cmdline/c_file/cfileutil.py b/chc/cmdline/c_file/cfileutil.py index c8cd8e9..38d5ba8 100644 --- a/chc/cmdline/c_file/cfileutil.py +++ b/chc/cmdline/c_file/cfileutil.py @@ -117,6 +117,7 @@ def cfile_parse_file(args: argparse.Namespace) -> NoReturn: # arguments pcfilename: str = os.path.abspath(args.filename) opttgtpath: Optional[str] = args.tgtpath + keep_system_includes: bool = args.keep_system_includes loglevel: str = args.loglevel logfilename: Optional[str] = args.logfilename logfilemode: str = args.logfilemode @@ -154,7 +155,8 @@ def cfile_parse_file(args: argparse.Namespace) -> NoReturn: chklogger.logger.info("Target path: %s", targetpath) - parsemanager = ParseManager(projectpath, projectname, targetpath) + parsemanager = ParseManager( + projectpath, projectname, targetpath, keep_system_includes=keep_system_includes) parsemanager.remove_semantics() parsemanager.initialize_paths() @@ -418,6 +420,7 @@ def cfile_analyze_file(args: argparse.Namespace) -> NoReturn: xcfilename: str = args.filename opttgtpath: Optional[str] = args.tgtpath wordsize: int = args.wordsize + keep_system_includes: bool = args.keep_system_includes verbose: bool = args.verbose loglevel: str = args.loglevel logfilename: Optional[str] = args.logfilename @@ -468,12 +471,21 @@ def cfile_analyze_file(args: argparse.Namespace) -> NoReturn: contractpath = os.path.join(targetpath, "chc_contracts") capp = CApplication( - projectpath, projectname, targetpath, contractpath, singlefile=True) + projectpath, + projectname, + targetpath, + contractpath, + singlefile=True, + keep_system_includes=keep_system_includes) capp.initialize_single_file(cfilename) cfile = capp.get_cfile() - am = AnalysisManager(capp, verbose=verbose, wordsize=wordsize) + am = AnalysisManager( + capp, + verbose=verbose, + wordsize=wordsize, + keep_system_includes=keep_system_includes) am.create_file_primary_proofobligations(cfilename) am.reset_tables(cfile) @@ -578,6 +590,7 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn: # arguments pcfilename: str = os.path.abspath(args.filename) opttgtpath: Optional[str] = args.tgtpath + keep_system_includes: bool = args.keep_system_includes cshowcode: bool = args.showcode copen: bool = args.open cshowinvariants: bool = args.showinvariants @@ -622,7 +635,8 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn: chklogger.logger.info("Target path: %s", targetpath) - parsemanager = ParseManager(projectpath, projectname, targetpath) + parsemanager = ParseManager( + projectpath, projectname, targetpath, keep_system_includes=keep_system_includes) parsemanager.remove_semantics() parsemanager.initialize_paths() @@ -672,7 +686,12 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn: contractpath = os.path.join(targetpath, "chc_contracts") capp = CApplication( - projectpath, projectname, targetpath, contractpath, singlefile=True) + projectpath, + projectname, + targetpath, + contractpath, + singlefile=True, + keep_system_includes=keep_system_includes) capp.initialize_single_file(cfilename) cfile = capp.get_cfile() @@ -695,7 +714,12 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn: chklogger.logger.info("cfile analyze completed") capp = CApplication( - projectpath, projectname, targetpath, contractpath, singlefile=True) + projectpath, + projectname, + targetpath, + contractpath, + singlefile=True, + keep_system_includes=keep_system_includes) capp.initialize_single_file(cfilename) cfile = capp.get_cfile() diff --git a/chc/cmdline/c_project/cprojectutil.py b/chc/cmdline/c_project/cprojectutil.py index b821477..553f254 100644 --- a/chc/cmdline/c_project/cprojectutil.py +++ b/chc/cmdline/c_project/cprojectutil.py @@ -68,7 +68,7 @@ def print_error(m: str) -> None: sys.stderr.write(("*" * 80) + "\n") - sys.stderr.write(m + "\n") + sys.stderr.write("F:" + m + "\n") sys.stderr.write(("*" * 80) + "\n") @@ -110,6 +110,7 @@ def cproject_parse_project(args: argparse.Namespace) -> NoReturn: projectpath: str = args.path projectname: str = args.projectname opttgtpath: Optional[str] = args.tgtpath + keep_system_includes: bool = args.keep_system_includes loglevel: str = args.loglevel logfilename: Optional[str] = args.logfilename logfilemode: str = args.logfilemode @@ -156,7 +157,8 @@ def cproject_parse_project(args: argparse.Namespace) -> NoReturn: print_error("The compile_commands.json file was found empty") exit(1) - parsemanager = ParseManager(projectpath, projectname, targetpath) + parsemanager = ParseManager( + projectpath, projectname, targetpath, keep_system_includes=keep_system_includes) parsemanager.remove_semantics() parsemanager.initialize_paths() parsemanager.parse_with_ccommands(compilecommands, copyfiles=True) @@ -423,6 +425,7 @@ def cproject_analyze_project(args: argparse.Namespace) -> NoReturn: # arguments tgtpath: str = args.tgtpath projectname: str = args.projectname + keep_system_includes: bool = args.keep_system_includes maxprocesses: int = args.maxprocesses loglevel: str = args.loglevel logfilename: Optional[str] = args.logfilename @@ -458,6 +461,7 @@ def cproject_analyze_project(args: argparse.Namespace) -> NoReturn: projectname, targetpath, contractpath, + keep_system_includes=keep_system_includes, excludefiles=excludefiles) def save_xrefs(f: "CFile") -> None: @@ -475,9 +479,10 @@ def save_xrefs(f: "CFile") -> None: projectname, targetpath, contractpath, + keep_system_includes=keep_system_includes, excludefiles=excludefiles) - am = AnalysisManager(capp, verbose=True) + am = AnalysisManager(capp, verbose=True, keep_system_includes=keep_system_includes) with timing("analysis"): @@ -490,13 +495,13 @@ def save_xrefs(f: "CFile") -> None: exit(1) for i in range(1): - am.generate_and_check_app("llrvisp", processes=maxprocesses) + am.generate_and_check_app("visp", processes=maxprocesses) capp.reinitialize_tables() capp.update_spos() for i in range(5): capp.update_spos() - am.generate_and_check_app("llrvisp", processes=maxprocesses) + am.generate_and_check_app("visp", processes=maxprocesses) capp.reinitialize_tables() timestamp = os.stat(UF.get_cchpath(targetpath, projectname)).st_ctime diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc index cb9113c..7b57951 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -634,6 +634,10 @@ def parse() -> argparse.Namespace: "--tgtpath", help=("directory in which to store the analysis artifacts " + "(default: )")) + cfileparse.add_argument( + "--keep-system-includes", + action="store_true", + help="do not filter out functions from files with absolute file names") cfileparse.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), @@ -720,6 +724,10 @@ def parse() -> argparse.Namespace: type=int, default=32, help="architecture wordsize in bits (16, 32, or 64)") + cfileanalyze.add_argument( + "--keep-system-includes", + action="store_true", + help="do not filter out functions from files with absolute file names") cfileanalyze.add_argument( "--verbose", "-v", action="store_true", @@ -794,6 +802,10 @@ def parse() -> argparse.Namespace: cfilerun.add_argument( "--tgtpath", help="directory to store the analysis results") + cfilerun.add_argument( + "--keep-system-includes", + action="store_true", + help="don't filter out functions from files with absolute filenames") cfilerun.add_argument( "--showcode", action="store_true", @@ -1366,6 +1378,10 @@ def parse() -> argparse.Namespace: "projectname", help="name of the project") cprojectparse.add_argument( "--tgtpath", help="directory to save the results") + cprojectparse.add_argument( + "--keep-system-includes", + action="store_true", + help="don't filter out functions from files with absolute filenames") cprojectparse.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), @@ -1454,6 +1470,10 @@ def parse() -> argparse.Namespace: "tgtpath", help="directory that contains the analysis results") cprojectanalyze.add_argument( "projectname", help="name of the project") + cprojectanalyze.add_argument( + "--keep-system-includes", + action="store_true", + help="don't filter out functions from files with absolute filenames") cprojectanalyze.add_argument( "--maxprocesses", help="number of files to process in parallel", From 6f974719de33e12e2417c319625c322f88ec2632 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 8 Nov 2025 18:49:44 -0800 Subject: [PATCH 02/22] PROOF: add support for output-parameter predicates --- chc/proof/CFilePredicateDictionary.py | 4 + chc/proof/CFilePredicateRecord.py | 7 +- chc/proof/CFunctionProofs.py | 23 ++++- chc/proof/CPOPredicate.py | 129 ++++++++++++++++++++++++++ 4 files changed, 161 insertions(+), 2 deletions(-) diff --git a/chc/proof/CFilePredicateDictionary.py b/chc/proof/CFilePredicateDictionary.py index 75368c5..141b7d2 100644 --- a/chc/proof/CFilePredicateDictionary.py +++ b/chc/proof/CFilePredicateDictionary.py @@ -194,6 +194,10 @@ def f(index: int, tags: List[str], args: List[int]) -> PO.CPOPredicate: p = cast(PO.CPOInitialized, p) args = [self.dictionary.index_lval(p.lval, subst=subst)] + elif p.is_locally_initialized: + p = cast(PO.CPOLocallyInitialized, p) + args = [self.dictionary.index_lval(p.lval, subst=subst)] + elif p.is_initialized_range: p = cast(PO.CPOInitializedRange, p) args = [ diff --git a/chc/proof/CFilePredicateRecord.py b/chc/proof/CFilePredicateRecord.py index 05e37d9..1e7e9f9 100644 --- a/chc/proof/CFilePredicateRecord.py +++ b/chc/proof/CFilePredicateRecord.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -37,6 +37,7 @@ if TYPE_CHECKING: from chc.app.CDictionary import CDictionary from chc.app.CFile import CFile + from chc.app.CFileDeclarations import CFileDeclarations from chc.proof.CFilePredicateDictionary import CFilePredicateDictionary @@ -59,6 +60,10 @@ def pd(self) -> "CFilePredicateDictionary": def cd(self) -> "CDictionary": return self.pd.dictionary + @property + def cdeclarations(self) -> "CFileDeclarations": + return self.cfile.declarations + @property def cfile(self) -> "CFile": return self.pd.cfile diff --git a/chc/proof/CFunctionProofs.py b/chc/proof/CFunctionProofs.py index c4e0187..91ce44c 100644 --- a/chc/proof/CFunctionProofs.py +++ b/chc/proof/CFunctionProofs.py @@ -30,7 +30,7 @@ import xml.etree.ElementTree as ET -from typing import Callable, List, Optional, TYPE_CHECKING +from typing import Callable, cast, List, Optional, TYPE_CHECKING from chc.proof.CFunctionCallsiteSPOs import CFunctionCallsiteSPOs from chc.proof.CFunctionPO import CFunctionPO @@ -44,6 +44,10 @@ from chc.app.CApplication import CApplication from chc.app.CFile import CFile from chc.app.CFunction import CFunction + from chc.proof.CPOPredicate import ( + CPOLocallyInitialized, + CPOOutputParameterInitialized, + CPOOutputParameterUnaltered) class CFunctionProofs: @@ -240,6 +244,23 @@ def _get_spos(self, force=False): + self.cfile.name ) + def get_output_parameter_ppos(self, vname: str) -> List[CFunctionPO]: + result: List[CFunctionPO] = [] + for ppo in self.ppolist: + if ppo.predicate.is_locally_initialized: + vinfo = cast("CPOLocallyInitialized", ppo.predicate).varinfo + if vinfo.vname == vname: + result.append(ppo) + elif ppo.predicate.is_output_parameter_initialized: + vinfo = cast("CPOOutputParameterInitialized", ppo.predicate).varinfo + if vinfo.vname == vname: + result.append(ppo) + elif ppo.predicate.is_output_parameter_unaltered: + vinfo = cast("CPOOutputParameterUnaltered", ppo.predicate).varinfo + if vinfo.vname == vname: + result.append(ppo) + return result + def _save_spos(self, cnode: ET.Element) -> None: UF.save_spo_file( self.targetpath, diff --git a/chc/proof/CPOPredicate.py b/chc/proof/CPOPredicate.py index bc2335e..47b49f6 100644 --- a/chc/proof/CPOPredicate.py +++ b/chc/proof/CPOPredicate.py @@ -40,7 +40,9 @@ from chc.app.CExp import CExp, CExpLval from chc.app.CLHost import CLHostVar from chc.app.CLval import CLval + from chc.app.COffset import COffset from chc.app.CTyp import CTyp + from chc.app.CVarInfo import CVarInfo from chc.proof.CFilePredicateDictionary import CFilePredicateDictionary @@ -71,12 +73,15 @@ 'iu': 'int-underflow', 'iub': 'index-upper-bound', 'lb': 'lower-bound', + 'li': 'locally-initialized', 'nm': 'new-memory', 'nn': 'not-null', 'nneg': 'non-negative', 'no': 'no-overlap', 'nt': 'null-terminated', 'null': 'null', + 'opi': 'output_parameter-initialized', + 'opu': 'output_parameter-unaltered', 'pc': 'pointer-cast', 'plb': 'ptr-lower-bound', 'pre': 'precondition', @@ -180,6 +185,10 @@ def is_index_upper_bound(self) -> bool: def is_initialized(self) -> bool: return False + @property + def is_locally_initialized(self) -> bool: + return False + @property def is_initialized_range(self) -> bool: return False @@ -224,6 +233,14 @@ def is_null(self) -> bool: def is_null_terminated(self) -> bool: return False + @property + def is_output_parameter_initialized(self) -> bool: + return False + + @property + def is_output_parameter_unaltered(self) -> bool: + return False + @property def is_pointer_cast(self) -> bool: return False @@ -962,6 +979,48 @@ def __str__(self) -> str: return "initialized(" + str(self.lval) + ")" +@pdregistry.register_tag("li", CPOPredicate) +class CPOLocallyInitialized(CPOPredicate): + """locally initialized(lval): location initialized within the function. + + - args[0]: index of lval in cdictionary + """ + + def __init__( + self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue + ) -> None: + CPOPredicate.__init__(self, pd, ixval) + + @property + def varinfo(self) -> "CVarInfo": + return self.cdeclarations.get_varinfo(self.args[0]) + + @property + def lval(self) -> "CLval": + return self.cd.get_lval(self.args[1]) + + @property + def is_locally_initialized(self) -> bool: + return True + + def has_variable(self, vid: int) -> bool: + return self.lval.has_variable(vid) + + def has_variable_deref(self, vid: int) -> bool: + return self.lval.has_variable_deref(vid) + + def has_ref_type(self) -> bool: + return self.lval.has_ref_type() + + def __str__(self) -> str: + return ( + "locally-initialized(" + + str(self.varinfo.vname) + + ", " + + str(self.lval) + + ")") + + @pdregistry.register_tag("ir", CPOPredicate) class CPOInitializedRange(CPOPredicate): """initialized-range(exp, size): the memory range starting at the address @@ -2162,3 +2221,73 @@ def has_variable(self, vid: int) -> bool: def __str__(self) -> str: return "preserves-value(" + str(self.exp) + ")" + + +@pdregistry.register_tag("opi", CPOPredicate) +class CPOOutputParameterInitialized(CPOPredicate): + """ + + - args[0]: index of varinfo in cdecls + """ + def __init__( + self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue + ) -> None: + CPOPredicate.__init__(self, pd, ixval) + + @property + def varinfo(self) -> "CVarInfo": + return self.cdeclarations.get_varinfo(self.args[0]) + + @property + def offset(self) -> "COffset": + return self.cd.get_offset(self.args[1]) + + @property + def is_output_parameter_initialized(self) -> bool: + return True + + def has_variable(self, vid: int) -> bool: + return self.varinfo.vid == vid + + def __str__(self) -> str: + return ( + "output_parameter-initialized(" + + str(self.varinfo.vname) + + ", " + + str(self.offset) + + ")") + + +@pdregistry.register_tag("opu", CPOPredicate) +class CPOOutputParameterUnaltered(CPOPredicate): + """ + + - args[0]: index of varinfo in cdecls + """ + def __init__( + self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue + ) -> None: + CPOPredicate.__init__(self, pd, ixval) + + @property + def varinfo(self) -> "CVarInfo": + return self.cdeclarations.get_varinfo(self.args[0]) + + @property + def offset(self) -> "COffset": + return self.cd.get_offset(self.args[1]) + + @property + def is_output_parameter_unaltered(self) -> bool: + return True + + def has_variable(self, vid: int) -> bool: + return self.varinfo.vid == vid + + def __str__(self) -> str: + return ( + "output_parameter-unaltered(" + + str(self.varinfo.vname) + + ", " + + str(self.offset) + + ")") From 32fa1c8bd77b48e33b5d2eebb9fac1b1275f13d7 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 8 Nov 2025 19:06:02 -0800 Subject: [PATCH 03/22] APP: add analysis info to function --- chc/app/CFunction.py | 102 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 102 insertions(+) diff --git a/chc/app/CFunction.py b/chc/app/CFunction.py index e7799cf..dde60a3 100644 --- a/chc/app/CFunction.py +++ b/chc/app/CFunction.py @@ -60,12 +60,93 @@ from chc.api.CFunctionContract import CFunctionContract from chc.api.InterfaceDictionary import InterfaceDictionary from chc.app.CApplication import CApplication + from chc.app.CDictionary import CDictionary from chc.app.CFile import CFile from chc.app.CFileDeclarations import CFileDeclarations + from chc.app.COffset import COffset from chc.app.CTyp import CTyp from chc.app.CVarInfo import CVarInfo +class CandidateOutputParameter: + + def __init__( + self, + cfun: "CFunction", + cvar: "CVarInfo", + offsets: List["COffset"]) -> None: + self._cfun = cfun + self._cvar = cvar + self._offsets = offsets + + @property + def cfun(self) -> "CFunction": + return self._cfun + + @property + def parameter(self) -> "CVarInfo": + return self._cvar + + @property + def offsets(self) -> List["COffset"]: + return self._offsets + + def __str__(self) -> str: + return ( + self.parameter.vname + "[" + ", ".join(str(o) for o in self.offsets) + "]") + + +class CAnalysisInfo: + + def __init__(self, xnode: Optional[ET.Element], cfun: "CFunction") -> None: + self._xnode = xnode + self._cfun = cfun + + @property + def cfun(self) -> "CFunction": + return self._cfun + + @property + def cdictionary(self) -> "CDictionary": + return self.cfun.cdictionary + + @property + def cfiledecls(self) -> "CFileDeclarations": + return self.cfun.cfiledecls + + @property + def analysis(self) -> str: + if self._xnode is None: + return "undefined-behavior" + else: + return self._xnode.get("name", "unknown") + + @property + def candidate_parameters(self) -> List[CandidateOutputParameter]: + result: List[CandidateOutputParameter] = [] + if self._xnode is not None: + if self.analysis == "output-parameters": + xparams = self._xnode.find("candidate-parameters") + if xparams is not None: + xparamlist = xparams.findall("vinfo") + for xparam in xparamlist: + xid = int(xparam.get("xid", "-1")) + if xid > 0: + vinfo = self.cfiledecls.get_varinfo(xid) + xoffsets = xparam.get("offsets", "") + if xoffsets is not None: + offsets = list( + self.cdictionary.get_offset(int(i)) + for i in xoffsets.split(",")) + + result.append(CandidateOutputParameter( + self.cfun, vinfo, offsets)) + return result + + def __str__(self) -> str: + return ", ".join(str(vinfo) for vinfo in self.candidate_parameters) + + class CFunction: """Function implementation.""" @@ -84,6 +165,7 @@ def __init__(self, cfile: "CFile", xnode: ET.Element, fname: str) -> None: self._vard: Optional[CFunVarDictionary] = None self._invd: Optional[CFunInvDictionary] = None self._invarianttable: Optional[CFunInvariantTable] = None + self._analysisinfo: Optional[CAnalysisInfo] = None def xmsg(self, txt: str) -> str: return "Function " + self.name + ": " + txt @@ -140,6 +222,10 @@ def ftype(self) -> "CTyp": def cfiledecls(self) -> "CFileDeclarations": return self.cfile.declarations + @property + def cdictionary(self) -> "CDictionary": + return self.cfile.dictionary + @property def interfacedictionary(self) -> "InterfaceDictionary": return self.cfile.interfacedictionary @@ -315,6 +401,22 @@ def proofs(self) -> CFunctionProofs: self._proofs = CFunctionProofs(self, xxpponode, xxsponode) return self._proofs + @property + def analysis_info(self) -> CAnalysisInfo: + if self._analysisinfo is None: + xpponode = UF.get_ppo_xnode( + self.targetpath, + self.projectname, + self.cfilepath, + self.cfilename, + self.name) + if xpponode is not None: + self._analysisinfo = ( + CAnalysisInfo(xpponode.find("analysis-info"), self)) + else: + self._analysisinfo = CAnalysisInfo(None, self) + return self._analysisinfo + def reinitialize_tables(self) -> None: self._api = None self._podictionary = None From c6f5e62b18a0e237ecc830355e94cfffa77782bc Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 8 Nov 2025 19:07:35 -0800 Subject: [PATCH 04/22] CMD: add cmdline options to choose analysis --- chc/cmdline/AnalysisManager.py | 49 +++++++++++++++++------- chc/cmdline/c_file/cfileutil.py | 52 +++++++++++++++++++++---- chc/cmdline/c_project/cprojectutil.py | 30 +++++++++++++-- chc/cmdline/chkc | 55 +++++++++++++++++++++++++++ chc/reporting/ProofObligations.py | 10 +++++ 5 files changed, 171 insertions(+), 25 deletions(-) diff --git a/chc/cmdline/AnalysisManager.py b/chc/cmdline/AnalysisManager.py index 99c8d4e..1873b96 100644 --- a/chc/cmdline/AnalysisManager.py +++ b/chc/cmdline/AnalysisManager.py @@ -49,13 +49,14 @@ class AnalysisManager: """Provide the interface to the codehawk (ocaml) analyzer.""" def __init__( - self, - capp: "CApplication", - wordsize: int = 0, - unreachability: bool = False, - thirdpartysummaries: List[str] = [], - keep_system_includes: bool = False, - verbose: bool = False, + self, + capp: "CApplication", + wordsize: int = 0, + unreachability: bool = False, + thirdpartysummaries: List[str] = [], + keep_system_includes: bool = False, + verbose: bool = False, + collectdiagnostics: bool = False ) -> None: """Initialize the analyzer location and target file location. @@ -78,6 +79,7 @@ def __init__( self.thirdpartysummaries = thirdpartysummaries self.unreachability = unreachability self.verbose = verbose + self._collectdiagnostics = collectdiagnostics @property def capp(self) -> "CApplication": @@ -87,6 +89,10 @@ def capp(self) -> "CApplication": def keep_system_includes(self) -> bool: return self._keep_system_includes + @property + def collect_diagnostics(self) -> bool: + return self._collectdiagnostics + @property def contractpath(self) -> Optional[str]: return self.capp.contractpath @@ -178,9 +184,11 @@ def _execute_cmd(self, CMD: List[str]) -> None: print(args) exit(1) - def _create_file_primary_proofobligations_cmd_partial(self) -> List[str]: + def _create_file_primary_proofobligations_cmd_partial( + self, po_cmd="undefined-behavior-primary" + ) -> List[str]: cmd: List[str] = [ - self.canalyzer, "-summaries", self.chsummaries, "-command", "primary"] + self.canalyzer, "-summaries", self.chsummaries, "-command", po_cmd] if not (self.thirdpartysummaries is None): for s in self.thirdpartysummaries: cmd.extend(["-summaries", s]) @@ -192,19 +200,26 @@ def _create_file_primary_proofobligations_cmd_partial(self) -> List[str]: cmd.append("-keep_system_includes") if self.wordsize > 0: cmd.extend(["-wordsize", str(self.wordsize)]) + if self.collect_diagnostics: + cmd.append("-diagnostics") cmd.append(self.targetpath) cmd.append("-cfilename") return cmd def create_file_primary_proofobligations( - self, cfilename: str, cfilepath: Optional[str] = None) -> None: + self, + cfilename: str, + cfilepath: Optional[str] = None, + po_cmd: str = "undefined-behavior-primary" + ) -> None: """Call analyzer to create primary proof obligations for a single file.""" chklogger.logger.info( "Create primiary proof obligations for file %s with path %s", cfilename, ("none" if cfilepath is None else cfilepath)) try: - cmd = self._create_file_primary_proofobligations_cmd_partial() + cmd = self._create_file_primary_proofobligations_cmd_partial( + po_cmd=po_cmd) cmd.append(cfilename) if cfilepath is not None: cmd.extend(["-cfilepath", cfilepath]) @@ -237,13 +252,17 @@ def create_file_primary_proofobligations( print(args) exit(1) - def create_app_primary_proofobligations(self, processes: int = 1) -> None: + def create_app_primary_proofobligations( + self, + po_cmd: str = "undefined-behavior-primary", + processes: int = 1) -> None: """Call analyzer to create ppo's for all application files.""" if processes > 1: def f(cfile: "CFile") -> None: - cmd = self._create_file_primary_proofobligations_cmd_partial() + cmd = self._create_file_primary_proofobligations_cmd_partial( + po_cmd=po_cmd) cmd.append(cfile.cfilename) if cfile.cfilepath is not None: cmd.extend(["-cfilepath", cfile.cfilepath]) @@ -290,6 +309,8 @@ def _generate_and_check_file_cmd_partial( cmd.append("-unreachability") if self.verbose: cmd.append("-verbose") + if self.collect_diagnostics: + cmd.append("-diagnostics") cmd.append(self.targetpath) if cfilepath is not None: cmd.extend(["-cfilepath", cfilepath]) @@ -317,7 +338,7 @@ def generate_and_check_file( result = subprocess.call( cmd, cwd=self.targetpath, - stdout=open(os.devnull, "w"), + # stdout=open(os.devnull, "w"), stderr=subprocess.STDOUT, ) if result != 0: diff --git a/chc/cmdline/c_file/cfileutil.py b/chc/cmdline/c_file/cfileutil.py index 38d5ba8..d715bd5 100644 --- a/chc/cmdline/c_file/cfileutil.py +++ b/chc/cmdline/c_file/cfileutil.py @@ -66,6 +66,8 @@ from chc.app.CApplication import CApplication from chc.app.CPrettyPrinter import CPrettyPrinter +from chc.proof.OutputParameterChecker import OutputParameterChecker + import chc.reporting.ProofObligations as RP from chc.util.Config import Config @@ -421,7 +423,10 @@ def cfile_analyze_file(args: argparse.Namespace) -> NoReturn: opttgtpath: Optional[str] = args.tgtpath wordsize: int = args.wordsize keep_system_includes: bool = args.keep_system_includes + analysis: str = args.analysis verbose: bool = args.verbose + analysisdomains: str = args.analysis_domains + collectdiagnostics: bool = args.collect_diagnostics loglevel: str = args.loglevel logfilename: Optional[str] = args.logfilename logfilemode: str = args.logfilemode @@ -433,6 +438,8 @@ def cfile_analyze_file(args: argparse.Namespace) -> NoReturn: cfilename = cfilename_ext[:-2] projectname = cfilename + po_cmd = analysis + "-primary" + set_logging( loglevel, targetpath, @@ -484,20 +491,21 @@ def cfile_analyze_file(args: argparse.Namespace) -> NoReturn: am = AnalysisManager( capp, verbose=verbose, + collectdiagnostics=collectdiagnostics, wordsize=wordsize, keep_system_includes=keep_system_includes) - am.create_file_primary_proofobligations(cfilename) + am.create_file_primary_proofobligations(cfilename, po_cmd=po_cmd) am.reset_tables(cfile) capp.collect_post_assumes() - am.generate_and_check_file(cfilename, None, "llrvisp") + am.generate_and_check_file(cfilename, None, analysisdomains) am.reset_tables(cfile) capp.collect_post_assumes() for k in range(5): capp.update_spos() - am.generate_and_check_file(cfilename, None, "llrvisp") + am.generate_and_check_file(cfilename, None, analysisdomains) am.reset_tables(cfile) chklogger.logger.info("cfile analyze completed") @@ -518,6 +526,7 @@ def cfile_report_file(args: argparse.Namespace) -> NoReturn: # arguments xcfilename: str = args.filename opttgtpath: Optional[str] = args.tgtpath + canalysis: str = args.analysis cshowcode: bool = args.showcode cshowinvariants: bool = args.showinvariants cfunctions: Optional[List[str]] = args.functions @@ -573,6 +582,16 @@ def pofilter(po: "CFunctionPO") -> bool: cfile, pofilter=pofilter, showinvs=cshowinvariants)) print(RP.file_proofobligation_stats_tostring(cfile)) + + if canalysis == "outputparameters": + for cfun in cfile.functions.values(): + try: + op_checker = OutputParameterChecker(cfun) + print(str(op_checker)) + except UF.CHCError as e: + print("Skipping function " + cfun.name) + continue + exit(0) for fnname in cfunctions: @@ -591,6 +610,9 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn: pcfilename: str = os.path.abspath(args.filename) opttgtpath: Optional[str] = args.tgtpath keep_system_includes: bool = args.keep_system_includes + analysis: str = args.analysis + analysisdomains: str = args.analysis_domains + collectdiagnostics: bool = args.collect_diagnostics cshowcode: bool = args.showcode copen: bool = args.open cshowinvariants: bool = args.showinvariants @@ -622,6 +644,8 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn: cfilename = cfilename_c[:-2] projectname = cfilename + po_cmd = analysis + "-primary" + if not os.path.isdir(targetpath): print_error("Target directory: " + targetpath + " does not exist") exit(1) @@ -696,19 +720,23 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn: capp.initialize_single_file(cfilename) cfile = capp.get_cfile() - am = AnalysisManager(capp, verbose=verbose) + am = AnalysisManager( + capp, + verbose=verbose, + collectdiagnostics=collectdiagnostics, + keep_system_includes=keep_system_includes) - am.create_file_primary_proofobligations(cfilename) + am.create_file_primary_proofobligations(cfilename, po_cmd=po_cmd) am.reset_tables(cfile) capp.collect_post_assumes() - am.generate_and_check_file(cfilename, None, "llrvisp") + am.generate_and_check_file(cfilename, None, analysisdomains) am.reset_tables(cfile) capp.collect_post_assumes() for k in range(5): capp.update_spos() - am.generate_and_check_file(cfilename, None, "llrvisp") + am.generate_and_check_file(cfilename, None, analysisdomains) am.reset_tables(cfile) chklogger.logger.info("cfile analyze completed") @@ -745,6 +773,16 @@ def pofilter(po: "CFunctionPO") -> bool: cfile, pofilter=pofilter, showinvs=cshowinvariants)) print(RP.file_proofobligation_stats_tostring(cfile)) + + if analysis == "outputparameters": + for cfun in cfile.functions.values(): + try: + op_checker = OutputParameterChecker(cfun) + print(str(op_checker)) + except UF.CHCError as e: + print("Skipping function " + cfun.name + ": " + str(e)) + continue + exit(0) diff --git a/chc/cmdline/c_project/cprojectutil.py b/chc/cmdline/c_project/cprojectutil.py index 553f254..8dc26dc 100644 --- a/chc/cmdline/c_project/cprojectutil.py +++ b/chc/cmdline/c_project/cprojectutil.py @@ -49,6 +49,8 @@ from chc.linker.CLinker import CLinker +from chc.proof.OutputParameterChecker import OutputParameterChecker + import chc.reporting.ProofObligations as RP from chc.util.Config import Config @@ -426,6 +428,9 @@ def cproject_analyze_project(args: argparse.Namespace) -> NoReturn: tgtpath: str = args.tgtpath projectname: str = args.projectname keep_system_includes: bool = args.keep_system_includes + analysis: str = args.analysis + analysisdomains: str = args.analysis_domains + collectdiagnostics: bool = args.collect_diagnostics maxprocesses: int = args.maxprocesses loglevel: str = args.loglevel logfilename: Optional[str] = args.logfilename @@ -435,6 +440,8 @@ def cproject_analyze_project(args: argparse.Namespace) -> NoReturn: if excludefiles is None: excludefiles = [] + po_cmd = analysis + "-primary" + if not os.path.isdir(tgtpath): print_error(f"Target directory {tgtpath} not found") exit(1) @@ -482,12 +489,17 @@ def save_xrefs(f: "CFile") -> None: keep_system_includes=keep_system_includes, excludefiles=excludefiles) - am = AnalysisManager(capp, verbose=True, keep_system_includes=keep_system_includes) + am = AnalysisManager( + capp, + verbose=True, + collectdiagnostics=collectdiagnostics, + keep_system_includes=keep_system_includes) with timing("analysis"): try: - am.create_app_primary_proofobligations(processes=maxprocesses) + am.create_app_primary_proofobligations( + po_cmd=po_cmd, processes=maxprocesses) capp.reinitialize_tables() capp.collect_post_assumes() except UF.CHError as e: @@ -495,13 +507,13 @@ def save_xrefs(f: "CFile") -> None: exit(1) for i in range(1): - am.generate_and_check_app("visp", processes=maxprocesses) + am.generate_and_check_app(analysisdomains, processes=maxprocesses) capp.reinitialize_tables() capp.update_spos() for i in range(5): capp.update_spos() - am.generate_and_check_app("visp", processes=maxprocesses) + am.generate_and_check_app(analysisdomains, processes=maxprocesses) capp.reinitialize_tables() timestamp = os.stat(UF.get_cchpath(targetpath, projectname)).st_ctime @@ -563,6 +575,7 @@ def cproject_report_file(args: argparse.Namespace) -> NoReturn: tgtpath: str = args.tgtpath projectname: str = args.projectname filename: str = args.filename + canalysis: str = args.analysis showcode: bool = args.showcode showopen: bool = args.open showinvariants: bool = args.showinvariants @@ -600,6 +613,15 @@ def pofilter(po: "CFunctionPO") -> bool: print(RP.file_proofobligation_stats_tostring(cfile)) + if canalysis == "outputparameters": + for cfun in cfile.functions.values(): + try: + op_checker = OutputParameterChecker(cfun) + print(str(op_checker)) + except UF.CHCError as e: + print("Skipping function " + cfun.name) + continue + exit(0) diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc index 7b57951..cdf0c52 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -728,6 +728,21 @@ def parse() -> argparse.Namespace: "--keep-system-includes", action="store_true", help="do not filter out functions from files with absolute file names") + cfileanalyze.add_argument( + "--analysis", + default="undefined-behavior", + choices=["undefined-behavior", "outputparameters"], + help="choose analysis for creating primary proof obligations") + cfileanalyze.add_argument( + "--collect-diagnostics", + action="store_true", + help="save diagnostics in a separate diagnostics log file") + cfileanalyze.add_argument( + "--analysis-domains", + default="llrvisp", + help=("choose analysis domains to be used (l: linear equalities" + ", r: pepr, v: value sets, i: intervals, s: symbolic sets" + ", p: pointer sets)")) cfileanalyze.add_argument( "--verbose", "-v", action="store_true", @@ -763,6 +778,11 @@ def parse() -> argparse.Namespace: "--functions", nargs="*", help="restrict output to function names listed (defualt: all)") + cfilereport.add_argument( + "--analysis", + default="undefined-behavior", + choices=["undefined-behavior", "outputparameters"], + help="choose analysis for reporting results") cfilereport.add_argument( "--open", action="store_true", @@ -806,6 +826,21 @@ def parse() -> argparse.Namespace: "--keep-system-includes", action="store_true", help="don't filter out functions from files with absolute filenames") + cfilerun.add_argument( + "--analysis", + default="undefined-behavior", + choices=["undefined-behavior", "outputparameters"], + help="choose analysis for creating primary proof obligations") + cfilerun.add_argument( + "--collect-diagnostics", + action="store_true", + help="save diagnostics in a separate diagnostics log file") + cfilerun.add_argument( + "--analysis-domains", + default="llrvisp", + help=("choose analysis domains to be used (l: linear equalities" + ", r: pepr, v: value sets, i: intervals, s: symbolic sets" + ", p: pointer sets)")) cfilerun.add_argument( "--showcode", action="store_true", @@ -1474,6 +1509,21 @@ def parse() -> argparse.Namespace: "--keep-system-includes", action="store_true", help="don't filter out functions from files with absolute filenames") + cprojectanalyze.add_argument( + "--analysis", + default="undefined-behavior", + choices=["undefined-behavior", "outputparameters"], + help="choose analysis for creating primary proof obligations") + cprojectanalyze.add_argument( + "--collect-diagnostics", + action="store_true", + help="save diagnostics in a separate diagnostics log file") + cprojectanalyze.add_argument( + "--analysis-domains", + default="llrvisp", + help=("choose analysis domains to be used (l: linear equalities" + ", r: pepr, v: value sets, i: intervals, s: symbolic sets" + ", p: pointer sets)")) cprojectanalyze.add_argument( "--maxprocesses", help="number of files to process in parallel", @@ -1516,6 +1566,11 @@ def parse() -> argparse.Namespace: "projectname", help="name of the project") cprojectreportfile.add_argument( "filename", help="filename with relative path wrt the project") + cprojectreportfile.add_argument( + "--analysis", + default="undefined-behavior", + choices=["undefined-behavior", "outputparameters"], + help="choose analysis for reporting results") cprojectreportfile.add_argument( "--showcode", action="store_true", diff --git a/chc/reporting/ProofObligations.py b/chc/reporting/ProofObligations.py index 26e1233..79cfed2 100644 --- a/chc/reporting/ProofObligations.py +++ b/chc/reporting/ProofObligations.py @@ -300,6 +300,11 @@ def pos_no_code_to_string( prefix = po.get_display_prefix() lines.append(prefix + " " + str(po)) lines.append((" " * indent) + str(expl)) + deps = po.dependencies.invs + lines.append( + ("\n" + " " * indent).join( + str(self.cfunction.invdictionary.get_invariant_fact(i) + for i in deps))) else: lines.append("\n " + str(po)) if po.has_diagnostic(): @@ -382,6 +387,11 @@ def pos_on_code_tostring( prefix = po.get_display_prefix() lines.append(prefix + " " + str(po)) lines.append((" " * indent) + str(expl)) + deps = po.dependencies.invs + lines.append( + ("\n" + " " * indent).join(str( + self.cfunction.invdictionary.get_invariant_fact(i)) + for i in deps)) else: contexts.add(po.context) lines.append("\n " + str(po)) From 4d8a418db2007ca93c45579f5895b396e2ac45d5 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 12 Nov 2025 23:32:12 -0800 Subject: [PATCH 05/22] PROOF: add checker for output parameters --- chc/cmdline/juliet/JulietTestScoring.py | 4 +- chc/proof/CFunctionCallsiteSPO.py | 4 +- chc/proof/CFunctionCallsiteSPOs.py | 8 +- chc/proof/CFunctionLocalSPO.py | 4 +- chc/proof/CFunctionPO.py | 8 +- chc/proof/CFunctionPPO.py | 4 +- chc/proof/CFunctionPPOs.py | 7 +- chc/proof/CFunctionReturnsiteSPO.py | 4 +- chc/proof/CFunctionReturnsiteSPOs.py | 8 +- chc/proof/CFunctionSPOs.py | 8 +- chc/proof/CProofDiagnostic.py | 99 ++++++++++-- chc/proof/OutputParameterChecker.py | 191 ++++++++++++++++++++++++ chc/reporting/ProofObligations.py | 22 +-- 13 files changed, 322 insertions(+), 49 deletions(-) create mode 100644 chc/proof/OutputParameterChecker.py diff --git a/chc/cmdline/juliet/JulietTestScoring.py b/chc/cmdline/juliet/JulietTestScoring.py index 14712e0..6a17c89 100644 --- a/chc/cmdline/juliet/JulietTestScoring.py +++ b/chc/cmdline/juliet/JulietTestScoring.py @@ -185,7 +185,7 @@ def f(spo: "CFunctionPO") -> None: if sev is None: sevtxt = "?" else: - sevtxt = spo.get_display_prefix() + " " + sev + sevtxt = spo.get_display_prefix() + " " + str(sev) lines.append( " C:" + str(spo.line).rjust(3) @@ -213,7 +213,7 @@ def testppo_results_tostring( if ev is None: evstr = "?" else: - evstr = ppo.get_display_prefix() + " " + ev + evstr = ppo.get_display_prefix() + " " + str(ev) lines.append( " " + str(ppo.line).rjust(3) diff --git a/chc/proof/CFunctionCallsiteSPO.py b/chc/proof/CFunctionCallsiteSPO.py index 0216e74..d3fa442 100644 --- a/chc/proof/CFunctionCallsiteSPO.py +++ b/chc/proof/CFunctionCallsiteSPO.py @@ -39,7 +39,7 @@ from chc.proof.CFunPODictionaryRecord import CFunPOType from chc.proof.CFunctionProofs import CFunctionProofs from chc.proof.CProofDependencies import CProofDependencies - from chc.proof.CProofDiagnostic import CProofDiagnostic + from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg from chc.proof.SPOType import CallsiteSPOType @@ -52,7 +52,7 @@ def __init__( potype: "CFunPOType", status: str = "open", deps: Optional["CProofDependencies"] = None, - expl: Optional[str] = None, + expl: Optional["SituatedMsg"] = None, diag: Optional["CProofDiagnostic"] = None) -> None: CFunctionPO.__init__(self, cproofs, potype, status, deps, expl, diag) diff --git a/chc/proof/CFunctionCallsiteSPOs.py b/chc/proof/CFunctionCallsiteSPOs.py index 99697bf..bf90da5 100644 --- a/chc/proof/CFunctionCallsiteSPOs.py +++ b/chc/proof/CFunctionCallsiteSPOs.py @@ -43,7 +43,7 @@ from chc.proof.CFunctionCallsiteSPO import CFunctionCallsiteSPO from chc.proof.CFunctionPO import po_status from chc.proof.CProofDependencies import CProofDependencies -from chc.proof.CProofDiagnostic import CProofDiagnostic +from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg import chc.util.fileutil as UF from chc.util.loggingutil import chklogger @@ -233,8 +233,10 @@ def spos(self) -> Dict[int, List[CFunctionCallsiteSPO]]: deps = CProofDependencies(self.cproofs, xpo) status = po_status[xpo.get("s", "o")] xexpl = xpo.find("e") - expl = None if xexpl is None else xexpl.get("txt") - diagnostic = CProofDiagnostic(xpo.find("d")) + expl = ( + None if xexpl is None + else SituatedMsg(self.cfun.cdictionary, xexpl)) + diagnostic = CProofDiagnostic(self.cproofs, xpo.find("d")) self._spos[int(xapid)].append( CFunctionCallsiteSPO( self.cproofs, diff --git a/chc/proof/CFunctionLocalSPO.py b/chc/proof/CFunctionLocalSPO.py index 91f1fe5..6b6930e 100644 --- a/chc/proof/CFunctionLocalSPO.py +++ b/chc/proof/CFunctionLocalSPO.py @@ -38,7 +38,7 @@ from chc.proof.CFunctionProofs import CFunctionProofs from chc.proof.CFunPODictionaryRecord import CFunPOType from chc.proof.CProofDependencies import CProofDependencies - from chc.proof.CProofDiagnostic import CProofDiagnostic + from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg class CFunctionLocalSPO(CFunctionPO): @@ -49,7 +49,7 @@ def __init__( potype: "CFunPOType", status: str = "open", deps: Optional["CProofDependencies"] = None, - expl: Optional[str] = None, + expl: Optional["SituatedMsg"] = None, diag: Optional["CProofDiagnostic"] = None) -> None: CFunctionPO.__init__(self, cproofs, potype, status, deps, expl, diag) diff --git a/chc/proof/CFunctionPO.py b/chc/proof/CFunctionPO.py index 05f5af2..e0f5be3 100644 --- a/chc/proof/CFunctionPO.py +++ b/chc/proof/CFunctionPO.py @@ -47,7 +47,7 @@ from chc.proof.CFunPODictionary import CFunPODictionary from chc.proof.CPOPredicate import CPOPredicate from chc.proof.CProofDependencies import CProofDependencies - from chc.proof.CProofDiagnostic import CProofDiagnostic + from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg from chc.proof.SPOType import SPOType @@ -72,7 +72,7 @@ def __init__( potype: CFunPOType, status: str = "open", deps: Optional["CProofDependencies"] = None, - expl: Optional[str] = None, + expl: Optional["SituatedMsg"] = None, diag: Optional["CProofDiagnostic"] = None) -> None: self._cproofs = cproofs self._potype = potype @@ -182,7 +182,7 @@ def has_dependencies(self) -> bool: return self._dependencies is not None @property - def explanation(self) -> Optional[str]: + def explanation(self) -> Optional["SituatedMsg"]: return self._explanation def has_explanation(self) -> bool: @@ -364,7 +364,7 @@ def write_xml(self, cnode: ET.Element) -> None: self.dependencies.write_xml(cnode) if self.explanation is not None: enode = ET.Element("e") - enode.set("txt", self.explanation) + enode.set("txt", self.explanation.msg) cnode.append(enode) if self.has_diagnostic(): dnode = ET.Element("d") diff --git a/chc/proof/CFunctionPPO.py b/chc/proof/CFunctionPPO.py index 9f87298..f2f4735 100644 --- a/chc/proof/CFunctionPPO.py +++ b/chc/proof/CFunctionPPO.py @@ -38,7 +38,7 @@ from chc.proof.CFunctionProofs import CFunctionProofs from chc.proof.CFunPODictionaryRecord import CFunPOType from chc.proof.CProofDependencies import CProofDependencies - from chc.proof.CProofDiagnostic import CProofDiagnostic + from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg class CFunctionPPO(CFunctionPO): @@ -50,7 +50,7 @@ def __init__( ppotype: "CFunPOType", status: str = "open", deps: Optional["CProofDependencies"] = None, - expl: Optional[str] = None, + expl: Optional["SituatedMsg"] = None, diag: Optional["CProofDiagnostic"] = None) -> None: CFunctionPO.__init__(self, cproofs, ppotype, status, deps, expl, diag) diff --git a/chc/proof/CFunctionPPOs.py b/chc/proof/CFunctionPPOs.py index 0145b12..d7e3e8c 100644 --- a/chc/proof/CFunctionPPOs.py +++ b/chc/proof/CFunctionPPOs.py @@ -34,7 +34,7 @@ from chc.proof.CFunctionPPO import CFunctionPPO from chc.proof.CProofDependencies import CProofDependencies -from chc.proof.CProofDiagnostic import CProofDiagnostic +from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg import chc.util.fileutil as UF @@ -90,12 +90,13 @@ def ppos(self) -> Dict[int, CFunctionPPO]: id = ppotype.index status = po_status[xp.get("s", "o")] deps = CProofDependencies(self.cproofs, xp) - diagnostic = CProofDiagnostic(xp.find("d")) + diagnostic = CProofDiagnostic(self.cproofs, xp.find("d")) # get explanation enode = xp.find("e") if enode is not None: - expl: Optional[str] = enode.get("txt", "") + expl: Optional[SituatedMsg] = SituatedMsg( + self.cfun.cdictionary, enode) else: expl = None diff --git a/chc/proof/CFunctionReturnsiteSPO.py b/chc/proof/CFunctionReturnsiteSPO.py index a77fd30..e17579b 100644 --- a/chc/proof/CFunctionReturnsiteSPO.py +++ b/chc/proof/CFunctionReturnsiteSPO.py @@ -38,7 +38,7 @@ from chc.proof.CFunctionReturnsiteSPOs import CFunctionReturnsiteSPOs from chc.proof.CFunPODictionaryRecord import CFunPOType from chc.proof.CProofDependencies import CProofDependencies - from chc.proof.CProofDiagnostic import CProofDiagnostic + from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg from chc.proof.SPOType import SPOType @@ -51,7 +51,7 @@ def __init__( potype: "CFunPOType", status: str = "open", deps: Optional["CProofDependencies"] = None, - expl: Optional[str] = None, + expl: Optional["SituatedMsg"] = None, diag: Optional["CProofDiagnostic"] = None) -> None: CFunctionPO.__init__( self, crspos.cproofs, potype, status, deps, expl, diag) diff --git a/chc/proof/CFunctionReturnsiteSPOs.py b/chc/proof/CFunctionReturnsiteSPOs.py index d407948..2268909 100644 --- a/chc/proof/CFunctionReturnsiteSPOs.py +++ b/chc/proof/CFunctionReturnsiteSPOs.py @@ -39,7 +39,7 @@ from chc.proof.CFunctionReturnsiteSPO import CFunctionReturnsiteSPO from chc.proof.CProofDependencies import CProofDependencies -from chc.proof.CProofDiagnostic import CProofDiagnostic +from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg import chc.util.fileutil as UF @@ -107,8 +107,10 @@ def spos(self) -> Dict[int, List[CFunctionReturnsiteSPO]]: deps = CProofDependencies(self.cproofs, xpo) status = po_status[xpo.get("s", "o")] xexpl = xpo.find("e") - expl = None if xexpl is None else xexpl.get("txt") - diagnostic = CProofDiagnostic(xpo.find("d")) + expl = ( + None if xexpl is None + else SituatedMsg(self.cfun.cdictionary, xexpl)) + diagnostic = CProofDiagnostic(self.cproofs, xpo.find("d")) self._spos[ipc].append( CFunctionReturnsiteSPO( self, spotype, status, deps, expl, diagnostic)) diff --git a/chc/proof/CFunctionSPOs.py b/chc/proof/CFunctionSPOs.py index fbebd26..5527013 100644 --- a/chc/proof/CFunctionSPOs.py +++ b/chc/proof/CFunctionSPOs.py @@ -40,7 +40,7 @@ from chc.proof.CFunctionPO import CFunctionPO from chc.proof.CFunctionPO import po_status from chc.proof.CProofDependencies import CProofDependencies -from chc.proof.CProofDiagnostic import CProofDiagnostic +from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg from chc.util.loggingutil import chklogger @@ -103,9 +103,11 @@ def local_spos(self) -> Dict[int, CFunctionLocalSPO]: for xpo in xlspos.findall("po"): spotype = self.podictionary.read_xml_spo_type(xpo) xexpl = xpo.find("e") - expl = None if xexpl is None else xexpl.get("txt") + expl = ( + None if xexpl is None + else SituatedMsg(self.cfun.cdictionary, xexpl)) deps = CProofDependencies(self.cproofs, xpo) - diagnostic = CProofDiagnostic(xpo.find("d")) + diagnostic = CProofDiagnostic(self.cproofs, xpo.find("d")) status = po_status[xpo.get("s", "o")] self._localspos[spotype.po_index] = CFunctionLocalSPO( self.cproofs, spotype, status, deps, expl, diagnostic) diff --git a/chc/proof/CProofDiagnostic.py b/chc/proof/CProofDiagnostic.py index a5a504b..5f6a50f 100644 --- a/chc/proof/CProofDiagnostic.py +++ b/chc/proof/CProofDiagnostic.py @@ -32,15 +32,88 @@ from typing import Dict, List, Optional, TYPE_CHECKING +if TYPE_CHECKING: + from chc.app.CDictionary import CDictionary + from chc.app.CFunction import CFunction + from chc.proof.CFunctionProofs import CFunctionProofs + + +class SituatedMsg: + + def __init__(self, cd: "CDictionary", xnode: ET.Element) -> None: + self._cd = cd + self._xnode = xnode + + @property + def cd(self) -> "CDictionary": + return self._cd + + @property + def msg(self) -> str: + result = self._xnode.get("t") + if result is None: + return self._xnode.get("txt", "?") + else: + return result + + @property + def file(self) -> Optional[str]: + xfile = self._xnode.get("file") + if xfile is not None: + return self.cd.get_string(int(xfile)) + return None + + @property + def line(self) -> Optional[int]: + xline = self._xnode.get("line") + if xline is not None: + return int(xline) + return None + + @property + def detail(self) -> Optional[str]: + xdetail = self._xnode.get("detail") + if xdetail is not None: + return self.cd.get_string(int(xdetail)) + return None + + @property + def is_situated(self) -> bool: + return ( + self.file is not None + and self.line is not None + and self.detail is not None) + + def __str__(self) -> str: + if self.is_situated: + return self.msg + " (" + str(self.line) + ": " + str(self.detail) + ")" + else: + return self.msg + class CProofDiagnostic: - def __init__(self, xnode: Optional[ET.Element]) -> None: + def __init__( + self, cproofs: "CFunctionProofs", xnode: Optional[ET.Element] + ) -> None: + self._cproofs = cproofs self._xnode = xnode self._invsmap: Optional[Dict[int, List[int]]] = None - self._amsgs: Optional[Dict[int, List[str]]] = None + self._amsgs: Optional[Dict[int, List[SituatedMsg]]] = None self._kmsgs: Optional[Dict[str, List[str]]] = None - self._msgs: Optional[List[str]] = None + self._msgs: Optional[List[SituatedMsg]] = None + + @property + def cproofs(self) -> "CFunctionProofs": + return self._cproofs + + @property + def cfun(self) -> "CFunction": + return self.cproofs.cfun + + @property + def cd(self) -> "CDictionary": + return self.cfun.cdictionary @property def invsmap(self) -> Dict[int, List[int]]: @@ -63,7 +136,7 @@ def invsmap(self) -> Dict[int, List[int]]: return self._invsmap @property - def msgs(self) -> List[str]: + def msgs(self) -> List[SituatedMsg]: """Returns general diagnostics pertaining to the proof obligation.""" if self._msgs is None: @@ -71,11 +144,12 @@ def msgs(self) -> List[str]: if self._xnode is not None: mnode = self._xnode.find("msgs") if mnode is not None: - self._msgs = [x.get("t", "") for x in mnode.findall("msg")] + self._msgs = [ + SituatedMsg(self.cd, x) for x in mnode.findall("msg")] return self._msgs @property - def argument_msgs(self) -> Dict[int, List[str]]: + def argument_msgs(self) -> Dict[int, List[SituatedMsg]]: """Returns argument-specific diagnostic messages. Note: argument index starts at 1. @@ -89,7 +163,8 @@ def argument_msgs(self) -> Dict[int, List[str]]: for n in anode.findall("arg"): xargindex = n.get("a") if xargindex is not None: - msgs = [x.get("t", "") for x in n.findall("msg")] + msgs = [ + SituatedMsg(self.cd, x) for x in n.findall("msg")] self._amsgs[int(xargindex)] = msgs return self._amsgs @@ -132,9 +207,9 @@ def write_xml(self, dnode: ET.Element) -> None: for arg in self.argument_msgs: anode = ET.Element("arg") anode.set("a", str(arg)) - for t in self.argument_msgs[arg]: + for msg in self.argument_msgs[arg]: tnode = ET.Element("msg") - tnode.set("t", t) + tnode.set("t", msg.msg) anode.append(tnode) aanode.append(anode) for key in self.keyword_msgs: @@ -145,13 +220,13 @@ def write_xml(self, dnode: ET.Element) -> None: tnode.set("t", t) knode.append(tnode) kknode.append(knode) - for t in self.msgs: + for msg in self.msgs: mnode = ET.Element("msg") - mnode.set("t", t) + mnode.set("t", msg.msg) mmnode.append(mnode) dnode.extend([inode, mmnode, aanode, kknode]) def __str__(self) -> str: if len(self.msgs) == 0: return "no diagnostic messages" - return "\n".join(self.msgs) + return "\n".join(str(m) for m in self.msgs) diff --git a/chc/proof/OutputParameterChecker.py b/chc/proof/OutputParameterChecker.py new file mode 100644 index 0000000..bb57613 --- /dev/null +++ b/chc/proof/OutputParameterChecker.py @@ -0,0 +1,191 @@ +# ------------------------------------------------------------------------------ +# CodeHawk C Analyzer +# Author: Henny Sipma +# ------------------------------------------------------------------------------ +# The MIT License (MIT) +# +# Copyright (c) 2025 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 + + +if TYPE_CHECKING: + from chc.app.CContextDictionary import CContextDictionary + from chc.app.CFile import CFile + from chc.app.CFunction import CFunction, CAnalysisInfo, CandidateOutputParameter + from chc.app.CVarInfo import CVarInfo + from chc.proof.CFunctionPO import CFunctionPO + + +class OutputParameterChecker: + """Interpret the proof obligation results for output parameters.""" + + def __init__(self, cfun: "CFunction") -> None: + self._cfun = cfun + + @property + def cfun(self) -> "CFunction": + return self._cfun + + @property + def analysis_info(self) -> "CAnalysisInfo": + return self.cfun.analysis_info + + @property + def cfile(self) -> "CFile": + return self.cfun.cfile + + @property + def contextdictionary(self) -> "CContextDictionary": + return self.cfile.contextdictionary + + def has_output_parameters(self) -> bool: + return self.cfun.analysis_info.analysis == "output-parameters" + + @property + def candidate_parameters(self) -> List["CandidateOutputParameter"]: + if self.has_output_parameters(): + return self.analysis_info.candidate_parameters + else: + return [] + + def context_candidate_output_ppos( + self, candidate: "CVarInfo", ctxtid: int) -> List["CFunctionPO"]: + """Return po's for a given parameter at a particular location in the ast.""" + + return [po for po in self.candidate_ppos(candidate) + if po.context.index == ctxtid + and (po.predicate.is_output_parameter_initialized + or po.predicate.is_output_parameter_unaltered)] + + def candidate_ppos(self, candidate: "CVarInfo") -> List["CFunctionPO"]: + """Return all po's for a given parameter.""" + + return self.cfun.proofs.get_output_parameter_ppos(candidate.vname) + + def is_pure_output_parameter(self, candidate: "CVarInfo") -> Optional[str]: + """Evaluate the status of the proof obligations related to the parameter. + + An output parameter is pure (that is, it can be safely converted to + a Rust return value) if: + + 1) its dereference is not read within the function + 2) it is fully written at some return site + 3) it is either fully written or not written at all at all return sites + + The first condition is represented by proof obligations with predicate + PLocallyInitialized, which should all be safe. + + The second and third condition are represented by proof obligations with + POutputParameterInitialized and POutputParameterUnaltered. + + Note: + There are more conditions to come that have not yet been implemented. + """ + + ppos = self.candidate_ppos(candidate) + ctxts = {ctxt.index for ctxt in [po.context for po in ppos]} + + notread = all( + po.is_safe for po in ppos if po.predicate.is_locally_initialized) + + def allwritten(po_s: List["CFunctionPO"]) -> bool: + return all(po.is_safe for po in po_s + if po.predicate.is_output_parameter_initialized) + + def allunaltered(po_s: List["CFunctionPO"]) -> bool: + return all(po.is_safe for po in po_s + if po.predicate.is_output_parameter_unaltered) + + writtenonce = False + must_parameter = True + all_or_nothing_written = True + for ctxtid in ctxts: + ctxtppos = self.context_candidate_output_ppos(candidate, ctxtid) + if len(ctxtppos) > 0: + ctxt_allwritten = allwritten(ctxtppos) + ctxt_allunaltered = allunaltered(ctxtppos) + if not (ctxt_allwritten or ctxt_allunaltered): + all_or_nothing_written = False + elif ctxt_allunaltered: + must_parameter = False + elif ctxt_allwritten: + writtenonce = True + + issafe = notread and all_or_nothing_written and writtenonce + + if issafe: + if must_parameter: + return "must-output-parameter" + else: + return "may-output-parameter" + + else: + return None + + def diagnostic(self, candidate: "CVarInfo") -> str: + if self.is_pure_output_parameter(candidate): + return "valid" + + lines: List[str] = [] + + ppos = self.candidate_ppos(candidate) + readppos = [po for po in ppos if po.predicate.is_locally_initialized] + readviolations = [po for po in readppos if po.is_violated] + readunknowns = [po for po in readppos if po.is_open] + if len(readviolations) + len(readunknowns) > 0: + lines.append("\nread violations and/or unknowns") + for po in (readviolations + readunknowns): + lines.append(str(po)) + + writeppos = [po for po in ppos + if po.predicate.is_output_parameter_initialized + or po.predicate.is_output_parameter_unaltered] + ctxts = {ctxt.index for ctxt in [po.context for po in ppos]} + + lines.append("\nfully written/unaltered violations and/or unknowns") + for index in ctxts: + output_po_s = self.context_candidate_output_ppos(candidate, index) + output_violations = [po for po in output_po_s if po.is_violated] + output_unknowns = [po for po in output_po_s if po.is_open] + if len(output_po_s) + len(output_unknowns) > 0: + ctxt = self.contextdictionary.get_program_context(index) + lines.append(str(ctxt)) + for po in (output_violations + output_unknowns): + lines.append(str(po)) + + return "\n".join(lines) + + def __str__(self) -> str: + lines: List[str] = [] + lines.append("\n\nOutput parameters for function " + self.cfun.name) + + for candidate in self.candidate_parameters: + if self.is_pure_output_parameter(candidate.parameter) is not None: + lines.append("\n- " + str(candidate.parameter.vname) + ": " + + str(self.is_pure_output_parameter( + candidate.parameter))) + else: + lines.append("- " + str(candidate.parameter.vname) + ": diagnostics:") + lines.append(self.diagnostic(candidate.parameter)) + + return "\n".join(lines) diff --git a/chc/reporting/ProofObligations.py b/chc/reporting/ProofObligations.py index 79cfed2..05e86ec 100644 --- a/chc/reporting/ProofObligations.py +++ b/chc/reporting/ProofObligations.py @@ -311,8 +311,8 @@ def pos_no_code_to_string( amsgs = po.diagnostic.argument_msgs if len(amsgs) > 0: for arg in sorted(amsgs): - for s in sorted(amsgs[arg]): - lines.append((" " * indent) + s) + for amsg in amsgs[arg]: + lines.append((" " * indent) + str(amsg)) kmsgs = po.diagnostic.keyword_msgs if len(kmsgs) > 0: for key in sorted(kmsgs): @@ -321,7 +321,7 @@ def pos_no_code_to_string( msgs = po.diagnostic.msgs if len(msgs) > 0: for m in msgs: - lines.append((" " * indent) + m) + lines.append((" " * indent) + str(m)) keys = po.diagnostic.argument_indices for k in sorted(keys): invids = po.diagnostic.get_invariant_ids(k) @@ -399,8 +399,8 @@ def pos_on_code_tostring( amsgs = po.diagnostic.argument_msgs if len(amsgs) > 0: for arg in sorted(amsgs): - for s in sorted(amsgs[arg]): - lines.append((" " * indent) + s) + for amsg in amsgs[arg]: + lines.append((" " * indent) + str(amsg)) kmsgs = po.diagnostic.keyword_msgs if len(kmsgs) > 0: for key in sorted(kmsgs): @@ -409,7 +409,7 @@ def pos_on_code_tostring( msgs = po.diagnostic.msgs if len(msgs) > 0: for m in msgs: - lines.append((" " * indent) + m) + lines.append((" " * indent) + str(m)) keys = po.diagnostic.argument_indices for k in sorted(keys): invids = po.diagnostic.get_invariant_ids(k) @@ -811,13 +811,13 @@ def tag_file_function_pos_tostring( amsgs = po.diagnostic.argument_msgs if len(amsgs) > 0: for arg in sorted(amsgs): - for s in sorted(amsgs[arg]): - lines.append((" " * 14) + s) + for amsg in amsgs[arg]: + lines.append((" " * 14) + str(amsg)) msgs = po.diagnostic.msgs if len(msgs) > 0: - lines.append((" " * 8) + " ---> " + msgs[0]) - for s in msgs[1:]: - lines.append((" " * 14) + s) + lines.append((" " * 8) + " ---> " + str(msgs[0])) + for msg in msgs[1:]: + lines.append((" " * 14) + str(msg)) lines.append(" ") keys = po.diagnostic.argument_indices for k in keys: From aee66d366a0df63a67da27806647ebe466a28f59 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Fri, 14 Nov 2025 17:35:31 -0800 Subject: [PATCH 06/22] PROOF: add unique-pointer predicate --- chc/proof/CPOPredicate.py | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/chc/proof/CPOPredicate.py b/chc/proof/CPOPredicate.py index 47b49f6..43dd244 100644 --- a/chc/proof/CPOPredicate.py +++ b/chc/proof/CPOPredicate.py @@ -94,6 +94,7 @@ 'ub': 'upper-bound', 'uio': 'uint-overflow', 'uiu': 'uint-underflow', + 'up': 'unique-pointer', 'va': 'var-args', 'vc': 'value-constraint', 'vm': 'valid-mem', @@ -297,6 +298,10 @@ def is_stack_address_escape(self) -> bool: def is_type_at_offset(self) -> bool: return False + @property + def is_unique_pointer(self) -> bool: + return False + @property def is_upper_bound(self) -> bool: return False @@ -2182,6 +2187,29 @@ def __str__(self) -> str: return "value-constraint(" + str(self.exp) + ")" +@pdregistry.register_tag("up", CPOPredicate) +class CPOUniquePointer(CPOPredicate): + + def __init__( + self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue + ) -> None: + CPOPredicate.__init__(self, pd, ixval) + + @property + def exp(self) -> "CExp": + return self.cd.get_exp(self.args[0]) + + @property + def is_unique_pointer(self) -> bool: + return True + + def has_variable(self, vid: int) -> bool: + return self.exp.has_variable(vid) + + def __str__(self) -> str: + return "unique-pointer(" + str(self.exp) + ")" + + @pdregistry.register_tag("prm", CPOPredicate) class CPOPreservedAllMemory(CPOPredicate): """preserves-all-memory(): true of a function that does not free any memory. From 366a572f6a7544a72bbdccd8626685029635c62e Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 18 Nov 2025 13:28:25 -0800 Subject: [PATCH 07/22] extend cil-source pretty printer --- chc/app/CAttributes.py | 54 +++++ chc/app/CCompInfo.py | 6 +- chc/app/CExp.py | 52 ++++- chc/app/CFieldInfo.py | 6 +- chc/app/CFile.py | 32 +++ chc/app/CFileGlobals.py | 10 + chc/app/CHVersion.py | 2 +- chc/app/CInitInfo.py | 24 +- chc/app/CInstr.py | 47 ++-- chc/app/CLHost.py | 13 +- chc/app/CLocation.py | 6 +- chc/app/CLval.py | 9 +- chc/app/COffset.py | 16 +- chc/app/CPrettyPrinter.py | 397 +++++++++++++++++++++++++++++++- chc/app/CStmt.py | 74 +++++- chc/app/CTypeInfo.py | 6 +- chc/app/CVisitor.py | 270 +++++++++++++++++++++- chc/cmdline/c_file/cfileutil.py | 69 ++++++ chc/cmdline/chkc | 28 +++ 19 files changed, 1084 insertions(+), 37 deletions(-) diff --git a/chc/app/CAttributes.py b/chc/app/CAttributes.py index 891b406..3a93aa7 100644 --- a/chc/app/CAttributes.py +++ b/chc/app/CAttributes.py @@ -113,6 +113,9 @@ def is_index(self) -> bool: def is_question(self) -> bool: return False + def accept(self, visitor: "CVisitor") -> None: + raise UF.CHCError("visitor not yet implemented for " + str(self)) + def __str__(self) -> str: return "attrparam:" + self.tags[0] @@ -135,6 +138,9 @@ def intvalue(self) -> int: def is_int(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_int(self) + def __str__(self) -> str: return "aint(" + str(self.intvalue) + ")" @@ -157,6 +163,9 @@ def stringvalue(self) -> str: def is_str(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_str(self) + def __str__(self) -> str: return "astr(" + str(self.stringvalue) + ")" @@ -184,6 +193,9 @@ def params(self) -> List[CAttr]: def is_cons(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_cons(self) + def __str__(self) -> str: return "acons(" + str(self.name) + ")" @@ -206,6 +218,9 @@ def typ(self) -> "CTyp": def is_sizeof(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_sizeof(self) + def __str__(self) -> str: return "asizeof(" + str(self.typ) + ")" @@ -228,6 +243,9 @@ def param(self) -> CAttr: def is_sizeofe(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_sizeofe(self) + def __str__(self) -> str: return "asizeofe(" + str(self.param) + ")" @@ -250,6 +268,9 @@ def typsig(self) -> "CTypsig": def is_sizeofs(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_sizeofs(self) + def __str__(self) -> str: return "asizeofs(" + str(self.typsig) + ")" @@ -272,6 +293,9 @@ def typ(self) -> "CTyp": def is_alignof(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_alignof(self) + def __str__(self) -> str: return "aalignof(" + str(self.typ) + ")" @@ -294,6 +318,9 @@ def param(self) -> CAttr: def is_alignofe(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_alignofe(self) + def __str__(self) -> str: return "aalignofe(" + str(self.param) + ")" @@ -316,6 +343,9 @@ def typsig(self) -> "CTypsig": def is_alignofs(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_alignofs(self) + def __str__(self) -> str: return "aalignofs(" + str(self.typsig) + ")" @@ -343,6 +373,9 @@ def param(self) -> CAttr: def is_unop(self) -> bool: return True + def acecpt(self, visitor: "CVisitor") -> None: + visitor.visit_attr_unop(self) + def __str__(self) -> str: return "aunop(" + self.op + "," + str(self.param) + ")" @@ -375,6 +408,9 @@ def param2(self) -> CAttr: def is_binop(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_binop(self) + def __str__(self) -> str: return ( "abinop(" @@ -410,6 +446,9 @@ def param(self) -> CAttr: def is_dot(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_dot(self) + def __str__(self) -> str: return "adot(" + str(self.param) + "." + self.suffix + ")" @@ -436,6 +475,9 @@ def param(self) -> CAttr: def is_star(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_star(self) + def __str__(self) -> str: if self.index == self.args[0]: return "astar()" @@ -461,6 +503,9 @@ def param(self) -> CAttr: def is_addrof(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_addrof(self) + def __str__(self) -> str: return "aaddrof(" + str(self.param) + ")" @@ -488,6 +533,9 @@ def param2(self) -> CAttr: def is_index(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_index(self) + def __str__(self) -> str: return "aindex(" + str(self.param1) + "," + str(self.param2) + ")" @@ -516,6 +564,9 @@ def param2(self) -> CAttr: def param3(self) -> CAttr: return self.cd.get_attrparam(int(self.args[2])) + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attr_question(self) + def __str__(self) -> str: return ( "aquestion(" @@ -541,6 +592,9 @@ def name(self) -> str: def params(self) -> List[CAttr]: return [self.cd.get_attrparam(int(i)) for i in self.args] + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_attribute(self) + def __str__(self) -> str: return self.name + ": " + ",".join([str(p) for p in self.params]) diff --git a/chc/app/CCompInfo.py b/chc/app/CCompInfo.py index 5c5d2f1..f296182 100644 --- a/chc/app/CCompInfo.py +++ b/chc/app/CCompInfo.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -39,6 +39,7 @@ from chc.app.CDeclarations import CDeclarations from chc.app.CFieldInfo import CFieldInfo from chc.app.CGlobalDeclarations import CGlobalDeclarations + from chc.app.CVisitor import CVisitor class CCompInfo(CDeclarationsRecord): @@ -100,6 +101,9 @@ def name(self) -> str: def field_strings(self) -> str: return ":".join([f.fname for f in self.fields]) + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_compinfo(self) + def __str__(self) -> str: lines = [] lines.append("struct " + self.name) diff --git a/chc/app/CExp.py b/chc/app/CExp.py index 3c0a3ee..1afce84 100644 --- a/chc/app/CExp.py +++ b/chc/app/CExp.py @@ -32,6 +32,7 @@ from chc.app.CDictionaryRecord import CDictionaryRecord, cdregistry +import chc.util.fileutil as UF import chc.util.IndexedTable as IT if TYPE_CHECKING: @@ -148,15 +149,15 @@ def get_strings(self) -> List[str]: def get_variable_uses(self, vid: int) -> int: return 0 - def accept(self, visitor: "CVisitor") -> None: - raise Exception("CExp.accept: " + str(self)) - def to_dict(self) -> Dict[str, Any]: return {"base": "exp"} def to_idict(self) -> Dict[str, Any]: return {"t": self.tags, "a": self.args} + def accept(self, visitor: "CVisitor") -> None: + raise UF.CHCError("visitor not yet implemented for: " + str(self)) + def __str__(self) -> str: return "baseexp:" + self.tags[0] @@ -223,6 +224,9 @@ def get_variable_uses(self, vid: int) -> int: def to_dict(self) -> Dict[str, Any]: return {"base": "lval", "lval": self.lval.to_dict()} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_explval(self) + def __str__(self) -> str: return str(self.lval) @@ -248,6 +252,9 @@ def is_sizeof(self) -> bool: def to_dict(self) -> Dict[str, Any]: return {"base": "sizeof", "type": self.typ.to_dict()} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_sizeof(self) + def __str__(self) -> str: return "sizeof(" + str(self.typ) + ")" @@ -279,6 +286,9 @@ def get_variable_uses(self, vid: int) -> int: def to_dict(self) -> Dict[str, Any]: return {"base": "sizeofe", "exp": self.exp.to_dict()} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_sizeofe(self) + def __str__(self) -> str: return "sizeofe(" + str(self.exp) + ")" @@ -307,6 +317,9 @@ def is_sizeofstr(self) -> bool: def to_dict(self) -> Dict[str, Any]: return {"base": "sizeofstr", "string": self.stringvalue} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_size_of_str(self) + def __str__(self) -> str: return "sizeofstr(" + str(self.stringvalue) + ")" @@ -332,6 +345,9 @@ def is_alignof(self) -> bool: def to_dict(self) -> Dict[str, Any]: return {"base": "alignof", "type": self.typ.to_dict()} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_alignof(self) + def __str__(self) -> str: return "alignof(" + str(self.typ) + ")" @@ -366,6 +382,9 @@ def get_variable_uses(self, vid: int) -> int: def to_dict(self) -> Dict[str, Any]: return {"base": "alignofe", "exp": self.exp.to_dict()} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_alignofe(self) + def __str__(self) -> str: return "alignofe(" + str(self.exp) + ")" @@ -411,6 +430,9 @@ def get_variable_uses(self, vid: int) -> int: def to_dict(self) -> Dict[str, Any]: return {"base": "unop", "op": self.op, "exp": self.exp.to_dict()} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_unop(self) + def __str__(self) -> str: return "(" + unoperatorstrings[self.op] + " " + str(self.exp) + ")" @@ -474,6 +496,9 @@ def to_dict(self) -> Dict[str, Any]: "exp2": self.exp2.to_dict(), } + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_binop(self) + def __str__(self) -> str: return ( "(" @@ -549,6 +574,9 @@ def to_dict(self) -> Dict[str, object]: "type": self.typ.to_dict(), } + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_question(self) + def __str__(self) -> str: return ( "(" @@ -600,6 +628,9 @@ def to_dict(self) -> Dict[str, object]: "type": self.typ.to_dict(), } + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_cast(self) + def __str__(self) -> str: return "caste(" + str(self.typ) + "," + str(self.exp) + ")" @@ -634,6 +665,9 @@ def get_variable_uses(self, vid: int) -> int: def to_dict(self) -> Dict[str, object]: return {"base": "addrof", "lval": self.lval.to_dict()} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_addrof(self) + def __str__(self) -> str: return "&(" + str(self.lval) + ")" @@ -655,6 +689,9 @@ def label_sid(self) -> int: def to_dict(self) -> Dict[str, object]: return {"base": "addroflabel", "label": self.label_sid} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_addr_of_label(self) + def __str__(self) -> str: return "addroflabel(" + str(self.label_sid) + ")" @@ -689,6 +726,9 @@ def get_variable_uses(self, vid: int) -> int: def to_dict(self) -> Dict[str, Any]: return {"base": "startof", "lval": self.lval.to_dict()} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_startof(self) + def __str__(self) -> str: return "&(" + str(self.lval) + ")" @@ -722,6 +762,9 @@ def arguments(self) -> List[Optional[CExp]]: def has_variable(self, vid: int) -> bool: return any([a.has_variable(vid) for a in self.arguments if a]) + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_fn_app(self) + def __str__(self) -> str: return ( "fnapp(" @@ -762,6 +805,9 @@ def arguments(self) -> List[Optional[CExp]]: def has_variable(self, vid: int) -> bool: return any([a.has_variable(vid) for a in self.arguments if a]) + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_cn_app(self) + def __str__(self) -> str: return ( "cnapp(" diff --git a/chc/app/CFieldInfo.py b/chc/app/CFieldInfo.py index 9446c57..43c0665 100644 --- a/chc/app/CFieldInfo.py +++ b/chc/app/CFieldInfo.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -40,6 +40,7 @@ from chc.app.CFileDeclarations import CFileDeclarations from chc.app.CLocation import CLocation from chc.app.CTyp import CTyp + from chc.app.CVisitor import CVisitor class CFieldInfo(CDeclarationsRecord): @@ -87,5 +88,8 @@ def attributes(self) -> Optional["CAttributes"]: return self.dictionary.get_attributes(self.args[3]) return None + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_fieldinfo(self) + def __str__(self) -> str: return self.fname + ":" + str(self.ftype) diff --git a/chc/app/CFile.py b/chc/app/CFile.py index d70d40d..d44f063 100644 --- a/chc/app/CFile.py +++ b/chc/app/CFile.py @@ -216,8 +216,40 @@ def header_declarations( fndecl = pp.function_declaration_str( fn.varinfo, srcloc=srcfilename, binloc=binloc) lines.append(fndecl) + return "\n".join(lines) + def cil_source(self) -> str: + lines: List[str] = [] + srcfilename = self.name + ".cil.c" + lines.append("// " + srcfilename + "\n") + gtypes = self.gtypes.values() + gcompdefs = self.gcomptagdefs.values() + gcompdecls = self.gcomptagdecls.values() + genumdefs = self.genumtagdefs.values() + genumdecls = self.genumtagdecls.values() + gvardefs = self.gvardefs.values() + gvardecls = self.gvardecls.values() + if len(gtypes) > 0: + lines.append("// type definitions") + for gtype in gtypes: + pp = CPrettyPrinter() + lines.append(pp.cgtypedef_str(gtype)) + if len(gcompdefs) > 0: + lines.append("// struct definitions") + for gcompdef in gcompdefs: + pp = CPrettyPrinter() + lines.append(pp.cgcomptag_str(gcompdef)) + if len(gvardefs) > 0: + lines.append("// static and global variable definitions\n") + for gvar in gvardefs: + pp = CPrettyPrinter() + lines.append(pp.cgvardef_str(gvar)) + for fn in self.functions.values(): + pp = CPrettyPrinter() + lines.append(pp.function_definition_to_string(fn)) + return "\n\n".join(lines) + @property def functioncount(self) -> int: return self.cfileglobals.functioncount diff --git a/chc/app/CFileGlobals.py b/chc/app/CFileGlobals.py index 8ae7527..5480370 100644 --- a/chc/app/CFileGlobals.py +++ b/chc/app/CFileGlobals.py @@ -50,6 +50,7 @@ from chc.app.CTyp import CTyp from chc.app.CTypeInfo import CTypeInfo from chc.app.CVarInfo import CVarInfo + from chc.app.CVisitor import CVisitor @dataclass @@ -71,6 +72,9 @@ def ckey(self) -> int: def is_struct(self) -> bool: return self.compinfo.is_struct + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_cgcomptag(self) + def __str__(self) -> str: if self.is_struct: return f"struct {self.name} (ckey: {self.ckey})" @@ -121,6 +125,9 @@ class CGType: location: "CLocation" typeinfo: "CTypeInfo" + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_cgtype(self) + @dataclass class CGVarDecl: @@ -149,6 +156,9 @@ def vname(self) -> str: def has_initializer(self) -> bool: return self.initializer is not None + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_cgvardef(self) + def __str__(self) -> str: if self.initializer is not None: return f"{self.varinfo} = {self.initializer}" diff --git a/chc/app/CHVersion.py b/chc/app/CHVersion.py index ced4e23..840f1b3 100644 --- a/chc/app/CHVersion.py +++ b/chc/app/CHVersion.py @@ -1 +1 @@ -chcversion: str = "0.2.0-2025-10-24" +chcversion: str = "0.2.0-2025-11-18" diff --git a/chc/app/CInitInfo.py b/chc/app/CInitInfo.py index b7463c3..c97141b 100644 --- a/chc/app/CInitInfo.py +++ b/chc/app/CInitInfo.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -32,6 +32,7 @@ from chc.app.CDictionaryRecord import CDeclarationsRecord +import chc.util.fileutil as UF import chc.util.IndexedTable as IT if TYPE_CHECKING: @@ -39,6 +40,7 @@ from chc.app.CTyp import CTyp from chc.app.CDeclarations import CDeclarations from chc.app.COffset import COffset + from chc.app.CVisitor import CVisitor class CInitInfo(CDeclarationsRecord): @@ -55,6 +57,9 @@ def is_single(self) -> bool: def is_compound(self) -> bool: return False + def accept(self, visitor: "CVisitor") -> None: + raise UF.CHCError("visitor not yet implemented for " + str(self)) + class CSingleInitInfo(CInitInfo): """Initializer of a simple variable. @@ -73,6 +78,9 @@ def exp(self) -> "CExp": def is_single(self) -> bool: return True + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_single_initinfo(self) + def __str__(self) -> str: return str(self.exp) @@ -95,8 +103,15 @@ def offset_initializers(self) -> List["COffsetInitInfo"]: return [self.decls.get_offset_init(x) for x in self.args[1:]] @property - def is_compound(self) -> bool: - return True + def is_struct(self) -> bool: + return self.typ.is_struct + + @property + def is_union(self) -> bool: + return self.typ.is_union + + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_compound_initinfo(self) def __str__(self) -> str: return "\n".join([str(x) for x in self.offset_initializers]) @@ -120,5 +135,8 @@ def offset(self) -> "COffset": def initializer(self) -> CInitInfo: return self.decls.get_initinfo(self.args[1]) + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_offset_initinfo(self) + def __str__(self) -> str: return str(self.offset) + ":=" + str(self.initializer) diff --git a/chc/app/CInstr.py b/chc/app/CInstr.py index 0808659..375b0c0 100644 --- a/chc/app/CInstr.py +++ b/chc/app/CInstr.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -41,6 +41,7 @@ from chc.app.CFunction import CFunction from chc.app.CLval import CLval from chc.app.CStmt import CStmt + from chc.app.CVisitor import CVisitor class CInstr: @@ -81,13 +82,15 @@ def strings(self) -> List[str]: def get_variable_uses(self, vid: int) -> int: return 0 + def accept(self, visitor: "CVisitor") -> None: + raise UF.CHCError("visitor not yet accepted on: " + str(self)) + class CCallInstr(CInstr): """Call instruction.""" def __init__(self, parent: "CStmt", xnode: ET.Element) -> None: CInstr.__init__(self, parent, xnode) - self._lhs: Optional["CLval"] = None self._callee: Optional["CExp"] = None self._callargs: Optional[List["CExp"]] = None @@ -96,14 +99,12 @@ def is_call(self) -> bool: return True @property - def lhs(self) -> "CLval": - if self._lhs is None: - xlval = self.xnode.get("ilval") - if xlval is not None: - self._lhs = self.cdictionary.get_lval(int(xlval)) - else: - raise UF.CHCError("call instruction does not have an lval") - return self._lhs + def lhs(self) -> Optional["CLval"]: + xlval = self.xnode.get("ilval") + if xlval is not None: + return self.cdictionary.get_lval(int(xlval)) + else: + return None @property def callee(self) -> "CExp": @@ -141,10 +142,16 @@ def has_lhs(self) -> bool: return "ilval" in self.xnode.attrib def get_variable_uses(self, vid: int) -> int: - lhsuse = self.lhs.get_variable_uses(vid) if self.has_lhs() else 0 - arguse = sum([a.get_variable_uses(vid) for a in self.callargs]) - calleeuse = self.callee.get_variable_uses(vid) - return lhsuse + arguse + calleeuse + if self.lhs is not None: + lhsuse = self.lhs.get_variable_uses(vid) if self.has_lhs() else 0 + arguse = sum([a.get_variable_uses(vid) for a in self.callargs]) + calleeuse = self.callee.get_variable_uses(vid) + return lhsuse + arguse + calleeuse + else: + return 0 + + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_call_instr(self) def __str__(self) -> str: return " call " + str(self.callee) @@ -193,6 +200,9 @@ def get_variable_uses(self, vid: int) -> int: rhsuse = self.rhs.get_variable_uses(vid) return lhsuse + rhsuse + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_assign_instr(self) + def __str__(self) -> str: return " assign: " + str(self.lhs) + " := " + str(self.rhs) @@ -243,6 +253,9 @@ def templates(self) -> List[str]: self._templates.append(ts) return self._templates + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_asm_instr(self) + def __str__(self) -> str: lines: List[str] = [] for s in self.templates: @@ -279,6 +292,9 @@ def lhs(self) -> "CLval": def constraint(self) -> str: return self.xnode.get("constraint", "none") + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_asm_output(self) + def __str__(self) -> str: return self.constraint + "; lval: " + str(self.lhs) @@ -308,5 +324,8 @@ def exp(self) -> "CExp": def constraint(self) -> str: return self.xnode.get("constraint", "none") + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_asm_input(self) + def __str__(self) -> str: return self.constraint + "; exp: " + str(self.exp) diff --git a/chc/app/CLHost.py b/chc/app/CLHost.py index 5b85bfa..caadb7a 100644 --- a/chc/app/CLHost.py +++ b/chc/app/CLHost.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -32,11 +32,13 @@ from chc.app.CDictionaryRecord import CDictionaryRecord, cdregistry +import chc.util.fileutil as UF import chc.util.IndexedTable as IT if TYPE_CHECKING: from chc.app.CDictionary import CDictionary from chc.app.CExp import CExp + from chc.app.CVisitor import CVisitor class CLHost(CDictionaryRecord): @@ -75,6 +77,9 @@ def get_variable_uses(self, vid: int) -> int: def to_dict(self) -> Dict[str, object]: return {"base": "lhost"} + def accept(self, visitor: "CVisitor") -> None: + raise UF.CHCError("visitor not implemented for: " + str(self)) + def __str__(self) -> str: return "lhostbase:" + self.tags[0] @@ -115,6 +120,9 @@ def get_variable_uses(self, vid: int) -> int: def to_dict(self) -> Dict[str, object]: return {"base": "var", "var": self.name} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_lhostvar(self) + def __str__(self) -> str: return self.name @@ -152,5 +160,8 @@ def has_variable_deref(self, vid: int) -> bool: def to_dict(self) -> Dict[str, object]: return {"base": "mem", "exp": self.exp.to_dict()} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_lhostmem(self) + def __str__(self) -> str: return "(*" + str(self.exp) + ")" diff --git a/chc/app/CLocation.py b/chc/app/CLocation.py index dabb57d..9522f0a 100644 --- a/chc/app/CLocation.py +++ b/chc/app/CLocation.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -39,6 +39,7 @@ if TYPE_CHECKING: from chc.app.CDeclarations import CDeclarations from chc.app.CFileDeclarations import CFileDeclarations + from chc.app.CVisitor import CVisitor class CLocation(CDeclarationsRecord): @@ -68,6 +69,9 @@ def file(self) -> str: def get_loc(self) -> Tuple[str, int, int]: return (self.file, self.line, self.byte) + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_location(self) + def __ge__(self, loc: "CLocation") -> bool: return self.get_loc() >= loc.get_loc() diff --git a/chc/app/CLval.py b/chc/app/CLval.py index a45bae4..851644a 100644 --- a/chc/app/CLval.py +++ b/chc/app/CLval.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -38,6 +38,7 @@ from chc.app.CDictionary import CDictionary from chc.app.CLHost import CLHost from chc.app.COffset import COffset + from chc.app.CVisitor import CVisitor class CLval(CDictionaryRecord): @@ -77,6 +78,9 @@ def has_variable_deref(self, vid: int) -> bool: def has_ref_type(self) -> bool: return self.lhost.has_ref_type() + def is_var(self) -> bool: + return self.lhost.is_var + def to_dict(self) -> Dict[str, object]: return { "lhost": self.lhost.to_dict(), @@ -86,5 +90,8 @@ def to_dict(self) -> Dict[str, object]: def to_idict(self) -> Dict[str, object]: return {"t": self.tags, "a": self.args} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_lval(self) + def __str__(self) -> str: return str(self.lhost) + str(self.offset) diff --git a/chc/app/COffset.py b/chc/app/COffset.py index d9fe0b2..453031e 100644 --- a/chc/app/COffset.py +++ b/chc/app/COffset.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -32,11 +32,13 @@ from chc.app.CDictionaryRecord import CDictionaryRecord, cdregistry +import chc.util.fileutil as UF import chc.util.IndexedTable as IT if TYPE_CHECKING: from chc.app.CDictionary import CDictionary from chc.app.CExp import CExp + from chc.app.CVisitor import CVisitor class COffset(CDictionaryRecord): @@ -69,6 +71,9 @@ def get_variable_uses(self, vid: int) -> int: def to_dict(self) -> Dict[str, object]: return {"base": "offset"} + def accept(self, visitor: "CVisitor") -> None: + raise UF.CHCError("visitor not implemented for: " + str(self)) + def __str__(self) -> str: return "offsetbase:" + self.tags[0] @@ -89,6 +94,9 @@ def is_no_offset(self) -> bool: def to_dict(self) -> Dict[str, object]: return {"base": "no-offset"} + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_nooffset(self) + def __str__(self) -> str: return "" @@ -129,6 +137,9 @@ def to_dict(self) -> Dict[str, object]: result["offset"] = self.offset.to_dict() return result + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_fieldoffset(self) + def __str__(self) -> str: offset = str(self.offset) if self.has_offset() else "" return "." + self.fieldname + offset @@ -169,6 +180,9 @@ def to_dict(self) -> Dict[str, object]: result["offset"] = self.offset.to_dict() return result + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_indexoffset(self) + def __str__(self) -> str: offset = str(self.offset) if self.has_offset() else "" return "[" + str(self.index_exp) + "]" + offset diff --git a/chc/app/CPrettyPrinter.py b/chc/app/CPrettyPrinter.py index af1bfd6..54ce2af 100644 --- a/chc/app/CPrettyPrinter.py +++ b/chc/app/CPrettyPrinter.py @@ -29,11 +29,27 @@ import chc.app.CAttributes as CA import chc.app.CExp as CE +import chc.app.CInstr as CI +import chc.app.CLHost as CH +import chc.app.CLval as CL +import chc.app.COffset as CO +import chc.app.CStmt as CS import chc.app.CTyp as CT from chc.app.CVarInfo import CVarInfo from chc.app.CVisitor import CVisitor +if TYPE_CHECKING: + from chc.app.CFileGlobals import CGCompTag, CGType, CGVarDef + from chc.app.CCompInfo import CCompInfo + from chc.app.CFieldInfo import CFieldInfo + from chc.app.CFunction import CFunction + from chc.app.CInitInfo import CSingleInitInfo, CCompoundInitInfo + from chc.app.CLocation import CLocation + from chc.app.CInitInfo import ( + CSingleInitInfo, CCompoundInitInfo, COffsetInitInfo) + from chc.app.CTypeInfo import CTypeInfo + integernames = { "ichar": "char", @@ -50,6 +66,33 @@ "iulonglong": "unsigned long long", } + +operators = { + "band": " & ", + "bor": " | ", + "bxor": " ^ ", + "div": " / ", + "eq": " == ", + "ge": " >= ", + "gt": " > ", + "indexpi": " + ", + "land": " && ", + "le": " <= ", + "lor": " || ", + "lt": " < ", + "minusa": " - ", + "minuspi": " - ", + "minuspp": " - ", + "mod": " % ", + "mult": " * ", + "ne": " != ", + "plusa": " + ", + "pluspi": " + ", + "shiftlt": " << ", + "shiftrt": " >> " +} + + floatnames = {"float": "float", "fdouble": "double", "flongdouble": "long double"} @@ -86,6 +129,32 @@ def __init__(self, indentation: int = 2) -> None: self._indent = 0 self._ccode = CPrettyCode() + def cgtypedef_str(self, gty: "CGType") -> str: + gty.accept(self) + return str(self.ccode) + + def cgcomptag_str(self, gcomp: "CGCompTag") -> str: + gcomp.accept(self) + return str(self.ccode) + + def cgvardef_str(self, gvardef: "CGVarDef") -> str: + gvardef.accept(self) + return str(self.ccode) + + def function_definition_to_string(self, cfun: "CFunction") -> str: + self.write_function_signature(cfun.svar) + self.ccode.write(" {") + self.ccode.newline(indent=self.indent) + self.increase_indent() + if len(cfun.locals) > 0: + self.write_function_locals(list(cfun.locals.values())) + self.ccode.newline(indent=self.indent) + cfun.sbody.accept(self) + self.decrease_indent() + self.ccode.newline(indent=self.indent) + self.ccode.write("}") + return str(self.ccode) + @property def indentation(self) -> int: return self._indentation @@ -104,6 +173,78 @@ def increase_indent(self) -> None: def decrease_indent(self) -> None: self._indent -= self.indentation + def visit_location(self, loc: "CLocation") -> None: + self.ccode.newline(indent=0) + self.ccode.write(f"// {loc.file}:{loc.line}:{loc.byte}") + + def visit_cgtype(self, cgtype: "CGType") -> None: + cgtype.location.accept(self) + cgtype.typeinfo.accept(self) + + def visit_cgcomptag(self, cgcomptag: "CGCompTag") -> None: + cgcomptag.location.accept(self) + self.ccode.newline(indent=0) + if cgcomptag.is_struct: + self.ccode.write(f"struct {cgcomptag.name}") + else: + self.ccode.write(f"union {cgcomptag.name}") + self.ccode.write(" {") + self.increase_indent() + cgcomptag.compinfo.accept(self) + self.decrease_indent() + self.ccode.newline() + self.ccode.write("}") + + def visit_cgvardef(self, cgvardef: "CGVarDef") -> None: + cgvardef.location.accept(self) + self.ccode.newline(indent=0) + cgvardef.varinfo.vtype.accept(self) + self.ccode.write(" ") + self.ccode.write(cgvardef.vname) + if cgvardef.initializer is not None: + self.ccode.write(" = ") + cgvardef.initializer.accept(self) + + def visit_typeinfo(self, typeinfo: "CTypeInfo") -> None: + self.ccode.newline(indent=0) + self.ccode.write("typedef ") + typeinfo.type.accept(self) + self.ccode.write(" ") + self.ccode.write(typeinfo.name) + self.ccode.write(";") + + def visit_compinfo(self, compinfo: "CCompInfo") -> None: + for field in compinfo.fields: + field.accept(self) + + def visit_fieldinfo(self, fieldinfo: "CFieldInfo") -> None: + self.ccode.newline(indent=self.indent) + fieldinfo.ftype.accept(self) + self.ccode.write(f" {fieldinfo.fname};") + + def visit_single_initinfo(self, initinfo: "CSingleInitInfo") -> None: + initinfo.exp.accept(self) + + def visit_compound_initinfo(self, initinfo: "CCompoundInitInfo") -> None: + if initinfo.typ.is_struct or initinfo.typ.is_union: + self.ccode.write("{") + else: + self.ccode.write("]") + if len(initinfo.offset_initializers) > 0: + for oi in initinfo.offset_initializers[:-1]: + oi.accept(self) + self.ccode.write(", ") + initinfo.offset_initializers[-1].accept(self) + if initinfo.typ.is_struct or initinfo.is_union: + self.ccode.write("}") + else: + self.ccode.write("]") + + def visit_offset_initinfo(self, initinfo: "COffsetInitInfo") -> None: + initinfo.offset.accept(self) + self.ccode.write(" = ") + initinfo.initializer.accept(self) + def visit_voidtyp(self, t: CT.CTypVoid) -> None: t.attributes.accept(self) self.ccode.write("void") @@ -228,6 +369,15 @@ def function_declaration_str( if not vinfo.vtype.is_function: return "error" + self.write_function_signature(vinfo, srcloc=srcloc, binloc=binloc) + self.ccode.write(";") + return str(self.ccode) + + def write_function_signature( + self, + vinfo: CVarInfo, + srcloc: Optional[str] = None, + binloc: Optional[str] = None) -> None: self.ccode.newline() ftype = cast(CT.CTypFun, vinfo.vtype) if ftype.return_type.is_function_pointer: @@ -245,10 +395,6 @@ def function_declaration_str( self.ccode.write(")") if srcloc is not None: self.write_chkx_srcloc_attribute(srcloc, vinfo.line, binloc) - self.ccode.write(";") - self.ccode.newline() - return str(self.ccode) - else: ftype.return_type.accept(self) self.ccode.write(" ") @@ -261,9 +407,14 @@ def function_declaration_str( self.ccode.write(")") if srcloc is not None: self.write_chkx_srcloc_attribute(srcloc, vinfo.line, binloc) - self.ccode.write(";") - self.ccode.newline() - return str(self.ccode) + + def write_function_locals(self, vinfos: List["CVarInfo"]) -> None: + for vinfo in vinfos: + self.ccode.newline(indent=self.indent) + vinfo.vtype.accept(self) + self.ccode.write(" ") + self.ccode.write(vinfo.vname) + self.ccode.write(";") def funtypptr_with_name(self, t: CT.CTypFun, name: str) -> None: if t.return_type.is_function_pointer: @@ -353,6 +504,7 @@ def ptrarg_with_attribute_length( self.ccode.write(str(aparam.intvalue)) self.ccode.write("]") + ''' def visit_attributes(self, a: CA.CAttributes) -> None: if a.length == 0: return @@ -362,6 +514,237 @@ def visit_attributes(self, a: CA.CAttributes) -> None: self.ccode.write("volatile ") else: self.ccode.write("[[" + a.attributes[0].name + " not yet supported]]") + ''' def visit_constexp(self, e: CE.CExpConst) -> None: self.ccode.write(str(e)) + + def function_body_str(self, cbody: CS.CFunctionBody) -> str: + self.ccode.newline() + cbody.accept(self) + return str(self.ccode) + + def visit_block(self, cblock: CS.CBlock) -> None: + for stmt in cblock.stmts.values(): + stmt.accept(self) + + def visit_function_body(self, cbody: CS.CFunctionBody) -> None: + for stmt in cbody.stmts.values(): + stmt.accept(self) + + def visit_if_stmt(self, ifstmt: CS.CIfStmt) -> None: + self.ccode.newline(indent=self.indent) + self.ccode.write("if (") + ifstmt.condition.accept(self) + self.ccode.write(") {") + if ifstmt.ifstmt is not None: + self.increase_indent() + ifstmt.ifstmt.accept(self) + self.decrease_indent() + self.ccode.newline(indent=self.indent) + if ifstmt.elsestmt is not None: + self.ccode.write("} else {") + self.increase_indent() + ifstmt.elsestmt.accept(self) + self.decrease_indent() + self.ccode.newline(indent=self.indent) + self.ccode.write("}") + + def visit_loop_stmt(self, loopstmt: CS.CLoopStmt) -> None: + pass + + def visit_switch_stmt(self, switchstmt: CS.CSwitchStmt) -> None: + pass + + def visit_break_stmt(self, breakstmt: CS.CBreakStmt) -> None: + pass + + def visit_continue_stmt(self, continuestmt: CS.CContinueStmt) -> None: + pass + + def visit_goto_stmt(self, gotostmt: CS.CGotoStmt) -> None: + pass + + def visit_return_stmt(self, returnstmt: CS.CReturnStmt) -> None: + returnstmt.location.accept(self) + self.ccode.newline(indent=self.indent) + if returnstmt.exp is not None: + self.ccode.write("return ") + returnstmt.exp.accept(self) + self.ccode.write(";") + else: + self.ccode.write("return;") + + def visit_instrs_stmt(self, instrsstmt: CS.CInstrsStmt) -> None: + for instr in instrsstmt.instrs: + instr.accept(self) + + def visit_assign_instr(self, assigninstr: CI.CAssignInstr) -> None: + self.ccode.newline(indent=self.indent) + assigninstr.lhs.accept(self) + self.ccode.write(" = ") + assigninstr.rhs.accept(self) + self.ccode.write(";") + + def visit_call_instr(self, callinstr: CI.CCallInstr) -> None: + self.ccode.newline(indent=self.indent) + if callinstr.lhs is not None: + callinstr.lhs.accept(self) + self.ccode.write(" = ") + callinstr.callee.accept(self) + self.ccode.write("(") + if len(callinstr.callargs) > 0: + for a in callinstr.callargs[:-1]: + a.accept(self) + self.ccode.write(", ") + callinstr.callargs[-1].accept(self) + self.ccode.write(");") + + def visit_asm_instr(self, asminstr: CI.CAsmInstr) -> None: + pass + + def visit_asm_output(self, asmoutput: CI.CAsmOutput) -> None: + pass + + def visit_asm_input(self, asminput: CI.CAsmInput) -> None: + pass + + def visit_lval(self, lval: CL.CLval) -> None: + lval.lhost.accept(self) + lval.offset.accept(self) + + def visit_lhostvar(self, lhostvar: CH.CLHostVar) -> None: + self.ccode.write(lhostvar.name) + + def visit_lhostmem(self, lhostmem: CH.CLHostMem) -> None: + self.ccode.write("*(") + lhostmem.exp.accept(self) + self.ccode.write(")") + + def visit_nooffset(self, nooffset: CO.CNoOffset) -> None: + pass + + def visit_fieldoffset(self, fieldoffset: CO.CFieldOffset) -> None: + self.ccode.write(".") + self.ccode.write(fieldoffset.fieldname) + fieldoffset.offset.accept(self) + + def visit_indexoffset(self, indexoffset: CO.CIndexOffset) -> None: + pass + + def visit_explval(self, explval: CE.CExpLval) -> None: + explval.lval.accept(self) + + def visit_sizeof(self, sizeof: CE.CExpSizeOf) -> None: + pass + + def visit_sizeofe(self, sizeofe: CE.CExpSizeOfE) -> None: + pass + + def visit_size_of_str(self, sizeofstr: CE.CExpSizeOfStr) -> None: + pass + + def visit_alignof(self, alignof: CE.CExpAlignOf) -> None: + pass + + def visit_alignofe(self, alignofe: CE.CExpAlignOfE) -> None: + pass + + def visit_unop(self, unop: CE.CExpUnOp) -> None: + pass + + def visit_binop(self, binop: CE.CExpBinOp) -> None: + self.ccode.write("(") + binop.exp1.accept(self) + self.ccode.write(operators[binop.op]) + binop.exp2.accept(self) + self.ccode.write(")") + + def visit_question(self, question: CE.CExpQuestion) -> None: + pass + + def visit_cast(self, ecast: CE.CExpCastE) -> None: + self.ccode.write("(") + ecast.typ.accept(self) + self.ccode.write(")") + ecast.exp.accept(self) + + def visit_addrof(self, addrof: CE.CExpAddrOf) -> None: + if addrof.lval.is_var: + self.ccode.write("&") + addrof.lval.accept(self) + else: + self.ccode.write("&(") + addrof.lval.accept(self) + self.ccode.write(")") + + def visit_addr_of_label(self, addroflabel: CE.CExpAddrOfLabel) -> None: + pass + + def visit_startof(self, startof: CE.CExpStartOf) -> None: + pass + + def visit_fn_app(self, fnapp: CE.CExpFnApp) -> None: + pass + + def visit_cn_app(self, cnapp: CE.CExpCnApp) -> None: + pass + + def visit_attributes(self, a: CA.CAttributes) -> None: + for attr in a.attributes: + attr.accept(self) + + def visit_attribute(self, a: CA.CAttribute) -> None: + if len(a.params) == 0: + self.ccode.write(a.name) + self.ccode.write(" ") + else: + self.ccode.write("attribute not yet supported " + str(a)) + + def visit_attr_int(self, a: CA.CAttrInt) -> None: + pass + + def visit_attr_str(self, a: CA.CAttrStr) -> None: + pass + + def visit_attr_cons(self, a: CA.CAttrCons) -> None: + pass + + def visit_attr_sizeof(self, a: CA.CAttrSizeOf) -> None: + pass + + def visit_attr_sizeofe(self, a: CA.CAttrSizeOfE) -> None: + pass + + def visit_attr_sizeofs(self, a: CA.CAttrSizeOfS) -> None: + pass + + def visit_attr_alignof(self, a: CA.CAttrAlignOf) -> None: + pass + + def visit_attr_alignofe(self, a: CA.CAttrAlignOfE) -> None: + pass + + def visit_attr_alignofs(self, a: CA.CAttrAlignOfS) -> None: + pass + + def visit_attr_unop(self, a: CA.CAttrUnOp) -> None: + pass + + def visit_attr_binop(self, a: CA.CAttrBinOp) -> None: + pass + + def visit_attr_dot(self, a: CA.CAttrDot) -> None: + pass + + def visit_attr_star(self, a: CA.CAttrStar) -> None: + pass + + def visit_attr_addrof(self, a: CA.CAttrAddrOf) -> None: + pass + + def visit_attr_index(self, a: CA.CAttrIndex) -> None: + pass + + def visit_attr_question(self, a: CA.CAttrQuestion) -> None: + pass diff --git a/chc/app/CStmt.py b/chc/app/CStmt.py index 2901d6c..8c0ce94 100644 --- a/chc/app/CStmt.py +++ b/chc/app/CStmt.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -39,8 +39,11 @@ if TYPE_CHECKING: from chc.app.CExp import CExp from chc.app.CFile import CFile + from chc.app.CFileDeclarations import CFileDeclarations from chc.app.CFileDictionary import CFileDictionary from chc.app.CFunction import CFunction + from chc.app.CLocation import CLocation + from chc.app.CVisitor import CVisitor stmt_constructors: Dict[str, Callable[["CStmt", ET.Element], "CStmt"]] = { @@ -93,6 +96,10 @@ def cfun(self) -> "CFunction": def cfile(self) -> "CFile": return self.cfun.cfile + @property + def declarations(self) -> "CFileDeclarations": + return self.cfile.declarations + @property def cdictionary(self) -> "CFileDictionary": return self.cfile.dictionary @@ -121,6 +128,14 @@ def kind(self) -> str: else: raise UF.CHCError("stag missing from stmt") + @property + def location(self) -> "CLocation": + xiloc = self.xskind.get("iloc") + if xiloc is not None: + return self.declarations.get_location(int(xiloc)) + else: + raise UF.CHCError("No location found in statement " + str(self)) + @property def preds(self) -> List[int]: if self._preds is None: @@ -190,6 +205,9 @@ def strings(self) -> List[str]: def get_variable_uses(self, vid: int) -> int: return sum(s.get_variable_uses(vid) for s in self.stmts.values()) + def accept(self, visitor: "CVisitor") -> None: + raise UF.CHCError("visitor not yet accepted on: " + str(self)) + def __str__(self) -> str: lines: List[str] = [] predecessors = ",".join(str(p) for p in self.preds) @@ -235,6 +253,9 @@ def is_block_stmt(self) -> bool: def block_count(self) -> int: return sum(s.block_count for s in self.stmts.values()) + 1 + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_block(self) + class CFunctionBody(CBlock): @@ -250,6 +271,9 @@ def cfun(self) -> "CFunction": def is_function_body(self) -> bool: return self.parent is None + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_function_body(self) + class CIfStmt(CStmt): @@ -273,6 +297,22 @@ def stmts(self) -> Dict[int, "CStmt"]: self._stmts[s.sid] = s return self._stmts + @property + def ifstmt(self) -> Optional["CStmt"]: + xthen = self.xskind.find("thenblock") + if xthen is not None: + return CBlock(self, xthen) + else: + return None + + @property + def elsestmt(self) -> Optional["CStmt"]: + xelse = self.xskind.find("elseblock") + if xelse is not None: + return CBlock(self, xelse) + else: + return None + @property def condition(self) -> "CExp": xiexp = self.xskind.get("iexp") @@ -294,6 +334,9 @@ def get_variable_uses(self, vid: int) -> int: result: int = sum(s.get_variable_uses(vid) for s in self.stmts.values()) return result + self.condition.get_variable_uses(vid) + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_if_stmt(self) + def __str__(self) -> str: return CStmt.__str__(self) + ": " + str(self.condition) @@ -317,6 +360,9 @@ def stmts(self) -> Dict[int, "CStmt"]: raise UF.CHCError("Loop stmt without nested block") return self._stmts + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_loop_stmt(self) + class CSwitchStmt(CStmt): @@ -337,24 +383,36 @@ def stmts(self) -> Dict[int, "CStmt"]: raise UF.CHCError("Switch stmt without nested block") return self._stmts + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_switch_stmt(self) + class CBreakStmt(CStmt): def __init__(self, parent: "CStmt", xnode: ET.Element) -> None: CStmt.__init__(self, parent, xnode) + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_break_stmt(self) + class CContinueStmt(CStmt): def __init__(self, parent: "CStmt", xnode: ET.Element) -> None: CStmt.__init__(self, parent, xnode) + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_continue_stmt(self) + class CGotoStmt(CStmt): def __init__(self, parent: "CStmt", xnode: ET.Element) -> None: CStmt.__init__(self, parent, xnode) + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_goto_stmt(self) + class CReturnStmt(CStmt): """Function return.""" @@ -362,6 +420,17 @@ class CReturnStmt(CStmt): def __init__(self, parent: "CStmt", xnode: ET.Element) -> None: CStmt.__init__(self, parent, xnode) + @property + def exp(self) -> Optional["CExp"]: + xreturnval = self.xskind.get("iexp") + if xreturnval is not None: + return self.cdictionary.get_exp(int(xreturnval)) + else: + return None + + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_return_stmt(self) + class CInstrsStmt(CStmt): """Sequence of instructions without control flow.""" @@ -403,6 +472,9 @@ def call_instrs(self) -> List["CCallInstr"]: result.append(cast("CCallInstr", i)) return result + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_instrs_stmt(self) + def __str__(self) -> str: lines: List[str] = [] lines.append(CStmt.__str__(self)) diff --git a/chc/app/CTypeInfo.py b/chc/app/CTypeInfo.py index 3442eb3..026a99c 100644 --- a/chc/app/CTypeInfo.py +++ b/chc/app/CTypeInfo.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -37,6 +37,7 @@ if TYPE_CHECKING: from chc.app.CDeclarations import CDeclarations from chc.app.CTyp import CTyp + from chc.app.CVisitor import CVisitor class CTypeInfo(CDeclarationsRecord): @@ -58,5 +59,8 @@ def name(self) -> str: def type(self) -> "CTyp": return self.dictionary.get_typ(self.args[0]) + def accept(self, visitor: "CVisitor") -> None: + visitor.visit_typeinfo(self) + def __str__(self) -> str: return self.name + ":" + str(self.type) diff --git a/chc/app/CVisitor.py b/chc/app/CVisitor.py index 0844c5d..61cb9c2 100644 --- a/chc/app/CVisitor.py +++ b/chc/app/CVisitor.py @@ -28,17 +28,133 @@ from abc import ABC, abstractmethod +from typing import TYPE_CHECKING + import chc.app.CAttributes as CA import chc.app.CExp as CE +import chc.app.CInstr as CI +import chc.app.CLHost as CH +import chc.app.CLval as CL +import chc.app.COffset as CO +import chc.app.CStmt as CS import chc.app.CTyp as CT from chc.app.CVarInfo import CVarInfo +if TYPE_CHECKING: + from chc.app.CFileGlobals import CGCompTag, CGType, CGVarDef + from chc.app.CCompInfo import CCompInfo + from chc.app.CFieldInfo import CFieldInfo + from chc.app.CInitInfo import ( + CSingleInitInfo, CCompoundInitInfo, COffsetInitInfo) + from chc.app.CLocation import CLocation + from chc.app.CTypeInfo import CTypeInfo + class CVisitor(ABC): def __init__(self) -> None: pass + @abstractmethod + def visit_location(self, loc: "CLocation") -> None: + ... + + @abstractmethod + def visit_cgtype(self, cgtype: "CGType") -> None: + ... + + @abstractmethod + def visit_cgcomptag(self, cgcomptag: "CGCompTag") -> None: + ... + + @abstractmethod + def visit_cgvardef(self, cgvardef: "CGVarDef") -> None: + ... + + @abstractmethod + def visit_typeinfo(self, typeinfo: "CTypeInfo") -> None: + ... + + @abstractmethod + def visit_compinfo(self, compinfo: "CCompInfo") -> None: + ... + + @abstractmethod + def visit_fieldinfo(self, fieldinfo: "CFieldInfo") -> None: + ... + + @abstractmethod + def visit_single_initinfo(self, initinfo: "CSingleInitInfo") -> None: + ... + + @abstractmethod + def visit_compound_initinfo(self, initinfo: "CCompoundInitInfo") -> None: + ... + + @abstractmethod + def visit_offset_initinfo(self, initinfo: "COffsetInitInfo") -> None: + ... + + @abstractmethod + def visit_block(self, cblock: CS.CBlock) -> None: + ... + + @abstractmethod + def visit_function_body(self, cbody: CS.CFunctionBody) -> None: + ... + + @abstractmethod + def visit_if_stmt(self, ifstmt: CS.CIfStmt) -> None: + ... + + @abstractmethod + def visit_loop_stmt(self, loopstmt: CS.CLoopStmt) -> None: + ... + + @abstractmethod + def visit_switch_stmt(self, switchstmt: CS.CSwitchStmt) -> None: + ... + + @abstractmethod + def visit_break_stmt(self, breakstmt: CS.CBreakStmt) -> None: + ... + + @abstractmethod + def visit_continue_stmt(self, continuestmt: CS.CContinueStmt) -> None: + ... + + @abstractmethod + def visit_goto_stmt(self, gotostmt: CS.CGotoStmt) -> None: + ... + + @abstractmethod + def visit_return_stmt(self, returnstmt: CS.CReturnStmt) -> None: + ... + + @abstractmethod + def visit_instrs_stmt(self, instrsstmt: CS.CInstrsStmt) -> None: + ... + + @abstractmethod + def visit_assign_instr(self, assigninstr: CI.CAssignInstr) -> None: + ... + + @abstractmethod + def visit_call_instr(self, callinstr: CI.CCallInstr) -> None: + ... + + @abstractmethod + def visit_asm_instr(self, asminstr: CI.CAsmInstr) -> None: + ... + + @abstractmethod + def visit_asm_output(self, asmoutput: CI.CAsmOutput) -> None: + ... + + @abstractmethod + def visit_asm_input(self, asminput: CI.CAsmInput) -> None: + ... + @abstractmethod def visit_voidtyp(self, ctyp: CT.CTypVoid) -> None: ... @@ -87,10 +203,162 @@ def visit_funarg(self, ctyp: CT.CFunArg) -> None: def visit_funargs(self, ctyp: CT.CFunArgs) -> None: ... + @abstractmethod + def visit_lval(self, lval: CL.CLval) -> None: + ... + + @abstractmethod + def visit_lhostvar(self, lhostvar: CH.CLHostVar) -> None: + ... + + @abstractmethod + def visit_lhostmem(self, lhostmem: CH.CLHostMem) -> None: + ... + + @abstractmethod + def visit_nooffset(self, nooffset: CO.CNoOffset) -> None: + ... + + @abstractmethod + def visit_fieldoffset(self, fieldoffset: CO.CFieldOffset) -> None: + ... + + @abstractmethod + def visit_indexoffset(self, indexoffset: CO.CIndexOffset) -> None: + ... + + @abstractmethod + def visit_constexp(self, c: CE.CExpConst) -> None: + ... + + @abstractmethod + def visit_explval(self, lval: CE.CExpLval) -> None: + ... + + @abstractmethod + def visit_sizeof(self, sizeof: CE.CExpSizeOf) -> None: + ... + + @abstractmethod + def visit_sizeofe(self, sizeofe: CE.CExpSizeOfE) -> None: + ... + + @abstractmethod + def visit_size_of_str(self, sizeofstr: CE.CExpSizeOfStr) -> None: + ... + + @abstractmethod + def visit_alignof(self, alignof: CE.CExpAlignOf) -> None: + ... + + @abstractmethod + def visit_alignofe(self, alignofe: CE.CExpAlignOfE) -> None: + ... + + @abstractmethod + def visit_unop(self, unop: CE.CExpUnOp) -> None: + ... + + @abstractmethod + def visit_binop(self, binop: CE.CExpBinOp) -> None: + ... + + @abstractmethod + def visit_question(self, question: CE.CExpQuestion) -> None: + ... + + @abstractmethod + def visit_cast(self, ecast: CE.CExpCastE) -> None: + ... + + @abstractmethod + def visit_addrof(self, addrof: CE.CExpAddrOf) -> None: + ... + + @abstractmethod + def visit_addr_of_label(self, addroflabel: CE.CExpAddrOfLabel) -> None: + ... + + @abstractmethod + def visit_startof(self, startof: CE.CExpStartOf) -> None: + ... + + @abstractmethod + def visit_fn_app(self, fnapp: CE.CExpFnApp) -> None: + ... + + @abstractmethod + def visit_cn_app(self, cnapp: CE.CExpCnApp) -> None: + ... + @abstractmethod def visit_attributes(self, a: CA.CAttributes) -> None: ... @abstractmethod - def visit_constexp(self, a: CE.CExpConst) -> None: + def visit_attribute(self, a: CA.CAttribute) -> None: + ... + + @abstractmethod + def visit_attr_int(self, a: CA.CAttrInt) -> None: + ... + + @abstractmethod + def visit_attr_str(self, a: CA.CAttrStr) -> None: + ... + + @abstractmethod + def visit_attr_cons(self, a: CA.CAttrCons) -> None: + ... + + @abstractmethod + def visit_attr_sizeof(self, a: CA.CAttrSizeOf) -> None: + ... + + @abstractmethod + def visit_attr_sizeofe(self, a: CA.CAttrSizeOfE) -> None: + ... + + @abstractmethod + def visit_attr_sizeofs(self, a: CA.CAttrSizeOfS) -> None: + ... + + @abstractmethod + def visit_attr_alignof(self, a: CA.CAttrAlignOf) -> None: + ... + + @abstractmethod + def visit_attr_alignofe(self, a: CA.CAttrAlignOfE) -> None: + ... + + @abstractmethod + def visit_attr_alignofs(self, a: CA.CAttrAlignOfS) -> None: + ... + + @abstractmethod + def visit_attr_unop(self, a: CA.CAttrUnOp) -> None: + ... + + @abstractmethod + def visit_attr_binop(self, a: CA.CAttrBinOp) -> None: + ... + + @abstractmethod + def visit_attr_dot(self, a: CA.CAttrDot) -> None: + ... + + @abstractmethod + def visit_attr_star(self, a: CA.CAttrStar) -> None: + ... + + @abstractmethod + def visit_attr_addrof(self, a: CA.CAttrAddrOf) -> None: + ... + + @abstractmethod + def visit_attr_index(self, a: CA.CAttrIndex) -> None: + ... + + @abstractmethod + def visit_attr_question(self, a: CA.CAttrQuestion) -> None: ... diff --git a/chc/cmdline/c_file/cfileutil.py b/chc/cmdline/c_file/cfileutil.py index d715bd5..c46f6ea 100644 --- a/chc/cmdline/c_file/cfileutil.py +++ b/chc/cmdline/c_file/cfileutil.py @@ -400,6 +400,75 @@ def cfile_mk_headerfile(args: argparse.Namespace) -> NoReturn: exit(0) +def cfile_cil_source(args: argparse.Namespace) -> NoReturn: + """Outputs a textual representation of the CIL AST. """ + + # arguments + xcfilename: str = args.filename + opttgtpath: Optional[str] = args.tgtpath + loglevel: str = args.loglevel + logfilename: Optional[str] = args.logfilename + logfilemode: str = args.logfilemode + xoutput: Optional[str] = args.output + + projectpath = os.path.dirname(os.path.abspath(xcfilename)) + targetpath = projectpath if opttgtpath is None else opttgtpath + targetpath = os.path.abspath(targetpath) + cfilename_ext = os.path.basename(xcfilename) + cfilename = cfilename_ext[:-2] + projectname = cfilename + + set_logging( + loglevel, + targetpath, + logfilename=logfilename, + mode=logfilemode, + msg="Command cfile mk-headerfile was invoked") + + chklogger.logger.info( + "Project path: %s; target path: %s", projectpath, targetpath) + + parsearchive = UF.get_parse_archive(targetpath, projectname) + + if not os.path.isfile(parsearchive): + print_error("Please run parser first on c file") + exit(1) + + if os.path.isfile(parsearchive): + chklogger.logger.info("Directory is changed to %s", targetpath) + os.chdir(targetpath) + tarname = os.path.basename(parsearchive) + cmd = ["tar", "xfz", os.path.basename(tarname)] + chklogger.logger.info("Semantics is extracted from %s", tarname) + result = subprocess.call(cmd, cwd=targetpath, stderr=subprocess.STDOUT) + if result != 0: + print_error("Error in extracting " + tarname) + exit(1) + chklogger.logger.info( + "Semantics was successfully extracted from %s", tarname) + + contractpath = os.path.join(targetpath, "chc_contracts") + + capp = CApplication( + projectpath, projectname, targetpath, contractpath, singlefile=True) + + capp.initialize_single_file(cfilename) + cfile = capp.get_cfile() + + fcilsource = cfile.cil_source() + + if xoutput is not None: + outputfilename = xoutput + ".cil.c" + with open(outputfilename, "w") as fp: + fp.write(fcilsource) + print("Cil source code written to " + outputfilename) + + else: + print(fcilsource) + + exit(0) + + def cfile_analyze_file(args: argparse.Namespace) -> NoReturn: """Analyzes a single c-file and saves the results in the .cch directory. diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc index cdf0c52..12921a7 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -710,6 +710,34 @@ def parse() -> argparse.Namespace: help="file mode for log file: append (a, default), or write (w)") cfilemkheader.set_defaults(func=C.cfile_mk_headerfile) + # --- cil-source + cfilecilsource = cfileparsers.add_parser("cil-source") + cfilecilsource.add_argument( + "filename", + help="name of file to be printed as cil-source text") + cfilecilsource.add_argument( + "--tgtpath", + help="directory in which to store the analysis artifacts " + + "(default: )") + cfilecilsource.add_argument( + "--output", "-o", + help=("basename of file to save output " + + "(without extension): a file with extension .cil.c will be created")) + cfilecilsource.add_argument( + "--loglevel", "-log", + choices=UL.LogLevel.options(), + default="NONE", + help="activate logging with given level (default to stderr)") + cfilecilsource.add_argument( + "--logfilename", + help="name of file to write log messages") + cfilecilsource.add_argument( + "--logfilemode", + choices=["a", "w"], + default="a", + help="file mode for log file: append (a, default), or write (w)") + cfilecilsource.set_defaults(func=C.cfile_cil_source) + # --- analyze cfileanalyze = cfileparsers.add_parser("analyze") cfileanalyze.add_argument( From 5ccf5a823d7cd332fe828c053a39a623f9791549 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 19 Nov 2025 16:42:27 -0800 Subject: [PATCH 08/22] PROOF: add return values to output parameter results --- chc/app/CContextDictionary.py | 10 ++ chc/app/CDictionary.py | 7 ++ chc/app/CFileDeclarations.py | 16 ++++ chc/app/CFunction.py | 62 +++++++++--- chc/app/CFunctionReturnSite.py | 92 ++++++++++++++++++ chc/cmdline/c_file/cfileutil.py | 17 ++-- chc/proof/OutputParameterChecker.py | 143 ++++++++++++++++++++++++---- chc/util/fileutil.py | 18 ++++ 8 files changed, 327 insertions(+), 38 deletions(-) create mode 100644 chc/app/CFunctionReturnSite.py diff --git a/chc/app/CContextDictionary.py b/chc/app/CContextDictionary.py index 09f22ff..c612a52 100644 --- a/chc/app/CContextDictionary.py +++ b/chc/app/CContextDictionary.py @@ -88,6 +88,16 @@ def get_program_context(self, ix: int) -> ProgramContext: def get_program_context_map(self) -> Dict[int, IndexedTableValue]: return self.context_table.objectmap(self.get_program_context) + # ----------------- read_xml service --------------------------------------- + + def read_xml_program_context( + self, node: ET.Element, tag: str = "ictxt") -> ProgramContext: + xtag = node.get(tag) + if xtag is not None: + return self.get_program_context(int(xtag)) + else: + raise UF.CHCError(f"Xml element {node.tag} is missing attribute {tag}") + # ----------------------- Printing ----------------------------------------- def objectmap_to_string(self, name: str) -> str: diff --git a/chc/app/CDictionary.py b/chc/app/CDictionary.py index 349335e..c74bad5 100644 --- a/chc/app/CDictionary.py +++ b/chc/app/CDictionary.py @@ -268,6 +268,13 @@ def read_xml_exp(self, node: ET.Element, tag: str = "iexp") -> CExp: else: raise Exception('xml node was missing the tag "' + tag + '"') + def read_xml_exp_o( + self, node: ET.Element, tag: str = "iexp") -> Optional[CExp]: + xtag_o = node.get(tag) + if xtag_o is not None: + return self.get_exp(int(xtag_o)) + return None + def write_xml_exp_opt( self, node: ET.Element, diff --git a/chc/app/CFileDeclarations.py b/chc/app/CFileDeclarations.py index c70dd07..2ad2366 100644 --- a/chc/app/CFileDeclarations.py +++ b/chc/app/CFileDeclarations.py @@ -37,6 +37,7 @@ List, Mapping, NoReturn, + Optional, Tuple, TYPE_CHECKING) import xml.etree.ElementTree as ET @@ -92,6 +93,10 @@ def xget_int_attr(p: ET.Element, tag: str) -> int: return UF.xget_int_attr(p, tag, "CFileDeclarations") +def xget_int_attr_o(node: ET.Element, tag: str) -> Optional[int]: + return UF.xget_int_attr_o(node, tag) + + class CFilename(CDeclarationsRecord): def __init__(self, decls: CDeclarations, ixval: IndexedTableValue): @@ -266,6 +271,17 @@ def read_xml_location( return CLocation(self, itv) return self.get_location(index) + def read_xml_location_o( + self, xnode: ET.Element, tag: str = "iloc") -> Optional[CLocation]: + index = xget_int_attr_o(xnode, tag) + if index is not None: + if index == -1: + args = [-1, -1, -1] + itv = IndexedTableValue(-1, [], args) + return CLocation(self, itv) + return self.get_location(index) + return None + # -------------------- Index items by category --------------------------- def index_filename(self, name: str) -> int: diff --git a/chc/app/CFunction.py b/chc/app/CFunction.py index dde60a3..49e5ddb 100644 --- a/chc/app/CFunction.py +++ b/chc/app/CFunction.py @@ -35,9 +35,10 @@ from chc.api.CFunctionApi import CFunctionApi -from chc.app.CLocation import CLocation from chc.app.CFunDeclarations import CFunDeclarations from chc.app.CInstr import CCallInstr +from chc.app.CFunctionReturnSite import CFunctionReturnSite +from chc.app.CLocation import CLocation from chc.app.CStmt import CFunctionBody from chc.app.IndexManager import FileVarReference @@ -159,6 +160,7 @@ def __init__(self, cfile: "CFile", xnode: ET.Element, fname: str) -> None: self._formals: Dict[int, "CVarInfo"] = {} # vid -> CVarInfo self._locals: Dict[int, "CVarInfo"] = {} # vid -> CVarInfo self._sbody: Optional[CFunctionBody] = None + self._returnsites: Optional[List[CFunctionReturnSite]] = None self._podictionary: Optional[CFunPODictionary] = None self._api: Optional[CFunctionApi] = None self._proofs: Optional[CFunctionProofs] = None @@ -373,6 +375,36 @@ def podictionary(self) -> CFunPODictionary: self._podictionary = CFunPODictionary(self, pxnode) return self._podictionary + @property + def returnsites(self) -> List[CFunctionReturnSite]: + if self._returnsites is None: + self._returnsites = [] + xsponode = UF.get_spo_xnode( + self.targetpath, + self.projectname, + self.cfilepath, + self.cfilename, + self.name) + if xsponode is None: + raise UF.CHCError(self.xmsg("spo file is missing")) + xxsponode = xsponode.find("spos") + if xxsponode is None: + raise UF.CHCError(self.xmsg("spo file has no spos element")) + xreturnsites = xxsponode.find("returnsites") + if xreturnsites is None: + raise UF.CHCError( + self.xmsg("spo file has no returnsites element")) + for xreturnsite in xreturnsites.findall("rs"): + self._returnsites.append(CFunctionReturnSite(self, xreturnsite)) + return self._returnsites + + def get_returnsite( + self, ctxtid: int) -> Optional[CFunctionReturnSite]: + for rs in self.returnsites: + if rs.context.index == ctxtid: + return rs + return None + @property def proofs(self) -> CFunctionProofs: if self._proofs is None: @@ -397,22 +429,30 @@ def proofs(self) -> CFunctionProofs: raise UF.CHCError(self.xmsg("spo file is missing")) xxsponode = xsponode.find("spos") if xxsponode is None: - raise UF.CHCError(self.xmsg("_spo file has no spos element")) + raise UF.CHCError(self.xmsg("spo file has no spos element")) self._proofs = CFunctionProofs(self, xxpponode, xxsponode) return self._proofs @property def analysis_info(self) -> CAnalysisInfo: if self._analysisinfo is None: - xpponode = UF.get_ppo_xnode( - self.targetpath, - self.projectname, - self.cfilepath, - self.cfilename, - self.name) - if xpponode is not None: - self._analysisinfo = ( - CAnalysisInfo(xpponode.find("analysis-info"), self)) + if UF.has_ppo_file( + self.targetpath, + self.projectname, + self.cfilepath, + self.cfilename, + self.name): + xpponode = UF.get_ppo_xnode( + self.targetpath, + self.projectname, + self.cfilepath, + self.cfilename, + self.name) + if xpponode is not None: + self._analysisinfo = ( + CAnalysisInfo(xpponode.find("analysis-info"), self)) + else: + self._analysisinfo = CAnalysisInfo(None, self) else: self._analysisinfo = CAnalysisInfo(None, self) return self._analysisinfo diff --git a/chc/app/CFunctionReturnSite.py b/chc/app/CFunctionReturnSite.py new file mode 100644 index 0000000..9cdbfcc --- /dev/null +++ b/chc/app/CFunctionReturnSite.py @@ -0,0 +1,92 @@ +# ------------------------------------------------------------------------------ +# CodeHawk C Analyzer +# Author: Henny Sipma +# ------------------------------------------------------------------------------ +# The MIT License (MIT) +# +# Copyright (c) 2025 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. +# ------------------------------------------------------------------------------ + +import xml.etree.ElementTree as ET + +from typing import Optional, TYPE_CHECKING + +if TYPE_CHECKING: + from chc.app.CContext import ProgramContext + from chc.app.CContext import CContextDictionary + from chc.app.CDictionary import CDictionary + from chc.app.CExp import CExp + from chc.app.CFile import CFile + from chc.app.CFileDeclarations import CFileDeclarations + from chc.app.CFunction import CFunction + from chc.app.CLocation import CLocation + + +class CFunctionReturnSite: + + def __init__(self, cfun: "CFunction", xnode: ET.Element) -> None: + self._cfun = cfun + self._xnode = xnode + + @property + def cfun(self) -> "CFunction": + return self._cfun + + @property + def cdictionary(self) -> "CDictionary": + return self.cfun.cdictionary + + @property + def cfile(self) -> "CFile": + return self.cfun.cfile + + @property + def cfiledeclarations(self) -> "CFileDeclarations": + return self.cfile.declarations + + @property + def contextdictionary(self) -> "CContextDictionary": + return self.cfile.contextdictionary + + @property + def xnode(self) -> ET.Element: + return self._xnode + + @property + def location(self) -> "CLocation": + return self.cfiledeclarations.read_xml_location(self.xnode) + + @property + def returnexp(self) -> Optional["CExp"]: + return self.cdictionary.read_xml_exp_o(self.xnode) + + @property + def context(self) -> "ProgramContext": + return self.contextdictionary.read_xml_program_context(self.xnode) + + def __str__(self): + rexp = str(self.returnexp) if self.returnexp else "" + return ( + "return " + rexp + " (" + + str(self.location.line) + ", " + str(self.location.byte) + + ") (" + + str(self.context) + ) diff --git a/chc/cmdline/c_file/cfileutil.py b/chc/cmdline/c_file/cfileutil.py index c46f6ea..dc1e943 100644 --- a/chc/cmdline/c_file/cfileutil.py +++ b/chc/cmdline/c_file/cfileutil.py @@ -653,14 +653,17 @@ def pofilter(po: "CFunctionPO") -> bool: print(RP.file_proofobligation_stats_tostring(cfile)) if canalysis == "outputparameters": + print("\n\nOutput parameter analysis results:\n") for cfun in cfile.functions.values(): - try: - op_checker = OutputParameterChecker(cfun) - print(str(op_checker)) - except UF.CHCError as e: - print("Skipping function " + cfun.name) - continue - + op_checker = OutputParameterChecker(cfun) + results = op_checker.results() + if len(results) > 0: + print("\nFunction: " + cfun.name + ": ") + for result in results: + if result.is_success(): + print(result.success_str()) + else: + print(result.failure_str()) exit(0) for fnname in cfunctions: diff --git a/chc/proof/OutputParameterChecker.py b/chc/proof/OutputParameterChecker.py index bb57613..f4e3d6d 100644 --- a/chc/proof/OutputParameterChecker.py +++ b/chc/proof/OutputParameterChecker.py @@ -25,17 +25,112 @@ # SOFTWARE. # ------------------------------------------------------------------------------ -from typing import List, Optional, TYPE_CHECKING +from typing import Dict, List, Optional, Tuple, TYPE_CHECKING if TYPE_CHECKING: + from chc.app.CContext import ProgramContext from chc.app.CContextDictionary import CContextDictionary + from chc.app.CExp import CExp from chc.app.CFile import CFile from chc.app.CFunction import CFunction, CAnalysisInfo, CandidateOutputParameter from chc.app.CVarInfo import CVarInfo from chc.proof.CFunctionPO import CFunctionPO +class OutputParameterResult: + + def __init__(self, varinfo: "CVarInfo") -> None: + self._varinfo = varinfo + self._fail_locally_initialized: List["CFunctionPO"] = [] + self._fail_all_or_nothing: Dict[int, List["CFunctionPO"]] = {} + self._returnsites: Dict[ + int, List[Tuple["ProgramContext", bool, Optional["CExp"]]]] = {} + + @property + def varinfo(self) -> "CVarInfo": + return self._varinfo + + @property + def fail_locally_initialized(self) -> List["CFunctionPO"]: + return self._fail_locally_initialized + + @property + def fail_all_or_nothing(self) -> Dict[int, List["CFunctionPO"]]: + return self._fail_all_or_nothing + + @property + def returnsites( + self) -> Dict[int, List[Tuple["ProgramContext", bool, Optional["CExp"]]]]: + return self._returnsites + + def is_failure(self) -> bool: + return ( + (len(self.fail_locally_initialized) > 0) + or (len(self.fail_all_or_nothing) > 0)) + + def is_success(self) -> bool: + return ( + (not self.is_failure()) + and any(r[0] for r in self.returnsites.values())) + + def add_locally_read(self, po_s: List["CFunctionPO"]) -> None: + self._fail_locally_initialized = po_s + + def add_fail_all_or_nothing( + self, ctxtid: int, po_s: List["CFunctionPO"]) -> None: + self._fail_all_or_nothing[ctxtid] = po_s + + def add_returnsite( + self, + ctxt: "ProgramContext", + byteloc: int, + allwritten: bool, + rv: Optional["CExp"] + ) -> None: + self._returnsites.setdefault(byteloc, []) + self._returnsites[byteloc].append((ctxt, allwritten, rv)) + + @property + def is_must_parameter(self) -> bool: + return all(r[0] for r in self.returnsites.values()) + + def success_str(self) -> str: + if not self.is_success: + return self.varinfo.vname + " is not an output parameter" + + rvlines: List[str] = [] + for (byteloc, contexts) in self.returnsites.items(): + rvlines.append(f" return site {byteloc}") + for (ctxt, allwritten, exp_o) in contexts: + pwritten = "all-written" if allwritten else "unaltered" + pexp = str(exp_o) if exp_o is not None else "no return value" + rvlines.append( + pwritten.rjust(14) + ": " + str(pexp).rjust(5) + + " (" + str(ctxt) + ")") + return ( + str(self.varinfo.vtype) + " " + self.varinfo.vname + ": " + + ("must-output-parameter" + if self.is_must_parameter else "may-output-parameter") + + "\nReturn values:\n" + + "\n".join(rvlines)) + + def failure_str(self) -> str: + lines: List[str] = [] + if len(self.fail_locally_initialized) > 0: + lines.append("Potential reads from the parameter: ") + for po in self.fail_locally_initialized: + lines.append(str(po)) + if len(self.fail_all_or_nothing) > 0: + lines.append("Potential failures to write all or nothing: ") + for (ctxtid, po_s) in self.fail_all_or_nothing.items(): + lines.append(str(ctxtid) + ": " + ", ".join(str(po) for po in po_s)) + if not (any(r[0] for r in self.returnsites.values())): + lines.append("Unable to prove fully written on any returnsite") + + return "\n".join(lines) + + class OutputParameterChecker: """Interpret the proof obligation results for output parameters.""" @@ -82,7 +177,8 @@ def candidate_ppos(self, candidate: "CVarInfo") -> List["CFunctionPO"]: return self.cfun.proofs.get_output_parameter_ppos(candidate.vname) - def is_pure_output_parameter(self, candidate: "CVarInfo") -> Optional[str]: + def is_pure_output_parameter( + self, candidate: "CVarInfo") -> OutputParameterResult: """Evaluate the status of the proof obligations related to the parameter. An output parameter is pure (that is, it can be safely converted to @@ -105,8 +201,16 @@ def is_pure_output_parameter(self, candidate: "CVarInfo") -> Optional[str]: ppos = self.candidate_ppos(candidate) ctxts = {ctxt.index for ctxt in [po.context for po in ppos]} - notread = all( - po.is_safe for po in ppos if po.predicate.is_locally_initialized) + result = OutputParameterResult(candidate) + + locallyread = list( + po for po in ppos + if po.predicate.is_locally_initialized and not po.is_safe) + + result.add_locally_read(locallyread) + + if result.is_failure(): + return result def allwritten(po_s: List["CFunctionPO"]) -> bool: return all(po.is_safe for po in po_s @@ -116,31 +220,30 @@ def allunaltered(po_s: List["CFunctionPO"]) -> bool: return all(po.is_safe for po in po_s if po.predicate.is_output_parameter_unaltered) - writtenonce = False - must_parameter = True - all_or_nothing_written = True for ctxtid in ctxts: + returnsite_o = self.cfun.get_returnsite(ctxtid) + returnexp_o = ( + returnsite_o.returnexp if returnsite_o is not None else None) ctxtppos = self.context_candidate_output_ppos(candidate, ctxtid) - if len(ctxtppos) > 0: + if len(ctxtppos) > 0 and returnsite_o is not None: + byteloc = ctxtppos[0].location.byte + ctxt = ctxtppos[0].context ctxt_allwritten = allwritten(ctxtppos) ctxt_allunaltered = allunaltered(ctxtppos) if not (ctxt_allwritten or ctxt_allunaltered): - all_or_nothing_written = False + result.add_fail_all_or_nothing(ctxtid, ctxtppos) elif ctxt_allunaltered: - must_parameter = False + result.add_returnsite(ctxt, byteloc, False, returnexp_o) elif ctxt_allwritten: - writtenonce = True - - issafe = notread and all_or_nothing_written and writtenonce + result.add_returnsite(ctxt, byteloc, True, returnexp_o) - if issafe: - if must_parameter: - return "must-output-parameter" - else: - return "may-output-parameter" + return result - else: - return None + def results(self) -> List[OutputParameterResult]: + opresults: List[OutputParameterResult] = [] + for candidate in self.candidate_parameters: + opresults.append(self.is_pure_output_parameter(candidate.parameter)) + return opresults def diagnostic(self, candidate: "CVarInfo") -> str: if self.is_pure_output_parameter(candidate): diff --git a/chc/util/fileutil.py b/chc/util/fileutil.py index 38f18a2..4a4b9f8 100644 --- a/chc/util/fileutil.py +++ b/chc/util/fileutil.py @@ -1285,6 +1285,17 @@ def get_ppo_filename( return os.path.join(fnpath, filename) +def has_ppo_file( + targetpath: str, + projectname: str, + cfilepath: Optional[str], + cfilename: str, + fnname: str) -> bool: + filename = get_ppo_filename( + targetpath, projectname, cfilepath, cfilename, fnname) + return os.path.isfile(filename) + + def get_ppo_xnode( targetpath: str, projectname: str, @@ -1961,6 +1972,13 @@ def xget_int_attr(p: ET.Element, tag: str, msg: str) -> int: return int(xdata) +def xget_int_attr_o(node: ET.Element, tag: str) -> Optional[int]: + xattrval = node.get(tag) + if xattrval is not None: + return int(xattrval) + return None + + if __name__ == "__main__": config = Config() From 0b1fb21f4228d1f1730f08873c6c213236999289 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 6 Dec 2025 15:23:39 -0800 Subject: [PATCH 09/22] CMD: delegate to analysis digests --- chc/cmdline/AnalysisManager.py | 4 +++ chc/cmdline/c_file/cfileutil.py | 31 ++++++++----------- chc/cmdline/c_project/cprojectutil.py | 44 +++++++++++++++++---------- chc/cmdline/chkc | 8 +++++ chc/cmdline/kendra/TestManager.py | 9 ++++-- 5 files changed, 59 insertions(+), 37 deletions(-) diff --git a/chc/cmdline/AnalysisManager.py b/chc/cmdline/AnalysisManager.py index 1873b96..2b993ae 100644 --- a/chc/cmdline/AnalysisManager.py +++ b/chc/cmdline/AnalysisManager.py @@ -56,6 +56,7 @@ def __init__( thirdpartysummaries: List[str] = [], keep_system_includes: bool = False, verbose: bool = False, + disable_timing: bool = False, collectdiagnostics: bool = False ) -> None: """Initialize the analyzer location and target file location. @@ -79,6 +80,7 @@ def __init__( self.thirdpartysummaries = thirdpartysummaries self.unreachability = unreachability self.verbose = verbose + self.disable_timing = disable_timing self._collectdiagnostics = collectdiagnostics @property @@ -309,6 +311,8 @@ def _generate_and_check_file_cmd_partial( cmd.append("-unreachability") if self.verbose: cmd.append("-verbose") + if self.disable_timing: + cmd.append("-disable_timing") if self.collect_diagnostics: cmd.append("-diagnostics") cmd.append(self.targetpath) diff --git a/chc/cmdline/c_file/cfileutil.py b/chc/cmdline/c_file/cfileutil.py index dc1e943..a73f177 100644 --- a/chc/cmdline/c_file/cfileutil.py +++ b/chc/cmdline/c_file/cfileutil.py @@ -66,8 +66,6 @@ from chc.app.CApplication import CApplication from chc.app.CPrettyPrinter import CPrettyPrinter -from chc.proof.OutputParameterChecker import OutputParameterChecker - import chc.reporting.ProofObligations as RP from chc.util.Config import Config @@ -76,6 +74,7 @@ if TYPE_CHECKING: from chc.app.CAttributes import CAttributes + from chc.app.CInstr import CCallInstr from chc.app.CTyp import ( CTypComp, CTypFloat, CTypFun, CTypInt, CTypPtr) from chc.proof.CFunctionPO import CFunctionPO @@ -652,18 +651,18 @@ def pofilter(po: "CFunctionPO") -> bool: print(RP.file_proofobligation_stats_tostring(cfile)) + def callsite_str(instr: "CCallInstr") -> str: + return ( + instr.parent.cfile.name + ".c:" + + instr.parent.cfun.name + ":" + + str(instr.location.line) + ) + if canalysis == "outputparameters": - print("\n\nOutput parameter analysis results:\n") for cfun in cfile.functions.values(): - op_checker = OutputParameterChecker(cfun) - results = op_checker.results() - if len(results) > 0: - print("\nFunction: " + cfun.name + ": ") - for result in results: - if result.is_success(): - print(result.success_str()) - else: - print(result.failure_str()) + print("\nFunction: " + cfun.name) + print(str(cfun.analysis_digests)) + exit(0) for fnname in cfunctions: @@ -848,12 +847,8 @@ def pofilter(po: "CFunctionPO") -> bool: if analysis == "outputparameters": for cfun in cfile.functions.values(): - try: - op_checker = OutputParameterChecker(cfun) - print(str(op_checker)) - except UF.CHCError as e: - print("Skipping function " + cfun.name + ": " + str(e)) - continue + print("\nFunction: " + cfun.name) + print(str(cfun.analysis_digests)) exit(0) diff --git a/chc/cmdline/c_project/cprojectutil.py b/chc/cmdline/c_project/cprojectutil.py index 8dc26dc..67879f0 100644 --- a/chc/cmdline/c_project/cprojectutil.py +++ b/chc/cmdline/c_project/cprojectutil.py @@ -49,8 +49,6 @@ from chc.linker.CLinker import CLinker -from chc.proof.OutputParameterChecker import OutputParameterChecker - import chc.reporting.ProofObligations as RP from chc.util.Config import Config @@ -61,7 +59,7 @@ from chc.app.CAttributes import CAttributes from chc.app.CFile import CFile from chc.app.CFunction import CFunction - from chc.app.CInstr import CInstr + from chc.app.CInstr import CInstr, CCallInstr from chc.app.CStmt import CInstrsStmt, CStmt from chc.app.CTyp import ( CTypComp, CTypFloat, CTypFun, CTypInt, CTypPtr) @@ -533,14 +531,17 @@ def cproject_report(args: argparse.Namespace) -> NoReturn: # arguments tgtpath: str = args.tgtpath projectname: str = args.projectname + canalysis: str = args.analysis + verbose: bool = args.verbose targetpath = os.path.abspath(tgtpath) projectpath = targetpath - result = UF.read_project_summary_results(targetpath, projectname) - if result is not None: - print(RP.project_proofobligation_stats_dict_to_string(result)) - exit(0) + statsresult = UF.read_project_summary_results(targetpath, projectname) + if statsresult is not None: + print(RP.project_proofobligation_stats_dict_to_string(statsresult)) + if canalysis == "undefinedbehavior": + exit(0) if not UF.has_analysisresults_path(targetpath, projectname): print_error( @@ -558,13 +559,21 @@ def cproject_report(args: argparse.Namespace) -> NoReturn: UF.save_project_summary_results(targetpath, projectname, fresult) UF.save_project_summary_results_as_xml(targetpath, projectname, fresult) - result = UF.read_project_summary_results(targetpath, projectname) - if result is not None: - print(RP.project_proofobligation_stats_dict_to_string(result)) + statsresult = UF.read_project_summary_results(targetpath, projectname) + if statsresult is not None: + print(RP.project_proofobligation_stats_dict_to_string(statsresult)) else: print_error("Results were not readable") exit(1) + if canalysis == "outputparameters": + + for cfile in capp.files.values(): + print("\nFile: " + cfile.name) + for cfun in cfile.functions.values(): + print("\nFunction: " + cfun.name) + print(str(cfun.analysis_digests)) + exit(0) @@ -613,14 +622,17 @@ def pofilter(po: "CFunctionPO") -> bool: print(RP.file_proofobligation_stats_tostring(cfile)) + def callsite_str(instr: "CCallInstr") -> str: + return ( + instr.parent.cfile.name + ".c:" + + instr.parent.cfun.name + ":" + + str(instr.location.line) + ) + if canalysis == "outputparameters": for cfun in cfile.functions.values(): - try: - op_checker = OutputParameterChecker(cfun) - print(str(op_checker)) - except UF.CHCError as e: - print("Skipping function " + cfun.name) - continue + print("\nFunction: " + cfun.name) + print(str(cfun.analysis_digests)) exit(0) diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc index 12921a7..a21d562 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -1584,6 +1584,14 @@ def parse() -> argparse.Namespace: "tgtpath", help="directory that contains the analysis results") cprojectreport.add_argument( "projectname", help="name of the project") + cprojectreport.add_argument( + "--analysis", + default="undefined-behavior", + choices=["undefined-behavior", "outputparameters"], + help="choose analysis for reporting results") + cprojectreport.add_argument( + "--verbose", "-v", + action="store_true") cprojectreport.set_defaults(func=P.cproject_report) # --- report-file diff --git a/chc/cmdline/kendra/TestManager.py b/chc/cmdline/kendra/TestManager.py index d42ef3e..b898641 100644 --- a/chc/cmdline/kendra/TestManager.py +++ b/chc/cmdline/kendra/TestManager.py @@ -345,7 +345,8 @@ def test_ppos(self) -> None: ) cfilename = creffilename_c[:-2] capp.initialize_single_file(cfilename) - am = AnalysisManager(capp, verbose=self.verbose) + am = AnalysisManager( + capp, verbose=self.verbose, disable_timing=True) am.create_file_primary_proofobligations(cfilename) cfile = capp.get_cfile() capp.collect_post_assumes() @@ -588,7 +589,8 @@ def test_ppo_proofs(self, delaytest: bool = False) -> None: # only generate invariants if required if creffile.has_domains(): for d in creffile.domains: - am = AnalysisManager(capp, verbose=self.verbose) + am = AnalysisManager( + capp, verbose=self.verbose, disable_timing=True) am.generate_and_check_file(cfilename, None, d) cfile.reinitialize_tables() ppos = cfile.get_ppos() @@ -668,7 +670,8 @@ def test_spo_proofs(self, delaytest: bool = False) -> None: cappfile = capp.get_cfile() if creffile.has_domains(): for d in creffile.domains: - am = AnalysisManager(capp, verbose=self.verbose) + am = AnalysisManager( + capp, verbose=self.verbose, disable_timing=True) am.generate_and_check_file(cfilename, None, d) cappfile.reinitialize_tables() spos = cappfile.get_spos() From b8040a0a9b08e9abef498c66a7b0bbba120fe683 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 6 Dec 2025 15:31:00 -0800 Subject: [PATCH 10/22] CHC:INSTR: ignore vardecl for now --- chc/app/CInstr.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/chc/app/CInstr.py b/chc/app/CInstr.py index 375b0c0..fade09a 100644 --- a/chc/app/CInstr.py +++ b/chc/app/CInstr.py @@ -39,6 +39,7 @@ from chc.app.CFile import CFile from chc.app.CFileDictionary import CFileDictionary from chc.app.CFunction import CFunction + from chc.app.CLocation import CLocation from chc.app.CLval import CLval from chc.app.CStmt import CStmt from chc.app.CVisitor import CVisitor @@ -63,6 +64,10 @@ def cfun(self) -> "CFunction": def cdictionary(self) -> "CFileDictionary": return self.parent.cdictionary + @property + def location(self) -> "CLocation": + return self.cfun.cfiledecls.read_xml_location(self.xnode) + @property def is_assign(self) -> bool: return False From d07415d8d4f68b370bbfdb6c4cd03066b6f5322b Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 6 Dec 2025 15:32:47 -0800 Subject: [PATCH 11/22] DECL: replace exception on unrecognized InitInfo by printed msg --- chc/app/CGlobalDeclarations.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/chc/app/CGlobalDeclarations.py b/chc/app/CGlobalDeclarations.py index 59e057b..ba7b718 100644 --- a/chc/app/CGlobalDeclarations.py +++ b/chc/app/CGlobalDeclarations.py @@ -604,7 +604,9 @@ def index_init(self, init: CInitInfo, fid: int = -1) -> int: return self.mk_compound_init_index(init.tags, args) else: - raise Exception("InitInfo not recognized") + # raise Exception("InitInfo not recognized: " + str(init)) + print("InitInfo not recognized: " + str(init)) + return -1 def index_offset_init(self, oinit: COffsetInitInfo, fid: int = -1) -> int: args: List[int] = [ From bf450d317f93ee5b9af3d4f8efb4ea4619b91d58 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 6 Dec 2025 15:34:31 -0800 Subject: [PATCH 12/22] replace analysis-info with analysis-digest --- chc/app/CFunction.py | 136 ++++++++++--------------------------------- chc/app/CStmt.py | 2 + 2 files changed, 32 insertions(+), 106 deletions(-) diff --git a/chc/app/CFunction.py b/chc/app/CFunction.py index 49e5ddb..55b5808 100644 --- a/chc/app/CFunction.py +++ b/chc/app/CFunction.py @@ -47,12 +47,13 @@ from chc.invariants.CFunInvariantTable import CFunInvariantTable from chc.invariants.CInvariantFact import CInvariantFact -from chc.proof.CFunPODictionary import CFunPODictionary +from chc.proof.CFunctionAnalysisDigest import CFunctionAnalysisDigests from chc.proof.CFunctionCallsiteSPOs import CFunctionCallsiteSPOs from chc.proof.CFunctionPO import CFunctionPO from chc.proof.CFunctionPPO import CFunctionPPO from chc.proof.CFunctionProofs import CFunctionProofs from chc.proof.CFunctionSPOs import CFunctionSPOs +from chc.proof.CFunPODictionary import CFunPODictionary import chc.util.fileutil as UF from chc.util.loggingutil import chklogger @@ -69,85 +70,6 @@ from chc.app.CVarInfo import CVarInfo -class CandidateOutputParameter: - - def __init__( - self, - cfun: "CFunction", - cvar: "CVarInfo", - offsets: List["COffset"]) -> None: - self._cfun = cfun - self._cvar = cvar - self._offsets = offsets - - @property - def cfun(self) -> "CFunction": - return self._cfun - - @property - def parameter(self) -> "CVarInfo": - return self._cvar - - @property - def offsets(self) -> List["COffset"]: - return self._offsets - - def __str__(self) -> str: - return ( - self.parameter.vname + "[" + ", ".join(str(o) for o in self.offsets) + "]") - - -class CAnalysisInfo: - - def __init__(self, xnode: Optional[ET.Element], cfun: "CFunction") -> None: - self._xnode = xnode - self._cfun = cfun - - @property - def cfun(self) -> "CFunction": - return self._cfun - - @property - def cdictionary(self) -> "CDictionary": - return self.cfun.cdictionary - - @property - def cfiledecls(self) -> "CFileDeclarations": - return self.cfun.cfiledecls - - @property - def analysis(self) -> str: - if self._xnode is None: - return "undefined-behavior" - else: - return self._xnode.get("name", "unknown") - - @property - def candidate_parameters(self) -> List[CandidateOutputParameter]: - result: List[CandidateOutputParameter] = [] - if self._xnode is not None: - if self.analysis == "output-parameters": - xparams = self._xnode.find("candidate-parameters") - if xparams is not None: - xparamlist = xparams.findall("vinfo") - for xparam in xparamlist: - xid = int(xparam.get("xid", "-1")) - if xid > 0: - vinfo = self.cfiledecls.get_varinfo(xid) - xoffsets = xparam.get("offsets", "") - if xoffsets is not None: - offsets = list( - self.cdictionary.get_offset(int(i)) - for i in xoffsets.split(",")) - - result.append(CandidateOutputParameter( - self.cfun, vinfo, offsets)) - return result - - def __str__(self) -> str: - return ", ".join(str(vinfo) for vinfo in self.candidate_parameters) - - class CFunction: """Function implementation.""" @@ -167,7 +89,7 @@ def __init__(self, cfile: "CFile", xnode: ET.Element, fname: str) -> None: self._vard: Optional[CFunVarDictionary] = None self._invd: Optional[CFunInvDictionary] = None self._invarianttable: Optional[CFunInvariantTable] = None - self._analysisinfo: Optional[CAnalysisInfo] = None + self._analysis_digests: Optional[CFunctionAnalysisDigests] = None def xmsg(self, txt: str) -> str: return "Function " + self.name + ": " + txt @@ -375,6 +297,32 @@ def podictionary(self) -> CFunPODictionary: self._podictionary = CFunPODictionary(self, pxnode) return self._podictionary + @property + def analysis_digests(self) -> CFunctionAnalysisDigests: + if self._analysis_digests is None: + adnode = UF.get_adg_xnode( + self.targetpath, + self.projectname, + self.cfilepath, + self.cfilename, + self.name) + if adnode is None: + print("DEBUG: No adg file found") + adgnode = None + # raise UF.CHCError(self.xmsg("adg file not found")) + else: + adgnode = adnode.find("analysis-digests") + self._analysis_digests = CFunctionAnalysisDigests(self, adgnode) + return self._analysis_digests + + def callsites(self) -> List[CCallInstr]: + callinstrs = self.capp.get_callinstrs() + result: List[CCallInstr] = [] + for instr in callinstrs: + if str(instr.callee) == self.name: + result.append(instr) + return result + @property def returnsites(self) -> List[CFunctionReturnSite]: if self._returnsites is None: @@ -433,30 +381,6 @@ def proofs(self) -> CFunctionProofs: self._proofs = CFunctionProofs(self, xxpponode, xxsponode) return self._proofs - @property - def analysis_info(self) -> CAnalysisInfo: - if self._analysisinfo is None: - if UF.has_ppo_file( - self.targetpath, - self.projectname, - self.cfilepath, - self.cfilename, - self.name): - xpponode = UF.get_ppo_xnode( - self.targetpath, - self.projectname, - self.cfilepath, - self.cfilename, - self.name) - if xpponode is not None: - self._analysisinfo = ( - CAnalysisInfo(xpponode.find("analysis-info"), self)) - else: - self._analysisinfo = CAnalysisInfo(None, self) - else: - self._analysisinfo = CAnalysisInfo(None, self) - return self._analysisinfo - def reinitialize_tables(self) -> None: self._api = None self._podictionary = None @@ -547,7 +471,7 @@ def get_source_code_file(self) -> str: def has_line_number(self) -> bool: if self.has_source_code_file(): srcfile = self.get_source_code_file() - return self.cfile.cfilename + ".c" == srcfile + return self.cfile.name + ".c" == srcfile else: return False diff --git a/chc/app/CStmt.py b/chc/app/CStmt.py index 8c0ce94..be9b871 100644 --- a/chc/app/CStmt.py +++ b/chc/app/CStmt.py @@ -460,6 +460,8 @@ def instrs(self) -> List[CInstr]: self._instrs.append(CAssignInstr(self, xinode)) elif xitag == "asm": self._instrs.append(CAsmInstr(self, xinode)) + elif xitag == "vardecl": + pass else: raise UF.CHCError("unknown instruction tag: " + xitag) return self._instrs From 5d24d1f722722e3e9f9361ece6ef55e297ae3f3e Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 6 Dec 2025 15:35:24 -0800 Subject: [PATCH 13/22] UF: add file utility for analysis-digest file --- chc/util/fileutil.py | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/chc/util/fileutil.py b/chc/util/fileutil.py index 4a4b9f8..29f43f9 100644 --- a/chc/util/fileutil.py +++ b/chc/util/fileutil.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -1331,6 +1331,30 @@ def get_spo_xnode( filename, "function", "Secondary proof obligations file", show=False) +def get_adg_filename( + targetpath: str, + projectname: str, + cfilepath: Optional[str], + cfilename: str, + fnname: str) -> str: + fnpath = get_cfile_fnpath( + targetpath, projectname, cfilepath, cfilename, fnname) + filename = get_fn_composite(cfilename, fnname, "adg") + return os.path.join(fnpath, filename) + + +def get_adg_xnode( + targetpath: str, + projectname: str, + cfilepath: Optional[str], + cfilename: str, + fnname: str) -> Optional[ET.Element]: + filename = get_adg_filename( + targetpath, projectname, cfilepath, cfilename, fnname) + return get_xnode( + filename, "function", "Analysis digests file", show=False) + + def save_spo_file( targetpath: str, projectname: str, From 16ec1710e2d3d3ed53f77008e6398a65ecc33f9f Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 6 Dec 2025 15:41:32 -0800 Subject: [PATCH 14/22] PROOF: output-parameter analysis digest support --- chc/app/CHVersion.py | 2 +- chc/proof/CFunPODictionary.py | 18 ++ chc/proof/CFunPODictionaryRecord.py | 5 + chc/proof/CFunctionAnalysisDigest.py | 129 +++++++++ chc/proof/CPOPredicate.py | 67 ++++- chc/proof/CandidateOutputParameter.py | 138 ++++++++++ chc/proof/OutputParameterCalleeCallsite.py | 96 +++++++ chc/proof/OutputParameterChecker.py | 294 --------------------- chc/proof/OutputParameterStatus.py | 142 ++++++++++ 9 files changed, 595 insertions(+), 296 deletions(-) create mode 100644 chc/proof/CFunctionAnalysisDigest.py create mode 100644 chc/proof/CandidateOutputParameter.py create mode 100644 chc/proof/OutputParameterCalleeCallsite.py delete mode 100644 chc/proof/OutputParameterChecker.py create mode 100644 chc/proof/OutputParameterStatus.py diff --git a/chc/app/CHVersion.py b/chc/app/CHVersion.py index 840f1b3..7499ea5 100644 --- a/chc/app/CHVersion.py +++ b/chc/app/CHVersion.py @@ -1 +1 @@ -chcversion: str = "0.2.0-2025-11-18" +chcversion: str = "0.2.0-2025-12-06" diff --git a/chc/proof/CFunPODictionary.py b/chc/proof/CFunPODictionary.py index 3fbb5a8..2fce50c 100644 --- a/chc/proof/CFunPODictionary.py +++ b/chc/proof/CFunPODictionary.py @@ -36,6 +36,7 @@ from typing import Callable, Dict, List, Mapping, TYPE_CHECKING from chc.proof.AssumptionType import AssumptionType +from chc.proof.OutputParameterStatus import OutputParameterStatus from chc.proof.CFunPODictionaryRecord import podregistry from chc.proof.PPOType import PPOType from chc.proof.SPOType import SPOType @@ -66,10 +67,13 @@ def __init__( cfun: "CFunction", xnode: ET.Element) -> None: self._cfun = cfun + self.output_parameter_status_table = IndexedTable( + "output-parameter-status-table") self.assumption_type_table = IndexedTable("assumption-table") self.ppo_type_table = IndexedTable("ppo-type-table") self.spo_type_table = IndexedTable("spo-type-table") self.tables = [ + self.output_parameter_status_table, self.assumption_type_table, self.ppo_type_table, self.spo_type_table] @@ -102,6 +106,12 @@ def interfacedictionary(self) -> "InterfaceDictionary": # ------------------------ Retrieve items from dictionary ---------------- + def get_output_parameter_status(self, ix: int) -> OutputParameterStatus: + return podregistry.mk_instance( + self, + self.output_parameter_status_table.retrieve(ix), + OutputParameterStatus) + def get_assumption_type(self, ix: int) -> AssumptionType: return podregistry.mk_instance( self, self.assumption_type_table.retrieve(ix), AssumptionType) @@ -125,6 +135,14 @@ def get_spo_type_map(self) -> Dict[int, IndexedTableValue]: # ------------------------- Provide read/write xml service --------------- + def read_xml_output_parameter_status( + self, txnode: ET.Element, tag: str = "icops") -> OutputParameterStatus: + optix = txnode.get(tag) + if optix is not None: + return self.get_output_parameter_status(int(optix)) + else: + raise UF.CHCError("Error in reading output-parameter-status") + def read_xml_assumption_type( self, txnode: ET.Element, tag: str = "iast") -> AssumptionType: optix = txnode.get(tag) diff --git a/chc/proof/CFunPODictionaryRecord.py b/chc/proof/CFunPODictionaryRecord.py index fd9c8dc..b673819 100644 --- a/chc/proof/CFunPODictionaryRecord.py +++ b/chc/proof/CFunPODictionaryRecord.py @@ -36,6 +36,7 @@ from chc.app.CApplication import CApplication from chc.app.CContext import ProgramContext from chc.app.CContextDictionary import CContextDictionary + from chc.app.CDictionary import CDictionary from chc.app.CFile import CFile from chc.app.CFileDeclarations import CFileDeclarations from chc.app.CFunction import CFunction @@ -75,6 +76,10 @@ def cfile(self) -> "CFile": def cdecls(self) -> "CFileDeclarations": return self.cfile.declarations + @property + def cdictionary(self) -> "CDictionary": + return self.cfile.dictionary + @property def cxd(self) -> "CContextDictionary": return self.cfile.contextdictionary diff --git a/chc/proof/CFunctionAnalysisDigest.py b/chc/proof/CFunctionAnalysisDigest.py new file mode 100644 index 0000000..0a93824 --- /dev/null +++ b/chc/proof/CFunctionAnalysisDigest.py @@ -0,0 +1,129 @@ +# ------------------------------------------------------------------------------ +# CodeHawk C Analyzer +# Author: Henny Sipma +# ------------------------------------------------------------------------------ +# The MIT License (MIT) +# +# Copyright (c) 2025 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. +# ------------------------------------------------------------------------------ + +import xml.etree.ElementTree as ET + +from typing import List, Optional, TYPE_CHECKING + +from chc.proof.CandidateOutputParameter import CandidateOutputParameter +from chc.proof.OutputParameterCalleeCallsite import OutputParameterCalleeCallsite + + +if TYPE_CHECKING: + from chc.app.CFile import CFile + from chc.app.CFileDeclarations import CFileDeclarations + from chc.app.CFunction import CFunction + from chc.app.CVarInfo import CVarInfo + from chc.proof.CFunPODictionary import CFunPODictionary + + +class CFunctionAnalysisDigest: + + def __init__(self, cfun: "CFunction", xnode: ET.Element) -> None: + self.xnode = xnode # analysis-digest node in adg file + self._cfun = cfun + + @property + def cfun(self) -> "CFunction": + return self._cfun + + @property + def cfile(self) -> "CFile": + return self.cfun.cfile + + +class CFunctionOutputParameterAnalysisDigest(CFunctionAnalysisDigest): + + def __init__(self, cfun: "CFunction", xnode: ET.Element) -> None: + CFunctionAnalysisDigest.__init__(self, cfun, xnode) + self._candidate_parameters: Optional[List[CandidateOutputParameter]] = None + self._callee_callsites: Optional[List[OutputParameterCalleeCallsite]] = None + + @property + def parameters(self) -> List[CandidateOutputParameter]: + if self._candidate_parameters is None: + self._candidate_parameters = [] + xparams = self.xnode.find("candidate-parameters") + if xparams is not None: + for xparam in xparams.findall("param"): + cparam = CandidateOutputParameter(self, xparam) + self._candidate_parameters.append(cparam) + return self._candidate_parameters + + @property + def callee_callsites(self) -> List[OutputParameterCalleeCallsite]: + if self._callee_callsites is None: + self._callee_callsites = [] + xsites = self.xnode.find("callee-callsites") + if xsites is not None: + for xsite in xsites.findall("ccs"): + ccsite = OutputParameterCalleeCallsite(self, xsite) + self._callee_callsites.append(ccsite) + return self._callee_callsites + + def __str__(self) -> str: + lines: List[str] = [] + for p in self.parameters: + lines.append(str(p)) + if len(self.callee_callsites) > 0: + lines.append("\nCallee-callsites:") + for ccs in self.callee_callsites: + lines.append(" " + str(ccs)) + return "\n".join(lines) + + +class CFunctionAnalysisDigests: + + def __init__(self, cfun: "CFunction", xnode: Optional[ET.Element]) -> None: + self._cfun = cfun + self.xnode = xnode # analysis-digests node + self._digests: Optional[List[CFunctionAnalysisDigest]] = None + + @property + def cfun(self) -> "CFunction": + return self._cfun + + @property + def digests(self) -> List[CFunctionAnalysisDigest]: + if self._digests is None: + self._digests = [] + if self.xnode is not None: + for xdigest in self.xnode.findall("analysis-digest"): + digestkind = xdigest.get("name", "none") + if digestkind == "output parameters": + digest = CFunctionOutputParameterAnalysisDigest( + self.cfun, xdigest) + self._digests.append(digest) + else: + print("DEBUG: xnode is none") + return self._digests + + def __str__(self) -> str: + lines: List[str] = [] + for digest in self.digests: + lines.append(str(digest)) + return "\n".join(lines) diff --git a/chc/proof/CPOPredicate.py b/chc/proof/CPOPredicate.py index 43dd244..2003f4c 100644 --- a/chc/proof/CPOPredicate.py +++ b/chc/proof/CPOPredicate.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -80,7 +80,10 @@ 'no': 'no-overlap', 'nt': 'null-terminated', 'null': 'null', + "opa": "output_parameter-argument", 'opi': 'output_parameter-initialized', + "opne": "output_parameter-no-escape", + "ops": "output_parameter-scalar", 'opu': 'output_parameter-unaltered', 'pc': 'pointer-cast', 'plb': 'ptr-lower-bound', @@ -2319,3 +2322,65 @@ def __str__(self) -> str: + ", " + str(self.offset) + ")") + + +@pdregistry.register_tag("opa", CPOPredicate) +class CPOOutputParameterArgument(CPOPredicate): + + def __init__( + self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue + ) -> None: + CPOPredicate.__init__(self, pd, ixval) + + @property + def exp(self) -> "CExp": + return self.cd.get_exp(self.args[0]) + + def __str__(self) -> str: + return "output-parameter-argument(" + str(self.exp) + ")" + + +@pdregistry.register_tag("ops", CPOPredicate) +class CPOOutputParameterScalar(CPOPredicate): + + def __init__( + self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue + ) -> None: + CPOPredicate.__init__(self, pd, ixval) + + @property + def varinfo(self) -> "CVarInfo": + return self.cdeclarations.get_varinfo(self.args[0]) + + @property + def exp(self) -> "CExp": + return self.cd.get_exp(self.args[1]) + + def __str__(self) -> str: + return ( + "output-parameter-scalar(" + + str(self.varinfo) + ", " + + str(self.exp) + ")") + + +@pdregistry.register_tag("opne", CPOPredicate) +class CPOOutputParameterNoEscape(CPOPredicate): + + def __init__( + self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue + ) -> None: + CPOPredicate.__init__(self, pd, ixval) + + @property + def varinfo(self) -> "CVarInfo": + return self.cdeclarations.get_varinfo(self.args[0]) + + @property + def exp(self) -> "CExp": + return self.cd.get_exp(self.args[1]) + + def __str__(self) -> str: + return ( + "output-parameter-no-escape(" + + str(self.varinfo) + ", " + + str(self.exp) + ")") diff --git a/chc/proof/CandidateOutputParameter.py b/chc/proof/CandidateOutputParameter.py new file mode 100644 index 0000000..04764a7 --- /dev/null +++ b/chc/proof/CandidateOutputParameter.py @@ -0,0 +1,138 @@ +# ------------------------------------------------------------------------------ +# CodeHawk C Analyzer +# Author: Henny Sipma +# ------------------------------------------------------------------------------ +# The MIT License (MIT) +# +# Copyright (c) 2025 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. +# ------------------------------------------------------------------------------ + +import xml.etree.ElementTree as ET + +from typing import List, Optional, TYPE_CHECKING + +if TYPE_CHECKING: + from chc.app.CFile import CFile + from chc.app.CFileDeclarations import CFileDeclarations + from chc.app.CFunction import CFunction + from chc.app.CLocation import CLocation + from chc.app.CVarInfo import CVarInfo + from chc.proof.CFunPODictionary import CFunPODictionary + from chc.proof.CFunctionAnalysisDigest import ( + CFunctionOutputParameterAnalysisDigest) + from chc.proof.OutputParameterStatus import OutputParameterStatus + + +class COpParamReturnsite: + + def __init__(self, cop: "CandidateOutputParameter", xnode: ET.Element) -> None: + self._cop = cop + self.xnode = xnode + + @property + def cop(self) -> "CandidateOutputParameter": + return self._cop + + @property + def cfun(self) -> "CFunction": + return self.cop.cfun + + @property + def cfile(self) -> "CFile": + return self.cop.cfile + + @property + def fdecls(self) -> "CFileDeclarations": + return self.cfile.declarations + + @property + def podictionary(self) -> "CFunPODictionary": + return self.cfun.podictionary + + @property + def location(self) -> "CLocation": + return self.fdecls.read_xml_location(self.xnode) + + @property + def status(self) -> "OutputParameterStatus": + return self.podictionary.read_xml_output_parameter_status(self.xnode) + + def __str__(self) -> str: + return str(self.location.line) + ": " + str(self.status) + + +class CandidateOutputParameter: + + def __init__( + self, adg: "CFunctionOutputParameterAnalysisDigest", xnode: ET.Element + ) -> None: + self._adg = adg + self.xnode = xnode # param node + self._returnsites: Optional[List[COpParamReturnsite]] = None + # self._calldeps: Optional[List[CopParamCallDependency]] = None + + @property + def adg(self) -> "CFunctionOutputParameterAnalysisDigest": + return self._adg + + @property + def cfun(self) -> "CFunction": + return self.adg.cfun + + @property + def cfile(self) -> "CFile": + return self.adg.cfile + + @property + def podictionary(self) -> "CFunPODictionary": + return self.cfun.podictionary + + @property + def fdecls(self) -> "CFileDeclarations": + return self.cfile.declarations + + @property + def parameter(self) -> "CVarInfo": + return self.fdecls.read_xml_varinfo(self.xnode) + + @property + def status(self) -> "OutputParameterStatus": + return self.podictionary.read_xml_output_parameter_status(self.xnode) + + @property + def returnsites(self) -> List[COpParamReturnsite]: + if self._returnsites is None: + self._returnsites = [] + xreturns = self.xnode.find("returnsites") + if xreturns is not None: + for xreturn in xreturns.findall("rs"): + returnsite = COpParamReturnsite(self, xreturn) + self._returnsites.append(returnsite) + return self._returnsites + + def __str__(self) -> str: + lines: List[str] = [] + lines.append(str(self.parameter) + ": " + str(self.status)) + if not self.status.is_rejected: + lines.append("Return sites") + for returnsite in self.returnsites: + lines.append(" " + str(returnsite)) + return "\n".join(lines) diff --git a/chc/proof/OutputParameterCalleeCallsite.py b/chc/proof/OutputParameterCalleeCallsite.py new file mode 100644 index 0000000..80c2175 --- /dev/null +++ b/chc/proof/OutputParameterCalleeCallsite.py @@ -0,0 +1,96 @@ +# ------------------------------------------------------------------------------ +# CodeHawk C Analyzer +# Author: Henny Sipma +# ------------------------------------------------------------------------------ +# The MIT License (MIT) +# +# Copyright (c) 2025 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. +# ------------------------------------------------------------------------------ + +import xml.etree.ElementTree as ET + +from typing import List, Optional, TYPE_CHECKING + +if TYPE_CHECKING: + from chc.app.CExp import CExp + from chc.app.CFile import CFile + from chc.app.CFileDictionary import CFileDictionary + from chc.app.CFileDeclarations import CFileDeclarations + from chc.app.CFunction import CFunction + from chc.app.CLocation import CLocation + from chc.app.CVarInfo import CVarInfo + from chc.proof.CFunctionAnalysisDigest import ( + CFunctionOutputParameterAnalysisDigest) + from chc.proof.CFunPODictionary import CFunPODictionary + from chc.proof.OutputParameterStatus import OutputParameterStatus + + +class OutputParameterCalleeCallsite: + + def __init__( + self, adg: "CFunctionOutputParameterAnalysisDigest", xnode: ET.Element + ) -> None: + self._adg = adg + self.xnode = xnode + + @property + def adg(self) -> "CFunctionOutputParameterAnalysisDigest": + return self._adg + + @property + def cfun(self) -> "CFunction": + return self.adg.cfun + + @property + def cfile(self) -> "CFile": + return self.adg.cfile + + @property + def cdictionary(self) -> "CFileDictionary": + return self.cfile.dictionary + + @property + def podictionary(self) -> "CFunPODictionary": + return self.cfun.podictionary + + @property + def fdecls(self) -> "CFileDeclarations": + return self.cfile.declarations + + @property + def status(self) -> "OutputParameterStatus": + return self.podictionary.read_xml_output_parameter_status(self.xnode) + + @property + def location(self) -> "CLocation": + return self.fdecls.read_xml_location(self.xnode) + + @property + def callee(self) -> "CExp": + return self.cdictionary.read_xml_exp(self.xnode) + + def __str__(self) -> str: + return ( + str(self.location.line) + + ": " + + str(self.status) + + "; callee: " + + str(self.callee)) diff --git a/chc/proof/OutputParameterChecker.py b/chc/proof/OutputParameterChecker.py deleted file mode 100644 index f4e3d6d..0000000 --- a/chc/proof/OutputParameterChecker.py +++ /dev/null @@ -1,294 +0,0 @@ -# ------------------------------------------------------------------------------ -# CodeHawk C Analyzer -# Author: Henny Sipma -# ------------------------------------------------------------------------------ -# The MIT License (MIT) -# -# Copyright (c) 2025 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 Dict, List, Optional, Tuple, TYPE_CHECKING - - -if TYPE_CHECKING: - from chc.app.CContext import ProgramContext - from chc.app.CContextDictionary import CContextDictionary - from chc.app.CExp import CExp - from chc.app.CFile import CFile - from chc.app.CFunction import CFunction, CAnalysisInfo, CandidateOutputParameter - from chc.app.CVarInfo import CVarInfo - from chc.proof.CFunctionPO import CFunctionPO - - -class OutputParameterResult: - - def __init__(self, varinfo: "CVarInfo") -> None: - self._varinfo = varinfo - self._fail_locally_initialized: List["CFunctionPO"] = [] - self._fail_all_or_nothing: Dict[int, List["CFunctionPO"]] = {} - self._returnsites: Dict[ - int, List[Tuple["ProgramContext", bool, Optional["CExp"]]]] = {} - - @property - def varinfo(self) -> "CVarInfo": - return self._varinfo - - @property - def fail_locally_initialized(self) -> List["CFunctionPO"]: - return self._fail_locally_initialized - - @property - def fail_all_or_nothing(self) -> Dict[int, List["CFunctionPO"]]: - return self._fail_all_or_nothing - - @property - def returnsites( - self) -> Dict[int, List[Tuple["ProgramContext", bool, Optional["CExp"]]]]: - return self._returnsites - - def is_failure(self) -> bool: - return ( - (len(self.fail_locally_initialized) > 0) - or (len(self.fail_all_or_nothing) > 0)) - - def is_success(self) -> bool: - return ( - (not self.is_failure()) - and any(r[0] for r in self.returnsites.values())) - - def add_locally_read(self, po_s: List["CFunctionPO"]) -> None: - self._fail_locally_initialized = po_s - - def add_fail_all_or_nothing( - self, ctxtid: int, po_s: List["CFunctionPO"]) -> None: - self._fail_all_or_nothing[ctxtid] = po_s - - def add_returnsite( - self, - ctxt: "ProgramContext", - byteloc: int, - allwritten: bool, - rv: Optional["CExp"] - ) -> None: - self._returnsites.setdefault(byteloc, []) - self._returnsites[byteloc].append((ctxt, allwritten, rv)) - - @property - def is_must_parameter(self) -> bool: - return all(r[0] for r in self.returnsites.values()) - - def success_str(self) -> str: - if not self.is_success: - return self.varinfo.vname + " is not an output parameter" - - rvlines: List[str] = [] - for (byteloc, contexts) in self.returnsites.items(): - rvlines.append(f" return site {byteloc}") - for (ctxt, allwritten, exp_o) in contexts: - pwritten = "all-written" if allwritten else "unaltered" - pexp = str(exp_o) if exp_o is not None else "no return value" - rvlines.append( - pwritten.rjust(14) + ": " + str(pexp).rjust(5) - + " (" + str(ctxt) + ")") - return ( - str(self.varinfo.vtype) + " " + self.varinfo.vname + ": " - + ("must-output-parameter" - if self.is_must_parameter else "may-output-parameter") - + "\nReturn values:\n" - + "\n".join(rvlines)) - - def failure_str(self) -> str: - lines: List[str] = [] - if len(self.fail_locally_initialized) > 0: - lines.append("Potential reads from the parameter: ") - for po in self.fail_locally_initialized: - lines.append(str(po)) - if len(self.fail_all_or_nothing) > 0: - lines.append("Potential failures to write all or nothing: ") - for (ctxtid, po_s) in self.fail_all_or_nothing.items(): - lines.append(str(ctxtid) + ": " + ", ".join(str(po) for po in po_s)) - if not (any(r[0] for r in self.returnsites.values())): - lines.append("Unable to prove fully written on any returnsite") - - return "\n".join(lines) - - -class OutputParameterChecker: - """Interpret the proof obligation results for output parameters.""" - - def __init__(self, cfun: "CFunction") -> None: - self._cfun = cfun - - @property - def cfun(self) -> "CFunction": - return self._cfun - - @property - def analysis_info(self) -> "CAnalysisInfo": - return self.cfun.analysis_info - - @property - def cfile(self) -> "CFile": - return self.cfun.cfile - - @property - def contextdictionary(self) -> "CContextDictionary": - return self.cfile.contextdictionary - - def has_output_parameters(self) -> bool: - return self.cfun.analysis_info.analysis == "output-parameters" - - @property - def candidate_parameters(self) -> List["CandidateOutputParameter"]: - if self.has_output_parameters(): - return self.analysis_info.candidate_parameters - else: - return [] - - def context_candidate_output_ppos( - self, candidate: "CVarInfo", ctxtid: int) -> List["CFunctionPO"]: - """Return po's for a given parameter at a particular location in the ast.""" - - return [po for po in self.candidate_ppos(candidate) - if po.context.index == ctxtid - and (po.predicate.is_output_parameter_initialized - or po.predicate.is_output_parameter_unaltered)] - - def candidate_ppos(self, candidate: "CVarInfo") -> List["CFunctionPO"]: - """Return all po's for a given parameter.""" - - return self.cfun.proofs.get_output_parameter_ppos(candidate.vname) - - def is_pure_output_parameter( - self, candidate: "CVarInfo") -> OutputParameterResult: - """Evaluate the status of the proof obligations related to the parameter. - - An output parameter is pure (that is, it can be safely converted to - a Rust return value) if: - - 1) its dereference is not read within the function - 2) it is fully written at some return site - 3) it is either fully written or not written at all at all return sites - - The first condition is represented by proof obligations with predicate - PLocallyInitialized, which should all be safe. - - The second and third condition are represented by proof obligations with - POutputParameterInitialized and POutputParameterUnaltered. - - Note: - There are more conditions to come that have not yet been implemented. - """ - - ppos = self.candidate_ppos(candidate) - ctxts = {ctxt.index for ctxt in [po.context for po in ppos]} - - result = OutputParameterResult(candidate) - - locallyread = list( - po for po in ppos - if po.predicate.is_locally_initialized and not po.is_safe) - - result.add_locally_read(locallyread) - - if result.is_failure(): - return result - - def allwritten(po_s: List["CFunctionPO"]) -> bool: - return all(po.is_safe for po in po_s - if po.predicate.is_output_parameter_initialized) - - def allunaltered(po_s: List["CFunctionPO"]) -> bool: - return all(po.is_safe for po in po_s - if po.predicate.is_output_parameter_unaltered) - - for ctxtid in ctxts: - returnsite_o = self.cfun.get_returnsite(ctxtid) - returnexp_o = ( - returnsite_o.returnexp if returnsite_o is not None else None) - ctxtppos = self.context_candidate_output_ppos(candidate, ctxtid) - if len(ctxtppos) > 0 and returnsite_o is not None: - byteloc = ctxtppos[0].location.byte - ctxt = ctxtppos[0].context - ctxt_allwritten = allwritten(ctxtppos) - ctxt_allunaltered = allunaltered(ctxtppos) - if not (ctxt_allwritten or ctxt_allunaltered): - result.add_fail_all_or_nothing(ctxtid, ctxtppos) - elif ctxt_allunaltered: - result.add_returnsite(ctxt, byteloc, False, returnexp_o) - elif ctxt_allwritten: - result.add_returnsite(ctxt, byteloc, True, returnexp_o) - - return result - - def results(self) -> List[OutputParameterResult]: - opresults: List[OutputParameterResult] = [] - for candidate in self.candidate_parameters: - opresults.append(self.is_pure_output_parameter(candidate.parameter)) - return opresults - - def diagnostic(self, candidate: "CVarInfo") -> str: - if self.is_pure_output_parameter(candidate): - return "valid" - - lines: List[str] = [] - - ppos = self.candidate_ppos(candidate) - readppos = [po for po in ppos if po.predicate.is_locally_initialized] - readviolations = [po for po in readppos if po.is_violated] - readunknowns = [po for po in readppos if po.is_open] - if len(readviolations) + len(readunknowns) > 0: - lines.append("\nread violations and/or unknowns") - for po in (readviolations + readunknowns): - lines.append(str(po)) - - writeppos = [po for po in ppos - if po.predicate.is_output_parameter_initialized - or po.predicate.is_output_parameter_unaltered] - ctxts = {ctxt.index for ctxt in [po.context for po in ppos]} - - lines.append("\nfully written/unaltered violations and/or unknowns") - for index in ctxts: - output_po_s = self.context_candidate_output_ppos(candidate, index) - output_violations = [po for po in output_po_s if po.is_violated] - output_unknowns = [po for po in output_po_s if po.is_open] - if len(output_po_s) + len(output_unknowns) > 0: - ctxt = self.contextdictionary.get_program_context(index) - lines.append(str(ctxt)) - for po in (output_violations + output_unknowns): - lines.append(str(po)) - - return "\n".join(lines) - - def __str__(self) -> str: - lines: List[str] = [] - lines.append("\n\nOutput parameters for function " + self.cfun.name) - - for candidate in self.candidate_parameters: - if self.is_pure_output_parameter(candidate.parameter) is not None: - lines.append("\n- " + str(candidate.parameter.vname) + ": " - + str(self.is_pure_output_parameter( - candidate.parameter))) - else: - lines.append("- " + str(candidate.parameter.vname) + ": diagnostics:") - lines.append(self.diagnostic(candidate.parameter)) - - return "\n".join(lines) diff --git a/chc/proof/OutputParameterStatus.py b/chc/proof/OutputParameterStatus.py new file mode 100644 index 0000000..5b189fc --- /dev/null +++ b/chc/proof/OutputParameterStatus.py @@ -0,0 +1,142 @@ +# ------------------------------------------------------------------------------ +# CodeHawk C Analyzer +# Author: Henny Sipma +# ------------------------------------------------------------------------------ +# The MIT License (MIT) +# +# Copyright (c) 2025 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, TYPE_CHECKING + +from chc.proof.CFunPODictionaryRecord import CFunPODictionaryRecord, podregistry + + +from chc.util.IndexedTable import IndexedTableValue + + +if TYPE_CHECKING: + from chc.app.CDictionary import CDictionary + from chc.proof.CFunPODictionary import CFunPODictionary + + +class OutputParameterStatus(CFunPODictionaryRecord): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + CFunPODictionaryRecord.__init__(self, pod, ixval) + + @property + def is_unknown(self) -> bool: + return False + + @property + def is_rejected(self) -> bool: + return False + + @property + def is_viable(self) -> bool: + return False + + +@podregistry.register_tag("u", OutputParameterStatus) +class OutputParameterStatusUnknown(OutputParameterStatus): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterStatus.__init__(self, pod, ixval) + + @property + def is_unknown(self) -> bool: + return True + + def __str__(self) -> str: + return "Unknown" + + +@podregistry.register_tag("v", OutputParameterStatus) +class OutputParameterStatusViable(OutputParameterStatus): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterStatus.__init__(self, pod, ixval) + + @property + def is_viable(self) -> bool: + return True + + def __str__(self) -> str: + return "Viable" + + +@podregistry.register_tag("r", OutputParameterStatus) +class OutputParameterStatusRejected(OutputParameterStatus): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterStatus.__init__(self, pod, ixval) + + @property + def is_rejected(self) -> bool: + return True + + @property + def reason(self) -> List[str]: + return [self.cdictionary.get_string(arg) for arg in self.args] + + def __str__(self) -> str: + return "Rejected: " + "; ".join(self.reason) + + +@podregistry.register_tag("w", OutputParameterStatus) +class OutputParameterStatusWritten(OutputParameterStatus): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterStatus.__init__(self, pod, ixval) + + @property + def is_viable(self) -> bool: + return True + + def __str__(self) -> str: + return "Written" + + +@podregistry.register_tag("a", OutputParameterStatus) +class OutputParameterStatusUnaltered(OutputParameterStatus): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterStatus.__init__(self, pod, ixval) + + @property + def is_viable(self) -> bool: + return True + + def __str__(self) -> str: + return "Unaltered" From bad32a4c74e3cf7d84bdd48c6fe252c7c09d5dfc Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Mon, 8 Dec 2025 11:17:34 -0800 Subject: [PATCH 15/22] APP: allow for possibility of missing ppo's and invariants --- chc/app/CFunction.py | 20 ++++++++++++++++---- chc/reporting/ProofObligations.py | 31 ++++++++++++++++++------------- 2 files changed, 34 insertions(+), 17 deletions(-) diff --git a/chc/app/CFunction.py b/chc/app/CFunction.py index 55b5808..c4e1a93 100644 --- a/chc/app/CFunction.py +++ b/chc/app/CFunction.py @@ -581,16 +581,28 @@ def get_spos(self) -> List[CFunctionPO]: return self.proofs.spolist def get_open_ppos(self) -> List[CFunctionPO]: - return self.proofs.open_ppos + try: + return self.proofs.open_ppos + except UF.CHCFileNotFoundError: + return [] def get_open_spos(self) -> List[CFunctionPO]: return self.proofs.open_spos def get_ppos_violated(self) -> List[CFunctionPO]: - return self.proofs.ppos_violated + try: + return self.proofs.ppos_violated + except UF.CHCFileNotFoundError: + return [] def get_spo_violations(self) -> List[CFunctionPO]: - return self.proofs.get_spo_violations() + try: + return self.proofs.get_spo_violations() + except UF.CHCFileNotFoundError: + return [] def get_ppos_delegated(self) -> List[CFunctionPO]: - return self.proofs.ppos_delegated + try: + return self.proofs.ppos_delegated + except UF.CHCFileNotFoundError: + return [] diff --git a/chc/reporting/ProofObligations.py b/chc/reporting/ProofObligations.py index 05e86ec..1cb8570 100644 --- a/chc/reporting/ProofObligations.py +++ b/chc/reporting/ProofObligations.py @@ -32,6 +32,8 @@ from typing import ( Any, Callable, cast, Dict, List, Sequence, Set, Tuple, TYPE_CHECKING) +import chc.util.fileutil as UF + if TYPE_CHECKING: from chc.app.CApplication import CApplication from chc.app.CFile import CFile @@ -802,7 +804,6 @@ def tag_file_function_pos_tostring( for ff in sorted(fundict[f]): lines.append(" Function: " + ff) for po in sorted(fundict[f][ff], key=lambda po: po.line): - invd = po.cfun.invdictionary lines.append((" " * 6) + str(po)) if po.is_closed: lines.append((" " * 14) + str(po.explanation)) @@ -820,18 +821,22 @@ def tag_file_function_pos_tostring( lines.append((" " * 14) + str(msg)) lines.append(" ") keys = po.diagnostic.argument_indices - for k in keys: - invids = po.diagnostic.get_invariant_ids(k) - for id in invids: - inv = invd.get_invariant_fact(id) - if inv.is_nrv_fact: - inv = cast("CInvariantNRVFact", inv) - nrv = inv.non_relational_value - lines.append( - (" " * 14) - + str(k) - + ": " - + str(nrv)) + try: + invd = po.cfun.invdictionary + for k in keys: + invids = po.diagnostic.get_invariant_ids(k) + for id in invids: + inv = invd.get_invariant_fact(id) + if inv.is_nrv_fact: + inv = cast("CInvariantNRVFact", inv) + nrv = inv.non_relational_value + lines.append( + (" " * 14) + + str(k) + + ": " + + str(nrv)) + except UF.CHCError: + pass lines.append(" ") From 5d9f0f241842b3543267adf12d6de6072f6ddae1 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Mon, 8 Dec 2025 11:18:09 -0800 Subject: [PATCH 16/22] CMD: add investigate command for projects --- chc/cmdline/c_project/cprojectutil.py | 60 ++++++++++++++++++++++++++- chc/cmdline/chkc | 12 ++++++ 2 files changed, 71 insertions(+), 1 deletion(-) diff --git a/chc/cmdline/c_project/cprojectutil.py b/chc/cmdline/c_project/cprojectutil.py index 67879f0..e38e3fa 100644 --- a/chc/cmdline/c_project/cprojectutil.py +++ b/chc/cmdline/c_project/cprojectutil.py @@ -540,7 +540,7 @@ def cproject_report(args: argparse.Namespace) -> NoReturn: statsresult = UF.read_project_summary_results(targetpath, projectname) if statsresult is not None: print(RP.project_proofobligation_stats_dict_to_string(statsresult)) - if canalysis == "undefinedbehavior": + if canalysis == "undefined-behavior": exit(0) if not UF.has_analysisresults_path(targetpath, projectname): @@ -637,6 +637,64 @@ def callsite_str(instr: "CCallInstr") -> str: exit(0) +def cproject_investigate(args: argparse.Namespace) -> NoReturn: + + # arguments + tgtpath: str = args.tgtpath + projectname: str = args.projectname + predicates: Optional[List[str]] = args.predicates + + targetpath = os.path.abspath(tgtpath) + projectpath = targetpath + contractpath = os.path.join(targetpath, "chc_contracts") + + if not UF.has_analysisresults_path(targetpath, projectname): + print_error( + f"No analysis results found for {projectname} in {targetpath}") + exit(1) + + capp = CApplication( + projectpath, projectname, targetpath, contractpath) + + def pofilter(po: "CFunctionPO") -> bool: + if predicates is not None: + return po.predicate_name in predicates + else: + return True + + def header(s: str) -> str: + return (s + ":\n" + ("=" * 80)) + + lines: List[str] = [] + + for cfile in capp.cfiles: + openppos = cfile.get_open_ppos() + violations = cfile.get_ppos_violated() + delegated = cfile.get_ppos_delegated() + + if len(openppos) + len(violations) + len(delegated) > 0: + lines.append("=" * 80) + lines.append(cfile.name) + lines.append("=" * 80) + + if len(openppos) > 0: + lines.append(header("Open primary proof obligations obligations")) + lines.append(RP.tag_file_function_pos_tostring(openppos, pofilter=pofilter)) + + if len(violations) > 0: + lines.append(header("Primary proof obligations violated")) + lines.append(RP.tag_file_function_pos_tostring( + violations, pofilter=pofilter)) + + if len(delegated) > 0: + lines.append(header("Primary proof obligations delegated")) + lines.append(RP.tag_file_function_pos_tostring(delegated, pofilter=pofilter)) + + print("\n".join(lines)) + + exit(0) + + def cproject_count_stmts(args: argparse.Namespace) -> NoReturn: """CLI command to output size statistics for a c project.""" diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc index a21d562..5199eef 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -1621,6 +1621,18 @@ def parse() -> argparse.Namespace: help="show location invariants on the code") cprojectreportfile.set_defaults(func=P.cproject_report_file) + # --- investigate + cprojectinvestigate = cprojectparsers.add_parser("investigate") + cprojectinvestigate.add_argument( + "tgtpath", help="directory that contains the analysis results") + cprojectinvestigate.add_argument( + "projectname", help="name of the project") + cprojectinvestigate.add_argument( + "--predicates", + nargs="*", + help="names of predicates of interest, e.g., not-null (default: all") + cprojectinvestigate.set_defaults(func=P.cproject_investigate) + # --- count-statements cprojectcountstmts = cprojectparsers.add_parser("count-statements") cprojectcountstmts.add_argument( From 728c20d207eb18974196e5752f665242360449c3 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 18 Dec 2025 09:53:58 -0800 Subject: [PATCH 17/22] PROOF: change representation for rejection reason --- chc/app/CFunction.py | 3 +- chc/cmdline/AnalysisManager.py | 2 +- chc/cmdline/c_project/cprojectutil.py | 10 ++ chc/cmdline/chkc | 14 ++ chc/proof/CFunPODictionary.py | 13 +- chc/proof/CFunctionAnalysisDigest.py | 3 +- chc/proof/OutputParameterRejectionReason.py | 172 ++++++++++++++++++++ chc/proof/OutputParameterStatus.py | 9 +- chc/reporting/ProofObligations.py | 20 ++- 9 files changed, 230 insertions(+), 16 deletions(-) create mode 100644 chc/proof/OutputParameterRejectionReason.py diff --git a/chc/app/CFunction.py b/chc/app/CFunction.py index c4e1a93..1a49c6c 100644 --- a/chc/app/CFunction.py +++ b/chc/app/CFunction.py @@ -307,7 +307,8 @@ def analysis_digests(self) -> CFunctionAnalysisDigests: self.cfilename, self.name) if adnode is None: - print("DEBUG: No adg file found") + chklogger.logger.warning( + "No adg file encountered for function %s", self.name) adgnode = None # raise UF.CHCError(self.xmsg("adg file not found")) else: diff --git a/chc/cmdline/AnalysisManager.py b/chc/cmdline/AnalysisManager.py index 2b993ae..7c9e25f 100644 --- a/chc/cmdline/AnalysisManager.py +++ b/chc/cmdline/AnalysisManager.py @@ -282,7 +282,7 @@ def f(cfile: "CFile") -> None: def f(cfile: "CFile") -> None: self.create_file_primary_proofobligations( - cfile.cfilename, cfile.cfilepath) + cfile.cfilename, cfile.cfilepath, po_cmd=po_cmd) self.capp.iter_files(f) diff --git a/chc/cmdline/c_project/cprojectutil.py b/chc/cmdline/c_project/cprojectutil.py index e38e3fa..f6ccb09 100644 --- a/chc/cmdline/c_project/cprojectutil.py +++ b/chc/cmdline/c_project/cprojectutil.py @@ -533,10 +533,20 @@ def cproject_report(args: argparse.Namespace) -> NoReturn: projectname: str = args.projectname canalysis: str = args.analysis verbose: bool = args.verbose + loglevel: str = args.loglevel + logfilename: Optional[str] = args.logfilename + logfilemode: str = args.logfilemode targetpath = os.path.abspath(tgtpath) projectpath = targetpath + set_logging( + loglevel, + targetpath, + logfilename=logfilename, + mode=logfilemode, + msg="c-project report invoked") + statsresult = UF.read_project_summary_results(targetpath, projectname) if statsresult is not None: print(RP.project_proofobligation_stats_dict_to_string(statsresult)) diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc index 5199eef..95f0aa3 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -1592,6 +1592,20 @@ def parse() -> argparse.Namespace: cprojectreport.add_argument( "--verbose", "-v", action="store_true") + cprojectreport.add_argument( + "--loglevel", "-log", + choices=UL.LogLevel.options(), + default="NONE", + help="activate logging with given level (default to stderr)") + cprojectreport.add_argument( + "--logfilename", + help="name of file to write log messages") + cprojectreport.add_argument( + "--logfilemode", + choices=["a", "w"], + default="a", + help="file mode for log file: append (a, default), or write (w)") + cprojectreport.set_defaults(func=P.cproject_report) # --- report-file diff --git a/chc/proof/CFunPODictionary.py b/chc/proof/CFunPODictionary.py index 2fce50c..63ce515 100644 --- a/chc/proof/CFunPODictionary.py +++ b/chc/proof/CFunPODictionary.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny B. Sipma -# Copyright (c) 2023-2024 Aarno Labs LLC +# Copyright (c) 2023-2025 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 @@ -36,6 +36,7 @@ from typing import Callable, Dict, List, Mapping, TYPE_CHECKING from chc.proof.AssumptionType import AssumptionType +from chc.proof.OutputParameterRejectionReason import OutputParameterRejectionReason from chc.proof.OutputParameterStatus import OutputParameterStatus from chc.proof.CFunPODictionaryRecord import podregistry from chc.proof.PPOType import PPOType @@ -67,12 +68,15 @@ def __init__( cfun: "CFunction", xnode: ET.Element) -> None: self._cfun = cfun + self.output_parameter_rejection_reason_table = IndexedTable( + "output-parameter-rejection-reason-table") self.output_parameter_status_table = IndexedTable( "output-parameter-status-table") self.assumption_type_table = IndexedTable("assumption-table") self.ppo_type_table = IndexedTable("ppo-type-table") self.spo_type_table = IndexedTable("spo-type-table") self.tables = [ + self.output_parameter_rejection_reason_table, self.output_parameter_status_table, self.assumption_type_table, self.ppo_type_table, @@ -106,6 +110,13 @@ def interfacedictionary(self) -> "InterfaceDictionary": # ------------------------ Retrieve items from dictionary ---------------- + def get_output_parameter_rejection_reason( + self, ix: int) -> OutputParameterRejectionReason: + return podregistry.mk_instance( + self, + self.output_parameter_rejection_reason_table.retrieve(ix), + OutputParameterRejectionReason) + def get_output_parameter_status(self, ix: int) -> OutputParameterStatus: return podregistry.mk_instance( self, diff --git a/chc/proof/CFunctionAnalysisDigest.py b/chc/proof/CFunctionAnalysisDigest.py index 0a93824..0d67270 100644 --- a/chc/proof/CFunctionAnalysisDigest.py +++ b/chc/proof/CFunctionAnalysisDigest.py @@ -32,6 +32,7 @@ from chc.proof.CandidateOutputParameter import CandidateOutputParameter from chc.proof.OutputParameterCalleeCallsite import OutputParameterCalleeCallsite +from chc.util.loggingutil import chklogger if TYPE_CHECKING: from chc.app.CFile import CFile @@ -119,7 +120,7 @@ def digests(self) -> List[CFunctionAnalysisDigest]: self.cfun, xdigest) self._digests.append(digest) else: - print("DEBUG: xnode is none") + chklogger.logger.warning("Adg xnode is None") return self._digests def __str__(self) -> str: diff --git a/chc/proof/OutputParameterRejectionReason.py b/chc/proof/OutputParameterRejectionReason.py new file mode 100644 index 0000000..ac8d728 --- /dev/null +++ b/chc/proof/OutputParameterRejectionReason.py @@ -0,0 +1,172 @@ +# ------------------------------------------------------------------------------ +# CodeHawk C Analyzer +# Author: Henny Sipma +# ------------------------------------------------------------------------------ +# The MIT License (MIT) +# +# Copyright (c) 2025 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, TYPE_CHECKING + +from chc.proof.CFunPODictionaryRecord import CFunPODictionaryRecord, podregistry + + +from chc.util.IndexedTable import IndexedTableValue + + +if TYPE_CHECKING: + from chc.app.CCompInfo import CCompInfo + from chc.app.CDictionary import CDictionary + from chc.app.CTyp import CTyp + from chc.proof.CFunPODictionary import CFunPODictionary + + +class OutputParameterRejectionReason(CFunPODictionaryRecord): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + CFunPODictionaryRecord.__init__(self, pod, ixval) + + +@podregistry.register_tag("a", OutputParameterRejectionReason) +class OutputParameterRejectionReasonArrayStruct(OutputParameterRejectionReason): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterRejectionReason.__init__(self, pod, ixval) + + @property + def compinfo(self) -> "CCompInfo": + return self.cdecls.get_compinfo(self.args[0]) + + def __str__(self) -> str: + return "Struct with embedded array: " + str(self.compinfo) + + +@podregistry.register_tag("at", OutputParameterRejectionReason) +class OutputParameterRejectionReasonArrayType(OutputParameterRejectionReason): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterRejectionReason.__init__(self, pod, ixval) + + @property + def typ(self) -> "CTyp": + return self.cdictionary.get_typ(self.args[0]) + + def __str__(self) -> str: + return "rray type: " + str(self.typ) + + +@podregistry.register_tag("c", OutputParameterRejectionReason) +class OutputParameterRejectionReasonConstQualifier(OutputParameterRejectionReason): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterRejectionReason.__init__(self, pod, ixval) + + @property + def typ(self) -> "CTyp": + return self.cdictionary.get_typ(self.args[0]) + + def __str__(self) -> str: + return "Const qualifier: " + str(self.typ) + + +@podregistry.register_tag("o", OutputParameterRejectionReason) +class OutputParameterRejectionReasonOtherReason(OutputParameterRejectionReason): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterRejectionReason.__init__(self, pod, ixval) + + @property + def reason(self) -> str: + return self.cdictionary.get_string(self.args[0]) + + def __str__(self) -> str: + return "Other: " + str(self.reason) + + +@podregistry.register_tag("p", OutputParameterRejectionReason) +class OutputParameterRejectionReasonPointerPointer(OutputParameterRejectionReason): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterRejectionReason.__init__(self, pod, ixval) + + @property + def typ(self) -> "CTyp": + return self.cdictionary.get_typ(self.args[0]) + + def __str__(self) -> str: + return "Pointer to pointer: " + str(self.typ) + + +@podregistry.register_tag("r", OutputParameterRejectionReason) +class OutputParameterRejectionReasonParameterRead(OutputParameterRejectionReason): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterRejectionReason.__init__(self, pod, ixval) + + @property + def linenumber(self) -> int: + return self.args[0] + + def __str__(self) -> str: + return "Parameter is read at line " + str(self.linenumber) + + +@podregistry.register_tag("s", OutputParameterRejectionReason) +class OutputParameterRejectionReasonSystemStruct(OutputParameterRejectionReason): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterRejectionReason.__init__(self, pod, ixval) + + @property + def compinfo(self) -> "CCompInfo": + return self.cdecls.get_compinfo(self.args[0]) + + def __str__(self) -> str: + return "Target type is a system struct: " + str(self.compinfo) + + +@podregistry.register_tag("v", OutputParameterRejectionReason) +class OutputParameterRejectionReasonVoidPointer(OutputParameterRejectionReason): + + def __init__( + self, pod: "CFunPODictionary", ixval: IndexedTableValue + ) -> None: + OutputParameterRejectionReason.__init__(self, pod, ixval) + + def __str__(self) -> str: + return "Void pointer" diff --git a/chc/proof/OutputParameterStatus.py b/chc/proof/OutputParameterStatus.py index 5b189fc..1e09e12 100644 --- a/chc/proof/OutputParameterStatus.py +++ b/chc/proof/OutputParameterStatus.py @@ -36,6 +36,7 @@ if TYPE_CHECKING: from chc.app.CDictionary import CDictionary from chc.proof.CFunPODictionary import CFunPODictionary + from chc.proof.OutputParameterRejectionReason import OutputParameterRejectionReason class OutputParameterStatus(CFunPODictionaryRecord): @@ -103,11 +104,11 @@ def is_rejected(self) -> bool: return True @property - def reason(self) -> List[str]: - return [self.cdictionary.get_string(arg) for arg in self.args] + def reasons(self) -> List["OutputParameterRejectionReason"]: + return [self.pod.get_output_parameter_rejection_reason(arg) for arg in self.args] def __str__(self) -> str: - return "Rejected: " + "; ".join(self.reason) + return "Rejected: " + "; ".join(str(reason) for reason in self.reasons) @podregistry.register_tag("w", OutputParameterStatus) @@ -119,7 +120,7 @@ def __init__( OutputParameterStatus.__init__(self, pod, ixval) @property - def is_viable(self) -> bool: + def is_written(self) -> bool: return True def __str__(self) -> str: diff --git a/chc/reporting/ProofObligations.py b/chc/reporting/ProofObligations.py index 1cb8570..759ea8e 100644 --- a/chc/reporting/ProofObligations.py +++ b/chc/reporting/ProofObligations.py @@ -663,16 +663,20 @@ def project_proofobligation_stats_dict_to_string( pporesults = stats_dict["fileresults"]["ppos"] sporesults = stats_dict["fileresults"]["spos"] - rhlen = max([len(x) for x in pporesults]) - lines.append( - proofobligation_stats_tostring( - pporesults, sporesults, rhlen=rhlen, header1="c files")) + if len(pporesults) > 0: + rhlen = max([len(x) for x in pporesults]) + lines.append( + proofobligation_stats_tostring( + pporesults, sporesults, rhlen=rhlen, header1="c files")) - lines.append("\n\nProof Obligation Statistics") + lines.append("\n\nProof Obligation Statistics") - tagpporesults = stats_dict["tagresults"]["ppos"] - tagsporesults = stats_dict["tagresults"]["spos"] - lines.append(proofobligation_stats_tostring(tagpporesults, tagsporesults)) + tagpporesults = stats_dict["tagresults"]["ppos"] + tagsporesults = stats_dict["tagresults"]["spos"] + lines.append(proofobligation_stats_tostring(tagpporesults, tagsporesults)) + + else: + lines.append("Zero primary proof obligations") return "\n".join(lines) From c7c7f3619646ce992a4e424e8eceb57c15138feb Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 18 Dec 2025 10:44:54 -0800 Subject: [PATCH 18/22] CMD: add cmd to show cil-based source code for project file --- chc/cmdline/c_project/cprojectutil.py | 49 +++++++++++++++++++++++++++ chc/cmdline/chkc | 23 +++++++++++++ 2 files changed, 72 insertions(+) diff --git a/chc/cmdline/c_project/cprojectutil.py b/chc/cmdline/c_project/cprojectutil.py index f6ccb09..87503e3 100644 --- a/chc/cmdline/c_project/cprojectutil.py +++ b/chc/cmdline/c_project/cprojectutil.py @@ -420,6 +420,55 @@ def is_included(path: Optional[str]) -> bool: exit(0) +def cproject_cil_source(args: argparse.Namespace) -> NoReturn: + """Outputs a textual representation of the CIL AST.""" + + #arguments + tgtpath: str = args.tgtpath + projectname: str = args.projectname + filename: str = args.filename + loglevel: str = args.loglevel + logfilename: Optional[str] = args.logfilename + logfilemode: str = args.logfilemode + + targetpath = os.path.abspath(tgtpath) + projectpath = targetpath + cfilename_c = os.path.basename(filename) + cfilename = cfilename_c[:-2] + cfilepath = os.path.dirname(filename) + + set_logging( + loglevel, + targetpath, + logfilename=logfilename, + mode=logfilemode, + msg="Command cfile mk-headerfile was invoked") + + if not UF.has_analysisresults_path(targetpath, projectname): + print_error( + f"No analysis results found for {projectname} in {targetpath}") + exit(1) + + contractpath = os.path.join(targetpath, "chc_contracts") + capp = CApplication( + projectpath, projectname, targetpath, contractpath) + + if capp.has_file(filename[:-2]): + cfile = capp.get_file(filename[:-2]) + else: + print_error(f"File {filename} not found") + exit(1) + + fcilsource = cfile.cil_source() + + outputfilename = cfile.cfilename + ".cil.c" + with open(outputfilename, "w") as fp: + fp.write(fcilsource) + print("Cil source code written to " + outputfilename) + + exit(0) + + def cproject_analyze_project(args: argparse.Namespace) -> NoReturn: # arguments diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc index 95f0aa3..44147bf 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -1527,6 +1527,29 @@ def parse() -> argparse.Namespace: help="file mode for log file: append (a, default), or write (w)") cprojectmkheader.set_defaults(func=P.cproject_mk_headerfile) + # --- cil-source + cprojectcilsource = cprojectparsers.add_parser("cil-source") + cprojectcilsource.add_argument( + "tgtpath", help="directory that contains the analysis results") + cprojectcilsource.add_argument( + "projectname", help="name of the project") + cprojectcilsource.add_argument( + "filename", help="filename with relative path wrt the project") + cprojectcilsource.add_argument( + "--loglevel", "-log", + choices=UL.LogLevel.options(), + default="NONE", + help="activate logging with given level (default to stderr)") + cprojectcilsource.add_argument( + "--logfilename", + help="name of file to write log messages") + cprojectcilsource.add_argument( + "--logfilemode", + choices=["a", "w"], + default="a", + help="file mode for log file: append (a, default), or write (w)") + cprojectcilsource.set_defaults(func=P.cproject_cil_source) + # --- analyze cprojectanalyze = cprojectparsers.add_parser("analyze") cprojectanalyze.add_argument( From 47a2aad072b3c20fa95a44ae9f1e217c7bfa7bc8 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 1 Feb 2026 18:23:14 -0800 Subject: [PATCH 19/22] APP: add offset-info --- chc/app/CInitInfo.py | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/chc/app/CInitInfo.py b/chc/app/CInitInfo.py index c97141b..ff8a58f 100644 --- a/chc/app/CInitInfo.py +++ b/chc/app/CInitInfo.py @@ -57,6 +57,10 @@ def is_single(self) -> bool: def is_compound(self) -> bool: return False + @property + def is_offset(self) -> bool: + return False + def accept(self, visitor: "CVisitor") -> None: raise UF.CHCError("visitor not yet implemented for " + str(self)) @@ -98,6 +102,10 @@ def __init__(self, decls: "CDeclarations", ixval: IT.IndexedTableValue): def typ(self) -> "CTyp": return self.dictionary.get_typ(self.args[0]) + @property + def is_compound(self) -> bool: + return True + @property def offset_initializers(self) -> List["COffsetInitInfo"]: return [self.decls.get_offset_init(x) for x in self.args[1:]] @@ -117,7 +125,7 @@ def __str__(self) -> str: return "\n".join([str(x) for x in self.offset_initializers]) -class COffsetInitInfo(CDeclarationsRecord): +class COffsetInitInfo(CInitInfo): """Component of a compound initializer. - args[0]: index of offset expression in cdictionary @@ -131,6 +139,10 @@ def __init__(self, decls: "CDeclarations", ixval: IT.IndexedTableValue): def offset(self) -> "COffset": return self.dictionary.get_offset(self.args[0]) + @property + def is_offset(self) -> bool: + return True + @property def initializer(self) -> CInitInfo: return self.decls.get_initinfo(self.args[1]) From 1c41aa95937038f559aca0ceb958be27cbc678cb Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 1 Feb 2026 18:23:59 -0800 Subject: [PATCH 20/22] APP: add offset-info --- chc/app/CGlobalDeclarations.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/chc/app/CGlobalDeclarations.py b/chc/app/CGlobalDeclarations.py index ba7b718..a92fe8d 100644 --- a/chc/app/CGlobalDeclarations.py +++ b/chc/app/CGlobalDeclarations.py @@ -594,7 +594,7 @@ def index_init(self, init: CInitInfo, fid: int = -1) -> int: args = [self.dictionary.index_exp(init.exp, fid=fid)] return self.mk_single_init_index(init.tags, args) - if init.is_compound: + elif init.is_compound: init = cast("CCompoundInitInfo", init) gtype = self.dictionary.index_typ(init.typ) oinits: List[int] = [ @@ -604,9 +604,9 @@ def index_init(self, init: CInitInfo, fid: int = -1) -> int: return self.mk_compound_init_index(init.tags, args) else: - # raise Exception("InitInfo not recognized: " + str(init)) - print("InitInfo not recognized: " + str(init)) - return -1 + init = cast("COffsetInitInfo", init) + args = [self.dictionary.index_offset(init.offset, fid=fid)] + return self.mk_offset_init_index(init.tags, args) def index_offset_init(self, oinit: COffsetInitInfo, fid: int = -1) -> int: args: List[int] = [ From 31ebfdff74093a8bf19640b24e914256c5a1f492 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 1 Feb 2026 18:28:12 -0800 Subject: [PATCH 21/22] CMD:top-level integration of output-parameter results --- chc/app/CApplication.py | 29 ++++++ chc/app/CFunction.py | 1 + chc/cmdline/AnalysisManager.py | 12 ++- chc/cmdline/ParseManager.py | 6 +- chc/cmdline/c_project/cprojectutil.py | 127 +++++++++++++++++++------- chc/cmdline/chkc | 4 + 6 files changed, 144 insertions(+), 35 deletions(-) diff --git a/chc/app/CApplication.py b/chc/app/CApplication.py index 6163c29..71d030f 100644 --- a/chc/app/CApplication.py +++ b/chc/app/CApplication.py @@ -54,6 +54,7 @@ if TYPE_CHECKING: from chc.app.CFunction import CFunction from chc.app.CInstr import CCallInstr + from chc.proof.CandidateOutputParameter import CandidateOutputParameter from chc.proof.CFunctionCallsiteSPOs import CFunctionCallsiteSPOs from chc.proof.CFunctionPO import CFunctionPO @@ -315,6 +316,34 @@ def g(fi: CFile) -> None: self.iter_files_parallel(g, maxprocesses) + def check_digests(self) -> bool: + for cfile in list(self.cfiles): + for cfun in cfile.get_functions(): + if cfun.analysis_digests.is_active: + return True + return False + + def outputparameters(self) -> Dict[str, List["CandidateOutputParameter"]]: + result: Dict[str, List["CandidateOutputParameter"]] = {} + for cfile in list(self.cfiles): + for cfun in cfile.get_functions(): + result[cfun.name] = cfun.analysis_digests.outputparameters() + return result + + def viable_outputparameters(self) -> Dict[str, List["CandidateOutputParameter"]]: + result: Dict[str, List["CandidateOutputParameter"]] = {} + for cfile in list(self.cfiles): + for cfun in cfile.get_functions(): + result[cfun.name] = cfun.analysis_digests.viable_outputparameters() + return result + + def maybe_outputparameters(self) -> Dict[str, List["CandidateOutputParameter"]]: + result: Dict[str, List["CandidateOutputParameter"]] = {} + for cfile in list(self.cfiles): + for cfun in cfile.get_functions(): + result[cfun.name] = cfun.analysis_digests.maybe_outputparameters() + return result + def resolve_vid_function( self, filevar: FileVarReference) -> Optional["CFunction"]: """Returns the function def for the local file-index fid and vid. diff --git a/chc/app/CFunction.py b/chc/app/CFunction.py index 1a49c6c..7eba674 100644 --- a/chc/app/CFunction.py +++ b/chc/app/CFunction.py @@ -386,6 +386,7 @@ def reinitialize_tables(self) -> None: self._api = None self._podictionary = None self._vardictionary = None + self._analysis_digests = None self._proofs = None def get_formal_vid(self, name: str) -> int: diff --git a/chc/cmdline/AnalysisManager.py b/chc/cmdline/AnalysisManager.py index 7c9e25f..c681259 100644 --- a/chc/cmdline/AnalysisManager.py +++ b/chc/cmdline/AnalysisManager.py @@ -32,6 +32,7 @@ import subprocess import os import shutil +import sys from typing import List, Optional, Tuple, TYPE_CHECKING @@ -45,6 +46,10 @@ from chc.app.CFile import CFile +def print_status(m: str) -> None: + sys.stderr.write(m + "\n") + + class AnalysisManager: """Provide the interface to the codehawk (ocaml) analyzer.""" @@ -178,7 +183,7 @@ def reset_tables(self, cfile: "CFile") -> None: def _execute_cmd(self, CMD: List[str]) -> None: try: - print(CMD) + print_status(", ".join(CMD)) result = subprocess.check_output(CMD) print(result.decode("utf-8")) except subprocess.CalledProcessError as args: @@ -228,7 +233,7 @@ def create_file_primary_proofobligations( chklogger.logger.info( "Ocaml analyzer is called with %s", str(cmd)) if self.verbose: - print(str(cmd)) + print_status(str(cmd)) result = subprocess.call( cmd, cwd=self.targetpath, stderr=subprocess.STDOUT) print("\nResult: " + str(result)) @@ -342,9 +347,10 @@ def generate_and_check_file( result = subprocess.call( cmd, cwd=self.targetpath, - # stdout=open(os.devnull, "w"), + stdout=open(os.devnull, "w"), stderr=subprocess.STDOUT, ) + print("\nResult: " + str(result)) if result != 0: chklogger.logger.error( "Error in generating invariants for %s", cfilename) diff --git a/chc/cmdline/ParseManager.py b/chc/cmdline/ParseManager.py index b082db3..80e3c5b 100644 --- a/chc/cmdline/ParseManager.py +++ b/chc/cmdline/ParseManager.py @@ -419,9 +419,11 @@ def preprocess( def parse_with_ccommands( self, compilecommands: List[Dict[str, Any]], - copyfiles: bool = True) -> None: + copyfiles: bool = True) -> int: """Preprocess and call C parser to produce xml semantics files.""" + exitcode = 0 + cfiles: Dict[str, int] = {} targetfiles = TargetFiles() for c in compilecommands: @@ -459,6 +461,7 @@ def parse_with_ccommands( print("\n" + ("*" * 80)) print("Parsing error in " + cfilename) print("*" * 80) + exitcode = 1 break if self.verbose: @@ -481,6 +484,7 @@ def parse_with_ccommands( ) os.chdir(self.projectpath) shutil.copy("compile_commands.json", self.savedsourcepath) + return exitcode def parse_ifiles(self, copyfiles: bool = True) -> None: """Run the CodeHawk C parser on all .i files in the directory.""" diff --git a/chc/cmdline/c_project/cprojectutil.py b/chc/cmdline/c_project/cprojectutil.py index 87503e3..b84beab 100644 --- a/chc/cmdline/c_project/cprojectutil.py +++ b/chc/cmdline/c_project/cprojectutil.py @@ -72,6 +72,10 @@ def print_error(m: str) -> None: sys.stderr.write(("*" * 80) + "\n") +def print_status_update(m: str) -> None: + sys.stderr.write("[chkc] " + m + "\n") + + def set_logging( level: str, path: str, @@ -158,13 +162,18 @@ def cproject_parse_project(args: argparse.Namespace) -> NoReturn: exit(1) parsemanager = ParseManager( - projectpath, projectname, targetpath, keep_system_includes=keep_system_includes) + projectpath, + projectname, + targetpath, + keep_system_includes=keep_system_includes) parsemanager.remove_semantics() parsemanager.initialize_paths() - parsemanager.parse_with_ccommands(compilecommands, copyfiles=True) - parsemanager.save_semantics() + exitcode = parsemanager.parse_with_ccommands(compilecommands, copyfiles=True) + if exitcode == 0: + parsemanager.save_semantics() - exit(0) + print_status_update("exitcode: " + str(exitcode)) + exit(exitcode) def cproject_scan_op(args: argparse.Namespace) -> NoReturn: @@ -423,7 +432,8 @@ def is_included(path: Optional[str]) -> bool: def cproject_cil_source(args: argparse.Namespace) -> NoReturn: """Outputs a textual representation of the CIL AST.""" - #arguments + # arguments + tgtpath: str = args.tgtpath projectname: str = args.projectname filename: str = args.filename @@ -479,6 +489,7 @@ def cproject_analyze_project(args: argparse.Namespace) -> NoReturn: analysisdomains: str = args.analysis_domains collectdiagnostics: bool = args.collect_diagnostics maxprocesses: int = args.maxprocesses + verbose: bool = args.verbose loglevel: str = args.loglevel logfilename: Optional[str] = args.logfilename logfilemode: str = args.logfilemode @@ -538,10 +549,18 @@ def save_xrefs(f: "CFile") -> None: am = AnalysisManager( capp, - verbose=True, + verbose=verbose, collectdiagnostics=collectdiagnostics, keep_system_includes=keep_system_includes) + exitcode = 0 + + def check_continuation() -> int: + if analysis == "outputparameters": + if not capp.check_digests(): + return 166 + return 0 + with timing("analysis"): try: @@ -553,15 +572,46 @@ def save_xrefs(f: "CFile") -> None: print(str(e.wrap())) exit(1) - for i in range(1): - am.generate_and_check_app(analysisdomains, processes=maxprocesses) - capp.reinitialize_tables() - capp.update_spos() - - for i in range(5): - capp.update_spos() - am.generate_and_check_app(analysisdomains, processes=maxprocesses) - capp.reinitialize_tables() + exitcode = check_continuation() + + if exitcode == 0: + for i in range(1): + am.generate_and_check_app(analysisdomains, processes=maxprocesses) + capp.reinitialize_tables() + capp.update_spos() + + exitcode = check_continuation() + + if exitcode == 0: + for i in range(5): + capp.update_spos() + am.generate_and_check_app(analysisdomains, processes=maxprocesses) + capp.reinitialize_tables() + + exitcode = check_continuation() + if exitcode > 0: + break + + if analysis == "outputparameters": + presult = capp.outputparameters() + vresult = capp.viable_outputparameters() + mresult = capp.maybe_outputparameters() + viable = sum(len(f) for f in vresult.values()) + maybe = sum(len(f) for f in mresult.values()) + opp = sum(len(f) for f in presult.values()) + print("Functions analyzed : " + str(len(vresult))) + print("Outputparameters : " + str(opp)) + print("Maybe outputparameters : " + str(maybe)) + print("Viable outputparameters: " + str(viable)) + for (fname, pl) in vresult.items(): + if len(pl) > 0: + print(" function: " + fname) + for p in pl: + print(" " + str(p.parameter)) + if viable > 0: + exitcode = 0 + elif maybe > 0: + exitcode = 167 timestamp = os.stat(UF.get_cchpath(targetpath, projectname)).st_ctime @@ -571,7 +621,8 @@ def save_xrefs(f: "CFile") -> None: UF.save_project_summary_results(targetpath, projectname, result) UF.save_project_summary_results_as_xml(targetpath, projectname, result) - exit(0) + print_status_update("exitcode: " + str(exitcode)) + exit(exitcode) def cproject_report(args: argparse.Namespace) -> NoReturn: @@ -596,28 +647,33 @@ def cproject_report(args: argparse.Namespace) -> NoReturn: mode=logfilemode, msg="c-project report invoked") - statsresult = UF.read_project_summary_results(targetpath, projectname) - if statsresult is not None: - print(RP.project_proofobligation_stats_dict_to_string(statsresult)) - if canalysis == "undefined-behavior": + if canalysis == "undefined-behavior": + statsresult = UF.read_project_summary_results(targetpath, projectname) + if statsresult is not None: + print(RP.project_proofobligation_stats_dict_to_string(statsresult)) exit(0) - if not UF.has_analysisresults_path(targetpath, projectname): - print_error( - f"No analysis results found for {projectname} in {targetpath}") - exit(1) + if not UF.has_analysisresults_path(targetpath, projectname): + print_error( + f"No analysis results found for {projectname} in {targetpath}") + exit(1) + + contractpath = os.path.join(targetpath, "chc_contracts") + capp = CApplication( + projectpath, projectname, targetpath, contractpath) + + timestamp = os.stat(UF.get_cchpath(targetpath, projectname)).st_ctime + fresult = RP.project_proofobligation_stats_to_dict(capp) + fresult["timestamp"] = timestamp + fresult["project"] = projectpath + UF.save_project_summary_results(targetpath, projectname, fresult) + UF.save_project_summary_results_as_xml(targetpath, projectname, fresult) + exit(0) contractpath = os.path.join(targetpath, "chc_contracts") capp = CApplication( projectpath, projectname, targetpath, contractpath) - timestamp = os.stat(UF.get_cchpath(targetpath, projectname)).st_ctime - fresult = RP.project_proofobligation_stats_to_dict(capp) - fresult["timestamp"] = timestamp - fresult["project"] = projectpath - UF.save_project_summary_results(targetpath, projectname, fresult) - UF.save_project_summary_results_as_xml(targetpath, projectname, fresult) - statsresult = UF.read_project_summary_results(targetpath, projectname) if statsresult is not None: print(RP.project_proofobligation_stats_dict_to_string(statsresult)) @@ -627,9 +683,18 @@ def cproject_report(args: argparse.Namespace) -> NoReturn: if canalysis == "outputparameters": + print("\n\nOutput-parameter analysis results") for cfile in capp.files.values(): print("\nFile: " + cfile.name) for cfun in cfile.functions.values(): + ''' + if len(cfun.analysis_digests.digests) == 0: + print( + "\nFunction: " + + cfun.name + + ": No candidate output parameters") + else: + ''' print("\nFunction: " + cfun.name) print(str(cfun.analysis_digests)) diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc index 44147bf..d47d2d2 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -1560,6 +1560,10 @@ def parse() -> argparse.Namespace: "--keep-system-includes", action="store_true", help="don't filter out functions from files with absolute filenames") + cprojectanalyze.add_argument( + "--verbose", "-v", + action="store_true", + help="print analyzer status updates of invariant generation process") cprojectanalyze.add_argument( "--analysis", default="undefined-behavior", From 53331ef1c7d9e6862b27298ea941627bda839569 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 1 Feb 2026 18:29:00 -0800 Subject: [PATCH 22/22] PROOF:supply results for integration of output-parameter analysis --- chc/proof/CFunctionAnalysisDigest.py | 108 ++++++++++++++++++-- chc/proof/CandidateOutputParameter.py | 39 ++++++- chc/proof/OutputParameterCalleeCallsite.py | 89 +++++++++++++++- chc/proof/OutputParameterRejectionReason.py | 2 +- chc/proof/OutputParameterStatus.py | 10 +- 5 files changed, 236 insertions(+), 12 deletions(-) diff --git a/chc/proof/CFunctionAnalysisDigest.py b/chc/proof/CFunctionAnalysisDigest.py index 0d67270..a10b28f 100644 --- a/chc/proof/CFunctionAnalysisDigest.py +++ b/chc/proof/CFunctionAnalysisDigest.py @@ -27,7 +27,7 @@ import xml.etree.ElementTree as ET -from typing import List, Optional, TYPE_CHECKING +from typing import cast, List, Optional, TYPE_CHECKING from chc.proof.CandidateOutputParameter import CandidateOutputParameter from chc.proof.OutputParameterCalleeCallsite import OutputParameterCalleeCallsite @@ -35,11 +35,13 @@ from chc.util.loggingutil import chklogger if TYPE_CHECKING: + from chc.app.CApplication import CApplication from chc.app.CFile import CFile from chc.app.CFileDeclarations import CFileDeclarations from chc.app.CFunction import CFunction from chc.app.CVarInfo import CVarInfo from chc.proof.CFunPODictionary import CFunPODictionary + from chc.proof.OutputParameterStatus import OutputParameterStatusRejected class CFunctionAnalysisDigest: @@ -56,6 +58,23 @@ def cfun(self) -> "CFunction": def cfile(self) -> "CFile": return self.cfun.cfile + @property + def is_active(self) -> bool: + return True + + @property + def capp(self) -> "CApplication": + return self.cfile.capp + + def viable_parameters(self) -> List[CandidateOutputParameter]: + return [] + + def outputparameters(self) -> List[CandidateOutputParameter]: + return [] + + def maybe_parameters(self) -> List[CandidateOutputParameter]: + return [] + class CFunctionOutputParameterAnalysisDigest(CFunctionAnalysisDigest): @@ -63,6 +82,7 @@ def __init__(self, cfun: "CFunction", xnode: ET.Element) -> None: CFunctionAnalysisDigest.__init__(self, cfun, xnode) self._candidate_parameters: Optional[List[CandidateOutputParameter]] = None self._callee_callsites: Optional[List[OutputParameterCalleeCallsite]] = None + self._caller_callsites: Optional[List[OutputParameterCalleeCallsite]] = None @property def parameters(self) -> List[CandidateOutputParameter]: @@ -75,6 +95,9 @@ def parameters(self) -> List[CandidateOutputParameter]: self._candidate_parameters.append(cparam) return self._candidate_parameters + def has_parameters(self) -> bool: + return len(self.parameters) > 0 + @property def callee_callsites(self) -> List[OutputParameterCalleeCallsite]: if self._callee_callsites is None: @@ -86,14 +109,63 @@ def callee_callsites(self) -> List[OutputParameterCalleeCallsite]: self._callee_callsites.append(ccsite) return self._callee_callsites + @property + def caller_callsites(self) -> List[OutputParameterCalleeCallsite]: + if self._caller_callsites is None: + self._caller_callsites = [] + callinstrs = self.capp.get_callinstrs() + for callinstr in callinstrs: + if str(callinstr.callee) == self.cfun.name: + caller = callinstr.cfun + cfunadgs = caller.analysis_digests + if len(cfunadgs.digests) == 1: + cfunadg = cfunadgs.digests[0] + cfunadg = cast( + "CFunctionOutputParameterAnalysisDigest", cfunadg) + callsites = cfunadg.callee_callsites + callsites = [ + callsite for callsite in callsites + if str(callsite.callee) == self.cfun.name] + self._caller_callsites = callsites + return self._caller_callsites + + @property + def is_active(self) -> bool: + if self.has_parameters(): + if all(p.status.is_rejected for p in self.parameters): + return False + else: + return True + else: + return False + + def outputparameters(self) -> List[CandidateOutputParameter]: + return self.parameters + + def viable_parameters(self) -> List[CandidateOutputParameter]: + return [p for p in self.parameters if p.is_viable()] + + def maybe_parameters(self) -> List[CandidateOutputParameter]: + return [p for p in self.parameters if not (p.status.is_rejected or p.is_viable())] + def __str__(self) -> str: lines: List[str] = [] for p in self.parameters: - lines.append(str(p)) - if len(self.callee_callsites) > 0: - lines.append("\nCallee-callsites:") - for ccs in self.callee_callsites: - lines.append(" " + str(ccs)) + if p.status.is_rejected: + pstatus = cast("OutputParameterStatusRejected", p.status) + lines.append( + " X " + str(p.parameter_index) + " " + str(p.parameter)) + lines.append( + "Reasons: " + "\n".join(str(r) for r in pstatus.reasons)) + elif p.is_viable(): + lines.append(" v " + str(p.parameter_index) + " " + str(p)) + else: + lines.append(" ? " + str(p.parameter_index) + " " + str(p)) + if any(p.is_viable() for p in self.parameters): + if len(self.caller_callsites) > 0: + lines.append("\nCaller-callsites:") + for ccs in self.caller_callsites: + lines.append(" " + str(ccs)) return "\n".join(lines) @@ -123,6 +195,30 @@ def digests(self) -> List[CFunctionAnalysisDigest]: chklogger.logger.warning("Adg xnode is None") return self._digests + def outputparameters(self) -> List[CandidateOutputParameter]: + result: List[CandidateOutputParameter] = [] + for d in self.digests: + result.extend(d.outputparameters()) + return result + + def viable_outputparameters(self) -> List[CandidateOutputParameter]: + result: List[CandidateOutputParameter] = [] + for d in self.digests: + result.extend(d.viable_parameters()) + return result + + def maybe_outputparameters(self) -> List[CandidateOutputParameter]: + result: List[CandidateOutputParameter] = [] + for d in self.digests: + result.extend(d.maybe_parameters()) + return result + + @property + def is_active(self) -> bool: + if len(self.digests) == 1: + return self.digests[0].is_active + return False + def __str__(self) -> str: lines: List[str] = [] for digest in self.digests: diff --git a/chc/proof/CandidateOutputParameter.py b/chc/proof/CandidateOutputParameter.py index 04764a7..96ea9ec 100644 --- a/chc/proof/CandidateOutputParameter.py +++ b/chc/proof/CandidateOutputParameter.py @@ -38,6 +38,9 @@ from chc.proof.CFunPODictionary import CFunPODictionary from chc.proof.CFunctionAnalysisDigest import ( CFunctionOutputParameterAnalysisDigest) + from chc.proof.OutputParameterCalleeCallsite import ( + OutputParameterCalleeCallsiteArg, + OutputParameterCalleeCallsite) from chc.proof.OutputParameterStatus import OutputParameterStatus @@ -75,6 +78,9 @@ def location(self) -> "CLocation": def status(self) -> "OutputParameterStatus": return self.podictionary.read_xml_output_parameter_status(self.xnode) + def is_viable(self) -> bool: + return self.status.is_written or self.status.is_unaltered + def __str__(self) -> str: return str(self.location.line) + ": " + str(self.status) @@ -87,6 +93,7 @@ def __init__( self._adg = adg self.xnode = xnode # param node self._returnsites: Optional[List[COpParamReturnsite]] = None + self._caller_callsite_args: Optional[List["OutputParameterCalleeCallsiteArg"]] = None # self._calldeps: Optional[List[CopParamCallDependency]] = None @property @@ -113,6 +120,11 @@ def fdecls(self) -> "CFileDeclarations": def parameter(self) -> "CVarInfo": return self.fdecls.read_xml_varinfo(self.xnode) + @property + def parameter_index(self) -> int: + """1-based index.""" + return int(self.xnode.get("paramindex", -1)) + @property def status(self) -> "OutputParameterStatus": return self.podictionary.read_xml_output_parameter_status(self.xnode) @@ -128,11 +140,34 @@ def returnsites(self) -> List[COpParamReturnsite]: self._returnsites.append(returnsite) return self._returnsites + @property + def caller_callsite_args(self) -> List["OutputParameterCalleeCallsiteArg"]: + if self._caller_callsite_args is None: + self._caller_callsite_args = [] + callsites = self.adg.caller_callsites + for callsite in callsites: + for callarg in callsite.callargs: + if callarg.arg_index == self.parameter_index: + self._caller_callsite_args.append(callarg) + return self._caller_callsite_args + + def is_viable(self) -> bool: + if self.status.is_rejected: + return False + returns_viable = ( + all(returnsite.is_viable() for returnsite in self.returnsites)) + callers_viable = ( + all(callarg.status.is_viable for callarg in self.caller_callsite_args)) + return returns_viable and callers_viable + def __str__(self) -> str: lines: List[str] = [] lines.append(str(self.parameter) + ": " + str(self.status)) if not self.status.is_rejected: - lines.append("Return sites") + lines.append(" Return sites") for returnsite in self.returnsites: - lines.append(" " + str(returnsite)) + lines.append(" " + str(returnsite)) + lines.append(" Call arguments") + for callsite_arg in self.caller_callsite_args: + lines.append(" " + str(callsite_arg)) return "\n".join(lines) diff --git a/chc/proof/OutputParameterCalleeCallsite.py b/chc/proof/OutputParameterCalleeCallsite.py index 80c2175..3c45ffa 100644 --- a/chc/proof/OutputParameterCalleeCallsite.py +++ b/chc/proof/OutputParameterCalleeCallsite.py @@ -30,6 +30,8 @@ from typing import List, Optional, TYPE_CHECKING if TYPE_CHECKING: + from chc.app.CContext import ProgramContext + from chc.app.CContextDictionary import CContextDictionary from chc.app.CExp import CExp from chc.app.CFile import CFile from chc.app.CFileDictionary import CFileDictionary @@ -43,6 +45,74 @@ from chc.proof.OutputParameterStatus import OutputParameterStatus +class OutputParameterCalleeCallsiteArg: + + def __init__( + self, opcallsite: "OutputParameterCalleeCallsite", xnode: ET.Element + ) -> None: + self._opcallsite = opcallsite + self.xnode = xnode + + @property + def opcallsite(self) -> "OutputParameterCalleeCallsite": + return self._opcallsite + + @property + def adg(self) -> "CFunctionOutputParameterAnalysisDigest": + return self.opcallsite.adg + + @property + def cfun(self) -> "CFunction": + return self.adg.cfun + + @property + def cfile(self) -> "CFile": + return self.adg.cfile + + @property + def cdictionary(self) -> "CFileDictionary": + return self.cfile.dictionary + + @property + def podictionary(self) -> "CFunPODictionary": + return self.cfun.podictionary + + @property + def contextdictionary(self) -> "CContextDictionary": + return self.cfile.contextdictionary + + @property + def fdecls(self) -> "CFileDeclarations": + return self.cfile.declarations + + @property + def status(self) -> "OutputParameterStatus": + return self.podictionary.read_xml_output_parameter_status(self.xnode) + + @property + def argument(self) -> "CExp": + return self.cdictionary.read_xml_exp(self.xnode) + + @property + def context(self) -> "ProgramContext": + return self.contextdictionary.read_xml_context(self.xnode) + + @property + def arg_index(self) -> int: + expctxt = self.context.exp_context + lastnode = expctxt.nodes[-1] + if str(lastnode).startswith("arg:"): + index = int(str(lastnode)[4:]) + return index + else: + return -1 + + def __str__(self) -> str: + return ( + str(self.status) + + " " + str(self.argument) + " (argindex: " + str(self.arg_index)) + + class OutputParameterCalleeCallsite: def __init__( @@ -50,6 +120,7 @@ def __init__( ) -> None: self._adg = adg self.xnode = xnode + self._callargs: Optional[List[OutputParameterCalleeCallsiteArg]] = None @property def adg(self) -> "CFunctionOutputParameterAnalysisDigest": @@ -75,6 +146,17 @@ def podictionary(self) -> "CFunPODictionary": def fdecls(self) -> "CFileDeclarations": return self.cfile.declarations + @property + def callargs(self) -> List[OutputParameterCalleeCallsiteArg]: + if self._callargs is None: + self._callargs = [] + xcallargs = self.xnode.find("callee-callsite-args") + if xcallargs is not None: + for xcallarg in xcallargs.findall("callarg"): + callarg = OutputParameterCalleeCallsiteArg(self, xcallarg) + self._callargs.append(callarg) + return self._callargs + @property def status(self) -> "OutputParameterStatus": return self.podictionary.read_xml_output_parameter_status(self.xnode) @@ -88,9 +170,12 @@ def callee(self) -> "CExp": return self.cdictionary.read_xml_exp(self.xnode) def __str__(self) -> str: - return ( + lines: List[str] = [] + lines.append( str(self.location.line) + ": " - + str(self.status) + "; callee: " + str(self.callee)) + for callarg in self.callargs: + lines.append(" " + str(callarg)) + return "\n".join(lines) diff --git a/chc/proof/OutputParameterRejectionReason.py b/chc/proof/OutputParameterRejectionReason.py index ac8d728..637ab43 100644 --- a/chc/proof/OutputParameterRejectionReason.py +++ b/chc/proof/OutputParameterRejectionReason.py @@ -77,7 +77,7 @@ def typ(self) -> "CTyp": return self.cdictionary.get_typ(self.args[0]) def __str__(self) -> str: - return "rray type: " + str(self.typ) + return "array type: " + str(self.typ) @podregistry.register_tag("c", OutputParameterRejectionReason) diff --git a/chc/proof/OutputParameterStatus.py b/chc/proof/OutputParameterStatus.py index 1e09e12..3d840e4 100644 --- a/chc/proof/OutputParameterStatus.py +++ b/chc/proof/OutputParameterStatus.py @@ -54,6 +54,14 @@ def is_unknown(self) -> bool: def is_rejected(self) -> bool: return False + @property + def is_written(self) -> bool: + return False + + @property + def is_unaltered(self) -> bool: + return False + @property def is_viable(self) -> bool: return False @@ -136,7 +144,7 @@ def __init__( OutputParameterStatus.__init__(self, pod, ixval) @property - def is_viable(self) -> bool: + def is_unaltered(self) -> bool: return True def __str__(self) -> str: