From c7ea696d70ed7a08e932175926e8a754dc54a7bf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Tue, 7 Jan 2025 18:18:34 +0100 Subject: [PATCH] Add eval Reduce mono memory limit --- .github/workflows/eval.yml | 32 ++++++++++++++++++++++++++++++ eval/axiom-profiler/build.sh | 5 +++++ eval/axiom-profiler/run.sh | 6 ++++++ eval/build.sh | 13 ++++++++++++ eval/eval.sh | 25 +++++++++++++++++++++++ eval/run.sh | 8 ++++++++ eval/smt-scope/build.sh | 2 ++ eval/smt-scope/run.sh | 2 ++ smt-log-parser/src/cmd/args.rs | 5 +++++ smt-log-parser/src/cmd/eval.rs | 36 ++++++++++++++++++++++++++++++++++ smt-log-parser/src/cmd/mod.rs | 2 ++ 11 files changed, 136 insertions(+) create mode 100644 .github/workflows/eval.yml create mode 100755 eval/axiom-profiler/build.sh create mode 100755 eval/axiom-profiler/run.sh create mode 100755 eval/build.sh create mode 100755 eval/eval.sh create mode 100755 eval/run.sh create mode 100755 eval/smt-scope/build.sh create mode 100755 eval/smt-scope/run.sh create mode 100644 smt-log-parser/src/cmd/eval.rs diff --git a/.github/workflows/eval.yml b/.github/workflows/eval.yml new file mode 100644 index 00000000..91e1ba5d --- /dev/null +++ b/.github/workflows/eval.yml @@ -0,0 +1,32 @@ +name: Run evaluation +on: + push: + branches: [cav-eval] + workflow_dispatch: + +jobs: + eval: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + - name: Install Z3 + uses: pavpanchekha/setup-z3@1.2.2 + with: + version: '4.8.7' + - name: Cache cargo + uses: Swatinem/rust-cache@v2 + with: + shared-key: "shared" + - run: ./eval/build.sh + - run: ./eval/eval.sh + + - name: Archive data for upload + if: always() + run: tar -czf data.tar.bz2 eval/data/ + - uses: actions/upload-artifact@v4.4.3 + if: always() + with: + name: "data" + path: data.tar.bz2 + retention-days: 30 diff --git a/eval/axiom-profiler/build.sh b/eval/axiom-profiler/build.sh new file mode 100755 index 00000000..623a641c --- /dev/null +++ b/eval/axiom-profiler/build.sh @@ -0,0 +1,5 @@ +cd "$(dirname "$0")" +rm -rf axiom-profiler +wget -O axiom-profiler.zip https://github.com/viperproject/axiom-profiler/releases/download/v-2025-01-08-0833/axiom-profiler-release-windows.zip +unzip -d axiom-profiler axiom-profiler.zip +rm -f axiom-profiler.zip diff --git a/eval/axiom-profiler/run.sh b/eval/axiom-profiler/run.sh new file mode 100755 index 00000000..d9bd4472 --- /dev/null +++ b/eval/axiom-profiler/run.sh @@ -0,0 +1,6 @@ +export MONO_GC_PARAMS="max-heap-size=14G" +SDIR="$(dirname "$0")" +mono "$SDIR/axiom-profiler/AxiomProfiler.exe" /headless /timing /loops:2147483647 /loopsMs:10000 /showNumChecks /showQuantStatistics /findHighBranching:6 /l:$1 +EXIT_CODE=$? +rm -f AxiomProfiler.basic AxiomProfiler.branching AxiomProfiler.loops AxiomProfiler.error +exit $EXIT_CODE diff --git a/eval/build.sh b/eval/build.sh new file mode 100755 index 00000000..8f14574d --- /dev/null +++ b/eval/build.sh @@ -0,0 +1,13 @@ +DIRNAME="$(realpath "$(dirname "$0")")" + +cd "$DIRNAME" +rm -rf smt-logs-smt2 +wget -O smt-logs.tar.gz https://github.com/viperproject/smt-logs/archive/refs/heads/smt2.tar.gz +tar -xvf smt-logs.tar.gz +rm -f smt-logs.tar.gz + +TOOLS="axiom-profiler smt-scope" +for tool in $TOOLS; do + cd "$DIRNAME/$tool" + ./build.sh || exit 1 +done diff --git a/eval/eval.sh b/eval/eval.sh new file mode 100755 index 00000000..b30b4182 --- /dev/null +++ b/eval/eval.sh @@ -0,0 +1,25 @@ +DIRNAME="$(realpath "$(dirname "$0")")" +mkdir -p "$DIRNAME/data" + +SMT2_DIR="$DIRNAME/smt-logs-smt2/smt2" +SMT2_FILES="$(find "$SMT2_DIR" -name "*.smt2")" + +while read -r file; do + cd "$DIRNAME/data" + "$SMT2_DIR/z3.sh" "$file" + + FILE="${file#"$SMT2_DIR/"}" + OUTPUT="$DIRNAME/data/${FILE%.*}" + OUTPUT_DIR="$(dirname "$OUTPUT")" + LOGFILE="$(find "$OUTPUT_DIR" -name "$(basename "$OUTPUT")-fHash-*.log" -maxdepth 1 -type f)" + [ -n "$LOGFILE" ] || exit 1 + [ -s "$LOGFILE" ] || exit 1 + cd "$OUTPUT_DIR" + + echo "\n[LOGFILE] $(basename "$LOGFILE") $(ls -l "$LOGFILE" | awk '{print $5}')b" > "$OUTPUT.data" + "$DIRNAME/run.sh" "$LOGFILE" >> "$OUTPUT.data" + + rm -f "$LOGFILE" +done <<< "$SMT2_FILES" + +# > Z3_EXE="~/Downloads/z3-4.8.7-x64-osx-10.14.6/bin/z3" ./eval/eval.sh diff --git a/eval/run.sh b/eval/run.sh new file mode 100755 index 00000000..75cd3ee3 --- /dev/null +++ b/eval/run.sh @@ -0,0 +1,8 @@ +DIRNAME="$(realpath "$(dirname "$0")")" + +TOOLS="axiom-profiler smt-scope" +for tool in $TOOLS; do + RUN="$DIRNAME/$tool/run.sh" + echo "[tool] $tool" + "$RUN" "$1" || exit 1 +done diff --git a/eval/smt-scope/build.sh b/eval/smt-scope/build.sh new file mode 100755 index 00000000..bfbc1480 --- /dev/null +++ b/eval/smt-scope/build.sh @@ -0,0 +1,2 @@ +cd "$(dirname "$0")/../.." +cargo build --release --bin smt-log-parser diff --git a/eval/smt-scope/run.sh b/eval/smt-scope/run.sh new file mode 100755 index 00000000..0c954746 --- /dev/null +++ b/eval/smt-scope/run.sh @@ -0,0 +1,2 @@ +EXE="$(dirname "$0")/../../target/release/smt-log-parser" +$EXE eval $1 diff --git a/smt-log-parser/src/cmd/args.rs b/smt-log-parser/src/cmd/args.rs index 05fca1ee..f274c8c6 100644 --- a/smt-log-parser/src/cmd/args.rs +++ b/smt-log-parser/src/cmd/args.rs @@ -56,4 +56,9 @@ pub enum Commands { /// The path to the smt log file logfile: std::path::PathBuf, }, + /// Run evaluation mode which times automatic analysis + Eval { + /// The path to the smt log file + logfile: std::path::PathBuf, + }, } diff --git a/smt-log-parser/src/cmd/eval.rs b/smt-log-parser/src/cmd/eval.rs new file mode 100644 index 00000000..cdeaa6dd --- /dev/null +++ b/smt-log-parser/src/cmd/eval.rs @@ -0,0 +1,36 @@ +use std::{ + path::PathBuf, + time::{Duration, Instant}, +}; + +use smt_log_parser::analysis::{InstGraph, RedundancyAnalysis}; + +pub struct Timer(Instant); +impl Timer { + pub fn start() -> Self { + Self(Instant::now()) + } + pub fn lap(&mut self) -> Duration { + let old = core::mem::replace(&mut self.0, Instant::now()); + self.0 - old + } +} + +pub fn run(logfile: PathBuf) -> Result<(), String> { + let mut timer = Timer::start(); + let mut parser = super::run_on_logfile(logfile)?; + let parse_time = timer.lap(); + let mut graph = InstGraph::new_lite(&parser).map_err(|e| format!("{e:?}"))?; + let graph_time = timer.lap(); + let loops = graph.search_matching_loops(&mut parser); + let redundancy = RedundancyAnalysis::new(&parser); + let analysis_time = timer.lap(); + println!("[Parse] {}us", parse_time.as_micros()); + println!("[Graph] {}us", graph_time.as_micros()); + println!("[Analysis] {}us", analysis_time.as_micros()); + println!("[Loops] {} true, {} false", loops.sure_mls, loops.maybe_mls); + let rpq = redundancy.per_quant.iter_enumerated(); + let pos_im = rpq.filter(|(_, d)| d.input_multiplicativity() > 1.0); + println!("[Branching] {}", pos_im.count()); + Ok(()) +} diff --git a/smt-log-parser/src/cmd/mod.rs b/smt-log-parser/src/cmd/mod.rs index 0dc7ed85..94f06bf3 100644 --- a/smt-log-parser/src/cmd/mod.rs +++ b/smt-log-parser/src/cmd/mod.rs @@ -1,6 +1,7 @@ mod args; #[cfg(feature = "analysis")] mod dependencies; +mod eval; mod reconstruct; mod redundancy; mod stats; @@ -25,6 +26,7 @@ pub fn run() -> Result<(), String> { } => test::run(logfiles, timeout, memory)?, args::Commands::Reconstruct { logfile, clean } => reconstruct::run(logfile, clean)?, args::Commands::Redundancy { logfile } => redundancy::run(logfile)?, + args::Commands::Eval { logfile } => eval::run(logfile)?, } Ok(())