Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339use crate::ast::*;use crate::ast_util::{ array_kind_of_typ, bool_typ, conjoin, disjoin, if_then_else, int_typ, mk_eq, mk_ineq, mk_int_lit_from_usize, place_to_spec_expr,};use crate::context::GlobalCtx;use crate::def::Spanned;use crate::messages::{Span, error};use std::collections::HashMap;use std::sync::Arc;
pub fn pattern_to_exprs( ctx: &GlobalCtx, place: &Place, pattern: &Pattern, has_guard: bool, decls: &mut Vec<Stmt>,) -> Result<Expr, VirErr> { let mut pattern_bound_decls = vec![]; let e = pattern_to_exprs_rec(ctx, pattern, place, &mut pattern_bound_decls, false)?;
for pbd in pattern_bound_decls { if has_guard && pbd.mut_ref { return Err(error( &pattern.span, "Verus does not currently support a match guard when at least one bound variable is mutably borrowed", )); }
let ComputedPatternBinding { name, mut_ref, place } = pbd;
let place = if mut_ref { PlaceX::spec_temporary(SpannedTyped::new( &place.span, &Arc::new(TypX::MutRef(place.typ.clone())), ExprX::BorrowMut(place.clone()), )) } else { place };
let pattern = PatternX::simple_var(name, &place.span, &place.typ); // Mode doesn't matter at this stage; arbitrarily set it to None let decl = StmtX::Decl { pattern, mode: None, init: Some(place.clone()), els: None, assert_irrefutable: false, }; decls.push(Spanned::new(place.span.clone(), decl)); }
Ok(e)}
struct ComputedPatternBinding { name: VarIdent, mut_ref: bool, place: Place,}
fn computed(binding: &PatternBinding, place: &Place) -> Result<ComputedPatternBinding, VirErr> { Ok(ComputedPatternBinding { name: binding.name.clone(), place: place.clone(), mut_ref: matches!(binding.by_ref, ByRef::MutRef), })}
fn read_place(place: &Place) -> Expr { SpannedTyped::new( &place.span, &place.typ, ExprX::ReadPlace( place.clone(), UnfinalizedReadKind { preliminary_kind: ReadKind::ImmutBor, id: 0 }, ), )}
fn err_if_bad_binding(span: &Span, in_immut: bool, by_ref: ByRef) -> Result<(), VirErr> { // extra sanity check, should be caught by lifetime checking, though if in_immut && matches!(by_ref, ByRef::MutRef) { return Err(error( span, "cannot borrow this place as mutable, as it is behind a `&` reference", )); } Ok(())}
fn pattern_to_exprs_rec( ctx: &GlobalCtx, pattern: &Pattern, place: &Place, bindings: &mut Vec<ComputedPatternBinding>, in_immut: bool,) -> Result<Expr, VirErr> { let t_bool = Arc::new(TypX::Bool); match &pattern.x { PatternX::Wildcard => { Ok(SpannedTyped::new(&pattern.span, &t_bool, ExprX::Const(Constant::Bool(true)))) } PatternX::Var(binding) => { err_if_bad_binding(&pattern.span, in_immut, binding.by_ref)?; bindings.push(computed(binding, place)?); Ok(SpannedTyped::new(&pattern.span, &t_bool, ExprX::Const(Constant::Bool(true)))) } PatternX::Binding { binding, sub_pat } => { err_if_bad_binding(&pattern.span, in_immut, binding.by_ref)?; let pattern_test = pattern_to_exprs_rec(ctx, sub_pat, place, bindings, in_immut)?; // This binding needs to go last in case we have something like this: // `ref mut x @ Some(y)` // (which is ok if the y is bound via copy) // In this case we need to read `y` before taking the mut ref bindings.push(computed(binding, place)?); Ok(pattern_test) } PatternX::Constructor(dt, variant, patterns) => { let expr = read_place(&place); let is_variant_opr = UnaryOpr::IsVariant { datatype: dt.clone(), variant: variant.clone() }; let test_variant = SpannedTyped::new( &pattern.span, &bool_typ(), ExprX::UnaryOpr(is_variant_opr, expr.clone()), );
let mut test = test_variant;
for binder in patterns.iter() { let field_opr = FieldOpr { datatype: dt.clone(), variant: variant.clone(), field: binder.name.clone(), get_variant: false, check: VariantCheck::None, }; let field_typ = &binder.a.typ; let field_place = SpannedTyped::new( &binder.a.span, field_typ, PlaceX::Field(field_opr, place.clone()), ); let pattern_test = pattern_to_exprs_rec(ctx, &binder.a, &field_place, bindings, in_immut)?; let and = ExprX::Logical(LogicalOp::And, test, pattern_test); test = SpannedTyped::new(&pattern.span, &t_bool, and); }
Ok(test) } PatternX::Or(pat1, pat2) => { let mut bindings1 = vec![]; let mut bindings2 = vec![];
let pat1_matches = pattern_to_exprs_rec(ctx, pat1, place, &mut bindings1, in_immut)?; let pat2_matches = pattern_to_exprs_rec(ctx, pat2, place, &mut bindings2, in_immut)?;
let matches = disjoin(&pattern.span, &vec![pat1_matches.clone(), pat2_matches]);
assert!(bindings1.len() == bindings2.len()); for d1 in bindings1 { let d2 = bindings2 .iter() .find(|d2| d2.name == d1.name) .expect("both sides of 'or' pattern should bind the same variables"); assert!(!d1.mut_ref); assert!(!d2.mut_ref);
let e1 = place_to_spec_expr(&d1.place); let e2 = place_to_spec_expr(&d2.place); let ite = if_then_else(&pattern.span, &pat1_matches, &e1, &e2);
let combined_binding = ComputedPatternBinding { name: d1.name, mut_ref: false, place: PlaceX::spec_temporary(ite), }; bindings.push(combined_binding); }
Ok(matches) } PatternX::Expr(e) => { let expr = read_place(&place); Ok(mk_eq(&pattern.span, &expr, e)) } PatternX::Range(lower, upper) => { let expr = read_place(&place); let mut v = vec![]; if let Some(lower) = lower { v.push(mk_ineq(&pattern.span, lower, &expr, InequalityOp::Le)); } if let Some((upper, upper_ineq)) = upper { v.push(mk_ineq(&pattern.span, &expr, upper, *upper_ineq)); } Ok(conjoin(&pattern.span, &v)) } PatternX::ImmutRef(sub_pat) => pattern_to_exprs_rec(ctx, sub_pat, place, bindings, true), PatternX::MutRef(sub_pat) => { let deref_place = SpannedTyped::new(&sub_pat.span, &sub_pat.typ, PlaceX::DerefMut(place.clone())); pattern_to_exprs_rec(ctx, sub_pat, &deref_place, bindings, in_immut) } PatternX::Slice(patterns) => { let (kind, elem_typ) = array_kind_of_typ(&pattern.typ);
let mut conjuncts = vec![];
// If it's a slice, we need to test the length if kind == ArrayKind::Slice { let actual_len = SpannedTyped::new( &pattern.span, &int_typ(), ExprX::Unary(UnaryOp::Length(ArrayKind::Slice), read_place(&place)), ); let expected_len = mk_int_lit_from_usize(&pattern.span, patterns.len()); conjuncts.push(mk_eq(&pattern.span, &actual_len, &expected_len)); }
for (i, p) in patterns.iter().enumerate() { let idx = mk_int_lit_from_usize(&p.span, i); let index_place = SpannedTyped::new( &p.span, &elem_typ, PlaceX::Index(place.clone(), idx, kind, BoundsCheck::Allow), ); let pattern_test = pattern_to_exprs_rec(ctx, p, &index_place, bindings, in_immut)?; conjuncts.push(pattern_test); }
Ok(conjoin(&pattern.span, &conjuncts)) } }}
pub fn pattern_find_mut_binding(pattern: &Pattern) -> Option<Span> { match &pattern.x { PatternX::Wildcard => None, PatternX::Var(binding) => { if matches!(binding.by_ref, ByRef::MutRef) { Some(pattern.span.clone()) } else { None } } PatternX::Binding { binding, sub_pat } => { if matches!(binding.by_ref, ByRef::MutRef) { Some(pattern.span.clone()) } else { pattern_find_mut_binding(sub_pat) } } PatternX::Constructor(_path, _variant, patterns) => { for binder in patterns.iter() { match pattern_find_mut_binding(&binder.a) { s @ Some(_) => { return s; } None => {} } } None } PatternX::Or(pat1, pat2) => { match pattern_find_mut_binding(pat1) { s @ Some(_) => { return s; } None => {} } pattern_find_mut_binding(pat2) } PatternX::Expr(_e) => None, PatternX::Range(_lower, _upper) => None, PatternX::ImmutRef(p) | PatternX::MutRef(p) => pattern_find_mut_binding(p), PatternX::Slice(patterns) => { for p in patterns.iter() { match pattern_find_mut_binding(p) { s @ Some(_) => { return s; } None => {} } } None } }}
pub(crate) fn pattern_has_mut(pattern: &Pattern) -> bool { pattern_find_mut_binding(pattern).is_some()}
pub(crate) fn pattern_has_or(pattern: &Pattern) -> bool { match &pattern.x { PatternX::Wildcard => false, PatternX::Var(_binding) => false, PatternX::Binding { binding: _, sub_pat } => pattern_has_or(sub_pat), PatternX::Constructor(_path, _variant, patterns) => { patterns.iter().any(|p| pattern_has_or(&p.a)) } PatternX::Or(_pat1, _pat2) => true, PatternX::Expr(_e) => false, PatternX::Range(_lower, _upper) => false, PatternX::ImmutRef(p) | PatternX::MutRef(p) => pattern_has_or(p), PatternX::Slice(patterns) => patterns.iter().any(|p| pattern_has_or(p)), }}
/// Returns true ==> the pattern is irrefutablepub(crate) fn definitely_irrefutable( pattern: &Pattern, datatypes: &HashMap<Path, Datatype>,) -> bool { match &pattern.x { PatternX::Wildcard => true, PatternX::Var(_binding) => true, PatternX::Binding { binding: _, sub_pat } => definitely_irrefutable(sub_pat, datatypes), PatternX::Constructor(dt, _variant, patterns) => { let one_variant = match dt { Dt::Path(p) => datatypes[p].x.variants.len() == 1, Dt::Tuple(_) => true, }; one_variant && patterns.iter().all(|p| definitely_irrefutable(&p.a, datatypes)) } PatternX::Or(_pat1, _pat2) => false, PatternX::Expr(_e) => false, PatternX::Range(_lower, _upper) => false, PatternX::ImmutRef(p) | PatternX::MutRef(p) => definitely_irrefutable(p, datatypes), PatternX::Slice(patterns) => match array_kind_of_typ(&pattern.typ).0 { ArrayKind::Slice => false, ArrayKind::Array => patterns.iter().all(|p| definitely_irrefutable(p, datatypes)), }, }}