Merge pull request #38 from ispras/script_for_traces_filtering

Add a script for filtering error traces

.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:

.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 }}

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/

README.md

@@ -30,7 +30,7 @@ make install-witness-visualizer DEPLOY_DIR=<deployment directory>
 After deployment Witness Visualizer can be used to convert witnesses from the `<deployment directory>` with command:
 
 ```
-scripts/visualize_witnesses.py OPTIONS
+<deployment directory>/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
+<deployment directory>/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=<deployment directory>
 #### 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 `<deployment directory>` with the following command:
+```shell
+make install-mea DEPLOY_DIR=<deployment directory>
+```
+
+#### Usage
+```shell
+<deployment directory>/scripts/mea.py -d <directory with violation witnesses>
+```
+All unique violation witnesses will be printed as a result.

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)

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

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:

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}'")