From e5b6d14f052c4faaa36ba294ad48d45fc48891ec Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Sun, 3 Jan 2021 17:20:53 +0100 Subject: [PATCH 1/3] Added configurable portfolio --- .github/workflows/build.yml | 3 + .travis.yml | 4 + Dockerfile | 7 +- doc/Portfolio.md | 68 ++ scripts/gazer_starter.py | 442 ------------- scripts/portfolio/Portfolio.pl | 221 +++++++ scripts/portfolio/lib/Execute.pm | 125 ++++ scripts/portfolio/lib/Logger.pm | 60 ++ scripts/portfolio/lib/Options.pm | 137 ++++ .../test-configs/SVComp_configuration.yml | 23 + .../SVComp_finish_all_configuration.yml | 23 + .../test-configs/config-file-example.yml | 24 + .../portfolio/test-configs/small_timeout.yml | 17 + .../portfolio/test-tasks/Problem01_label02.c | 611 ++++++++++++++++++ .../portfolio/test-tasks/overflow_example.c | 10 + .../portfolio/test-tasks/test_locks_14-2.c | 223 +++++++ .../portfolio/test-tasks/zerodiv_example.c | 19 + test/portfolio/SVComp_configuration.yml | 23 + .../SVComp_finish_all_configuration.yml | 23 + test/portfolio/lit.local.cfg | 13 + test/portfolio/small_timeout.yml | 17 + test/portfolio/test_locks_14-2.c | 227 +++++++ test/portfolio/test_locks_14-2_finish_all.c | 231 +++++++ test/portfolio/zerodiv_example.c | 24 + test/portfolio/zerodiv_example_finish_all.c | 27 + 25 files changed, 2158 insertions(+), 444 deletions(-) create mode 100644 doc/Portfolio.md delete mode 100755 scripts/gazer_starter.py create mode 100755 scripts/portfolio/Portfolio.pl create mode 100644 scripts/portfolio/lib/Execute.pm create mode 100644 scripts/portfolio/lib/Logger.pm create mode 100644 scripts/portfolio/lib/Options.pm create mode 100644 scripts/portfolio/test-configs/SVComp_configuration.yml create mode 100644 scripts/portfolio/test-configs/SVComp_finish_all_configuration.yml create mode 100644 scripts/portfolio/test-configs/config-file-example.yml create mode 100644 scripts/portfolio/test-configs/small_timeout.yml create mode 100644 scripts/portfolio/test-tasks/Problem01_label02.c create mode 100644 scripts/portfolio/test-tasks/overflow_example.c create mode 100644 scripts/portfolio/test-tasks/test_locks_14-2.c create mode 100644 scripts/portfolio/test-tasks/zerodiv_example.c create mode 100644 test/portfolio/SVComp_configuration.yml create mode 100644 test/portfolio/SVComp_finish_all_configuration.yml create mode 100644 test/portfolio/lit.local.cfg create mode 100644 test/portfolio/small_timeout.yml create mode 100644 test/portfolio/test_locks_14-2.c create mode 100644 test/portfolio/test_locks_14-2_finish_all.c create mode 100644 test/portfolio/zerodiv_example.c create mode 100644 test/portfolio/zerodiv_example_finish_all.c diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 0326c5d3..3e2024dc 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -12,9 +12,12 @@ jobs: - name: Set up some more dependencies run: | sudo apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime libboost-all-dev + sudo ln -sf /usr/bin/clang-9 /usr/bin/clang sudo ln -s `which opt-9` /usr/bin/opt -f sudo ln -s `which FileCheck-9` /usr/bin/FileCheck sudo pip3 install lit + - name: Set up portfolio dependencies + run: sudo apt-get install perl libyaml-tiny-perl libproc-processtable-perl - name: Build run: cmake -DCMAKE_CXX_COMPILER=clang++-9 -DGAZER_ENABLE_UNIT_TESTS=On -DCMAKE_BUILD_TYPE=Debug -DCMAKE_EXPORT_COMPILE_COMMANDS=On . && make - name: Get Theta diff --git a/.travis.yml b/.travis.yml index f53319db..b031be5b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -16,6 +16,9 @@ addons: - python3-pip - python3-setuptools - python3-psutil + - perl + - libyaml-tiny-perl + - libproc-processtable-perl sonarcloud: organization: "ftsrg" cache: @@ -29,6 +32,7 @@ script: - sudo add-apt-repository ppa:mhier/libboost-latest -y - sudo apt-get update - sudo apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime libboost1.70-dev +- sudo ln -sf /usr/bin/clang-9 /usr/bin/clang - sudo ln -s `which opt-9` /usr/bin/opt -f - sudo ln -s `which FileCheck-9` /usr/bin/FileCheck - sudo pip3 install lit diff --git a/Dockerfile b/Dockerfile index d4d85a1d..9a18e823 100644 --- a/Dockerfile +++ b/Dockerfile @@ -14,14 +14,17 @@ RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - && \ apt-get update && \ add-apt-repository ppa:mhier/libboost-latest && \ apt-get update && \ - apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime libboost1.70-dev + apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime libboost1.70-dev perl libyaml-tiny-perl # create a new user `user` with the password `user` and sudo rights RUN useradd -m user && \ echo user:user | chpasswd && \ cp /etc/sudoers /etc/sudoers.bak && \ echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers - + +# (the portfolio uses clang) +RUN ln -sf /usr/bin/clang-9 /usr/bin/clang + USER user ENV GAZER_DIR /home/user/gazer diff --git a/doc/Portfolio.md b/doc/Portfolio.md new file mode 100644 index 00000000..377e9488 --- /dev/null +++ b/doc/Portfolio.md @@ -0,0 +1,68 @@ +# Gazer-Theta Portfolio +## What is the Portfolio script? +Gazer can be used as a command-line tool (gazer-cfa, gazer-bmc or gazer-theta) with lots of possible configurations. But in those cases Gazer simply executes that configuration on the given input program and returns the output of the verification process. The portfolio script adds another "level" to these command-line tools: it enables the sequential run of several configurations based on a YAML configuration file. This, on one hand, enables the user to easily compare configurations, as some may be better suited for a specific set of inputs than others. On the other hand it also enables of saving such successful configuration groups - portfolios - which then can be reused later. + +## Usage of script +### Configuration file (YAML) +This file configures the portfolio and it is given to the Portfolio script as the argument of the flag *--configuration/-c* +#### Global options +##### generate-witness: Yes/No +Gazer - among other formats - can generate a counterexample in the format of SV-Comps violation witnesses. More about the witnesses [here](https://github.com/sosy-lab/sv-witnesses). +##### finish-all-configurations: Yes/No +If Yes, the script will run all the configurations in the order they were given in the configuration file. +If No, the script will stop, when a configuration (with test harness checked, if set so) gives back a result (failed or succesful) and will output that as the final result +##### check-harness +If defined, then Gazer will generate a test harness in the appropriate cases and the script will compile, execute and check this test harness, with which it can filter out false positive results execute-harness-timeout and compile-harness-timeout need to be given in this case as well (in seconds), for example: +``` +check-harness: + execute-harness-timeout: 100 + check-harness-timeout: 150 +``` +#### Configuration of the portfolio itself +An array of the configurations, something like this: +``` +configurations: + - name: config1 + tool: gazer-bmc + timeout: 1 # sec + flags: --inline all --bound 1000000* + - name: config2 + tool: gazer-theta + flags: --inline all --domain EXPL +``` +- The **name** and **tool** attributes are required, **timeout** and **flags** are optional. +- The **name** can be any arbitrary name, it mostly serves readability purposes. +- The possible values of **tool** are *gazer-bmc* or *gazer-theta*. +- Giving a **timeout** is optional, but not doing so can possibly result in an endless run, if Gazer or Theta gets stuck. +- Documentation of the available **flags**: [for Gazer](https://github.com/ftsrg/gazer/blob/master/README.md), [for Theta](https://github.com/ftsrg/theta/blob/master/doc/CEGAR-algorithms.md) + +For more detailed examples, see the *test-configs* directory under *scripts/portfolio/* + +### Flags +**--version/-v** - outputs the Gazer and Theta versions *(and does nothing else)* +**--configuration/-c "filename"** - YAML portfolio configuration file +**--task/-t "filename"** - C program to be verified (.c, .i, .ll) +**--log-level/-l** - minimal or verbose (verbose outputs the output of Gazer as well) +**--output-directory/-o** - output path, where a portfolio-output directory will be created and used by the script (default: working directory) +**--debug/-d**** - if given, the logs are extended with more information about the script for debugging purposes (directories used, configuration list, etc.) + +### Example +./Portfolio.pl -c test-files/config-file-example.yml -t test-files/test_locks_14-2.c -l minimal -o test_output/ + +## Required Perl packages +YAML::Tiny *(Parses YAML, not part of core packages)* +Getopt::Long *(Handles flags, part of core packages)* +Digest::file *(generates SHA256 hash for witnesses, part of core packages)* +Process::Killfam *(Required for properly terminating tools after timeout, not a core package)* + +### from apt on Ubuntu: +https://packages.ubuntu.com/bionic/perl +https://packages.ubuntu.com/bionic/libyaml-tiny-perl +https://packages.ubuntu.com/bionic/libproc-processtable-perl + +### through CPAN: +``` +perl -MCPAN -e shell +install +exit +``` diff --git a/scripts/gazer_starter.py b/scripts/gazer_starter.py deleted file mode 100755 index cf29b17a..00000000 --- a/scripts/gazer_starter.py +++ /dev/null @@ -1,442 +0,0 @@ -#!/usr/bin/python3 - -# This script runs Gazer and Theta with several configurations on the given programfile -# test harnesses (counterexamples) and witnesses in the format of SV-Comp '21 are generated - -import re -import os -import errno -import signal -import sys -import subprocess -import hashlib -import argparse -import enum -from subprocess import Popen, PIPE, TimeoutExpired -from time import monotonic as timer - -# TODO tweak timeouts, should the cartpred config get a timeout? -bmc_timeout = 150.0 # timeout of bmc run -theta_explicit_timeout = 100.0 # timeout of explicit theta run -test_harness_compile_timeout = 50.0 # timeout of compiling test harness/counterexample -counterexample_run_timeout = 100.0 # timeout of running the generated counterexample - -theta_explicit_config = [ - "--search ERR", - "--domain EXPL", - "--maxenum 100", - "--refinement BW_BIN_ITP", - "--initprec ALLVARS", -] -theta_cartpred_config = [ - "--inline all", - "--search ERR", - "--domain PRED_CART", - "--refinement BW_BIN_ITP", - "--initprec EMPTY", -] -bmc_config = [ - "--inline all", - "--bound 1000000", -] # bound: We'll kill it after the timeout anyway, so it can be really big, why not - -# default values -output_path = os.getcwd() -tool_directory = os.path.abspath( - os.path.dirname(os.path.dirname(os.path.abspath(__file__))) + "/build/tools" -) # /tools, if built like the Docker, /build/tools, if built in a build directory - - -class Result(enum.Enum): - UNKNOWN = 1 - ERROR = 2 - TRUE = 3 - FALSE = 4 - - -result = Result.UNKNOWN # should be printed with result.name - - -def print_bmc(): - print("gazer-bmc:") - - -def print_theta(): - print("gazer-theta:") - - -def print_line(): - print("\n------------------------------------------\n") - - -def print_result(): - print("Result of gazer-theta run: " + result.name) - - -# If output is None, prints "No output" -def print_if_not_empty(output): - if output != None: - print(output.decode("utf-8")) - else: - print("No output") - - -# raises CalledProcessError, if returncode isn't 0; raises TimeoutExpire, if process times out -def run_with_timeout(command, timeout, env=None, no_print=False): - # instead of subprocess.check_output() - # to enforce timeout before Python 3.7.5 - # and kill sub-processes to avoid interference - # https://stackoverflow.com/a/36955420 - start = timer() - with subprocess.Popen( - command, - shell=True, - stdout=subprocess.PIPE, - stderr=subprocess.STDOUT, - start_new_session=True, - env=env, - ) as process: - try: - # note: stderr is forwarded to stdout and they are handled together, so we won't use stderr_dummy - stdout_bytes, stderr_dummy = process.communicate( - input=None, timeout=timeout - ) - returncode = process.poll() - - if returncode: - if not no_print: - print( - "Command returned with " - + str(returncode) - + " after {:.2f} seconds".format(timer() - start) - ) - raise subprocess.CalledProcessError( - returncode, process.args, output=stdout_bytes - ) - else: - if not no_print: - print( - "Command returned with 0 after {:.2f} seconds".format( - timer() - start - ) - ) - return stdout_bytes - except KeyboardInterrupt: - os.killpg( - os.getpgid(process.pid), signal.SIGINT - ) # send signal to the process group - raise KeyboardInterrupt - except subprocess.TimeoutExpired: - os.killpg( - os.getpgid(process.pid), signal.SIGTERM - ) # send signal to the process group - # stdout_bytes, stderr_dummy = process.communicate() - hangs sometimes - if not no_print: - print("Command timeout after {:.2f} seconds".format(timer() - start)) - raise TimeoutExpired(process.args, timeout, output=None) - - -# raises CalledProcessError, if returncode isn't 0; no timeout - waits for the process to return infinitely -def run_without_timeout(command, env=None, no_print=False): - # instead of subprocess.check_output() - # to enforce timeout before Python 3.7.5 - # and kill sub-processes to avoid interference - # https://stackoverflow.com/a/36955420 - start = timer() - with subprocess.Popen( - command, - shell=True, - stdout=subprocess.PIPE, - stderr=subprocess.STDOUT, - start_new_session=True, - env=env, - ) as process: - try: - # note: stderr is forwarded to stdout and they are handled together, so we won't use stderr_dummy - stdout_bytes, stderr_dummy = process.communicate(input=None) - returncode = process.poll() - - if returncode: - if not no_print: - print( - "Command returned with " - + str(returncode) - + " after {:.2f} seconds".format(timer() - start) - ) - raise subprocess.CalledProcessError( - returncode, process.args, output=stdout_bytes - ) - else: - if not no_print: - print( - "Command returned with 0 after {:.2f} seconds".format( - timer() - start - ) - ) - return stdout_bytes - except KeyboardInterrupt: - os.killpg( - os.getpgid(process.pid), signal.SIGINT - ) # send signal to the process group - raise KeyboardInterrupt - - -# changes the global result parameter based on output of the given bmc/theta run -# tries to run the test harness, if needed -# should be given an output from a run with return code 0 -def parse_output(output, task): - global result - # parses in reverse, as the output can be long, but the lines searched are around the end (mostly the last lines) - for line in reversed(output.decode("utf-8").split("\n")): - if "Verification FAILED" in line: - result = run_test_harness(task) # FALSE, ERROR or UNKNOWN - if "Verification SUCCESSFUL" in line: - result = Result.TRUE - if "Verification BOUND REACHED" in line: - result = Result.UNKNOWN - if "Verification INTERNAL ERROR" in line: - result = Result.ERROR - - -# We know about the run that it was successful, but if it has a false result, we should run -# the generated test harness as well to make sure, that the counterexample is correct -def run_test_harness(task): - task_name = os.path.basename(task) - # clang task harness.ll -o task_test - # ./task_test -> if it outputs Aborted return True, if not return False - clang_command = ( - "clang " - + task - + " " - + output_path - + "/" - + task_name - + ".ll -o " - + output_path - + "/" - + task_name - + "_test" - ) - test_command = output_path + "/" + task_name + "_test" - - print("Running " + clang_command + "\n") - try: - clang_output = run_with_timeout(clang_command, test_harness_compile_timeout) - except subprocess.CalledProcessError as err: - print(err) - print("Could not compile test harness") - return Result.ERROR - except subprocess.TimeoutExpired as err: - print("Could not compile test harness, timed out after " + str(err.timeout)) - return Result.ERROR - except: # Shouldn't happen, but just in case - print("Unexpected error:", sys.exc_info()[0]) - print("Could not compile test harness") - return Result.ERROR - else: - print_if_not_empty(clang_output) - - print("Running " + test_command + "\n") - try: - test_output = run_with_timeout(test_command, counterexample_run_timeout) - print_if_not_empty(test_output) - print("Counterexample is wrong, result is unknown") - return Result.UNKNOWN - except subprocess.CalledProcessError as err: - good_output = r"reach_error(\(\))?: Assertion.*failed" - if re.search(good_output, err.output.decode("utf-8")): - print("Counterexample ok") - return Result.FALSE - else: - print("Counterexample is wrong, result is unknown") - return Result.UNKNOWN - except subprocess.TimeoutExpired as err: - print("Counterexample timed out after " + str(err.timeout)) - return Result.ERROR - except: # Shouldn't happen, but just in case - print("Unexpected error:", sys.exc_info()[0]) - print("Problems while running test harness") - return Result.ERROR - - -# if timeout is 0, then it will be run without timeout -def run_next_config(toolname, flags, task_with_path, timeout): - global result - print_line() - - command = tool_directory + toolname + " " + " ".join(flags) + " " + task_with_path - print("Running " + command + "\n") - if timeout != 0: - try: - output = run_with_timeout(command, timeout) - print_if_not_empty(output) - if output != None: - parse_output(output, task_with_path) - print_line() - except subprocess.CalledProcessError as err: - print_if_not_empty(err.output) - except subprocess.TimeoutExpired as err: - print_if_not_empty(err.output) - except KeyboardInterrupt: - raise KeyboardInterrupt - except: # Shouldn't happen, but just in case - print("Unexpected error:", sys.exc_info()[0]) - print("Changing result to unknown") - result = Result.UNKNOWN - else: - try: - output = run_without_timeout(command) - print_if_not_empty(output) - if output != None: - parse_output(output, task_with_path) - print_line() - except subprocess.CalledProcessError as err: - print_if_not_empty(err.output) - except KeyboardInterrupt: - raise KeyboardInterrupt - except: # Shouldn't happen, but just in case - print("Unexpected error:", sys.exc_info()[0]) - print("Changing result to unknown") - result = Result.UNKNOWN - - -def get_version_number(): - z3path = tool_directory + "/gazer-theta/theta/lib" - gazer_version = run_without_timeout( - tool_directory + "/gazer-theta/gazer-theta --version", no_print=True - ) - theta_ver = run_without_timeout( - "java -Djava.library.path=" - + z3path - + " -jar " - + tool_directory - + "/gazer-theta/theta/theta-cfa-cli.jar --version", - env={"LD_LIBRARY_PATH": z3path}, - no_print=True, - ) - return ( - "Theta v" - + theta_ver.decode("utf-8") - + re.search(r"Gazer v\d*[.]\d*[.]\d*", gazer_version.decode("utf-8")).group() - ) - - -def main(): - global output_path - global result - - parser = argparse.ArgumentParser() - - # optional TODO get_version_number runs in every case, even when --version isn't used - it shouldn't - parser.add_argument("--version", action="version", version=get_version_number()) - parser.add_argument("task", help="name of the to be verified programfile with path") - parser.add_argument( - "--output", - help="output directory (for the witness and test harness), default: working directory", - ) - - args = parser.parse_args() - print("Parsing arguments done") - - # initialize argument values - taskname = os.path.basename(args.task) - task_with_path = os.path.abspath(args.task) - - if args.output != None: - output_path = os.path.abspath(args.output) - - # check if the output directory exists, create it if not - if not os.path.exists(output_path) or not os.path.isdir(output_path): - try: - os.makedirs(output_path) - except OSError as err: - # possible race condition here (someone creates the output dir between our check and makedirs), then an incorrect OSError can happen - # see http://deepix.github.io/2017/02/02/eexists.html - if err.errno != errno.EEXIST: - print("Creation of the output directory %s failed" % output_path) - result = Result.ERROR - print_result() - return - else: - print("Successfully created the output directory %s" % output_path) - - # check, if the tool directory is correct and has gazer-bmc, gazer-theta, theta and z3 libs as well - if not os.path.isfile(tool_directory + "/gazer-bmc/gazer-bmc"): - raise FileNotFoundError( - errno.ENOENT, - os.strerror(errno.ENOENT), - tool_directory + "/gazer-bmc/gazer-bmc", - ) - if not os.path.isfile(tool_directory + "/gazer-theta/gazer-theta"): - raise FileNotFoundError( - errno.ENOENT, - os.strerror(errno.ENOENT), - tool_directory + "/gazer-theta/gazer-theta", - ) - if not os.path.isfile(tool_directory + "/gazer-theta/theta/theta-cfa-cli.jar"): - raise FileNotFoundError( - errno.ENOENT, - os.strerror(errno.ENOENT), - tool_directory + "/gazer-theta/theta/theta-cfa-cli.jar", - ) - if not os.path.isfile(tool_directory + "/gazer-theta/theta/lib/libz3.so"): - raise FileNotFoundError( - errno.ENOENT, - os.strerror(errno.ENOENT), - tool_directory + "/gazer-theta/theta/lib/libz3.so", - ) - if not os.path.isfile(tool_directory + "/gazer-theta/theta/lib/libz3java.so"): - raise FileNotFoundError( - errno.ENOENT, - os.strerror(errno.ENOENT), - tool_directory + "/gazer-theta/theta/lib/libz3java.so", - ) - - # hash to use in the witness - print("Hashing taskfile " + taskname) - with open(task_with_path, "r") as pgf: - hash_of_source = hashlib.sha256(pgf.read().encode("utf-8")).hexdigest() - print("Hashing done") - - outputfile_flags = [ - "--witness " + output_path + "/" + taskname + ".witness.graphml", - "--hash " + hash_of_source, - "--trace", - "-test-harness=" + output_path + "/" + taskname + ".ll", - ] - - print_line() - print("Starting combined gazer-theta-bmc run...") - - run_next_config( - "/gazer-bmc/gazer-bmc", - bmc_config + outputfile_flags, - task_with_path, - bmc_timeout, - ) - if result == Result.FALSE or result == Result.TRUE: - print_result() - return - - run_next_config( - "/gazer-theta/gazer-theta", - theta_explicit_config + outputfile_flags, - task_with_path, - theta_explicit_timeout, - ) - if result == Result.FALSE or result == Result.TRUE: - print_result() - return - - run_next_config( - "/gazer-theta/gazer-theta", - theta_cartpred_config + outputfile_flags, - task_with_path, - 0, - ) - - print_result() - - -if __name__ == "__main__": - main() diff --git a/scripts/portfolio/Portfolio.pl b/scripts/portfolio/Portfolio.pl new file mode 100755 index 00000000..35377be7 --- /dev/null +++ b/scripts/portfolio/Portfolio.pl @@ -0,0 +1,221 @@ +#!/usr/bin/perl +use strict; +use warnings; + +use FindBin qw($Bin); +use lib "$Bin/lib"; + +use Execute qw ( run_gazer check_harness ); +use Logger; +use Options qw ( initialize_flags initialize_gazer_path ); # handles inits + +use YAML::Tiny 'LoadFile'; +use File::Basename; +use Digest::file qw(digest_file_hex); + +initialize_environment(); + +# Initializing YAML +# Open the config - [0] means the first document (the config should only have one) +my $config = YAML::Tiny->read($Options::config_path_name)->[0]; +my @configurations_arr_ref = @{ $config->{configurations} }; # YAML config file + +# Listing and initializing configurations from YAML +initialize_configs(); + +Logger::log_h1("2. Executing Portfolio"); +my %results; +my $last_config; +my $successful = 0 + ; # flag, 1 if any configuration (optionally with a test harness check) resulted in success (positive/negative, but not timeout or error) + +execute_configurations(); + +Logger::log_h1("3. Evaluating Results"); +list_results(); + +unless ( $config->{"finish-all-configurations"} eq "Yes" ) +{ # we only draw a conclusion, if finish all configs is No/not set + if ($successful) { + Logger::log_h2( + "Final result of portfolio: " . $results{ $last_config->{name} } ); + } + else { + Logger::log_h2("Final result of portfolio: NONE"); + } +} + +Logger::close_logfile; + +### Subroutines of main part ### + +sub initialize_environment { + + # Initalizing gazer path, so --version works, when initializing flags + my $dirname = dirname(__FILE__); + Options::initialize_gazer_path($dirname); + +# Initialization of input flags, input files, output directory and logfile (which means, logging only works after this subroutine) + Options::initialize_flags(); + + # Listing of paths + Logger::log_h1 "1. Initializing Portfolio"; + +# Although --version also exists (it only prints the version and does nothing else), from a traceability point it is nice to always log the version + Logger::log_minimal Options::get_version(); + my $pwd = `pwd`; + chomp($pwd); + Logger::log_debug "Working directory: $pwd"; + Logger::log_debug "Path to portfolio script: $dirname"; + Logger::log_debug "Path to the gazer executables: $Options::gazer_path"; + Logger::log_debug "Output path: " . $Options::output_directory; +} + +sub initialize_configs { + foreach (@configurations_arr_ref) { # for every given config + my $config_string = "" + ; # in this we'll put together the attributes of the configuration for logging + $config_string = + $config_string . $_->{name} . ":\n\t"; # get name of config + $config_string = + $config_string . $_->{tool} . "; "; # get gazer tool used + if ( defined $_->{timeout} ) { # see if it has a timeout + $config_string = $config_string . $_->{timeout} . "; "; + } + else { + $config_string = $config_string . "no timeout; "; + $_->{timeout} = 0; + } # if there is no timeout, set it to 0 (that we'll behave the right way) + + if ( not defined $_->{flags} ) { + $_->{flags} = ""; + } # see if we got any flags + $_->{flags} = $_->{flags} + . " --trace"; # put --trace in it - for now we always run with --trace + if ( defined $config->{"generate-witness"} ) + { # adding flags for generating witness, if needed + my $hash = digest_file_hex( $Options::task_path_name, "SHA-256" ); + $_->{flags} = $_->{flags} + . " --witness ${Options::output_directory}${Options::task_file_name}.witness.graphml --hash $hash"; + } + if ( defined $config->{"check-harness"} ) + { # adding flags for generating a test harness, if needed + $_->{flags} = $_->{flags} + . " -test-harness=${Options::output_directory}${Options::task_file_name}.ll"; + } + $config_string = $config_string . $_->{flags}; + Logger::log_debug $config_string; + } + + # Warnings and errors + foreach (@configurations_arr_ref) { + if ( not defined $_->{tool} ) { + Logger::log_minimal( +"ERROR: In $_->{name}: every configuration needs the tool attribute to be set to gazer-bmc or gazer-theta.\nTerminating..." + ); + terminate(); + } + if ( not defined $_->{tool} ) { + Logger::log_minimal( +"ERROR: In $_->{name}: every configuration needs the name attribute to be set.\nTerminating..." + ); + terminate(); + } + + if ( not defined $_->{timeout} ) { + Logger::log_minimal( +"WARNING: No timeout set for configuration $_->{name}, portfolio can end up running endlessly, if not terminate()d manually!" + ); + } + } + if ( defined $config->{"check-harness"} ) { + if ( + not defined $config->{"check-harness"}->{"execute-harness-timeout"} + ) + { + Logger::log_minimal( +"ERROR in YAML: If check-harness is defined, execute-harness-timeout must also be defined as its child.\nTerminating..." + ); + terminate(); + } + elsif ( + not defined $config->{"check-harness"}->{"compile-harness-timeout"} + ) + { + Logger::log_minimal( +"ERROR in YAML: If check-harness is defined, compile-harness-timeout must also be defined as its child.\nTerminating..." + ); + terminate(); + } + } +} + +sub execute_configurations { + foreach (@configurations_arr_ref) + { # Iterating through the given configurations + $last_config = $_; + Logger::log_h2 "Running $_->{name}..."; + $results{ $_->{name} } = + Execute::run_gazer( $_->{name}, $_->{tool}, $_->{flags}, + $_->{timeout} ); # run gazer-theta + Logger::log_minimal $results{ $_->{name} }; + + if ( $results{ $_->{name} } =~ /Verification FAILED/ ) + { # we found a potential problem + + if ( defined $config->{"check-harness"} ) + { # let's check the test harness, if check-harness is set to Yes in YAML + Logger::log_minimal("Checking test harness..."); + my $test_harness_result = Execute::check_harness( + $config->{"check-harness"}->{"compile-harness-timeout"}, + $config->{"check-harness"}->{"execute-harness-timeout"} + ); + $results{ $_->{name} . "-test-harness" } = $test_harness_result; + Logger::log_minimal $results{ $_->{name} . "-test-harness" }; + + if ( $test_harness_result =~ /Test harness SUCCESSFUL WITNESS/ ) + { + $successful = 1; + if ( not defined $config->{"finish-all-configurations"} + or $config->{"finish-all-configurations"} eq "No" ) + { + # let's stop the portfolio if finish all configs isn't set to yes in the YAML + last; + } + } + + } + + } + elsif ( $results{ $_->{name} } =~ /Verification SUCCESSFUL/ ) + { # nothing else to do, we're done, we found no problems + $successful = 1; + if ( not defined $config->{"finish-all-configurations"} + or $config->{"finish-all-configurations"} eq "No" ) + { + # let's stop the portfolio if finish all configs isn't set to yes in the YAML + last; + } + } + } +} + +sub list_results { + foreach (@configurations_arr_ref) { + if ( defined $results{ $_->{name} } ) { + Logger::log_minimal("Result of $_->{name}: $results{$_->{name}}"); + if ( defined $results{ $_->{name} . "-test-harness" } ) { + Logger::log_minimal( "Result of " + . $_->{name} + . "-test-harness" . ": " + . $results{ $_->{name} . "-test-harness" } ); + } + Logger::log_minimal(""); + } + } +} + +sub terminate() { + close_logfile(); + exit; +} diff --git a/scripts/portfolio/lib/Execute.pm b/scripts/portfolio/lib/Execute.pm new file mode 100644 index 00000000..bda22f82 --- /dev/null +++ b/scripts/portfolio/lib/Execute.pm @@ -0,0 +1,125 @@ +package Execute; +use strict; +use warnings; + +use FindBin qw($Bin); +use lib "$Bin/lib"; +use Options; +use Logger; + +use IO::Select; +use Proc::Killfam; + +sub run_command { + +# arguments: +# command +# timeout +# return_0 - if this is 1, the subroutine returns ERROR if the return_code wasn't 0 +# output format (optional) + my ( $command, $timeout, $return_0, $output_format ) = + @_; # defining parameters + my $result + ; # for storing the "Verification failed/successful/etc. output or TIMEOUT/ERROR/NONE" + + eval { # eval, so alarm can work as a timeout + # handling of timeout + my $pid; + my $fhandle; + local $SIG{TERM} = 'IGNORE' + ; # the script itself is part of the process group SIGTERM-d in case of a timeout + local $SIG{ALRM} = sub { + $result = "TIMEOUT"; + killfam( 'TERM', $pid ) unless ( not defined $pid ); + close $fhandle unless ( not defined $fhandle ); + die "\`$command\` timed out after ${timeout}sec"; + }; + $pid = open( $fhandle, '-|', $command ) + or die $!; # Open a pipe to read output from a command. + + alarm $timeout + ; # the timeout is evoked by alarm, which means, that we are counting walltime + # Note: if timeout value is 0 then there is no timeout set + + while ( my $line = <$fhandle> ) { + chomp($line); + Logger::log_verbose($line); + if ( defined $output_format and $line =~ /$output_format/ ) { + $result = $line; + } + } + Logger::log_verbose ""; + + alarm 0; # timeout wasn't reached, stop the timer + close $fhandle; + }; + + unless ( $return_0 eq 0 or $? eq 0 or $result = "TIMEOUT" ) { + $result = "ERROR"; + } + if ( not defined $result ) { + $result = "NONE"; + } + + # returns the output or TIMEOUT or ERROR + return $result; +} + +sub run_gazer { + + # arguments: + # tool: gazer-bmc or gazer-theta + # flags: string of flags + # timeout + my ( $config_name, $tool, $flags, $timeout ) = @_; # defining parameters + + my $command_string = + $Options::gazer_path . "/" + . $tool . "/" + . $tool . " " + . $Options::task_path_name . " " + . $flags + . " 2>&1"; # concatenating command + Logger::log_minimal "Running \`" . $command_string . "\`"; + + return run_command( $command_string, $timeout, 1, "Verification.*" ); +} + +sub check_harness { + +# arguments: +# harness compile +# execution timeout +# gazer output (the line, where the type of the problem is defined - div by zero, etc.) + my ( $compile_timeout, $test_timeout, $gazer_output ) = + @_; # defining arguments + + my $clang_command = +"clang $Options::task_path_name $Options::output_directory$Options::task_file_name.ll -o $Options::output_directory${Options::task_file_name}_test 2>&1" + ; # concatenating command + Logger::log_minimal "Running \`" . $clang_command . "\`"; + my $clang_result = run_command( $clang_command, $compile_timeout, 0 ); + + return "Test harness compilation " . $clang_result + unless ( $clang_result eq "NONE" ) + ; # if the compilation wasn't successful, return with the TIMEOUT/ERROR + +# reason for bash -c: if there is a signal without a handler (like an FPE), +# then the "Floating point exception(core dumped)" will be the output of bash, not the C program + my $test_command = +"bash -c \"${Options::output_directory}${Options::task_file_name}_test; true\" 2>&1"; + + # run test harness + Logger::log_minimal "Running \`" . $test_command . "\`"; + my $required_test_output = + "(Assertion(.)*failed)|(Floating point exception)"; + my $test_result = + run_command( $test_command, $test_timeout, 0, $required_test_output ); + if ( $test_result =~ $required_test_output ) { + return "Test harness SUCCESSFUL WITNESS"; + } + else { + return "Test harness WITNESS FAILED: " . $test_result; + } +} +1; diff --git a/scripts/portfolio/lib/Logger.pm b/scripts/portfolio/lib/Logger.pm new file mode 100644 index 00000000..3389f0cc --- /dev/null +++ b/scripts/portfolio/lib/Logger.pm @@ -0,0 +1,60 @@ +package Logger; +use strict; +use warnings; + +my $log; + +sub initialize_logfile { + my ($timestamp) = @_; + open( $log, ">>", "$Options::output_directory." / ".$timestamp.log" ) + or die "Can't open logfile: $!\nTerminating..."; +} + +sub close_logfile { + close($log); +} + +sub log_h1 { + + # string to log into file + my ($string) = @_; + print "\n-- " . $string . " --\n"; + print $log "\n-- " . $string . " --\n"; +} + +sub log_h2 { + + # string to log into file + my ($string) = @_; + print "\n" . $string . "\n"; + print $log "\n" . $string . "\n"; +} + +sub log_minimal { + + # string to log into file + my ($string) = @_; + print $string. "\n"; + print $log $string . "\n"; +} + +sub log_verbose { + + # string to log into file + my ($string) = @_; + if ( $Options::log_level eq "verbose" ) { + print $string. "\n"; + print $log $string . "\n"; + } +} + +sub log_debug { + + # string to log into file + my ($string) = @_; + if ( $Options::debug eq 1 ) { + print $string. "\n"; + print $log $string . "\n"; + } +} +1; diff --git a/scripts/portfolio/lib/Options.pm b/scripts/portfolio/lib/Options.pm new file mode 100644 index 00000000..b9adb50b --- /dev/null +++ b/scripts/portfolio/lib/Options.pm @@ -0,0 +1,137 @@ +package Options; +use strict; +use warnings; + +use Logger; + +use Getopt::Long; +use File::Basename; +use POSIX qw(strftime); +use Cwd; +use Cwd 'abs_path'; + +sub initialize_flags { + GetOptions( # the values of most options are globally accessible with the Options namespace + 'version' => \my $version, + 'configuration=s' => \$Options::config_path_name, # relative to wd + 'task=s' => \$Options::task_path_name, # relative to wd + 'output-directory=s' => \$Options::output_directory, # relative to wd + # log-levels: + # - minimal: lists the commands used, flow of executing the steps, results of configs, and the final result - nothing else, + # - (default) verbose: minimal + tool-output, + 'log-level=s' => \$Options::log_level, + +# if used, the script outputs more data about the workings of the script itself, e.g. directories used, config list, etc. for debugging purposes (but independent of log-level) + 'debug' => \$Options::debug + ) or die "Invalid options passed to $0\n"; + + if ( not defined $version ) { + lint_flags() + ; # check, if all required flags are present and the values of them are valid + my $wd = getcwd() . "/"; # get the working dir + $Options::task_path_name = + abs_path($Options::task_path_name); # use the absolute path + $Options::task_file_name = "/" + . basename($Options::task_path_name) + ; # we'll need the file name from the path as well + + # initialize output directory + my $iso8601_timestamp = strftime "%Y-%m-%dT%H:%M:%S", gmtime; + if ( not defined $Options::output_directory ) + { # if the output directory wasn't explicitly set, then we put it in wd/portfolio-output-timestamp/ + $Options::output_directory = + "${wd}portfolio-output-$iso8601_timestamp"; + } + else + { # if an output directory was given, than we create the portfolio-output-timestamp dir there + $Options::output_directory = + abs_path($Options::output_directory); # chop of /, if there is one + $Options::output_directory = $Options::output_directory + . "/portfolio-output-$iso8601_timestamp"; + } + `mkdir -p $Options::output_directory` + unless ( -d $Options::output_directory ) + ; # create output dir, if we need to + +# Logger only works after calling this subroutine, but puts logfile into output dir, so that part should be done already + Logger::initialize_logfile($iso8601_timestamp); + } + else { # --version received + print get_version() + ; # not logged but printed, as log is not initialized if --version was given - we don't really need to log this into a file + exit; + } +} + +sub initialize_gazer_path { + + # script_path: path to the scripts folder in the gazer project + my ($script_path) = @_; + my $gazer_path = abs_path( dirname( dirname( abs_path($script_path) ) ) ); + my $build_path = $gazer_path . "/build/tools"; + my $tools_path = $gazer_path . "/tools"; + if ( -d $build_path ) { + $Options::gazer_path = $build_path; + } + elsif ( -d $tools_path ) { + $Options::gazer_path = $tools_path; + } + else { + Logger::log_minimal( +"ERROR: Gazer tool directory gazer/build/tools or gazer/tools does not exist! Terminating..." + ); + terminate(); + + } +} + +sub get_version { # needs gazer_path to be initialized at this point + my $z3path = "$Options::gazer_path/gazer-theta/theta/lib"; + $ENV{"LD_LIBRARY_PATH"} = $z3path; + my $theta_version = +`java -Djava.library.path=$z3path -jar $Options::gazer_path/gazer-theta/theta/theta-cfa-cli.jar --version 2>&1`; + + my $gazer_version = + `$Options::gazer_path/gazer-bmc/gazer-bmc --version 2>&1` + ; # tool hardcoded, as all gazer tools output the same version + # print $gazer_version; + return "$gazer_version\nTheta v$theta_version"; +} + +sub lint_flags { + + # check if required flags are present + if ( not defined $Options::config_path_name ) { + die +"ERROR: YAML configuration file missing (use the flag --configuration/-c).\nTerminating..."; + } + elsif ( not defined $Options::task_path_name ) { + die + "ERROR: input file missing (use the flag --task/-t).\nTerminating..."; + } + + # check, if --log-level is present and initialize log level + if ( not defined $Options::log_level ) { # the default is verbose + $Options::log_level = "verbose"; + } + unless ( $Options::log_level eq "verbose" + or $Options::log_level eq "minimal" ) + { + die +"ERROR: Invalid log-level value (valid: minimal, verbose)\nTerminating..."; + } + +# check if -d/--debug was given (this outputs more information about the workings of the script - it is independent of the log-level used) + if ( not defined $Options::debug ) { + $Options::debug = 0; + } + + # check, if input and yml files exist + unless ( -f $Options::task_path_name ) { + die "ERROR: Task file does not exist!\nTerminating..."; + } + unless ( -f $Options::config_path_name ) { + die "ERROR: Configuration file does not exist!\nTerminating..."; + } +} +1; diff --git a/scripts/portfolio/test-configs/SVComp_configuration.yml b/scripts/portfolio/test-configs/SVComp_configuration.yml new file mode 100644 index 00000000..55f59be5 --- /dev/null +++ b/scripts/portfolio/test-configs/SVComp_configuration.yml @@ -0,0 +1,23 @@ +--- +generate-witness: Yes +finish-all-configurations: No + +check-harness: # should it be a local (/config) or global attribute? + execute-harness-timeout: 50 + compile-harness-timeout: 100 + +configurations: # list of configs to be run. For every configuration a tool is mandatory, all others have default values. + # tool valid values: gazer-bmc, gazer-theta + - name: bmc-inline + tool: gazer-bmc + timeout: 150 # sec + flags: --inline all --bound 1000000 + + - name: theta-expl + tool: gazer-theta + timeout: 100 # sec + flags: --search ERR --domain EXPL --maxenum 100 --refinement BW_BIN_ITP --initprec ALLVARS + + - name: theta-pred + tool: gazer-theta + flags: --inline all --search ERR --domain PRED_CART --refinement BW_BIN_ITP --initprec EMPTY diff --git a/scripts/portfolio/test-configs/SVComp_finish_all_configuration.yml b/scripts/portfolio/test-configs/SVComp_finish_all_configuration.yml new file mode 100644 index 00000000..fe963467 --- /dev/null +++ b/scripts/portfolio/test-configs/SVComp_finish_all_configuration.yml @@ -0,0 +1,23 @@ +--- +generate-witness: Yes +finish-all-configurations: Yes + +check-harness: # should it be a local (/config) or global attribute? + execute-harness-timeout: 50 + compile-harness-timeout: 100 + +configurations: # list of configs to be run. For every configuration a tool is mandatory, all others have default values. + # tool valid values: gazer-bmc, gazer-theta + - name: bmc-inline + tool: gazer-bmc + timeout: 150 # sec + flags: --inline all --bound 1000000 + + - name: theta-expl + tool: gazer-theta + timeout: 100 # sec + flags: --search ERR --domain EXPL --maxenum 100 --refinement BW_BIN_ITP --initprec ALLVARS + + - name: theta-pred + tool: gazer-theta + flags: --inline all --search ERR --domain PRED_CART --refinement BW_BIN_ITP --initprec EMPTY diff --git a/scripts/portfolio/test-configs/config-file-example.yml b/scripts/portfolio/test-configs/config-file-example.yml new file mode 100644 index 00000000..8fd0cd4b --- /dev/null +++ b/scripts/portfolio/test-configs/config-file-example.yml @@ -0,0 +1,24 @@ +--- +generate-witness: Yes +finish-all-configurations: No # if turned on, it will finish/kill after timeout all given configurations (possible endless loop!) +# Note: Currently finish all configs has no "final result" - it just lists the results from the configurations + +check-harness: # should it be a local (/config) or global attribute? + execute-harness-timeout: 200 + compile-harness-timeout: 150 + +configurations: # list of configs to be run. For every configuration a tool is mandatory, all others have default values. + # tool valid values: gazer-bmc, gazer-theta + - name: config1 + tool: gazer-bmc + timeout: 10 # sec + + - name: config2 + tool: gazer-bmc + timeout: 1 # sec + flags: --inline all --bound 1000000 + + - name: config3 + tool: gazer-theta + timeout: 100 # sec + flags: --domain EXPL --search ERR diff --git a/scripts/portfolio/test-configs/small_timeout.yml b/scripts/portfolio/test-configs/small_timeout.yml new file mode 100644 index 00000000..ff3723cb --- /dev/null +++ b/scripts/portfolio/test-configs/small_timeout.yml @@ -0,0 +1,17 @@ +--- +generate-witness: Yes +finish-all-configurations: No # if turned on, it will finish/kill after timeout all given configurations (possible endless loop!) +# Note: Currently finish all configs has no "final result" - it just lists the results from the configurations + +check-harness: # should it be a local (/config) or global attribute? + execute-harness-timeout: 200 + compile-harness-timeout: 150 + +configurations: + - name: config2 + tool: gazer-bmc + timeout: 5 # sec + - name: config3 + tool: gazer-theta + timeout: 5 # sec + flags: --domain EXPL --search ERR diff --git a/scripts/portfolio/test-tasks/Problem01_label02.c b/scripts/portfolio/test-tasks/Problem01_label02.c new file mode 100644 index 00000000..d039dadb --- /dev/null +++ b/scripts/portfolio/test-tasks/Problem01_label02.c @@ -0,0 +1,611 @@ +// RUN: %portfolio -c small_timeout.yml -t "%s" -l minimal | FileCheck "%s" + +// CHECK: -- 3. Evaluating Results -- +// CHECK-NEXT: Result of config2: TIMEOUT +// CHECK-NEXT: Result of config3: TIMEOUT +// CHECK-NEXT: Final result of portfolio: NONE + +// This file is part of the SV-Benchmarks collection of verification tasks: +// https://github.com/sosy-lab/sv-benchmarks +// +// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community +// SPDX-FileCopyrightText: 2012 The RERS Challenge +// +// SPDX-License-Identifier: Apache-2.0 + +int calculate_output(int); +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); +void reach_error() { __assert_fail("0", "Problem01_label02.c", 4, "reach_error"); } +extern int __VERIFIER_nondet_int(void); +extern void exit(int); + + // inputs + int a= 1; + int d= 4; + int e= 5; + int f= 6; + int c= 3; + int b= 2; + + // outputs + int u = 21; + int v = 22; + int w = 23; + int x = 24; + int y = 25; + int z = 26; + + int a17 = 1; + int a7 = 0; + int a20 = 1; + int a8 = 15; + int a12 = 8; + int a16 = 5; + int a21 = 1; + + int calculate_output(int input) { + if((((a8==15)&&(((((a21==1)&&(((a16==5)||(a16==6))&&(input==1)))&&(a20==1))&&(a17==1))&&!(a7==1)))&&(a12==8))){ + a16 = 5; + a20 = 0; + return 24; + } else if((((((((input==5)&&((((a16==6)&&(a17==1))||(!(a17==1)&&(a16==4)))||(!(a17==1)&&(a16==5))))&&(a20==1))&&(a12==8))&&(a7==1))&&!(a21==1))&&(a8==13))){ + a20 = 0; + a16 = 6; + a17 = 0; + a8 = 15; + a7 = 0; + a21 = 1; + return 26; + } else if(((!(a7==1)&&((((a16==6)&&((a21==1)&&((a17==1)&&(input==3))))&&!(a20==1))&&(a8==15)))&&(a12==8))){ + a20 = 1; + a16 = 4; + a7 = 1; + a8 = 13; + return -1; + } else if(((a17==1)&&((!(a7==1)&&(((a21==1)&&((((a16==5)||(a16==6))&&(input==6))&&(a20==1)))&&(a8==15)))&&(a12==8)))){ + a8 = 13; + a7 = 1; + a16 = 4; + return -1; + } else if((((input==3)&&((((a16==6)&&((!(a20==1)&&(!(a7==1)&&!(a17==1)))&&(a8==15)))&&(a21==1))||((((a8==13)&&((a20==1)&&((a17==1)&&(a7==1))))&&(a16==4))&&!(a21==1))))&&(a12==8))){ + a7 = 0; + a20 = 1; + a21 = 1; + a16 = 4; + a17 = 1; + a8 = 13; + return -1; + } else if((((a17==1)&&(((a21==1)&&((!(a7==1)&&((input==4)&&(a8==15)))&&!(a20==1)))&&(a12==8)))&&(a16==6))){ + a17 = 0; + return 26; + } else if((((a12==8)&&(((a21==1)&&((((input==5)&&!(a7==1))&&(a8==15))&&(a16==5)))&&!(a20==1)))&&!(a17==1))){ + a7 = 1; + a16 = 4; + a8 = 13; + a20 = 1; + a17 = 1; + return -1; + } else if(((a12==8)&&((input==1)&&(((a21==1)&&(((a8==15)&&((!(a17==1)&&!(a7==1))&&!(a20==1)))&&(a16==6)))||(!(a21==1)&&((a16==4)&&((a8==13)&&(((a17==1)&&(a7==1))&&(a20==1))))))))){ + a7 = 1; + a17 = 1; + a21 = 0; + a20 = 1; + a8 = 13; + a16 = 5; + return 26; + } else if(((((!(a17==1)&&(!(a7==1)&&((a21==1)&&((a8==15)&&(input==4)))))&&!(a20==1))&&(a12==8))&&(a16==4))){ + a17 = 1; + a16 = 5; + return 21; + } else if(((((((a16==6)&&((!(a20==1)&&(!(a17==1)&&!(a7==1)))&&(a8==15)))&&(a21==1))||(((a16==4)&&(((a20==1)&&((a17==1)&&(a7==1)))&&(a8==13)))&&!(a21==1)))&&(input==2))&&(a12==8))){ + a7 = 0; + a20 = 1; + a8 = 14; + a16 = 4; + a21 = 1; + a17 = 0; + return -1; + } else if(((a8==13)&&(!(a21==1)&&((((input==3)&&((((a20==1)&&!(a17==1))&&(a16==6))||((!(a20==1)&&(a17==1))&&(a16==4))))&&(a12==8))&&(a7==1))))){ + a16 = 4; + a17 = 1; + a20 = 1; + return 26; + } else if(((((a21==1)&&((a12==8)&&((input==1)&&(((!(a20==1)&&(a17==1))&&(a16==4))||(((a16==5)&&(!(a17==1)&&(a20==1)))||((a16==6)&&(!(a17==1)&&(a20==1))))))))&&!(a7==1))&&(a8==15))){ + a16 = 6; + a20 = 1; + a17 = 0; + return 24; + } else if((((a16==5)&&(((a7==1)&&((!(a21==1)&&((a12==8)&&(input==3)))&&(a8==13)))&&(a17==1)))&&(a20==1))){ + a20 = 0; + a8 = 15; + a17 = 0; + a21 = 1; + return -1; + } else if(((a17==1)&&(((a8==15)&&(((a12==8)&&((!(a7==1)&&(input==5))&&(a21==1)))&&!(a20==1)))&&(a16==5)))){ + a20 = 1; + a8 = 13; + a7 = 1; + a16 = 4; + return -1; + } else if((!(a7==1)&&(((((a21==1)&&(((a8==15)&&(input==5))&&!(a17==1)))&&(a12==8))&&(a20==1))&&(a16==4)))){ + a8 = 13; + a17 = 1; + a7 = 1; + return -1; + } else if(((!(a21==1)&&(((a12==8)&&((((a16==6)&&((a20==1)&&!(a17==1)))||((!(a20==1)&&(a17==1))&&(a16==4)))&&(input==1)))&&(a8==13)))&&(a7==1))){ + a16 = 6; + a20 = 1; + a17 = 0; + return -1; + } else if(((a17==1)&&(!(a7==1)&&(((a21==1)&&(((a12==8)&&((input==5)&&((a16==5)||(a16==6))))&&(a20==1)))&&(a8==15))))){ + a7 = 1; + a16 = 4; + a8 = 13; + return -1; + } else if((((a12==8)&&(!(a21==1)&&((a7==1)&&((a8==13)&&((input==6)&&((((a16==6)&&(a17==1))||((a16==4)&&!(a17==1)))||((a16==5)&&!(a17==1))))))))&&(a20==1))){ + a8 = 15; + a17 = 0; + a21 = 1; + a20 = 0; + a16 = 4; + return -1; + } else if((((a16==5)&&((((a8==15)&&((!(a7==1)&&(input==2))&&(a21==1)))&&(a12==8))&&!(a20==1)))&&!(a17==1))){ + a16 = 4; + a17 = 1; + return 24; + } else if((!(a20==1)&&((a21==1)&&((a16==4)&&((a8==15)&&(((a12==8)&&((input==2)&&!(a7==1)))&&!(a17==1))))))){ + a17 = 1; + a16 = 5; + return 21; + } else if((((a21==1)&&(!(a7==1)&&((!(a20==1)&&(!(a17==1)&&((a12==8)&&(input==6))))&&(a16==4))))&&(a8==15))){ + a20 = 1; + a16 = 6; + return 22; + } else if(((a17==1)&&((((((a12==8)&&((input==4)&&(a8==13)))&&(a20==1))&&!(a21==1))&&(a16==5))&&(a7==1)))){ + a16 = 4; + a17 = 0; + return 25; + } else if(((((a8==13)&&((a12==8)&&((((((a16==6)&&(a17==1))||(!(a17==1)&&(a16==4)))||(!(a17==1)&&(a16==5)))&&(input==1))&&!(a21==1))))&&(a20==1))&&(a7==1))){ + a8 = 15; + a16 = 6; + a21 = 1; + a20 = 0; + a7 = 0; + a17 = 1; + return -1; + } else if(((a8==13)&&(!(a21==1)&&((((((!(a17==1)&&(a20==1))&&(a16==6))||((a16==4)&&((a17==1)&&!(a20==1))))&&(input==5))&&(a7==1))&&(a12==8))))){ + a17 = 1; + a20 = 0; + a16 = 4; + return 25; + } else if(((!(a21==1)&&((((((a16==6)&&((a20==1)&&!(a17==1)))||(((a17==1)&&!(a20==1))&&(a16==4)))&&(input==4))&&(a7==1))&&(a12==8)))&&(a8==13))){ + a8 = 15; + a21 = 1; + a20 = 0; + a7 = 0; + a16 = 6; + a17 = 0; + return 26; + } else if((((a21==1)&&(!(a7==1)&&((((((a16==5)&&((a20==1)&&!(a17==1)))||((!(a17==1)&&(a20==1))&&(a16==6)))||((a16==4)&&((a17==1)&&!(a20==1))))&&(input==4))&&(a12==8))))&&(a8==15))){ + a16 = 4; + a20 = 0; + a17 = 0; + return 24; + } else if(((((((a16==6)&&((!(a20==1)&&(!(a17==1)&&!(a7==1)))&&(a8==15)))&&(a21==1))||(((a16==4)&&((((a7==1)&&(a17==1))&&(a20==1))&&(a8==13)))&&!(a21==1)))&&(input==4))&&(a12==8))){ + a17 = 0; + a16 = 5; + a21 = 1; + a8 = 14; + a7 = 1; + a20 = 1; + return -1; + } else if((!(a17==1)&&(((a12==8)&&(!(a20==1)&&(((a8==15)&&((a21==1)&&(input==4)))&&!(a7==1))))&&(a16==5)))){ + a17 = 1; + return 24; + } else if((((!(a7==1)&&(((input==2)&&((((a16==5)&&((a20==1)&&!(a17==1)))||((a16==6)&&((a20==1)&&!(a17==1))))||((a16==4)&&(!(a20==1)&&(a17==1)))))&&(a8==15)))&&(a12==8))&&(a21==1))){ + a17 = 0; + a16 = 5; + a20 = 1; + return 25; + } else if((!(a20==1)&&(((((((input==6)&&(a16==5))&&(a21==1))&&!(a17==1))&&(a12==8))&&!(a7==1))&&(a8==15)))){ + a17 = 1; + return 24; + } else if(((a12==8)&&(((((((a21==1)&&(input==5))&&(a8==15))&&(a17==1))&&!(a7==1))&&!(a20==1))&&(a16==6)))){ + a20 = 1; + a16 = 4; + a7 = 1; + a8 = 13; + return -1; + } else if(((((a8==15)&&(!(a7==1)&&((((!(a20==1)&&(a17==1))&&(a16==4))||(((!(a17==1)&&(a20==1))&&(a16==5))||((a16==6)&&((a20==1)&&!(a17==1)))))&&(input==6))))&&(a12==8))&&(a21==1))){ + a20 = 0; + a17 = 1; + a16 = 4; + return 22; + } else if(((a8==15)&&((a16==4)&&(!(a20==1)&&((((a21==1)&&(!(a17==1)&&(input==5)))&&!(a7==1))&&(a12==8)))))){ + a7 = 1; + a8 = 13; + a17 = 1; + a20 = 1; + return -1; + } else if(((a17==1)&&((a12==8)&&((a8==15)&&(((!(a7==1)&&(((a16==5)||(a16==6))&&(input==2)))&&(a21==1))&&(a20==1)))))){ + a17 = 0; + a16 = 6; + return 22; + } else if((!(a7==1)&&(((a8==15)&&((!(a17==1)&&((a12==8)&&((input==3)&&(a21==1))))&&(a16==4)))&&(a20==1)))){ + a17 = 1; + a7 = 1; + a8 = 13; + return -1; + } else if(((a16==5)&&((!(a21==1)&&(((a8==13)&&(((input==2)&&(a20==1))&&(a12==8)))&&(a7==1)))&&(a17==1)))){ + a21 = 1; + a8 = 14; + a16 = 4; + a20 = 0; + a7 = 0; + a17 = 0; + return -1; + } else if(((a20==1)&&(((a12==8)&&((a7==1)&&((a8==13)&&(((!(a17==1)&&(a16==5))||(((a17==1)&&(a16==6))||(!(a17==1)&&(a16==4))))&&(input==3)))))&&!(a21==1)))){ + a8 = 14; + a7 = 0; + a17 = 1; + a21 = 1; + a16 = 4; + return -1; + } else if(((a12==8)&&((a7==1)&&(!(a21==1)&&((a8==13)&&((input==6)&&(((a16==6)&&((a20==1)&&!(a17==1)))||((a16==4)&&((a17==1)&&!(a20==1)))))))))){ + a20 = 0; + a21 = 1; + a17 = 0; + a8 = 14; + a16 = 4; + return -1; + } else if(((!(a7==1)&&(!(a17==1)&&((((a16==4)&&((a8==15)&&(input==1)))&&(a12==8))&&(a21==1))))&&(a20==1))){ + a7 = 1; + a8 = 13; + a17 = 1; + return -1; + } else if(((a17==1)&&(((a21==1)&&(!(a20==1)&&((a12==8)&&((a8==15)&&(!(a7==1)&&(input==1))))))&&(a16==6)))){ + a20 = 1; + a8 = 13; + a7 = 1; + a16 = 4; + return -1; + } else if(((a20==1)&&((a12==8)&&((((a17==1)&&((((a16==5)||(a16==6))&&(input==4))&&(a8==15)))&&(a21==1))&&!(a7==1))))){ + a16 = 4; + a7 = 1; + a8 = 13; + return -1; + } else if(((((a8==13)&&((((!(a21==1)&&(input==6))&&(a20==1))&&(a12==8))&&(a17==1)))&&(a7==1))&&(a16==5))){ + a16 = 4; + a20 = 0; + return 25; + } else if(((a16==5)&&(((((a12==8)&&(!(a7==1)&&((input==2)&&!(a20==1))))&&(a21==1))&&(a17==1))&&(a8==15)))){ + a17 = 0; + return 24; + } else if((((a12==8)&&(((!(a17==1)&&((a21==1)&&((input==4)&&!(a7==1))))&&(a8==15))&&(a20==1)))&&(a16==4))){ + a20 = 0; + a17 = 1; + a16 = 6; + return 21; + } else if(((a7==1)&&((a8==13)&&((a12==8)&&(!(a21==1)&&((input==2)&&((((a20==1)&&!(a17==1))&&(a16==6))||(((a17==1)&&!(a20==1))&&(a16==4))))))))){ + a16 = 4; + a20 = 0; + a17 = 1; + return -1; + } else if((((((((!(a20==1)&&(!(a17==1)&&!(a7==1)))&&(a8==15))&&(a16==6))&&(a21==1))||((((a8==13)&&(((a17==1)&&(a7==1))&&(a20==1)))&&(a16==4))&&!(a21==1)))&&(input==6))&&(a12==8))){ + a20 = 1; + a8 = 13; + a16 = 4; + a7 = 0; + a21 = 1; + a17 = 0; + return -1; + } else if(((!(a7==1)&&(!(a17==1)&&(((((input==3)&&(a21==1))&&(a16==4))&&(a8==15))&&(a12==8))))&&!(a20==1))){ + a17 = 1; + a7 = 1; + a8 = 13; + a20 = 1; + return -1; + } else if((((((a12==8)&&(((((a17==1)&&!(a20==1))&&(a16==4))||((((a20==1)&&!(a17==1))&&(a16==5))||((!(a17==1)&&(a20==1))&&(a16==6))))&&(input==3)))&&(a8==15))&&(a21==1))&&!(a7==1))){ + a16 = 4; + a17 = 1; + a8 = 13; + a20 = 1; + a7 = 1; + return -1; + } else if((((!(a7==1)&&(((input==5)&&((((a16==5)&&(!(a17==1)&&(a20==1)))||((a16==6)&&((a20==1)&&!(a17==1))))||((a16==4)&&(!(a20==1)&&(a17==1)))))&&(a12==8)))&&(a21==1))&&(a8==15))){ + a16 = 4; + a17 = 1; + a7 = 1; + a20 = 1; + a8 = 13; + return -1; + } else if(((!(a7==1)&&(((a21==1)&&(((a17==1)&&((a12==8)&&(input==2)))&&!(a20==1)))&&(a16==6)))&&(a8==15))){ + a8 = 13; + a20 = 1; + a16 = 4; + a7 = 1; + return -1; + } else if(((!(a17==1)&&((a21==1)&&((!(a20==1)&&((a12==8)&&((input==3)&&!(a7==1))))&&(a8==15))))&&(a16==5))){ + a8 = 13; + a16 = 4; + return -1; + } else if((((a16==5)&&(!(a20==1)&&(((((input==6)&&(a21==1))&&(a17==1))&&!(a7==1))&&(a12==8))))&&(a8==15))){ + return 24; + } else if((!(a7==1)&&((a17==1)&&(((a16==6)&&(!(a20==1)&&(((input==6)&&(a12==8))&&(a21==1))))&&(a8==15))))){ + a7 = 1; + a8 = 13; + a20 = 1; + a16 = 4; + return -1; + } else if(((((a21==1)&&((a8==15)&&((a12==8)&&(!(a7==1)&&(!(a17==1)&&(input==2))))))&&(a16==4))&&(a20==1))){ + a17 = 1; + a8 = 13; + a7 = 1; + return -1; + } else if(((a8==15)&&(((a16==4)&&((a12==8)&&((!(a20==1)&&(!(a7==1)&&(input==1)))&&!(a17==1))))&&(a21==1)))){ + a16 = 6; + a20 = 1; + return 22; + } else if(((a21==1)&&(((a12==8)&&((((a17==1)&&((input==3)&&((a16==5)||(a16==6))))&&!(a7==1))&&(a20==1)))&&(a8==15)))){ + a17 = 0; + a16 = 4; + return 21; + } else if((!(a21==1)&&((a20==1)&&(((a12==8)&&((a8==13)&&((((a16==5)&&!(a17==1))||(((a17==1)&&(a16==6))||(!(a17==1)&&(a16==4))))&&(input==2))))&&(a7==1))))){ + a21 = 1; + a8 = 15; + a17 = 1; + a7 = 0; + a16 = 6; + a20 = 0; + return -1; + } else if(((a7==1)&&((a12==8)&&((((a20==1)&&(((!(a17==1)&&(a16==5))||(((a17==1)&&(a16==6))||((a16==4)&&!(a17==1))))&&(input==4)))&&(a8==13))&&!(a21==1))))){ + a8 = 15; + a16 = 6; + a21 = 1; + a7 = 0; + a20 = 0; + a17 = 0; + return 26; + } else if(((a21==1)&&((((!(a7==1)&&((a8==15)&&(!(a20==1)&&(input==4))))&&(a17==1))&&(a16==5))&&(a12==8)))){ + return 24; + } else if((((!(a7==1)&&((!(a20==1)&&((a21==1)&&((input==3)&&(a17==1))))&&(a8==15)))&&(a12==8))&&(a16==5))){ + a20 = 1; + a8 = 13; + a7 = 1; + a16 = 4; + return -1; + } else if(((((!(a17==1)&&(!(a20==1)&&((a8==15)&&((input==1)&&(a16==5)))))&&(a12==8))&&(a21==1))&&!(a7==1))){ + return -1; + } else if(((((a21==1)&&((a8==15)&&(((a16==5)&&((a12==8)&&(input==1)))&&(a17==1))))&&!(a7==1))&&!(a20==1))){ + return 21; + } else if(((!(a21==1)&&((a20==1)&&((((a8==13)&&((a7==1)&&(input==5)))&&(a17==1))&&(a12==8))))&&(a16==5))){ + a21 = 1; + a7 = 0; + a17 = 0; + a8 = 14; + a20 = 0; + return -1; + } else if((((!(a7==1)&&((a21==1)&&((((input==6)&&(a20==1))&&(a8==15))&&!(a17==1))))&&(a12==8))&&(a16==4))){ + a7 = 1; + a8 = 13; + a17 = 1; + return -1; + } else if(((((a20==1)&&(((!(a21==1)&&((a7==1)&&(input==1)))&&(a8==13))&&(a17==1)))&&(a12==8))&&(a16==5))){ + a21 = 1; + a16 = 6; + a7 = 0; + return -1; + } else if(((a12==8)&&((input==5)&&((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==15))&&(a16==6))&&(a21==1))||(!(a21==1)&&((a16==4)&&(((a20==1)&&((a7==1)&&(a17==1)))&&(a8==13)))))))){ + a20 = 0; + a21 = 1; + a8 = 14; + a17 = 0; + a16 = 5; + a7 = 1; + return -1; + } + if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_20: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_47: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==15))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_32: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_37: exit(0); + } + if(((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_56: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==15))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_33: exit(0); + } + if(((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_57: exit(0); + } + if(((((((!(a17==1)&&!(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_50: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_35: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_15: exit(0); + } + if(((((((!(a17==1)&&!(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_38: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_21: exit(0); + } + if(((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_44: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_41: exit(0); + } + if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_19: exit(0); + } + if(((((((!(a17==1)&&!(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_40: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_27: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_59: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_2: {reach_error();abort();} + } + if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_1: exit(0); + } + if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==15))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_31: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_28: exit(0); + } + if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_5: exit(0); + } + if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_23: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_4: exit(0); + } + if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){ + globalError: exit(0); + } + if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_24: exit(0); + } + if(((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_58: exit(0); + } + if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_18: exit(0); + } + if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==15))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_29: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_36: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_26: exit(0); + } + if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_7: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==15))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_34: exit(0); + } + if(((((((!(a17==1)&&!(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_51: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_49: exit(0); + } + if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_0: exit(0); + } + if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_11: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_10: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_55: exit(0); + } + if(((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_46: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_8: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_53: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_42: exit(0); + } + if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_17: exit(0); + } + if(((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_45: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_9: exit(0); + } + if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_25: exit(0); + } + if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_12: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_48: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_54: exit(0); + } + if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_13: exit(0); + } + if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_6: exit(0); + } + if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==15))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_30: exit(0); + } + if(((((((!(a17==1)&&!(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_52: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_22: exit(0); + } + if((((((((a17==1)&&!(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_43: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_3: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){ + error_16: exit(0); + } + if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){ + error_14: exit(0); + } + if(((((((!(a17==1)&&!(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){ + error_39: exit(0); + } + return -2; + } + +int main() +{ + // default output + int output = -1; + + // main i/o-loop + while(1) + { + // read input + int input; + input = __VERIFIER_nondet_int(); + if ((input != 1) && (input != 2) && (input != 3) && (input != 4) && (input != 5) && (input != 6)) return -2; + + // operate eca engine + output = calculate_output(input); + + } +} diff --git a/scripts/portfolio/test-tasks/overflow_example.c b/scripts/portfolio/test-tasks/overflow_example.c new file mode 100644 index 00000000..7f3c551b --- /dev/null +++ b/scripts/portfolio/test-tasks/overflow_example.c @@ -0,0 +1,10 @@ +#include + +int main(void) { + int k = 2147483643; + k+=5; + + printf("%d\n", k); + + return 0; +} diff --git a/scripts/portfolio/test-tasks/test_locks_14-2.c b/scripts/portfolio/test-tasks/test_locks_14-2.c new file mode 100644 index 00000000..e2ab5699 --- /dev/null +++ b/scripts/portfolio/test-tasks/test_locks_14-2.c @@ -0,0 +1,223 @@ +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); +void reach_error() { __assert_fail("0", "test_locks_14-2.c", 3, "reach_error"); } + +extern int __VERIFIER_nondet_int(); +int main() +{ + int p1 = __VERIFIER_nondet_int(); // condition variable + int lk1; // lock variable + + int p2 = __VERIFIER_nondet_int(); // condition variable + int lk2; // lock variable + + int p3 = __VERIFIER_nondet_int(); // condition variable + int lk3; // lock variable + + int p4 = __VERIFIER_nondet_int(); // condition variable + int lk4; // lock variable + + int p5 = __VERIFIER_nondet_int(); // condition variable + int lk5; // lock variable + + int p6 = __VERIFIER_nondet_int(); // condition variable + int lk6; // lock variable + + int p7 = __VERIFIER_nondet_int(); // condition variable + int lk7; // lock variable + + int p8 = __VERIFIER_nondet_int(); // condition variable + int lk8; // lock variable + + int p9 = __VERIFIER_nondet_int(); // condition variable + int lk9; // lock variable + + int p10 = __VERIFIER_nondet_int(); // condition variable + int lk10; // lock variable + + int p11 = __VERIFIER_nondet_int(); // condition variable + int lk11; // lock variable + + int p12 = __VERIFIER_nondet_int(); // condition variable + int lk12; // lock variable + + int p13 = __VERIFIER_nondet_int(); // condition variable + int lk13; // lock variable + + int p14 = __VERIFIER_nondet_int(); // condition variable + int lk14; // lock variable + + + int cond; + + while(1) { + cond = __VERIFIER_nondet_int(); + if (cond == 0) { + goto out; + } else {} + lk1 = 0; // initially lock is open + + lk2 = 0; // initially lock is open + + lk3 = 0; // initially lock is open + + lk4 = 0; // initially lock is open + + lk5 = 0; // initially lock is open + + lk6 = 0; // initially lock is open + + lk7 = 0; // initially lock is open + + lk8 = 0; // initially lock is open + + lk9 = 0; // initially lock is open + + lk10 = 0; // initially lock is open + + lk11 = 0; // initially lock is open + + lk12 = 0; // initially lock is open + + lk13 = 0; // initially lock is open + + lk14 = 0; // initially lock is open + + + // lock phase + if (p1 != 0) { + lk1 = 1; // acquire lock + } else {} + + if (p2 != 0) { + lk2 = 1; // acquire lock + } else {} + + if (p3 != 0) { + lk3 = 1; // acquire lock + } else {} + + if (p4 != 0) { + lk4 = 1; // acquire lock + } else {} + + if (p5 != 0) { + lk5 = 1; // acquire lock + } else {} + + if (p6 != 0) { + lk6 = 1; // acquire lock + } else {} + + if (p7 != 0) { + lk7 = 1; // acquire lock + } else {} + + if (p8 != 0) { + lk8 = 1; // acquire lock + } else {} + + if (p9 != 0) { + lk9 = 1; // acquire lock + } else {} + + if (p10 != 0) { + lk10 = 1; // acquire lock + } else {} + + if (p11 != 0) { + lk11 = 1; // acquire lock + } else {} + + if (p12 != 0) { + lk12 = 1; // acquire lock + } else {} + + if (p13 != 0) { + lk13 = 1; // acquire lock + } else {} + + if (p14 != 0) { + lk14 = 1; // acquire lock + } else {} + + + // unlock phase + if (p1 != 0) { + if (lk1 != 1) goto ERROR; // assertion failure + lk1 = 0; + } else {} + + if (p2 != 0) { + if (lk2 != 1) goto ERROR; // assertion failure + lk2 = 0; + } else {goto ERROR;} + + if (p3 != 0) { + if (lk3 != 1) goto ERROR; // assertion failure + lk3 = 0; + } else {} + + if (p4 != 0) { + if (lk4 != 1) goto ERROR; // assertion failure + lk4 = 0; + } else {} + + if (p5 != 0) { + if (lk5 != 1) goto ERROR; // assertion failure + lk5 = 0; + } else {} + + if (p6 != 0) { + if (lk6 != 1) goto ERROR; // assertion failure + lk6 = 0; + } else {} + + if (p7 != 0) { + if (lk7 != 1) goto ERROR; // assertion failure + lk7 = 0; + } else {} + + if (p8 != 0) { + if (lk8 != 1) goto ERROR; // assertion failure + lk8 = 0; + } else {} + + if (p9 != 0) { + if (lk9 != 1) goto ERROR; // assertion failure + lk9 = 0; + } else {} + + if (p10 != 0) { + if (lk10 != 1) goto ERROR; // assertion failure + lk10 = 0; + } else {} + + if (p11 != 0) { + if (lk11 != 1) goto ERROR; // assertion failure + lk11 = 0; + } else {} + + if (p12 != 0) { + if (lk12 != 1) goto ERROR; // assertion failure + lk12 = 0; + } else {} + + if (p13 != 0) { + if (lk13 != 1) goto ERROR; // assertion failure + lk13 = 0; + } else {} + + if (p14 != 0) { + if (lk14 != 1) goto ERROR; // assertion failure + lk14 = 0; + } else {goto ERROR;} + + } + out: + return 0; + ERROR: {reach_error();abort();} + return 0; +} + + diff --git a/scripts/portfolio/test-tasks/zerodiv_example.c b/scripts/portfolio/test-tasks/zerodiv_example.c new file mode 100644 index 00000000..c0f9e343 --- /dev/null +++ b/scripts/portfolio/test-tasks/zerodiv_example.c @@ -0,0 +1,19 @@ +#include + +extern int ioread32(void); + +int main(void) { + int k = ioread32(); + int i = 0; + int j = k + 5; + while (i < 3) { + i = i + 1; + j = j + 3; + } + + k = k / (i - j); + + printf("%d\n", k); + + return 0; +} \ No newline at end of file diff --git a/test/portfolio/SVComp_configuration.yml b/test/portfolio/SVComp_configuration.yml new file mode 100644 index 00000000..55f59be5 --- /dev/null +++ b/test/portfolio/SVComp_configuration.yml @@ -0,0 +1,23 @@ +--- +generate-witness: Yes +finish-all-configurations: No + +check-harness: # should it be a local (/config) or global attribute? + execute-harness-timeout: 50 + compile-harness-timeout: 100 + +configurations: # list of configs to be run. For every configuration a tool is mandatory, all others have default values. + # tool valid values: gazer-bmc, gazer-theta + - name: bmc-inline + tool: gazer-bmc + timeout: 150 # sec + flags: --inline all --bound 1000000 + + - name: theta-expl + tool: gazer-theta + timeout: 100 # sec + flags: --search ERR --domain EXPL --maxenum 100 --refinement BW_BIN_ITP --initprec ALLVARS + + - name: theta-pred + tool: gazer-theta + flags: --inline all --search ERR --domain PRED_CART --refinement BW_BIN_ITP --initprec EMPTY diff --git a/test/portfolio/SVComp_finish_all_configuration.yml b/test/portfolio/SVComp_finish_all_configuration.yml new file mode 100644 index 00000000..fe963467 --- /dev/null +++ b/test/portfolio/SVComp_finish_all_configuration.yml @@ -0,0 +1,23 @@ +--- +generate-witness: Yes +finish-all-configurations: Yes + +check-harness: # should it be a local (/config) or global attribute? + execute-harness-timeout: 50 + compile-harness-timeout: 100 + +configurations: # list of configs to be run. For every configuration a tool is mandatory, all others have default values. + # tool valid values: gazer-bmc, gazer-theta + - name: bmc-inline + tool: gazer-bmc + timeout: 150 # sec + flags: --inline all --bound 1000000 + + - name: theta-expl + tool: gazer-theta + timeout: 100 # sec + flags: --search ERR --domain EXPL --maxenum 100 --refinement BW_BIN_ITP --initprec ALLVARS + + - name: theta-pred + tool: gazer-theta + flags: --inline all --search ERR --domain PRED_CART --refinement BW_BIN_ITP --initprec EMPTY diff --git a/test/portfolio/lit.local.cfg b/test/portfolio/lit.local.cfg new file mode 100644 index 00000000..632fa995 --- /dev/null +++ b/test/portfolio/lit.local.cfg @@ -0,0 +1,13 @@ +# -*- Python -*- + +import lit + +try: + gazer_tools_dir = os.path.abspath(os.environ['GAZER_TOOLS_DIR']) +except KeyError: + lit_config.fatal('Missing GAZER_TOOLS_DIR environment variable.') + +config.environment['GAZER_TOOLS_DIR'] = gazer_tools_dir + +scripts_path = gazer_tools_dir.rsplit("/gazer/", 1)[0] + "/gazer/scripts/portfolio/Portfolio.pl" +config.substitutions.append(('%portfolio', scripts_path)) diff --git a/test/portfolio/small_timeout.yml b/test/portfolio/small_timeout.yml new file mode 100644 index 00000000..ff3723cb --- /dev/null +++ b/test/portfolio/small_timeout.yml @@ -0,0 +1,17 @@ +--- +generate-witness: Yes +finish-all-configurations: No # if turned on, it will finish/kill after timeout all given configurations (possible endless loop!) +# Note: Currently finish all configs has no "final result" - it just lists the results from the configurations + +check-harness: # should it be a local (/config) or global attribute? + execute-harness-timeout: 200 + compile-harness-timeout: 150 + +configurations: + - name: config2 + tool: gazer-bmc + timeout: 5 # sec + - name: config3 + tool: gazer-theta + timeout: 5 # sec + flags: --domain EXPL --search ERR diff --git a/test/portfolio/test_locks_14-2.c b/test/portfolio/test_locks_14-2.c new file mode 100644 index 00000000..9dcec9ec --- /dev/null +++ b/test/portfolio/test_locks_14-2.c @@ -0,0 +1,227 @@ +// RUN: %portfolio -c "%S"/SVComp_configuration.yml -l minimal -t "%s" -o /tmp | FileCheck "%s" + +// CHECK: Result of bmc-inline: Verification FAILED. +// CHECK-NEXT: Result of bmc-inline-test-harness: Test harness SUCCESSFUL WITNESS +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); +void reach_error() { __assert_fail("0", "test_locks_14-2.c", 3, "reach_error"); } + +extern int __VERIFIER_nondet_int(); +int main() +{ + int p1 = __VERIFIER_nondet_int(); // condition variable + int lk1; // lock variable + + int p2 = __VERIFIER_nondet_int(); // condition variable + int lk2; // lock variable + + int p3 = __VERIFIER_nondet_int(); // condition variable + int lk3; // lock variable + + int p4 = __VERIFIER_nondet_int(); // condition variable + int lk4; // lock variable + + int p5 = __VERIFIER_nondet_int(); // condition variable + int lk5; // lock variable + + int p6 = __VERIFIER_nondet_int(); // condition variable + int lk6; // lock variable + + int p7 = __VERIFIER_nondet_int(); // condition variable + int lk7; // lock variable + + int p8 = __VERIFIER_nondet_int(); // condition variable + int lk8; // lock variable + + int p9 = __VERIFIER_nondet_int(); // condition variable + int lk9; // lock variable + + int p10 = __VERIFIER_nondet_int(); // condition variable + int lk10; // lock variable + + int p11 = __VERIFIER_nondet_int(); // condition variable + int lk11; // lock variable + + int p12 = __VERIFIER_nondet_int(); // condition variable + int lk12; // lock variable + + int p13 = __VERIFIER_nondet_int(); // condition variable + int lk13; // lock variable + + int p14 = __VERIFIER_nondet_int(); // condition variable + int lk14; // lock variable + + + int cond; + + while(1) { + cond = __VERIFIER_nondet_int(); + if (cond == 0) { + goto out; + } else {} + lk1 = 0; // initially lock is open + + lk2 = 0; // initially lock is open + + lk3 = 0; // initially lock is open + + lk4 = 0; // initially lock is open + + lk5 = 0; // initially lock is open + + lk6 = 0; // initially lock is open + + lk7 = 0; // initially lock is open + + lk8 = 0; // initially lock is open + + lk9 = 0; // initially lock is open + + lk10 = 0; // initially lock is open + + lk11 = 0; // initially lock is open + + lk12 = 0; // initially lock is open + + lk13 = 0; // initially lock is open + + lk14 = 0; // initially lock is open + + + // lock phase + if (p1 != 0) { + lk1 = 1; // acquire lock + } else {} + + if (p2 != 0) { + lk2 = 1; // acquire lock + } else {} + + if (p3 != 0) { + lk3 = 1; // acquire lock + } else {} + + if (p4 != 0) { + lk4 = 1; // acquire lock + } else {} + + if (p5 != 0) { + lk5 = 1; // acquire lock + } else {} + + if (p6 != 0) { + lk6 = 1; // acquire lock + } else {} + + if (p7 != 0) { + lk7 = 1; // acquire lock + } else {} + + if (p8 != 0) { + lk8 = 1; // acquire lock + } else {} + + if (p9 != 0) { + lk9 = 1; // acquire lock + } else {} + + if (p10 != 0) { + lk10 = 1; // acquire lock + } else {} + + if (p11 != 0) { + lk11 = 1; // acquire lock + } else {} + + if (p12 != 0) { + lk12 = 1; // acquire lock + } else {} + + if (p13 != 0) { + lk13 = 1; // acquire lock + } else {} + + if (p14 != 0) { + lk14 = 1; // acquire lock + } else {} + + + // unlock phase + if (p1 != 0) { + if (lk1 != 1) goto ERROR; // assertion failure + lk1 = 0; + } else {} + + if (p2 != 0) { + if (lk2 != 1) goto ERROR; // assertion failure + lk2 = 0; + } else {goto ERROR;} + + if (p3 != 0) { + if (lk3 != 1) goto ERROR; // assertion failure + lk3 = 0; + } else {} + + if (p4 != 0) { + if (lk4 != 1) goto ERROR; // assertion failure + lk4 = 0; + } else {} + + if (p5 != 0) { + if (lk5 != 1) goto ERROR; // assertion failure + lk5 = 0; + } else {} + + if (p6 != 0) { + if (lk6 != 1) goto ERROR; // assertion failure + lk6 = 0; + } else {} + + if (p7 != 0) { + if (lk7 != 1) goto ERROR; // assertion failure + lk7 = 0; + } else {} + + if (p8 != 0) { + if (lk8 != 1) goto ERROR; // assertion failure + lk8 = 0; + } else {} + + if (p9 != 0) { + if (lk9 != 1) goto ERROR; // assertion failure + lk9 = 0; + } else {} + + if (p10 != 0) { + if (lk10 != 1) goto ERROR; // assertion failure + lk10 = 0; + } else {} + + if (p11 != 0) { + if (lk11 != 1) goto ERROR; // assertion failure + lk11 = 0; + } else {} + + if (p12 != 0) { + if (lk12 != 1) goto ERROR; // assertion failure + lk12 = 0; + } else {} + + if (p13 != 0) { + if (lk13 != 1) goto ERROR; // assertion failure + lk13 = 0; + } else {} + + if (p14 != 0) { + if (lk14 != 1) goto ERROR; // assertion failure + lk14 = 0; + } else {goto ERROR;} + + } + out: + return 0; + ERROR: {reach_error();abort();} + return 0; +} + + diff --git a/test/portfolio/test_locks_14-2_finish_all.c b/test/portfolio/test_locks_14-2_finish_all.c new file mode 100644 index 00000000..e179e50c --- /dev/null +++ b/test/portfolio/test_locks_14-2_finish_all.c @@ -0,0 +1,231 @@ +// RUN: %portfolio -c "%S"/SVComp_finish_all_configuration.yml -l minimal -t "%s" -o /tmp | FileCheck "%s" + +// CHECK: Result of bmc-inline: Verification FAILED. +// CHECK-NEXT: Result of bmc-inline-test-harness: Test harness SUCCESSFUL WITNESS +// CHECK: Result of theta-expl: Verification FAILED. +// CHECK-NEXT: Result of theta-expl-test-harness: Test harness SUCCESSFUL WITNESS +// CHECK: Result of theta-pred: Verification FAILED. +// CHECK-NEXT: Result of theta-pred-test-harness: Test harness SUCCESSFUL WITNESS +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); +void reach_error() { __assert_fail("0", "test_locks_14-2.c", 3, "reach_error"); } + +extern int __VERIFIER_nondet_int(); +int main() +{ + int p1 = __VERIFIER_nondet_int(); // condition variable + int lk1; // lock variable + + int p2 = __VERIFIER_nondet_int(); // condition variable + int lk2; // lock variable + + int p3 = __VERIFIER_nondet_int(); // condition variable + int lk3; // lock variable + + int p4 = __VERIFIER_nondet_int(); // condition variable + int lk4; // lock variable + + int p5 = __VERIFIER_nondet_int(); // condition variable + int lk5; // lock variable + + int p6 = __VERIFIER_nondet_int(); // condition variable + int lk6; // lock variable + + int p7 = __VERIFIER_nondet_int(); // condition variable + int lk7; // lock variable + + int p8 = __VERIFIER_nondet_int(); // condition variable + int lk8; // lock variable + + int p9 = __VERIFIER_nondet_int(); // condition variable + int lk9; // lock variable + + int p10 = __VERIFIER_nondet_int(); // condition variable + int lk10; // lock variable + + int p11 = __VERIFIER_nondet_int(); // condition variable + int lk11; // lock variable + + int p12 = __VERIFIER_nondet_int(); // condition variable + int lk12; // lock variable + + int p13 = __VERIFIER_nondet_int(); // condition variable + int lk13; // lock variable + + int p14 = __VERIFIER_nondet_int(); // condition variable + int lk14; // lock variable + + + int cond; + + while(1) { + cond = __VERIFIER_nondet_int(); + if (cond == 0) { + goto out; + } else {} + lk1 = 0; // initially lock is open + + lk2 = 0; // initially lock is open + + lk3 = 0; // initially lock is open + + lk4 = 0; // initially lock is open + + lk5 = 0; // initially lock is open + + lk6 = 0; // initially lock is open + + lk7 = 0; // initially lock is open + + lk8 = 0; // initially lock is open + + lk9 = 0; // initially lock is open + + lk10 = 0; // initially lock is open + + lk11 = 0; // initially lock is open + + lk12 = 0; // initially lock is open + + lk13 = 0; // initially lock is open + + lk14 = 0; // initially lock is open + + + // lock phase + if (p1 != 0) { + lk1 = 1; // acquire lock + } else {} + + if (p2 != 0) { + lk2 = 1; // acquire lock + } else {} + + if (p3 != 0) { + lk3 = 1; // acquire lock + } else {} + + if (p4 != 0) { + lk4 = 1; // acquire lock + } else {} + + if (p5 != 0) { + lk5 = 1; // acquire lock + } else {} + + if (p6 != 0) { + lk6 = 1; // acquire lock + } else {} + + if (p7 != 0) { + lk7 = 1; // acquire lock + } else {} + + if (p8 != 0) { + lk8 = 1; // acquire lock + } else {} + + if (p9 != 0) { + lk9 = 1; // acquire lock + } else {} + + if (p10 != 0) { + lk10 = 1; // acquire lock + } else {} + + if (p11 != 0) { + lk11 = 1; // acquire lock + } else {} + + if (p12 != 0) { + lk12 = 1; // acquire lock + } else {} + + if (p13 != 0) { + lk13 = 1; // acquire lock + } else {} + + if (p14 != 0) { + lk14 = 1; // acquire lock + } else {} + + + // unlock phase + if (p1 != 0) { + if (lk1 != 1) goto ERROR; // assertion failure + lk1 = 0; + } else {} + + if (p2 != 0) { + if (lk2 != 1) goto ERROR; // assertion failure + lk2 = 0; + } else {goto ERROR;} + + if (p3 != 0) { + if (lk3 != 1) goto ERROR; // assertion failure + lk3 = 0; + } else {} + + if (p4 != 0) { + if (lk4 != 1) goto ERROR; // assertion failure + lk4 = 0; + } else {} + + if (p5 != 0) { + if (lk5 != 1) goto ERROR; // assertion failure + lk5 = 0; + } else {} + + if (p6 != 0) { + if (lk6 != 1) goto ERROR; // assertion failure + lk6 = 0; + } else {} + + if (p7 != 0) { + if (lk7 != 1) goto ERROR; // assertion failure + lk7 = 0; + } else {} + + if (p8 != 0) { + if (lk8 != 1) goto ERROR; // assertion failure + lk8 = 0; + } else {} + + if (p9 != 0) { + if (lk9 != 1) goto ERROR; // assertion failure + lk9 = 0; + } else {} + + if (p10 != 0) { + if (lk10 != 1) goto ERROR; // assertion failure + lk10 = 0; + } else {} + + if (p11 != 0) { + if (lk11 != 1) goto ERROR; // assertion failure + lk11 = 0; + } else {} + + if (p12 != 0) { + if (lk12 != 1) goto ERROR; // assertion failure + lk12 = 0; + } else {} + + if (p13 != 0) { + if (lk13 != 1) goto ERROR; // assertion failure + lk13 = 0; + } else {} + + if (p14 != 0) { + if (lk14 != 1) goto ERROR; // assertion failure + lk14 = 0; + } else {goto ERROR;} + + } + out: + return 0; + ERROR: {reach_error();abort();} + return 0; +} + + diff --git a/test/portfolio/zerodiv_example.c b/test/portfolio/zerodiv_example.c new file mode 100644 index 00000000..1fa66bcb --- /dev/null +++ b/test/portfolio/zerodiv_example.c @@ -0,0 +1,24 @@ +// RUN: %portfolio -c "%S"/SVComp_configuration.yml -l minimal -t "%s" -o /tmp | FileCheck "%s" + +// CHECK: Result of bmc-inline: Verification FAILED. +// CHECK-NEXT: Result of bmc-inline-test-harness: Test harness SUCCESSFUL WITNESS +// CHECK: Final result of portfolio: Verification FAILED. +#include + +extern int ioread32(void); + +int main(void) { + int k = ioread32(); + int i = 0; + int j = k + 5; + while (i < 3) { + i = i + 1; + j = j + 3; + } + + k = k / (i - j); + + printf("%d\n", k); + + return 0; +} diff --git a/test/portfolio/zerodiv_example_finish_all.c b/test/portfolio/zerodiv_example_finish_all.c new file mode 100644 index 00000000..fdb0b43b --- /dev/null +++ b/test/portfolio/zerodiv_example_finish_all.c @@ -0,0 +1,27 @@ +// RUN: %portfolio -c "%S"/SVComp_finish_all_configuration.yml -l minimal -t "%s" -o /tmp | FileCheck "%s" + +// CHECK: Result of bmc-inline: Verification FAILED. +// CHECK-NEXT: Result of bmc-inline-test-harness: Test harness SUCCESSFUL WITNESS +// CHECK: Result of theta-expl: Verification FAILED. +// CHECK-NEXT: Result of theta-expl-test-harness: Test harness SUCCESSFUL WITNESS +// CHECK: Result of theta-pred: Verification FAILED. +// CHECK-NEXT: Result of theta-pred-test-harness: Test harness SUCCESSFUL WITNESS +#include + +extern int ioread32(void); + +int main(void) { + int k = ioread32(); + int i = 0; + int j = k + 5; + while (i < 3) { + i = i + 1; + j = j + 3; + } + + k = k / (i - j); + + printf("%d\n", k); + + return 0; +} From 4347b8c61f04edb77b8954c94fe3660c5f8dcc47 Mon Sep 17 00:00:00 2001 From: Akos Hajdu Date: Sun, 24 Jan 2021 10:32:10 +0100 Subject: [PATCH 2/3] Improve docs, bump version --- CMakeLists.txt | 4 +- doc/Portfolio.md | 122 +++++++++++++++++++++++++++++++---------------- 2 files changed, 82 insertions(+), 44 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 04eb2c03..4383d123 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -7,10 +7,10 @@ if(NOT DEFINED GAZER_VERSION_MAJOR) set(GAZER_VERSION_MAJOR 1) endif() if(NOT DEFINED GAZER_VERSION_MINOR) - set(GAZER_VERSION_MINOR 3) + set(GAZER_VERSION_MINOR 4) endif() if(NOT DEFINED GAZER_VERSION_PATCH) - set(GAZER_VERSION_PATCH 2) + set(GAZER_VERSION_PATCH 0) endif() if(NOT DEFINED GAZER_VERSION_SUFFIX) set(GAZER_VERSION_SUFFIX "") diff --git a/doc/Portfolio.md b/doc/Portfolio.md index 377e9488..69f16c7d 100644 --- a/doc/Portfolio.md +++ b/doc/Portfolio.md @@ -1,25 +1,76 @@ # Gazer-Theta Portfolio + ## What is the Portfolio script? -Gazer can be used as a command-line tool (gazer-cfa, gazer-bmc or gazer-theta) with lots of possible configurations. But in those cases Gazer simply executes that configuration on the given input program and returns the output of the verification process. The portfolio script adds another "level" to these command-line tools: it enables the sequential run of several configurations based on a YAML configuration file. This, on one hand, enables the user to easily compare configurations, as some may be better suited for a specific set of inputs than others. On the other hand it also enables of saving such successful configuration groups - portfolios - which then can be reused later. -## Usage of script +Gazer, and its backends can be used as a command-line tools (gazer-cfa, gazer-bmc or gazer-theta) with lots of possible configurations. +In those cases, Gazer simply executes the given configuration on the given input program and returns the result. +However, formal verification of software is a hard problem, so there is usually no single "best" configuration that is effective on all input programs. + +The portfolio script adds another layer to the command-line tools by enabling the sequential execution of different configurations, which can be described in a YAML configuration file. +This way, multiple configurations can be tried for the input program, which together have a higher chance of succeeding than a single configuration alone. +Furthermore, portfolios that seem to be efficient can be saved in files to be reused later. + +## Setting up the portfolio script + +The portfolio script requires Perl with the following packages: +- `YAML::Tiny` *(Parses YAML, not part of core packages)* +- `Getopt::Long` *(Handles flags, part of core packages)* +- `Digest::file` *(generates SHA256 hash for witnesses, part of core packages)* +- `Process::Killfam` *(Required for properly terminating tools after timeout, not a core package)* + +### Setting up via apt on Ubuntu + +- https://packages.ubuntu.com/bionic/perl +- https://packages.ubuntu.com/bionic/libyaml-tiny-perl +- https://packages.ubuntu.com/bionic/libproc-processtable-perl + +### Setting up through CPAN + +``` +perl -MCPAN -e shell +install +exit +``` + +## Using the portfolio script + +The entry point of the portfolio script is `scripts/portfolio/Portfolio.pl`. + ### Configuration file (YAML) -This file configures the portfolio and it is given to the Portfolio script as the argument of the flag *--configuration/-c* -#### Global options -##### generate-witness: Yes/No -Gazer - among other formats - can generate a counterexample in the format of SV-Comps violation witnesses. More about the witnesses [here](https://github.com/sosy-lab/sv-witnesses). -##### finish-all-configurations: Yes/No -If Yes, the script will run all the configurations in the order they were given in the configuration file. -If No, the script will stop, when a configuration (with test harness checked, if set so) gives back a result (failed or succesful) and will output that as the final result -##### check-harness -If defined, then Gazer will generate a test harness in the appropriate cases and the script will compile, execute and check this test harness, with which it can filter out false positive results execute-harness-timeout and compile-harness-timeout need to be given in this case as well (in seconds), for example: + +The configurations can be described using a YAML configuration file, which has to be passed to the portfolio script as `--configuration config.yml` or `-c config.yml`, where `config.yml` is an example YAML file. +The YAML configuration file has two main parts: the **global options** and the **description of the configurations**. + +**Global options** + +`generate-witness`: `Yes`/`No` + +Gazer - among other formats - can generate a counterexample in the [format of SV-COMP's violation witnesses](https://github.com/sosy-lab/sv-witnesses). + +`finish-all-configurations`: `Yes`/`No` + +If `No`, the script stops as soon as the first configuration gives a conclusive (safe/unsafe) result, and returns this result. +If `Yes`, the script will run all the configurations in the order they were given in the configuration file. + +`check-harness` + +When defined Gazer generates an executable test harness if the result is unsafe. +The script compiles, executes and checks this test harness. +If the test harness does not trigger a property violation, the unsafe result is treated as unknown/inconclusive instead. +This can filter out false positives. +This option has two parameters: `compile-harness-timeout` and `execute-harness-timeout` describe the time limit for compiling and executing the harness (in seconds). +For example: ``` check-harness: execute-harness-timeout: 100 - check-harness-timeout: 150 + compile-harness-timeout: 150 ``` -#### Configuration of the portfolio itself -An array of the configurations, something like this: + +**Description of the configurations** + +Configurations can be given as a list, where each item in the list corresponds to a particular configuration. +Their order in the list also defines their execution order. +For example: ``` configurations: - name: config1 @@ -30,39 +81,26 @@ configurations: tool: gazer-theta flags: --inline all --domain EXPL ``` -- The **name** and **tool** attributes are required, **timeout** and **flags** are optional. -- The **name** can be any arbitrary name, it mostly serves readability purposes. -- The possible values of **tool** are *gazer-bmc* or *gazer-theta*. -- Giving a **timeout** is optional, but not doing so can possibly result in an endless run, if Gazer or Theta gets stuck. -- Documentation of the available **flags**: [for Gazer](https://github.com/ftsrg/gazer/blob/master/README.md), [for Theta](https://github.com/ftsrg/theta/blob/master/doc/CEGAR-algorithms.md) +- The `name` and `tool` attributes are required, while `timeout` and `flags` are optional. +- The `name` can be an arbitrary identifier, which just makes the output easier to interpret. +- The possible values of `tool` are currently `gazer-bmc` or `gazer-theta`. +- Giving a `timeout` is optional, however it is recommended to avoid configurations getting stuck (e.g., an infinite loop in the verifier backend). +- The `flags` describe the additional flags given to the particular backend. See the documentation of [Gazer](https://github.com/ftsrg/gazer/blob/master/README.md) and [Theta](https://github.com/ftsrg/theta/blob/master/doc/CEGAR-algorithms.md) for the available options. -For more detailed examples, see the *test-configs* directory under *scripts/portfolio/* +For more detailed examples, see `scripts/portfolio/test-configs`. ### Flags -**--version/-v** - outputs the Gazer and Theta versions *(and does nothing else)* -**--configuration/-c "filename"** - YAML portfolio configuration file -**--task/-t "filename"** - C program to be verified (.c, .i, .ll) -**--log-level/-l** - minimal or verbose (verbose outputs the output of Gazer as well) -**--output-directory/-o** - output path, where a portfolio-output directory will be created and used by the script (default: working directory) -**--debug/-d**** - if given, the logs are extended with more information about the script for debugging purposes (directories used, configuration list, etc.) - -### Example -./Portfolio.pl -c test-files/config-file-example.yml -t test-files/test_locks_14-2.c -l minimal -o test_output/ -## Required Perl packages -YAML::Tiny *(Parses YAML, not part of core packages)* -Getopt::Long *(Handles flags, part of core packages)* -Digest::file *(generates SHA256 hash for witnesses, part of core packages)* -Process::Killfam *(Required for properly terminating tools after timeout, not a core package)* +The portfolio script has the following flags. -### from apt on Ubuntu: -https://packages.ubuntu.com/bionic/perl -https://packages.ubuntu.com/bionic/libyaml-tiny-perl -https://packages.ubuntu.com/bionic/libproc-processtable-perl +- `--version`/`-v`: outputs the Gazer and Theta versions *(and does nothing else)*. +- `--configuration`/`-c` ``: configuration file in YAML format. +- `--task`/`-t` ``: The input C program to be verified (`*.c`, `*.i`, `*.ll`). +- `--log-level`/`-l`: Level of logging, possible values are `minimal` or `verbose` (`verbose` outputs the output of Gazer as well). +- `--output-directory`/`-o` ``: Output path, where a portfolio-output directory will be created and used by the script (default: working directory). +- `--debug`/`-d`: If given, the logs are extended with more information about the script for debugging purposes (directories used, configuration list, etc.). -### through CPAN: +### Example ``` -perl -MCPAN -e shell -install -exit +./Portfolio.pl -c test-files/config-file-example.yml -t test-files/test_locks_14-2.c -l minimal -o test_output/ ``` From a156a4eeb1c90f584f62c76f1233ea5694224751 Mon Sep 17 00:00:00 2001 From: Akos Hajdu Date: Sun, 24 Jan 2021 10:34:06 +0100 Subject: [PATCH 3/3] Add info on portfolio in main readme --- README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/README.md b/README.md index 047ea0a0..f89be26e 100644 --- a/README.md +++ b/README.md @@ -8,6 +8,9 @@ Currently we support two verification backends: * Currently, [v2.8.0](https://github.com/ftsrg/theta/releases/tag/v2.8.0) is tested, but newer releases might also work. * `gazer-bmc` is gazer's built-in bounded model checking engine. +Furthermore, it is also possible to run multiple backends with different options as a portfolio. +See [doc/Portfolio.md](doc/Portfolio.md) for more information. + # Usage Consider the following C program (`example.c`):