Struct move_model::spec_translator::TranslatedSpec

pub struct TranslatedSpec {
    pub saved_memory: BTreeMap<QualifiedInstId<StructId>, MemoryLabel>,
    pub saved_spec_vars: BTreeMap<QualifiedInstId<SpecVarId>, MemoryLabel>,
    pub saved_params: BTreeMap<TempIndex, TempIndex>,
    pub debug_traces: Vec<(NodeId, Exp)>,
    pub pre: Vec<(Loc, Exp)>,
    pub post: Vec<(Loc, Exp)>,
    pub aborts: Vec<(Loc, Exp, Option<Exp>)>,
    pub aborts_with: Vec<(Loc, Vec<Exp>)>,
    pub emits: Vec<(Loc, Exp, Exp, Option<Exp>)>,
    pub modifies: Vec<(Loc, Exp)>,
    pub invariants: Vec<(Loc, GlobalId, Exp)>,
    pub lets: Vec<(Loc, bool, TempIndex, Exp)>,
}

Represents a translated spec.

Fields

saved_memory: BTreeMap<QualifiedInstId<StructId>, MemoryLabel>

saved_spec_vars: BTreeMap<QualifiedInstId<SpecVarId>, MemoryLabel>

saved_params: BTreeMap<TempIndex, TempIndex>

debug_traces: Vec<(NodeId, Exp)>

pre: Vec<(Loc, Exp)>

post: Vec<(Loc, Exp)>

aborts: Vec<(Loc, Exp, Option<Exp>)>

aborts_with: Vec<(Loc, Vec<Exp>)>

emits: Vec<(Loc, Exp, Exp, Option<Exp>)>

modifies: Vec<(Loc, Exp)>

invariants: Vec<(Loc, GlobalId, Exp)>

lets: Vec<(Loc, bool, TempIndex, Exp)>

Implementations

impl TranslatedSpec

pub fn aborts_condition<'a, T: ExpGenerator<'a>>( &self, builder: &T ) -> Option<Exp>

Creates a boolean expression which describes the overall abort condition. This is a disjunction of the individual abort conditions.

pub fn aborts_code_condition<'a, T: ExpGenerator<'a>>( &self, builder: &T, actual_code: &Exp ) -> Option<Exp>

Creates a boolean expression which describes the overall condition which constraints the abort code.

Let (P1, C1)..(Pj, Cj) be aborts_if with a code, Pk..Pl aborts_if without a code, and the Cm..Cn standalone aborts codes from an aborts_with:

 P1 && abort_code == C1 || .. || Pj && abort_code == Cj
     || Pk || .. || Pl
     || abort_code == Cm || .. || abort_code == Cn

This characterizes the allowed value of the code. In the presence of aborts_if with code, whenever the aborts condition is true, the code must also be the specified ones. Notice that still allows any other member of the disjunction to make the overall condition true. Specifically, if someone specifies aborts_if P with C1; aborts_with C2, then even if P is true, C2 is allowed as an abort code.

pub fn has_aborts_code_specs(&self) -> bool

Returns true if there are any specs about the abort code.

pub fn pre_conditions<'a, T: ExpGenerator<'a>>( &self, _builder: &T ) -> impl Iterator<Item = (Loc, Exp)> + '_

Return an iterator of effective pre conditions.

pub fn emits_conditions<'a, T: ExpGenerator<'a>>( &self, builder: &T ) -> Vec<(Loc, Exp)>

Returns a sequence of EventStoreIncludes expressions which verify the emits clauses of a function spec. While logically we could generate a single EventStoreIncludes, for better error reporting we construct incrementally multiple EventStoreIncludes expressions with some redundancy for each individual `emits, so we the see the exact failure at the right emit condition.

pub fn emits_completeness_condition<'a, T: ExpGenerator<'a>>( &self, builder: &T ) -> Exp

Trait Implementations

impl Default for TranslatedSpec

fn default() -> TranslatedSpec

Returns the “default value” for a type.