Enum Body 

pub enum Body {
    Unstructured(ExprBody),
    Structured(ExprBody),
    TargetDispatch(SeqHashMap<TargetTriple, FunDeclRef>),
    Extern(String),
    Intrinsic {
        name: String,
        arg_names: Vec<Option<String>>,
    },
    Opaque,
    Missing,
    Error(Error),
}

The body of a function.

A normal function has a body that’s either structured or unstructured. These are two equivalent representations of the same function body, which only differ in how control-flow is represented. By default bodies are structured; passing --ullbc to Charon makes bodies unstructured.

Besides these, some functions have virtual bodies or no body, see the doc for each variant.

Variants

Unstructured(ExprBody)

Body represented as a control-flow graph (CFG), i.e. with numbered blocks and jumps/GOTOs between them. This is available when passing --ullbc to Charon.

This is also the same structure as rustc’s MIR, and is in fact a direct translation of it.

Structured(ExprBody)

Body represented with structured control flow, i.e. with nested if/match/loop blocks. This is available when --ullbc is not passed to Charon.

This structure is recovered from the unstructured body in the ullbc_to_llbc pass.

TargetDispatch(SeqHashMap<TargetTriple, FunDeclRef>)

A façade body that dispatches to one of several per-target function bodies. This is created during multi-target merging (using --target) to represent functions that have a different implementation across targets.

Extern(String)

Function declared in an extern { ... } block. The string is the foreign symbol name.

Intrinsic

Rust intrinsic function. This has no body and describes a “built-in” operation that must be handled by the codegen backend.

Fields

name: String

The intrinsic name.

arg_names: Vec<Option<String>>

The argument names, None if not available.

Opaque

A body that the user chose not to translate, based on opacity settings like --include/--opaque.

Missing

A body that was not available.

These can occur when using a sysroot that doesn’t have MIR for all the standard library functions. This is the case of the sysroot that ships with every Rust toolchain, but Charon uses a custom-built sysroot that does. So this shouldn’t happen unless you’re passing --sysroot to charon.

Error(Error)

We encountered an error while translating this body.

Implementations

impl Body

pub fn is_unstructured(&self) -> bool

pub fn is_structured(&self) -> bool

pub fn is_target_dispatch(&self) -> bool

pub fn is_extern(&self) -> bool

pub fn is_intrinsic(&self) -> bool

pub fn is_opaque(&self) -> bool

pub fn is_missing(&self) -> bool

pub fn is_error(&self) -> bool

impl Body

pub fn as_unstructured(&self) -> Option<&ExprBody>

pub fn as_structured(&self) -> Option<&ExprBody>

pub fn as_target_dispatch( &self, ) -> Option<&SeqHashMap<TargetTriple, FunDeclRef>>

pub fn as_extern(&self) -> Option<&String>

pub fn as_intrinsic(&self) -> Option<(&String, &Vec<Option<String>>)>

pub fn as_opaque(&self) -> Option<()>

pub fn as_missing(&self) -> Option<()>

pub fn as_error(&self) -> Option<&Error>

impl Body

pub fn as_unstructured_mut(&mut self) -> Option<&mut ExprBody>

pub fn as_structured_mut(&mut self) -> Option<&mut ExprBody>

pub fn as_target_dispatch_mut( &mut self, ) -> Option<&mut SeqHashMap<TargetTriple, FunDeclRef>>

pub fn as_extern_mut(&mut self) -> Option<&mut String>

pub fn as_intrinsic_mut( &mut self, ) -> Option<(&mut String, &mut Vec<Option<String>>)>

pub fn as_opaque_mut(&mut self) -> Option<()>

pub fn as_missing_mut(&mut self) -> Option<()>

pub fn as_error_mut(&mut self) -> Option<&mut Error>

impl Body

pub fn to_unstructured(self) -> Option<ExprBody>

pub fn to_structured(self) -> Option<ExprBody>

pub fn to_target_dispatch(self) -> Option<SeqHashMap<TargetTriple, FunDeclRef>>

pub fn to_extern(self) -> Option<String>

pub fn to_intrinsic(self) -> Option<(String, Vec<Option<String>>)>

pub fn to_opaque(self) -> Option<()>

pub fn to_missing(self) -> Option<()>

pub fn to_error(self) -> Option<Error>

impl Body

pub fn has_contents(&self) -> bool

Whether there is an actual body with statements etc, as opposed to the body being missing for some reason.

pub fn locals(&self) -> &Locals

Trait Implementations

impl AstVisitable for Body

fn drive<V: VisitAst>(&self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn drive_mut<V: VisitAstMut>(&mut self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn drive_two<V: ZipAst>(&self, other: &Self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn name(&self) -> &'static str

The name of the type, used for debug logging.

fn dyn_visit<T: AstVisitable>(&self, f: impl FnMut(&T))

where Self: Sized,

Visit all occurrences of that type inside self, in pre-order traversal.

fn dyn_visit_mut<T: AstVisitable>(&mut self, f: impl FnMut(&mut T))

where Self: Sized,

Visit all occurrences of that type inside self, in pre-order traversal.

impl BodyVisitable for Body

fn drive_body<V: VisitBody>(&self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn drive_body_mut<V: VisitBodyMut>( &mut self, v: &mut V, ) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn dyn_visit_in_body<T: BodyVisitable>(&self, f: impl FnMut(&T))

where Self: Sized,

Visit all occurrences of that type inside self, in pre-order traversal.

fn dyn_visit_in_body_mut<T: BodyVisitable>(&mut self, f: impl FnMut(&mut T))

where Self: Sized,

Visit all occurrences of that type inside self, in pre-order traversal.

impl Clone for Body

fn clone(&self) -> Body

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Body

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

Formats the value using the given formatter.

impl<'de, __State: ?Sized + DedupSerializerState> DeserializeState<'de, __State> for Body

fn deserialize_state<__D>( __state: &__State, __deserializer: __D, ) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

impl<'s, V> Drive<'s, V> for Body

where V: Visitor + Visit<'s, ExprBody> + Visit<'s, ExprBody> + Visit<'s, SeqHashMap<TargetTriple, FunDeclRef>> + Visit<'s, String> + Visit<'s, Vec<Option<String>>> + Visit<'s, Error>,

fn drive_inner(&'s self, visitor: &mut V) -> ControlFlow<V::Break>

Call v.visit() on the immediate contents of self.

impl<'s, V> DriveMut<'s, V> for Body

where V: Visitor + VisitMut<'s, ExprBody> + VisitMut<'s, ExprBody> + VisitMut<'s, SeqHashMap<TargetTriple, FunDeclRef>> + VisitMut<'s, String> + VisitMut<'s, Vec<Option<String>>> + VisitMut<'s, Error>,

fn drive_inner_mut(&'s mut self, visitor: &mut V) -> ControlFlow<V::Break>

Call v.visit() on the immediate contents of self.

impl<'s, V> DriveTwo<'s, V> for Body

where V: Visitor<Break: Default> + VisitTwo<'s, ExprBody> + VisitTwo<'s, ExprBody> + VisitTwo<'s, SeqHashMap<TargetTriple, FunDeclRef>> + VisitTwo<'s, String> + VisitTwo<'s, Vec<Option<String>>> + VisitTwo<'s, Error>,

fn drive_two_inner( &'s self, other: &'s Self, visitor: &mut V, ) -> ControlFlow<V::Break>

Call v.visit() on the immediate contents of self and other, if they correspond. If the values don’t match up, this returns Break(Default::default()).

impl<C: AstFormatter> FmtWithCtx<C> for Body

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

fn with_ctx<'a>(&'a self, ctx: &'a C) -> WithCtx<'a, C, Self>

Returns a struct that implements Display. This allows the following:

fn to_string_with_ctx(&self, ctx: &C) -> String

impl<__State: ?Sized + DedupSerializerState> SerializeState<__State> for Body

fn serialize_state<__S>( &self, __state: &__State, __serializer: __S, ) -> Result<__S::Ok, __S::Error>

where __S: Serializer,