Add eval

Reduce mono memory limit

.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

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

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

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

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

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

eval/smt-scope/build.sh

@@ -0,0 +1,2 @@
+cd "$(dirname "$0")/../.."
+cargo build --release --bin smt-log-parser

eval/smt-scope/run.sh

@@ -0,0 +1,2 @@
+EXE="$(dirname "$0")/../../target/release/smt-log-parser"
+$EXE eval $1

smt-log-parser/src/bin/smt-scope/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,
+    },
 }

smt-log-parser/src/bin/smt-scope/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(())
+}

smt-log-parser/src/bin/smt-scope/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(())