Enum move_model::ast::ExpData

pub enum ExpData {
    Invalid(NodeId),
    Value(NodeId, Value),
    LocalVar(NodeId, Symbol),
    Temporary(NodeId, TempIndex),
    Call(NodeId, Operation, Vec<Exp>),
    Invoke(NodeId, Exp, Vec<Exp>),
    Lambda(NodeId, Vec<LocalVarDecl>, Exp),
    Quant(NodeId, QuantKind, Vec<(LocalVarDecl, Exp)>, Vec<Vec<Exp>>, Option<Exp>, Exp),
    Block(NodeId, Vec<LocalVarDecl>, Exp),
    IfElse(NodeId, Exp, Exp, Exp),
}

The type of expression data.

Expression layout follows the following design principles:

• We try to keep the number of expression variants minimal, for easier treatment in generic traversals. Builtin and user functions are abstracted into a general Call(.., operation, args) construct.
• Each expression has a unique node id assigned. This id allows to build attribute tables for additional information, like expression type and source location. The id is globally unique.

Variants

Invalid(NodeId)

Represents an invalid expression. This is used as a stub for algorithms which generate expressions but can fail with multiple errors, like a translator from some other source into expressions. Consumers of expressions should assume this variant is not present and can panic when seeing it.

Value(NodeId, Value)

Represents a value.

LocalVar(NodeId, Symbol)

Represents a reference to a local variable introduced by a specification construct, e.g. a quantifier.

Temporary(NodeId, TempIndex)

Represents a reference to a temporary used in bytecode.

Call(NodeId, Operation, Vec<Exp>)

Represents a call to an operation. The Operation enum covers all builtin functions (including operators, constants, …) as well as user functions.

Invoke(NodeId, Exp, Vec<Exp>)

Represents an invocation of a function value, as a lambda.

Lambda(NodeId, Vec<LocalVarDecl>, Exp)

Represents a lambda.

Quant(NodeId, QuantKind, Vec<(LocalVarDecl, Exp)>, Vec<Vec<Exp>>, Option<Exp>, Exp)

Tuple Fields

0: NodeId

1: QuantKind

2: Vec<(LocalVarDecl, Exp)>

Ranges

3: Vec<Vec<Exp>>

Triggers

4: Option<Exp>

Optional where clause

5: Exp

Body

Represents a quantified formula over multiple variables and ranges.

Block(NodeId, Vec<LocalVarDecl>, Exp)

Represents a block which contains a set of variable bindings and an expression for which those are defined.

IfElse(NodeId, Exp, Exp, Exp)

Represents a conditional.

Implementations

impl ExpData

pub fn into_exp(self) -> Exp

Version of into which does not require type annotations.

pub fn ptr_eq(e1: &Exp, e2: &Exp) -> bool

pub fn node_id(&self) -> NodeId

pub fn call_args(&self) -> &[Exp]

pub fn node_ids(&self) -> Vec<NodeId>

pub fn free_vars(&self, env: &GlobalEnv) -> Vec<(Symbol, Type)>

Returns the free local variables, inclusive their types, used in this expression. Result is ordered by occurrence.

pub fn used_memory(
    &self,
    env: &GlobalEnv
) -> BTreeSet<(QualifiedInstId<StructId>, Option<MemoryLabel>)>

Returns the used memory of this expression.

pub fn used_temporaries(&self, env: &GlobalEnv) -> Vec<(TempIndex, Type)>

Returns the temporaries used in this expression. Result is ordered by occurrence.

pub fn visit<F>(&self, visitor: &mut F) where
    F: FnMut(&ExpData), 

Visits expression, calling visitor on each sub-expression, depth first.

pub fn any<P>(&self, predicate: &mut P) -> bool where
    P: FnMut(&ExpData) -> bool, 

pub fn visit_pre_post<F>(&self, visitor: &mut F) where
    F: FnMut(bool, &ExpData), 

Visits expression, calling visitor on each sub-expression. visitor(false, ..) will be called before descending into expression, and visitor(true, ..) after. Notice we use one function instead of two so a lambda can be passed which encapsulates mutable references.

pub fn rewrite<F>(exp: Exp, exp_rewriter: &mut F) -> Exp where
    F: FnMut(Exp) -> Result<Exp, Exp>, 

Rewrites this expression and sub-expression based on the rewriter function. The function returns Ok(e) if the expression is rewritten, and passes back ownership using Err(e) if the expression stays unchanged. This function stops traversing on Ok(e) and descents into sub-expressions on Err(e).

pub fn rewrite_node_id<F>(exp: Exp, node_rewriter: &mut F) -> Exp where
    F: FnMut(NodeId) -> Option<NodeId>, 

Rewrites the node ids in the expression. This is used to rewrite types of expressions.

pub fn rewrite_exp_and_node_id<F, G>(
    exp: Exp,
    exp_rewriter: &mut F,
    node_rewriter: &mut G
) -> Exp where
    F: FnMut(Exp) -> Result<Exp, Exp>,
    G: FnMut(NodeId) -> Option<NodeId>, 

Rewrites the expression and for unchanged sub-expressions, the node ids in the expression

pub fn instantiate_node(
    env: &GlobalEnv,
    id: NodeId,
    targs: &[Type]
) -> Option<NodeId>

A function which can be used for Exp::rewrite_node_id to instantiate types in an expression based on a type parameter instantiation.

pub fn module_usage(&self, usage: &mut BTreeSet<ModuleId>)

Returns the set of module ids used by this expression.

pub fn extract_ghost_mem_access(
    &self,
    env: &GlobalEnv
) -> Option<(QualifiedInstId<StructId>, FieldId, Exp)>

Extract access to ghost memory from expression. Returns a tuple of the instantiated struct, the field of the selected value, and the expression with the address of the access.

pub fn struct_usage(&self, usage: &mut BTreeSet<QualifiedId<StructId>>)

Collect struct-related operations

pub fn field_usage(
    &self,
    usage: &mut BTreeSet<(QualifiedId<StructId>, FieldId)>
)

Collect field-related operations

pub fn vector_usage(&self, usage: &mut HashSet<Operation>)

Collect vector-related operations

impl ExpData

pub fn uses_memory<F>(&self, check_pure: &F) -> bool where
    F: Fn(ModuleId, SpecFunId) -> bool, 

Determines whether this expression depends on global memory

impl ExpData

pub fn is_pure(&self, env: &GlobalEnv) -> bool

Checks whether the expression is pure, i.e. does not depend on memory or mutable variables.

impl ExpData

pub fn display<'a>(&'a self, env: &'a GlobalEnv) -> ExpDisplay<'a>

Creates a display of an expression which can be used in formatting.

Trait Implementations

impl AsRef<ExpData> for Exp

fn as_ref(&self) -> &ExpData

Converts this type into a shared reference of the (usually inferred) input type.

impl Borrow<ExpData> for Exp

fn borrow(&self) -> &ExpData

Immutably borrows from an owned value.

impl Clone for ExpData

fn clone(&self) -> ExpData

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ExpData

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl From<Exp> for ExpData

fn from(exp: Exp) -> ExpData

Takes an expression and returns expression data.

impl From<ExpData> for Exp

fn from(data: ExpData) -> Self

Converts to this type from the input type.

impl Hash for ExpData

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given Hasher.

impl PartialEq<ExpData> for ExpData

fn eq(&self, other: &ExpData) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &ExpData) -> bool

This method tests for !=.

impl Eq for ExpData

impl StructuralEq for ExpData

impl StructuralPartialEq for ExpData