Struct ExprEncodingCtxt 

pub struct ExprEncodingCtxt<'genv, 'tcx> {
    genv: GlobalEnv<'genv, 'tcx>,
    local_var_env: LocalVarEnv,
    const_env: ConstEnv<'tcx>,
    errors: Errors<'genv>,
    def_id: Option<MaybeExternId>,
    infcx: InferCtxt<'tcx>,
}

Fields

genv: GlobalEnv<'genv, 'tcx>

local_var_env: LocalVarEnv

const_env: ConstEnv<'tcx>

errors: Errors<'genv>

def_id: Option<MaybeExternId>

Id of the item being checked. This is a MaybeExternId because we may be encoding invariants for an extern spec on an enum.

infcx: InferCtxt<'tcx>

Implementations

impl<'genv, 'tcx> ExprEncodingCtxt<'genv, 'tcx>

pub fn new(genv: GlobalEnv<'genv, 'tcx>, def_id: Option<MaybeExternId>) -> Self

fn def_span(&self) -> Span

fn var_to_fixpoint(&self, var: &Var) -> Var

fn variant_to_fixpoint( &self, scx: &mut SortEncodingCtxt, enum_def_id: &DefId, idx: VariantIdx, ) -> Var

fn struct_fields_to_fixpoint( &mut self, did: &DefId, flds: &[Expr], scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

fn fields_to_fixpoint( &mut self, flds: &[Expr], scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

fn internal_func_to_fixpoint( &mut self, internal_func: &InternalFuncKind, sort_args: &[SortArg], args: &[Expr], scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

fn structurally_normalize_expr(&self, expr: &Expr) -> QueryResult<Expr>

fn expr_to_fixpoint( &mut self, expr: &Expr, scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

fn exprs_to_fixpoint<'b>( &mut self, exprs: impl IntoIterator<Item = &'b Expr>, scx: &mut SortEncodingCtxt, ) -> QueryResult<Vec<Expr>>

fn proj_to_fixpoint( &mut self, e: &Expr, proj: FieldProj, scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

fn un_op_to_fixpoint( &mut self, op: UnOp, e: &Expr, scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

fn bv_rel_to_fixpoint(&self, rel: &BinRel) -> Expr

fn bv_op_to_fixpoint(&self, op: &BinOp) -> Expr

fn bin_op_to_fixpoint( &mut self, op: &BinOp, e1: &Expr, e2: &Expr, scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

fn bin_rel_to_fixpoint( &mut self, sort: &Sort, rel: BinRel, e1: &Expr, e2: &Expr, scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

A binary relation is encoded as a structurally recursive relation between aggregate sorts. For “leaf” expressions, we encode them as an interpreted relation if the sort supports it, otherwise we use an uninterpreted function. For example, consider the following relation between two tuples of sort (int, int -> int)

(0, λv. v + 1) <= (1, λv. v + 1)

The encoding in fixpoint will be

0 <= 1 && (le (λv. v + 1) (λv. v + 1))

Where <= is the (interpreted) less than or equal relation between integers and le is an uninterpreted relation between (the encoding of) lambdas.

fn apply_bin_rel_rec( &mut self, sorts: &[Sort], rel: BinRel, e1: &Expr, e2: &Expr, scx: &mut SortEncodingCtxt, mk_proj: impl Fn(u32) -> FieldProj, ) -> QueryResult<Expr>

Apply binary relation recursively over aggregate expressions

fn imm( &mut self, arg: &Expr, sort: &Sort, scx: &mut SortEncodingCtxt, bindings: &mut Vec<Bind>, ) -> QueryResult<Var>

pub fn declare_fun(&mut self, def_id: FluxDefId) -> Var

Declare that the def_id of a Flux function definition needs to be encoded and assigns a name to it if it hasn’t yet been declared. The encoding of the function body happens in Self::define_funs.

fn prim_op_sort(op: &BinOp, span: Span) -> PolyFuncSort

The logic below is a bit “duplicated” with the [prim_op_sort`] in sortck.rs; They are not exactly the same because this is on rty and the other one on fhir. We should make sure these two remain in sync.

(NOTE:PrimOpSort) We are somewhat “overloading” the BinOps: as we are using them for (a) interpreted operations on bit vectors AND (b) uninterpreted functions on integers. So when Binop::BitShr (a) appears in a ExprKind::BinOp, it means bit vectors, but (b) inside ExprKind::InternalFunc it means int.

fn define_const_for_cast( &mut self, from: &Sort, to: &Sort, scx: &mut SortEncodingCtxt, ) -> Var

fn define_const_for_prim_op( &mut self, op: &BinOp, scx: &mut SortEncodingCtxt, ) -> Var

fn define_const_for_uif( &mut self, def_id: FluxDefId, scx: &mut SortEncodingCtxt, ) -> Var

fn define_const_for_rust_const( &mut self, def_id: DefId, scx: &mut SortEncodingCtxt, ) -> Var

fn define_const_for_alias_reft( &mut self, alias_reft: &AliasReft, fsort: FuncSort, scx: &mut SortEncodingCtxt, ) -> Var

returns the ‘constant’ UIF for Var used to represent the alias_pred, creating and adding it to the const_map if necessary

fn define_const_for_lambda( &mut self, lam: &Lambda, scx: &mut SortEncodingCtxt, ) -> Var

We encode lambdas with uninterpreted constant. Two syntactically equal lambdas will be encoded with the same constant.

fn assume_const_values( &mut self, constraint: Constraint, scx: &mut SortEncodingCtxt, ) -> QueryResult<Constraint>

fn qualifiers_for( &mut self, def_id: LocalDefId, scx: &mut SortEncodingCtxt, ) -> QueryResult<Vec<Qualifier>>

fn define_funs( &mut self, def_id: MaybeExternId, scx: &mut SortEncodingCtxt, ) -> QueryResult<(Vec<FunDef>, Vec<ConstDecl>)>

pub fn fun_decl_to_fixpoint( &mut self, def_id: FluxDefId, scx: &mut SortEncodingCtxt, ) -> ConstDecl

pub fn fun_def_to_fixpoint( &mut self, def_id: FluxDefId, scx: &mut SortEncodingCtxt, ) -> QueryResult<FunDef>

fn body_to_fixpoint( &mut self, body: &Binder<Expr>, scx: &mut SortEncodingCtxt, ) -> QueryResult<(Vec<(Var, Sort)>, Expr)>

fn qualifier_to_fixpoint( &mut self, qualifier: &Qualifier, scx: &mut SortEncodingCtxt, ) -> QueryResult<Qualifier>