CPROJ: add CLI commands

Author: sipma

chc/cmdline/AnalysisManager.py

@@ -202,21 +202,19 @@ def create_file_primary_proofobligations(
         """Call analyzer to create primary proof obligations for a single file."""
 
         chklogger.logger.info(
-            "Create primiary proof obligations for %s", cfilename)
+            "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.append(cfilename)
             if cfilepath is not None:
                 cmd.extend(["-cfilepath", cfilepath])
-            chklogger.logger.info(
-                "Primary proof obligations are created for %s", cfilename)
             chklogger.logger.info(
                 "Ocaml analyzer is called with %s", str(cmd))
             if self.verbose:
                 result = subprocess.call(
                     cmd, cwd=self.targetpath, stderr=subprocess.STDOUT)
                 print("\nResult: " + str(result))
-                # self.capp.get_file(cfilename).predicatedictionary.initialize()
             else:
                 result = subprocess.call(
                     cmd,
@@ -227,7 +225,10 @@ def create_file_primary_proofobligations(
             if result != 0:
                 print("Error in creating primary proof obligations")
                 exit(1)
-            cfile = self.capp.get_file(cfilename)
+            pcfilename = (
+                cfilename if cfilepath is None
+                else os.path.join(cfilepath, cfilename))
+            cfile = self.capp.get_file(pcfilename)
             cfile.reinitialize_tables()
             cfile.reload_ppos()
             cfile.reload_spos()
@@ -237,24 +238,28 @@ def create_file_primary_proofobligations(
             exit(1)
 
     def create_app_primary_proofobligations(self, processes: int = 1) -> None:
-        """Call analyzer to create primary proof obligations for all application files."""
+        """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.append(cfile.name)
+                if cfile.cfilepath is not None:
+                    cmd.extend(["-filepath", cfile.cfilepath])
+                cmd.append(cfile.cfilename)
                 self._execute_cmd(cmd)
 
             self.capp.iter_files_parallel(f, processes)
         else:
 
             def f(cfile: "CFile") -> None:
-                self.create_file_primary_proofobligations(cfile.name)
+                self.create_file_primary_proofobligations(
+                    cfile.cfilename, cfile.cfilepath)
 
             self.capp.iter_files(f)
 
-    def _generate_and_check_file_cmd_partial(self, domains: str) -> List[str]:
+    def _generate_and_check_file_cmd_partial(
+            self, cfilepath: Optional[str], domains: str) -> List[str]:
         cmd: List[str] = [
             self.canalyzer,
             "-summaries",
@@ -279,14 +284,20 @@ def _generate_and_check_file_cmd_partial(self, domains: str) -> List[str]:
         if self.verbose:
             cmd.append("-verbose")
         cmd.append(self.targetpath)
+        if cfilepath is not None:
+            cmd.extend(["-cfilepath", cfilepath])
         cmd.append("-cfilename")
         return cmd
 
-    def generate_and_check_file(self, cfilename: str, domains: str) -> None:
+    def generate_and_check_file(
+            self,
+            cfilename: str,
+            cfilepath: Optional[str],
+            domains: str) -> None:
         """Generate invariants and check proof obligations for a single file."""
 
         try:
-            cmd = self._generate_and_check_file_cmd_partial(domains)
+            cmd = self._generate_and_check_file_cmd_partial(cfilepath, domains)
             cmd.append(cfilename)
             chklogger.logger.info(
                 "Calling AI to generate invariants: %s",
@@ -303,7 +314,8 @@ def generate_and_check_file(self, cfilename: str, domains: str) -> None:
                     stderr=subprocess.STDOUT,
                 )
             if result != 0:
-                print("Error in generating invariants or checking proof obligations")
+                chklogger.logger.error(
+                    "Error in generating invariants for %s", cfilename)
                 exit(1)
         except subprocess.CalledProcessError as args:
             print(args.output)
@@ -316,15 +328,17 @@ def generate_and_check_app(self, domains: str, processes: int = 1) -> None:
         if processes > 1:
 
             def f(cfile: "CFile") -> None:
-                cmd = self._generate_and_check_file_cmd_partial(domains)
-                cmd.append(cfile.name)
+                cmd = self._generate_and_check_file_cmd_partial(
+                    cfile.cfilepath, domains)
+                cmd.append(cfile.cfilename)
                 self._execute_cmd(cmd)
 
             self.capp.iter_files_parallel(f, processes)
         else:
 
             def f(cfile: "CFile") -> None:
-                self.generate_and_check_file(cfile.name, domains)
+                self.generate_and_check_file(
+                    cfile.cfilename, cfile.cfilepath, domains)
 
             self.capp.iter_files(f)
         self.capp.iter_files(self.reset_tables)

chc/cmdline/c_file/cfileutil.py

@@ -24,7 +24,7 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 # ------------------------------------------------------------------------------
-"""Command-line interface to the CodeHawk C Analyzer.
+"""Implementation of commands for processing single files in the CLI.
 
 The functions in this module support the commands available in the single-file
 mode of the CodeHawk-C analyzer.
@@ -145,7 +145,7 @@ def cfile_parse_file(args: argparse.Namespace) -> NoReturn:
         targetpath,
         logfilename=logfilename,
         mode=logfilemode,
-        msg="cfile parse invoked")
+        msg="c-file parse invoked")
 
     chklogger.logger.info("Target path: %s", targetpath)
 
@@ -257,13 +257,13 @@ def cfile_analyze_file(args: argparse.Namespace) -> NoReturn:
     am.reset_tables(cfile)
     capp.collect_post_assumes()
 
-    am.generate_and_check_file(cfilename, "llrvisp")
+    am.generate_and_check_file(cfilename, None, "llrvisp")
     am.reset_tables(cfile)
     capp.collect_post_assumes()
 
     for k in range(5):
         capp.update_spos()
-        am.generate_and_check_file(cfilename, "llrvisp")
+        am.generate_and_check_file(cfilename, None, "llrvisp")
         am.reset_tables(cfile)
 
     chklogger.logger.info("cfile analyze completed")
@@ -517,13 +517,13 @@ def cfile_testlibc_summary(args: argparse.Namespace) -> NoReturn:
     am.reset_tables(cfile)
     capp.collect_post_assumes()
 
-    am.generate_and_check_file(cfilename, "llrvisp")
+    am.generate_and_check_file(cfilename, None, "llrvisp")
     am.reset_tables(cfile)
     capp.collect_post_assumes()
 
     for k in range(5):
         capp.update_spos()
-        am.generate_and_check_file(cfilename, "llrvisp")
+        am.generate_and_check_file(cfilename, None, "llrvisp")
         am.reset_tables(cfile)
 
     chklogger.logger.info("cfile analyze completed")