Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912913914915916917918919920921922923924925926927928929930931932933934935936937938939940941942943944945946947948949950951952953954955956957958959960961962963964965966967968969970971972973974975976977978979980981982983984985986987988989990991992993994995996997998999100010011002100310041005100610071008100910101011101210131014101510161017101810191020102110221023102410251026102710281029103010311032103310341035103610371038103910401041104210431044104510461047104810491050105110521053105410551056105710581059106010611062106310641065106610671068106910701071107210731074107510761077107810791080108110821083108410851086108710881089109010911092109310941095109610971098109911001101110211031104110511061107110811091110111111121113111411151116111711181119112011211122112311241125112611271128112911301131113211331134113511361137113811391140114111421143114411451146114711481149115011511152115311541155115611571158115911601161116211631164116511661167116811691170117111721173117411751176117711781179118011811182118311841185118611871188118911901191119211931194119511961197119811991200120112021203120412051206120712081209121012111212121312141215121612171218121912201221122212231224122512261227122812291230123112321233123412351236123712381239124012411242124312441245124612471248124912501251125212531254125512561257125812591260126112621263126412651266126712681269127012711272127312741275127612771278127912801281128212831284128512861287128812891290129112921293129412951296129712981299130013011302130313041305130613071308130913101311131213131314131513161317131813191320132113221323132413251326132713281329133013311332133313341335133613371338133913401341134213431344134513461347134813491350135113521353135413551356135713581359136013611362136313641365136613671368136913701371137213731374137513761377137813791380138113821383138413851386138713881389139013911392139313941395139613971398139914001401140214031404140514061407140814091410141114121413141414151416141714181419142014211422142314241425142614271428142914301431143214331434143514361437143814391440144114421443144414451446144714481449//! Insert Poly types and Box/Unbox expressions to represent polymorphism (generics).
/*The SMT solver does not support polymorphic types directly,so polymorphism must be encoded by coercing expressions to and from a universalPoly type via Box and Unbox coercions.The predicate has_type describes which underlying type a Box value holds.
In this encoding, we have to decide which expressions have native monomorphictypes (e.g. int, bool) and which expressions have Poly type.This decision is motivated by three goals:
1) For efficiency, use native types where possible, avoiding unnecessary coercions. (For example, to represent 1 + 2 + 3, we wouldn't want to coerce between int and Poly around every + operation.)2) For efficiency, since we've already type-checked the expressions, avoid reasoning about has_type unless necessary.3) For completeness, avoid adding coercions to variables inside quantifier triggers, because this can cause expressions to fail to match triggers in some cases. For example, if f(g(a)) is encoded without coercions in one place, but there's a quantifier that encodes f(x) as f(Box(x)), using a trigger f(Box(x)), then f(g(a)) will fail to match the f(Box(x)) trigger for any x, whereas without the Box, f(g(a)) matches f(x) via x = g(a).
These goals are in conflict, unfortunately, so we have to compromise.We prioritize (3) to avoid inexplicable triggering failures, and wedo as best we can with (1) and (2) on a case-by-case basis.
For (2), we introduce sorts to represent monomorphic instantiations of abstract datatypes.For example, if Set<A> is an abstract datatype, Set<u64> and Set<bool> would each get their own sort.On the other hand, we represent abstract datatypes applied to type variables as Poly.
REVIEW: We could also introduce sorts to represent integer range types like u64,but this would lead to extra complexity, so we use int and Poly instead.
Suppose Map<A, B> is an abstract datatype and Pair<A, B> is a transparent datatype.The following table summarizes what sorts are used for which Rust types in which situations,where A is a type parameter:
bool int u64 A Map<u64, u8> Map<u64, A> Pair<u64, u8> Pair<u64, A>
quantifier variable Poly Poly Poly Poly Poly Poly Poly Polyspec function parameter Poly Poly Poly Poly Poly Poly Poly Polytrait method parameter Poly Poly Poly Poly Poly Poly Poly Polytrait method return type Poly Poly Poly Poly Poly Poly Poly Poly
exec/proof function parameter bool int int* Poly map_u64_u8 Poly pair* pair*datatype field bool int int* Poly map_u64_u8 Poly pair* pair*return type bool int int* Poly map_u64_u8 Poly pair* pair*local variable / let binding bool int int* Poly map_u64_u8 Poly pair* pair*
(The "int*" and "pair*" indicate that the values of the types need additional invariants,such as a u64 being in the range 0..2^64. In addition, all Poly values need a has_type invariant.)
Because of (3), we represent all quantified variables as Poly types rather than native types.Thus, a VIR quantifier like:
forall x: int. f(x, 1)
becomes an AIR quantifier like one of the following, depending on how we translate f:
forall x: Poly. has_type(x, t) ==> f(x, Box(1)) forall x: Poly. has_type(x, t) ==> f(Unbox(x), Unbox(Box(1)))
The first version assumes that f's parameters are Poly (as is the case for spec functions),while the latter assumes that f's parameters are int (as is the case for datatype constructors).Note that the latter two cases lead to triggers involving "Unbox(x)", not just x.This can lead to the completeness problems of (3).Therefore, the expression Unbox(Box(1)) explicitly introduces a superfluous Unbox to handle (3).
For triggers on arithmetic expressions like #[trigger] (x * y),we use int instead of Poly for the arithmetic variables in the trigger.(This is an exception to the table above.)Otherwise, an expression like 3 * 4 would fail to match the trigger (Unbox(x) * Unbox(y)).
Note that if a variable x is used *both* as a function argument and an arithmetic argument,as in #[trigger] g(f(x), x + 1), we have more flexibility, because any term passed to boththe function and the arithmetic must be boxed or unboxed in one or the other.For example, in g(f(3), 3 + 1) would be represented as g(f(Box(3)), Box(3 + 1)),so that Box(3) triggers the unbox-box axiom yielding Unbox(Box(3)) = 3.In this case, a trigger of g(f(x), Unbox(x) + 1) for x: Poly e-matches the expanded termg(f(Box(3)), Box(Unbox(Box(3)) + 1)).We take advantage of this to support mixed function-arithmetic triggers with Poly variables(native variables would also work if we wanted, relying on Box(Unbox(x)) axioms.)*/
use crate::ast::{ AssocTypeImpl, Datatype, DatatypeX, Dt, FieldOpr, FunctionKind, IntRange, Mode, NullaryOpr, Primitive, SpannedTyped, Typ, TypDecorationArg, TypX, Typs, UnaryOp, UnaryOpr, VarBinder, VarBinderX, VarBinders, VarIdent, Variant,};use crate::ast_util::typ_contains_opaque;use crate::context::Ctx;use crate::def::Spanned;use crate::sst::{ BinaryOp, BndX, CallFun, Dest, Exp, ExpX, Exps, FuncCheckSst, FuncDeclSst, FunctionSst, FunctionSstX, InternalFun, KrateSst, KrateSstX, LocalDecl, LocalDeclKind, Par, ParX, Pars, PostConditionSst, Stm, StmX, Stms, Trigs, UnwindSst,};use crate::triggers::native_quant_vars;use crate::util::vec_map;use air::ast::Binder;use air::scope_map::ScopeMap;use std::collections::{HashMap, HashSet};use std::sync::Arc;
pub type MonoTyp = Arc<MonoTypX>;pub type MonoTyps = Arc<Vec<MonoTyp>>;#[derive(Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]pub enum MonoTypX { Bool, Int(IntRange), Real, Float(u32), Datatype(Dt, MonoTyps), Decorate(crate::ast::TypDecoration, MonoTyp), Decorate2(crate::ast::TypDecoration, MonoTyps), Primitive(Primitive, MonoTyps),}
struct State { remaining_temps: HashSet<VarIdent>, types: ScopeMap<VarIdent, Typ>, temp_types: HashMap<VarIdent, Typ>, is_trait: bool, in_exec_closure: bool, // does the function return type contain an opaque type encoded as Poly? is_poly_ret_with_opaque: bool,}
fn monotyps_as_mono(typs: &Typs) -> Option<Vec<MonoTyp>> { let mut monotyps: Vec<MonoTyp> = Vec::new(); for typ in typs.iter() { if let Some(monotyp) = typ_as_mono(typ) { monotyps.push(monotyp); } else { return None; } } Some(monotyps)}
pub(crate) fn typ_as_mono(typ: &Typ) -> Option<MonoTyp> { match &**typ { TypX::Bool => Some(Arc::new(MonoTypX::Bool)), TypX::Int(range) => Some(Arc::new(MonoTypX::Int(*range))), TypX::Real => Some(Arc::new(MonoTypX::Real)), TypX::Float(range) => Some(Arc::new(MonoTypX::Float(*range))), TypX::Datatype(path, typs, _impl_paths) => { let monotyps = monotyps_as_mono(typs)?; Some(Arc::new(MonoTypX::Datatype(path.clone(), Arc::new(monotyps)))) } TypX::Dyn(..) => None, TypX::Decorate(d, None, t) => typ_as_mono(t).map(|m| Arc::new(MonoTypX::Decorate(*d, m))), TypX::Decorate(d, Some(TypDecorationArg { allocator_typ }), t) => { let m1 = typ_as_mono(allocator_typ)?; let m2 = typ_as_mono(t)?; Some(Arc::new(MonoTypX::Decorate2(*d, Arc::new(vec![m1, m2])))) } TypX::Primitive(Primitive::Array, _) => None, TypX::Primitive(name, typs) => { let monotyps = monotyps_as_mono(typs)?; Some(Arc::new(MonoTypX::Primitive(*name, Arc::new(monotyps)))) } TypX::AnonymousClosure(..) => { panic!("internal error: AnonymousClosure should be removed by ast_simplify") } TypX::TypeId => panic!("internal error: TypeId created too soon"), TypX::Air(_) => panic!("internal error: Air type created too soon"), TypX::Boxed(..) | TypX::TypParam(..) | TypX::SpecFn(..) | TypX::FnDef(..) => None, TypX::ConstInt(_) => None, TypX::ConstBool(_) => None, TypX::Projection { .. } => None, TypX::PointeeMetadata(_) => None, TypX::MutRef(_) => None, TypX::Opaque { .. } => None, }}
pub(crate) fn monotyp_to_typ(monotyp: &MonoTyp) -> Typ { match &**monotyp { MonoTypX::Bool => Arc::new(TypX::Bool), MonoTypX::Int(range) => Arc::new(TypX::Int(*range)), MonoTypX::Real => Arc::new(TypX::Real), MonoTypX::Float(range) => Arc::new(TypX::Float(*range)), MonoTypX::Datatype(path, typs) => { let typs = vec_map(&**typs, monotyp_to_typ); Arc::new(TypX::Datatype(path.clone(), Arc::new(typs), Arc::new(vec![]))) } MonoTypX::Primitive(name, typs) => { let typs = vec_map(&**typs, monotyp_to_typ); Arc::new(TypX::Primitive(*name, Arc::new(typs))) } MonoTypX::Decorate(d, typ) => Arc::new(TypX::Decorate(*d, None, monotyp_to_typ(typ))), MonoTypX::Decorate2(d, typs) => { assert!(typs.len() == 2); let allocator_typ = monotyp_to_typ(&typs[0]); let typ = monotyp_to_typ(&typs[1]); Arc::new(TypX::Decorate(*d, Some(TypDecorationArg { allocator_typ }), typ)) } }}
pub(crate) fn typ_is_poly(ctx: &Ctx, typ: &Typ) -> bool { match &**typ { TypX::Bool | TypX::Int(_) | TypX::Real | TypX::Float(_) => false, TypX::SpecFn(..) | TypX::FnDef(..) => false, TypX::Primitive(Primitive::Array, _) => false, TypX::AnonymousClosure(..) => { panic!("internal error: AnonymousClosure should be removed by ast_simplify") } TypX::Datatype(path, _, _) => { if ctx.datatype_is_transparent[path] { false } else { typ_as_mono(typ).is_none() } } TypX::Dyn(..) => true, TypX::Decorate(_, _, t) => typ_is_poly(ctx, t), // Note: we rely on rust_to_vir_base normalizing TypX::Projection { .. }. // If it normalized to a projection, it is poly; otherwise it is handled by // one of the other TypX::* cases. TypX::Boxed(_) | TypX::TypParam(_) | TypX::Projection { .. } | TypX::PointeeMetadata(_) => { true } TypX::Primitive(_, _) => typ_as_mono(typ).is_none(), TypX::TypeId => panic!("internal error: TypeId created too soon"), TypX::ConstInt(_) => panic!("internal error: expression should not have ConstInt type"), TypX::ConstBool(_) => panic!("internal error: expression should not have ConstBool type"), TypX::Air(_) => panic!("internal error: Air type created too soon"), TypX::MutRef(_) => true, TypX::Opaque { .. } => true, }}
/// Intended to be called on the pre-Poly SSTpub(crate) fn coerce_typ_to_native(ctx: &Ctx, typ: &Typ) -> Typ { match &**typ { TypX::Bool | TypX::Int(_) | TypX::Real | TypX::Float(_) => typ.clone(), TypX::SpecFn(..) | TypX::FnDef(..) => typ.clone(), TypX::Primitive(Primitive::Array, _) => typ.clone(), TypX::AnonymousClosure(..) => { panic!("internal error: AnonymousClosure should be removed by ast_simplify") } TypX::Datatype(path, _, _) => { if ctx.datatype_is_transparent[path] { typ.clone() } else { if typ_as_mono(typ).is_none() { Arc::new(TypX::Boxed(typ.clone())) } else { typ.clone() } } } TypX::Dyn(..) => typ.clone(), TypX::Decorate(d, targ, t) => { Arc::new(TypX::Decorate(*d, targ.clone(), coerce_typ_to_native(ctx, t))) } TypX::Boxed(_) => panic!("Boxed unexpected here"), TypX::TypParam(_) | TypX::Projection { .. } | TypX::PointeeMetadata(_) => typ.clone(), TypX::Primitive(_, _) => { if typ_as_mono(typ).is_none() { Arc::new(TypX::Boxed(typ.clone())) } else { typ.clone() } } TypX::TypeId => panic!("internal error: TypeId created too soon"), TypX::ConstInt(_) => panic!("internal error: expression should not have ConstInt type"), TypX::ConstBool(_) => panic!("internal error: expression should not have ConstBool type"), TypX::Air(_) => panic!("internal error: Air type created too soon"), TypX::MutRef(_) => typ.clone(), TypX::Opaque { .. } => typ.clone(), }}
pub(crate) fn coerce_typ_to_poly(_ctx: &Ctx, typ: &Typ) -> Typ { match &**typ { TypX::Bool | TypX::Int(_) => Arc::new(TypX::Boxed(typ.clone())), TypX::Real | TypX::Float(_) => Arc::new(TypX::Boxed(typ.clone())), TypX::SpecFn(..) | TypX::FnDef(..) => Arc::new(TypX::Boxed(typ.clone())), TypX::AnonymousClosure(..) => { panic!("internal error: AnonymousClosure should be removed by ast_simplify") } TypX::Datatype(..) | TypX::Primitive(_, _) => Arc::new(TypX::Boxed(typ.clone())), TypX::Dyn(..) => typ.clone(), TypX::Decorate(d, targ, t) => { Arc::new(TypX::Decorate(*d, targ.clone(), coerce_typ_to_poly(_ctx, t))) } TypX::Boxed(_) | TypX::TypParam(_) | TypX::Projection { .. } | TypX::PointeeMetadata(_) => { typ.clone() } TypX::TypeId => panic!("internal error: TypeId created too soon"), TypX::ConstInt(_) => typ.clone(), TypX::ConstBool(_) => typ.clone(), TypX::Air(_) => panic!("internal error: Air type created too soon"), TypX::MutRef(_) => typ.clone(), TypX::Opaque { .. } => typ.clone(), }}
pub(crate) fn coerce_exp_to_native(ctx: &Ctx, exp: &Exp) -> Exp { match &*crate::ast_util::undecorate_typ(&exp.typ) { TypX::Bool | TypX::Int(_) | TypX::Real | TypX::Float(_) | TypX::SpecFn(..) | TypX::Datatype(..) | TypX::Dyn(..) | TypX::Primitive(_, _) | TypX::FnDef(..) => exp.clone(), TypX::AnonymousClosure(..) => { panic!("internal error: AnonymousClosure should be removed by ast_simplify") } TypX::Decorate(..) => { panic!("internal error: Decorate should be removed by undecorate_typ") } TypX::Boxed(typ) => { if typ_is_poly(ctx, typ) { exp.clone() } else { let op = UnaryOpr::Unbox(typ.clone()); let expx = ExpX::UnaryOpr(op, exp.clone()); SpannedTyped::new(&exp.span, typ, expx) } } TypX::TypParam(_) | TypX::Projection { .. } | TypX::PointeeMetadata(_) | TypX::MutRef(_) => exp.clone(), TypX::Opaque { .. } => exp.clone(), TypX::TypeId => panic!("internal error: TypeId created too soon"), TypX::ConstInt(_) => panic!("internal error: expression should not have ConstInt type"), TypX::ConstBool(_) => panic!("internal error: expression should not have ConstBool type"), TypX::Air(_) => panic!("internal error: Air type created too soon"), }}
pub(crate) fn coerce_exp_to_poly(ctx: &Ctx, exp: &Exp) -> Exp { if typ_is_poly(ctx, &exp.typ) { exp.clone() } else { let op = UnaryOpr::Box(exp.typ.clone()); let expx = ExpX::UnaryOpr(op, exp.clone()); let typ = Arc::new(TypX::Boxed(exp.typ.clone())); SpannedTyped::new(&exp.span, &typ, expx) }}
fn coerce_exps_to_agree(ctx: &Ctx, exp1: &Exp, exp2: &Exp) -> (Exp, Exp) { if typ_is_poly(ctx, &exp1.typ) && typ_is_poly(ctx, &exp2.typ) { (exp1.clone(), exp2.clone()) } else { match (&*exp1.typ, &*exp2.typ) { (TypX::TypParam(_) | TypX::Projection { .. }, _) | (_, TypX::TypParam(_) | TypX::Projection { .. }) => { // See rust_verify_tests assoc_type_impls ensures_projection_poly // (inherited ensures don't have projections substituted) (coerce_exp_to_poly(ctx, exp1), coerce_exp_to_poly(ctx, exp2)) } _ => (coerce_exp_to_native(ctx, exp1), coerce_exp_to_native(ctx, exp2)), } }}
// Rewrite VarBinders and insert into types into the ScopeMap's current scope.// (The caller must make sure that the ScopeMap has a pushed scope,// and the caller is responsible for eventually popping the scope.)fn visit_and_insert_binders( ctx: &Ctx, types: &mut ScopeMap<VarIdent, Typ>, natives: &HashSet<VarIdent>, bs: &VarBinders<Typ>,) -> VarBinders<Typ> { let mut new_bs: Vec<VarBinder<Typ>> = Vec::new(); for b in bs.iter() { let typ = match &*b.a { TypX::TypeId => b.a.clone(), _ if natives.contains(&b.name) => coerce_typ_to_native(ctx, &b.a), _ => coerce_typ_to_poly(ctx, &b.a), }; let _ = types.insert(b.name.clone(), typ.clone()); let bx = VarBinderX { name: b.name.clone(), a: typ }; new_bs.push(Arc::new(bx)); } Arc::new(new_bs)}
#[derive(Debug)]enum InsertPars { Native, Poly, NativeFor(HashSet<VarIdent>),}
// Rewrite Pars and insert into types into the ScopeMap's current scope.// (The caller must make sure that the ScopeMap has a pushed scope,// and the caller is responsible for eventually popping the scope.)fn visit_and_insert_pars( ctx: &Ctx, types: &mut ScopeMap<VarIdent, Typ>, poly: &InsertPars, pars: &Pars,) -> Pars { // Parameter types are made Poly for spec functions and trait methods let mut new_pars: Vec<Par> = Vec::new(); for par in pars.iter() { let ParX { name, typ, mode } = &par.x; let is_poly = match poly { InsertPars::Native => false, InsertPars::Poly => true, InsertPars::NativeFor(natives) => !natives.contains(name), }; let typ = if is_poly { coerce_typ_to_poly(ctx, typ) } else { coerce_typ_to_native(ctx, typ) }; let _ = types.insert(name.clone(), typ.clone()); let parx = ParX { name: name.clone(), typ, mode: *mode }; new_pars.push(Spanned::new(par.span.clone(), parx)); } Arc::new(new_pars)}
fn return_typ(ctx: &Ctx, function: &FunctionSstX, is_trait: bool, typ: &Typ) -> Typ { if (is_trait || typ_is_poly(ctx, &function.outer_ret.x.typ)) && (function.ens_has_return || function.mode == Mode::Spec) { coerce_typ_to_poly(ctx, typ) } else { coerce_typ_to_native(ctx, typ) }}
pub(crate) fn ret_needs_native( ctx: &Ctx, kind: &FunctionKind, ret_typ: &Typ, dest_typ: &Typ,) -> bool { let is_trait = !matches!(kind, FunctionKind::Static); let ret_typ = if is_trait { coerce_typ_to_poly(ctx, ret_typ) } else { coerce_typ_to_native(ctx, ret_typ) }; let dest_typ = coerce_typ_to_native(ctx, dest_typ); typ_is_poly(ctx, &ret_typ) && !typ_is_poly(ctx, &dest_typ)}
pub(crate) fn arg_is_poly(ctx: &Ctx, kind: &FunctionKind, mode: Mode, arg_typ: &Typ) -> bool { let is_spec = mode == Mode::Spec; let is_trait = !matches!(kind, FunctionKind::Static); is_spec || is_trait || typ_is_poly(ctx, arg_typ)}
fn visit_exp(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp { let mk_exp = |e: ExpX| SpannedTyped::new(&exp.span, &exp.typ, e); let mk_exp_typ = |t: &Typ, e: ExpX| SpannedTyped::new(&exp.span, t, e); match &exp.x { ExpX::Const(_) => exp.clone(), ExpX::Var(x) => SpannedTyped::new( &exp.span, match state.types.get(x) { Some(typ) => typ, None => { // If you encounter this, consider giving the variable a LocalDeclKind // that is not TempViaAssign. panic!("variable is unknown or type has not been inferred: {:?}", x) } }, ExpX::Var(x.clone()), ), ExpX::VarLoc(x) => SpannedTyped::new(&exp.span, &state.types[x], ExpX::VarLoc(x.clone())), ExpX::VarAt(x, at) => { SpannedTyped::new(&exp.span, &state.types[x], ExpX::VarAt(x.clone(), *at)) } ExpX::StaticVar(_) => exp.clone(), ExpX::Loc(e) => { let exp = visit_exp(ctx, state, e); mk_exp_typ(&exp.clone().typ, ExpX::Loc(exp)) } ExpX::Old(..) => panic!("internal error: unexpected ExpX::Old"), ExpX::Call(call_fun, typs, exps) => match call_fun { CallFun::Fun(name, _) | CallFun::Recursive(name) => { let function = match ctx.func_sst_map.get(name) { Some(fun) => &fun.x, None => panic!("unknown function: {:?}", name), };
let is_spec = function.mode == Mode::Spec; let is_trait = !matches!(function.kind, FunctionKind::Static); let mut args: Vec<Exp> = Vec::new(); for (par, arg) in function.pars.iter().zip(exps.iter()) { let arg = if is_spec || is_trait || typ_is_poly(ctx, &par.x.typ) { visit_exp_poly(ctx, state, arg) } else { visit_exp_native(ctx, state, arg) }; args.push(arg); } match call_fun { CallFun::Fun(..) => { assert!(exps.len() == function.pars.len()); } CallFun::Recursive(_) => { assert!(exps.len() == function.pars.len() + 1); let last = exps.last().unwrap(); // The last argument is the fuel parameter assert!(matches!(&last.x, ExpX::Var(_))); args.push(last.clone()); } _ => unreachable!(), }; let typ = return_typ(ctx, function, is_trait, &exp.typ); mk_exp_typ(&typ, ExpX::Call(call_fun.clone(), typs.clone(), Arc::new(args))) } CallFun::InternalFun(InternalFun::OpenInvariantMask(name, _i)) => { let function = &ctx.func_sst_map[name].x; let is_spec = function.mode == Mode::Spec; let is_trait = !matches!(function.kind, FunctionKind::Static); let mut args: Vec<Exp> = Vec::new(); for (par, arg) in function.pars.iter().zip(exps.iter()) { let arg = if is_spec || is_trait || typ_is_poly(ctx, &par.x.typ) { visit_exp_poly(ctx, state, arg) } else { visit_exp_native(ctx, state, arg) }; args.push(arg); } mk_exp(ExpX::Call(call_fun.clone(), typs.clone(), Arc::new(args))) } CallFun::InternalFun( InternalFun::ClosureReq | InternalFun::ClosureEns | InternalFun::DefaultEns, ) => { let exps = visit_exps_poly(ctx, state, exps); mk_exp(ExpX::Call(call_fun.clone(), typs.clone(), exps)) } CallFun::InternalFun(InternalFun::ClosureOpensInvariants) => { let exps = visit_exps_poly(ctx, state, exps); let typ = coerce_typ_to_poly(ctx, &exp.typ); mk_exp_typ(&typ, ExpX::Call(call_fun.clone(), typs.clone(), exps)) } CallFun::InternalFun(InternalFun::CheckDecreaseHeight) => { assert!(exps.len() == 3); let e0 = visit_exp_poly(ctx, state, &exps[0]); let e1 = visit_exp_poly(ctx, state, &exps[1]); let e2 = visit_exp_native(ctx, state, &exps[2]); mk_exp(ExpX::Call(call_fun.clone(), typs.clone(), Arc::new(vec![e0, e1, e2]))) } }, ExpX::CallLambda(callee, args) => { let callee = visit_exp_native(ctx, state, callee); let args = visit_exps_poly(ctx, state, args); let typ = coerce_typ_to_poly(ctx, &exp.typ); mk_exp_typ(&typ, ExpX::CallLambda(callee, args)) } ExpX::Ctor(path, variant, binders) => { let Some(dt) = ctx.datatype_map.get(path) else { panic!("failed to find {path:?} in datatype map"); }; let fields = &dt.x.get_variant(variant).fields; let mut bs: Vec<Binder<Exp>> = Vec::new(); for binder in binders.iter() { let field = crate::ast_util::get_field(fields, &binder.name); let e = if typ_is_poly(ctx, &field.a.0) { visit_exp_poly(ctx, state, &binder.a) } else { // Force an expression of the form unbox(...) to match triggers with unbox: let e = visit_exp_poly(ctx, state, &binder.a); coerce_exp_to_native(ctx, &e) }; bs.push(binder.new_a(e)); } mk_exp(ExpX::Ctor(path.clone(), variant.clone(), Arc::new(bs))) } ExpX::NullaryOpr(NullaryOpr::ConstGeneric(_)) => exp.clone(), ExpX::NullaryOpr(NullaryOpr::TraitBound(..)) => exp.clone(), ExpX::NullaryOpr(NullaryOpr::TypEqualityBound(..)) => exp.clone(), ExpX::NullaryOpr(NullaryOpr::ConstTypBound(..)) => exp.clone(), ExpX::Unary(op, e1) => { let e1 = visit_exp(ctx, state, e1); match op { UnaryOp::IeeeFloat(crate::ast::IeeeFloatUnaryOp::Cast) => { let e1 = coerce_exp_to_poly(ctx, &e1); mk_exp_typ(&coerce_typ_to_poly(ctx, &exp.typ), ExpX::Unary(*op, e1)) } UnaryOp::Not | UnaryOp::Clip { .. } | UnaryOp::IntToReal | UnaryOp::RealToInt | UnaryOp::FloatToBits | UnaryOp::IeeeFloat(..) | UnaryOp::BitNot(_) | UnaryOp::NewStrLit | UnaryOp::StrLen => { let e1 = coerce_exp_to_native(ctx, &e1); mk_exp(ExpX::Unary(*op, e1)) } UnaryOp::HeightTrigger | UnaryOp::Length(_) => { let e1 = coerce_exp_to_poly(ctx, &e1); mk_exp(ExpX::Unary(*op, e1)) } UnaryOp::Trigger(_) | UnaryOp::CoerceMode { .. } => { mk_exp_typ(&e1.typ, ExpX::Unary(*op, e1.clone())) } UnaryOp::MustBeFinalized | UnaryOp::MustBeElaborated => { panic!("internal error: MustBeFinalized in SST") } UnaryOp::CastToInteger => match &*crate::ast_util::undecorate_typ(&e1.typ) { TypX::TypParam(_) => { // View as boxed integer rather than type parameter // (e.g. so that it can be unboxed if needed, // or passed as boxed int argument if needed) e1.new_typ(&Arc::new(TypX::Boxed(Arc::new(TypX::Int(IntRange::Int))))) } _ => e1.clone(), }, UnaryOp::MutRefCurrent | UnaryOp::MutRefFuture(_) => { let e1 = coerce_exp_to_native(ctx, &e1); mk_exp_typ(&coerce_typ_to_poly(ctx, &exp.typ), ExpX::Unary(*op, e1)) } UnaryOp::MutRefFinal(_) => { panic!("internal error: MustBeFinalized in SST") } } } ExpX::UnaryOpr(op, e1) => { let e1 = visit_exp(ctx, state, e1); match op { UnaryOpr::Box(_) | UnaryOpr::Unbox(_) => { panic!("internal error: {:?} already has Box/Unbox", e1) } UnaryOpr::HasType(t) => { // REVIEW: not clear that typ_to_poly is appropriate here for abstract datatypes let (e1, t) = match (typ_is_poly(ctx, &e1.typ), typ_is_poly(ctx, t)) { (false, true) => (coerce_exp_to_poly(ctx, &e1), t.clone()), (true, _) => (e1.clone(), coerce_typ_to_poly(ctx, t)), _ => (e1.clone(), t.clone()), }; mk_exp(ExpX::UnaryOpr(UnaryOpr::HasType(t), e1)) } UnaryOpr::IsVariant { .. } | UnaryOpr::IntegerTypeBound(..) => { let e1 = coerce_exp_to_native(ctx, &e1); mk_exp(ExpX::UnaryOpr(op.clone(), e1)) } UnaryOpr::CustomErr(_) | UnaryOpr::ProofNote(_) | UnaryOpr::AutoDecreases | UnaryOpr::AutoLoopEnsures => { mk_exp_typ(&e1.typ, ExpX::UnaryOpr(op.clone(), e1.clone())) } UnaryOpr::ToDyn(..) => { let e1 = coerce_exp_to_poly(ctx, &e1); mk_exp(ExpX::UnaryOpr(op.clone(), e1)) } UnaryOpr::Field(FieldOpr { datatype, variant, field, get_variant: _, check: _, }) => { let fields = &ctx.datatype_map[datatype].x.get_variant(variant).fields; let field = crate::ast_util::get_field(fields, field);
// Force an expression of the form unbox(...) to match triggers with unbox: let e1 = coerce_exp_to_poly(ctx, &e1); let e1 = coerce_exp_to_native(ctx, &e1);
let exprx = ExpX::UnaryOpr(op.clone(), e1); let typ = if typ_is_poly(ctx, &field.a.0) { coerce_typ_to_poly(ctx, &exp.typ) } else { coerce_typ_to_native(ctx, &exp.typ) }; mk_exp_typ(&typ, exprx) } UnaryOpr::HasResolved(_t) => { let e = coerce_exp_to_poly(ctx, &e1); mk_exp(ExpX::UnaryOpr(op.clone(), e.clone())) } UnaryOpr::LoopIsolationBoundary(..) => { panic!("internal error: LoopIsolationBoundary in SST") } } } ExpX::Binary(BinaryOp::Index(kind), e1, e2) => { let e1 = visit_exp(ctx, state, e1); let e2 = visit_exp(ctx, state, e2); let e1 = coerce_exp_to_native(ctx, &e1); let e2 = coerce_exp_to_poly(ctx, &e2); let typ = coerce_typ_to_poly(ctx, &exp.typ); mk_exp_typ(&typ, ExpX::Binary(BinaryOp::Index(*kind), e1, e2)) } ExpX::Binary(op, e1, e2) => { let e1 = visit_exp(ctx, state, e1); let e2 = visit_exp(ctx, state, e2); let (native, poly) = match op { BinaryOp::And | BinaryOp::Or | BinaryOp::Xor => (true, false), BinaryOp::Implies | BinaryOp::Inequality(_) => (true, false), BinaryOp::HeightCompare { .. } => (false, true), BinaryOp::Arith(..) => (true, false), BinaryOp::RealArith(..) => (true, false), BinaryOp::Eq | BinaryOp::Ne => (false, false), BinaryOp::Bitwise(..) => (true, false), BinaryOp::IeeeFloat(..) => (true, false), BinaryOp::StrGetChar { .. } => (true, false), BinaryOp::Index(..) => unreachable!("Index"), }; if native { let e1 = coerce_exp_to_native(ctx, &e1); let e2 = coerce_exp_to_native(ctx, &e2); mk_exp(ExpX::Binary(*op, e1, e2)) } else if poly { let e1 = coerce_exp_to_poly(ctx, &e1); let e2 = coerce_exp_to_poly(ctx, &e2); mk_exp(ExpX::Binary(*op, e1, e2)) } else { let (e1, e2) = coerce_exps_to_agree(ctx, &e1, &e2); mk_exp(ExpX::Binary(*op, e1, e2)) } } ExpX::BinaryOpr(op @ crate::ast::BinaryOpr::ExtEq(..), e1, e2) => { let e1 = visit_exp_poly(ctx, state, e1); let e2 = visit_exp_poly(ctx, state, e2); mk_exp(ExpX::BinaryOpr(op.clone(), e1, e2)) } ExpX::If(e0, e1, e2) => { let e0 = visit_exp_native(ctx, state, e0); let e1 = visit_exp(ctx, state, e1); let e2 = visit_exp(ctx, state, e2); let (e1, e2) = coerce_exps_to_agree(ctx, &e1, &e2); let t = if typ_is_poly(ctx, &e1.typ) { coerce_typ_to_poly(ctx, &exp.typ) } else { coerce_typ_to_native(ctx, &exp.typ) }; mk_exp_typ(&t, ExpX::If(e0, e1, e2)) } ExpX::WithTriggers(trigs, body) => { let trigs = visit_trigs(ctx, state, trigs); let body = visit_exp(ctx, state, body); mk_exp_typ(&body.clone().typ, ExpX::WithTriggers(trigs, body)) } ExpX::Bind(bnd, e1) => match &bnd.x { BndX::Let(bs) => { state.types.push_scope(true); let mut new_bs: Vec<VarBinder<Exp>> = Vec::new(); for b in bs.iter() { // TODO: this might be better as just visit_exp: let a = visit_exp_native(ctx, state, &b.a); let _ = state.types.insert(b.name.clone(), a.typ.clone()); let bx = VarBinderX { name: b.name.clone(), a }; new_bs.push(Arc::new(bx)); } let e1 = visit_exp(ctx, state, e1); state.types.pop_scope(); mk_exp_typ(&e1.typ, ExpX::Bind(bnd.new_x(BndX::Let(Arc::new(new_bs))), e1.clone())) } BndX::Quant(quant, bs, trigs, _) => { let natives = native_quant_vars(bs, trigs); state.types.push_scope(true); let bs = visit_and_insert_binders(ctx, &mut state.types, &natives, bs); let trigs = visit_trigs(ctx, state, trigs); let e1 = visit_exp_native(ctx, state, e1); state.types.pop_scope(); mk_exp(ExpX::Bind(bnd.new_x(BndX::Quant(*quant, bs, trigs, None)), e1)) } BndX::Lambda(bs, trigs) => { let natives = native_quant_vars(bs, trigs); state.types.push_scope(true); let bs = visit_and_insert_binders(ctx, &mut state.types, &natives, bs); let trigs = visit_trigs(ctx, state, trigs); let e1 = visit_exp_poly(ctx, state, e1); state.types.pop_scope(); mk_exp(ExpX::Bind(bnd.new_x(BndX::Lambda(bs, trigs)), e1)) } BndX::Choose(bs, trigs, e2) => { let natives = native_quant_vars(bs, trigs); state.types.push_scope(true); let bs = visit_and_insert_binders(ctx, &mut state.types, &natives, bs); let trigs = visit_trigs(ctx, state, trigs); let e1 = visit_exp_poly(ctx, state, e1); let e2 = visit_exp_native(ctx, state, e2); state.types.pop_scope(); mk_exp_typ(&e1.clone().typ, ExpX::Bind(bnd.new_x(BndX::Choose(bs, trigs, e2)), e1)) } }, ExpX::ExecFnByName(_) => exp.clone(), ExpX::ArrayLiteral(es) => { let es = visit_exps_poly(ctx, state, es); let typ = coerce_typ_to_poly(ctx, &exp.typ); mk_exp_typ(&typ, ExpX::ArrayLiteral(es)) } ExpX::Interp(_) => panic!("unexpected ExpX::Interp"), ExpX::FuelConst(_) => exp.clone(), }}
fn visit_exps(ctx: &Ctx, state: &mut State, exps: &Exps) -> Exps { Arc::new(exps.iter().map(|e| visit_exp(ctx, state, e)).collect())}
fn visit_exp_native(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp { coerce_exp_to_native(ctx, &visit_exp(ctx, state, exp))}
fn visit_exp_poly(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp { coerce_exp_to_poly(ctx, &visit_exp(ctx, state, exp))}
fn visit_exps_native(ctx: &Ctx, state: &mut State, exps: &Exps) -> Exps { Arc::new(exps.iter().map(|e| visit_exp_native(ctx, state, e)).collect())}
fn visit_exps_poly(ctx: &Ctx, state: &mut State, exps: &Exps) -> Exps { Arc::new(exps.iter().map(|e| visit_exp_poly(ctx, state, e)).collect())}
fn visit_trigs(ctx: &Ctx, state: &mut State, trigs: &Trigs) -> Trigs { Arc::new(trigs.iter().map(|e| visit_exps(ctx, state, e)).collect())}
pub(crate) fn visit_exp_native_for_pure_exp(ctx: &Ctx, exp: &Exp) -> Exp { let mut state = State { remaining_temps: HashSet::new(), types: ScopeMap::new(), temp_types: HashMap::new(), is_trait: false, in_exec_closure: false, is_poly_ret_with_opaque: false, }; visit_exp_native(ctx, &mut state, exp)}
fn take_temp(state: &mut State, dest: &Dest) -> Option<VarIdent> { if dest.is_init { if let ExpX::VarLoc(x) = &dest.dest.x { if state.remaining_temps.contains(x) { state.remaining_temps.remove(x); return Some(x.clone()); } } } None}
fn visit_stm(ctx: &Ctx, state: &mut State, stm: &Stm) -> Stm { let mk_stm = |s: StmX| Spanned::new(stm.span.clone(), s); match &stm.x { StmX::Call { fun, resolved_method, is_trait_default, mode, typ_args, args, split, dest, assert_id, body, } => { let (is_polys, function) = if let crate::sst::CallTarget::Fun(fun) = fun { let function = &ctx.func_sst_map[fun].x; let is_spec = function.mode == Mode::Spec; let is_trait = !matches!(function.kind, FunctionKind::Static); let is_polys: Vec<bool> = function .pars .iter() .map(|par| is_spec || is_trait || typ_is_poly(ctx, &par.x.typ)) .collect(); (is_polys, Some(function)) } else { let is_polys: Vec<bool> = args.iter().map(|_| false).collect(); (is_polys, None) }; let mut new_args: Vec<Exp> = Vec::new(); assert!(is_polys.len() == args.len()); for (is_poly, arg) in is_polys.iter().zip(args.iter()) { let arg = if *is_poly { visit_exp_poly(ctx, state, arg) } else { visit_exp_native(ctx, state, arg) }; new_args.push(arg); } let dest = if let Some(dest) = dest { if let Some(x) = take_temp(state, dest) { let typ = if let Some(function) = function { let is_trait = !matches!(function.kind, FunctionKind::Static); return_typ(ctx, function, is_trait, &dest.dest.typ) } else { dest.dest.typ.clone() }; assert!(!state.temp_types.contains_key(&x)); assert!(!state.types.contains_key(&x)); let _ = state.temp_types.insert(x.clone(), typ.clone()); let _ = state.types.insert(x, typ); } let dst = visit_exp(ctx, state, &dest.dest); Some(Dest { dest: dst, is_init: dest.is_init }) } else { None }; let body = body.as_ref().map(|stm| visit_stm(ctx, state, stm)); mk_stm(StmX::Call { fun: fun.clone(), resolved_method: resolved_method.clone(), is_trait_default: *is_trait_default, mode: *mode, typ_args: typ_args.clone(), args: Arc::new(new_args), split: split.clone(), dest, assert_id: assert_id.clone(), body, }) } StmX::Assert(id, msg, e1) => { let e1 = visit_exp_native(ctx, state, e1); mk_stm(StmX::Assert(id.clone(), msg.clone(), e1)) } StmX::AssertBitVector { requires, ensures } => { let requires = visit_exps_native(ctx, state, requires); let ensures = visit_exps_native(ctx, state, ensures); mk_stm(StmX::AssertBitVector { requires, ensures }) } StmX::AssertQuery { mode, typ_inv_exps, typ_inv_vars, body } => { let body = visit_stm(ctx, state, body); let typ_inv_exps = visit_exps(ctx, state, typ_inv_exps); let typ_inv_vars = typ_inv_vars.iter().map(|(x, _)| (x.clone(), state.types[x].clone())).collect(); mk_stm(StmX::AssertQuery { mode: *mode, typ_inv_exps, typ_inv_vars: Arc::new(typ_inv_vars), body, }) } StmX::AssertCompute(..) => panic!("AssertCompute should be removed by sst_elaborate"), StmX::Assume(e1) => { let e1 = visit_exp_native(ctx, state, e1); mk_stm(StmX::Assume(e1)) } StmX::Assign { lhs, rhs } => { let (e1, rhs) = if let Some(x) = take_temp(state, lhs) { let rhs = visit_exp(ctx, state, rhs); // x needs to be in types before we can visit e1: assert!(!state.temp_types.contains_key(&x)); assert!(!state.types.contains_key(&x)); let _ = state.temp_types.insert(x.clone(), rhs.typ.clone()); let _ = state.types.insert(x, rhs.typ.clone()); let e1 = visit_exp(ctx, state, &lhs.dest); (e1, rhs) } else { let e1 = visit_exp(ctx, state, &lhs.dest); let rhs = if typ_is_poly(ctx, &e1.typ) { visit_exp_poly(ctx, state, rhs) } else { visit_exp_native(ctx, state, rhs) }; (e1, rhs) }; let lhs = Dest { dest: e1, is_init: lhs.is_init }; mk_stm(StmX::Assign { lhs, rhs }) } StmX::Fuel(_, _) => stm.clone(), StmX::RevealString(_) => stm.clone(), StmX::RevealByteString(_) => stm.clone(), StmX::DeadEnd(stm) => { let stm = visit_stm(ctx, state, stm); mk_stm(StmX::DeadEnd(stm)) } StmX::Return { assert_id, base_error, ret_exp, inside_body } => { let ret_exp = if let Some(e1) = ret_exp { let e1 = if state.is_trait && !state.in_exec_closure { visit_exp_poly(ctx, state, e1) } else { visit_exp_native(ctx, state, e1) };
// opaque type has to be poly if state.is_poly_ret_with_opaque { Some(crate::poly::coerce_exp_to_poly(ctx, &e1)) } else { Some(e1) } } else { None };
mk_stm(StmX::Return { assert_id: assert_id.clone(), base_error: base_error.clone(), ret_exp, inside_body: *inside_body, }) } StmX::BreakOrContinue { .. } => stm.clone(), StmX::If(e, s1, s2) => { let e = visit_exp_native(ctx, state, e); let s1 = visit_stm(ctx, state, s1); let s2 = s2.as_ref().map(|s| visit_stm(ctx, state, s)); mk_stm(StmX::If(e, s1, s2)) } StmX::Loop { pre_stms, loop_isolation, is_for_loop, id, label, cond, body, invs, decrease, typ_inv_vars, modified_vars, au_branch_bool, pre_modified_params_excl, pre_modified_params_incl, } => { let pre_stms = visit_stms(ctx, state, pre_stms); let cond = cond .as_ref() .map(|(s, e)| (visit_stm(ctx, state, s), visit_exp_native(ctx, state, e))); let body = visit_stm(ctx, state, body); let invs = invs.iter().map(|inv| crate::sst::LoopInv { inv: visit_exp_native(ctx, state, &inv.inv), ..inv.clone() }); let invs = Arc::new(invs.collect()); let decrease = visit_exps_native(ctx, state, decrease); let au_branch_bool = au_branch_bool.as_ref().map(|e| visit_exp_native(ctx, state, e)); mk_stm(StmX::Loop { pre_stms: pre_stms.clone(), loop_isolation: *loop_isolation, is_for_loop: *is_for_loop, id: *id, label: label.clone(), cond, body, invs, decrease, typ_inv_vars: typ_inv_vars.clone(), modified_vars: modified_vars.clone(), au_branch_bool, pre_modified_params_excl: pre_modified_params_excl.clone(), pre_modified_params_incl: pre_modified_params_incl.clone(), }) } StmX::OpenInvariant(s) => { let s = visit_stm(ctx, state, s); mk_stm(StmX::OpenInvariant(s)) } StmX::ClosureInner { body, typ_inv_vars } => { let typ_inv_vars = Arc::new( typ_inv_vars .iter() .map(|(uid, typ)| (uid.clone(), coerce_typ_to_native(ctx, typ))) .collect::<Vec<_>>(), );
state.types.push_scope(true); for (name, typ) in typ_inv_vars.iter() { let _ = state.types.insert(name.clone(), typ.clone()); } let body = visit_stm(ctx, state, body); state.types.pop_scope(); mk_stm(StmX::ClosureInner { body, typ_inv_vars: typ_inv_vars }) } StmX::Air(_) => stm.clone(), StmX::Block(stms) => mk_stm(StmX::Block(visit_stms(ctx, state, stms))), }}
fn visit_stms(ctx: &Ctx, state: &mut State, stms: &Stms) -> Stms { let mut ss: Vec<Stm> = Vec::new(); for s in stms.iter() { ss.push(visit_stm(ctx, state, s)); } Arc::new(ss)}
fn visit_func_decl_sst( ctx: &Ctx, state: &mut State, poly_pars: &InsertPars, function: &FuncDeclSst,) -> FuncDeclSst { let FuncDeclSst { req_inv_pars, ens_pars, reqs, enss: (enss0, enss1), inv_masks, unwind_condition, fndef_axioms, } = function;
state.types.push_scope(true); let req_inv_pars = visit_and_insert_pars(ctx, &mut state.types, poly_pars, req_inv_pars); let reqs = visit_exps_native(ctx, state, reqs); let inv_masks = Arc::new(inv_masks.iter().map(|es| visit_exps_native(ctx, state, es)).collect()); let unwind_condition = unwind_condition.as_ref().map(|e| visit_exp_native(ctx, state, e)); state.types.pop_scope();
state.types.push_scope(true); let ens_pars = visit_and_insert_pars(ctx, &mut state.types, poly_pars, ens_pars); let enss0 = visit_exps_native(ctx, state, enss0); let enss1 = visit_exps_native(ctx, state, enss1); state.types.pop_scope();
let fndef_axioms = visit_exps_native(ctx, state, fndef_axioms); FuncDeclSst { req_inv_pars, ens_pars, reqs, enss: (enss0, enss1), inv_masks, unwind_condition, fndef_axioms, }}
fn update_temp_locals( state: &mut State, locals: &mut Vec<LocalDecl>, updated_temps: &mut HashSet<VarIdent>,) { for l in locals.iter_mut() { if matches!(l.kind, LocalDeclKind::TempViaAssign) { if !state.remaining_temps.contains(&l.ident) && !updated_temps.contains(&l.ident) { let typ = state.temp_types[&l.ident].clone(); Arc::make_mut(l).typ = typ; updated_temps.insert(l.ident.clone()); } } }}
fn visit_func_check_sst( ctx: &Ctx, state: &mut State, function: &FuncCheckSst, poly_pars: &InsertPars, poly_ret: &InsertPars, ret_typ: &Typ,) -> FuncCheckSst { let FuncCheckSst { reqs, return_opaque_type_eqs, post_condition, unwind, body, local_decls, local_decls_decreases_init, statics, } = function;
state.temp_types.clear();
let reqs = visit_exps_native(ctx, state, reqs);
let unwind = match &unwind { UnwindSst::MayUnwind | UnwindSst::NoUnwind => unwind.clone(), UnwindSst::NoUnwindWhen(e) => { let e = visit_exp_native(ctx, state, e); UnwindSst::NoUnwindWhen(e) } };
state.types.push_scope(true); let mut locals: Vec<LocalDecl> = Vec::new(); for l in local_decls.iter() { let typ = match (l.kind, poly_pars, poly_ret) { (_, InsertPars::NativeFor(..), _) => panic!("unexpected NativeFor"), (_, _, InsertPars::NativeFor(..)) => panic!("unexpected NativeFor"), (LocalDeclKind::Param { .. }, InsertPars::Poly, _) | (LocalDeclKind::Return, _, InsertPars::Poly) | (LocalDeclKind::StmCallArg { native: false }, _, _) | (LocalDeclKind::AssertByVar { native: false }, _, _) | (LocalDeclKind::QuantBinder, _, _) | (LocalDeclKind::ChooseBinder, _, _) | (LocalDeclKind::ClosureBinder, _, _) => coerce_typ_to_poly(ctx, &l.typ), (LocalDeclKind::Param { .. }, InsertPars::Native, _) | (LocalDeclKind::Return, _, InsertPars::Native) | (LocalDeclKind::StmtLet { .. }, _, _) | (LocalDeclKind::StmCallArg { native: true }, _, _) | (LocalDeclKind::Assert, _, _) | (LocalDeclKind::AssertByVar { native: true }, _, _) | (LocalDeclKind::LetBinder, _, _) | (LocalDeclKind::OpenInvariantInnerTemp, _, _) | (LocalDeclKind::ExecClosureId, _, _) | (LocalDeclKind::ExecClosureParam { .. }, _, _) | (LocalDeclKind::Nondeterministic, _, _) | (LocalDeclKind::BorrowMut, _, _) | (LocalDeclKind::ExecClosureRet, _, _) | (LocalDeclKind::LoopBreakValue, _, _) | (LocalDeclKind::Decreases, _, _) => coerce_typ_to_native(ctx, &l.typ), (LocalDeclKind::TempViaAssign, _, _) => l.typ.clone(), }; match l.kind { LocalDeclKind::TempViaAssign => { state.remaining_temps.insert(l.ident.clone()); } _ => { let _ = state.types.insert(l.ident.clone(), typ.clone()); } } let l = Arc::new(crate::sst::LocalDeclX { ident: l.ident.clone(), typ, kind: l.kind }); locals.push(l); }
let mut updated_temps: HashSet<VarIdent> = HashSet::new();
state.types.push_scope(true); if let Some(ret) = &post_condition.dest { let _ = state.types.insert(ret.clone(), ret_typ.clone()); } let post_condition = Arc::new(PostConditionSst { dest: post_condition.dest.clone(), ens_exps: visit_exps_native(ctx, state, &post_condition.ens_exps), ens_spec_precondition_stms: visit_stms( ctx, state, &post_condition.ens_spec_precondition_stms, ), kind: post_condition.kind, }); state.types.pop_scope();
let body = visit_stm(ctx, state, body);
let local_decls_decreases_init = visit_stms(ctx, state, local_decls_decreases_init);
update_temp_locals(state, &mut locals, &mut updated_temps); state.remaining_temps.clear(); state.types.pop_scope();
FuncCheckSst { reqs, return_opaque_type_eqs: return_opaque_type_eqs.clone(), post_condition, unwind, body, local_decls: Arc::new(locals), local_decls_decreases_init, statics: statics.clone(), }}
fn visit_function(ctx: &Ctx, function: &FunctionSst) -> FunctionSst { let &FunctionSstX { ref name, ref kind, ref body_visibility, ref opaqueness, ref owning_module, mode: mut function_mode, ref typ_params, ref typ_bounds, ref pars, ref outer_ret, ref inner_ret, ref ens_has_return, ref item_kind, ref attrs, ref has, ref decl, ref axioms, ref exec_proof_check, ref recommends_check, ref safe_api_check, ref hidden, } = &function.x;
if attrs.is_decrease_by { // This is actually code for a the spec function that has the decreases clause function_mode = Mode::Spec; }
let types = ScopeMap::new(); let is_trait = !matches!(kind, FunctionKind::Static); let poly_pars = if function_mode == Mode::Spec || is_trait { InsertPars::Poly } else { InsertPars::Native }; let poly_ret = if is_trait && (*ens_has_return || function_mode == Mode::Spec) { InsertPars::Poly } else { InsertPars::Native }; let mut state = State { types, temp_types: HashMap::new(), is_trait, in_exec_closure: false, remaining_temps: HashSet::new(), is_poly_ret_with_opaque: typ_contains_opaque(&inner_ret.x.typ) && typ_is_poly(ctx, &inner_ret.x.typ), };
let decl = Arc::new(visit_func_decl_sst(ctx, &mut state, &poly_pars, decl));
let proof_exec_axioms = if let Some((pars, body, trigs)) = &axioms.proof_exec_axioms { let mut bs: Vec<VarBinder<Typ>> = Vec::new(); for par in pars.iter() { let ParX { name, typ, .. } = &par.x; bs.push(Arc::new(crate::ast::VarBinderX { name: name.clone(), a: typ.clone() })); } let natives = native_quant_vars(&Arc::new(bs), trigs); state.types.push_scope(true); let pars = visit_and_insert_pars(ctx, &mut state.types, &InsertPars::NativeFor(natives), pars); let body = visit_exp_native(ctx, &mut state, body); let trigs = visit_trigs(ctx, &mut state, trigs); state.types.pop_scope(); Some((pars, body, trigs)) } else { None };
// Return type is left native (except for trait methods) let outer_ret_typ = match poly_ret { InsertPars::Poly => coerce_typ_to_poly(ctx, &outer_ret.x.typ), InsertPars::Native => coerce_typ_to_native(ctx, &outer_ret.x.typ), _ => unreachable!(), }; let outer_ret = Spanned::new(outer_ret.span.clone(), ParX { typ: outer_ret_typ, ..outer_ret.x.clone() });
let inner_ret_typ = match poly_ret { InsertPars::Poly => coerce_typ_to_poly(ctx, &inner_ret.x.typ), InsertPars::Native => coerce_typ_to_native(ctx, &inner_ret.x.typ), _ => unreachable!(), }; let inner_ret = Spanned::new(inner_ret.span.clone(), ParX { typ: inner_ret_typ, ..inner_ret.x.clone() });
state.types.push_scope(true); let pars = visit_and_insert_pars(ctx, &mut state.types, &poly_pars, pars);
let spec_axioms = if let Some(spec_body) = &axioms.spec_axioms { let decrease_when = spec_body.decrease_when.as_ref().map(|e| visit_exp_native(ctx, &mut state, e)); let termination_check = spec_body.termination_check.as_ref().map(|f| { visit_func_check_sst(ctx, &mut state, f, &poly_pars, &poly_ret, &inner_ret.x.typ) }); let body_exp = if is_trait && (function.x.ens_has_return || function_mode == Mode::Spec) { visit_exp_poly(ctx, &mut state, &spec_body.body_exp) } else { visit_exp_native(ctx, &mut state, &spec_body.body_exp) }; let spec_body = crate::sst::FuncSpecBodySst { decrease_when, termination_check, body_exp }; Some(spec_body) } else { None }; let axioms = Arc::new(crate::sst::FuncAxiomsSst { spec_axioms, proof_exec_axioms });
let exec_proof_check = exec_proof_check.as_ref().map(|f| { Arc::new(visit_func_check_sst(ctx, &mut state, f, &poly_pars, &poly_ret, &inner_ret.x.typ)) }); let recommends_check = recommends_check.as_ref().map(|f| { Arc::new(visit_func_check_sst(ctx, &mut state, f, &poly_pars, &poly_ret, &inner_ret.x.typ)) }); let safe_api_check = safe_api_check.as_ref().map(|f| { Arc::new(visit_func_check_sst(ctx, &mut state, f, &poly_pars, &poly_ret, &inner_ret.x.typ)) });
state.types.pop_scope(); assert_eq!(state.types.num_scopes(), 0);
let functionx = FunctionSstX { name: name.clone(), kind: kind.clone(), body_visibility: body_visibility.clone(), opaqueness: opaqueness.clone(), owning_module: owning_module.clone(), mode: function_mode, typ_params: typ_params.clone(), typ_bounds: typ_bounds.clone(), pars, outer_ret, inner_ret: inner_ret.clone(), ens_has_return: *ens_has_return, item_kind: *item_kind, attrs: attrs.clone(), has: has.clone(), decl, axioms, exec_proof_check, recommends_check, safe_api_check, hidden: hidden.clone(), }; Spanned::new(function.span.clone(), functionx)}
fn visit_datatype(ctx: &Ctx, datatype: &Datatype) -> Datatype { let variants = vec_map(&*datatype.x.variants, |v| Variant { fields: Arc::new(vec_map(&v.fields, |f| { f.map_a(|(t, m, v)| (coerce_typ_to_native(ctx, t), *m, v.clone())) })), ..v.clone() }); let variants = Arc::new(variants); let datatypex = DatatypeX { variants, ..datatype.x.clone() }; Spanned::new(datatype.span.clone(), datatypex)}
fn visit_assoc_type_impl(ctx: &Ctx, assoc: &AssocTypeImpl) -> AssocTypeImpl { crate::ast_visitor::map_assoc_type_impl_visitor_env(assoc, &mut (), &|(), t| { Ok(coerce_typ_to_poly(ctx, t)) }) .expect("visit_assoc_type_impl")}
pub fn poly_krate_for_module(ctx: &mut Ctx, krate: &KrateSst) -> KrateSst { let KrateSstX { functions, datatypes, opaque_types, traits, trait_impls, assoc_type_impls, reveal_groups, } = &**krate; let kratex = KrateSstX { functions: functions.iter().map(|f| visit_function(ctx, f)).collect(), datatypes: datatypes.iter().map(|d| visit_datatype(ctx, d)).collect(), opaque_types: opaque_types.clone(), traits: traits.clone(), trait_impls: trait_impls.clone(), assoc_type_impls: assoc_type_impls.iter().map(|a| visit_assoc_type_impl(ctx, a)).collect(), reveal_groups: reveal_groups.clone(), }; ctx.func_sst_map = HashMap::new(); for function in kratex.functions.iter() { ctx.func_sst_map.insert(function.x.name.clone(), function.clone()); } ctx.datatype_map = HashMap::new(); for datatype in kratex.datatypes.iter() { ctx.datatype_map.insert(datatype.x.name.clone(), datatype.clone()); } Arc::new(kratex)}