CMD: add cmdline options to choose analysis

Author: sipma

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:

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)
 
 

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,26 +489,31 @@ 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:
             print(str(e.wrap()))
             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)