<jupyter_start><jupyter_text>License---This file is part of CPAchecker, a tool for configurable software verification:  https://cpachecker.sosy-lab.orgSPDX-FileCopyrightText: 2020 <NAME> (https://www.sosy-lab.org)SPDX-License-Identifier: Apache-2.0Instructions---*description*You can set a threshold to substract the start-up time of CPAchecker.<jupyter_code># threshold in seconds. 
# Increase the time limit by <threshold> seconds to substract the time CPAchecker needs to start. Only applied on sequential analysis.
threshold = 5
# necessary to get tablegenerator versions >= 3.8 to work
import decimal
decimal.DefaultContext.rounding = decimal.ROUND_HALF_UP<jupyter_output><empty_output><jupyter_text>This cell provides the util methods to convert the result sets to pandas dataframe format.<jupyter_code>from benchexec import tablegenerator
import benchexec.result
import pandas as pd
import numpy as np
from typing import Optional, List, Union, Tuple
from dataclasses import dataclass
import os

UNK = "ERR/UNKNOWN/TIMEOUT"

def get_data(data_files: Union[List[str], str], table_definition=None) -> List[pd.DataFrame]:
    if not isinstance(data_files, str):
        return [d for f in data_files for d in get_data(f, table_definition)]
    raw_data = _load_data(data_files, table_definition)
    return [pd.DataFrame(data=_get_values(raw_data), columns=_get_column_titles(raw_data))]


def _load_data(data_file: str, table_definition: Optional[str]=None) -> tablegenerator.RunSetResult:
    parser = tablegenerator.create_argument_parser()
    args = [data_file]
    if table_definition:
        args += ['-x', table_definition]
    options = parser.parse_args(args)
    if table_definition:
        parsed_tabledef = tablegenerator.parse_table_definition_file(table_definition)
        return list(tablegenerator.load_results_with_table_definition([data_file], parsed_tabledef, table_definition, options))[0]
    else:
        return tablegenerator.load_result(data_file, options)

    
def _get_column_titles(result_set: tablegenerator.RunSetResult):
    return ['task_id', 'category'] + [col.title for col in result_set.columns]


def _get_values(result_set):
    return [[r.task_id[0], r.category] + cast_values(r) for r in result_set.results]


def cast_values(r: tablegenerator.RunResult):
    return [to_value(value, column) for value, column in zip(r.values, r.columns)]


def to_value(value, column):
    if not column.is_numeric() or value is None:
        return value
    if column.unit is None:
        return value
    return float(value[:-len(column.unit)])


def merge_columns(category, status):
    merge_dict = {
        ("correct", "false(unreach-call)"): "TP",
        ("wrong", "false(unreach-call)"): "FP",
        ("correct", "true"): "TN",
        ("wrong", "true"): "FN"
    }
    if (category, status) in merge_dict:
        return merge_dict[(category, status)]
    return UNK


def read_benchmarks(*data_files):
    frames = []
    for df in get_data(data_files):
        # skip tables with missing columns (e.g. analysis was aborted)
        if not {'cputime', 'status', 'category'}.issubset(df.columns):
            print("Skipped table because it is missing columns. The first 5 rows: ")
            print(df.head(5))
            frames.append(pd.DataFrame(columns=['task_id', 'result', 'cputime']))
            continue
        # skip aborted tasks
        df = df[df['category'] != "aborted"]
        df = df.drop(columns=['host'], errors='ignore')
        df['result'] = df.apply(lambda row: merge_columns(row['category'], row['status']), axis=1)
        frames.append(df[COLUMNS_USED])
    return frames<jupyter_output><empty_output><jupyter_text>The following methods are used to work with feature vectors.<jupyter_code>from typing import NamedTuple
class FeatureVector(NamedTuple):
    has_floats: int = -1
    has_array: int = -1
    has_recursion: int = -1
    has_composite_handling: int = -1
    has_loop: int = -1
    has_alias_handling: int = -1

    def matches(self, fv):
        for elem in zip(self,fv):
            if elem[0] == -1 or elem[1] == -1:
                continue
            if (elem[0] != elem[1]):
                return False
        return True
    
    def find_match(self, lookup: list):
        for key in lookup:
            if not isinstance(key, FeatureVector):
                raise ValueError(f"Key in given sequence not of type 'FeatureVector': {key}")
            if key.matches(self):
                return key
        raise ValueError(f"Given sequence did contain no matching key. Did you forget the default case? Sequence: {lookup}")
    
    @staticmethod
    def from_dataframe_row(row):
        return FeatureVector(row['has_floats'],
                             row['has_arrays'],
                             row['has_recursion'],
                             row['has_composite_handling'],
                             row['has_loop'],
                             row['has_alias_handling'])

    
FeatureVector.default = FeatureVector()<jupyter_output><empty_output><jupyter_text>The following methods are used to calculate the final score.<jupyter_code>def prepare_frames(input_sets, sequential=False):
    frames = []
    for (df, timelimit) in input_sets:
        if not timelimit:
            frames.append(df)
            continue
        if sequential and threshold and frames:
            df.cputime = df.cputime - threshold
        condition = df.cputime > timelimit
        df.loc[condition, 'result'] = UNK
        df.loc[condition, 'cputime'] = timelimit
        frames.append(df)
    return frames


def _join(frames):
    join = sequence[0]
    for idx, candidate in enumerate(sequence[1:], start=1):
        join = pd.merge(join.copy(), candidate.copy(), left_on="task_id", right_on="task_id", suffixes=('', f'_{idx}'), how="outer")
    return join


def sequential(*input_sets):
    sequence = prepare_frames(input_sets, sequential=True)
    join = _join(sequence)
    results = join[COLUMNS_USED]
    for idx, _ in enumerate(sequence[1:], start=1):
        mask = (results.result == UNK)
        if not results[mask].empty:
            results.loc[mask,'result'] = join.loc[mask, f'result_{idx}']
            results.loc[mask,'cputime'] = results.loc[mask,'cputime'] + join.loc[mask, f'cputime_{idx}']
    return results


def parallel(*input_sets):
    prepared = prepare_frames([(df, None) for df in input_sets])
    prepared = prepared[COLUMNS_USED]
    distinct_ids = prepared.task_id.unique()
    results = pd.DataFrame(columns = prepared.columns)
    # loop through every distinct key
    for key in distinct_ids:
        selection = prepared[prepared['task_id'] == key]
        col_result_distinct = selection.result.unique()
        # if all results are unknown the tasks takes max(cputime)
        if len(col_result_distinct) == 1:
            if col_result_distinct[0] == UNK:
                max_time = selection['cputime'].max()
                new_row = pd.DataFrame([[key, UNK, max_time]], columns=prepared.columns)
                results = results.append(new_row)
                continue
        # otherwise return result of first analysis that finishes min(cputime | result != "UNKNOWN")
        selection = selection[selection['result'] != UNK]
        selection = selection[selection['cputime'] == selection['cputime'].min()].head(1)
        results = results.append(selection)
    return results


def select(fv_table, config):
    df = pd.DataFrame(columns=fv_table.columns)
    for index, row in fv_table.iterrows():
        fv = FeatureVector.from_dataframe_row(row)
        selected = config[fv.find_match(config.keys())]
        selected_row = selected[selected["task_id"] == row["task_id"]]
        df = pd.concat([df,selected_row])
    return df
        

def evaluate(df):
    counts = df.result.value_counts()
    average_time = int(df.cputime.mean())
    time = pd.Series([average_time], index=['Average time'])
    return counts.append(time)<jupyter_output><empty_output><jupyter_text>There are 2 strategies available:- sequential:```simulates the sequential execution of all given analyses| analysis 0 | analysis 1 | ... | analysis n |```- parallel:```file2simulates the parallel execution of all given analyses|      analysis 0     ||      analysis 1     ||      analysis 2     |```All analyses simulate an execution where the calculation terminates as soon as a result different from "UNKNOWN", "ERROR" or "TIMEOUT" occurs (if possible).<jupyter_code>COLUMNS_USED = ['task_id', 'result', 'cputime']

# define your tasks here
result_files = {
    'valueAnalysis': 'results/svcomp21--bare--configs.2020-11-12_15-42-21.results.valueAnalysis.xml.bz2',
    'valueAnalysis-itp': 'results/svcomp21--bare--configs.2020-11-12_15-42-21.results.valueAnalysis-itp.xml.bz2',
    'predicateAnalysis': 'results/svcomp21--bare--configs.2020-11-12_15-42-21.results.predicateAnalysis.xml.bz2',
    'bmc': 'results/svcomp21--bare--configs.2020-11-12_15-42-21.results.bmc.xml.bz2',
}

results = {
    key: read_benchmarks(results_file)[0]
    for key, results_file in result_files.items()
}
featureExtraction = get_data('results/featureExtraction.2020-11-13_14-08-04.results.SV-COMP21_unreach-call.ReachSafety-ECA.xml.bz2',
                            table_definition='table-featureVectors.xml')[0]<jupyter_output><empty_output><jupyter_text>Create a configuration for feature vectors. A vector has 6 attributes with values `1, 0, -1`. Value `1` translates to `True`, `0` to `False` and `-1` to 'irrelevant'.Here you can see an example for a configuration:<jupyter_code># define your configuration here. Paths must be specified relative to the directory of this notebook.

bmc = results['bmc']
value_predicate_bmc = sequential((results['valueAnalysis'], 90),
                         (results['valueAnalysis-itp'], 60),
                         (results['predicateAnalysis'], 200),
                         (bmc, None))

value_bmc = sequential((results['valueAnalysis'], 90),
                     (results['valueAnalysis-itp'], None),
                     (bmc, None))

configuration = {
    FeatureVector(has_loop=0): bmc,
    FeatureVector(has_loop=1, has_composite_handling=0): value_predicate_bmc,
    FeatureVector.default: value_bmc,
}

strategy_selection = select(featureExtraction, configuration)<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.11719277922579399, 'fraction_numerical': 0.014190558934260064, 'mean_word_length': 3.3202668890742286, 'pattern_counts': {'":': 0, '<': 27, '<?xml version=': 0, '>': 31, 'https://': 2, 'lorem ipsum': 0, 'www.': 1, 'xml': 6}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '6', 'dir': 'jupyter-structured-clean-dedup', 'id': '334858', 'license': 'Apache-2.0', 'n_tokens_mistral': 3244, 'n_tokens_neox': 3096, 'n_words': 767, 'path': 'contrib/composition-simulation/CompositionSimulation.ipynb', 'repo_name': 'Po-Chun-Chien/cpachecker', 'size': '10363'}