Source code for chc.cmdline.chkc

#!/usr/bin/env python3
# ------------------------------------------------------------------------------
# CodeHawk C Analyzer
# Author: Henny Sipma
# ------------------------------------------------------------------------------
# The MIT License (MIT)
#
# 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
# in the Software without restriction, including without limitation the rights
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
# copies of the Software, and to permit persons to whom the Software is
# furnished to do so, subject to the following conditions:
#
# The above copyright notice and this permission notice shall be included in all
# copies or substantial portions of the Software.
#
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
# 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.

The CodeHawk C Analyzer is a sound static analysis tool that attempts to prove
the absence of undefined behavior. It does so by generating a comprehensive set
of proof obligations that capture all conditions that can lead to undefined
behavior and attempts to prove that the negation of those conditions is valid,
that is true for all inputs. The status of these proof obligations can then
be inspected via various reports.

The CodeHawk-C analyzer calls two executables from the codehawk repository
that perform the parsing and analysis. To check if these two executables are
available, you can run:

- chkc info

Analysis commands are provided for two distinct ways of analysis:

- chkc c-file .... analyzes a single source file (that can be parsed by gcc)
- chkc c-project ...
             analyzes a project of multiple files that comes with a Makefile

Run the respective option for more information on either one.
"""

import argparse
import json
import os
import subprocess
import sys

from typing import NoReturn

from chc.app.CHVersion import chcversion

import chc.cmdline.c_file.cfileutil as C
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

from chc.util.Config import Config
import chc.util.loggingutil as UL


[docs]def showversion(args: argparse.Namespace) -> NoReturn: print("CodeHawk-C Analyzer (python) Version: " + chcversion) config = Config() canalyzer = config.canalyzer cmd = [canalyzer, "version"] subprocess.call(cmd, stderr=subprocess.STDOUT) exit(0)
[docs]def showinfo(args: argparse.Namespace) -> NoReturn: print(str(Config())) exit(0)
[docs]def cfilecommand(args: argparse.Namespace) -> NoReturn: descr = """ The chkc c-file set of commands is used to analyze a single file. The regular sequence of commands is: > chkc c-file parse <cfilename>.c This command will call gcc to preprocess the file and produce an .i file. Then the CodeHawk/CIL parser is called to convert the preprocessed file into OCaml data structures for further analysis. The data structures are stored in xml_format in (by default) the directory <cfilename>.cch . The command > chkc c-file analyze <cfilename>.c loads the data structures and generates proof obligations, and then generates invariants, using abstract interpretation, to be used to discharge the proof obligations. This is repeated (by default) 5 times. The analysis results are stored in xml-form in the same directory. The command > chkc c-file report <cfilename>.c produces a (text or json) report of the proof obligations proven and those that could not be proven, with some additional information why they could not be proven that may be helpful in either fixing the code or providing additional assumptions on the code. """ print(descr) exit(0)
[docs]def cfile_filetable_command(args: argparse.Namespace) -> NoReturn: descr = """ The chkc c-file file-table set of commands is used to inspect a table of indexed values created by the analyzer for each file to communicate results back and forth between the ocaml and python components of the analyzer. File tables available: - api-param : function api parameters - attrparam : attribute parameters - attribute : attributes of variables and types - attributes : attribute lists - cfg-context : structural representations of locations relative to cfg - compinfo : struct/union data structures - constant : constants used throughout the c-file - enuminfo : enumeration data types - enumitem : enumeration data type items - exp : C expressions - exp-context : structural representations of expression locations - fieldinfo : struct/union field information - funarg : function arguments - funargs : function arguments lists - initinfo : global variable initializers - lhost : base left-hand-side values - location : program locations - lval : left-hand-side values - offset : memory offsets - offsetinto : offsets in global initializers - po-predicate : proof-obligation predicates - post-assume : assumptions on post conditions - post-request : requests for post conditions - program-context: structural representations of program locations - s-offset : offsets in external expressions - s-term : terms in external expressions - typeinfo : type definitions - typsig : attribute type signatures - typsiglist : attribute type signatures lists - varinfo : global/local variable information - xpredicate : external predicates """ print(descr) exit(0)
[docs]def cfile_functiontable_command(args: argparse.Namespace) -> NoReturn: descr = """ The chkc c-file function-table set of commands is used to inspect a table of indexed values created by the analyzer for each function to communicate results back and forth between the ocaml and python components of the analyzer. Function tables available: - assumption-type : expressions used as assumptions - constant-value-variable: C analysis variables that are constant in a function - invariant-fact : invariant expressions - memory-base : C analysis memory base values - memory-reference : C analysis memory reference values - non-relational-value : single-variable invariant values - numerical : CHIF numerical values - ppo-type : primary proof obligations - spo-type : supporting proof obligations - symbol : CHIF symbols - variable : CHIF variables - variable-denotation : C analysis variables - varinfo : global/local C variables used within a function - xconstant : xpr constants - xpr : xpr expressions - xpr-list : lists of xpr expressions - xpr-list-list : lists of lists of xpr expressions """ print(descr) exit(0)
[docs]def cprojectcommand(args: argparse.Namespace) -> NoReturn: descr = """ The chkc c-project set of commands is used to analyze a c project, which is assumed to come with a Makefile. The regular sequence of commands is: > chkc c-project parse <path> This command expects to find a compile_commands.json file in <path> that can be rerun to build the project. (Some projects create this file as part of the regular build process, alternatively it can be created by utilities like 'bear'). The directory is expected to be in a state where the commands in compile_commands.json can be rerun. The compile_commands.json file is modified to emit preprocessed source files (.i files). These .i files are parsed by the CodeHawk parser (powered by goblint CIL) to produce ocaml data structures for all data and function declarations and definitions in all source files. These artifacts are saved in a gzipped tar archive for further analysis. """ print(descr) exit(0)
[docs]def julietcommand(args: argparse.Namespace) -> NoReturn: descr = """ The chkc juliet set of commands is used to analyze the juliet test suite cases provided in https://github.com/static-analysis-engineering/CodeHawk-C-Targets-Juliet All commands in the juliet collection of commands assume that a pointer to the location of these (pre-parsed) tests is configured in util/Config.py or in util/ConfigLocal.py. To check wheter this is the case, run > chkc juliet check_config It should show the analyzer configuration and the location of the juliet test case index file. The command > chkc juliet list lists the individual test cases provided with the date/time the analyzer was last run on this test, and the date/time when the results were compared with the accompanying scoring key. The command > chkc juliet analyze <cwe> <test> (e.g., CWE121 char_type_overrun_memcpy) runs the analysis on a juliet test. An individual juliet test typically consists of 18-60 files. Analysis of all of these files can be run in parallel with the optional commandline option --maxprocesses <n> where <n> is the number of processors to be applied. A summary of the results is saved in the file summaryresults.json for later reference. Detailed results are saved in the .cch/a directory, as usual. The command > chkc juliet analyze-sets can be used to automatically run all (or a subset) of the juliet tests provided. In this case parallelism is applied to the sets, rather than to the individual files within a set. The commands below can be run only on tests that have already been analyzed. The command > chkc juliet report <cwe> <test> outputs a summary of the proof obligation analysis statistics for the given test. The command > chkc juliet report-file <cwe> <test> <filename> (e.g., x01.c) outputs the original source code annotated with the proof obligations and their analysis results for each line of code for the given source file, as well as the proof obligation analysis statistics for that source file. The command > chkc juliet score <cwe> <test> compares the analysis results the given test with the expected analysis, as provided by the scorekey.json file that comes with each test. The command > chkc juliet investigate <cwe> <test> outputs the list of open/violated/delegated proof obligations, together with their dependencies and diagnostics for the given test. """ print(descr) exit(0)
[docs]def parse() -> argparse.Namespace: parser = argparse.ArgumentParser( formatter_class=argparse.RawDescriptionHelpFormatter, description=__doc__, epilog="See for more information ...") if len(sys.argv) == 1: parser.print_help(sys.stderr) exit(0) subparsers = parser.add_subparsers(title="subcommands") parser_info = subparsers.add_parser("info") parser_info.set_defaults(func=showinfo) parser_version = subparsers.add_parser("version") parser_version.set_defaults(func=showversion) # --------------------------------------------------------------- kendra --- kendracmd = subparsers.add_parser("kendra") kendraparsers = kendracmd.add_subparsers(title="show options") # --- kendra list kendralist = kendraparsers.add_parser("list") kendralist.set_defaults(func=K.kendra_list) # --- kendra show-set kendrashowset = kendraparsers.add_parser("show-set") kendrashowset.add_argument( "testset", help="name of test directory (e.g., id115Q)") kendrashowset.set_defaults(func=K.kendra_show_set) # --- kendra clean-set kendracleanset = kendraparsers.add_parser("clean-set") kendracleanset.add_argument( "testset", help="name of test directory (e.g., id115Q)") kendracleanset.set_defaults(func=K.kendra_clean_set) # --- kendra test-set kendratestset = kendraparsers.add_parser("test-set") kendratestset.add_argument( "testset", help="name of test directory (e.g., id115Q)") kendratestset.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), default="WARNING", help="activate logging with given level (default to stderr)") kendratestset.add_argument( "--logfilename", help="name of file to write log messages (default is <testset>_log.txt)") kendratestset.add_argument( "--logfilemode", choices=["a", "w"], default="a", help="file mode for log file: append (a, default), or write (w)") kendratestset.add_argument( "--verbose", "-v", help="print verbose output", action="store_true") kendratestset.set_defaults(func=K.kendra_test_set) # --- kendra test-sets kendratestsets = kendraparsers.add_parser("test-sets") kendratestsets.add_argument( "--verbose", "-v", help="print_verbose_output", action="store_true") kendratestsets.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), default="WARNING", help="activate logging with given level (default to stderr)") kendratestsets.add_argument( "--logfilename", help="name of file to write log messages (default is <testset>_log.txt)") kendratestsets.add_argument( "--logfilemode", choices=["a", "w"], default="a", help="file mode for log file: append (a, default), or write (w)") kendratestsets.set_defaults(func=K.kendra_test_sets) # --- kendra dashboard kendradashboard = kendraparsers.add_parser("dashboard") kendradashboard.set_defaults(func=K.kendra_dashboard) # --- kendra report-file kendrareportfile = kendraparsers.add_parser("report-file") kendrareportfile.add_argument( "cfilename", help="name of kendra c file (e.g., id115.c)") kendrareportfile.add_argument( "--show_invariants", help="show invariants at each line in the source code", action="store_true") kendrareportfile.set_defaults(func=K.kendra_report_file) # --- kendra show-file-table kendrashowfiletable = kendraparsers.add_parser("show-file-table") kendrashowfiletable.add_argument( "cfilename", help="name of kendra c file (e.g., id115.c)") kendrashowfiletable.add_argument( "tablename", help="name of table") kendrashowfiletable.set_defaults(func=K.kendra_show_file_table) # --- kendra show-function-table kendrashowfunctiontable = kendraparsers.add_parser("show-function-table") kendrashowfunctiontable.add_argument( "cfilename", help="name of kendra c file (e.g., id115.c)") kendrashowfunctiontable.add_argument( "functionname", help="name of function in c file (e.g., main)") kendrashowfunctiontable.add_argument( "tablename", help="name of table") kendrashowfunctiontable.set_defaults(func=K.kendra_show_function_table) # --------------------------------------------------------------- juliet --- julietcmd = subparsers.add_parser("juliet") julietcmd.set_defaults(func=julietcommand) julietparsers = julietcmd.add_subparsers(title="show options") # --- check-config julietconfig = julietparsers.add_parser("check-config") julietconfig.set_defaults(func=J.juliet_check_config) # --- list julietlist = julietparsers.add_parser("list") julietlist.add_argument("--cwe", help="only list tests for CWE") julietlist.set_defaults(func=J.juliet_list) # --- convert julietconvert = julietparsers.add_parser("convert") julietconvert.add_argument("cwe", help="name of cwe, e.g., CWE121") julietconvert.add_argument( "test", help="name of test case, e.g., CWE129_large") julietconvert.add_argument( "targetpath", help="directory in which to store converted set") julietconvert.set_defaults(func=J.juliet_convert) # --- analyze julietanalyze = julietparsers.add_parser("analyze") julietanalyze.add_argument("cwe", help="name of cwe, e.g., CWE121") julietanalyze.add_argument( "test", help="name of test case, e.g., CWE129_large") julietanalyze.add_argument( "--maxprocesses", help="number of files to process in parallel", type=int, default=1) julietanalyze.add_argument( "--analysisrounds", help="number of times to generate supporting proof obligations", type=int, default=5) julietanalyze.add_argument( "--wordsize", help="architecture word size in bits", type=int, default=64) julietanalyze.add_argument( "--contractpath", help="path to save the contracts file", default=None) julietanalyze.add_argument( "--verbose", "-v", action="store_true", help="show output from ocaml analyzer") julietanalyze.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), default="WARNING", help="activate logging with given level (default to stderr)") julietanalyze.add_argument( "--logfilename", help="name of file to write log messages (default is <testset>_log.txt)") julietanalyze.add_argument( "--logfilemode", choices=["a", "w"], default="a", help="file mode for log file: append (a, default), or write (w)") julietanalyze.set_defaults(func=J.juliet_analyze) # --- analyze-sets julietanalyzesets = julietparsers.add_parser("analyze-sets") julietanalyzesets.add_argument( "--maxprocesses", help="maximum number of processors to use", type=int, default=1) julietanalyzesets.add_argument( "--cwes", nargs="*", help="restrict analysis to these cwe's (default is all)", default=[]) julietanalyzesets.set_defaults(func=J.juliet_analyze_sets) # --- report julietreport = julietparsers.add_parser("report") julietreport.add_argument("cwe", help="name of cwe, e.g., CWE121") julietreport.add_argument( "test", help="name of test case, e.g., CWE129_large") julietreport.set_defaults(func=J.juliet_report) # --- report-file julietreportfile = julietparsers.add_parser("report-file") julietreportfile.add_argument("cwe", help="name of cwe, e.g., CWE121") julietreportfile.add_argument( "test", help="name of test case, e.g., CWE129_large") julietreportfile.add_argument( "filename", help="name of c file, e.g., x01.c") julietreportfile.add_argument( "--showcode", action="store_true", help="show the proof obligations on the code") julietreportfile.add_argument( "--open", action="store_true", help="show only open proof obligations on the code") julietreportfile.add_argument( "--showinvariants", action="store_true", help="show invariants for open proof obligations") julietreportfile.set_defaults(func=J.juliet_report_file) # --- score julietscore = julietparsers.add_parser("score") julietscore.add_argument("cwe", help="name of cwe, e.g., CWE121") julietscore.add_argument( "test", help="name of test case, e.g., CWE129_large") julietscore.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), default="WARNING", help="activate logging with given level (default to stderr)") julietscore.add_argument( "--logfilename", help="name of file to write log messages (default is <testset>_log.txt)") julietscore.add_argument( "--logfilemode", choices=["a", "w"], default="a", help="file mode for log file: append (a, default), or write (w)") julietscore.set_defaults(func=J.juliet_score) # --- score-sets julietscoresets = julietparsers.add_parser("score-sets") julietscoresets.add_argument( "--maxprocesses", type=int, default=1, help="maximum number of processors to use") julietscoresets.add_argument( "--cwes", nargs="*", default=[], help="only score the tests with the given cwe's (default is all)") julietscoresets.set_defaults(func=J.juliet_score_sets) # --- investigate julietinvestigate = julietparsers.add_parser("investigate") julietinvestigate.add_argument("cwe", help="name of cwe, e.g., CWE121") julietinvestigate.add_argument( "test", help="name of test case, e.g., CWE129_large") julietinvestigate.add_argument( "--xdelegated", help="exclude delegated proof obligations", action="store_true") julietinvestigate.add_argument( "--xviolated", help="exclude violated proof obligations", action="store_true") julietinvestigate.add_argument( "--predicates", nargs="*", help="predicates of interest (default: all)", default=[]) julietinvestigate.set_defaults(func=J.juliet_investigate) # --- report-requests julietreprequests = julietparsers.add_parser("report-requests") julietreprequests.add_argument("cwe", help="name of cwe, e.g., CWE121") julietreprequests.add_argument( "test", help="name of test case, e.g., CWE129_large") julietreprequests.set_defaults(func=J.juliet_report_requests) # --- dashboard julietdashboard = julietparsers.add_parser("dashboard") julietdashboard.add_argument( "--cwe", help="only report results on the given cwe") julietdashboard.add_argument( "--variant", help="only report results on the given variant") julietdashboard.set_defaults(func=J.juliet_dashboard) # --- project-dashboard julietpdashboard = julietparsers.add_parser("project-dashboard") julietpdashboard.add_argument( "--cwe", help="only report results on the given cwe") julietpdashboard.set_defaults(func=J.juliet_project_dashboard) # --------------------------------------------------------------- c-file --- cfilecmd = subparsers.add_parser("c-file") cfilecmd.set_defaults(func=cfilecommand) cfileparsers = cfilecmd.add_subparsers(title="show options") # --- parse cfileparse = cfileparsers.add_parser( "parse", usage=""" Call with the name of c file to be parsed. Example: > chkc c-file parse myfile.c The parse results will be saved in the subdirectory myfile.cch. To save the parse results in a different directory, say myresults, call with the additional argument --tgtpath: > chkc c-file parse myfile --tgtpath myresults Note: the directory passed to tgtpath must exist """) cfileparse.add_argument( "filename", help="name of file to parse ((<cpath/>)<cfilename>)") cfileparse.add_argument( "--tgtpath", help=("directory in which to store the analysis artifacts " + "(default: <cpath>)")) cfileparse.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), default="NONE", help="activate logging with given level (default to stderr)") cfileparse.add_argument( "--logfilename", help="name of file to write log messages") cfileparse.add_argument( "--logfilemode", choices=["a", "w"], default="a", help="file mode for log file: append (a, default), or write (w)") cfileparse.set_defaults(func=C.cfile_parse_file) # --- analyze cfileanalyze = cfileparsers.add_parser("analyze") cfileanalyze.add_argument( "filename", help="name of file to analyze ((<cpath/>)<cfilename>)") cfileanalyze.add_argument( "--tgtpath", help="directory in which to store the analysis artifacts " + "(default: <cpath>)") cfileanalyze.add_argument( "--wordsize", type=int, default=32, help="architecture wordsize in bits (16, 32, or 64)") cfileanalyze.add_argument( "--verbose", "-v", action="store_true", help="print intermediate results") cfileanalyze.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), default="NONE", help="activate logging with given level (default to stderr)") cfileanalyze.add_argument( "--logfilename", help="name of file to write log messages") cfileanalyze.add_argument( "--logfilemode", choices=["a", "w"], default="a", help="file mode for log file: append (a, default), or write (w)") cfileanalyze.set_defaults(func=C.cfile_analyze_file) # --- report cfilereport = cfileparsers.add_parser("report") cfilereport.add_argument( "filename", help="name of file to analyze ((<cpath/>)<cfilename>)") cfilereport.add_argument( "--tgtpath", help="directory that holds the analysis results") cfilereport.add_argument( "--showcode", action="store_true", help="show proof obligations on code for entire file") cfilereport.add_argument( "--functions", nargs="*", help="restrict output to function names listed (defualt: all)") cfilereport.add_argument( "--open", action="store_true", help="only show open proof obligations") cfilereport.add_argument( "--json", action="store_true", help="output results in json format") cfilereport.add_argument( "--output", "-o", help="name of outputfile (without extension)") cfilereport.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), default="NONE", help="activate logging with given level (default to stderr)") cfilereport.add_argument( "--logfilename", help="name of file to write log messages") cfilereport.add_argument( "--logfilemode", choices=["a", "w"], default="a", help="file mode for log file: append (a, default), or write (w)") cfilereport.set_defaults(func=C.cfile_report_file) # --- investigate cfileinvestigate = cfileparsers.add_parser("investigate") cfileinvestigate.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfileinvestigate.add_argument( "--tgtpath", help="directory that holds the analysis results") cfileinvestigate.add_argument( "--predicates", nargs="*", help="names of predicates of interest, e.g., not-null (default: all") cfileinvestigate.add_argument( "--referrals", action="store_true", help="show diagnostics with a domain referral") cfileinvestigate.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), default="NONE", help="activate logging with given level (default to stderr)") cfileinvestigate.add_argument( "--logfilename", help="name of file to write log messages") cfileinvestigate.add_argument( "--logfilemode", choices=["a", "w"], default="a", help="file mode for log file: append (a, default), or write (w)") cfileinvestigate.set_defaults(func=C.cfile_investigate_file) # --- test libc summary cfiletestlibc = cfileparsers.add_parser("test-libc-summary") cfiletestlibc.add_argument( "header", help="name of header file, e.g., time") cfiletestlibc.add_argument( "function", help="name of function, e.g., localtime") cfiletestlibc.add_argument( "--showcode", action="store_true", help="show proof obligations and results on code") cfiletestlibc.add_argument( "--open", action="store_true", help="only show open proof obligations on code") cfiletestlibc.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), default="NONE", help="activate logging with given level (default to stderr)") cfiletestlibc.add_argument( "--logfilename", help="name of file to write log messages") cfiletestlibc.add_argument( "--logfilemode", choices=["a", "w"], default="a", help="file mode for log file: append (a, default), or write (w)") cfiletestlibc.set_defaults(func=C.cfile_testlibc_summary) # --- show globals cfileshowglobals = cfileparsers.add_parser("show-globals") cfileshowglobals.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfileshowglobals.add_argument( "--tgtpath", help="name of directory that holds the analysis results") cfileshowglobals.set_defaults(func=C.cfile_showglobals) # --- file-table cfilefiletablescmd = cfileparsers.add_parser("file-table") cfilefiletablescmd.set_defaults(func=cfile_filetable_command) cfiletablesparsers = cfilefiletablescmd.add_subparsers(title="show options") # --- file-table: attrparam cfile_attrparamtable = cfiletablesparsers.add_parser("attrparam") cfile_attrparamtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_attrparamtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_attrparamtable.set_defaults(func=CT.cfile_attrparam_table) # --- file-table: attribute cfile_attributetable = cfiletablesparsers.add_parser("attribute") cfile_attributetable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_attributetable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_attributetable.set_defaults(func=CT.cfile_attribute_table) # --- file-table: attributes cfile_attributestable = cfiletablesparsers.add_parser("attributes") cfile_attributestable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_attributestable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_attributestable.set_defaults(func=CT.cfile_attributes_table) # --- file-table: constant cfile_constanttable = cfiletablesparsers.add_parser("constant") cfile_constanttable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_constanttable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_constanttable.set_defaults(func=CT.cfile_constant_table) # --- file-table: exp cfile_exptable = cfiletablesparsers.add_parser("exp") cfile_exptable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_exptable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_exptable.set_defaults(func=CT.cfile_exp_table) # --- file-table: funarg cfile_funargtable = cfiletablesparsers.add_parser("funarg") cfile_funargtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_funargtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_funargtable.set_defaults(func=CT.cfile_funarg_table) # --- file-table: funargs cfile_funargstable = cfiletablesparsers.add_parser("funargs") cfile_funargstable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_funargstable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_funargstable.set_defaults(func=CT.cfile_funargs_table) # --- file-table: lhost cfile_lhosttable = cfiletablesparsers.add_parser("lhost") cfile_lhosttable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_lhosttable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_lhosttable.set_defaults(func=CT.cfile_lhost_table) # --- file-table: lval cfile_lvaltable = cfiletablesparsers.add_parser("lval") cfile_lvaltable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_lvaltable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_lvaltable.set_defaults(func=CT.cfile_lval_table) # --- file-table: offset cfile_offsettable = cfiletablesparsers.add_parser("offset") cfile_offsettable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_offsettable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_offsettable.set_defaults(func=CT.cfile_offset_table) # --- file-table: typ cfile_typtable = cfiletablesparsers.add_parser("typ") cfile_typtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_typtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_typtable.set_defaults(func=CT.cfile_typ_table) # --- file-table: typsig cfile_typsigtable = cfiletablesparsers.add_parser("typsig") cfile_typsigtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_typsigtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_typsigtable.set_defaults(func=CT.cfile_typsig_table) # --- file-table: typsiglist cfile_typsiglisttable = cfiletablesparsers.add_parser("typsig-list") cfile_typsiglisttable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_typsiglisttable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_typsiglisttable.set_defaults(func=CT.cfile_typsiglist_table) # --- file table: compinfo cfile_compinfotable = cfiletablesparsers.add_parser("compinfo") cfile_compinfotable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_compinfotable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_compinfotable.set_defaults(func=CT.cfile_compinfo_table) # --- file table: enuminfo cfile_enuminfotable = cfiletablesparsers.add_parser("enuminfo") cfile_enuminfotable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_enuminfotable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_enuminfotable.set_defaults(func=CT.cfile_enuminfo_table) # --- file table: enumitem cfile_enumitemtable = cfiletablesparsers.add_parser("enumitem") cfile_enumitemtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_enumitemtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_enumitemtable.set_defaults(func=CT.cfile_enumitem_table) # --- file table: fieldinfo cfile_fieldinfotable = cfiletablesparsers.add_parser("fieldinfo") cfile_fieldinfotable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_fieldinfotable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_fieldinfotable.set_defaults(func=CT.cfile_fieldinfo_table) # --- file table: initinfo cfile_initinfotable = cfiletablesparsers.add_parser("initinfo") cfile_initinfotable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_initinfotable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_initinfotable.set_defaults(func=CT.cfile_initinfo_table) # --- file table: location cfile_locationtable = cfiletablesparsers.add_parser("location") cfile_locationtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_locationtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_locationtable.set_defaults(func=CT.cfile_location_table) # --- file table: offsetinfo cfile_offsetinfotable = cfiletablesparsers.add_parser("offsetinfo") cfile_offsetinfotable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_offsetinfotable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_offsetinfotable.set_defaults(func=CT.cfile_offsetinfo_table) # --- file table: typeinfo cfile_typeinfotable = cfiletablesparsers.add_parser("typeinfo") cfile_typeinfotable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_typeinfotable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_typeinfotable.set_defaults(func=CT.cfile_typeinfo_table) # --- file table: varinfo cfile_varinfotable = cfiletablesparsers.add_parser("varinfo") cfile_varinfotable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_varinfotable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_varinfotable.set_defaults(func=CT.cfile_varinfo_table) # --- file table: program-context cfile_pcontexttable = cfiletablesparsers.add_parser("program-context") cfile_pcontexttable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_pcontexttable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_pcontexttable.set_defaults(func=CT.cfile_pcontext_table) # --- file table: exp-context cfile_expcontexttable = cfiletablesparsers.add_parser("exp-context") cfile_expcontexttable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_expcontexttable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_expcontexttable.set_defaults(func=CT.cfile_expcontext_table) # --- file table: cfg-context cfile_cfgcontexttable = cfiletablesparsers.add_parser("cfg-context") cfile_cfgcontexttable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_cfgcontexttable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_cfgcontexttable.set_defaults(func=CT.cfile_cfgcontext_table) # --- file table: api-param cfile_apiparamtable = cfiletablesparsers.add_parser("api-param") cfile_apiparamtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_apiparamtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_apiparamtable.set_defaults(func=CT.cfile_apiparam_table) # --- file table: post-assume cfile_postassumetable = cfiletablesparsers.add_parser("post-assume") cfile_postassumetable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_postassumetable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_postassumetable.set_defaults(func=CT.cfile_postassume_table) # --- file table: post-request cfile_postrequesttable = cfiletablesparsers.add_parser("post-request") cfile_postrequesttable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_postrequesttable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_postrequesttable.set_defaults(func=CT.cfile_postrequest_table) # --- file table: sterm cfile_stermtable = cfiletablesparsers.add_parser("s-term") cfile_stermtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_stermtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_stermtable.set_defaults(func=CT.cfile_sterm_table) # --- file table: soffset cfile_soffsettable = cfiletablesparsers.add_parser("s-offset") cfile_soffsettable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_soffsettable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_soffsettable.set_defaults(func=CT.cfile_soffset_table) # --- file table: xpredicate cfile_xpredtable = cfiletablesparsers.add_parser("xpredicate") cfile_xpredtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_xpredtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_xpredtable.set_defaults(func=CT.cfile_xpred_table) # --- file table: po-predicate cfile_predicatetable = cfiletablesparsers.add_parser("po-predicate") cfile_predicatetable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_predicatetable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_predicatetable.set_defaults(func=CT.cfile_predicate_table) # --- function-table cfilefntablescmd = cfileparsers.add_parser("function-table") cfilefntablescmd.set_defaults(func=cfile_functiontable_command) cfilefntablesparsers = cfilefntablescmd.add_subparsers(title="show options") # --- function table: numerical cfile_numericaltable = cfilefntablesparsers.add_parser("numerical") cfile_numericaltable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_numericaltable.add_argument( "function", help="name of function of interest") cfile_numericaltable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_numericaltable.set_defaults(func=CT.cfile_numerical_table) # --- function table: symbol cfile_symboltable = cfilefntablesparsers.add_parser("symbol") cfile_symboltable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_symboltable.add_argument( "function", help="name of function of interest") cfile_symboltable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_symboltable.set_defaults(func=CT.cfile_symbol_table) # --- function table: variable cfile_variabletable = cfilefntablesparsers.add_parser("variable") cfile_variabletable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_variabletable.add_argument( "function", help="name of function of interest") cfile_variabletable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_variabletable.set_defaults(func=CT.cfile_variable_table) # --- function table: xcst cfile_xcsttable = cfilefntablesparsers.add_parser("xconstant") cfile_xcsttable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_xcsttable.add_argument( "function", help="name of function of interest") cfile_xcsttable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_xcsttable.set_defaults(func=CT.cfile_xcst_table) # --- function table: xpr cfile_xprtable = cfilefntablesparsers.add_parser("xpr") cfile_xprtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_xprtable.add_argument( "function", help="name of function of interest") cfile_xprtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_xprtable.set_defaults(func=CT.cfile_xpr_table) # --- function table: xpr-list cfile_xprlisttable = cfilefntablesparsers.add_parser("xpr-list") cfile_xprlisttable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_xprlisttable.add_argument( "function", help="name of function of interest") cfile_xprlisttable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_xprlisttable.set_defaults(func=CT.cfile_xprlist_table) # --- function table: xpr-list-list cfile_xprlistlisttable = cfilefntablesparsers.add_parser("xpr-list-list") cfile_xprlistlisttable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_xprlistlisttable.add_argument( "function", help="name of function of interest") cfile_xprlistlisttable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_xprlistlisttable.set_defaults(func=CT.cfile_xprlistlist_table) # --- function table: membase cfile_membasetable = cfilefntablesparsers.add_parser("memory-base") cfile_membasetable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_membasetable.add_argument( "function", help="name of function of interest") cfile_membasetable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_membasetable.set_defaults(func=CT.cfile_membase_table) # --- function table: membase cfile_membasetable = cfilefntablesparsers.add_parser("memory-base") cfile_membasetable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_membasetable.add_argument( "function", help="name of function of interest") cfile_membasetable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_membasetable.set_defaults(func=CT.cfile_membase_table) # --- function table: memref cfile_memreftable = cfilefntablesparsers.add_parser("memory-reference") cfile_memreftable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_memreftable.add_argument( "function", help="name of function of interest") cfile_memreftable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_memreftable.set_defaults(func=CT.cfile_memref_table) # --- function table: constant-value-variable cfile_cvvtable = cfilefntablesparsers.add_parser("constant-value-variable") cfile_cvvtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_cvvtable.add_argument( "function", help="name of function of interest") cfile_cvvtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_cvvtable.set_defaults(func=CT.cfile_cvv_table) # --- function table: variable-denotation cfile_cvdtable = cfilefntablesparsers.add_parser("variable-denotation") cfile_cvdtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_cvdtable.add_argument( "function", help="name of function of interest") cfile_cvdtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_cvdtable.set_defaults(func=CT.cfile_cvd_table) # --- function table: varinfo cfile_fnvarinfotable = cfilefntablesparsers.add_parser("varinfo") cfile_fnvarinfotable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_fnvarinfotable.add_argument( "function", help="name of function of interest") cfile_fnvarinfotable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_fnvarinfotable.set_defaults(func=CT.cfile_fnvarinfo_table) # --- function table: ppo-type cfile_ppotypetable = cfilefntablesparsers.add_parser("ppo-type") cfile_ppotypetable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_ppotypetable.add_argument( "function", help="name of function of interest") cfile_ppotypetable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_ppotypetable.set_defaults(func=CT.cfile_ppotype_table) # --- function table: spo-type cfile_spotypetable = cfilefntablesparsers.add_parser("spo-type") cfile_spotypetable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_spotypetable.add_argument( "function", help="name of function of interest") cfile_spotypetable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_spotypetable.set_defaults(func=CT.cfile_spotype_table) # --- function table: assumption cfile_assumptiontable = cfilefntablesparsers.add_parser("assumption") cfile_assumptiontable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_assumptiontable.add_argument( "function", help="name of function of interest") cfile_assumptiontable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_assumptiontable.set_defaults(func=CT.cfile_assumption_table) # --- function table: non-relational-value cfile_nrvtable = cfilefntablesparsers.add_parser("non-relational-value") cfile_nrvtable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_nrvtable.add_argument( "function", help="name of function of interest") cfile_nrvtable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_nrvtable.set_defaults(func=CT.cfile_nrv_table) # --- function table: invariant-fact cfile_invfacttable = cfilefntablesparsers.add_parser("invariant-fact") cfile_invfacttable.add_argument( "filename", help="name of file analyzed ((<cpath/>)<cfilename>)") cfile_invfacttable.add_argument( "function", help="name of function of interest") cfile_invfacttable.add_argument( "--tgtpath", help="directory that holds the analysis results") cfile_invfacttable.set_defaults(func=CT.cfile_invfact_table) # ------------------------------------------------------------ c-project --- cprojectcmd = subparsers.add_parser("c-project") cprojectcmd.set_defaults(func=cprojectcommand) cprojectparsers = cprojectcmd.add_subparsers(title="show options") # --- parse cprojectparse = cprojectparsers.add_parser( "parse", usage=""" Call with the top directory of the project and the project name Example: chkc c-project parse myprojectdir myprojectname The parse results will be saved in the subdirectory myprojectname.cch To save the parse results in a different directory, say myresults, call with additional argument --tgtpath: chkc c-project parse myprojectdir myprojectname --tgtpath myresults Note: the directory passed to tgtpath must exist. """) cprojectparse.add_argument( "path", help="top directory of c-project (with compile_commands.json)") cprojectparse.add_argument( "projectname", help="name of the project") cprojectparse.add_argument( "--tgtpath", help="directory to save the results") cprojectparse.add_argument( "--loglevel", "-log", choices=UL.LogLevel.options(), default="NONE", help="activate logging with given level (default to stderr)") cprojectparse.add_argument( "--logfilename", help="name of file to write log messages") cprojectparse.add_argument( "--logfilemode", choices=["a", "w"], default="a", help="file mode for log file: append (a, default), or write (w)") cprojectparse.set_defaults(func=P.cproject_parse_project) # --- analyze cprojectanalyze = cprojectparsers.add_parser("analyze") cprojectanalyze.add_argument( "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(), default="NONE", help="activate logging with given level (default to stderr)") cprojectanalyze.add_argument( "--logfilename", help="name of file to write log messages") cprojectanalyze.add_argument( "--logfilemode", choices=["a", "w"], default="a", help="file mode for log file: append (a, default), or write (w)") cprojectanalyze.set_defaults(func=P.cproject_analyze_project) # --- report cprojectreport = cprojectparsers.add_parser("report") cprojectreport.add_argument( "tgtpath", help="directory that contains the analysis results") cprojectreport.add_argument( "projectname", help="name of the project") cprojectreport.set_defaults(func=P.cproject_report) # --- report-file cprojectreportfile = cprojectparsers.add_parser("report-file") cprojectreportfile.add_argument( "tgtpath", help="directory that contains the analysis results") cprojectreportfile.add_argument( "projectname", help="name of the project") cprojectreportfile.add_argument( "filename", help="filename with relative path wrt the project") cprojectreportfile.add_argument( "--showcode", action="store_true", help="show proof obligations on code for entire file") cprojectreportfile.add_argument( "--open", action="store_true", help="only show open proof obligations (or violations)") cprojectreportfile.set_defaults(func=P.cproject_report_file) # --- count-statements cprojectcountstmts = cprojectparsers.add_parser("count-statements") cprojectcountstmts.add_argument( "tgtpath", help="directory that contains the analysis results") cprojectcountstmts.add_argument( "projectname", help="name of the project") cprojectcountstmts.add_argument( "--verbose", "-v", action="store_true", help="show values for individual functions") cprojectcountstmts.set_defaults(func=P.cproject_count_stmts) # --- make-callgraph cprojectcallgraph = cprojectparsers.add_parser("make-callgraph") cprojectcallgraph.add_argument( "tgtpath", help="directory that contains the analysis results") cprojectcallgraph.add_argument( "projectname", help="name of the project") cprojectcallgraph.add_argument( "--save", help="name of file (without extension) to save the results") cprojectcallgraph.set_defaults(func=P.cproject_make_callgraph) # --- missing-summaries cprojectmissingsummaries = cprojectparsers.add_parser("missing-summaries") cprojectmissingsummaries.add_argument( "tgtpath", help="directory that contains the analysis results") cprojectmissingsummaries.add_argument( "projectname", help="name of the project") cprojectmissingsummaries.add_argument( "--all", action="store_true", help="show for all files (including application files)") cprojectmissingsummaries.set_defaults(func=P.cproject_missing_summaries) args = parser.parse_args() return args
if __name__ == "__main__": args = parse() args.func(args)