Add more test cases (#91)

* Add more test cases

* Improve reconstruct

smt-log-parser/src/cmd/args.rs

@@ -43,5 +43,9 @@ pub enum Commands {
     Reconstruct {
         /// The path to the smt log file
         logfile: std::path::PathBuf,
+        /// Whether to print out the file without details about what happened
+        /// after each line
+        #[arg(short, long, default_value_t = false)]
+        clean: bool,
     },
 }

smt-log-parser/src/cmd/mod.rs

@@ -18,7 +18,7 @@ pub fn run() -> Result<(), String> {
         } => dependencies::run(logfile, depth, pretty_print)?,
         args::Commands::Stats { logfile, k } => stats::run(logfile, k)?,
         args::Commands::Test { logfiles, timeout } => test::run(logfiles, timeout)?,
-        args::Commands::Reconstruct { logfile } => reconstruct::run(logfile)?,
+        args::Commands::Reconstruct { logfile, clean } => reconstruct::run(logfile, clean)?,
     }
 
     Ok(())

smt-log-parser/src/cmd/reconstruct.rs

@@ -5,7 +5,7 @@ use smt_log_parser::{
     formatter::TermDisplayContext,
 };
 
-pub fn run(logfile: PathBuf) -> Result<(), String> {
+pub fn run(logfile: PathBuf, clean: bool) -> Result<(), String> {
     let parser = super::run_on_logfile(logfile)?;
     let config = DisplayConfiguration {
         replace_symbols: SymbolReplacement::None,
@@ -18,12 +18,12 @@ pub fn run(logfile: PathBuf) -> Result<(), String> {
         term_display: &term_display,
     };
     for event in parser.events.events() {
-        println!(
-            "{} ; {} enodes | {} insts",
-            event.kind.with(&ctxt),
-            event.enodes,
-            event.insts
-        );
+        print!("{}", event.kind.with(&ctxt));
+        if !clean {
+            println!(" ; {} enodes | {} insts", event.enodes, event.insts);
+        } else {
+            println!();
+        }
     }
 
     Ok(())

smt-problems/handwritten/prototype_logs/heaps.smt2

@@ -0,0 +1,22 @@
+(declare-sort Arr)
+(declare-sort Loc)
+(declare-sort Heap)
+
+(declare-fun slot (Arr Int) Loc)
+(declare-fun lookup (Heap Loc) Int)
+(declare-fun next (Loc) Loc)
+
+(declare-const h1 Heap)
+(declare-const h2 Heap)
+(declare-const a Arr)
+(declare-const size Int)
+(declare-const j Int)
+
+(assert (forall ((i Int)) (!
+  (or (= (lookup h2 (slot a i)) (lookup h1 (slot a (- i 32)))) (< i 32) (>= i size))
+)))
+
+(assert (>= j 1024))
+(assert (>= size (+ j 1024)))
+(assert (not (= (lookup h1 (slot a j)) 42)))
+(check-sat)

smt-problems/handwritten/prototype_logs/heaps2.smt2

@@ -0,0 +1,25 @@
+(declare-sort Arr)
+(declare-sort Loc)
+(declare-sort Heap)
+
+(declare-fun slot (Arr Int) Loc)
+(declare-fun lookup (Heap Loc) Int)
+(declare-fun next (Loc) Loc)
+
+(declare-const h1 Heap)
+(declare-const a Arr)
+(declare-const size Int)
+(declare-const j Int)
+
+(assert (forall ((i Int)) (!
+  (or (>= (lookup h1 (slot a i)) (lookup h1 (next (slot a i)))) (< i 0) (>= i size))
+)))
+(assert (forall ((ar Arr) (i Int)) (!
+  (= (next (slot a i)) (slot a (+ i 1)))
+  :pattern ((next (slot ar i)))
+)))
+
+(assert (>= j 1024))
+(assert (>= size (+ j 1024)))
+(assert (not (= (lookup h1 (slot a j)) 42)))
+(check-sat)

smt-problems/handwritten/rfmig_talk/a_running-example.smt2

@@ -0,0 +1,69 @@
+; some z3 options
+(set-option :print-success false)
+(set-info :smt-lib-version 2.0)
+(set-option :auto_config false)
+(set-option :smt.mbqi false)
+(set-option :smt.QI.EAGER_THRESHOLD 100)
+(set-option :smt.refine_inj_axioms false)
+
+
+(declare-sort Slice) ; &[i32]
+(declare-sort Address) ; *const i32
+(declare-sort Heap)
+
+; fn slot(slice: &[i32], idx: usize) -> *const i32 {
+;     &slice[idx] as *const _
+; }
+(declare-fun slot (Slice Int) Address)
+
+; unsafe fn lookup(address: *const i32) -> i32 {
+;     unsafe { *address }
+; }
+(declare-fun lookup (Heap Address) Int) ; dereference on the heap
+
+; fn next(address: *const i32) -> *const i32 {
+;     address.wrapping_offset(1)
+; }
+(declare-fun next (Address) Address)
+
+
+(assert (forall
+    ((slice Slice) (i Int) (j Int))
+    (!
+        ; ∀ slice, i, j. i != j ==> slot(slice, i) != slot(slice, j)
+        (or (= i j) (not (= (slot slice i) (slot slice j))))
+
+        :pattern ((slot slice i) (slot slice j))
+        :qid injectivity
+    )
+))
+(assert (forall
+    ((slice Slice) (i Int))
+    (!
+        ; ∀ slice, i. next(slot(slice, i)) == slot(slice, i + 1)
+        (= (next (slot slice i)) (slot slice (+ i 1)) )
+
+        :pattern ((slot slice i))
+        :qid next_def
+    )
+))
+
+(declare-const heap Heap)
+(declare-const s Slice)
+(declare-const idx Int)
+(declare-const len Int)
+
+(assert (forall
+    ((i Int))
+    (!
+        ; ∀ i. 0 <= i && i < len ==> lookup(heap, slot(s, i)) <= lookup(heap, next(slot(s, i)))
+        (or (< i 0) (>= i len) (<= (lookup heap (slot s i)) (lookup heap (next (slot s i)))) )
+
+        :pattern ((lookup heap (slot s i)))
+        :qid sortedness
+    )
+))
+
+(assert (and (>= idx 0) (< (+ idx 100) len)))
+(assert (not (< (lookup heap (slot s idx)) (lookup heap (next (slot s idx))) )))
+(check-sat)

smt-problems/handwritten/rfmig_talk/b_running-example.smt2

@@ -0,0 +1,69 @@
+; some z3 options
+(set-option :print-success false)
+(set-info :smt-lib-version 2.0)
+(set-option :auto_config false)
+(set-option :smt.mbqi false)
+(set-option :smt.QI.EAGER_THRESHOLD 100)
+(set-option :smt.refine_inj_axioms false)
+
+
+(declare-sort Slice) ; &[i32]
+(declare-sort Address) ; *const i32
+(declare-sort Heap)
+
+; fn slot(slice: &[i32], idx: usize) -> *const i32 {
+;     &slice[idx] as *const _
+; }
+(declare-fun slot (Slice Int) Address)
+
+; unsafe fn lookup(address: *const i32) -> i32 {
+;     unsafe { *address }
+; }
+(declare-fun lookup (Heap Address) Int) ; dereference on the heap
+
+; fn next(address: *const i32) -> *const i32 {
+;     address.wrapping_offset(1)
+; }
+(declare-fun next (Address) Address)
+
+
+(assert (forall
+    ((slice Slice) (i Int) (j Int))
+    (!
+        ; ∀ slice, i, j. i != j ==> slot(slice, i) != slot(slice, j)
+        (or (= i j) (not (= (slot slice i) (slot slice j))))
+
+        :pattern ((slot slice i) (slot slice j))
+        :qid injectivity
+    )
+))
+(assert (forall
+    ((slice Slice) (i Int))
+    (!
+        ; ∀ slice, i. next(slot(slice, i)) == slot(slice, i + 1)
+        (= (next (slot slice i)) (slot slice (+ i 1)) )
+
+        :pattern ((next (slot slice i)))
+        :qid next_def
+    )
+))
+
+(declare-const heap Heap)
+(declare-const s Slice)
+(declare-const idx Int)
+(declare-const len Int)
+
+(assert (forall
+    ((i Int))
+    (!
+        ; ∀ i. 0 <= i && i < len ==> lookup(heap, slot(s, i)) <= lookup(heap, next(slot(s, i)))
+        (or (< i 0) (>= i len) (<= (lookup heap (slot s i)) (lookup heap (next (slot s i)))) )
+
+        :pattern ((lookup heap (slot s i)))
+        :qid sortedness
+    )
+))
+
+(assert (and (>= idx 0) (< (+ idx 100) len)))
+(assert (not (< (lookup heap (slot s idx)) (lookup heap (next (slot s idx))) )))
+(check-sat)

smt-problems/handwritten/rfmig_talk/c_running-example.smt2

@@ -0,0 +1,74 @@
+; some z3 options
+(set-option :print-success false)
+(set-info :smt-lib-version 2.0)
+(set-option :auto_config false)
+(set-option :smt.mbqi false)
+(set-option :smt.QI.EAGER_THRESHOLD 100)
+(set-option :smt.refine_inj_axioms false)
+
+
+(declare-sort Slice) ; &[i32]
+(declare-sort Address) ; *const i32
+(declare-sort Heap)
+
+; fn slot(slice: &[i32], idx: usize) -> *const i32 {
+;     &slice[idx] as *const _
+; }
+(declare-fun slot (Slice Int) Address)
+
+; fn slot_inverse(slice: &[i32], address: *const i32) -> usize {
+;     ...
+; }
+(declare-fun slot_inverse (Slice Address) Int)
+
+; unsafe fn lookup(address: *const i32) -> i32 {
+;     unsafe { *address }
+; }
+(declare-fun lookup (Heap Address) Int) ; dereference on the heap
+
+; fn next(address: *const i32) -> *const i32 {
+;     address.wrapping_offset(1)
+; }
+(declare-fun next (Address) Address)
+
+
+(assert (forall
+    ((slice Slice) (i Int))
+    (!
+        ; ∀ slice, i. i == slot_inverse(slice, slot(slice, i))
+        (= i (slot_inverse slice (slot slice i)) )
+
+        :pattern ((slot slice i))
+        :qid injectivity
+    )
+))
+(assert (forall
+    ((slice Slice) (i Int))
+    (!
+        ; ∀ slice, i. next(slot(slice, i)) == slot(slice, i + 1)
+        (= (next (slot slice i)) (slot slice (+ i 1)) )
+
+        :pattern ((next (slot slice i)))
+        :qid next_def
+    )
+))
+
+(declare-const heap Heap)
+(declare-const s Slice)
+(declare-const idx Int)
+(declare-const len Int)
+
+(assert (forall
+    ((i Int))
+    (!
+        ; ∀ i. 0 <= i && i < len ==> lookup(heap, slot(s, i)) <= lookup(heap, next(slot(s, i)))
+        (or (< i 0) (>= i len) (<= (lookup heap (slot s i)) (lookup heap (next (slot s i)))) )
+
+        :pattern ((lookup heap (slot s i)))
+        :qid sortedness
+    )
+))
+
+(assert (and (>= idx 0) (< (+ idx 100) len)))
+(assert (not (< (lookup heap (slot s idx)) (lookup heap (next (slot s idx))) )))
+(check-sat)

smt-problems/handwritten/rfmig_talk/d_running-example.smt2

@@ -0,0 +1,74 @@
+; some z3 options
+(set-option :print-success false)
+(set-info :smt-lib-version 2.0)
+(set-option :auto_config false)
+(set-option :smt.mbqi false)
+(set-option :smt.QI.EAGER_THRESHOLD 100)
+(set-option :smt.refine_inj_axioms false)
+
+
+(declare-sort Slice) ; &[i32]
+(declare-sort Address) ; *const i32
+(declare-sort Heap)
+
+; fn slot(slice: &[i32], idx: usize) -> *const i32 {
+;     &slice[idx] as *const _
+; }
+(declare-fun slot (Slice Int) Address)
+
+; fn slot_inverse(slice: &[i32], address: *const i32) -> usize {
+;     ...
+; }
+(declare-fun slot_inverse (Slice Address) Int)
+
+; unsafe fn lookup(address: *const i32) -> i32 {
+;     unsafe { *address }
+; }
+(declare-fun lookup (Heap Address) Int) ; dereference on the heap
+
+; fn next(address: *const i32) -> *const i32 {
+;     address.wrapping_offset(1)
+; }
+(declare-fun next (Address) Address)
+
+
+(assert (forall
+    ((slice Slice) (i Int))
+    (!
+        ; ∀ slice, i. i == slot_inverse(slice, slot(slice, i))
+        (= i (slot_inverse slice (slot slice i)) )
+
+        :pattern ((slot slice i))
+        :qid injectivity
+    )
+))
+(assert (forall
+    ((slice Slice) (i Int))
+    (!
+        ; ∀ slice, i. next(slot(slice, i)) == slot(slice, i + 1)
+        (= (next (slot slice i)) (slot slice (+ i 1)) )
+
+        :pattern ((next (slot slice i)))
+        :qid next_def
+    )
+))
+
+(declare-const heap Heap)
+(declare-const s Slice)
+(declare-const idx Int)
+(declare-const len Int)
+
+(assert (forall
+    ((i Int) (j Int))
+    (!
+        ; ∀ i, j. 0 <= i && i < j && j < len ==> lookup(heap, slot(s, i)) <= lookup(heap, slot(s, j))
+        (or (< i 0) (>= i j) (>= j len) (<= (lookup heap (slot s i)) (lookup heap (slot s j))) )
+
+        :pattern ((lookup heap (slot s i)) (lookup heap (slot s j)))
+        :qid sortedness
+    )
+))
+
+(assert (and (>= idx 0) (< (+ idx 100) len)))
+(assert (not (< (lookup heap (slot s idx)) (lookup heap (next (slot s idx))) )))
+(check-sat)