Struct bytecode::function_data_builder::FunctionDataBuilder

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

A builder for FunctionData.

Fields

fun_env: &'env FunctionEnv<'env>

data: FunctionData

options: FunctionDataBuilderOptions

Implementations

impl<'env> FunctionDataBuilder<'env>

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

Creates a new builder with customized options

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

Creates a new builder with options set to default values

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.

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

Add a return parameter.

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.

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

Sets the default location from a code attribute id.

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

Gets the location from the bytecode attribute.

pub fn new_attr(&mut self) -> AttrId

Creates a new bytecode attribute id with default location.

pub fn new_label(&mut self) -> Label

Creates a new branching label for bytecode.

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

Emits a bytecode.

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

Emits a sequence of bytecodes.

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.

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| ..).

pub fn clear_next_debug_comment(&mut self)

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

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.

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

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

Trait Implementations

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

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

Get the functional environment

fn get_current_loc(&self) -> Loc

Get the current location

fn set_loc(&mut self, loc: Loc)

Set the current location

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

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

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.