From c92168b497ebd4aa951475f0e75a2d12632af9e2 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 4 Dec 2025 16:49:02 -0800 Subject: [PATCH 1/2] CMD: add query facility for invariants --- chc/app/CContext.py | 10 ++++- chc/app/CFile.py | 25 +++++++----- chc/app/CHVersion.py | 2 +- chc/cmdline/c_file/cfileutil.py | 59 ++++++++++++++++++++++++++- chc/cmdline/c_project/cprojectutil.py | 59 +++++++++++++++++++++++++++ chc/cmdline/chkc | 43 +++++++++++++++++++ chc/invariants/CInvariantFact.py | 8 ++++ chc/invariants/CXVariable.py | 7 ++++ chc/util/fileutil.py | 10 +++++ 9 files changed, 209 insertions(+), 14 deletions(-) diff --git a/chc/app/CContext.py b/chc/app/CContext.py index aab2f65..8f26e8d 100644 --- a/chc/app/CContext.py +++ b/chc/app/CContext.py @@ -31,7 +31,7 @@ """ -from typing import List, TYPE_CHECKING +from typing import Any, cast, List, TYPE_CHECKING import chc.util.fileutil as UF from chc.util.IndexedTable import IndexedTableValue @@ -163,5 +163,13 @@ def cfg_context(self) -> CfgContext: def exp_context(self) -> ExpContext: return self.cxd.get_exp_context(self.args[1]) + def __eq__(self, other: Any) -> bool: + if not isinstance(other, ProgramContext): + return NotImplemented + return self.index == cast("ProgramContext", other).index + + def __hash__(self) -> int: + return self.index + def __str__(self) -> str: return "(" + str(self.cfg_context) + "," + str(self.exp_context) + ")" diff --git a/chc/app/CFile.py b/chc/app/CFile.py index 4a4e0a0..be69244 100644 --- a/chc/app/CFile.py +++ b/chc/app/CFile.py @@ -270,17 +270,20 @@ def functions(self) -> Dict[int, CFunction]: if self._functions is None: self._functions = {} for (vid, gf) in self.gfunctions.items(): - fnname = gf.vname - xnode = UF.get_cfun_xnode( - self.targetpath, - self.projectname, - self.cfilepath, - self.cfilename, - fnname) - if xnode is not None: - cfunction = CFunction(self, xnode, fnname) - self._functions[vid] = cfunction - else: + try: + fnname = gf.vname + xnode = UF.get_cfun_xnode( + self.targetpath, + self.projectname, + self.cfilepath, + self.cfilename, + fnname) + if xnode is not None: + cfunction = CFunction(self, xnode, fnname) + self._functions[vid] = cfunction + else: + chklogger.logger.warning("Function {fnname} not found") + except Exception as e: chklogger.logger.warning("Function {fnname} not found") return self._functions diff --git a/chc/app/CHVersion.py b/chc/app/CHVersion.py index 61e0a46..8c97256 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-2024-12-04" diff --git a/chc/cmdline/c_file/cfileutil.py b/chc/cmdline/c_file/cfileutil.py index abdc97c..408e225 100644 --- a/chc/cmdline/c_file/cfileutil.py +++ b/chc/cmdline/c_file/cfileutil.py @@ -56,7 +56,7 @@ import subprocess import sys -from typing import Callable, List, NoReturn, Optional, TYPE_CHECKING +from typing import Callable, cast, List, NoReturn, Optional, TYPE_CHECKING from chc.cmdline.AnalysisManager import AnalysisManager from chc.cmdline.ParseManager import ParseManager @@ -71,6 +71,7 @@ from chc.util.loggingutil import chklogger, LogLevel if TYPE_CHECKING: + from chc.invariants.CInvariantFact import CInvariantNRVFact from chc.proof.CFunctionPO import CFunctionPO @@ -665,6 +666,62 @@ def header(s: str) -> str: exit(0) +def cfile_query_invariants(args: argparse.Namespace) -> NoReturn: + + # arguments + xcfilename: str = args.filename + opttgtpath: Optional[str] = args.tgtpath + xfunction: str = args.function + xline: int = args.line + + projectpath = os.path.dirname(os.path.abspath(xcfilename)) + targetpath = projectpath if opttgtpath is None else opttgtpath + targetpath = os.path.abspath(targetpath) + cfilename_c = os.path.basename(xcfilename) + cfilename = cfilename_c[:-2] + projectname = cfilename + + cchpath = UF.get_cchpath(targetpath, projectname) + contractpath = os.path.join(targetpath, "chc_contracts") + + if not UF.check_analysis_results_files(targetpath, projectname, None, cfilename): + print_error("No analysis results found for " + cfilename + + ". Please run analyzer first.") + exit(1) + + capp = CApplication( + projectpath, projectname, targetpath, contractpath, singlefile=True) + capp.initialize_single_file(cfilename) + cfile = capp.get_cfile() + + if not cfile.has_function_by_name(xfunction): + print_error("No function found with name " + xfunction) + exit(1) + + cfun = cfile.get_function_by_name(xfunction) + ppos = cfun.get_ppos() + contexts = {ppo.context for ppo in ppos if ppo.line == xline} + + print("Invariants for function " + xfunction + ", line " + str(xline)) + if len(contexts) == 0: + print("\nNo ast positions found with invariants on line " + str(xline) + ".") + exit(0) + + for ctxt in contexts: + print("\nAST position: " + str(ctxt)) + print("-" * (len(str(ctxt)) + 14)) + invs = cfun.invarianttable.get_sorted_invariants(ctxt) + nrvfacts: List[str] = [] + for inv in invs: + if inv.is_nrv_fact: + inv = cast("CInvariantNRVFact", inv) + if not inv.variable.is_check_variable: + nrvfacts.append(str(inv)) + print("\n".join(nrvfacts)) + + exit(0) + + def cfile_testlibc_summary(args: argparse.Namespace) -> NoReturn: """Runs one of the programs in tests/libcsummaries diff --git a/chc/cmdline/c_project/cprojectutil.py b/chc/cmdline/c_project/cprojectutil.py index d134fc2..8b41c9d 100644 --- a/chc/cmdline/c_project/cprojectutil.py +++ b/chc/cmdline/c_project/cprojectutil.py @@ -59,6 +59,7 @@ from chc.app.CFunction import CFunction from chc.app.CInstr import CInstr from chc.app.CStmt import CInstrsStmt, CStmt + from chc.invariants.CInvariantFact import CInvariantNRVFact from chc.proof.CFunctionPO import CFunctionPO @@ -410,6 +411,64 @@ def pofilter(po: "CFunctionPO") -> bool: exit(0) +def cproject_query_invariants(args: argparse.Namespace) -> NoReturn: + + # arguments + tgtpath: str = args.tgtpath + projectname: str = args.projectname + filename: str = args.filename + xfunction: str = args.function + xline: int = args.line + + targetpath = os.path.abspath(tgtpath) + projectpath = targetpath + cfilename_c = os.path.basename(filename) + cfilename = cfilename_c[:-2] + cfilepath = os.path.dirname(filename) + + 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) + + if not cfile.has_function_by_name(xfunction): + print_error("No function found with name " + xfunction) + exit(1) + + cfun = cfile.get_function_by_name(xfunction) + ppos = cfun.get_ppos() + contexts = {ppo.context for ppo in ppos if ppo.line == xline} + + print("Invariants for function " + xfunction + ", line " + str(xline)) + if len(contexts) == 0: + print("\nNo ast positions found with invariants on line " + str(xline) + ".") + exit(0) + + for ctxt in contexts: + print("\nAST position: " + str(ctxt)) + print("-" * (len(str(ctxt)) + 14)) + invs = cfun.invarianttable.get_sorted_invariants(ctxt) + nrvfacts: List[str] = [] + for inv in invs: + if inv.is_nrv_fact: + inv = cast("CInvariantNRVFact", inv) + if not inv.variable.is_check_variable: + nrvfacts.append(str(inv)) + print("\n".join(nrvfacts)) + + 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 fa14016..f2a40a9 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -834,6 +834,28 @@ def parse() -> argparse.Namespace: help="file mode for log file: append (a, default), or write (w)") cfileinvestigate.set_defaults(func=C.cfile_investigate_file) + # --- query + cfilequery = cfileparsers.add_parser("query") + cfilequeryparsers = cfilequery.add_subparsers(title="show options") + + # -- query invariants -- + cfilequeryinvs = cfilequeryparsers.add_parser("invariants") + cfilequeryinvs.add_argument( + "filename", + help="name of file analyzed (())") + cfilequeryinvs.add_argument( + "function", + help="name of function") + cfilequeryinvs.add_argument( + "line", + type=int, + help="line number in the code for which to show invariants") + cfilequeryinvs.add_argument( + "--tgtpath", + help="directory that holds the analysis results") + cfilequeryinvs.set_defaults(func=C.cfile_query_invariants) + + # --- test libc summary cfiletestlibc = cfileparsers.add_parser("test-libc-summary") cfiletestlibc.add_argument( @@ -1451,6 +1473,27 @@ def parse() -> argparse.Namespace: help="show location invariants on the code") cprojectreportfile.set_defaults(func=P.cproject_report_file) + # --- query + cprojectquery = cprojectparsers.add_parser("query") + cprojectqueryparsers = cprojectquery.add_subparsers(title="show options") + + # --- query invariants + cprojectqueryinvs = cprojectqueryparsers.add_parser("invariants") + cprojectqueryinvs.add_argument( + "tgtpath", help="directory that contains the analysis results") + cprojectqueryinvs.add_argument( + "projectname", help="name of the project") + cprojectqueryinvs.add_argument( + "filename", help="filename with relative path wrt the project") + cprojectqueryinvs.add_argument( + "function", help="name of function") + cprojectqueryinvs.add_argument( + "line", + type=int, + help="line number in the source code to show invariants") + cprojectqueryinvs.set_defaults(func=P.cproject_query_invariants) + + # --- count-statements cprojectcountstmts = cprojectparsers.add_parser("count-statements") cprojectcountstmts.add_argument( diff --git a/chc/invariants/CInvariantFact.py b/chc/invariants/CInvariantFact.py index 15f596b..1f216c0 100644 --- a/chc/invariants/CInvariantFact.py +++ b/chc/invariants/CInvariantFact.py @@ -58,6 +58,10 @@ def is_nrv_fact(self) -> bool: def is_unreachable_fact(self) -> bool: return False + @property + def is_parameter_constraint(self) -> bool: + return False + def __str__(self) -> str: return "invariant-fact:" + self.tags[0] @@ -100,6 +104,10 @@ def __init__( def xpr(self) -> "CXXpr": return self.xd.get_xpr(self.args[0]) + @property + def is_parameter_constraint(self) -> bool: + return True + def __str__(self) -> str: return str(self.xpr) diff --git a/chc/invariants/CXVariable.py b/chc/invariants/CXVariable.py index 3d6aaea..6e0eff4 100644 --- a/chc/invariants/CXVariable.py +++ b/chc/invariants/CXVariable.py @@ -75,6 +75,13 @@ def denotation(self) -> "CVariableDenotation": else: raise UF.CHCError("Variable does not have a denotation") + @property + def is_check_variable(self) -> bool: + if self.has_denotation(): + return self.vd.get_c_variable_denotation(self.seqnr).is_check_variable + else: + return False + def has_denotation(self) -> bool: return self.seqnr > 0 diff --git a/chc/util/fileutil.py b/chc/util/fileutil.py index 7882f45..a0c9fc8 100644 --- a/chc/util/fileutil.py +++ b/chc/util/fileutil.py @@ -939,6 +939,16 @@ def get_cfile_predicate_dictionaryname( return os.path.join(filepath, cfilename + "_prd.xml") +def check_analysis_results_files( + targetpath: str, + projectname: str, + cfilepath: Optional[str], + cfilename: str) -> bool: + filename = get_cfile_predicate_dictionaryname( + targetpath, projectname, cfilepath, cfilename) + return os.path.isfile(filename) + + def get_cfile_predicate_dictionary_xnode( targetpath: str, projectname: str, From 66ca36d1b958cd9e15a43ccc88c80cbec9f6f5b3 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 4 Dec 2025 16:54:29 -0800 Subject: [PATCH 2/2] fix pycode style issues --- chc/cmdline/chkc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc index f2a40a9..35a62f3 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -855,7 +855,6 @@ def parse() -> argparse.Namespace: help="directory that holds the analysis results") cfilequeryinvs.set_defaults(func=C.cfile_query_invariants) - # --- test libc summary cfiletestlibc = cfileparsers.add_parser("test-libc-summary") cfiletestlibc.add_argument( @@ -1438,9 +1437,11 @@ def parse() -> argparse.Namespace: choices=["a", "w"], default="a", help="file mode for log file: append (a, default), or write (w)") - cprojectanalyze.add_argument("-x", "--exclude", action='append', + cprojectanalyze.add_argument( + "-x", "--exclude", + action='append', help="Exclude file from analysis. To exclude multiple files, use " - "this option for each file, e.g. -x dir1/f1.c, -x dir2/f2.c") + "this option for each file, e.g. -x dir1/f1.c, -x dir2/f2.c") cprojectanalyze.set_defaults(func=P.cproject_analyze_project) # --- report @@ -1493,7 +1494,6 @@ def parse() -> argparse.Namespace: help="line number in the source code to show invariants") cprojectqueryinvs.set_defaults(func=P.cproject_query_invariants) - # --- count-statements cprojectcountstmts = cprojectparsers.add_parser("count-statements") cprojectcountstmts.add_argument(