CMD: add command to list arguments to calls

Author: sipma

chc/cmdline/c_project/cprojectutil.py

@@ -38,7 +38,7 @@
 from contextlib import contextmanager
 
 from typing import (
-    Any, cast, Dict, Generator, List, Optional, NoReturn, TYPE_CHECKING)
+    Any, cast, Dict, Generator, List, Optional, NoReturn, Tuple, TYPE_CHECKING)
 
 from chc.app.CApplication import CApplication
 
@@ -291,6 +291,7 @@ def cproject_report_file(args: argparse.Namespace) -> NoReturn:
     filename: str = args.filename
     showcode: bool = args.showcode
     showopen: bool = args.open
+    showinvariants: bool = args.showinvariants
 
     targetpath = os.path.abspath(tgtpath)
     projectpath = targetpath
@@ -320,7 +321,8 @@ def pofilter(po: "CFunctionPO") -> bool:
             return True
 
     if showcode:
-        print(RP.file_code_tostring(cfile, pofilter=pofilter))
+        print(RP.file_code_tostring(
+            cfile, pofilter=pofilter, showinvs=showinvariants))
 
     print(RP.file_proofobligation_stats_tostring(cfile))
 
@@ -523,6 +525,58 @@ def collect_fi_callees(cfile: "CFile") -> None:
     exit(0)
 
 
+def cproject_collect_call_arguments(args: argparse.Namespace) -> NoReturn:
+
+    # arguments
+    tgtpath: str = args.tgtpath
+    projectname: str = args.projectname
+
+    targetpath = os.path.abspath(tgtpath)
+    projectpath = targetpath
+    contractpath = os.path.join(targetpath, "chc_contracts")
+
+    if not UF.has_analysisresults_path(targetpath, projectname):
+        print_error(
+            f"No analysis results found for {projectname} in {targetpath}")
+        exit(1)
+
+    capp = CApplication(
+        projectpath, projectname, targetpath, contractpath)
+
+    # callee -> (file, caller) -> arguments
+    result: Dict[str, Dict[Tuple[int, str, str], List[str]]] = {}
+
+    counter: int = 0
+    for cfile in capp.cfiles:
+        for cfun in cfile.get_functions():
+            for instr in cfun.call_instrs:
+                callee = str(instr.callee)
+                callargs = instr.callargs
+                result.setdefault(callee, {})
+                result[callee][(counter, cfile.cfilename, cfun.name)] = [
+                    str(i) for i in callargs]
+                counter += 1
+
+    lines: List[str] = []
+
+    for callee in sorted(result):
+        lines.append("\n" + callee)
+        lines.append("-" * len(callee))
+        for (index, cfilename, caller) in sorted(result[callee]):
+            calltxt = (
+                callee
+                + "("
+                + ", ".join(result[callee][(index, cfilename, caller)])
+                + ")")
+            lines.append(
+                ("[" + cfilename + ".c:" + caller + "] ").ljust(35)
+                + calltxt)
+
+    print("\n".join(lines))
+
+    exit(0)
+
+
 def cproject_missing_summaries(args: argparse.Namespace) -> NoReturn:
     """CLI command to output library functions without summaries."""
 

chc/cmdline/chkc

@@ -1376,6 +1376,10 @@ def parse() -> argparse.Namespace:
         "--open",
         action="store_true",
         help="only show open proof obligations (or violations)")
+    cprojectreportfile.add_argument(
+        "--showinvariants",
+        action="store_true",
+        help="show location invariants on the code")
     cprojectreportfile.set_defaults(func=P.cproject_report_file)
 
     # --- count-statements
@@ -1400,6 +1404,14 @@ def parse() -> argparse.Namespace:
         "--save", help="name of file (without extension) to save the results")
     cprojectcallgraph.set_defaults(func=P.cproject_make_callgraph)
 
+    # --- collect-call-arguments
+    cprojectcollectcallargs = cprojectparsers.add_parser("collect-call-arguments")
+    cprojectcollectcallargs.add_argument(
+        "tgtpath", help="directory that contains the analysis results")
+    cprojectcollectcallargs.add_argument(
+        "projectname", help="name of the project")
+    cprojectcollectcallargs.set_defaults(func=P.cproject_collect_call_arguments)
+
     # --- missing-summaries
     cprojectmissingsummaries = cprojectparsers.add_parser("missing-summaries")
     cprojectmissingsummaries.add_argument(