Quantifiers to snapshots, fix unsized type bound checking bug

native-verifier/src/fol.rs

@@ -33,10 +33,43 @@ fn vir_statement_to_fol_statements(
             vec![FolStatement::Assume(eq)]
         }
         Statement::Conditional(cond) => {
+            // handle trivial cases where the guard is constant true or false, emit the branches instead
+            if let Expression::Constant(Constant {
+                value: ConstantValue::Bool(true),
+                ..
+            }) = cond.guard
+            {
+                return cond
+                    .then_branch
+                    .iter()
+                    .flat_map(|s| vir_statement_to_fol_statements(s, known_methods))
+                    .collect();
+            } else if let Expression::Constant(Constant {
+                value: ConstantValue::Bool(false),
+                ..
+            }) = cond.guard
+            {
+                return cond
+                    .else_branch
+                    .iter()
+                    .flat_map(|s| vir_statement_to_fol_statements(s, known_methods))
+                    .collect();
+            }
+
             if !(cond.then_branch.is_empty() && cond.else_branch.is_empty()) {
-                log::warn!(
-                    "Conditional statement with non-empty branches, guard: {:?}",
-                    cond.guard
+                unimplemented!(
+                    "Non-trivial conditional statements not supported!!\nGuard: {}\n\nThen-branch:\n{}\n\nElse-branch:\n{}",
+                    cond.guard,
+                    cond.then_branch
+                        .iter()
+                        .map(|s| format!("{}", s))
+                        .collect::<Vec<_>>()
+                        .join(";\n"),
+                    cond.else_branch
+                        .iter()
+                        .map(|s| format!("{}", s))
+                        .collect::<Vec<_>>()
+                        .join(";\n")
                 );
             }
             vec![]

native-verifier/src/smt_lib.rs

@@ -18,6 +18,7 @@ use vir::{
 lazy_static! {
     static ref ONE_PARAM_RE: Regex = Regex::new(r"(Set|Seq|MultiSet)<([^>]+)>").unwrap();
     static ref TWO_PARAM_RE: Regex = Regex::new(r"Map<([^>]+)\s*,\s*([^>]+)>").unwrap();
+    static ref MARKER_RE: Regex = Regex::new(r"label.*\$marker\b\s").unwrap();
 }
 
 const NO_Z3_PREAMBLE: &str = include_str!("theories/Preamble.smt2");
@@ -67,7 +68,6 @@ impl SMTLib {
                 // check if just asserting true
                 // TODO: Optimization module
                 if let Expression::Constant(Constant {
-                    ty: Type::Bool,
                     value: ConstantValue::Bool(true),
                     ..
                 }) = expression
@@ -118,6 +118,7 @@ impl SMTLib {
 
         // assume precond if any
         if let Some(precond) = precond {
+            // TODO: Location of the call site
             self.add_code("; Branch precond:".to_string());
             self.add_code(format!("(assert {})", precond.to_smt()));
         }
@@ -140,7 +141,6 @@ impl SMTLib {
                 let (last_expr, last_label) = mapping.iter().last().unwrap();
 
                 if let Expression::Constant(Constant {
-                    ty: Type::Bool,
                     value: ConstantValue::Bool(true),
                     ..
                 }) = last_expr
@@ -263,7 +263,7 @@ impl ToString for SMTLib {
 
         result
             .lines()
-            .filter(|&line| !line.contains("$marker")) // TODO: SSO form for marker variables?
+            .filter(|&line| !MARKER_RE.is_match(line)) // TODO: SSO form for marker variables?
             .filter(|&line| line != "(assert true)") // TODO: Optimization module
             .collect::<Vec<_>>()
             .join("\n")
@@ -471,8 +471,16 @@ impl SMTTranslatable for Expression {
                 ConstantValue::BigInt(s) => s.clone(),
             },
             Expression::MagicWand(wand) => {
-                warn!("MagicWand not supported: {}", wand);
-                format!("(=> {} {})", wand.left.to_smt(), wand.right.to_smt())
+                // if left is just constant true, we can ignore it
+                if let Expression::Constant(Constant {
+                    value: ConstantValue::Bool(true),
+                    ..
+                }) = *wand.left
+                {
+                    format!("(=> {} {})", wand.left.to_smt(), wand.right.to_smt())
+                } else {
+                    unimplemented!("Non-trivial MagicWand not supported: {}", wand);
+                }
             }
             Expression::PredicateAccessPredicate(_access) => {
                 warn!("PredicateAccessPredicate not supported: {}", _access);

prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/common/mod.rs

@@ -75,7 +75,9 @@ pub(super) trait IntoSnapshotLowerer<'p, 'v: 'p, 'tcx: 'v> {
             vir_mid::Expression::Conditional(expression) => {
                 self.conditional_to_snapshot(lowerer, expression, expect_math_bool)
             }
-            // vir_mid::Expression::Quantifier(expression) => self.quantifier_to_snapshot(lowerer, expression, expect_math_bool),
+            vir_mid::Expression::Quantifier(expression) => {
+                self.quantifier_to_snapshot(lowerer, expression, expect_math_bool)
+            }
             // vir_mid::Expression::LetExpr(expression) => self.letexpr_to_snapshot(lowerer, expression, expect_math_bool),
             vir_mid::Expression::FuncApp(expression) => {
                 self.func_app_to_snapshot(lowerer, expression, expect_math_bool)
@@ -103,6 +105,58 @@ pub(super) trait IntoSnapshotLowerer<'p, 'v: 'p, 'tcx: 'v> {
         }
     }
 
+    fn quantifier_to_snapshot(
+        &mut self,
+        lowerer: &mut Lowerer<'p, 'v, 'tcx>,
+        quantifier: &vir_mid::Quantifier,
+        expect_math_bool: bool,
+    ) -> SpannedEncodingResult<vir_low::Expression> {
+        let vir_mid::Quantifier {
+            kind,
+            variables,
+            triggers,
+            body,
+            position,
+        } = quantifier;
+
+        let vars = variables
+            .iter()
+            .map(|variable| self.variable_to_snapshot(lowerer, variable))
+            .collect::<SpannedEncodingResult<Vec<_>>>()?;
+
+        let trigs = triggers
+            .iter()
+            .map(|trigger| {
+                let trig = self
+                    .expression_vec_to_snapshot(lowerer, &trigger.terms, expect_math_bool)
+                    .unwrap();
+                vir_low::Trigger { terms: trig }
+            })
+            .collect();
+
+        let body = self.expression_to_snapshot(lowerer, body, expect_math_bool)?;
+
+        let kind = match kind {
+            vir_mid::expression::QuantifierKind::ForAll => {
+                vir_low::expression::QuantifierKind::ForAll
+            }
+            vir_mid::expression::QuantifierKind::Exists => {
+                vir_low::expression::QuantifierKind::Exists
+            }
+        };
+
+        // no call to ensure_bool_expression since quantifiers are always math bool and forall is built-in to SMT solvers
+        Ok(vir_low::Expression::Quantifier(
+            vir_low::expression::Quantifier {
+                kind,
+                variables: vars,
+                triggers: trigs,
+                body: Box::new(body),
+                position: *position,
+            },
+        ))
+    }
+
     fn variable_to_snapshot(
         &mut self,
         lowerer: &mut Lowerer<'p, 'v, 'tcx>,

prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs

@@ -147,9 +147,16 @@ pub(super) fn encode_quantifier_high<'tcx>(
         if config::check_overflows() {
             bounds.extend(encoder.encode_type_bounds_high(&encoded_qvar.clone().into(), arg_ty));
         } else if config::encode_unsigned_num_constraint() {
-            if let ty::TyKind::Uint(_) = arg_ty.kind() {
-                let expr =
-                    vir_high::Expression::less_equals(0u32.into(), encoded_qvar.clone().into());
+            if let ty::TyKind::Uint(utype) = arg_ty.kind() {
+                let zero = match utype {
+                    ty::UintTy::U8 => 0u8.into(),
+                    ty::UintTy::U16 => 0u16.into(),
+                    ty::UintTy::U32 => 0u32.into(),
+                    ty::UintTy::U64 => 0u64.into(),
+                    ty::UintTy::U128 => 0u128.into(),
+                    ty::UintTy::Usize => 0usize.into(),
+                };
+                let expr = vir_high::Expression::less_equals(zero, encoded_qvar.clone().into());
                 bounds.push(expr);
             }
         }