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 c8cd8e9..b598584 100644 --- a/chc/cmdline/c_file/cfileutil.py +++ b/chc/cmdline/c_file/cfileutil.py @@ -56,6 +56,7 @@ import subprocess import sys + from typing import ( Any, Callable, cast, Dict, List, NoReturn, Optional, TYPE_CHECKING) @@ -73,6 +74,7 @@ from chc.util.loggingutil import chklogger, LogLevel if TYPE_CHECKING: + from chc.invariants.CInvariantFact import CInvariantNRVFact from chc.app.CAttributes import CAttributes from chc.app.CTyp import ( CTypComp, CTypFloat, CTypFun, CTypInt, CTypPtr) @@ -813,6 +815,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 b821477..14dbd17 100644 --- a/chc/cmdline/c_project/cprojectutil.py +++ b/chc/cmdline/c_project/cprojectutil.py @@ -61,6 +61,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.app.CTyp import ( CTypComp, CTypFloat, CTypFun, CTypInt, CTypPtr) from chc.proof.CFunctionPO import CFunctionPO @@ -598,6 +599,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 cb9113c..b104086 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -862,6 +862,27 @@ 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( @@ -1510,6 +1531,26 @@ 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 38f18a2..4815200 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,