Update smt-logs and add time

viperproject · Jan 27, 2025 · 4775b3e · 4775b3e
1 parent 044bfb5
commit 4775b3e
Show file tree

Hide file tree

Showing 5 changed files with 851 additions and 81 deletions.
diff --git a/eval/Analyse.ipynb b/eval/Analyse.ipynb
diff --git a/eval/eval.sh b/eval/eval.sh
@@ -24,15 +24,17 @@ while read -r file; do
 
     # [ "$FILE" == "silicon/silver/src/test/resources/quantifiedpermissions/misc/functions-01.smt2" ] || continue
     cd "$DIRNAME/data"
-    "$SMT2_DIR/z3.sh" "$file"
+    exec 3>&1 4>&2
+    Z3_TIME=$(TIMEFORMAT="%R"; { time "$SMT2_DIR/z3.sh" "$file" 1>&3 2>&4; } 2>&1)
+    exec 3>&- 4>&-
 
     OUTPUT_DIR="$(dirname "$OUTPUT")"
     LOGFILE="$(find "$OUTPUT_DIR" -name "$(basename "$OUTPUT")-fHash-*.log" -maxdepth 1 -type f)"
     [ ! -n "$LOGFILE" ] && echo "!!! No logfile found" && continue || true
     [ ! -s "$LOGFILE" ] && echo "!!! Log file is empty for \"$FILE\"" && continue || true
     cd "$OUTPUT_DIR"
 
-    echo "[LOGFILE] $(basename "$LOGFILE") $(ls -l "$LOGFILE" | awk '{print $5}')b" > "$OUTPUT.data"
+    echo "[LOGFILE] $(basename "$LOGFILE") $(ls -l "$LOGFILE" | awk '{print $5}')b ${Z3_TIME}s" > "$OUTPUT.data"
     "$DIRNAME/run.sh" "$LOGFILE" >> "$OUTPUT.data"
 
     rm -f "$LOGFILE"

diff --git a/eval/smt-logs b/eval/smt-logs
diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs
@@ -13,7 +13,7 @@ use mem_dbg::{MemDbg, MemSize};
 
 use crate::{idx, items::InstIdx, BoxSlice, FxHashMap, Graph, TiVec};
 
-pub const MIN_MATCHING_LOOP_LENGTH: u32 = 6;
+pub const MIN_MATCHING_LOOP_LENGTH: u32 = 5;
 
 idx!(MlSigIdx, "∞{}");
 

diff --git a/smt-log-parser/src/bin/smt-scope/cmd/eval.rs b/smt-log-parser/src/bin/smt-scope/cmd/eval.rs
@@ -73,6 +73,13 @@ pub fn run(logfile: PathBuf, dummy: bool) -> Result<(), String> {
             }
         }
         println!("{}", to_print.join(" -> "));
+        if ml.leaves.0.len() > 1 {
+            print!("[ExtraLoop]");
+            for (repetitions, _) in ml.leaves.0.iter().skip(1) {
+                print!(" {repetitions}");
+            }
+            println!();
+        }
     }
     let rpq = redundancy.per_quant.iter_enumerated();
     let pos_im = rpq.filter(|(_, d)| d.input_multiplicativity() > 1.0);