pub struct FunctionDataBuilder<'env> {
    pub fun_env: &'env FunctionEnv<'env>,
    pub data: FunctionData,
    pub options: FunctionDataBuilderOptions,
    /* private fields */
}
Expand description

A builder for FunctionData.

Fields§

§fun_env: &'env FunctionEnv<'env>§data: FunctionData§options: FunctionDataBuilderOptions

Implementations§

source§

impl<'env> FunctionDataBuilder<'env>

source

pub fn new_with_options( fun_env: &'env FunctionEnv<'env>, data: FunctionData, options: FunctionDataBuilderOptions ) -> Self

Creates a new builder with customized options

source

pub fn new(fun_env: &'env FunctionEnv<'env>, data: FunctionData) -> Self

Creates a new builder with options set to default values

source

pub fn get_target(&self) -> FunctionTarget<'_>

Gets a function target viewpoint on this builder. This locks the data for mutation until the returned value dies.

source

pub fn add_return(&mut self, ty: Type) -> usize

Add a return parameter.

source

pub fn set_loc_and_vc_info(&mut self, loc: Loc, message: &str)

Sets the default location as well as information about the verification condition message associated with the next instruction generated with emit_with.

source

pub fn set_loc_from_attr(&mut self, attr_id: AttrId)

Sets the default location from a code attribute id.

source

pub fn get_loc(&self, attr_id: AttrId) -> Loc

Gets the location from the bytecode attribute.

source

pub fn new_attr(&mut self) -> AttrId

Creates a new bytecode attribute id with default location.

source

pub fn new_label(&mut self) -> Label

Creates a new branching label for bytecode.

source

pub fn emit(&mut self, bc: Bytecode)

Emits a bytecode.

source

pub fn emit_vec(&mut self, bcs: Vec<Bytecode>)

Emits a sequence of bytecodes.

source

pub fn emit_with<F>(&mut self, f: F)where F: FnOnce(AttrId) -> Bytecode,

Emits a bytecode via a function which takes a freshly generated attribute id.

source

pub fn set_next_debug_comment(&mut self, comment: String)

Sets the debug comment which should be associated with the next instruction emitted with self.emit_with(|id| ..).

source

pub fn clear_next_debug_comment(&mut self)

This will clear the state that the next self.emit_with(..) will add a debug comment.

source

pub fn emit_let(&mut self, def: Exp) -> (TempIndex, Exp)

Emits a let: this creates a new temporary and emits an assumption that this temporary is equal to the given expression. This can be used to abbreviate large expressions which are used multiple times, or get the value of an expression into a temporary for bytecode. Returns the temporary and a local expression referring to it.

source

pub fn emit_let_havoc(&mut self, ty: Type) -> (TempIndex, Exp)

Emits a new temporary with a havoced value of given type.

Trait Implementations§

source§

impl<'env> ExpGenerator<'env> for FunctionDataBuilder<'env>

source§

fn function_env(&self) -> &FunctionEnv<'env>

Get the functional environment
source§

fn get_current_loc(&self) -> Loc

Get the current location
source§

fn set_loc(&mut self, loc: Loc)

Set the current location
source§

fn add_local(&mut self, ty: Type) -> TempIndex

Add a local variable with given type, return the local index.
source§

fn get_local_type(&self, temp: TempIndex) -> Type

Get the type of a local given at temp index
§

fn global_env(&self) -> &'env GlobalEnv

Get the global environment
§

fn set_loc_from_node(&mut self, node_id: NodeId)

Sets the default location from a node id.
§

fn new_node(&self, ty: Type, inst_opt: Option<Vec<Type, Global>>) -> NodeId

Creates a new expression node id, using current default location, provided type, and optional instantiation.
§

fn new_temp(&mut self, ty: Type) -> usize

Allocates a new temporary.
§

fn mk_bool_const(&self, value: bool) -> Exp

Make a boolean constant expression.
§

fn mk_call(&self, ty: &Type, oper: Operation, args: Vec<Exp, Global>) -> Exp

Makes a Call expression.
§

fn mk_call_with_inst( &self, ty: &Type, inst: Vec<Type, Global>, oper: Operation, args: Vec<Exp, Global> ) -> Exp

Makes a Call expression with type instantiation.
§

fn mk_ite(&self, cond: ExpData, if_true: ExpData, if_false: ExpData) -> Exp

Makes an if-then-else expression.
§

fn mk_bool_call(&self, oper: Operation, args: Vec<Exp, Global>) -> Exp

Makes a Call expression with boolean result type.
§

fn mk_not(&self, arg: Exp) -> Exp

Make a boolean not expression.
§

fn mk_eq(&self, arg1: Exp, arg2: Exp) -> Exp

Make an equality expression.
§

fn mk_identical(&self, arg1: Exp, arg2: Exp) -> Exp

Make an identical equality expression. This is stronger than make_equal because it requires the exact same representation, not only interpretation.
§

fn mk_and(&self, arg1: Exp, arg2: Exp) -> Exp

Make an and expression.
§

fn mk_or(&self, arg1: Exp, arg2: Exp) -> Exp

Make an or expression.
§

fn mk_implies(&self, arg1: Exp, arg2: Exp) -> Exp

Make an implies expression.
§

fn mk_iff(&self, arg1: Exp, arg2: Exp) -> Exp

Make an iff expression.
§

fn mk_builtin_num_const(&self, oper: Operation) -> Exp

Make a numerical expression for some of the builtin constants.
§

fn mk_join_bool( &self, oper: Operation, args: impl Iterator<Item = Exp> ) -> Option<Exp>

Join an iterator of boolean expressions with a boolean binary operator.
§

fn mk_join_opt_bool( &self, oper: Operation, arg1: Option<Exp>, arg2: Option<Exp> ) -> Option<Exp>

Join two boolean optional expression with binary operator.
§

fn mk_vector_quant_opt<F>( &self, kind: QuantKind, vector: Exp, elem_ty: &Type, f: &mut F ) -> Option<Exp>where F: FnMut(Exp) -> Option<Exp>,

Creates a quantifier over the content of a vector. The passed function f receives an expression representing an element of the vector and returns the quantifiers predicate; if it returns None, this function will also return None, otherwise the quantifier will be returned.
§

fn mk_mem_quant_opt<F>( &self, kind: QuantKind, mem: QualifiedId<StructId>, f: &mut F ) -> Option<ExpData>where F: FnMut(Exp) -> Option<Exp>,

Creates a quantifier over the content of memory. The passed function f receives
§

fn mk_inst_mem_quant_opt<F>( &self, kind: QuantKind, mem: &QualifiedInstId<StructId>, f: &mut F ) -> Option<Exp>where F: FnMut(Exp) -> Option<Exp>,

Creates a quantifier over the content of instantiated memory. The passed function f receives an expression representing a value in memory and returns the quantifiers predicate;
§

fn mk_decl(&self, name: Symbol, ty: Type, binding: Option<Exp>) -> LocalVarDecl

Makes a local variable declaration.
§

fn mk_symbol(&self, str: &str) -> Symbol

Makes a symbol from a string.
§

fn mk_type_domain(&self, ty: Type) -> Exp

Makes a type domain expression.
§

fn mk_field_select( &self, field_env: &FieldEnv<'_>, targs: &[Type], exp: Exp ) -> Exp

Makes an expression which selects a field from a struct.
§

fn mk_temporary(&self, temp: usize) -> Exp

Makes an expression for a temporary.
§

fn mk_local(&self, name: &str, ty: Type) -> Exp

Makes an expression for a named local.
§

fn get_memory_of_node(&self, node_id: NodeId) -> QualifiedInstId<StructId>

Get’s the memory associated with a Call(Global,..) or Call(Exists, ..) node. Crashes if the the node is not typed as expected.

Auto Trait Implementations§

§

impl<'env> !RefUnwindSafe for FunctionDataBuilder<'env>

§

impl<'env> !Send for FunctionDataBuilder<'env>

§

impl<'env> !Sync for FunctionDataBuilder<'env>

§

impl<'env> Unpin for FunctionDataBuilder<'env>

§

impl<'env> !UnwindSafe for FunctionDataBuilder<'env>

Blanket Implementations§

source§

impl<T> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

const: unstable · source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for Twhere T: ?Sized,

const: unstable · source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<T> From<T> for T

const: unstable · source§

fn from(t: T) -> T

Returns the argument unchanged.

source§

impl<T, U> Into<U> for Twhere U: From<T>,

const: unstable · source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T> Same<T> for T

§

type Output = T

Should always be Self
source§

impl<T, U> TryFrom<U> for Twhere U: Into<T>,

§

type Error = Infallible

The type returned in the event of a conversion error.
const: unstable · source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for Twhere U: TryFrom<T>,

§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
const: unstable · source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<V, T> VZip<V> for Twhere V: MultiLane<T>,

§

fn vzip(self) -> V