diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml index 6e652c9..91287f2 100644 --- a/.github/workflows/deploy.yml +++ b/.github/workflows/deploy.yml @@ -1,13 +1,13 @@ name: Deploy -on: [push, pull_request, workflow_dispatch] +on: [push, workflow_dispatch] jobs: build-launcher: runs-on: ubuntu-latest strategy: matrix: - python-version: ["3.8", "3.9", "3.10"] + python-version: ["3.8"] steps: - uses: actions/checkout@v3 - name: Set up Python ${{ matrix.python-version }} @@ -31,7 +31,7 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - python-version: ["3.8", "3.9", "3.10"] + python-version: ["3.8"] steps: - uses: actions/checkout@v3 - name: Set up Python ${{ matrix.python-version }} @@ -48,6 +48,26 @@ jobs: cd build python3 ./scripts/visualize_witnesses.py -r results/ -d ../docs/examples/witnesses/violation/ python3 ./scripts/visualize_witnesses.py -r results/ -d ../docs/examples/witnesses/correctness/ + build-mea: + runs-on: ubuntu-latest + strategy: + matrix: + python-version: ["3.8"] + steps: + - uses: actions/checkout@v3 + - name: Set up Python ${{ matrix.python-version }} + uses: actions/setup-python@v3 + with: + python-version: ${{ matrix.python-version }} + - name: Install dependencies + run: | + python3 -m pip install --upgrade pip + pip3 install requests ujson graphviz ply pytest atomicwrites more-itertools pluggy py attrs setuptools six django==2.1 psycopg2 pycparser sympy + - name: Deployment of MEA + run: | + DEPLOY_DIR=build make install-mea -j$(nproc) + cd build + python3 ./scripts/mea.py -d ../docs/examples/witnesses/violation/ build-frama-c-cil: runs-on: ubuntu-latest strategy: diff --git a/.github/workflows/pylint.yml b/.github/workflows/pylint.yml index 3955e9c..11bc95d 100644 --- a/.github/workflows/pylint.yml +++ b/.github/workflows/pylint.yml @@ -1,13 +1,13 @@ name: Pylint -on: [push, pull_request, workflow_dispatch] +on: [push, workflow_dispatch] jobs: build: runs-on: ubuntu-latest strategy: matrix: - python-version: ["3.8", "3.9", "3.10"] + python-version: ["3.8"] steps: - uses: actions/checkout@v3 - name: Set up Python ${{ matrix.python-version }} diff --git a/Makefile b/Makefile index 75ebb19..3fc5e47 100644 --- a/Makefile +++ b/Makefile @@ -231,6 +231,12 @@ install-witness-visualizer: check-deploy-dir build-klever cp ${klever_dir}/bridge/reports/mea/core.py scripts/aux/mea.py @echo "*** Witness Visualizer has been successfully installed into the directory ${DEPLOY_DIR} ***" +install-mea: install-witness-visualizer + @cd ${DEPLOY_DIR} ; \ + rm -f scripts/${wv_script} ; \ + rm -rf ${klever_dir}/bridge/ + @echo "*** MEA has been successfully installed into the directory ${DEPLOY_DIR} ***" + install-benchmark-visualizer: install-witness-visualizer @cp -r ${klever_dir}/utils/ ${DEPLOY_DIR}/${klever_dir}/ @cp -f ${root_dir}/scripts/${bv_script} ${DEPLOY_DIR}/scripts/ diff --git a/README.md b/README.md index 89ceafe..81f9088 100644 --- a/README.md +++ b/README.md @@ -30,7 +30,7 @@ make install-witness-visualizer DEPLOY_DIR= After deployment Witness Visualizer can be used to convert witnesses from the `` with command: ``` -scripts/visualize_witnesses.py OPTIONS +/scripts/visualize_witnesses.py OPTIONS ``` Primary options: @@ -44,7 +44,7 @@ Primary options: For example: ```bash -scripts/visualize_witnesses.py --witness output/witness.graphml --result-dir results/ --source-dir ~/sv-benchmarks +/scripts/visualize_witnesses.py --witness output/witness.graphml --result-dir results/ --source-dir ~/sv-benchmarks ``` There are some examples of [SV-COMP](https://sv-comp.sosy-lab.org) witnesses in the `docs/examples/witnesses` directory, @@ -71,3 +71,23 @@ make install-benchmark-visualizer DEPLOY_DIR= #### Usage See instruction [docs/benchmark_visualizer.md](docs/benchmark_visualizer.md). + +## Filtering of witnesses + +Multiple Error Analysis (MEA) stands for semi-automatic violation witnesses filtering. +This framework provides part of MEA, which performs automatic filtering. +In order to do it, some core elements are extracted from a violation witness by means of +a specified `conversion` function and then compared with core elements of other witnesses +by means of a specified `comparison` function. + +#### Deployment +MEA library can be installed in the `` with the following command: +```shell +make install-mea DEPLOY_DIR= +``` + +#### Usage +```shell +/scripts/mea.py -d +``` +All unique violation witnesses will be printed as a result. diff --git a/scripts/auto_check.py b/scripts/auto_check.py index 5d36596..d290a09 100755 --- a/scripts/auto_check.py +++ b/scripts/auto_check.py @@ -86,11 +86,14 @@ def __init__(self, config_file: str): self.output_desc = sys.stdout else: self.output_desc = subprocess.DEVNULL - logger_level = logging.DEBUG if self.debug else logging.INFO - logging.basicConfig(format='%(asctime)s: %(name)s: %(levelname)s: %(message)s', - level=logger_level, datefmt='%Y-%m-%d %H:%M:%S') + self.logger = logging.getLogger(name=COMPONENT_AUTO_CHECKER) - self.logger.setLevel(logger_level) + stream_handler = logging.StreamHandler(stream=sys.stdout) + stream_handler.setFormatter(logging.Formatter( + '%(asctime)s: %(name)s: %(levelname)s: %(message)s', '%Y-%m-%d %H:%M:%S') + ) + self.logger.addHandler(stream_handler) + self.logger.setLevel(logging.DEBUG if self.debug else logging.INFO) self.hostname = None self.hostname = self.__command_caller("hostname", get_stdout=True) diff --git a/scripts/components/component.py b/scripts/components/component.py index cb26094..13e20c9 100644 --- a/scripts/components/component.py +++ b/scripts/components/component.py @@ -69,17 +69,17 @@ def __init__(self, name: str, config: dict): # Debug and logging. self.debug = self.component_config.get(TAG_DEBUG, False) - logger_level = logging.DEBUG if self.debug else logging.INFO - logging.basicConfig(format='%(name)s: %(levelname)s: %(message)s', level=logger_level) - self.logger = logging.getLogger(name=self.name) - self.logger.setLevel(logger_level) + self.logger = self._create_logger(self.name, logging.DEBUG if self.debug else logging.INFO) # Should be rewritten. self.install_dir = None self.error_logs = set() self.temp_logs = set() if not Component.tools_config: - with open(TOOL_CONFIG_FILE, encoding='ascii') as file_obj: + install_dir = os.path.abspath( + os.path.join(os.path.dirname(os.path.realpath(__file__)), os.pardir, os.pardir) + ) + with open(os.path.join(install_dir, TOOL_CONFIG_FILE), encoding='ascii') as file_obj: Component.tools_config = json.load(file_obj) def __propagate_config(self): @@ -93,6 +93,15 @@ def __propagate_config(self): component_config[tag] = self.config[tag] self.component_config = component_config + @staticmethod + def _create_logger(logger_name: str, logger_level): + logger = logging.getLogger(name=logger_name) + stream_handler = logging.StreamHandler(stream=sys.stdout) + stream_handler.setFormatter(logging.Formatter('%(name)s: %(levelname)s: %(message)s')) + logger.addHandler(stream_handler) + logger.setLevel(logger_level) + return logger + def runexec_wrapper(self, cmd, output_dir=None, output_file=None): """ Call a command inside RunExec tool, track its resources and redirect its output into diff --git a/scripts/components/mea.py b/scripts/components/mea.py index 643bff7..3c32bb5 100644 --- a/scripts/components/mea.py +++ b/scripts/components/mea.py @@ -352,12 +352,9 @@ def __parse_trace(self, error_trace_file: str, supported_types: set) -> dict: from core.vrp.et import import_error_trace # Those messages are waste of space. - logger = logging.getLogger(name="Witness processor") - logging.basicConfig(format='%(name)s: %(levelname)s: %(message)s') - if self.debug: - logger.setLevel(logging.WARNING) - else: - logger.setLevel(logging.ERROR) + logger = self._create_logger( + "Witness processor", logging.WARNING if self.debug else logging.ERROR + ) try: json_error_trace = import_error_trace(logger, error_trace_file, self.source_dir) if self.dry_run: diff --git a/scripts/mea.py b/scripts/mea.py new file mode 100644 index 0000000..b99c2ac --- /dev/null +++ b/scripts/mea.py @@ -0,0 +1,94 @@ +#!/usr/bin/python3 +# +# CV is a framework for continuous verification. +# +# Copyright (c) 2018-2023 ISP RAS (http://www.ispras.ru) +# Ivannikov Institute for System Programming of the Russian Academy of Sciences +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +# + +""" +This script provides functionality to filter a given witnesses. +""" + +import argparse + +from components.mea import * + + +def _create_config(options=None, conversion_function="", comparison_function=""): + additional_mf = [] + is_debug = False + if options: + conversion_function = options.conversion + comparison_function = options.comparison + additional_mf = options.mf or [] + is_debug = options.debug + return { + COMPONENT_MEA: { + TAG_COMPARISON_FUNCTION: comparison_function, + TAG_CONVERSION_FUNCTION: conversion_function, + TAG_CONVERSION_FUNCTION_ARGUMENTS: { + TAG_ADDITIONAL_MODEL_FUNCTIONS: additional_mf + }, + TAG_DEBUG: is_debug, + TAG_CLEAN: False, + TAG_UNZIP: False, + TAG_DRY_RUN: False, + TAG_SOURCE_DIR: None + } + } + + +def _parse_cmdline() -> tuple: + parser = argparse.ArgumentParser() + parser.add_argument("-d", "--directory", help="directory with witnesses to be filtered", + required=True) + parser.add_argument("--conversion", help="conversion function", + default=DEFAULT_CONVERSION_FUNCTION) + parser.add_argument("--comparison", help="comparison function", + default=DEFAULT_COMPARISON_FUNCTION) + parser.add_argument("--additional-model-functions", dest='mf', nargs='+', + help="additional model functions, separated by whitespace") + parser.add_argument('--debug', action='store_true') + options = parser.parse_args() + + witnesses = glob.glob(os.path.join(options.directory, f"witness.*{GRAPHML_EXTENSION}")) + return witnesses, _create_config(options) + + +def execute_filtering(witnesses: list, config=None, conversion_function="", + comparison_function="") -> list: + """ + Filter the given violation witnesses. + """ + if not config: + config = _create_config(conversion_function=conversion_function, + comparison_function=comparison_function) + script_dir = os.path.join(os.path.dirname(os.path.realpath(__file__)), os.pardir) + install_dir = os.path.abspath(os.path.join(script_dir, DEFAULT_INSTALL_DIR)) + + if not os.path.exists(install_dir): + install_dir = os.path.abspath(os.path.join(os.pardir, DEFAULT_INSTALL_DIR)) + mea = MEA(config, witnesses, install_dir) + mea.logger.debug(f"Received {len(witnesses)} witnesses") + processed_witnesses = mea.filter() + mea.logger.debug(f"Number of unique witnesses is {len(processed_witnesses)}") + return processed_witnesses + + +if __name__ == "__main__": + m_witnesses, m_config = _parse_cmdline() + for witness in execute_filtering(m_witnesses, m_config): + print(f"Unique witness '{witness}'")