diff --git a/theses/README.md b/theses/README.md index ba9dbe94..33ea9019 100644 --- a/theses/README.md +++ b/theses/README.md @@ -1,5 +1,43 @@ # Bachelor Theses on Selfie +## Exploring Reasoning Performance of RISC-V Software Models in BTOR2 by Nadir Fejzić, University of Salzburg, Austria, 2024 ([PDF](https://github.com/cksystemsteaching/selfie/blob/main/theses/bachelor_thesis_fejzic.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_fejzic)) + +When working with software programs, we want to ensure that they do not +reach certain unsafe states. Various techniques exist for this purpose, +such as testing. However, testing requires running the program with every +possible input, which is often not practical because of the large input +space. Most often we want to check whether an input exists such that our +program reaches a specific state. This is known as the state reachability +problem, which can be reduced to the boolean satisfiability problem and +solved by SAT-solvers. + +The reduction can be done by encoding the sequence of machine instructions +in the program as a satisfiability formula in the theory of bit-vectors, +known as a Satisfiability Modulo Theory (SMT) formula. The resulting +formula is the model of our program. SMT-formulae are then further reduced +to boolean logic formulae by technique called bit-blasting. We can then run +a SAT-solver on resulting boolean formulae, which will tell us whether the +program satisfies the given constraints. Effectively, we reduced the +problem of program correctness to the satisfiability problem. Important to +notice is that only a finite number of instructions can be transformed this +way, which makes the model checking bounded in number of executed +instructions. + +As we reduced the program correctness problem to satisfiability problem, +solving it is NP-Complete and computationally expensive. However, model +generation is linear in the size of the input program. We took advantage of +this property and generated many equivalent models to analyze impact of +different configurations on solving performance of \texttt{btormc} model +checker. + +In this thesis, we present a toolbox \texttt{peRISCope} for easy +benchmarking of different model configurations. We also present and analyze +results from benchmarking of solving time for models with different code +and non-code memory granularity configurations. We found that models with +smaller memory granularity were solved faster in models generated from +binaries compiled with \texttt{starc} compiler. On models generated from +binaries compiled with \texttt{gcc} compiler, models with larger memory +granularity were solved faster. ## Automated Testing of Atomic Instructions (`LR`/`SC`) Implementations in Selfie by Luis Thiele, University of Salzburg, Austria, 2022 ([PDF](https://github.com/cksystemsteaching/selfie/blob/main/theses/bachelor_thesis_thiele.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_thiele)) @@ -9,16 +47,13 @@ This thesis is about extending the autograder to grade an assignment called `tre Additionally, this thesis also describes the correct implementations of the `LR` and `SC` instructions in the emulator and a correct implementation of the Treiber stack in order to pass the entirety of the autograded `treiber-stack` assignment. All prerequesite requirements are also explained, namely a correct implementation of support for threads (`threads` assignment), as well as any concepts and details about the emulator one must understand such as paging or system calls. - ## Visualizing BTOR2 Models by Markus Diller, University of Salzburg, Austria, 2022 ([PDF](https://github.com/cksystemsteaching/selfie/blob/main/theses/bachelor_thesis_diller.pdf), [Repository](https://github.com/cksystemsgroup/beator-visualizer)) The process of bounded model checking is very helpful in finding edge cases for invalid program inputs. To be able to do this, a format representing the model is necessary. Unfortunately, the model file itself does not provide any information about metrics or quality of a model. Its only purpose is to serve as an input to a model checker. In this thesis a tool called `beatle` for a subset of the BTOR2 modeling language is described. It helps to alleviate the aforementioned limitations of a standalone model file by visually displaying relevant information in the browser. - ## RISC-U Binary Optimization for Selfie by David Pape, University of Salzburg, Austria, 2021 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_pape/bachelor_thesis_pape.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_pape)) - -Optimizers are part of any modern compiler, and their practical importance in writing performant code cannot be understated. Still, they introduce major complexity, and its complement: bugs. In this work, we present a binary optimizer for RISC-U, a small subset of RISC-V and the target architecture of selfies[@selfie] educational compiler. To address the complexity issue, our optimizer is structured as a standalone binary, keeping the compiler simple. Since this comes at the cost of compile-time information, a binary analyzer is a prerequisite. With it, our optimizer is able to remove redundant instructions and apply several peephole optimizations, leading to a roughly five percent speedup. +Optimizers are part of any modern compiler, and their practical importance in writing performant code cannot be understated. Still, they introduce major complexity, and its complement: bugs. In this work, we present a binary optimizer for RISC-U, a small subset of RISC-V and the target architecture of selfies[@selfie] educational compiler. To address the complexity issue, our optimizer is structured as a standalone binary, keeping the compiler simple. Since this comes at the cost of compile-time information, a binary analyzer is a prerequisite. With it, our optimizer is able to remove redundant instructions and apply several peephole optimizations, leading to a roughly five percent speedup. ## Linear-Time Static Analysis of RISC-V Binary Code by Thomas Wulz, University of Salzburg, Austria, 2021 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_wulz/bachelor_thesis_wulz.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_wulz)) @@ -27,7 +62,7 @@ We present algorithms for static analysis of such RISC-V binaries along with a C ## RISC-V Bare-Metal Library Operating System for Selfie by Marcell Haritopoulos, University of Salzburg, Austria, 2021 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_haritopoulos/bachelor_thesis_haritopoulos.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_haritopoulos)) -Despite its young age, the field of Computer Science is multifaceted and complex, at the expense of the entry barrier. Selfie, an educational project, aims to close the gap on the fundamentals. It runs on a hosted environment, but was not able to run on bare metal RISC-V hardware. We introduce a simple library operating system for RISC-V that implements the system call interface of Selfie and supports (nearly) all applications, that are written in Selfie's tiny C subset C* and are using its syscall interface, without any modifications, including Selfie itself. The OS is linked to the application as a static library and is responsible for maintaining a C environment. System calls are performed as mere function invocations instead of raising an exception using ecall. Files are stored in a static read-only file system. I/O system calls are implemented in a general way so that related projects may share the same semantics. +Despite its young age, the field of Computer Science is multifaceted and complex, at the expense of the entry barrier. Selfie, an educational project, aims to close the gap on the fundamentals. It runs on a hosted environment, but was not able to run on bare metal RISC-V hardware. We introduce a simple library operating system for RISC-V that implements the system call interface of Selfie and supports (nearly) all applications, that are written in Selfie's tiny C subset C\* and are using its syscall interface, without any modifications, including Selfie itself. The OS is linked to the application as a static library and is responsible for maintaining a C environment. System calls are performed as mere function invocations instead of raising an exception using ecall. Files are stored in a static read-only file system. I/O system calls are implemented in a general way so that related projects may share the same semantics. ## RISC-V S-Mode-Hosted Bare-Metal Selfie by Martin Fischer, University of Salzburg, Austria, 2020 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_fischer/bachelor_thesis_fischer.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_fischer)) @@ -43,7 +78,7 @@ Given a 64-bit RISC-V binary we compute a single logical formula that is satisfi ## Implementation and Application of a Parser for Boolector's Witness Format by Christoph Siller, University of Salzburg, Austria, 2020 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_siller/bachelor_thesis_siller.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_siller)) -In this bachelor thesis, a parser for Boolector’s witness format is introduced, which enables automated input validation. The toolchain takes a C* file containing read calls as input and generates a Btor2 model of it, using Selfie’s model generator. The resulting model is then fed to the Boolector-based bounded model checker BtorMC. By using SMT-solving, BtorMC is able to find error states in the model within a maximum number of executed instructions. In case an error state is found, BtorMC generates a witness. This witness is parsed in order to extract the input string that causes the C* program to run into the error. To validate that the extracted string indeed triggers an error, it is fed to the C* program while running it on Mipster. If the input string was generated correctly, Mipster runs into the predicted error. In addition to the parser, this thesis provides background information on all technologies used and the concepts they are based on. +In this bachelor thesis, a parser for Boolector’s witness format is introduced, which enables automated input validation. The toolchain takes a C* file containing read calls as input and generates a Btor2 model of it, using Selfie’s model generator. The resulting model is then fed to the Boolector-based bounded model checker BtorMC. By using SMT-solving, BtorMC is able to find error states in the model within a maximum number of executed instructions. In case an error state is found, BtorMC generates a witness. This witness is parsed in order to extract the input string that causes the C* program to run into the error. To validate that the extracted string indeed triggers an error, it is fed to the C\* program while running it on Mipster. If the input string was generated correctly, Mipster runs into the predicted error. In addition to the parser, this thesis provides background information on all technologies used and the concepts they are based on. ## Selfie - RISC-V to x86-64 Binary Translation by Alexander Kollert, University of Salzburg, Austria, 2020 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_kollert/bachelor_thesis_kollert.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_kollert)) diff --git a/theses/bachelor_thesis_fejzic.pdf b/theses/bachelor_thesis_fejzic.pdf new file mode 100644 index 00000000..b4ef15c9 Binary files /dev/null and b/theses/bachelor_thesis_fejzic.pdf differ diff --git a/tools/periscope/README.md b/tools/periscope/README.md new file mode 100644 index 00000000..a0dd025d --- /dev/null +++ b/tools/periscope/README.md @@ -0,0 +1,17 @@ +# peRISCope + +This is a project for exploring the reasoning performance of RISC-V software +models in BTOR2. The name `periscope` is derived from the idea of exploring +PErformance of RISC models, and the idea of a periscope that can be used to +explore the unknown surroundings. + +## Structure + +The project consists of two sub-projects: + +- [`periscope-rs`](./periscope-rs) - A binary written in Rust that can be used + to parse witness format producec by `btormc`, and for benchmarking of model + checking. Check the [README](./periscope-rs/README.md) for more information. +- [`periscope-py`](./periscope-py) - A Python package that can be used to read + output of `periscope-rs` and produce plots. Check the + [README](./periscope-py/README.md) for more information. diff --git a/tools/periscope/periscope-py/.gitignore b/tools/periscope/periscope-py/.gitignore new file mode 100644 index 00000000..4dd37aff --- /dev/null +++ b/tools/periscope/periscope-py/.gitignore @@ -0,0 +1,3 @@ +.venv/ + +src/__pycache__/ diff --git a/tools/periscope/periscope-py/README.md b/tools/periscope/periscope-py/README.md new file mode 100644 index 00000000..18b093bc --- /dev/null +++ b/tools/periscope/periscope-py/README.md @@ -0,0 +1,27 @@ +# PeRISCope - Python script for results visualisation + +This is a simple Python script for generating plots of benchmarking results +produced by [`periscope-rs`](../periscope-rs). + +## Usage + +Make sure you installed all required dependencies: + +```sh +pip install -r requirements.txt +``` + +After that, run the main script file with `--help` flag to get more information: + +```sh +python src/periscope.py --help +``` + +## Example usage: + +```sh +# Generate a plot with bars for each configuration, overall sort-by median time, +# and scale the y-axis logarithmically. Plot results contained in `results_dir` +# and save the plot to test.png file. +python src/periscope.py --sort-by median --scale log --type cmp-bars -o test.png results_dir +``` diff --git a/tools/periscope/periscope-py/pyrightconfig.json b/tools/periscope/periscope-py/pyrightconfig.json new file mode 100644 index 00000000..c36f4017 --- /dev/null +++ b/tools/periscope/periscope-py/pyrightconfig.json @@ -0,0 +1,27 @@ +{ + "include": [ + "src", + ], + + "exclude": [ + "**/node_modules", + "**/__pycache__", + ".venv", + ], + + "venvPath": ".", + "venv": ".venv", + + "ignore": [ + "src/oldstuff" + ], + + "reportMissingImports": true, + "reportMissingTypeStubs": false, + + "executionEnvironments": [ + { + "root": "src" + } + ] +} diff --git a/tools/periscope/periscope-py/requirements.txt b/tools/periscope/periscope-py/requirements.txt new file mode 100644 index 00000000..c68e3544 --- /dev/null +++ b/tools/periscope/periscope-py/requirements.txt @@ -0,0 +1,2 @@ +jsonpickle==3.0.4 +matplotlib==3.8.4 diff --git a/tools/periscope/periscope-py/src/cmp_bars.py b/tools/periscope/periscope-py/src/cmp_bars.py new file mode 100644 index 00000000..56fdbd98 --- /dev/null +++ b/tools/periscope/periscope-py/src/cmp_bars.py @@ -0,0 +1,134 @@ +import argparse +import functools + +from matplotlib import figure +import matplotlib.pyplot as plt +import numpy as np + +from periscope_result import BenchResult + + +def cmp_median(medians: list[float], labels: list[str]): + def compare(i, j): + med_cmp = medians[i] - medians[j] + if med_cmp == 0: + return labels[i] < labels[j] + else: + return med_cmp + + return compare + + +def cmp_median_multi(): + def compare( + i: tuple[str, dict[str, BenchResult]], j: tuple[str, dict[str, BenchResult]] + ): + med_i_avg = sum([b.hyperfine_results()[0].median for b in i[1].values()]) / len( + i + ) + med_j_avg = sum([b.hyperfine_results()[0].median for b in j[1].values()]) / len( + i + ) + + med_cmp = med_i_avg - med_j_avg + return int(med_cmp) + + return compare + + +def cmp_legend(): + def compare(a: str, b: str): + all_numbers_a = list( + filter(lambda x: len(x) > 0 and x[0].isdigit(), a.split("-")) + ) + all_numbers_b = list( + filter(lambda x: len(x) > 0 and x[0].isdigit(), b.split("-")) + ) + + for num_a, num_b in zip(all_numbers_a, all_numbers_b): + num_a = int(num_a.removesuffix("b")) + num_b = int(num_b.removesuffix("b")) + + if num_a != num_b: + return num_a - num_b + + return 0 + + return compare + + +def plot_cmp_bars( + args: argparse.Namespace, + periscope_results: dict[str, list[BenchResult]], + figure: figure.Figure, +): + legend = sorted( + list(periscope_results.keys()), + key=functools.cmp_to_key(cmp_legend()), + # key=lambda x: int(x.split("-")[0].removesuffix("b")), + ) + + bar_w = (1 - 0.4) / len(legend) + group_w = bar_w * len(legend) + offsets = np.arange(start=-(group_w / 2), stop=group_w / 2, step=bar_w) + cmap = plt.get_cmap("rainbow") + colors = [cmap(val / len(legend)) for val in range(len(legend))] + + ax = figure.subplots(1, 1) + _, ax2 = plt.subplots(figsize=(20, 10), constrained_layout=True) + + handles = [] + + per_file: dict[str, dict[str, BenchResult]] = {} + + for bench_config in legend: + for bench_name in periscope_results[bench_config]: + b_name = ( + bench_name.name.removesuffix("-rotorized.btor2") + .removesuffix("-35") + .removesuffix("-10") + .removesuffix("-1") + .removesuffix("-2") + .removesuffix("-3") + ) + if b_name not in per_file: + per_file[b_name] = {} + + per_file[b_name][bench_config] = bench_name + + plt.title("Comparison of median times with different model configurations") + + if args.sort_by == "median": + per_file = dict( + sorted(per_file.items(), key=functools.cmp_to_key(cmp_median_multi())) + ) + + if args.scale == "log": + ax2.set_yscale("log") + plt.title( + "Comparison of median times with different model configurations (Log scale)", + ) + + plt.ylabel("Time [s]") + + labels = list(per_file.keys()) + label_positions = np.arange(len(labels)) - 0.1 + plt.tick_params(axis="x", length=20) + plt.xticks(list(label_positions), labels, rotation=55, ha="right") + + # label_positions = list() + + for idx, file in enumerate(per_file.values()): + for bench_idx, bench_name in enumerate(file.values()): + offs = offsets[bench_idx] + time = bench_name.hyperfine_results()[0].median + color = colors[bench_idx] + ax = plt.bar(x=idx + offs, height=time, width=bar_w, color=color) + handles.append(ax) + # label_positions.append(idx + offs) + + # plt.xticks(label_positions, labels, rotation=0) + + plt.ylim(0.1, 300) + legend = list(map(lambda x: x.removesuffix(".json").replace("-", " "), legend)) + plt.legend(handles=handles, labels=legend) diff --git a/tools/periscope/periscope-py/src/histogram.py b/tools/periscope/periscope-py/src/histogram.py new file mode 100644 index 00000000..074d0fbe --- /dev/null +++ b/tools/periscope/periscope-py/src/histogram.py @@ -0,0 +1,62 @@ +import argparse + +from matplotlib import figure, pyplot as plt +import numpy as np + +from periscope_result import BenchResult + + +def cmp_wc(labels: list[str], periscope_results: list[BenchResult]): + def compare(i, j): + wc_i = periscope_results[i].wc + wc_j = periscope_results[j].wc + if wc_i == wc_j: + return labels[i] < labels[j] + else: + return wc_i - wc_j + + return compare + + +def plot_histogram( + args: argparse.Namespace, + periscope_results: list[BenchResult], + figure: figure.Figure, + of_dump: bool, +): + labels = [b.name for b in periscope_results] + all_times = [b.times for pr in periscope_results for b in pr.hyperfine_results()] + + t_min = np.min(list(map(np.min, all_times))) + t_max = np.max(list(map(np.max, all_times))) + + if of_dump: + wcs = [pr.results.wc_btormc_dump for pr in periscope_results] + else: + wcs = [pr.results.wc_raw for pr in periscope_results] + + times = list(map(np.min, all_times)) + + _ = figure.subplots(1, 1) + cmap = plt.get_cmap("rainbow") + colors = [cmap(val / len(times)) for val in range(len(times))] + plt.bar(x=times, height=wcs, label=labels, color=colors, width=5) + + plt.title("Solving time and model size") + plt.xlabel("Time [s]") + + if of_dump: + plt.ylabel("Model Size after btormc dump [#chars]") + else: + plt.ylabel("Model Size [#chars]") + + plt.xticks(np.arange(np.floor(t_min), np.floor(t_max), step=10)) + plt.xticks( + list(map(np.min, all_times)), + labels, + rotation=65, + minor=True, + ) + + for xtick, color in zip(plt.gca().get_xticklabels(which="minor"), colors): + xtick.set_color(color) diff --git a/tools/periscope/periscope-py/src/periscope.py b/tools/periscope/periscope-py/src/periscope.py new file mode 100755 index 00000000..80622cda --- /dev/null +++ b/tools/periscope/periscope-py/src/periscope.py @@ -0,0 +1,90 @@ +#!/usr/bin/env python + +"""This program shows `hyperfine` benchmark results as a box and whisker plot. + +Quoting from the matplotlib documentation: + The box extends from the lower to upper quartile values of the data, with + a line at the median. The whiskers extend from the box to show the range + of the data. Flier points are those past the end of the whiskers. +""" + +import argparse +from logging import error + +from os import listdir +from os.path import isfile, join + +import matplotlib +import matplotlib.pyplot as plt + +import whiskers +import cmp_bars +import histogram +import periscope_result + + +def main(args: argparse.Namespace): + figure = plt.figure(figsize=(20, 15), constrained_layout=True) + + matplotlib.rcParams.update({"font.size": 16}) + + match args.type: + case "whisker": + periscope_results = periscope_result.results_from_file(args.path) + whiskers.plot_whiskers(args, periscope_results, figure) + case "cmp-bars": + figure = plt.figure(figsize=(20, 15), constrained_layout=True) + + if isfile(args.path): + error(f"'{args.path}' is not a directory.") + + files_with_results = {} + for file in listdir(args.path): + periscope_file = periscope_result.results_from_file( + join(args.path, file) + ) + files_with_results[file] = periscope_file + + cmp_bars.plot_cmp_bars(args, files_with_results, figure) + case "histogram": + figure = plt.figure(figsize=(20, 15), constrained_layout=True) + periscope_results = periscope_result.results_from_file(args.path) + histogram.plot_histogram(args, periscope_results, figure, of_dump=False) + case "histogram-after-dump": + periscope_results = periscope_result.results_from_file(args.path) + histogram.plot_histogram(args, periscope_results, figure, of_dump=True) + case _: + print("Unknown type passed.") + return + + if args.output: + plt.savefig(args.output) + else: + plt.show() + + +def parse_args(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "path", help="JSON file or path with json files with benchmark results" + ) + parser.add_argument("--title", help="Plot Title") + parser.add_argument("--sort-by", choices=["median", "wc"], help="Sort method") + parser.add_argument( + "--scale", choices=["linear", "log"], help="Scaling of the plog" + ) + parser.add_argument( + "--type", + choices=["whisker", "cmp-bars", "histogram", "histogram-after-dump"], + help="Creates a histogram with word count of \ + (dump of ) the model on y axis and the time on x axis \ + for each file.", + ) + parser.add_argument("-o", "--output", help="Save image to the given filename.") + + return parser.parse_args() + + +if __name__ == "__main__": + args = parse_args() + main(args) diff --git a/tools/periscope/periscope-py/src/periscope_result.py b/tools/periscope/periscope-py/src/periscope_result.py new file mode 100644 index 00000000..a1006e92 --- /dev/null +++ b/tools/periscope/periscope-py/src/periscope_result.py @@ -0,0 +1,237 @@ +import json +from typing import Optional +import jsonpickle +from os import listdir +from os.path import isfile + + +class HyperfineResult: + command: str + mean: float + stddev: float + median: float + user: float + system: float + min: float + max: float + times: list[float] + exit_codes: list[int] + + def __init__( + self, + command, + mean, + stddev, + median, + user, + system, + min, + max, + times, + exit_codes, + ) -> None: + self.command = command + self.mean = mean + self.stddev = stddev + self.median = median + self.user = user + self.system = system + self.min = min + self.max = max + self.times = times + self.exit_codes = exit_codes + + +def to_hyperfine_result(input: dict) -> HyperfineResult: + command, mean, stddev, median, user, system, min, max, times, exit_codes = ( + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + ) + if "command" in input: + command = input["command"] + if "mean" in input: + mean = input["mean"] + if "stddev" in input: + stddev = input["stddev"] + if "median" in input: + median = input["median"] + if "user" in input: + user = input["user"] + if "system" in input: + system = input["system"] + if "min" in input: + min = input["min"] + if "max" in input: + max = input["max"] + if "times" in input: + times = input["times"] + if "exit_codes" in input: + exit_codes = input["exit_codes"] + if ( + command is None + or mean is None + or stddev is None + or median is None + or user is None + or system is None + or min is None + or max is None + or times is None + or exit_codes is None + ): + raise Exception("Invalid JSON format for HyperfineResult") + else: + return HyperfineResult( + command, mean, stddev, median, user, system, min, max, times, exit_codes + ) + + +class Hyperfine: + results: list[HyperfineResult] + + def __init__(self, results) -> None: + self.results = results + + +def to_hyperfine(input: dict) -> Hyperfine: + results = [] + if "results" in input: + results = [to_hyperfine_result(res) for res in input["results"]] + + return Hyperfine(results) + + +class PeriscopeProp: + kind: str + name: str + node: int + idx: int + + def __init__(self, kind, name, node, idx) -> None: + self.kind = kind + self.name = name + self.node = node + self.idx = idx + + +def to_prop(input: dict) -> PeriscopeProp: + kind, name, node, idx = (None, None, None, None) + + if "kind" in input: + kind = input["kind"] + + if "name" in input: + name = input["name"] + + if "node" in input: + node = input["node"] + + if "idx" in input: + idx = input["idx"] + + if kind is None or name is None or node is None or idx is None: + raise Exception("Invalid JSON format for PeriscopeProp") + else: + return PeriscopeProp(kind, name, node, idx) + + +class PeriscopeResult: + props: list[PeriscopeProp] + steps: Optional[int] + hyperfine: Hyperfine + wc_raw: int + wc_btormc_dump: int + + def __init__(self, props, steps, hyperfine, wc_raw, wc_btormc_dump): + self.props = props + self.steps = steps + self.hyperfine = hyperfine + self.wc_raw = wc_raw + self.wc_btormc_dump = wc_btormc_dump + + +def to_per_result(input: dict) -> PeriscopeResult: + props, steps, hyperfine, wc_raw, wc_btormc_dump = ( + [], + None, + None, + None, + None, + ) + + if "props" in input: + props = [to_prop(prop) for prop in input["props"]] + + if "steps" in input: + steps = input["steps"] + + if "hyperfine" in input: + hyperfine = to_hyperfine(input["hyperfine"]) + + if "wc_raw" in input: + wc_raw = input["wc_raw"] + + if "wc_btormc_dump" in input: + wc_btormc_dump = input["wc_btormc_dump"] + + if props is None or hyperfine is None or wc_raw is None or wc_btormc_dump is None: + raise Exception("Invalid JSON format for PeriscopeResult") + else: + return PeriscopeResult(props, steps, hyperfine, wc_raw, wc_btormc_dump) + + +class PeriscopeResultEnum: + Success: Optional[PeriscopeResult] + Failed: Optional[PeriscopeResult] + + +class BenchResult: + name: str + results: PeriscopeResult + failed: bool + + def __init__(self, name: str, results: dict, failed: bool): + self.name = name + self.results = to_per_result(results) + self.failed = failed + + def hyperfine_results(self) -> list[HyperfineResult]: + return self.results.hyperfine.results + + +def to_bench_result(name: str, pre: dict) -> BenchResult: + if "Success" in pre: + return BenchResult(name, pre["Success"], False) + elif "Failed" in pre: + return BenchResult(name, pre["Failed"], True) + else: + raise Exception("Invalid JSON format for bench result") + + +def results_from_file(path: str) -> list[BenchResult]: + with open(path, encoding="utf-8") as f: + results_file = json.load(f) + + test = jsonpickle.decode( + json.dumps(results_file), + classes=( + PeriscopeResult, + PeriscopeResultEnum, + PeriscopeProp, + Hyperfine, + HyperfineResult, + ), + ) + + if isinstance(test, dict): + return [to_bench_result(name, pre) for name, pre in test.items()] + else: + raise Exception("Invalid JSON format") diff --git a/tools/periscope/periscope-py/src/whiskers.py b/tools/periscope/periscope-py/src/whiskers.py new file mode 100644 index 00000000..364c7af4 --- /dev/null +++ b/tools/periscope/periscope-py/src/whiskers.py @@ -0,0 +1,54 @@ +import argparse +import functools +import pathlib + +from matplotlib import figure +import matplotlib.pyplot as plt + +from periscope_result import BenchResult + + +def cmp_median(medians: list[float], labels: list[str]): + def compare(i, j): + med_cmp = medians[i] - medians[j] + if med_cmp == 0: + return labels[i] < labels[j] + else: + return med_cmp + + return compare + + +def plot_whiskers( + args: argparse.Namespace, + periscope_results: list[BenchResult], + figure: figure.Figure, +): + labels = [b.name for b in periscope_results] + times = [b.times for pr in periscope_results for b in pr.hyperfine_results()] + + if args.sort_by == "median": + medians = [b.median for pr in periscope_results for b in pr.hyperfine_results()] + indices = sorted( + range(len(labels)), + key=functools.cmp_to_key(cmp_median(medians, labels)), + ) + labels = [labels[i] for i in indices] + times = [times[i] for i in indices] + + _ = figure.subplots(1, 1) + plt.subplots(figsize=(20, 12), constrained_layout=True) + boxplot = plt.boxplot(times, vert=True, patch_artist=True) + cmap = plt.get_cmap("rainbow") + colors = [cmap(val / len(times)) for val in range(len(times))] + + for patch, color in zip(boxplot["boxes"], colors): + patch.set_facecolor(color) + + if args.title: + plt.title(args.title) + # plt.legend(handles=boxplot["boxes"], labels=labels, loc="best", fontsize="medium") + plt.title("Solving time and model size") + plt.ylabel("Time [s]") + plt.ylim(0, None) + plt.xticks(list(range(1, len(labels) + 1)), labels, rotation=65) diff --git a/tools/periscope/periscope-rs/.gitignore b/tools/periscope/periscope-rs/.gitignore new file mode 100644 index 00000000..92dd8f06 --- /dev/null +++ b/tools/periscope/periscope-rs/.gitignore @@ -0,0 +1,2 @@ +/target +/.periscope diff --git a/tools/periscope/periscope-rs/Cargo.lock b/tools/periscope/periscope-rs/Cargo.lock new file mode 100644 index 00000000..25f8ff4c --- /dev/null +++ b/tools/periscope/periscope-rs/Cargo.lock @@ -0,0 +1,340 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "anstream" +version = "0.6.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d96bd03f33fe50a863e394ee9718a706f988b9079b20c3784fb726e7678b62fb" +dependencies = [ + "anstyle", + "anstyle-parse", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "utf8parse", +] + +[[package]] +name = "anstyle" +version = "1.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8901269c6307e8d93993578286ac0edf7f195079ffff5ebdeea6a59ffb7e36bc" + +[[package]] +name = "anstyle-parse" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c75ac65da39e5fe5ab759307499ddad880d724eed2f6ce5b5e8a26f4f387928c" +dependencies = [ + "utf8parse", +] + +[[package]] +name = "anstyle-query" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e28923312444cdd728e4738b3f9c9cac739500909bb3d3c94b43551b16517648" +dependencies = [ + "windows-sys", +] + +[[package]] +name = "anstyle-wincon" +version = "3.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1cd54b81ec8d6180e24654d0b371ad22fc3dd083b6ff8ba325b72e00c87660a7" +dependencies = [ + "anstyle", + "windows-sys", +] + +[[package]] +name = "anyhow" +version = "1.0.83" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "25bdb32cbbdce2b519a9cd7df3a678443100e265d5e25ca763b7572a5104f5f3" + +[[package]] +name = "clap" +version = "4.5.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "90bc066a67923782aa8515dbaea16946c5bcc5addbd668bb80af688e53e548a0" +dependencies = [ + "clap_builder", + "clap_derive", +] + +[[package]] +name = "clap_builder" +version = "4.5.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae129e2e766ae0ec03484e609954119f123cc1fe650337e155d03b022f24f7b4" +dependencies = [ + "anstream", + "anstyle", + "clap_lex", + "strsim", +] + +[[package]] +name = "clap_derive" +version = "4.5.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "528131438037fd55894f62d6e9f068b8f45ac57ffa77517819645d10aed04f64" +dependencies = [ + "heck", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "clap_lex" +version = "0.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "98cc8fbded0c607b7ba9dd60cd98df59af97e84d24e49c8557331cfc26d301ce" + +[[package]] +name = "colorchoice" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7" + +[[package]] +name = "equivalent" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" + +[[package]] +name = "hashbrown" +version = "0.14.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1" + +[[package]] +name = "heck" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" + +[[package]] +name = "indexmap" +version = "2.2.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "168fb715dda47215e360912c096649d23d58bf392ac62f73919e831745e40f26" +dependencies = [ + "equivalent", + "hashbrown", +] + +[[package]] +name = "itoa" +version = "1.0.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" + +[[package]] +name = "memchr" +version = "2.7.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6c8640c5d730cb13ebd907d8d04b52f55ac9a2eec55b440c8892f40d56c76c1d" + +[[package]] +name = "minimal-lexical" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" + +[[package]] +name = "nom" +version = "7.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a" +dependencies = [ + "memchr", + "minimal-lexical", +] + +[[package]] +name = "periscope" +version = "0.1.0" +dependencies = [ + "anyhow", + "clap", + "nom", + "serde", + "serde_json", + "serde_yaml", +] + +[[package]] +name = "proc-macro2" +version = "1.0.79" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e835ff2298f5721608eb1a980ecaee1aef2c132bf95ecc026a11b7bf3c01c02e" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.35" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "291ec9ab5efd934aaf503a6466c5d5251535d108ee747472c3977cc5acc868ef" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "ryu" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f3cb5ba0dc43242ce17de99c180e96db90b235b8a9fdc9543c96d2209116bd9f" + +[[package]] +name = "serde" +version = "1.0.201" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "780f1cebed1629e4753a1a38a3c72d30b97ec044f0aef68cb26650a3c5cf363c" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.201" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c5e405930b9796f1c00bee880d03fc7e0bb4b9a11afc776885ffe84320da2865" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "serde_json" +version = "1.0.117" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "455182ea6142b14f93f4bc5320a2b31c1f266b66a4a5c858b013302a5d8cbfc3" +dependencies = [ + "itoa", + "ryu", + "serde", +] + +[[package]] +name = "serde_yaml" +version = "0.9.34+deprecated" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47" +dependencies = [ + "indexmap", + "itoa", + "ryu", + "serde", + "unsafe-libyaml", +] + +[[package]] +name = "strsim" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5ee073c9e4cd00e28217186dbe12796d692868f432bf2e97ee73bed0c56dfa01" + +[[package]] +name = "syn" +version = "2.0.55" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "002a1b3dbf967edfafc32655d0f377ab0bb7b994aa1d32c8cc7e9b8bf3ebb8f0" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "unicode-ident" +version = "1.0.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" + +[[package]] +name = "unsafe-libyaml" +version = "0.2.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "673aac59facbab8a9007c7f6108d11f63b603f7cabff99fabf650fea5c32b861" + +[[package]] +name = "utf8parse" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a" + +[[package]] +name = "windows-sys" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" +dependencies = [ + "windows-targets", +] + +[[package]] +name = "windows-targets" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7dd37b7e5ab9018759f893a1952c9420d060016fc19a472b4bb20d1bdd694d1b" +dependencies = [ + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", +] + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bcf46cf4c365c6f2d1cc93ce535f2c8b244591df96ceee75d8e83deb70a9cac9" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da9f259dd3bcf6990b55bffd094c4f7235817ba4ceebde8e6d11cd0c5633b675" + +[[package]] +name = "windows_i686_gnu" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b474d8268f99e0995f25b9f095bc7434632601028cf86590aea5c8a5cb7801d3" + +[[package]] +name = "windows_i686_msvc" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1515e9a29e5bed743cb4415a9ecf5dfca648ce85ee42e15873c3cd8610ff8e02" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5eee091590e89cc02ad514ffe3ead9eb6b660aedca2183455434b93546371a03" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "77ca79f2451b49fa9e2af39f0747fe999fcda4f5e241b2898624dca97a1f2177" + +[[package]] +name = "windows_x86_64_msvc" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8" diff --git a/tools/periscope/periscope-rs/Cargo.toml b/tools/periscope/periscope-rs/Cargo.toml new file mode 100644 index 00000000..48427598 --- /dev/null +++ b/tools/periscope/periscope-rs/Cargo.toml @@ -0,0 +1,17 @@ +[package] +name = "periscope" +description = "To be added" +version = "0.1.0" +edition = "2021" +authors = [ "Nadir Fejzic " ] +license = "MIT" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +anyhow = "1.0.83" +clap = { version = "4.5.4", features = ["derive"] } +nom = "7.1.3" +serde = { version = "1.0.201", features = ["serde_derive"] } +serde_json = "1.0.117" +serde_yaml = "0.9.34" diff --git a/tools/periscope/periscope-rs/README.md b/tools/periscope/periscope-rs/README.md new file mode 100644 index 00000000..a89af860 --- /dev/null +++ b/tools/periscope/periscope-rs/README.md @@ -0,0 +1,88 @@ +# peRISCope + +Small tool written as a part of my work for bachelor thesis. It can be used to +visualize simpler version of the witness format produced `btormc`, and for +benchmaring of `btormc`. + +## Requirements + +In order for some commands to successfully run, you need to have following tools +available on your system: + +- [Rust](https://www.rust-lang.org/learn/get-started) toolchain for building, + running and installation of the `periscope` binary. +- [boolector](https://boolector.github.io/) which provide the `btormc` binary. +- [`wc`](https://linux.die.net/man/1/wc) command for counting number of + characters in model files. +- [hyperfine](https://github.com/sharkdp/hyperfine) - command line benchmarking + tool +- [timeout](https://www.gnu.org/software/coreutils/manual/html_node/timeout-invocation.html) - command + for running commands with a time limit. + +## Build + +To build this project you need to have Rust toolchain installed on your +computer. Check the [official website](https://www.rust-lang.org/tools/install) +for installation instructions. + +After that, building is as simple as running: + +``` +cargo build +``` + +## Install + +You can also install the program on your machine: + +``` +cargo install --path . +``` + +This will make the `periscope` command available in your terminal. + +``` +periscope --help +``` + +## Running + +You can install the `periscope` as shown in the previous section. You can also +build and run directly using `cargo`: + +``` +cargo run -- +``` + +For better performance, you can use the `--release` flag: + +``` +cargo run --release -- +``` + +## Configuration + +peRISCope uses a configuration file in either JSON or YAML format. Consult the +reference configuration for more information: + +```yaml +# optional timeout. If present, the `btormc` command will run no longer than the +# number of seconds specified here. +timeout: 300 + +# optional additional flags for btormc. Default is "-kmax 200" +btormc-flags: "-kmax 200" + +# list of filenames to filter. Only models that match one of the filenames +# specified in this list will be benchmarked. +files: + - "model1.btor" + - "model2.btor" + +# list of run names and corresponding arguments for `rotor`. The `rotor` will +# be run with these (additional) arguments, and the results of the run will be +# saved in file with the name of the run as filename. +runs: + 32-codewordsize: "0 -codewordsize 32" + 64-codewordsize: "0 -codewordsize 64" +``` diff --git a/tools/periscope/periscope-rs/src/bench/hyperfine.rs b/tools/periscope/periscope-rs/src/bench/hyperfine.rs new file mode 100644 index 00000000..abe3bf87 --- /dev/null +++ b/tools/periscope/periscope-rs/src/bench/hyperfine.rs @@ -0,0 +1,73 @@ +use std::{fs::OpenOptions, io::Read, path::Path, process::Command}; + +use anyhow::Context; +use serde::{Deserialize, Serialize}; + +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct Hyperfine { + pub results: Vec, +} + +/// Results from a single run of `hyperfine`. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct HyperfineResult { + pub command: String, + pub mean: f64, + pub stddev: f64, + pub median: f64, + pub user: f64, + pub system: f64, + pub min: f64, + pub max: f64, + pub times: Vec, + pub exit_codes: Vec, +} + +/// Run `hyperfine` on a `btormc` and return the parsed results. +pub fn run( + path: impl AsRef, + hyperfine_output: impl AsRef, + hyperfine_json_path: impl AsRef, + btormc_flags: &Option, + timeout: Option, +) -> anyhow::Result { + let json_path = hyperfine_json_path.as_ref(); + let mut json_out = OpenOptions::new() + .create(true) + .write(true) + .truncate(true) + .read(true) + .open(json_path)?; + + let btormc_flags = btormc_flags.as_deref().unwrap_or("-kmax 200"); + let mut btormc_cmd = format!("btormc {} {}", path.as_ref().display(), btormc_flags); + + if let Some(timeout) = timeout { + btormc_cmd = format!("timeout --foreground {}s {}", timeout, btormc_cmd); + } + + let _ = Command::new("hyperfine") + .args(["--warmup", "3"]) + .args(["--runs", "5"]) + .arg("--ignore-failure") + .arg("--export-json") + .arg(json_path) + .args([ + "--output", + hyperfine_output + .as_ref() + .to_str() + .context("Invalid path for output from 'btormc'")?, + ]) + .arg(&btormc_cmd) + .spawn()? + .wait()?; + + let hyperfine: Hyperfine = serde_json::from_reader(&json_out).map_err(|_| { + let mut output = String::new(); + json_out.read_to_string(&mut output).unwrap_or_default(); + anyhow::format_err!("Failed reading json_output: \n{}\n", output) + })?; + + Ok(hyperfine) +} diff --git a/tools/periscope/periscope-rs/src/bench/mod.rs b/tools/periscope/periscope-rs/src/bench/mod.rs new file mode 100644 index 00000000..b0037377 --- /dev/null +++ b/tools/periscope/periscope-rs/src/bench/mod.rs @@ -0,0 +1,381 @@ +use std::{ + collections::HashMap, + ffi::OsStr, + fs::File, + path::{Path, PathBuf}, + sync::Mutex, +}; + +use anyhow::Context; +use serde::{Deserialize, Serialize}; + +use crate::btor; + +use self::hyperfine::Hyperfine; + +mod hyperfine; +mod rotor; +mod wc; + +/// Configuration for benchmarking. +#[derive(Default, Debug, Clone, Serialize, Deserialize)] +pub struct BenchConfig { + /// Timeout for each `btormc` run. No timeout per default. + pub timeout: Option, + + /// Additional flags to pass to `btormc` command. + #[serde(rename = "btormc-flags")] + pub btormc_flags: Option, + + /// Filenames to filter BTOR2 models. Models with filenames that don't match any of the files + /// specified in this filter will be ignored. + pub files: Vec, + + /// Names of benchmarking runs with their respective (additional) `rotor` arguments. + pub runs: HashMap, + + /// Path to the results file or folder. Not supported in configuration file, only as CLI + /// argument. + #[serde(skip)] + pub results_path: Option, +} + +#[derive(Debug, Clone, Serialize, Deserialize)] +struct Prop { + kind: btor::PropKind, + name: Option, + node: usize, + idx: u64, +} + +/// Possible results of a benchmark run. +#[derive(Debug, Clone, Serialize, Deserialize)] +enum BenchResult { + /// `btormc` terminated and witness format was successfully parsed. + Success { + /// Properties that were satisfied. + props: Vec, + /// Number of steps in the witness format. + steps: usize, + /// Output of benchmarking with `hyperfine`. + hyperfine: Hyperfine, + /// Word count in the BTOR2 file generated by `rotor`. + wc_raw: usize, + /// Word count in the BTOR2 dump generated by `btormc` after loading BTOR2 file from + /// `rotor`. + wc_btormc_dump: usize, + }, + /// `btormc` did not terminate within the specified timeout. + Failed { + /// `stdout` and `stderr` output of `hyperfine` + output: String, + /// Output of benchmarking with `hyperfine`. + hyperfine: Hyperfine, + /// Word count in the BTOR2 file generated by `rotor`. + wc_raw: usize, + /// Word count in the BTOR2 dump generated by `btormc` after loading BTOR2 file from + /// `rotor`. + wc_btormc_dump: usize, + }, +} + +/// Collects all `*.btor2` files in the given path and runs the `btormc` on them, benchmarking the +/// runs. +pub fn run_benches( + path: PathBuf, + bench_config: BenchConfig, + make_target: Option, + jobs: u8, +) -> anyhow::Result<()> { + let dot_periscope = create_dot_periscope(); + + if bench_config.runs.is_empty() { + bench_file_or_dir(path, &dot_periscope, bench_config) + } else { + run_benches_with_rotor(path, bench_config, &dot_periscope, make_target, jobs) + } +} + +/// Benchmarks a BTOR2 file or all BTOR2 files in the specified directory. +fn bench_file_or_dir( + path: PathBuf, + dot_periscope: &Path, + bench_config: BenchConfig, +) -> anyhow::Result<()> { + let (mut results, results_path) = + load_or_create_results(dot_periscope, bench_config.results_path); + + let mut paths: Vec = Vec::new(); + + if path.is_file() { + paths.push(path); + } else { + paths.extend( + std::fs::read_dir(&path) + .expect("Could not open directory.") + .flat_map(|e| e.ok().map(|e| e.path()).filter(|e| e.is_file())), + ); + } + + for path in paths { + let bench_result = self::bench_file( + &path, + dot_periscope, + bench_config.timeout, + &bench_config.btormc_flags, + )?; + + let filename = path + .file_name() + .and_then(OsStr::to_str) + .map(String::from) + .expect("Failed to get filename."); + + results.insert(filename, bench_result); + } + + let mut results_file = File::create(results_path).unwrap(); + serde_json::to_writer_pretty(&mut results_file, &results) + .expect("Failed serializing results into the results file."); + + Ok(()) +} + +/// Runst `rotor` with given configurations, then benchmarks the generated BTOR2 files with +/// `hyperfine` and `btormc`. +fn run_benches_with_rotor( + selfie_dir: PathBuf, + config: BenchConfig, + dot_periscope: &Path, + make_target: Option, + jobs: u8, +) -> anyhow::Result<()> { + for (name, rotor_args) in config.runs { + println!("\nRunning '{name}':"); + + // run rotor with the given config + rotor::run_rotor(&selfie_dir, &rotor_args, &make_target)?; + + // collect filtered files + let files: Vec = std::fs::read_dir(selfie_dir.join("examples").join("symbolic"))? + .filter_map(|entry| { + // only files + entry + .ok() + .and_then(|e| e.path().is_file().then(|| e.path())) + }) + .filter(|p| { + config + .files + .iter() + .any(|el| el == p.file_name().and_then(OsStr::to_str).unwrap_or_default()) + }) + .collect(); + + // ensure results dir exists: + let results_dir = dot_periscope.join("results"); + std::fs::create_dir_all(&results_dir).with_context(|| { + format!( + "Failed creating results directory at '{}'.", + results_dir.display() + ) + })?; + + // create results file + let results_path = results_dir.join(format!("{}.json", name)); + let (mut results, results_path) = load_or_create_results(dot_periscope, Some(results_path)); + + let run_single_bench = |file: PathBuf| -> anyhow::Result<(String, BenchResult)> { + let bench_result = + bench_file(&file, dot_periscope, config.timeout, &config.btormc_flags) + .with_context(|| format!("Failed benching file {}", file.display()))?; + + let filename = file + .file_name() + .and_then(OsStr::to_str) + .map(String::from) + .expect("Failed to get filename."); + + // results.insert(filename, bench_result); + Ok((filename, bench_result)) + }; + + if jobs > 1 { + let files = Mutex::new(files); + + let (tx, rx) = std::sync::mpsc::channel(); + + std::thread::scope(|s| { + for _ in 0..jobs { + println!("Spawning thread."); + s.spawn(|| loop { + let mut files_lock = files.lock().unwrap(); + let file = files_lock.pop(); + drop(files_lock); // release lock + + match file { + Some(f) => { + println!("Running bench on '{}'", f.display()); + let res = run_single_bench(f); + + if tx.send(res).is_err() { + break; + } + } + None => break, + } + }); + } + + while let Ok(res) = rx.recv() { + match res { + Ok((filename, bench_result)) => { + results.insert(filename, bench_result); + } + Err(err) => return Err(err), + } + } + + Ok(()) + })?; + } else { + for file in files { + let (filename, bench_result) = run_single_bench(file)?; + results.insert(filename, bench_result); + } + } + + let mut results_file = File::create(&results_path) + .with_context(|| format!("Failed creating '{}'", results_path.display()))?; + serde_json::to_writer_pretty(&mut results_file, &results) + .context("Failed serializing results into the results file.")?; + } + + Ok(()) +} + +/// Creates the `.periscope` directory for temporary data generated by the `periscope` command. +fn create_dot_periscope() -> PathBuf { + let dot_periscope = PathBuf::from(".periscope/bench"); + + if !dot_periscope.exists() || !dot_periscope.is_dir() { + std::fs::create_dir_all(&dot_periscope) + .unwrap_or_else(|err| panic!("Failed creating '{}': {}", dot_periscope.display(), err)) + } + + dot_periscope +} + +/// Loads the current results file (in JSON format) if it exists for further appending of new +/// results. If the file does not exist, it is created. +fn load_or_create_results( + dot_periscope: &Path, + results_path: Option, +) -> (HashMap, PathBuf) { + let results_path = results_path.unwrap_or_else(|| dot_periscope.join("results.json")); + + let results = File::open(&results_path) + .context("Failed reading file.") + .and_then(|f| serde_json::from_reader(&f).context("Falied deserializing results file.")) + .inspect_err(|err| { + eprintln!( + "Deserialization of '{}' failed: {}", + results_path.display(), + err + ) + }) + .unwrap_or_default(); + + (results, results_path) +} + +/// Benchmarks a single BTOR2 file with `btormc` and `hyperfine`. +fn bench_file( + path: impl AsRef, + dot_periscope: &Path, + timeout: Option, + btormc_flags: &Option, +) -> anyhow::Result { + let path = path.as_ref(); + let wc_raw = wc::char_count_in_file(path)?; + let wc_of_dump = wc::char_count_in_dump(path)?; + + debug_assert!(dot_periscope.exists()); + + let file_name = path.file_name().and_then(OsStr::to_str).unwrap_or_default(); + + let hyperfine_out_path = dot_periscope.join(format!("{file_name}_hyperfine_output")); + let hyperfine_json_path = dot_periscope.join(format!("{file_name}_hyperfine.json")); + let hyperfine = hyperfine::run( + path, + &hyperfine_out_path, + hyperfine_json_path, + btormc_flags, + timeout, + )?; + + let mut props_in_steps = { + if let Ok(witness) = + btor::parse_btor_witness(File::open(&hyperfine_out_path)?, File::open(path).ok()) + .inspect_err(|_| { + let witness = std::fs::read_to_string(&hyperfine_out_path).unwrap_or_default(); + format!("Failed parsing btor witness format: \n{}", witness); + }) + { + witness.props_in_steps() + } else { + return Ok(BenchResult::Failed { + output: std::fs::read_to_string(hyperfine_out_path)?, + hyperfine, + wc_raw, + wc_btormc_dump: wc_of_dump, + }); + } + }; + + assert!( + props_in_steps.len() == 1, + "Expected only 1 frame from btor2 witness format, but found {}.", + props_in_steps.len() + ); + + let props = props_in_steps[0] + .0 + .inner + .drain(..) + .map(|mut p| { + Ok(Prop { + kind: p.kind, + name: p.property.as_mut().and_then(|p| p.name.take()), + node: p + .property + .map(|p| p.node) + .context("Node ID is mandatory in btor2.")?, + idx: p.idx, + }) + }) + .collect::>>()?; + + let steps = props_in_steps[0].1; + + if props_in_steps.len() == 1 { + println!( + "{}:\n\t{} characters, {} characters in dump.\n\tFound {} in {} steps.", + path.file_name() + .and_then(OsStr::to_str) + .context("Invalid path to btor2 file.")?, + wc_raw, + wc_of_dump, + props_in_steps[0].0.formatted_string(), + props_in_steps[0].1 + ); + } + + Ok(BenchResult::Success { + props, + steps, + hyperfine, + wc_raw, + wc_btormc_dump: wc_of_dump, + }) +} diff --git a/tools/periscope/periscope-rs/src/bench/rotor.rs b/tools/periscope/periscope-rs/src/bench/rotor.rs new file mode 100644 index 00000000..dfd4e8d3 --- /dev/null +++ b/tools/periscope/periscope-rs/src/bench/rotor.rs @@ -0,0 +1,33 @@ +use std::{path::Path, process::Command}; + +/// Run rotor in the provided selfie directory. Make sure that the following make targets exist: +/// * `clean` +/// * `rotor-symbolic` +/// +/// Other make targets can be run by providing the corresponding CLI flag. [Commands::Bench] for more +/// information. +/// +/// [Commands::Bench]: crate::Commands::Bench +pub fn run_rotor( + selfie_dir: &Path, + rotor_args: &str, + make_target: &Option, +) -> anyhow::Result<()> { + // make sure we start fresh + Command::new("make") + .arg("clean") + .current_dir(selfie_dir) + .spawn()? + .wait()?; + + let make_target = make_target.as_deref().unwrap_or("rotor-symbolic"); + + Command::new("make") + .arg(make_target) + .arg(format!("rotor={}", rotor_args)) + .current_dir(selfie_dir) + .spawn()? + .wait()?; + + Ok(()) +} diff --git a/tools/periscope/periscope-rs/src/bench/wc.rs b/tools/periscope/periscope-rs/src/bench/wc.rs new file mode 100644 index 00000000..c5433ed9 --- /dev/null +++ b/tools/periscope/periscope-rs/src/bench/wc.rs @@ -0,0 +1,56 @@ +use std::{ + io::Write, + path::Path, + process::{Command, Stdio}, +}; + +use anyhow::Context; + +/// Count number of characters in the BTOR2 file generated by `rotor`. +pub fn char_count_in_file(file: impl AsRef) -> anyhow::Result { + let wc = Command::new("wc") + .arg("-c") + .arg(file.as_ref()) + .output()? + .stdout; + + parse_wc_output(&wc) +} + +/// Count the number of characters in dump generated by `btormc` from BTOR2 file generated by +/// `rotor`. +pub fn char_count_in_dump(path: impl AsRef) -> anyhow::Result { + let s = Command::new("btormc") + .arg("-d") + .arg(path.as_ref()) + .output()? + .stdout; + + let mut wc_child = Command::new("wc") + .arg("-c") + .arg("-") + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .spawn()?; + + if let Some(stdin) = wc_child.stdin.as_mut() { + stdin.write_all(&s)?; + } + + let wc = wc_child.wait_with_output()?.stdout; + + parse_wc_output(&wc) +} + +/// Parse the output of the `wc` command into `usize`. +fn parse_wc_output(output: &[u8]) -> anyhow::Result { + let idx = output + .iter() + .position(|c| c == &b' ') + .context("Bad output from 'wc' command.")?; + + let wc = std::str::from_utf8(output[..idx].as_ref())?; + + wc.parse() + .context("Could not parse output of 'wc' command.") +} diff --git a/tools/periscope/periscope-rs/src/btor/assignment.rs b/tools/periscope/periscope-rs/src/btor/assignment.rs new file mode 100644 index 00000000..27978044 --- /dev/null +++ b/tools/periscope/periscope-rs/src/btor/assignment.rs @@ -0,0 +1,155 @@ +use nom::{ + branch, + bytes::{self, complete}, + character, combinator, sequence, +}; +use std::fmt::Write; + +use super::helpers; + +#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] +pub enum AssignmentKind { + /// Assignment to a bitvector. + BitVec { + /// Value of the bitvector at the given transition. + value: u64, + /// Number of bits in the bitvector. + bits: usize, + }, + + /// Assignment to an array of bitvectors. + Array { + /// Index in the array + index: u64, + /// Value of the bitvector at `index` at the given transition. + value: u64, + /// Number of bits the bitvector + bits: usize, + }, +} + +impl AssignmentKind { + pub fn to_binary_string(self) -> String { + let (bits, extra) = match self { + AssignmentKind::BitVec { bits, .. } => (bits, 0), + AssignmentKind::Array { bits, .. } => (bits * 2, 4), + }; + + let mut buf = String::with_capacity(bits + extra); + + let write_bits = |buf: &mut String, value, len: usize| { + (0..len).rev().for_each(|i| { + let bit = (value >> i) & 1; + write!(buf, "{}", bit).expect("Writing to string is infallible."); + }); + }; + + match self { + AssignmentKind::BitVec { value, .. } => write_bits(&mut buf, value, bits), + AssignmentKind::Array { value, index, .. } => { + buf.push('['); + write_bits(&mut buf, index, bits / 2); + buf.push(']'); + + buf.push_str(" -> "); + + write_bits(&mut buf, value, bits / 2); + } + }; + + buf + } +} + +#[derive(Clone, PartialEq, Eq, PartialOrd, Ord)] +pub struct Assignment { + pub kind: AssignmentKind, + pub symbol: Option, +} + +impl Assignment { + pub fn parse(input: &str) -> nom::IResult<&str, Assignment> { + let (input, _uint) = helpers::uint(input)?; + + let (input, _whitespace) = character::complete::space0(input)?; + + let (input, assignment) = branch::alt((bitvec_assign, array_assign))(input)?; + + let (input, _whitespace) = character::complete::space0(input)?; + + let (input, symbol) = combinator::opt(symbol)(input)?; + + let (input, _newline) = helpers::newline(input)?; + + Ok(( + input, + Assignment { + kind: assignment, + symbol: symbol.map(String::from), + }, + )) + } + + pub fn get_value(&self) -> u64 { + match self.kind { + AssignmentKind::BitVec { value, .. } => value, + AssignmentKind::Array { value, .. } => value, + } + } +} + +impl std::fmt::Debug for Assignment { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + if let Some(symbol) = &self.symbol { + write!(f, "{} = ", symbol)?; + } + + write!(f, "{}", self.kind.to_binary_string())?; + + Ok(()) + } +} + +fn symbol(input: &str) -> nom::IResult<&str, &str> { + let (input, mut symbol) = + complete::take_while1(|txt: char| txt.is_ascii() && txt != '\n')(input)?; + + if let Some(idx) = symbol.find('@') { + symbol = &symbol[..idx]; + } + + Ok((input, symbol)) +} + +fn binary_string(input: &str) -> nom::IResult<&str, &str> { + bytes::complete::take_while1(|i| i == '0' || i == '1')(input) +} + +fn bitvec_assign(input: &str) -> nom::IResult<&str, AssignmentKind> { + combinator::map(binary_string, |val| { + let value = u64::from_str_radix(val, 2).expect("binary_string parses only 0s and 1s."); + + AssignmentKind::BitVec { + value, + bits: val.len(), + } + })(input) +} + +fn array_assign(input: &str) -> nom::IResult<&str, AssignmentKind> { + let array_index = sequence::preceded( + complete::tag("["), + sequence::terminated(binary_string, complete::tag("]")), + ); + + let array_index = sequence::terminated(array_index, character::complete::space0); + + combinator::map( + sequence::tuple((array_index, binary_string)), + |(idx, value)| AssignmentKind::Array { + index: idx.parse().expect("binary_string parses only 0s and 1s."), + value: u64::from_str_radix(value, 2).expect("binary_string parses only 0s and 1s."), + bits: value.len(), + }, + )(input) +} diff --git a/tools/periscope/periscope-rs/src/btor/btor2.rs b/tools/periscope/periscope-rs/src/btor/btor2.rs new file mode 100644 index 00000000..dabae8b2 --- /dev/null +++ b/tools/periscope/periscope-rs/src/btor/btor2.rs @@ -0,0 +1,47 @@ +use std::{ + collections::HashMap, + io::{BufRead, BufReader, Read}, +}; + +use serde::{Deserialize, Serialize}; + +use crate::btor::witness_format::PropKind; + +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct Property { + pub node: usize, + pub _kind: PropKind, + pub name: Option, +} + +pub(super) fn get_property_names(input: R) -> HashMap { + let input = BufReader::new(input); + input + .lines() + .filter(|line| match line { + Ok(line) => line + .split(' ') + .nth(1) + .is_some_and(|kind| kind == "bad" || kind == "justice"), + Err(_) => false, + }) + .enumerate() + .filter_map(|(idx, line)| { + let line = line.ok()?; + let mut iter = line.split(' '); + let node = iter.next()?.parse().ok()?; + let kind: PropKind = iter.next()?.parse().ok()?; + let name = iter.nth(1).map(String::from); + let idx = idx.try_into().ok()?; + + Some(( + idx, + Property { + node, + _kind: kind, + name, + }, + )) + }) + .collect() +} diff --git a/tools/periscope/periscope-rs/src/btor/helpers.rs b/tools/periscope/periscope-rs/src/btor/helpers.rs new file mode 100644 index 00000000..41734c2b --- /dev/null +++ b/tools/periscope/periscope-rs/src/btor/helpers.rs @@ -0,0 +1,14 @@ +use nom::{bytes::complete, character, combinator, sequence}; + +pub fn uint(input: &str) -> nom::IResult<&str, u64> { + combinator::map_res(character::complete::digit1, |s: &str| s.parse())(input) +} + +pub fn newline(input: &str) -> nom::IResult<&str, &str> { + complete::tag("\n")(input) +} + +pub fn comment(input: &str) -> nom::IResult<&str, ()> { + let first = sequence::preceded(complete::tag(";"), complete::take_until("\\n")); + combinator::map(sequence::terminated(first, newline), |_| ())(input) +} diff --git a/tools/periscope/periscope-rs/src/btor/mod.rs b/tools/periscope/periscope-rs/src/btor/mod.rs new file mode 100644 index 00000000..9f5aaec3 --- /dev/null +++ b/tools/periscope/periscope-rs/src/btor/mod.rs @@ -0,0 +1,252 @@ +mod assignment; +mod btor2; +mod helpers; +mod witness_format; + +use std::{ + collections::{BTreeMap, HashMap}, + fmt::Write, + io::Read, + str::FromStr, +}; + +use nom::{branch, combinator, multi}; + +use self::{ + assignment::Assignment, + btor2::Property, + witness_format::{WitnessFormat, WitnessFrame}, +}; + +pub use witness_format::{Prop, PropKind, PropVec}; + +pub fn parse_btor_witness( + mut input: I, + btor2: Option, +) -> anyhow::Result { + let mut buf = String::new(); + let _ = input.read_to_string(&mut buf); + + let mut witness = Witness::from_str(&buf) + .map_err(|err| anyhow::format_err!("Failed to parse witness. Cause: {err}"))?; + + if let Some(btor2_prop_names) = btor2.map(|inner| btor2::get_property_names(inner)) { + witness.add_prop_names(btor2_prop_names); + } + + Ok(witness) +} + +#[derive(Debug, Clone)] +pub struct Witness { + pub formats: Vec, +} + +impl FromStr for Witness { + type Err = String; + + fn from_str(input: &str) -> Result { + if input.is_empty() { + return Err(String::from("No satisfiable property found.")); + } + + let comment_parser = combinator::map(multi::many1(helpers::comment), |_| vec![]); + let whole_parser = branch::alt((comment_parser, multi::many1(WitnessFormat::parse))); + + let mut witness_parser = + combinator::map(whole_parser, |parsed| Witness { formats: parsed }); + + match witness_parser(input) { + Ok((rest, witness)) => { + if !rest.is_empty() { + Err(format!("Could not parse full input. Remaining: {rest}")) + } else { + Ok(witness) + } + } + Err(err) => Err(err.to_string()), + } + } +} + +enum FlowType { + State, + Input, +} + +impl Witness { + pub fn props_in_steps(&self) -> Vec<(PropVec, usize)> { + let mut res = Vec::with_capacity(self.formats.len()); + + for format in &self.formats { + let props = format.header.props.clone(); + res.push((PropVec { inner: props }, format.frames.len())); + } + + res + } + + pub fn analyze_and_report(&self) { + for (props, steps) in self.props_in_steps() { + let props = props + .inner + .iter() + .map(|prop| { + let mut prop_string = prop.to_string(); + + if matches!(&prop.property, Some(property) if property.name.is_some()) { + let property = prop.property.as_ref().unwrap(); + let _ = write!( + &mut prop_string, + " named '{}' with nid: {}", + property.name.as_ref().unwrap(), + property.node + ); + } + + prop_string + }) + .collect::>() + .join(", "); + + println!("Satisifed properties in {} steps:\n {}\n", steps, props,); + } + + self.analyze_input_flow(); + self.analyze_state_flow(); + } + + fn collect_assignments<'a, I>(iter: I) -> (BTreeMap>, u64) + where + I: Iterator, + { + let mut inputs: BTreeMap> = BTreeMap::new(); + let mut max_step = 1; + + for (idx, (frame, input)) in iter.enumerate() { + let step = frame.input_part.step; + + if step > max_step { + max_step = step; + } + + let idx_as_str = idx.to_string(); + let name = input.symbol.clone().unwrap_or(idx_as_str); + + let entry = inputs.entry(name).or_default(); + + let value = input.get_value(); + + match entry.last() { + Some((_, last_assignment)) => { + if last_assignment.get_value() != value { + entry.push((step, input.clone())); + } + } + None => entry.push((step, input.clone())), + } + } + + (inputs, max_step) + } + + fn print_flow( + inputs: &BTreeMap>, + max_step: u64, + flow_type: FlowType, + ) { + let indent = " ".repeat(4); + + let prefix = match flow_type { + FlowType::State => "#", + FlowType::Input => "@", + }; + + for (name, flow) in inputs.iter() { + println!("{indent}{}: ", name); + + let largest_val = flow + .iter() + .map(|(_, assignment)| assignment.get_value()) + .max() + .unwrap_or(1) + .max(1); + + let width = max_step.ilog10() as usize + 1; + let val_width = largest_val.ilog10() as usize + 1; + + for (idx, (step, assignment)) in flow.iter().enumerate() { + print!("{indent}{indent}"); + + if idx > 0 { + print!("-> "); + } else { + print!(" "); + } + + println!( + "{}{:>w$}: {:>v_w$} ({})", + prefix, + step, + assignment.get_value(), + assignment.kind.to_binary_string(), + w = width, + v_w = val_width, + ); + } + + println!( + "{indent}{indent}-> {}{:>w$}: end\n", + prefix, + max_step, + w = width + ); + } + } + + fn analyze_input_flow(&self) { + let frames_and_assignments = + self.formats + .iter() + .flat_map(|fmt| &fmt.frames) + .flat_map(|frame| { + std::iter::repeat(frame).zip(frame.input_part.model.assignments.iter()) + }); + + let (inputs, max_step) = Self::collect_assignments(frames_and_assignments); + + println!("Inputs flow:"); + + Self::print_flow(&inputs, max_step, FlowType::Input); + } + + fn analyze_state_flow(&self) { + let frames_and_assignments = + self.formats + .iter() + .flat_map(|fmt| &fmt.frames) + .flat_map(|frame| { + std::iter::repeat(frame).zip( + frame + .state_part + .iter() + .flat_map(|sp| sp.model.assignments.iter()), + ) + }); + + let (inputs, max_step) = Self::collect_assignments(frames_and_assignments); + + println!("States flow:"); + Self::print_flow(&inputs, max_step, FlowType::State); + } + + fn add_prop_names(&mut self, mut btor2_prop_names: HashMap) { + for format in &mut self.formats { + for prop in format.header.props.iter_mut() { + if let Some(property) = btor2_prop_names.remove(&prop.idx) { + prop.property = Some(property); + } + } + } + } +} diff --git a/tools/periscope/periscope-rs/src/btor/witness_format.rs b/tools/periscope/periscope-rs/src/btor/witness_format.rs new file mode 100644 index 00000000..67707f5e --- /dev/null +++ b/tools/periscope/periscope-rs/src/btor/witness_format.rs @@ -0,0 +1,209 @@ +use std::{fmt::Write, str::FromStr}; + +use nom::{branch, bytes::complete, character, combinator, multi, sequence}; +use serde::{Deserialize, Serialize}; + +use super::{assignment::Assignment, btor2::Property, helpers}; + +#[derive(Debug, Clone, Serialize, Deserialize)] +pub enum PropKind { + Bad, + Justice, +} + +impl FromStr for PropKind { + type Err = String; + + fn from_str(s: &str) -> Result { + match s { + "bad" => Ok(Self::Bad), + "justice" => Ok(Self::Justice), + _ => Err(format!("Unknown prop kind: '{s}'")), + } + } +} + +#[repr(transparent)] +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct PropVec { + pub inner: Vec, +} + +impl PropVec { + pub fn formatted_string(&self) -> String { + self.inner + .iter() + .map(|prop| { + let mut prop_string = prop.to_string(); + + if matches!(&prop.property, Some(property) if property.name.is_some()) { + let property = prop.property.as_ref().unwrap(); + let _ = write!( + &mut prop_string, + " named '{}' with nid: {}", + property.name.as_ref().unwrap(), + property.node + ); + } + + prop_string + }) + .collect::>() + .join(", ") + } +} + +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct Prop { + pub kind: PropKind, + pub idx: u64, + pub property: Option, +} + +impl std::fmt::Display for Prop { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self.kind { + PropKind::Bad => write!(f, "Bad at ")?, + PropKind::Justice => write!(f, "Justice at ")?, + }; + + write!(f, "{}", self.idx) + } +} + +impl Prop { + fn parse(input: &str) -> nom::IResult<&str, Self> { + combinator::map( + sequence::pair( + branch::alt((complete::tag("b"), complete::tag("j"))), + character::complete::digit1, + ), + |(kind_str, idx_str): (&str, &str)| { + let idx = idx_str.parse().expect("digit1 parses only digits."); + let kind = match kind_str { + "b" => PropKind::Bad, + "j" => PropKind::Justice, + _ => unreachable!("Parser recognizes only 'j' and 'b' as prop kinds."), + }; + Prop { + kind, + idx, + property: None, + } + }, + )(input) + } +} + +#[derive(Debug, Clone)] +pub struct WitnessHeader { + pub props: Vec, +} + +impl WitnessHeader { + fn parse(input: &str) -> nom::IResult<&str, Self> { + combinator::map( + sequence::terminated( + sequence::preceded(complete::tag("sat\n"), multi::many1(Prop::parse)), + helpers::newline, + ), + |props| WitnessHeader { props }, + )(input) + } +} + +#[derive(Debug, Default, Clone)] +pub struct Model { + pub assignments: Vec, +} + +impl Model { + fn parse(input: &str) -> nom::IResult<&str, Self> { + let comment = |input| { + combinator::opt(sequence::terminated(helpers::comment, helpers::newline))(input) + }; + + let assignment = combinator::opt(Assignment::parse); + + let model_parser = + combinator::map_opt(sequence::pair(comment, assignment), |(_, assignment)| { + assignment + }); + + combinator::map(multi::many1(model_parser), |assignments| Model { + assignments, + })(input) + } +} + +#[derive(Debug, Clone)] +pub struct Transition { + pub step: u64, + pub model: Model, +} + +impl Transition { + fn parse(input: &str) -> nom::IResult<&str, Self> { + combinator::map( + sequence::pair( + sequence::terminated(helpers::uint, helpers::newline), + combinator::opt(Model::parse), + ), + |(step, model)| Transition { + step, + model: model.unwrap_or_default(), + }, + )(input) + } +} + +#[derive(Debug, Clone)] +pub struct WitnessFrame { + pub state_part: Option, + pub input_part: Transition, +} + +impl WitnessFrame { + fn parse(input: &str) -> nom::IResult<&str, Self> { + let part_with_prefix = + |prefix| sequence::preceded(complete::tag(prefix), Transition::parse); + + let state_part = part_with_prefix("#"); + let input_part = part_with_prefix("@"); + + combinator::map( + sequence::pair(combinator::opt(state_part), input_part), + |(state_part, input_part)| Self { + state_part, + input_part, + }, + )(input) + } + + fn parse_multi(input: &str) -> nom::IResult<&str, Vec> { + multi::many1(Self::parse)(input) + } +} + +#[derive(Debug, Clone)] +pub struct WitnessFormat { + pub header: WitnessHeader, + pub frames: Vec, +} + +impl WitnessFormat { + pub fn parse(input: &str) -> nom::IResult<&str, Self> { + combinator::map( + sequence::tuple(( + WitnessHeader::parse, + WitnessFrame::parse_multi, + complete::tag("."), + combinator::opt(helpers::newline), + )), + |(_header, _frames, _dot, _newline)| WitnessFormat { + header: _header, + frames: _frames, + }, + )(input) + } +} diff --git a/tools/periscope/periscope-rs/src/lib.rs b/tools/periscope/periscope-rs/src/lib.rs new file mode 100644 index 00000000..1d897c6a --- /dev/null +++ b/tools/periscope/periscope-rs/src/lib.rs @@ -0,0 +1,94 @@ +use std::path::PathBuf; + +use clap::{Parser, Subcommand}; + +pub mod bench; +pub mod btor; + +#[derive(Debug, Clone, Parser)] +#[clap(long_about)] +pub struct Config { + /// Parse witness format of btormc generated from btor2 model. Parses from stdin if path to + /// file is not provided. + #[command(subcommand)] + pub command: Commands, +} + +#[derive(Debug, Clone, Subcommand)] +#[command(long_about)] +pub enum Commands { + ParseWitness { + /// Path to the witness file. + file: Option, + + /// Path to the BTOR2 model file, typically ends with '.btor2' extension. + #[arg(short, long)] + btor2: Option, + }, + + Bench { + /// Path to the results file where the benchmark results will be stored in JSON format. + /// By default, the results will be stored in the '.periscope/bench/results.json' file. + /// + /// If 'run-rotor' flag is provided, then the results are stored in + /// '.periscope/bench/results/{run-name}.json' regardless of this option. + #[arg(long)] + results_path: Option, + + /// Whether to run rotor to generate files first. + #[arg(short = 'r', long = "run-rotor")] + run_rotor: bool, + + /// Files that should be benchmarked. Files that do not match the provided names will be + /// ignored. + /// + /// The 'filter-files' option has priority if both 'filter-files' and 'filter-config' are + /// provided. + #[arg(short, long, requires = "run_rotor")] + filter_files: Vec, + + /// Config file that should be used for filtering. This is an alternative to using the + /// 'filter-files' option. The file can be in JSON or YAML format. + /// + /// The 'filter-files' option has priority if both 'filter-files' and 'filter-config' are + /// provided. + /// + /// # Example: + /// + /// ```yaml + /// # timeout in seconds + /// timeout: 300 # 5m = (5 * 60) s = 300 seconds + /// files: + /// - "file1.btor2" + /// - "file2.btor2" + /// - "file3.btor3" + /// + /// runs: + /// 8-bit-codeword-size: "0 -codewordsize 8" + /// 16-bit-codeword-size: "0 -codewordsize 16" + /// ``` + #[arg(short = 'c', long, requires = "run_rotor", verbatim_doc_comment)] + bench_config: Option, + + /// Path to the directory that contains selfie and rotor. You can clone selfie from + /// [selfie's Github repository](https://www.github.com/cksystemsteaching/selfie). + #[arg(short = 's', long = "selfie-dir", required_if_eq("run_rotor", "true"))] + selfie_dir: Option, + + /// Path to folder containing BTOR2 files. All BTOR2 files should have the ".btor2" + /// extension. Alternatively, path to a single BTOR2 file can be provided for single + /// benchmark. + #[arg(required_unless_present("run_rotor"))] + path: Option, + + /// Target for runing `make` inside of the selfie directory. + #[arg(short = 'm', long = "make-target", required_if_eq("run_rotor", "true"))] + make_target: Option, + + /// Number of parallel benchmarks to run. By default benchmarks are run sequentially. + /// However, if you have multiple CPU cores, you can spin-up multiple benchmarks in + /// parallel. Maximum value is 255. + #[arg(short = 'j', long = "jobs", default_value = "1")] + jobs: u8, + }, +} diff --git a/tools/periscope/periscope-rs/src/main.rs b/tools/periscope/periscope-rs/src/main.rs new file mode 100644 index 00000000..bdaa5eae --- /dev/null +++ b/tools/periscope/periscope-rs/src/main.rs @@ -0,0 +1,97 @@ +use std::{ffi::OsStr, io::Read, path::PathBuf}; + +use anyhow::Context; +use clap::Parser; +use periscope::{ + bench::{self, BenchConfig}, + btor::{self}, + Commands, Config, +}; + +fn main() -> anyhow::Result<()> { + let config = Config::parse(); + + match config.command { + Commands::ParseWitness { file, btor2 } => { + let witness: Box = match file { + Some(path) => Box::new(std::fs::File::open(path).unwrap()), + None => Box::new(std::io::stdin()), + }; + + let btor2 = btor2.and_then(|path| { + std::fs::File::open(path) + .inspect_err(|err| { + format!("Could not open provided btor2 file: {}", err); + }) + .ok() + }); + + let witness = btor::parse_btor_witness(witness, btor2)?; + + witness.analyze_and_report(); + } + Commands::Bench { + path, + run_rotor, + results_path, + filter_files, + bench_config, + selfie_dir, + make_target, + jobs, + } => { + let path = if run_rotor { + selfie_dir.context("Selfie directory is required when running rotor.")? + } else { + path.context( + "Path to a BTOR2 file or directory containing BTOR2 files is required.", + )? + }; + + let config = prepare_bench_config(run_rotor, filter_files, bench_config, results_path)?; + + bench::run_benches(path, config, make_target, jobs)?; + } + }; + + Ok(()) +} + +/// Reads and deserializes the configuration file for benchmarking. If no file is provided, default +/// configuration values are used. +fn prepare_bench_config( + run_rotor: bool, + filter_files: Vec, + bench_config_path: Option, + results_path: Option, +) -> anyhow::Result { + let mut config = BenchConfig::default(); + + if run_rotor { + config = bench_config_path + .map(|path| { + let file = std::fs::File::open(&path) + .map_err(|err| anyhow::format_err!("Could not open config file: {err}"))?; + + match path.extension().and_then(OsStr::to_str) { + Some("json") => { + serde_json::from_reader(file).context("Config has invalid JSON format.") + } + Some("yaml") => { + serde_yaml::from_reader(file).context("Config has invalid YAML format.") + } + _ => anyhow::bail!("Config file must be in JSON or YAML format."), + } + }) + .transpose()? + .unwrap_or_default(); + + if !filter_files.is_empty() { + config.files = filter_files; + } + } + + config.results_path = results_path; + + Ok(config) +}