Clean up SMT preambles, fix modulo operator encoding

viperproject · Oct 22, 2023 · 8e18928 · 8e18928
1 parent d97b664
commit 8e18928
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 90 deletions.
diff --git a/native-verifier/src/smt_lib.rs b/native-verifier/src/smt_lib.rs
@@ -67,8 +67,13 @@ impl SMTLib {
                 self.add_code(format!("(assert {})", expression.to_smt()));
             }
             FolStatement::Assert { expression, reason } => {
-                // negate predicate
                 let position = expression.position();
+
+                if position.id == 0 {
+                    return;
+                }
+
+                // negate predicate
                 let negated = Expression::UnaryOp(UnaryOp {
                     op_kind: UnaryOpKind::Not,
                     argument: Box::new(expression.clone()),
@@ -647,7 +652,7 @@ impl SMTTranslatable for IntBinaryOpKind {
             BinaryOpKind::Sub => "-",
             BinaryOpKind::Mul => "*",
             BinaryOpKind::Div => "div",
-            BinaryOpKind::Mod => "mod",
+            BinaryOpKind::Mod => "rust_mod",
             BinaryOpKind::And => "and",
             BinaryOpKind::Or => "or",
             BinaryOpKind::Implies => "=>",

diff --git a/native-verifier/src/theories/Preamble.smt2 b/native-verifier/src/theories/Preamble.smt2
@@ -6,55 +6,22 @@
 (set-option :produce-models true) ; equivalent to model.v2 in Z3
 (set-option :produce-assignments false) ; similar to model.partial in Z3
 
-; --- Floating-point arithmetic ---
+; --- Modelling Rust's implementation of % ---
 
-(define-fun fp.neq32 ((x (_ FloatingPoint 8 24)) (y (_ FloatingPoint 8 24))) Bool (not (fp.eq x y)))
-(define-fun fp.neq64 ((x (_ FloatingPoint 11 53)) (y (_ FloatingPoint 11 53))) Bool (not (fp.eq x y)))
-
-; --- Snapshots ---
-
-(declare-datatypes (($Snap 0)) ((
-    ($Snap.unit)
-    ($Snap.combine ($Snap.first $Snap) ($Snap.second $Snap)))))
+(define-fun rust_mod ((dividend Int) (divisor Int)) Int
+  (ite (>= dividend 0)
+    (mod dividend (abs divisor))
+    (- (mod (- dividend) (abs divisor)))
+  )
+)
 
-; --- References ---
+; --- Inequality operator for FloatingPoint bit-vectors ---
 
-(declare-sort $Ref 0)
-(declare-const $Ref.null $Ref)
+(define-fun fp.neq32 ((x (_ FloatingPoint 8 24)) (y (_ FloatingPoint 8 24))) Bool (not (fp.eq x y)))
+(define-fun fp.neq64 ((x (_ FloatingPoint 11 53)) (y (_ FloatingPoint 11 53))) Bool (not (fp.eq x y)))
 
-; --- Permissions ---
+; --- Legacy permission sort ---
 
-(declare-sort $FPM 0)
-(declare-sort $PPM 0)
 (define-sort $Perm () Real)
 
-(define-const $Perm.Write $Perm 1.0)
-(define-const $Perm.No $Perm 0.0)
-
-(define-fun $Perm.isValidVar ((p $Perm)) Bool
-	(<= $Perm.No p))
-
-(define-fun $Perm.isReadVar ((p $Perm)) Bool
-    (and ($Perm.isValidVar p)
-         (not (= p $Perm.No))))
-
-; min function for permissions
-(define-fun $Perm.min ((p1 $Perm) (p2 $Perm)) Real
-    (ite (<= p1 p2) p1 p2))
-
-; --- Sort wrappers ---
-
-; Sort wrappers are no longer part of the static preamble. Instead, they are
-; emitted as part of the program-specific preamble.
-
-; --- Math ---
-
-;function Math#min(a: int, b: int): int;
-(define-fun $Math.min ((a Int) (b Int)) Int
-    (ite (<= a b) a b))
-
-;function Math#clip(a: int): int;
-(define-fun $Math.clip ((a Int)) Int
-    (ite (< a 0) 0 a))
-
 ; ===== End static preamble =====
diff --git a/native-verifier/src/theories/PreambleZ3.smt2 b/native-verifier/src/theories/PreambleZ3.smt2
@@ -35,55 +35,22 @@
 
 (set-option :timeout 10000)
 
-; --- Floating-point arithmetic ---
+; --- Modelling Rust's implementation of % ---
 
-(define-fun fp.neq32 ((x (_ FloatingPoint 8 24)) (y (_ FloatingPoint 8 24))) Bool (not (fp.eq x y)))
-(define-fun fp.neq64 ((x (_ FloatingPoint 11 53)) (y (_ FloatingPoint 11 53))) Bool (not (fp.eq x y)))
-
-; --- Snapshots ---
-
-(declare-datatypes (($Snap 0)) ((
-    ($Snap.unit)
-    ($Snap.combine ($Snap.first $Snap) ($Snap.second $Snap)))))
+(define-fun rust_mod ((dividend Int) (divisor Int)) Int
+  (ite (>= dividend 0)
+    (mod dividend (abs divisor))
+    (- (mod (- dividend) (abs divisor)))
+  )
+)
 
-; --- References ---
+; --- Inequality operator for FloatingPoint bit-vectors ---
 
-(declare-sort $Ref 0)
-(declare-const $Ref.null $Ref)
+(define-fun fp.neq32 ((x (_ FloatingPoint 8 24)) (y (_ FloatingPoint 8 24))) Bool (not (fp.eq x y)))
+(define-fun fp.neq64 ((x (_ FloatingPoint 11 53)) (y (_ FloatingPoint 11 53))) Bool (not (fp.eq x y)))
 
-; --- Permissions ---
+; --- Legacy permission sort ---
 
-(declare-sort $FPM 0)
-(declare-sort $PPM 0)
 (define-sort $Perm () Real)
 
-(define-const $Perm.Write $Perm 1.0)
-(define-const $Perm.No $Perm 0.0)
-
-(define-fun $Perm.isValidVar ((p $Perm)) Bool
-	(<= $Perm.No p))
-
-(define-fun $Perm.isReadVar ((p $Perm)) Bool
-    (and ($Perm.isValidVar p)
-         (not (= p $Perm.No))))
-
-; min function for permissions
-(define-fun $Perm.min ((p1 $Perm) (p2 $Perm)) Real
-    (ite (<= p1 p2) p1 p2))
-
-; --- Sort wrappers ---
-
-; Sort wrappers are no longer part of the static preamble. Instead, they are
-; emitted as part of the program-specific preamble.
-
-; --- Math ---
-
-;function Math#min(a: int, b: int): int;
-(define-fun $Math.min ((a Int) (b Int)) Int
-    (ite (<= a b) a b))
-
-;function Math#clip(a: int): int;
-(define-fun $Math.clip ((a Int)) Int
-    (ite (< a 0) 0 a))
-
 ; ===== End static preamble =====