diff --git a/native-verifier/src/fol.rs b/native-verifier/src/fol.rs index 302858d544d..95e8b7cf83d 100644 --- 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 index 50ff82bacb1..fb1e0f48dcf 100644 --- 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::>() + .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::>() + .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::>() + .join(" ") + ) } Expression::FieldAccessPredicate(_) => unimplemented!(), Expression::Unfolding(_) => unimplemented!(), @@ -481,7 +522,18 @@ 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 { @@ -489,7 +541,7 @@ impl SMTTranslatable for Expression { 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 index 6e56e887b01..933a6330bbe 100644 --- 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 new file mode 100644 index 00000000000..09677dda590 --- /dev/null +++ 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 index 4892355cd95..7631e4ce845 100644 --- 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 index f88ff2b7ac6..dd6bc554443 100644 --- 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 index 98af319413c..b09a20813d1 100644 --- 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 index aa2b046f5dd..31b133f11e5 100644 --- 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 index 41b3dd1e814..f78861a0fcc 100644 --- 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 index 90cefcd028c..88837d28ede 100644 --- 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 index 302071ab05c..ad2e2cb49f5 100644 --- 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())},