diff --git a/chc/app/CPrettyPrinter.py b/chc/app/CPrettyPrinter.py
index d74f4df..af1bfd6 100644
--- a/chc/app/CPrettyPrinter.py
+++ b/chc/app/CPrettyPrinter.py
@@ -310,12 +310,12 @@ def visit_funarg(self, funarg: CT.CFunArg) -> None:
self.funtypptr_with_name(ptx, funarg.name)
return
- if (
- argtyp.attributes.length > 0
- and argtyp.attributes.attributes[0].name == "arraylen"):
- self.ptrarg_with_attribute_length(
- ptargtyp, argtyp.attributes.attributes[0], funarg.name)
- return
+ # if (
+ # argtyp.attributes.length > 0
+ # and argtyp.attributes.attributes[0].name == "arraylen"):
+ # self.ptrarg_with_attribute_length(
+ # ptargtyp, argtyp.attributes.attributes[0], funarg.name)
+ # return
funarg.typ.accept(self)
self.ccode.write(" ")
diff --git a/chc/app/CTyp.py b/chc/app/CTyp.py
index 3c9e666..1a8e87b 100644
--- a/chc/app/CTyp.py
+++ b/chc/app/CTyp.py
@@ -184,6 +184,10 @@ def is_pointer(self) -> bool:
def is_struct(self) -> bool:
return False
+ @property
+ def is_union(self) -> bool:
+ return False
+
@property
def is_void(self) -> bool:
return False
@@ -388,6 +392,10 @@ def name(self) -> str:
def is_struct(self) -> bool:
return self.compinfo.is_struct
+ @property
+ def is_union(self) -> bool:
+ return not self.compinfo.is_struct
+
def accept(self, visitor: "CVisitor") -> None:
visitor.visit_comptyp(self)
diff --git a/chc/cmdline/c_file/cfileutil.py b/chc/cmdline/c_file/cfileutil.py
index abdc97c..788b80b 100644
--- a/chc/cmdline/c_file/cfileutil.py
+++ b/chc/cmdline/c_file/cfileutil.py
@@ -56,13 +56,15 @@
import subprocess
import sys
-from typing import Callable, List, NoReturn, Optional, TYPE_CHECKING
+from typing import (
+ Any, Callable, cast, Dict, List, NoReturn, Optional, TYPE_CHECKING)
from chc.cmdline.AnalysisManager import AnalysisManager
from chc.cmdline.ParseManager import ParseManager
import chc.cmdline.jsonresultutil as JU
from chc.app.CApplication import CApplication
+from chc.app.CPrettyPrinter import CPrettyPrinter
import chc.reporting.ProofObligations as RP
@@ -71,6 +73,9 @@
from chc.util.loggingutil import chklogger, LogLevel
if TYPE_CHECKING:
+ from chc.app.CAttributes import CAttributes
+ from chc.app.CTyp import (
+ CTypComp, CTypFloat, CTypFun, CTypInt, CTypPtr)
from chc.proof.CFunctionPO import CFunctionPO
@@ -174,6 +179,149 @@ def cfile_parse_file(args: argparse.Namespace) -> NoReturn:
exit(0)
+def cfile_scan_op(args: argparse.Namespace) -> NoReturn:
+
+ # arguments
+ xcfilename: str = args.filename
+ jsonoutput: bool = args.json
+ outputfilename: Optional[str] = args.output
+ loglevel: str = args.loglevel
+ logfilename: Optional[str] = args.logfilename
+ logfilemode: str = args.logfilemode
+
+ projectpath = os.path.dirname(os.path.abspath(xcfilename))
+ targetpath = projectpath
+ targetpath = os.path.abspath(targetpath)
+ cfilename_ext = os.path.basename(xcfilename)
+ cfilename = cfilename_ext[:-2]
+ projectname = cfilename
+
+ set_logging(
+ loglevel,
+ targetpath,
+ logfilename=logfilename,
+ mode=logfilemode,
+ msg="Command cfile scan-output-parameters invoked")
+
+ chklogger.logger.info(
+ "Project path: %s; target path: %s", projectpath, targetpath)
+
+ parsearchive = UF.get_parse_archive(targetpath, projectname)
+
+ if not os.path.isfile(parsearchive):
+ print_error("Please run parser first on c file")
+ exit(1)
+
+ if os.path.isfile(parsearchive):
+ os.chdir(targetpath)
+ tarname = os.path.basename(parsearchive)
+ cmd = ["tar", "xfz", os.path.basename(tarname)]
+ result = subprocess.call(cmd, cwd=targetpath, stderr=subprocess.STDOUT)
+ if result != 0:
+ print_error("Error in extracting " + tarname)
+ exit(1)
+
+ def has_const_attribute(attrs: "CAttributes") -> bool:
+ for attr in attrs.attributes:
+ if "const" in attr.name:
+ return True
+ return False
+
+ contractpath = os.path.join(targetpath, "chc_contracts")
+
+ capp = CApplication(
+ projectpath, projectname, targetpath, contractpath, singlefile=True)
+
+ capp.initialize_single_file(cfilename)
+ cfile = capp.get_cfile()
+
+ ptrcandidates: List[Dict[str, Any]] = []
+ opcandidates: List[Dict[str, Any]] = []
+
+ for cfun in cfile.gfunctions.values():
+ if cfun.varinfo.vname == "main":
+ continue
+ pp = CPrettyPrinter()
+ fndecl = pp.function_declaration_str(cfun.varinfo).strip()
+ cfuntyp = cfun.varinfo.vtype
+ if not cfuntyp.is_function:
+ continue
+ cfuntyp = cast("CTypFun", cfuntyp)
+ cfunargs = cfuntyp.funargs
+ if cfunargs is None:
+ continue
+ cfunarguments = cfunargs.arguments
+ if not any(cfunarg.typ.is_pointer for cfunarg in cfunarguments):
+ continue
+ candidate: Dict[str, Any] = {}
+ candidate["name"] = cfun.vname
+ candidate["signature"] = fndecl
+ ptrargs = candidate["ptrargs"] = []
+ for (index, cfunarg) in enumerate(cfunarguments):
+ argtyp = cfunarg.typ.expand()
+ if argtyp.is_pointer:
+ disqualifiers: List[str] = []
+ argtgttyp = cast("CTypPtr", argtyp).pointedto_type.expand()
+ ptrarg: Dict[str, Any] = {}
+ ptrarg["index"] = index
+ ptrarg["name"] = cfunarg.name
+ ptrarg["target-type"] = str(argtgttyp)
+ if argtgttyp.attributes.length > 0:
+ ptrarg["attributes"] = (
+ [str(attr) for attr in argtgttyp.attributes.attributes])
+ if has_const_attribute(argtgttyp.attributes):
+ disqualifiers.append("const")
+ if argtgttyp.is_int:
+ ptrarg["kind"] = ["int", cast("CTypInt", argtgttyp).ikind]
+ if "ichar" in ptrarg["kind"]:
+ disqualifiers.append("ichar")
+ elif "iuchar" in ptrarg["kind"]:
+ disqualifiers.append("iuchar")
+ elif argtgttyp.is_float:
+ ptrarg["kind"] = ["float", cast("CTypFloat", argtgttyp).fkind]
+ elif argtgttyp.is_void:
+ ptrarg["kind"] = ["void"]
+ disqualifiers.append("void")
+ elif argtgttyp.is_pointer:
+ ptrarg["kind"] = ["pointer"]
+ disqualifiers.append("pointer")
+ elif argtgttyp.is_struct:
+ ptrarg["kind"] = ["struct", cast("CTypComp", argtgttyp).name]
+ elif argtgttyp.is_union:
+ ptrarg["kind"] = ["union", cast("CTypComp", argtgttyp).name]
+ disqualifiers.append("union")
+ else:
+ ptrarg["kind"] = ["other"]
+ if len(disqualifiers) > 0:
+ ptrarg["disqualifiers"] = disqualifiers
+ else:
+ opcandidate: Dict[str, Any] = {}
+ opcandidate["function"] = cfun.varinfo.vname
+ opcandidate["arg-index"] = index
+ opcandidate["arg-name"] = cfunarg.name
+ opcandidate["arg-target-type"] = str(argtgttyp)
+ opcandidates.append(opcandidate)
+ ptrargs.append(ptrarg)
+ ptrcandidates.append(candidate)
+
+ results: Dict[str, Any] = {}
+ results["function-count"] = len(cfile.gfunctions.keys())
+ results["ptr-candidates"] = ptrcandidates
+ results["op-candidates"] = opcandidates
+
+ if jsonoutput:
+ jsonresult = JU.cfile_output_parameters_to_json_result(cfilename, results)
+ jsonok = JU.jsonok("scan_output_parameters", jsonresult.content)
+ if outputfilename is not None:
+ with open(outputfilename, "w") as fp:
+ json.dump(jsonok, fp, indent=2)
+ else:
+ resultstring = json.dumps(jsonok, indent=2)
+ print(resultstring)
+
+ exit(0)
+
+
def cfile_mk_headerfile(args: argparse.Namespace) -> NoReturn:
"""Produces a .c file with prototype definitions of functions and global variables.
diff --git a/chc/cmdline/c_project/cprojectutil.py b/chc/cmdline/c_project/cprojectutil.py
index d134fc2..b821477 100644
--- a/chc/cmdline/c_project/cprojectutil.py
+++ b/chc/cmdline/c_project/cprojectutil.py
@@ -41,6 +41,7 @@
Any, cast, Dict, Generator, List, Optional, NoReturn, Tuple, TYPE_CHECKING)
from chc.app.CApplication import CApplication
+from chc.app.CPrettyPrinter import CPrettyPrinter
from chc.cmdline.AnalysisManager import AnalysisManager
from chc.cmdline.ParseManager import ParseManager
@@ -55,10 +56,13 @@
from chc.util.loggingutil import chklogger, LogLevel
if TYPE_CHECKING:
+ 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.CStmt import CInstrsStmt, CStmt
+ from chc.app.CTyp import (
+ CTypComp, CTypFloat, CTypFun, CTypInt, CTypPtr)
from chc.proof.CFunctionPO import CFunctionPO
@@ -161,6 +165,179 @@ def cproject_parse_project(args: argparse.Namespace) -> NoReturn:
exit(0)
+def cproject_scan_op(args: argparse.Namespace) -> NoReturn:
+
+ # arguments
+ tgtpath: str = args.tgtpath
+ projectname: str = args.projectname
+ jsonoutput: bool = args.json
+ outputfilename: Optional[str] = args.output
+ loglevel: str = args.loglevel
+ logfilename: Optional[str] = args.logfilename
+ logfilemode: str = args.logfilemode
+
+ if not os.path.isdir(tgtpath):
+ print_error(f"Target directory {tgtpath} not found")
+ exit(1)
+
+ targetpath = os.path.abspath(tgtpath)
+ projectpath = targetpath
+ contractpath = os.path.join(projectpath, "cch_contracts")
+
+ set_logging(
+ loglevel,
+ targetpath,
+ logfilename=logfilename,
+ mode=logfilemode,
+ msg="c-project scan-output-parameters invoked")
+
+ capp = CApplication(
+ projectpath, projectname, targetpath, contractpath)
+
+ def has_const_attribute(attrs: "CAttributes") -> bool:
+ for attr in attrs.attributes:
+ if "const" in attr.name:
+ return True
+ return False
+
+ cfilecandidates: List[Dict[str, Any]] = []
+ opcandidates: List[Dict[str, Any]] = []
+ disqualifiersum: Dict[str, int] = {}
+ qualifiersum: Dict[str, int] = {}
+ structsum: Dict[str, int] = {}
+
+ totalfunctioncount = 0
+ totalptrargcount = 0
+ totalcandidatefns = 0
+
+ for cfile in capp.cfiles:
+ if cfile.cfilepath is not None:
+ cfilename = os.path.join(cfile.cfilepath, cfile.cfilename)
+ else:
+ cfilename = cfile.cfilename
+
+ candidates: List[Dict[str, Any]] = []
+ for cfun in cfile.gfunctions.values():
+ if cfun.varinfo.vname == "main":
+ continue
+ pp = CPrettyPrinter()
+ fndecl = pp.function_declaration_str(cfun.varinfo).strip()
+ cfuntyp = cfun.varinfo.vtype
+ if not cfuntyp.is_function:
+ continue
+ cfuntyp = cast("CTypFun", cfuntyp)
+ cfunargs = cfuntyp.funargs
+ if cfunargs is None:
+ continue
+ cfunarguments = cfunargs.arguments
+ if not any(cfunarg.typ.is_pointer for cfunarg in cfunarguments):
+ continue
+ candidate: Dict[str, Any] = {}
+ candidate["name"] = cfun.vname
+ candidate["signature"] = fndecl
+ ptrargs = candidate["ptrargs"] = []
+ for (index, cfunarg) in enumerate(cfunarguments):
+ argtyp = cfunarg.typ.expand()
+ if argtyp.is_pointer:
+ totalptrargcount += 1
+ disqualifiers: List[str] = []
+ t = cast("CTypPtr", argtyp).pointedto_type.expand()
+ ptrarg: Dict[str, Any] = {}
+ ptrarg["index"] = index
+ ptrarg["name"] = cfunarg.name
+ ptrarg["target-type"] = str(t)
+ if cfunarg.typ.attributes.length > 0:
+ ptrarg["attributes"] = (
+ [str(attr) for attr in cfunarg.typ.attributes.attributes])
+ if has_const_attribute(cfunarg.typ.attributes):
+ disqualifiers.append("const")
+ if t.attributes.length > 0:
+ ptrarg["attributes"] = (
+ [str(attr) for attr in t.attributes.attributes])
+ if has_const_attribute(t.attributes):
+ disqualifiers.append("const")
+ disqualifiersum.setdefault("const", 0)
+ disqualifiersum["const"] += 1
+ if t.is_int:
+ ptrarg["kind"] = ["int", cast("CTypInt", t).ikind]
+ if "ichar" in ptrarg["kind"]:
+ disqualifiers.append("ichar")
+ disqualifiersum.setdefault("char", 0)
+ disqualifiersum["char"] == 1
+ elif "iuchar" in ptrarg["kind"]:
+ disqualifiers.append("iuchar")
+ disqualifiersum.setdefault("char", 0)
+ disqualifiersum["char"] += 1
+ elif t.is_float:
+ ptrarg["kind"] = ["float", cast("CTypFloat", t).fkind]
+ elif t.is_void:
+ ptrarg["kind"] = ["void"]
+ disqualifiers.append("void")
+ disqualifiersum.setdefault("void", 0)
+ disqualifiersum["void"] += 1
+ elif t.is_pointer:
+ ptrarg["kind"] = ["pointer"]
+ disqualifiers.append("pointer")
+ disqualifiersum.setdefault("pointer", 0)
+ disqualifiersum["pointer"] += 1
+ elif t.is_struct:
+ structname = cast("CTypComp", t).name
+ ptrarg["kind"] = ["struct", structname]
+ structsum.setdefault(structname, 0)
+ structsum[structname] += 1
+ elif t.is_union:
+ ptrarg["kind"] = ["union", cast("CTypComp", t).name]
+ disqualifiers.append("union")
+ disqualifiersum.setdefault("union", 0)
+ disqualifiersum["union"] += 1
+ else:
+ ptrarg["kind"] = ["other"]
+ if len(disqualifiers) > 0:
+ ptrarg["disqualifiers"] = disqualifiers
+ else:
+ opcandidate: Dict[str, Any] = {}
+ opcandidate["file"] = cfilename
+ opcandidate["function"] = cfun.varinfo.vname
+ opcandidate["arg-index"] = index
+ opcandidate["arg-name"] = cfunarg.name
+ opcandidate["arg-target-type"] = str(t)
+ if t.is_struct:
+ opcandidate["struct-name"] = cast("CTypComp", t).name
+ opcandidates.append(opcandidate)
+ ptrargs.append(ptrarg)
+ candidates.append(candidate)
+ totalcandidatefns += 1
+ cfilecandidate: Dict[str, Any] = {}
+ cfilecandidate["filename"] = cfilename
+ cfilecandidate["candidates"] = candidates
+ cfilecandidate["function-count"] = len(cfile.gfunctions.keys())
+ totalfunctioncount += len(cfile.gfunctions.keys())
+ cfilecandidates.append(cfilecandidate)
+
+ results: Dict[str, Any] = {}
+ results["files"] = cfilecandidates
+ results["op-candidates"] = opcandidates
+ results["struct-summary"] = structsum
+ results["disqualifier-summary"] = disqualifiersum
+ results["file-count"] = len(list(capp.cfiles))
+ results["total-function-count"] = totalfunctioncount
+ results["total-function-candidate-count"] = totalcandidatefns
+ results["total-argptr-count"] = totalptrargcount
+ results["op-candidate-count"] = len(opcandidates)
+
+ if jsonoutput:
+ jsonresult = JU.cproject_output_parameters_to_json_result(projectname, results)
+ jsonok = JU.jsonok("scan_output_parameters", jsonresult.content)
+ if outputfilename is not None:
+ with open(outputfilename, "w") as fp:
+ json.dump(jsonok, fp, indent=2)
+ else:
+ resultstring = json.dumps(jsonok, indent=2)
+ print(resultstring)
+
+ exit(0)
+
+
def cproject_mk_headerfile(args: argparse.Namespace) -> NoReturn:
# arguments
@@ -252,6 +429,9 @@ def cproject_analyze_project(args: argparse.Namespace) -> NoReturn:
logfilemode: str = args.logfilemode
excludefiles: List[str] = args.exclude
+ if excludefiles is None:
+ excludefiles = []
+
if not os.path.isdir(tgtpath):
print_error(f"Target directory {tgtpath} not found")
exit(1)
@@ -274,7 +454,11 @@ def cproject_analyze_project(args: argparse.Namespace) -> NoReturn:
exit(1)
capp = CApplication(
- projectpath, projectname, targetpath, contractpath, excludefiles=excludefiles)
+ projectpath,
+ projectname,
+ targetpath,
+ contractpath,
+ excludefiles=excludefiles)
def save_xrefs(f: "CFile") -> None:
capp.indexmanager.save_xrefs(
@@ -287,7 +471,11 @@ def save_xrefs(f: "CFile") -> None:
linker.save_global_compinfos()
capp = CApplication(
- projectpath, projectname, targetpath, contractpath, excludefiles=excludefiles)
+ projectpath,
+ projectname,
+ targetpath,
+ contractpath,
+ excludefiles=excludefiles)
am = AnalysisManager(capp, verbose=True)
diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc
index fa14016..2bf9dc0 100755
--- a/chc/cmdline/chkc
+++ b/chc/cmdline/chkc
@@ -650,6 +650,34 @@ def parse() -> argparse.Namespace:
cfileparse.set_defaults(func=C.cfile_parse_file)
+ # --- scan for output parameters
+ cfilescanop = cfileparsers.add_parser("scan-output-parameters")
+ cfilescanop.add_argument(
+ "filename",
+ help="name of file to scan (())")
+ cfilescanop.add_argument(
+ "--json",
+ action="store_true",
+ help="output results in json format")
+ cfilescanop.add_argument(
+ "--output", "-o",
+ help="name of output file")
+ cfilescanop.add_argument(
+ "--loglevel", "-log",
+ choices=UL.LogLevel.options(),
+ default="NONE",
+ help="activate logging with given level (default to stderr)")
+ cfilescanop.add_argument(
+ "--logfilename",
+ help="name of file to write log messages")
+ cfilescanop.add_argument(
+ "--logfilemode",
+ choices=["a", "w"],
+ default="a",
+ help="file mode for log file: append (a, default), or write (w)")
+
+ cfilescanop.set_defaults(func=C.cfile_scan_op)
+
# --- mk-headerfile
cfilemkheader = cfileparsers.add_parser("mk-headerfile")
cfilemkheader.add_argument(
@@ -1354,6 +1382,34 @@ def parse() -> argparse.Namespace:
cprojectparse.set_defaults(func=P.cproject_parse_project)
+ # --- scan for output parameters
+ cprojectscanop = cprojectparsers.add_parser("scan-output-parameters")
+ cprojectscanop.add_argument(
+ "tgtpath", help="directory that contains the analysis results")
+ cprojectscanop.add_argument(
+ "projectname", help="name of the project")
+ cprojectscanop.add_argument(
+ "--json",
+ action="store_true",
+ help="output results in json format")
+ cprojectscanop.add_argument(
+ "--output", "-o",
+ help="name of output file")
+ cprojectscanop.add_argument(
+ "--loglevel", "-log",
+ choices=UL.LogLevel.options(),
+ default="NONE",
+ help="activate logging with given level (default to stderr)")
+ cprojectscanop.add_argument(
+ "--logfilename",
+ help="name of file to write log messages")
+ cprojectscanop.add_argument(
+ "--logfilemode",
+ choices=["a", "w"],
+ default="a",
+ help="file mode for log file: append (a, default), or write (w)")
+ cprojectscanop.set_defaults(func=P.cproject_scan_op)
+
# --- mk-headerfile
cprojectmkheader = cprojectparsers.add_parser("mk-headerfile")
cprojectmkheader.add_argument(
@@ -1416,9 +1472,12 @@ def parse() -> argparse.Namespace:
choices=["a", "w"],
default="a",
help="file mode for log file: append (a, default), or write (w)")
- cprojectanalyze.add_argument("-x", "--exclude", action='append',
- help="Exclude file from analysis. To exclude multiple files, use "
- "this option for each file, e.g. -x dir1/f1.c, -x dir2/f2.c")
+ cprojectanalyze.add_argument(
+ "-x", "--exclude",
+ action="append",
+ help=(
+ "Exclude file from analysis. To exclude multiple files, use "
+ "this option for each file, e.g. -x dir1/f1.c, -x dir2/f2.c"))
cprojectanalyze.set_defaults(func=P.cproject_analyze_project)
# --- report
diff --git a/chc/cmdline/jsonresultutil.py b/chc/cmdline/jsonresultutil.py
index a8da57f..fca9e6c 100644
--- a/chc/cmdline/jsonresultutil.py
+++ b/chc/cmdline/jsonresultutil.py
@@ -243,3 +243,19 @@ def file_proofobligations_to_json_result(cfile: "CFile") -> JSONResult:
fnsdata.append(fndata)
content["functions"] = fnsdata
return JSONResult("fileproofobligations", content, "ok")
+
+
+def cfile_output_parameters_to_json_result(
+ cfilename: str, results: Dict[str, Any]) -> JSONResult:
+ content: Dict[str, Any] = {}
+ content["cfilename"] = cfilename
+ content["output-parameter-candidates"] = results
+ return JSONResult("cfile_output_parameter_candidates", content, "ok")
+
+
+def cproject_output_parameters_to_json_result(
+ projectname: str, results: Dict[str, Any]) -> JSONResult:
+ content: Dict[str, Any] = {}
+ content["cfilename"] = projectname
+ content["output-parameter-candidates"] = results
+ return JSONResult("cfile_output_parameter_candidates", content, "ok")