CFILE: add c-file run command

Author: sipma

chc/cmdline/c_file/cfileutil.py

@@ -348,6 +348,155 @@ def pofilter(po: "CFunctionPO") -> bool:
     exit(0)
 
 
+def cfile_run_file(args: argparse.Namespace) -> NoReturn:
+    """Parses, analyzes, and outputs a report for a single file."""
+
+    # arguments
+    pcfilename: str = os.path.abspath(args.filename)
+    opttgtpath: Optional[str] = args.tgtpath
+    cshowcode: bool = args.showcode
+    copen: bool = args.open
+    jsonoutput: bool = args.json
+    outputfile: Optional[str] = args.output
+    loglevel: str = args.loglevel
+    logfilename: Optional[str] = args.logfilename
+    logfilemode: str = args.logfilemode
+
+    try:
+        UF.check_parser()
+    except UF.CHError as e:
+        print(str(e.wrap()))
+        exit(1)
+
+    if not os.path.isfile(os.path.abspath(pcfilename)):
+        print_error("C source code file " + pcfilename + " not found")
+        exit(1)
+
+    if not pcfilename.endswith(".c"):
+        print_error("C source code file should have extension .c")
+        exit(1)
+
+    projectpath = os.path.dirname(os.path.abspath(pcfilename))
+    targetpath = projectpath if opttgtpath is None else opttgtpath
+    targetpath = os.path.abspath(targetpath)
+    cfilename_c = os.path.basename(pcfilename)
+    cfilename = cfilename_c[:-2]
+    projectname = cfilename
+
+    if not os.path.isdir(targetpath):
+        print_error("Target directory: " + targetpath + " does not exist")
+        exit(1)
+
+    set_logging(
+        loglevel,
+        targetpath,
+        logfilename=logfilename,
+        mode=logfilemode,
+        msg="Command cfile run was invoked")
+
+    chklogger.logger.info("Target path: %s", targetpath)
+
+    parsemanager = ParseManager(projectpath, projectname, targetpath)
+    parsemanager.remove_semantics()
+    parsemanager.initialize_paths()
+
+    try:
+        cfilename_i = parsemanager.preprocess_file_with_gcc(cfilename_c)
+        result = parsemanager.parse_ifile(cfilename_i)
+        if result != 0:
+            print("*" * 80)
+            print("Error in parsing " + cfilename_c)
+            if Config().platform == "macOS":
+                print("  (Problem may be related to standard header files on macOS)")
+            print("*" * 80)
+            exit(1)
+    except OSError as e:
+        print_error("Error when parsing file: " + str(e))
+        exit(1)
+
+    parsemanager.save_semantics()
+
+    chklogger.logger.info("cfile parse completed")
+
+    parsearchive = UF.get_parse_archive(targetpath, projectname)
+
+    if not os.path.isfile(parsearchive):
+        print_error("Please run parser first on c file")
+        exit(1)
+
+    cchpath = UF.get_cchpath(targetpath, projectname)
+
+    if os.path.isdir(cchpath):
+        chklogger.logger.info("Old analysis results: %s are removed", cchpath)
+        shutil.rmtree(cchpath)
+
+    if os.path.isfile(parsearchive):
+        chklogger.logger.info("Directory is changed to %s", targetpath)
+        os.chdir(targetpath)
+        tarname = os.path.basename(parsearchive)
+        cmd = ["tar", "xfz", os.path.basename(tarname)]
+        chklogger.logger.info("Semantics is extracted from %s", tarname)
+        result = subprocess.call(cmd, cwd=targetpath, stderr=subprocess.STDOUT)
+        if result != 0:
+            print_error("Error in extracting " + tarname)
+            exit(1)
+        chklogger.logger.info(
+            "Semantics was successfully extracted from %s", tarname)
+
+    contractpath = os.path.join(targetpath, "chc_contracts")
+
+    capp = CApplication(
+        projectpath, projectname, targetpath, contractpath, singlefile=True)
+
+    capp.initialize_single_file(cfilename)
+    cfile = capp.get_cfile()
+
+    am = AnalysisManager(capp)
+
+    am.create_file_primary_proofobligations(cfilename)
+    am.reset_tables(cfile)
+    capp.collect_post_assumes()
+
+    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, None, "llrvisp")
+        am.reset_tables(cfile)
+
+    chklogger.logger.info("cfile analyze completed")
+
+    capp = CApplication(
+        projectpath, projectname, targetpath, contractpath, singlefile=True)
+    capp.initialize_single_file(cfilename)
+    cfile = capp.get_cfile()
+
+    if jsonoutput:
+        jsonresult = JU.file_proofobligations_to_json_result(cfile)
+        if jsonresult.is_ok:
+            jsonokresult = JU.jsonok("fileproofobligations", jsonresult.content)
+            if outputfile:
+                with open(outputfile + ".json", "w") as fp:
+                    json.dump(jsonokresult, fp, indent=2)
+            else:
+                print(json.dumps(jsonokresult, indent=2))
+        exit(0)
+
+    def pofilter(po: "CFunctionPO") -> bool:
+        if copen:
+            return not po.is_closed
+        else:
+            return True
+
+    if cshowcode:
+        print(RP.file_code_tostring(cfile, pofilter=pofilter))
+
+    print(RP.file_proofobligation_stats_tostring(cfile))
+    exit(0)
+
+
 def cfile_investigate_file(args: argparse.Namespace) -> NoReturn:
     """Shows a list of open, delegated, and violated proof obligations.
 

chc/cmdline/chkc

@@ -726,6 +726,44 @@ def parse() -> argparse.Namespace:
 
     cfilereport.set_defaults(func=C.cfile_report_file)
 
+    # --- run
+    cfilerun = cfileparsers.add_parser("run")
+    cfilerun.add_argument(
+        "filename",
+        help="name of file to be analyzed (<cpath/>)<cfilename>)")
+    cfilerun.add_argument(
+        "--tgtpath",
+        help="directory to store the analysis results")
+    cfilerun.add_argument(
+        "--showcode",
+        action="store_true",
+        help="show proof obligations on code for entire file")
+    cfilerun.add_argument(
+        "--open",
+        action="store_true",
+        help="only show open proof obligations")
+    cfilerun.add_argument(
+        "--json",
+        action="store_true",
+        help="output results in json format")
+    cfilerun.add_argument(
+        "--output", "-o",
+        help="name of outputfile (without extension)")
+    cfilerun.add_argument(
+        "--loglevel", "-log",
+        choices=UL.LogLevel.options(),
+        default="NONE",
+        help="activate logging with given level (default to stderr)")
+    cfilerun.add_argument(
+        "--logfilename",
+        help="name of file to write log messages")
+    cfilerun.add_argument(
+        "--logfilemode",
+        choices=["a", "w"],
+        default="a",
+        help="file mode for log file: append (a, default), or write (w)")
+    cfilerun.set_defaults(func=C.cfile_run_file)
+
     # --- investigate
     cfileinvestigate = cfileparsers.add_parser("investigate")
     cfileinvestigate.add_argument(