Add preamble for CVC5, split fp.neq into 32 and 64-bit variants

native-verifier/src/smt_lib.rs

@@ -20,24 +20,27 @@ lazy_static! {
     static ref TWO_PARAM_RE: Regex = Regex::new(r"Map<([^>]+)\s*,\s*([^>]+)>").unwrap();
 }
 
-const SMT_PREAMBLE: &str = include_str!("theories/Preamble.smt2");
+const NO_Z3_PREAMBLE: &str = include_str!("theories/Preamble.smt2");
+const Z3_PREAMBLE: &str = include_str!("theories/PreambleZ3.smt2");
 
 pub struct SMTLib {
     sort_decls: Vec<String>,
     func_decls: Vec<String>,
     code: Vec<String>,
     methods: HashMap<String, MethodDecl>,
     blocks: HashMap<String, BasicBlock>,
+    using_z3: bool,
 }
 
 impl SMTLib {
-    pub fn new() -> Self {
+    pub fn new(using_z3: bool) -> Self {
         Self {
             sort_decls: Vec::new(),
             func_decls: Vec::new(),
             code: Vec::new(),
             methods: HashMap::new(),
             blocks: Default::default(),
+            using_z3,
         }
     }
     fn add_sort_decl(&mut self, sort_decl: String) {
@@ -192,7 +195,11 @@ impl SMTLib {
 impl ToString for SMTLib {
     fn to_string(&self) -> String {
         let mut result = String::new();
-        result.push_str(SMT_PREAMBLE);
+        result.push_str(if self.using_z3 {
+            Z3_PREAMBLE
+        } else {
+            NO_Z3_PREAMBLE
+        });
         result.push_str("\n\n");
         result.push_str(&self.sort_decls.join("\n"));
         result.push_str("\n\n");
@@ -492,8 +499,8 @@ impl SMTTranslatable for Expression {
                 format!("({} {})", op_smt, unary_op.argument.to_smt())
             }
             Expression::BinaryOp(binary_op) => {
-                let op_smt = if binary_op.left.get_type().is_float() {
-                    FloatBinaryOpKind(binary_op.op_kind).to_smt()
+                let op_smt = if let Type::Float(fsize) = binary_op.left.get_type() {
+                    FloatBinaryOpKind(binary_op.op_kind, *fsize).to_smt()
                 } else {
                     IntBinaryOpKind(binary_op.op_kind).to_smt()
                 };
@@ -585,7 +592,7 @@ impl SMTTranslatable for Expression {
 }
 
 struct IntBinaryOpKind(BinaryOpKind);
-struct FloatBinaryOpKind(BinaryOpKind);
+struct FloatBinaryOpKind(BinaryOpKind, Float);
 
 impl SMTTranslatable for IntBinaryOpKind {
     fn to_smt(&self) -> String {
@@ -611,22 +618,21 @@ impl SMTTranslatable for IntBinaryOpKind {
 
 impl SMTTranslatable for FloatBinaryOpKind {
     fn to_smt(&self) -> String {
-        match self.0 {
+        match (self.0, self.1) {
             // BinaryOpKind::EqCmp => "fp.eq", // TODO: = in axioms, fp.eq in arithmetic?
-            BinaryOpKind::EqCmp => "=",
-            BinaryOpKind::NeCmp => "fp.neq", // Not in SMT-LIB 2.6 standard, part of static preamble
-            BinaryOpKind::GtCmp => "fp.gt",
-            BinaryOpKind::GeCmp => "fp.geq",
-            BinaryOpKind::LtCmp => "fp.lt",
-            BinaryOpKind::LeCmp => "fp.leq",
-            BinaryOpKind::Add => "fp.add roundNearestTiesToAway",
-            BinaryOpKind::Sub => "fp.sub roundNearestTiesToAway",
-            BinaryOpKind::Mul => "fp.mul roundNearestTiesToAway",
-            BinaryOpKind::Div => "fp.div roundNearestTiesToAway",
-            BinaryOpKind::Mod => "fp.rem",
-            BinaryOpKind::And => unreachable!("FP and"),
-            BinaryOpKind::Or => unreachable!("FP or"),
-            BinaryOpKind::Implies => unreachable!("FP implication"),
+            (BinaryOpKind::EqCmp, _) => "=",
+            (BinaryOpKind::NeCmp, Float::F32) => "fp.neq32", // Not in SMT-LIB 2.6 standard, part of static preamble
+            (BinaryOpKind::NeCmp, Float::F64) => "fp.neq64", // Not in SMT-LIB 2.6 standard, part of static preamble
+            (BinaryOpKind::GtCmp, _) => "fp.gt",
+            (BinaryOpKind::GeCmp, _) => "fp.geq",
+            (BinaryOpKind::LtCmp, _) => "fp.lt",
+            (BinaryOpKind::LeCmp, _) => "fp.leq",
+            (BinaryOpKind::Add, _) => "fp.add roundNearestTiesToAway",
+            (BinaryOpKind::Sub, _) => "fp.sub roundNearestTiesToAway",
+            (BinaryOpKind::Mul, _) => "fp.mul roundNearestTiesToAway",
+            (BinaryOpKind::Div, _) => "fp.div roundNearestTiesToAway",
+            (BinaryOpKind::Mod, _) => "fp.rem",
+            (other, _) => unreachable!("FP {}", other),
         }
         .to_string()
     }

native-verifier/src/theories/Preamble.smt2

@@ -1,42 +1,11 @@
 ; ===== Static preamble =====
 
-(set-option :global-decls true) ; Boogie: default
-(set-option :auto_config false) ; Usually a good idea
-(set-option :smt.restart_strategy 0)
-(set-option :smt.restart_factor |1.5|)
-(set-option :smt.case_split 3)
-(set-option :smt.delay_units true)
-(set-option :smt.delay_units_threshold 16)
-(set-option :nnf.sk_hack true)
-(set-option :type_check true)
-(set-option :smt.bv.reflect true)
-(set-option :smt.mbqi false)
-(set-option :smt.qi.cost "(+ weight generation)")
-(set-option :smt.qi.eager_threshold 1000)
-(set-option :smt.qi.max_multi_patterns 1000)
-(set-option :smt.phase_selection 0) ; default: 3, Boogie: 0
-(set-option :sat.phase caching)
-(set-option :sat.random_seed 0)
-(set-option :nlsat.randomize true)
-(set-option :nlsat.seed 0)
-(set-option :nlsat.shuffle_vars false)
-(set-option :fp.spacer.order_children 0) ; Not available with Z3 4.5
-(set-option :fp.spacer.random_seed 0) ; Not available with Z3 4.5
-(set-option :smt.arith.random_initial_value true) ; Boogie: true
-(set-option :smt.random_seed 0)
-(set-option :sls.random_offset true)
-(set-option :sls.random_seed 0)
-(set-option :sls.restart_init false)
-(set-option :sls.walksat_ucb true)
-(set-option :model.v2 true)
-(set-option :model.partial false)
-
-(set-option :timeout 1000)
+(set-logic ALL)
 
 ; --- Floating-point arithmetic ---
 
-(define-fun fp.neq ((x (_ FloatingPoint 8 24)) (y (_ FloatingPoint 8 24))) Bool (not (fp.eq x y)))
-(define-fun fp.neq ((x (_ FloatingPoint 11 53)) (y (_ FloatingPoint 11 53))) Bool (not (fp.eq x y)))
+(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 ---
 

native-verifier/src/theories/PreambleZ3.smt2

@@ -0,0 +1,87 @@
+; ===== Static preamble =====
+
+(set-option :global-decls true) ; Boogie: default
+(set-option :auto_config false) ; Usually a good idea
+(set-option :smt.restart_strategy 0)
+(set-option :smt.restart_factor |1.5|)
+(set-option :smt.case_split 3)
+(set-option :smt.delay_units true)
+(set-option :smt.delay_units_threshold 16)
+(set-option :nnf.sk_hack true)
+(set-option :type_check true)
+(set-option :smt.bv.reflect true)
+(set-option :smt.mbqi false)
+(set-option :smt.qi.cost "(+ weight generation)")
+(set-option :smt.qi.eager_threshold 1000)
+(set-option :smt.qi.max_multi_patterns 1000)
+(set-option :smt.phase_selection 0) ; default: 3, Boogie: 0
+(set-option :sat.phase caching)
+(set-option :sat.random_seed 0)
+(set-option :nlsat.randomize true)
+(set-option :nlsat.seed 0)
+(set-option :nlsat.shuffle_vars false)
+(set-option :fp.spacer.order_children 0) ; Not available with Z3 4.5
+(set-option :fp.spacer.random_seed 0) ; Not available with Z3 4.5
+(set-option :smt.arith.random_initial_value true) ; Boogie: true
+(set-option :smt.random_seed 0)
+(set-option :sls.random_offset true)
+(set-option :sls.random_seed 0)
+(set-option :sls.restart_init false)
+(set-option :sls.walksat_ucb true)
+(set-option :model.v2 true)
+(set-option :model.partial false)
+
+(set-option :timeout 1000)
+
+; --- Floating-point arithmetic ---
+
+(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)))))
+
+; --- References ---
+
+(declare-sort $Ref 0)
+(declare-const $Ref.null $Ref)
+
+; --- Permissions ---
+
+(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 =====

native-verifier/src/verifier.rs

@@ -7,31 +7,42 @@
 use crate::smt_lib::*;
 use backend_common::{VerificationError, VerificationResult};
 use core::panic;
+use lazy_static::lazy_static;
 use log::{self, debug};
 use prusti_common::vir::program::Program;
 use prusti_utils::{report::log::report_with_writer, run_timed};
+use regex::Regex;
 use std::{
     error::Error,
     io::Write,
     process::{Command, Stdio},
 };
 
+// lazy regex for parsing z3 output
+lazy_static! {
+    static ref POSITION_REGEX: Regex = Regex::new(r#"^"?position: (\d+)"?"#).unwrap();
+}
+
 pub struct Verifier {
-    z3_exe: String,
+    smt_solver_exe: String,
 }
 
 impl Verifier {
     pub fn new(z3_exe: String) -> Self {
-        Self { z3_exe }
+        Self {
+            smt_solver_exe: z3_exe,
+        }
     }
 
     pub fn verify(&mut self, program: &Program) -> VerificationResult {
         let Program::Low(program) = program else {
             panic!("Lithium backend only supports low programs");
         };
 
+        let is_z3 = self.smt_solver_exe.ends_with("z3");
+
         run_timed!("Translation to SMT-LIB", debug,
-            let mut smt = SMTLib::new();
+            let mut smt = SMTLib::new(is_z3);
             program.build_smt(&mut smt);
             let smt_program = smt.to_string();
 
@@ -44,11 +55,17 @@ impl Verifier {
             );
         );
 
-        run_timed!("SMT verification", debug,
+        run_timed!(format!("SMT verification with {}", if is_z3 {"Z3"} else {"CVC5"}), debug,
             let result: Result<String, Box<dyn Error>> = try {
-                let mut child = Command::new(self.z3_exe.clone())
-                    .args(["-smt2", "-in"])
-                    .stdin(Stdio::piped())
+                let mut command = Command::new(self.smt_solver_exe.clone());
+
+                if is_z3 {
+                    command.args(&["-smt2", "-in"]);
+                } else {
+                    command.args(&["--incremental"]);
+                }
+
+                let mut child = command.stdin(Stdio::piped())
                     .stderr(Stdio::piped())
                     .stdout(Stdio::piped())
                     .spawn()?;
@@ -87,9 +104,8 @@ impl Verifier {
 
         let mut last_pos: i32 = 0;
         for line in result.unwrap().lines() {
-            if line.starts_with("position: ") {
-                let position_id = line.split("position: ").nth(1).unwrap();
-                last_pos = position_id.parse().unwrap();
+            if let Some(caps) = POSITION_REGEX.captures(line) {
+                last_pos = caps[1].parse().unwrap();
             } else if line == "sat" || line == "unknown" {
                 errors.push(VerificationError::new(
                     "assert.failed:assertion.false".to_string(),

vir/defs/low/ast/ty.rs

@@ -17,6 +17,7 @@ pub enum Type {
     Domain(Domain),
 }
 
+#[derive(Copy)]
 pub enum Float {
     F32,
     F64,