Module bytecode::data_invariant_instrumentation
source · Expand description
Transformation which injects data invariants into the bytecode.
This transformation adds the data invariant to all occurrences of the WellFormed(x) call
which has been introduced by the spec instrumenter, by essentially transforming WellFormed(x)
into WellFormed(x) && <data invariant>(x). The WellFormed expressions are maintained in the
output for processing by the backend, in case type assumptions needed to be added by the backend
(which depends on the compilation scheme). It also handles PackRef/PackRefDeep
instructions introduced by memory instrumentation, as well as the Pack instructions.