diff --git a/chc/app/CHVersion.py b/chc/app/CHVersion.py index 58d6793..95dda84 100644 --- a/chc/app/CHVersion.py +++ b/chc/app/CHVersion.py @@ -1 +1 @@ -chcversion: str = "0.2.0-2026-02-26" +chcversion: str = "0.2.0-2026-06-06" diff --git a/chc/cmdline/AnalysisManager.py b/chc/cmdline/AnalysisManager.py index c89f9c4..ab11f54 100644 --- a/chc/cmdline/AnalysisManager.py +++ b/chc/cmdline/AnalysisManager.py @@ -217,9 +217,18 @@ def create_file_primary_proofobligations( self, cfilename: str, cfilepath: Optional[str] = None, - po_cmd: str = "undefined-behavior-primary" - ) -> None: - """Call analyzer to create primary proof obligations for a single file.""" + po_cmd: str = "undefined-behavior-primary", + return_status: bool = False, + chloglevel: str = "WARNING" + ) -> int: + """Call analyzer to create primary proof obligations for a single file. + + If return_status is False this method exits with 1 if the call to the + ocaml analyzer fails. If return_status is True this method always returns + the return status of the ocaml analyzer to the caller. The latter is + typically used for the regression tests, such that subsequent tests will + still be run. + """ chklogger.logger.info( "Create primiary proof obligations for file %s with path %s", @@ -230,6 +239,7 @@ def create_file_primary_proofobligations( cmd.append(cfilename) if cfilepath is not None: cmd.extend(["-cfilepath", cfilepath]) + cmd.extend(["-loglevel", chloglevel]) chklogger.logger.info( "Ocaml analyzer is called with %s", str(cmd)) if self.verbose: @@ -246,6 +256,8 @@ def create_file_primary_proofobligations( ) if result != 0: print("Error in creating primary proof obligations") + if return_status: + return 1 exit(1) pcfilename = ( cfilename if cfilepath is None @@ -255,10 +267,14 @@ def create_file_primary_proofobligations( cfile.reload_ppos() cfile.reload_spos() except subprocess.CalledProcessError as args: + if return_status: + return 1 print(args.output) print(args) exit(1) + return 0 + def create_app_primary_proofobligations( self, po_cmd: str = "undefined-behavior-primary", @@ -332,12 +348,22 @@ def generate_and_check_file( cfilename: str, cfilepath: Optional[str], domains: str, - iteration: int) -> None: - """Generate invariants and check proof obligations for a single file.""" + iteration: int, + return_status=False, + chloglevel: str = "WARNING") -> int: + """Generate invariants and check proof obligations for a single file. + + If return_status is False this method exits with 1 if the call to the + ocaml analyzer fails. If return_status is True this method always returns + the return status of the ocaml analyzer to the caller. The latter is + typically used for the regression tests, such that subsequent tests will + still be run. +""" try: cmd = self._generate_and_check_file_cmd_partial(cfilepath, domains, iteration) cmd.append(cfilename) + cmd.extend(["-loglevel", chloglevel]) chklogger.logger.info( "Calling AI to generate invariants: %s", " ".join(cmd)) @@ -354,14 +380,20 @@ def generate_and_check_file( ) print_status("\nGenerate-and-check: result: " + str(result)) if result != 0: + if return_status: + return 1 chklogger.logger.error( "Error in generating invariants for %s", cfilename) exit(1) except subprocess.CalledProcessError as args: + if return_status: + return 1 print(args.output) print(args) exit(1) + return 0 + def generate_and_check_app(self, domains: str, iteration: int, processes: int = 1) -> None: """Generate invariants and check proof obligations for application.""" diff --git a/chc/cmdline/ParseManager.py b/chc/cmdline/ParseManager.py index 80e3c5b..8472c50 100644 --- a/chc/cmdline/ParseManager.py +++ b/chc/cmdline/ParseManager.py @@ -225,7 +225,9 @@ def preprocess_file_with_cc( self, cfilename: str, copyfiles: bool = True, - moreoptions: List[str] = []) -> str: + moreoptions: List[str] = [], + chloglevel: str = "WARNING" + ) -> str: """Invoke C preprocessor on c source file. Args: @@ -518,7 +520,7 @@ def parse_cfiles(self, copyfiles: bool = True) -> None: targetfiles.add_file(self.normalize_filename(fname)) targetfiles.save_xml_file(self.analysisresultspath) - def parse_ifile(self, ifilename: str) -> int: + def parse_ifile(self, ifilename: str, chloglevel: str = "WARNING") -> int: """Invoke the CodeHawk C parser frontend on preprocessed source file Args: @@ -539,6 +541,7 @@ def parse_ifile(self, ifilename: str) -> int: ] if not self.keep_system_includes: cmd.append("-keep_system_includes") + cmd.extend(["-loglevel", chloglevel]) if self.keepUnused: cmd.append("-keepUnused") cmd.append(ifilename) diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc index 591296c..35b3f10 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -5,7 +5,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2023-2025 Aarno Labs, LLC +# Copyright (c) 2023-2026 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 @@ -64,6 +64,7 @@ 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.cmdline.regression.regressionutil as R from chc.util.Config import Config import chc.util.loggingutil as UL @@ -418,6 +419,30 @@ def parse() -> argparse.Namespace: help="name of table") kendrashowfunctiontable.set_defaults(func=K.kendra_show_function_table) + # ----------------------------------------------------- regression tests --- + + regressioncmd = subparsers.add_parser("regression") + regressionparsers = regressioncmd.add_subparsers(title="show options") + + # --- regression list + regressionlist = regressionparsers.add_parser("list") + regressionlist.set_defaults(func=R.regression_list) + + # --- regression test-file + regressiontestfile = regressionparsers.add_parser("test-file") + regressiontestfile.add_argument( + "cfilename", help="name of testfile to run (e.g., bool_integer_promotion.c)") + regressiontestfile.set_defaults(func=R.regression_test_file) + + # --- regressions run-tests + regressionruntests = regressionparsers.add_parser("run-tests") + regressionruntests.add_argument( + "--loglevel", "-log", + choices=UL.LogLevel.options(), + default="WARNING", + help="activate logging in CHC with given level") + regressionruntests.set_defaults(func=R.regression_run_tests) + # --------------------------------------------------------------- juliet --- julietcmd = subparsers.add_parser("juliet") diff --git a/chc/cmdline/regression/__init__.py b/chc/cmdline/regression/__init__.py new file mode 100644 index 0000000..0a105c3 --- /dev/null +++ b/chc/cmdline/regression/__init__.py @@ -0,0 +1 @@ +"""Support for analyzing the kendra (regression) tests.""" diff --git a/chc/cmdline/regression/regressionutil.py b/chc/cmdline/regression/regressionutil.py new file mode 100644 index 0000000..e397b03 --- /dev/null +++ b/chc/cmdline/regression/regressionutil.py @@ -0,0 +1,245 @@ +# ------------------------------------------------------------------------------ +# CodeHawk C Analyzer +# Author: Henny Sipma +# ------------------------------------------------------------------------------ +# The MIT License (MIT) +# +# Copyright (c) 2026 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 run regression tests.""" + +import argparse +import json +import os +import subprocess +import shutil +import sys + +from typing import Any, Dict, List, NoReturn + +from chc.app.CApplication import CApplication +from chc.cmdline.AnalysisManager import AnalysisManager +from chc.cmdline.ParseManager import ParseManager + +import chc.util.fileutil as UF + + +def print_error(m: str) -> None: + sys.stderr.write(("*" * 80) + "\n") + sys.stderr.write(m + "\n") + sys.stderr.write(("*" * 80) + "\n") + + +def get_tests() -> List[Dict[str, Any]]: + testsfile = UF.get_regression_tests_json_file() + + with open(testsfile, "r") as fp: + return json.load(fp).get("tests", []) + return [] + + +def has_test(cfilename: str) -> bool: + tests = get_tests() + + return any(test.get("filename", "?") == cfilename for test in tests) + + +def get_test(cfilename: str) -> Dict[str, Any]: + for test in get_tests(): + if test.get("filename", "?") == cfilename: + return test + raise UF.CHError("No test found with name " + cfilename) + + +def regression_list(args: argparse.Namespace) -> NoReturn: + + testsfile = UF.get_regression_tests_json_file() + + with open(testsfile, "r") as fp: + testlist = json.load(fp).get("tests", []) + + print("Regression tests listed:") + for testrec in testlist: + print(" - " + testrec.get("filename")) + + exit(0) + + +def run_regression_test_file( + testspec: Dict[str, Any], + loglevel="WARNING") -> str: + + try: + UF.check_parser() + except UF.CHError as e: + print_error(str(e.wrap())) + exit(1) + + cfilename = testspec.get("filename", "?") + + def returnmsg(s: str) -> str: + return cfilename.ljust(32) + "[" + s.ljust(50) + "]" + + pcfile_c = UF.get_regression_testfile_path(cfilename) + projectpath = os.path.dirname(os.path.abspath(pcfile_c)) + targetpath = projectpath + cfilename_c = os.path.basename(pcfile_c) + cfilename = cfilename_c[:-2] + projectname = cfilename + + po_cmd = "undefined-behavior-primary" + analysisdomains = "llrvisp" + + parsemanager = ParseManager(projectpath, projectname, targetpath) + parsemanager.remove_semantics() + parsemanager.initialize_paths() + + try: + cfilename_i = parsemanager.preprocess_file_with_cc(cfilename_c) + result = parsemanager.parse_ifile(cfilename_i, chloglevel=loglevel) + if result != 0: + return returnmsg("Error in parsing") + except OSError as e: + return returnmsg("Failed: Error in parsing: " + str(e)) + + parsemanager.save_semantics() + 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): + shutil.rmtree(cchpath) + + 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) + if result != 0: + return returnmsg("Failed: Error in extracting") + + contractpath = os.path.join(targetpath, "chc_contracts") + + capp = CApplication( + projectpath, + projectname, + targetpath, + contractpath, + singlefile=True, + keep_system_includes=True) + + capp.initialize_single_file(cfilename) + cfile = capp.get_cfile() + + am = AnalysisManager( + capp, + verbose=False, + collectdiagnostics=False, + keep_system_includes=True) + + status = am.create_file_primary_proofobligations( + cfilename, po_cmd=po_cmd, return_status=True, chloglevel=loglevel) + if status != 0: + return returnmsg("Failed in creating primary proof obligations") + am.reset_tables(cfile) + capp.collect_post_assumes() + + status = am.generate_and_check_file( + cfilename, + None, + analysisdomains, + 0, + return_status=True, + chloglevel=loglevel) + if status != 0: + return returnmsg("Failed in generate-and-check (round 0)") + am.reset_tables(cfile) + capp.collect_post_assumes() + + for k in range(5): + capp.update_spos() + status = am.generate_and_check_file( + cfilename, None, analysisdomains, k + 1, return_status=True) + if status != 0: + return returnmsg("Failed in generate-and-check (round " + + str(k + 1) + ")") + am.reset_tables(cfile) + + statusresults: Dict[str, int] = {} + + for fn in cfile.get_functions(): + ppos = fn.get_ppos() + for ppo in ppos: + statusresults.setdefault(ppo.status, 0) + statusresults[ppo.status] += 1 + + expected = testspec.get("expected", {}) + for (s, c) in expected.items(): + if s in statusresults: + if not statusresults[s] == expected[s]: + resultmsg = ( + "Failed: Expected " + s + ":" + str(c) + + ", but found " + s + ":" + str(statusresults[s])) + break + else: + resultmsg = ( + "Failed: Expected " + s + ":" + str(c) + + ", but found none for " + s) + break + + else: + resultmsg = "Passed " + ("." * 43) + + return returnmsg(resultmsg) + + +def regression_test_file(args: argparse.Namespace) -> NoReturn: + + # arguments + cfilename: str = args.cfilename + + if not has_test(cfilename): + print_error("File " + cfilename + " not found") + exit(1) + + run_regression_test_file(get_test(cfilename)) + + exit(0) + + +def regression_run_tests(args: argparse.Namespace) -> NoReturn: + + # arguments + loglevel: str = args.loglevel + + lines: List[str] = [] + for test in get_tests(): + if test.get("status", "pass") == "fail": + continue + lines.append(run_regression_test_file(test, loglevel=loglevel)) + + print("\n".join(lines)) + + exit(0) diff --git a/chc/util/Config.py b/chc/util/Config.py index 162efbc..dfa634d 100644 --- a/chc/util/Config.py +++ b/chc/util/Config.py @@ -6,7 +6,7 @@ # # Copyright (c) 2017-2020 Kestrel Technology LLC # Copyright (c) 2020-2022 Henny Sipma -# Copyright (c) 2023 Aarno Labs LLC +# Copyright (c) 2023-2026 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 @@ -75,6 +75,7 @@ def __init__(self) -> None: # tests included in this repository self.kendradir = os.path.join(self.testdir, "kendra") self.libcsummarytestdir = os.path.join(self.testdir, "libcsummaries") + self.regressiondir = os.path.join(self.testdir, "regression") # analysis targets self.name_separator = ":" diff --git a/chc/util/fileutil.py b/chc/util/fileutil.py index 48c3d43..179e178 100644 --- a/chc/util/fileutil.py +++ b/chc/util/fileutil.py @@ -1573,6 +1573,23 @@ def get_kendra_cpath(cfilename: str) -> str: raise CHCFileNotFoundError(cfilename) +# --------------------------------------------------------- regression tests --- + +def get_regression_test_path() -> str: + return Config().regressiondir + + +def get_regression_testfile_path(filename: str) -> str: + cfilename = os.path.join(get_regression_test_path(), filename) + if os.path.isfile(cfilename): + return cfilename + raise CHCFileNotFoundError(cfilename) + + +def get_regression_tests_json_file() -> str: + return os.path.join(get_regression_test_path(), "tests.json") + + # --------------------------------------------------------libc summary tests --- diff --git a/tests/regression/bool_integer_promotion.c b/tests/regression/bool_integer_promotion.c new file mode 100644 index 0000000..92ae12f --- /dev/null +++ b/tests/regression/bool_integer_promotion.c @@ -0,0 +1,8 @@ +/* Ref Issue #69: https://github.com/static-analysis-engineering/CodeHawk-C/issues/69 */ + +typedef unsigned long UV; + +void grow(UV len, UV offset, _Bool add_one) { + UV bytes = (len + offset + add_one) * sizeof(UV); + (void)bytes; +} diff --git a/tests/regression/enum_integer_promotion.c b/tests/regression/enum_integer_promotion.c new file mode 100644 index 0000000..4caef26 --- /dev/null +++ b/tests/regression/enum_integer_promotion.c @@ -0,0 +1,31 @@ +/* + * Reproducer for a CodeHawk-C integer-promotion failure seen in perlbench + * ext/re/re_exec.c:S_isGCB. + * + * Perl combines two enum values with: + * + * (GCB_ENUM_COUNT * before) + after + * + * The proof checker reconstructs this as arithmetic over int and enum types. + * C's usual arithmetic conversions allow enum operands to participate in + * integer arithmetic, but CH-C's get_integer_promotion only accepted TInt + * operands and failed on int and enum. + * + * Ref Issue #71: https://github.com/static-analysis-engineering/CodeHawk-C/issues/71 + */ + +typedef enum { + GCB_OTHER = 0, + GCB_CR = 1, + GCB_LF = 2, + GCB_ENUM_COUNT = 14 +} GCB_enum; + +int enum_integer_promotion(GCB_enum before, GCB_enum after) { + switch ((GCB_ENUM_COUNT * before) + after) { + case (GCB_ENUM_COUNT * GCB_CR) + GCB_LF: + return 1; + default: + return 0; + } +} diff --git a/tests/regression/imagick-float-arithmetic-po.c b/tests/regression/imagick-float-arithmetic-po.c new file mode 100644 index 0000000..2a0dfb0 --- /dev/null +++ b/tests/regression/imagick-float-arithmetic-po.c @@ -0,0 +1,21 @@ +/* Mirrors the relevant ColorDodge expression from ImageMagick + + Ref Issue #78: https://github.com/static-analysis-engineering/CodeHawk-C/issues/78 +*/ + +typedef double MagickRealType; + +static MagickRealType ColorDodge( + const MagickRealType Sca, + const MagickRealType Sa, + const MagickRealType Dca, + const MagickRealType Da) { + if ((Sca * Da + Dca * Sa) >= Sa * Da) { + return Sa * Da + Sca * (1.0 - Da) + Dca * (1.0 - Sa); + } + return Dca * Sa * Sa / (Sa - Sca) + Sca * (1.0 - Da) + Dca * (1.0 - Sa); +} + +int main(void) { + return ColorDodge(0.1, 0.5, 0.2, 0.7) > 0.0; +} diff --git a/tests/regression/test_POCheckInitialized.c b/tests/regression/test_POCheckInitialized.c new file mode 100644 index 0000000..b9b7482 --- /dev/null +++ b/tests/regression/test_POCheckInitialized.c @@ -0,0 +1,101 @@ +/* Tests for cchanalyze/cCHPOCheckInitialized.ml */ + + +int gl_inv_001(void) { + + int i = 5; + + return i; +} + + +typedef struct mystruct_s { + int fld1; + int fld2; +} mystruct; + + +int gl_inv_002(void) { + + mystruct s = {.fld1 = 5, .fld2 = 3 }; + + return s.fld1; +} + + +int gl_inv_003(int k) { + + int i; + + if (k > 0) { + i = 5; + } else { + i = 3; + } + + return i; +} + + +int gl_inv_bounded_xpr_001(int k) { + + int i; + int *p = &i; + + if (k > 5) { + i = 5; + } else { + i = 3; + } + + return *p; +} + + +int gl_inv_xpr_001(void) { + + int i = 5; + + int *p = &i; + + return *p; +} + + +int gl_inv_xpr_002(void) { + + int i = 5; + + int *p = &i; + + i = 8; + + return *p; +} + + +int gl_inv_xpr_003(void) { + + int i; + + int *p = &i; + + *p = 8; + + return i; +} + + +int gl_stackvar_001(int k) { + + int i; + int *p = &i; + + if (k > 5) { + i = 5; + } else { + i = k; + } + + return *p; +} diff --git a/tests/regression/tests.json b/tests/regression/tests.json new file mode 100644 index 0000000..eb816ce --- /dev/null +++ b/tests/regression/tests.json @@ -0,0 +1,31 @@ +{ + "date": "2026-06-05", + "tests": [ + { + "filename": "bool_integer_promotion.c", + "expected": { + "safe": 10 + } + }, + { + "filename": "enum_integer_promotion.c", + "expected": { + "safe": 8 + } + }, + { + "filename": "imagick-float-arithmetic-po.c", + "expected": { + "safe": 37 + } + }, + { + "filename": "test_POCheckInitialized.c", + "expected": { + "safe": 42, + "open": 5 + }, + "goal": "improve" + } + ] +}