CMD: add query facility for invariants

Author: sipma

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) + ")"

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
 

chc/app/CHVersion.py

@@ -1 +1 @@
-chcversion: str = "0.2.0-2024-11-04"
+chcversion: str = "0.2.0-2024-12-04"

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
 

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."""
 

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 ((<cpath/>)<cfilename>)")
+    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(

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)
 

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
 

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,