From 023d442f9b1d223382918c7eda670b1cef706282 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?M=C3=A1rton=20Csord=C3=A1s?= Date: Fri, 8 Apr 2022 09:39:08 +0200 Subject: [PATCH] [test] Add tests for z3 functionality --- analyzer/tests/functional/z3/__init__.py | 90 ++++++++++++++++++ analyzer/tests/functional/z3/test_z3.py | 111 ++++++++++++++++++++++ analyzer/tests/projects/suppress/Makefile | 2 +- 3 files changed, 202 insertions(+), 1 deletion(-) create mode 100644 analyzer/tests/functional/z3/__init__.py create mode 100644 analyzer/tests/functional/z3/test_z3.py diff --git a/analyzer/tests/functional/z3/__init__.py b/analyzer/tests/functional/z3/__init__.py new file mode 100644 index 0000000000..550340a2ec --- /dev/null +++ b/analyzer/tests/functional/z3/__init__.py @@ -0,0 +1,90 @@ +# coding=utf-8 +# ------------------------------------------------------------------------- +# +# Part of the CodeChecker project, under the Apache License v2.0 with +# LLVM Exceptions. See LICENSE for license information. +# SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +# +# ------------------------------------------------------------------------- + +""" Setup for the test package z3 capability. """ + + +import os +import shutil +import sys +import uuid + +from libtest import codechecker +from libtest import env +from libtest import project + + +# Test workspace should be initialized in this module. +TEST_WORKSPACE = None + + +def setup_package(): + """Setup the environment for testing z3.""" + + global TEST_WORKSPACE + TEST_WORKSPACE = env.get_workspace('z3') + + # Set the TEST_WORKSPACE used by the tests. + os.environ['TEST_WORKSPACE'] = TEST_WORKSPACE + + test_config = {} + + test_project = 'suppress' + + project_info = project.get_info(test_project) + + # Copy the test project to the workspace. The tests should + # work only on this test project. + test_proj_path = os.path.join(TEST_WORKSPACE, "test_proj") + shutil.copytree(project.path(test_project), test_proj_path) + + project_info['project_path'] = test_proj_path + + test_config['test_project'] = project_info + + # Suppress file should be set here if needed by the tests. + suppress_file = None + + # Skip list file should be set here if needed by the tests. + skip_list_file = None + + # Get an environment which should be used by the tests. + test_env = env.test_env(TEST_WORKSPACE) + + # Create a basic CodeChecker config for the tests, this should + # be imported by the tests and they should only depend on these + # configuration options. + codechecker_cfg = { + 'suppress_file': suppress_file, + 'skip_list_file': skip_list_file, + 'check_env': test_env, + 'workspace': TEST_WORKSPACE, + 'checkers': [] + } + + # Clean the test project, if needed by the tests. + ret = project.clean(test_project) + if ret: + sys.exit(ret) + + test_config['codechecker_cfg'] = codechecker_cfg + + # Export the test configuration to the workspace. + env.export_test_cfg(TEST_WORKSPACE, test_config) + + +def teardown_package(): + """Clean up after the test.""" + + # TODO: If environment variable is set keep the workspace + # and print out the path. + global TEST_WORKSPACE + + print("Removing: " + TEST_WORKSPACE) + shutil.rmtree(TEST_WORKSPACE, ignore_errors=True) diff --git a/analyzer/tests/functional/z3/test_z3.py b/analyzer/tests/functional/z3/test_z3.py new file mode 100644 index 0000000000..53c05f8dc3 --- /dev/null +++ b/analyzer/tests/functional/z3/test_z3.py @@ -0,0 +1,111 @@ +# +# ------------------------------------------------------------------------- +# +# Part of the CodeChecker project, under the Apache License v2.0 with +# LLVM Exceptions. See LICENSE for license information. +# SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +# +# ------------------------------------------------------------------------- + +""" Z3 feature test. """ + + +from distutils import util +import os +import unittest +import shlex + +from libtest import env +from libtest.codechecker import call_command + +NO_Z3_MESSAGE = "Z3 is not supported" + + +class TestSkeleton(unittest.TestCase): + + _ccClient = None + + def setUp(self): + + # TEST_WORKSPACE is automatically set by test package __init__.py . + test_workspace = os.environ['TEST_WORKSPACE'] + + test_class = self.__class__.__name__ + print('Running ' + test_class + ' tests in ' + test_workspace) + + # Get the test project configuration from the prepared test workspace. + self._testproject_data = env.setup_test_proj_cfg(test_workspace) + self.assertIsNotNone(self._testproject_data) + + # Get the CodeChecker cmd if needed for the tests. + self._codechecker_cmd = env.codechecker_cmd() + + self.env = env.codechecker_env() + + # Get if the package is z3 compatible. + cmd = [self._codechecker_cmd, 'analyze', '-h'] + output, _, _ = call_command(cmd, cwd=test_workspace, env=self.env) + self.z3_capable = '--z3' in output + print(f"'analyze' reported z3 compatibility? {self.z3_capable}") + + if not self.z3_capable: + try: + self.z3_capable = bool(util.strtobool( + os.environ['CC_TEST_FORCE_Z3_CAPABLE'])) + except (ValueError, KeyError): + pass + + test_project_path = self._testproject_data['project_path'] + test_project_build = shlex.split(self._testproject_data['build_cmd']) + test_project_clean = shlex.split(self._testproject_data['clean_cmd']) + + # Clean the test project before logging the compiler commands. + output, err, _ = call_command( + test_project_clean, cwd=test_project_path, env=self.env) + print(output) + print(err) + + # Create compilation log used in the tests. + log_cmd = [ + self._codechecker_cmd, 'log', '-o', 'compile_command.json', '-b'] + log_cmd.extend(test_project_build) + output, err, _ = call_command( + log_cmd, cwd=test_project_path, env=self.env) + print(output) + print(err) + + def test_z3(self): + """ Enable z3 during analysis. """ + if not self.z3_capable: + self.skipTest(NO_Z3_MESSAGE) + + test_project_path = self._testproject_data['project_path'] + + cmd = [ + self._codechecker_cmd, 'analyze', + 'compile_command.json', + '-o', 'reports', + '--z3', 'on', + '--verbose', 'debug'] + output, _, ret = call_command( + cmd, cwd=test_project_path, env=self.env) + self.assertEqual(ret, 0) + self.assertIn("-analyzer-constraints=z3", output) + + def test_z3_refutation(self): + """ Enable z3 refutation during analysis. """ + if not self.z3_capable: + self.skipTest(NO_Z3_MESSAGE) + + test_project_path = self._testproject_data['project_path'] + + cmd = [ + self._codechecker_cmd, 'analyze', + 'compile_command.json', + '-o', 'reports', + '--z3-refutation', 'on', + '--verbose', 'debug'] + output, _, ret = call_command( + cmd, cwd=test_project_path, env=self.env) + self.assertEqual(ret, 0) + self.assertIn("crosscheck-with-z3=true", output) diff --git a/analyzer/tests/projects/suppress/Makefile b/analyzer/tests/projects/suppress/Makefile index 1cec29bb98..c5359817fd 100644 --- a/analyzer/tests/projects/suppress/Makefile +++ b/analyzer/tests/projects/suppress/Makefile @@ -4,4 +4,4 @@ all: suppress_already_confirmed.cpp suppress_without_bug.cpp clean: - rm a.out + rm -f a.out