Handle another case where partially evaluated sequences need to

be handed back to the SST pipeline.
verus-lang · Jul 27, 2023 · 9ef594f · 9ef594f
1 parent a76746c
commit 9ef594f
Show file tree

Hide file tree

Showing 3 changed files with 36 additions and 2 deletions.
diff --git a/source/rust_verify_test/tests/assert_by_compute.rs b/source/rust_verify_test/tests/assert_by_compute.rs
@@ -486,3 +486,18 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] partially_simplified_boxed_sequence_699 verus_code! {
+        #[allow(unused_imports)]
+        use vstd::seq::*;
+
+        // GitHub issue 699: When converting partially simplified
+        // sequences to SST, handle boxed sequence types as well
+        proof fn test() {
+            let s: Seq<int> = seq![1, 2, 3, 4, 5];
+            let even: Seq<int> = s.filter(|x: int| x % 2 == 0);
+            assert(even =~= seq![2, 4]) by (compute);   // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}
diff --git a/source/vir/src/interpreter.rs b/source/vir/src/interpreter.rs
@@ -1575,15 +1575,34 @@ fn eval_expr_launch(
                             TypX::Datatype(_, typs, _) => {
                                 // Grab the type the sequence holds
                                 let inner_type = typs[0].clone();
+                                // Convert back to a standard SST sequence representation
                                 let s = seq_to_sst(&e.span, inner_type.clone(), v);
-                                // Wrap the sequence construction in unwrap to account for the Poly
+                                // Wrap the sequence construction in unbox to account for the Poly
                                 // type of the sequence functions
                                 let unbox_opr = crate::ast::UnaryOpr::Unbox(e.typ.clone());
                                 let unboxed_expx = crate::sst::ExpX::UnaryOpr(unbox_opr, s);
                                 let unboxed_e =
                                     SpannedTyped::new(&e.span, &e.typ.clone(), unboxed_expx);
                                 Ok(unboxed_e)
                             }
+                            TypX::Boxed(t) => {
+                                match &**t {
+                                    TypX::Datatype(_, typs, _) => {
+                                        // Grab the type the sequence holds
+                                        let inner_type = typs[0].clone();
+                                        // Convert back to a standard SST sequence representation
+                                        let s = seq_to_sst(&e.span, inner_type.clone(), v);
+                                        Ok(s)
+                                    }
+                                    _ => error(
+                                        &e.span,
+                                        format!(
+                                            "Internal error: Expected to find a sequence type but found: {:?}",
+                                            e.typ,
+                                        ),
+                                    ),
+                                }
+                            }
                             _ => error(
                                 &e.span,
                                 format!(

diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs
@@ -963,7 +963,7 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result<
             }
             UnaryOpr::Unbox(typ) => {
                 let expr = exp_to_expr(ctx, exp, expr_ctxt)?;
-                try_unbox(ctx, expr, typ).expect("Unbox")
+                try_unbox(ctx, expr.clone(), typ).expect(&format!("Unbox: {:?}", expr).to_owned())
             }
             UnaryOpr::HasType(typ) => {
                 let expr = exp_to_expr(ctx, exp, expr_ctxt)?;