Add initial F32 and F64 support

viperproject · Oct 22, 2023 · c68d489 · c68d489
1 parent e3cb301
commit c68d489
Show file tree

Hide file tree

Showing 11 changed files with 203 additions and 15 deletions.
diff --git a/native-verifier/src/fol.rs b/native-verifier/src/fol.rs
@@ -132,8 +132,7 @@ fn vir_statement_to_fol_statements(
         Statement::Comment(comment) => vec![FolStatement::Comment(comment.comment.clone())],
         Statement::LogEvent(_) => vec![], // TODO: Embed in SMT-LIB code
         _ => {
-            log::warn!("Statement {:?} not yet supported", statement);
-            vec![]
+            unimplemented!("Statement {:?} not yet supported", statement);
         }
     }
 }

diff --git a/native-verifier/src/smt_lib.rs b/native-verifier/src/smt_lib.rs
@@ -343,7 +343,7 @@ impl SMTTranslatable for DomainAxiomDecl {
             smt.add_assert(format!("; {}", comment));
         }
 
-        smt.add_assert(self.body.to_smt());
+        smt.add_code(format!("(assert {}) ; {}", self.body.to_smt(), self.name));
     }
 }
 
@@ -430,13 +430,54 @@ impl SMTTranslatable for Expression {
             Expression::Constant(constant) => match &constant.value {
                 ConstantValue::Bool(bool) => bool.to_string(),
                 ConstantValue::Int(i64) => i64.to_string(),
+                ConstantValue::Float32(u32) => {
+                    let bits = u32.to_le_bytes();
+                    let bits = bits
+                        .iter()
+                        .rev()
+                        .map(|b| format!("{:08b}", b))
+                        .collect::<Vec<_>>()
+                        .join("");
+                    format!(
+                        "(fp #b{} #b{} #b{})",
+                        &bits.chars().next().unwrap(),
+                        &bits[1..=8],
+                        &bits[9..=31]
+                    )
+                }
+                ConstantValue::Float64(u64) => {
+                    let bits = u64.to_le_bytes();
+                    let bits = bits
+                        .iter()
+                        .rev()
+                        .map(|b| format!("{:08b}", b))
+                        .collect::<Vec<_>>()
+                        .join("");
+                    format!(
+                        "(fp #b{} #b{} #b{})",
+                        &bits.chars().next().unwrap(),
+                        &bits[1..=11],
+                        &bits[12..=63]
+                    )
+                }
                 ConstantValue::BigInt(s) => s.clone(),
             },
-            Expression::MagicWand(_) => unimplemented!("Magic wands are not supported"),
+            Expression::MagicWand(wand) => {
+                warn!("MagicWand not supported: {}", wand);
+                format!("(=> {} {})", wand.left.to_smt(), wand.right.to_smt())
+            }
             Expression::PredicateAccessPredicate(_access) => {
-                // TODO: access predicates for predicates
-                warn!("PredicateAccessPredicate not supported");
-                "".to_string()
+                warn!("PredicateAccessPredicate not supported: {}", _access);
+                format!(
+                    "({} {})",
+                    _access.name,
+                    _access
+                        .arguments
+                        .iter()
+                        .map(|x| x.to_smt())
+                        .collect::<Vec<_>>()
+                        .join(" ")
+                )
             }
             Expression::FieldAccessPredicate(_) => unimplemented!(),
             Expression::Unfolding(_) => unimplemented!(),
@@ -481,15 +522,26 @@ impl SMTTranslatable for Expression {
                     );
                     quant.push_str(") ");
 
-                    if quantifier.triggers.is_empty() {
+                    let triggers: Vec<_> = quantifier
+                        .triggers
+                        .iter()
+                        .filter(|t| {
+                            !t.terms
+                                .iter()
+                                .any(|t| matches!(t, Expression::PredicateAccessPredicate(_)))
+                            // TODO: Support triggers with predicate access predicates?
+                        })
+                        .collect();
+
+                    if triggers.is_empty() {
                         quant.push_str(&quantifier.body.to_smt());
                         quant.push_str(")");
                     } else {
                         // triggers are :pattern
                         quant.push_str("(!");
                         quant.push_str(&quantifier.body.to_smt());
 
-                        for trigger in &quantifier.triggers {
+                        for trigger in &triggers {
                             quant.push_str(" :pattern (");
 
                             quant.push_str(

diff --git a/prusti-common/src/vir/low_to_viper/ast.rs b/prusti-common/src/vir/low_to_viper/ast.rs
@@ -287,6 +287,8 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for expression::Constant {
                 expression::ConstantValue::Int(value) => {
                     ast.int_lit_with_pos(*value, self.position.to_viper(context, ast))
                 }
+                expression::ConstantValue::Float32(_) => unimplemented!("Float32 to Viper"),
+                expression::ConstantValue::Float64(_) => unimplemented!("Float64 to Viper"),
                 expression::ConstantValue::BigInt(value) => {
                     ast.int_lit_from_ref_with_pos(value, self.position.to_viper(context, ast))
                 }
@@ -308,7 +310,9 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for expression::Constant {
             Type::Map(_) => unimplemented!(),
             Type::Ref => unimplemented!(),
             Type::Perm => match &self.value {
-                expression::ConstantValue::Bool(_) => {
+                expression::ConstantValue::Float32(_)
+                | expression::ConstantValue::Float64(_)
+                | expression::ConstantValue::Bool(_) => {
                     unreachable!()
                 }
                 expression::ConstantValue::Int(value) => match value {

diff --git a/prusti-tests/tests/verify/pass/native/ackermann.rs b/prusti-tests/tests/verify/pass/native/ackermann.rs
@@ -0,0 +1,52 @@
+// compile-flags: -Pviper_backend=Lithium
+use prusti_contracts::*;
+
+#[pure]
+#[terminates(trusted)]
+#[requires(0 <= m && 0 <= n)]
+#[ensures(result >= 0)]
+fn ack_pure(m: i64, n: i64) -> i64 {
+    if m == 0 {
+        n + 1
+    } else if n == 0 {
+        ack_pure(m - 1, 1)
+    } else {
+        ack_pure(m - 1, ack_pure(m, n - 1))
+    }
+}
+
+#[requires(0 <= m && 0 <= n)]
+#[ensures(result == ack_pure(m, n))]
+#[ensures(result >= 0)]
+fn ack1(m: i64, n: i64) -> i64 {
+    if m == 0 {
+        n + 1
+    } else if n == 0 {
+        ack1(m - 1, 1)
+    } else {
+        ack1(m - 1, ack1(m, n - 1))
+    }
+}
+
+#[requires(0 <= m && 0 <= n)]
+#[ensures(result == ack_pure(m, n))]
+#[ensures(result >= 0)]
+fn ack2(m: i64, n: i64) -> i64 {
+    match (m, n) {
+        (0, n) => n + 1,
+        (m, 0) => ack2(m - 1, 1),
+        (m, n) => ack2(m - 1, ack2(m, n - 1)),
+    }
+}
+
+#[trusted]
+fn print_i64(a: i64) {
+    println!("{}", a); // 125
+}
+
+fn main() {
+    let a1 = ack1(3, 4);
+    let a2 = ack2(3, 4);
+    assert!(a1 == a2);
+    print_i64(a1);
+}
diff --git a/prusti-viper/src/encoder/builtin_encoder.rs b/prusti-viper/src/encoder/builtin_encoder.rs
@@ -277,12 +277,20 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinEncoder<'p, 'v, 'tcx> {
         let mut functions = vec![];
         let mut axioms = vec![];
 
-        for t in &[vir::Type::Bool, vir::Type::Int] {
+        for t in &[
+            vir::Type::Bool,
+            vir::Type::Int,
+            vir::Type::Float(vir::Float::F32),
+            vir::Type::Float(vir::Float::F64),
+        ] {
             //let f = snapshot::valid_func_for_type(t);
             let f = {
                 let domain_name: String = match t {
                     // vir::Type::Domain(name) => name.clone(),
-                    vir::Type::Bool | vir::Type::Int => domain_name.to_string(),
+                    vir::Type::Bool
+                    | vir::Type::Int
+                    | vir::Type::Float(vir::Float::F32)
+                    | vir::Type::Float(vir::Float::F64) => domain_name.to_string(),
                     // vir::Type::TypedRef(_) => unreachable!(),
                     // vir::Type::TypeVar(_) => unreachable!(),
                     // vir::Type::Snapshot(_) => unreachable!(),
@@ -293,6 +301,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinEncoder<'p, 'v, 'tcx> {
                     // vir::Type::Domain(vir::DomainType{label, ..}) => vir::Type::domain(label.clone()),
                     vir::Type::Bool => vir::Type::Bool,
                     vir::Type::Int => vir::Type::Int,
+                    vir::Type::Float(vir::Float::F32) => vir::Type::Float(vir::Float::F32),
+                    vir::Type::Float(vir::Float::F64) => vir::Type::Float(vir::Float::F64),
                     // vir::Type::TypedRef(_) => unreachable!(),
                     // vir::Type::TypeVar(_) => unreachable!(),
                     // vir::Type::Snapshot(_) => unreachable!(),

diff --git a/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/common/mod.rs b/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/common/mod.rs
@@ -236,6 +236,12 @@ pub(super) trait IntoSnapshotLowerer<'p, 'v: 'p, 'tcx: 'v> {
             vir_mid::Type::MFloat64 => unimplemented!(),
             vir_mid::Type::Bool => vir_low::Type::Bool,
             vir_mid::Type::Int(_) => vir_low::Type::Int,
+            vir_mid::Type::Float(vir_mid::ty::Float::F32) => {
+                vir_low::Type::Float(vir_low::ty::Float::F32)
+            }
+            vir_mid::Type::Float(vir_mid::ty::Float::F64) => {
+                vir_low::Type::Float(vir_low::ty::Float::F64)
+            }
             vir_mid::Type::MPerm => vir_low::Type::Perm,
             _ => unimplemented!("constant: {:?}", constant),
         };
@@ -274,9 +280,12 @@ pub(super) trait IntoSnapshotLowerer<'p, 'v: 'p, 'tcx: 'v> {
             vir_mid::expression::ConstantValue::BigInt(value) => {
                 vir_low::expression::ConstantValue::BigInt(value.clone())
             }
-            vir_mid::expression::ConstantValue::Float(_value) => {
-                unimplemented!();
-            }
+            vir_mid::expression::ConstantValue::Float(vir_crate::polymorphic::FloatConst::F32(
+                value,
+            )) => vir_low::expression::ConstantValue::Float32(*value),
+            vir_mid::expression::ConstantValue::Float(vir_crate::polymorphic::FloatConst::F64(
+                value,
+            )) => vir_low::expression::ConstantValue::Float64(*value),
             vir_mid::expression::ConstantValue::FnPtr => {
                 unimplemented!();
             }

diff --git a/prusti-viper/src/encoder/middle/core_proof/snapshots/values/interface.rs b/prusti-viper/src/encoder/middle/core_proof/snapshots/values/interface.rs
@@ -105,6 +105,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> SnapshotValuesInterface for Lowerer<'p, 'v, 'tcx> {
         let return_type = match &ty {
             vir_mid::Type::Bool => vir_low::Type::Bool,
             vir_mid::Type::Int(_) => vir_low::Type::Int,
+            vir_mid::Type::Float(vir_mid::ty::Float::F32) => {
+                vir_low::Type::Float(vir_low::ty::Float::F32)
+            }
+            vir_mid::Type::Float(vir_mid::ty::Float::F64) => {
+                vir_low::Type::Float(vir_low::ty::Float::F64)
+            }
             vir_mid::Type::Pointer(_) => self.address_type()?,
             x => unimplemented!("{:?}", x),
         };
@@ -205,6 +211,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> SnapshotValuesInterface for Lowerer<'p, 'v, 'tcx> {
         let low_type = match &ty {
             vir_mid::Type::Bool => vir_low::Type::Bool,
             vir_mid::Type::Int(_) => vir_low::Type::Int,
+            vir_mid::Type::Float(vir_mid::ty::Float::F32) => {
+                vir_low::Type::Float(vir_low::ty::Float::F32)
+            }
+            vir_mid::Type::Float(vir_mid::ty::Float::F64) => {
+                vir_low::Type::Float(vir_low::ty::Float::F64)
+            }
             vir_mid::Type::Pointer(_) => self.address_type()?,
             vir_mid::Type::Reference(_) => self.address_type()?,
             x => unimplemented!("{:?}", x),

diff --git a/prusti-viper/src/encoder/middle/core_proof/types/interface.rs b/prusti-viper/src/encoder/middle/core_proof/types/interface.rs
@@ -98,6 +98,30 @@ impl<'p, 'v: 'p, 'tcx: 'v> Private for Lowerer<'p, 'v, 'tcx> {
                 let validity = conjuncts.into_iter().conjoin();
                 self.encode_validity_axioms_primitive(&domain_name, vir_low::Type::Int, validity)?;
             }
+            vir_mid::TypeDecl::Float(decl) => {
+                self.ensure_type_definition(&vir_mid::Type::Bool)?;
+                self.register_constant_constructor(
+                    &domain_name,
+                    vir_low::Type::Float(vir_low::ty::Float::F32), // TODO: What about f64?
+                )?;
+                var_decls! { value: Float64 };
+
+                let mut conjuncts = Vec::new();
+                if let Some(lower_bound) = &decl.lower_bound {
+                    conjuncts
+                        .push(expr! { [lower_bound.clone().to_pure_snapshot(self)? ] <= value });
+                }
+                if let Some(upper_bound) = &decl.upper_bound {
+                    conjuncts
+                        .push(expr! { value <= [upper_bound.clone().to_pure_snapshot(self)? ] });
+                }
+                let validity = conjuncts.into_iter().conjoin();
+                self.encode_validity_axioms_primitive(
+                    &domain_name,
+                    vir_low::Type::Float(vir_low::ty::Float::F32),
+                    validity,
+                )?;
+            }
             vir_mid::TypeDecl::Trusted(_) => {
                 // FIXME: ensure type definition for trusted
             }
@@ -422,6 +446,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> TypesInterface for Lowerer<'p, 'v, 'tcx> {
             let constant_type = match argument_type {
                 vir_mid::Type::Bool => Some(ty! { Bool }),
                 vir_mid::Type::Int(_) => Some(ty! {Int}),
+                vir_mid::Type::Float(vir_mid::ty::Float::F32) => Some(ty! {Float32}),
+                vir_mid::Type::Float(vir_mid::ty::Float::F64) => Some(ty! {Float64}),
                 vir_mid::Type::Pointer(_) => Some(ty!(Address)),
                 _ => None,
             };

diff --git a/prusti-viper/src/encoder/mir/constants/interface.rs b/prusti-viper/src/encoder/mir/constants/interface.rs
@@ -55,6 +55,26 @@ impl<'v, 'tcx: 'v> ConstantsEncoderInterface<'tcx> for super::super::super::Enco
                     .unwrap();
                 number.into()
             }
+            ty::TyKind::Float(ty::FloatTy::F32) => {
+                let ty = self.encode_type_high(mir_type)?;
+                let bits = scalar_value()?.to_u32().unwrap();
+                vir_high::Expression::constant_no_pos(
+                    vir_high::expression::ConstantValue::Float(
+                        vir_high::expression::FloatConst::F32(bits),
+                    ),
+                    ty,
+                )
+            }
+            ty::TyKind::Float(ty::FloatTy::F64) => {
+                let ty = self.encode_type_high(mir_type)?;
+                let bits = scalar_value()?.to_u64().unwrap();
+                vir_high::Expression::constant_no_pos(
+                    vir_high::expression::ConstantValue::Float(
+                        vir_high::expression::FloatConst::F64(bits),
+                    ),
+                    ty,
+                )
+            }
             ty::TyKind::FnDef(..) => {
                 let ty = self.encode_type_high(mir_type)?;
                 vir_high::Expression::constant_no_pos(

diff --git a/vir/defs/low/ast/expression.rs b/vir/defs/low/ast/expression.rs
@@ -65,6 +65,8 @@ pub struct Constant {
 pub enum ConstantValue {
     Bool(bool),
     Int(i64),
+    Float32(f32),
+    Float64(f64),
     BigInt(String),
 }
 

diff --git a/vir/src/low/macros.rs b/vir/src/low/macros.rs
@@ -1,5 +1,7 @@
 pub macro ty {
     (Int) => {$crate::low::ast::ty::Type::Int},
+    (Float32) => {$crate::low::ast::ty::Type::Float(crate::low::ast::ty::Float::F32)},
+    (Float64) => {$crate::low::ast::ty::Type::Float(crate::low::ast::ty::Float::F64)},
     (Bool) => {$crate::low::ast::ty::Type::Bool},
     (Perm) => {$crate::low::ast::ty::Type::Perm},
     (Place) => {$crate::low::ast::ty::Type::domain("Place".to_string())},