Module Value_codec.Encoder

encode ?offset v ty Converts a Rust_val.t of type ty into an iterator over its sub values, along with their offset. Offsets all blocks by offset if specified

Iterates over the validity constraints of this particular value for a given type, traversing it recursively. For every requirement, this associates to it the error to be raised if the requirement is not met.

An optional check_refs function can be provided, to further check the validity of references and boxes relative to some state; this allows checking that references are not dangling, and that their pointees are valid. By default this function already checks references are well-aligned and non-null. Note that this check will raise errors in the outside monad, rather than in the returned list, since it is not possible to represent constraints in the state in first order logic. We provide this possibility here, to avoid re-implementing value traversal elsewhere.

This doesn't check:

• the fact the bytes of the value cannot be undefined, as that is checked when the memory is read; once we have a Rust_val.t, we are guaranteed the data is initialised.
• the validity of the discriminant of an enum, as that is checked when the memory is read (otherwise it would be impossible to even decode the value in the first place).

Reference: https://doc.rust-lang.org/reference/behavior-considered-undefined.html#r-undefined.validity

Applies a validity check for a value, given a check_ref state monad operation. This assumes check_ref is effect-free: the returned state is the input state. See validity.

Cast between literals; perform validation of the type's constraints. This is different from a transmute! It doesn't simply reinterpret the bits, but rather converts between types, e.g. rounding, truncating, extending, etc.

See also: https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-cast

Converts a floating value to a bitvector, preserving it's bit representation. This is a symbolic process, because SMT-Lib has no operation for "float->bv" that preserves the bits, due to NaN.

See https://smt-lib.org/theories-FloatingPoint.shtml, "Conversions to other sorts"

Transmutes a singular rust value, without splitting. This is under the assumption that size_of to_ty = size_of v, and both are primitives (literal or pointer).

nondet_raw ty returns a nondeterministic value for ty, by traversing ty: the returned value will have the right structure, and any required nondet variable will have been created. Importantly, the returned value may not uphold the validity invariant of ty*. To ensure the value is also valid, use validity, assume-ing the constraints it returns.

* Much like in validity, this function actually assumes two validity invariants: the data is initialised, and the discriminant of enums corresponds to that a variant.

Much like nondet_raw, but also assumes validity invariants for the value, with validity. Note this uses "stateless" validity: references are not checked to be e.g. non-dangling.

Apply the compiler-attribute to the given value

Traverses the given type and rust value, and returns all findable references with their type (ignores pointers, except if include_ptrs is true). This is needed e.g. when needing to get the pointers along with the size of their pointee, in particular in nested cases.

Folds over all the references and boxes in the given value and type, applying fn to them. This is used to update nested references when reborrowing. Calls fn with the pointer value and the pointer type (not the pointee).

Calculates the size and alignment of a type t, according to the pointer metadata meta. Receives an arbitrary state and load function, to possibly access a heap to get VTable information.