CMD: delegate to analysis digests

Author: sipma

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)

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)
 

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)
 

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

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()