Skip to content

Commit 9e00c04

Browse files
slerpyyyslerpyyy
authored
Add call body to VIR and SST (#2623)
1 parent dbd208c commit 9e00c04

21 files changed

Lines changed: 440 additions & 186 deletions

‎source/rust_verify/src/fn_call_to_vir.rs‎

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -319,7 +319,7 @@ fn fn_call_or_assoc_const_to_vir<'tcx>(
319319
Ok(bctx.spanned_typed_new(
320320
expr.span,
321321
&expr_typ()?,
322-
ExprX::Call(target, Arc::new(vir_args), None),
322+
ExprX::Call { target, args: Arc::new(vir_args), post_args: None, body: None },
323323
))
324324
}
325325

@@ -395,7 +395,7 @@ pub(crate) fn deref_to_vir<'tcx>(
395395
let call_target =
396396
CallTarget::Fun(target_kind, trait_fun, typ_args, impl_paths, call_target_attrs);
397397
let args = Arc::new(vec![arg.clone()]);
398-
let x = ExprX::Call(call_target, args, None);
398+
let x = ExprX::Call { target: call_target, args, post_args: None, body: None };
399399

400400
Ok(bctx.spanned_typed_new(span, &expr_typ, x))
401401
}
@@ -2022,11 +2022,12 @@ fn verus_item_to_vir<'tcx, 'a>(
20222022

20232023
let impl_paths = get_impl_paths(bctx, f, node_substs, None, false, expr.span)?;
20242024

2025-
return mk_expr(ExprX::Call(
2026-
CallTarget::BuiltinSpecFun(bsf, typ_args, impl_paths),
2027-
Arc::new(vir_args),
2028-
None,
2029-
));
2025+
return mk_expr(ExprX::Call {
2026+
target: CallTarget::BuiltinSpecFun(bsf, typ_args, impl_paths),
2027+
args: Arc::new(vir_args),
2028+
post_args: None,
2029+
body: None,
2030+
});
20302031
}
20312032
VerusItem::ErasedGhostValue
20322033
| VerusItem::ShadowGhostValue

‎source/rust_verify/src/rust_to_vir_expr.rs‎

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1491,7 +1491,7 @@ pub(crate) fn expr_to_vir_with_adjustments<'tcx>(
14911491
);
14921492
let arg = arg.consume(bctx, get_inner_ty());
14931493
let args = Arc::new(vec![arg.clone()]);
1494-
let x = ExprX::Call(call_target, args, None);
1494+
let x = ExprX::Call { target: call_target, args, post_args: None, body: None };
14951495
let expr_typ = bctx.mid_ty_to_vir(expr.span, &ty2)?;
14961496
Ok(ExprOrPlace::Expr(bctx.spanned_typed_new(expr.span, &expr_typ, x)))
14971497
} else {
@@ -2161,7 +2161,12 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
21612161
Ok(ExprOrPlace::Expr(bctx.spanned_typed_new(
21622162
expr.span,
21632163
&expr_typ,
2164-
ExprX::Call(target, Arc::new(vir_args), None),
2164+
ExprX::Call {
2165+
target,
2166+
args: Arc::new(vir_args),
2167+
post_args: None,
2168+
body: None,
2169+
},
21652170
)))
21662171
}
21672172
}
@@ -2211,7 +2216,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
22112216
call_target_attrs,
22122217
);
22132218
let args = Arc::new(vec![arg_vir.clone()]);
2214-
mk_expr(ExprX::Call(call_target, args, None))
2219+
mk_expr(ExprX::Call { target: call_target, args, post_args: None, body: None })
22152220
} else {
22162221
// Could be a const. In this case the array needs to be translated like:
22172222
// forall |i| array[i] satisfies post-condition of const
@@ -2312,7 +2317,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
23122317
call_target_attrs,
23132318
);
23142319
let args = Arc::new(vec![source_vir_expr.clone()]);
2315-
mk_expr(ExprX::Call(call_target, args, None))
2320+
mk_expr(ExprX::Call { target: call_target, args, post_args: None, body: None })
23162321
}
23172322
_ => {
23182323
let to_ty = bctx.types.expr_ty(expr);
@@ -3100,7 +3105,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
31003105
// tgt[idx] is equivalent to either *index(tgt, idx) or *index_mut(tgt, idx)
31013106
// (The * on the outside isn't part of the adjustments; we add it here)
31023107
let args = Arc::new(vec![tgt_vir.clone(), idx_vir.clone()]);
3103-
let x = ExprX::Call(call_target, args, None);
3108+
let x = ExprX::Call { target: call_target, args, post_args: None, body: None };
31043109
let call_ret_typ = if mutbl {
31053110
Arc::new(TypX::MutRef(expr_typ()?))
31063111
} else {
@@ -3946,7 +3951,7 @@ pub(crate) fn maybe_do_ptr_cast<'tcx>(
39463951
call_target_attrs,
39473952
);
39483953
let args = Arc::new(vec![src_vir.clone()]);
3949-
let x = ExprX::Call(call_target, args, None);
3954+
let x = ExprX::Call { target: call_target, args, post_args: None, body: None };
39503955
let expr_typ = typ_of_node_unadjusted(bctx, dst_expr.span, &dst_expr.hir_id)?;
39513956

39523957
if clip {

‎source/vir/src/ast.rs‎

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1065,9 +1065,18 @@ pub enum ExprX {
10651065
/// Use of a static variable.
10661066
StaticVar(Fun),
10671067
/// Call to a function passing some expression arguments
1068-
/// The optional expression is to be executed *after* the arguments but *before* the call.
1069-
/// This is used for two-phase borrows.
1070-
Call(CallTarget, Exprs, Option<Expr>),
1068+
Call {
1069+
target: CallTarget,
1070+
args: Exprs,
1071+
/// To be executed *after* the arguments but *before* the call.
1072+
///
1073+
/// This is used for two-phase borrows.
1074+
post_args: Option<Expr>,
1075+
/// Executed *inside* the function call, between the pre- and postcondition.
1076+
///
1077+
/// We use this for the `atomically |update| { ... }` block of the atomic function call.
1078+
body: Option<Expr>,
1079+
},
10711080
/// Construct datatype value of type Path and variant Ident,
10721081
/// with field initializers Binders<Expr> and an optional ".." update expression.
10731082
/// For tuple-style variants, the fields are named "0", "1", etc.

‎source/vir/src/ast_simplify.rs‎

Lines changed: 29 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -365,20 +365,26 @@ fn simplify_one_expr(
365365
const_var: true,
366366
assume_external_allowed: false,
367367
};
368-
let call = ExprX::Call(
369-
CallTarget::Fun(
368+
let call = ExprX::Call {
369+
target: CallTarget::Fun(
370370
CallTargetKind::Static,
371371
x.clone(),
372372
Arc::new(vec![]),
373373
Arc::new(vec![]),
374374
call_target_attrs,
375375
),
376-
Arc::new(vec![]),
377-
None,
378-
);
376+
args: Arc::new(vec![]),
377+
post_args: None,
378+
body: None,
379+
};
379380
Ok(SpannedTyped::new(&expr.span, &expr.typ, call))
380381
}
381-
ExprX::Call(CallTarget::Fun(kind, tgt, typs, impl_paths, attrs), args, post_args) => {
382+
ExprX::Call {
383+
target: CallTarget::Fun(kind, tgt, typs, impl_paths, attrs),
384+
args,
385+
post_args,
386+
body,
387+
} => {
382388
assert!(attrs.autospec == AutospecUsage::Final);
383389

384390
let is_trait_impl = match kind {
@@ -399,17 +405,18 @@ fn simplify_one_expr(
399405
args.clone()
400406
};
401407

402-
let call = ExprX::Call(
403-
CallTarget::Fun(
408+
let call = ExprX::Call {
409+
target: CallTarget::Fun(
404410
kind.clone(),
405411
tgt.clone(),
406412
typs.clone(),
407413
impl_paths.clone(),
408414
attrs.clone(),
409415
),
410416
args,
411-
post_args.clone(),
412-
);
417+
post_args: post_args.clone(),
418+
body: body.clone(),
419+
};
413420
Ok(SpannedTyped::new(&expr.span, &expr.typ, call))
414421
}
415422
ExprX::Ctor(name, variant, partial_binders, Some(update)) => {
@@ -785,15 +792,16 @@ fn mk_closure_req_call(
785792
SpannedTyped::new(
786793
span,
787794
&bool_typ,
788-
ExprX::Call(
789-
CallTarget::BuiltinSpecFun(
795+
ExprX::Call {
796+
target: CallTarget::BuiltinSpecFun(
790797
BuiltinSpecFun::ClosureReq,
791798
closure_trait_call_typ_args(state, fn_val, params),
792799
Arc::new(vec![]),
793800
),
794-
Arc::new(vec![fn_val.clone(), arg_tuple.clone()]),
795-
None,
796-
),
801+
args: Arc::new(vec![fn_val.clone(), arg_tuple.clone()]),
802+
post_args: None,
803+
body: None,
804+
},
797805
)
798806
}
799807

@@ -810,15 +818,16 @@ fn mk_closure_ens_call(
810818
SpannedTyped::new(
811819
span,
812820
&bool_typ,
813-
ExprX::Call(
814-
CallTarget::BuiltinSpecFun(
821+
ExprX::Call {
822+
target: CallTarget::BuiltinSpecFun(
815823
builtin_spec_fun,
816824
closure_trait_call_typ_args(state, fn_val, params),
817825
Arc::new(vec![]),
818826
),
819-
Arc::new(vec![fn_val.clone(), arg_tuple.clone(), ret_arg.clone()]),
820-
None,
821-
),
827+
args: Arc::new(vec![fn_val.clone(), arg_tuple.clone(), ret_arg.clone()]),
828+
post_args: None,
829+
body: None,
830+
},
822831
)
823832
}
824833

0 commit comments

Comments
 (0)