update project results

Author: sipma

.gitignore

@@ -1,12 +1,17 @@
 # CodeHawk C Analyzer artifacts
 semantics
 *.i
+*.cch
 
 # CodeHawk-C local configuration file
 ConfigLocal.py
 
 # Emacs
 *.py~
+*.rst~
+*.c~
+*.css~
+chkc~
 
 # Byte-compiled / optimized / DLL files
 __pycache__/
@@ -15,6 +20,7 @@ __pycache__/
 
 # C extensions
 *.so
+*.o
 
 # Distribution / packaging
 .Python

chc/api/ApiParameter.py

@@ -5,8 +5,8 @@
 # The MIT License (MIT)
 #
 # Copyright (c) 2017-2020 Kestrel Technology LLC
-# Copyright (c) 2020-2022 Henny Sipma
-# Copyright (c) 2023      Aarno Labs LLC
+# Copyright (c) 2020-2022 Henny B. Sipma
+# Copyright (c) 2023-2024 Aarno Labs LLC
 #
 # Permission is hereby granted, free of charge, to any person obtaining a copy
 # of this software and associated documentation files (the "Software"), to deal

chc/api/InterfaceDictionary.py

@@ -104,7 +104,8 @@ def __init__(self, cfile: "CFile", xnode: Optional[ET.Element]):
             self.postrequest_table,
             self.postassume_table,
             self.ds_condition_table]
-        self._objmaps: Dict[str, Callable[[], Mapping[int, IndexedTableValue]]] = {
+        self._objmaps: Dict[
+            str, Callable[[], Mapping[int, IndexedTableValue]]] = {
             "apiparam": self.get_api_parameter_map,
             "postassume": self.get_postassume_map,
             "postrequest": self.get_postrequest_map,
@@ -668,10 +669,12 @@ def objectmap_to_string(self, name: str) -> str:
             objmap = self._objmaps[name]()
             lines: List[str] = []
             if len(objmap) == 0:
-                lines.append("Table is empty")
+                lines.append(f"\nTable for {name} is empty\n")
             else:
+                lines.append("index  value")
+                lines.append("-" * 80)
                 for (ix, obj) in objmap.items():
-                    lines.append(str(ix).rjust(3) + "  " + str(obj))
+                    lines.append(str(ix).rjust(3) + "    " + str(obj))
             return "\n".join(lines)
         else:
             raise UF.CHCError(

chc/api/STerm.py

@@ -26,7 +26,16 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 # ------------------------------------------------------------------------------
-"""Object representation of sum type s_term (term in an external predicate)."""
+"""Object representation of sum type s_term (term in an external predicate).
+
+Object representation of the corresponding OCaml sumtype: s_term_t: a term that
+solely refers to entities that are visible outside of a function, such as its
+parameters or return value.
+
+The properties of a term are constructed from its indexed value in the
+InterfaceDictionary.
+
+"""
 from typing import Dict, List, Optional, TYPE_CHECKING
 import xml.etree.ElementTree as ET
 

chc/api/XPredicate.py

@@ -26,7 +26,15 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 # ------------------------------------------------------------------------------
-"""Object representation of sum type xpredicate_t."""
+"""Object representation of sum type xpredicate_t.
+
+Object representation of the corresponding OCaml sumtype: xpredicate_t: a
+predicate over s_term_t terms (terms that are visible outside of a function).
+
+The properties of an xpredicate are constructed from its indexed value in the
+InterfaceDictionary
+
+"""
 
 from typing import cast, List, Optional, TYPE_CHECKING
 import xml.etree.ElementTree as ET

chc/cmdline/AnalysisManager.py

@@ -244,10 +244,17 @@ def create_app_primary_proofobligations(self, processes: int = 1) -> None:
 
             def f(cfile: "CFile") -> None:
                 cmd = self._create_file_primary_proofobligations_cmd_partial()
-                if cfile.cfilepath is not None:
-                    cmd.extend(["-filepath", cfile.cfilepath])
                 cmd.append(cfile.cfilename)
+                if cfile.cfilepath is not None:
+                    cmd.extend(["-cfilepath", cfile.cfilepath])
                 self._execute_cmd(cmd)
+                pcfilename = (
+                    cfile.cfilename if cfile.cfilepath is None
+                    else os.path.join(cfile.cfilepath, cfile.cfilename))
+                cfile = self.capp.get_file(pcfilename)
+                cfile.reinitialize_tables()
+                cfile.reload_ppos()
+                cfile.reload_spos()
 
             self.capp.iter_files_parallel(f, processes)
         else:

chc/cmdline/c_project/cprojectutil.py

@@ -166,6 +166,7 @@ def cproject_analyze_project(args: argparse.Namespace) -> NoReturn:
     # arguments
     tgtpath: str = args.tgtpath
     projectname: str = args.projectname
+    maxprocesses: int = args.maxprocesses
     loglevel: str = args.loglevel
     logfilename: Optional[str] = args.logfilename
     logfilemode: str = args.logfilemode
@@ -212,30 +213,30 @@ def save_xrefs(f: "CFile") -> None:
     with timing("analysis"):
 
         try:
-            am.create_app_primary_proofobligations()
+            am.create_app_primary_proofobligations(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("llrvisp")
+            am.generate_and_check_app("llrvisp", processes=maxprocesses)
             capp.reinitialize_tables()
             capp.update_spos()
 
         for i in range(5):
             capp.update_spos()
-            am.generate_and_check_app("llrvisp")
+            am.generate_and_check_app("llrvisp", processes=maxprocesses)
             capp.reinitialize_tables()
 
     timestamp = os.stat(UF.get_cchpath(targetpath, projectname)).st_ctime
 
     result = RP.project_proofobligation_stats_to_dict(capp)
     result["timestamp"] = timestamp
     result["project"] = projectpath
-    UF.save_project_summary_results(targetpath, result)
-    UF.save_project_summary_results_as_xml(targetpath, result)
+    UF.save_project_summary_results(targetpath, projectname, result)
+    UF.save_project_summary_results_as_xml(targetpath, projectname, result)
 
     exit(0)
 
@@ -250,7 +251,7 @@ def cproject_report(args: argparse.Namespace) -> NoReturn:
     targetpath = os.path.abspath(tgtpath)
     projectpath = targetpath
 
-    result = UF.read_project_summary_results(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)
@@ -268,10 +269,10 @@ def cproject_report(args: argparse.Namespace) -> NoReturn:
     fresult = RP.project_proofobligation_stats_to_dict(capp)
     fresult["timestamp"] = timestamp
     fresult["project"] = projectpath
-    UF.save_project_summary_results(targetpath, fresult)
-    UF.save_project_summary_results_as_xml(targetpath, fresult)
+    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)
+    result = UF.read_project_summary_results(targetpath, projectname)
     if result is not None:
         print(RP.project_proofobligation_stats_dict_to_string(result))
     else:

chc/cmdline/chkc

@@ -65,7 +65,6 @@ import chc.cmdline.c_file.cfiletableutil as CT
 import chc.cmdline.c_project.cprojectutil as P
 import chc.cmdline.juliet.julietutil as J
 import chc.cmdline.kendra.kendrautil as K
-import chc.reporting.DictionaryTables as DT
 
 from chc.util.Config import Config
 import chc.util.loggingutil as UL
@@ -405,8 +404,7 @@ def parse() -> argparse.Namespace:
         "cfilename", help="name of kendra c file (e.g., id115.c)")
     kendrashowfiletable.add_argument(
         "tablename",
-        help="name of table",
-        choices = DT.file_table_list())
+        help="name of table")
     kendrashowfiletable.set_defaults(func=K.kendra_show_file_table)
 
     # --- kendra show-function-table
@@ -417,8 +415,7 @@ def parse() -> argparse.Namespace:
         "functionname", help="name of function in c file (e.g., main)")
     kendrashowfunctiontable.add_argument(
         "tablename",
-        help="name of table",
-        choices = DT.function_table_list())
+        help="name of table")
     kendrashowfunctiontable.set_defaults(func=K.kendra_show_function_table)
 
     # --------------------------------------------------------------- juliet ---
@@ -1296,6 +1293,11 @@ def parse() -> argparse.Namespace:
         "tgtpath", help="directory that contains the analysis results")
     cprojectanalyze.add_argument(
         "projectname", help="name of the project")
+    cprojectanalyze.add_argument(
+        "--maxprocesses",
+        help="number of files to process in parallel",
+        type=int,
+        default=1)
     cprojectanalyze.add_argument(
         "--loglevel", "-log",
         choices=UL.LogLevel.options(),

chc/cmdline/juliet/julietutil.py

@@ -404,7 +404,7 @@ def filefilter(filename: str) -> bool:
             capp, filefilter=filefilter)
         result["timestamp"] = timestamp
         result["path"] = capp.projectpath
-        UF.save_project_summary_results(capp.targetpath, result)
+        UF.save_project_summary_results(capp.targetpath, "juliet", result)
     except Exception as e:
         print(str(e))
         exit(1)
@@ -488,7 +488,7 @@ def juliet_report(args: argparse.Namespace) -> NoReturn:
     excludefiles = ["io.c", "main_linux.c", "std_thread.c"]
     targetpath = projectpath
 
-    summary = UF.read_project_summary_results(targetpath)
+    summary = UF.read_project_summary_results(targetpath, "juliet")
     if summary is not None:
         print(RP.project_proofobligation_stats_dict_to_string(summary))
         exit(0)
@@ -1026,7 +1026,7 @@ def juliet_project_dashboard(args: argparse.Namespace) -> NoReturn:
         for test in testcases[cwe]:
             pname = f"{cwe}:{test}"
             path = UF.get_juliet_testpath(cwe, test)
-            results = UF.read_project_summary_results(path)
+            results = UF.read_project_summary_results(path, "juliet")
             if results is None:
                 nosummary.append(pname)
                 continue

chc/cmdline/kendra/kendrautil.py

@@ -41,7 +41,6 @@
 from chc.cmdline.kendra.TestSetRef import TestSetRef
 from chc.cmdline.ParseManager import ParseManager
 
-import chc.reporting.DictionaryTables as DT
 import chc.reporting.ProofObligations as RP
 
 import chc.util.fileutil as UF