Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WIP: add Wasmi translation invariants checker #1233

Draft
wants to merge 4 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
370 changes: 370 additions & 0 deletions crates/wasmi/src/engine/translator/conditions.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,370 @@
//! Wasmi translation post-conditions.
//!
//! These are run if `cfg(debug-assertions)` are enabled and
//! provide another layer of protection for invalid Wasmi translations.
//!
//! They are mostly intended for debugging purposes or for fuzzing Wasmi
//! as they would add too much overhead to conventional Wasmi translation.
//!
//! The set of post-conditions is run right after Wasmi translation has
//! finished compiling a Wasm function and just before the compiled function
//! is stored into Wasmi's `CodeMap`.
//!
//! The checks generally check invariants and guarantees given by the Wasmi
//! translation and therefore also act as "documentation" about some of them.

use super::{FuncTranslator, Instr};
use crate::ir::{self, BranchOffset, Instruction, Reg};
use core::{
cmp,
fmt::{self, Display},
};
use std::vec::Vec;

/// A non-empty list of [`Error`]s.
pub struct ErrorList<'ctx> {
ctx: ErrorContext<'ctx>,
errors: Vec<Error>,
}

impl<'ctx> ErrorList<'ctx> {
/// Creates a new [`ErrorList`].
///
/// # Panics
///
/// If `errors` is empty.
fn new(ctx: ErrorContext<'ctx>, errors: Vec<Error>) -> Self {
assert!(!errors.is_empty());

Check warning on line 37 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L36-L37

Added lines #L36 - L37 were not covered by tests
Self { ctx, errors }
}
}

impl ErrorList<'_> {
/// Returns `true` if `self` contains at least one [`Error`].
fn has_errors(&self) -> bool {
!self.errors.is_empty()

Check warning on line 45 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L44-L45

Added lines #L44 - L45 were not covered by tests
}

/// Returns the number of [`Error`]s in `self`.
fn len_errors(&self) -> usize {
self.errors.len()

Check warning on line 50 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L49-L50

Added lines #L49 - L50 were not covered by tests
}
}

impl Display for ErrorList<'_> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
if !self.has_errors() {
return writeln!(f, "all checked Wasmi translation invariants are uphold");

Check warning on line 57 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L55-L57

Added lines #L55 - L57 were not covered by tests
}
writeln!(
f,

Check warning on line 60 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L59-L60

Added lines #L59 - L60 were not covered by tests
"encountered {} broken invariants for Wasmi translation:",
self.len_errors()

Check warning on line 62 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L62

Added line #L62 was not covered by tests
)?;
let ctx = self.ctx;
for (n, error) in self.errors.iter().cloned().enumerate() {
write!(f, "error({n}): {}", ErrorWithContext { ctx, error })?;

Check warning on line 66 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L64-L66

Added lines #L64 - L66 were not covered by tests
}
Ok(())

Check warning on line 68 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L68

Added line #L68 was not covered by tests
}
}

/// An error describing a broken Wasmi translation invariant.
#[derive(Debug, Clone)]
pub struct Error {
/// The erraneous `Instruction` index.
instr: Instr,
/// The reason for the error.
reason: Reason,
}

/// The reason behind a broken Wasmi translation invariant.
#[derive(Debug, Clone)]
pub enum Reason {
InvalidRegister {
/// The invalid `Reg`.
reg: Reg,
},
InvalidGlobal {
/// The invalid `Global` index.
invalid_global: ir::index::Global,
},
InvalidFunc {
/// The invalid `Global` index.
invalid_func: ir::index::Func,
},
InvalidTable {
/// The invalid `Table` index.
invalid_table: ir::index::Table,
},
InvalidMemory {
/// The invalid `Memory` index.
invalid_memory: ir::index::Memory,
},
InvalidBranchOffset {
/// The invalid `BranchOffset`.
invalid_offset: BranchOffset,
},
InvalidBranchTarget {
/// The invalid target of the branch `Instruction`.
invalid_target: Instr,
},
InvalidConsumeFuel {
/// The invalid fuel consumption amount. (usually 0)
invalid_fuel: u64,
},
InvalidInstructionParameter {
/// The invalid `Instruction` parameter index.
invalid_param: Instr,
},
InvalidReturnValues {
/// The invalid number of returned values.
invalid_results: u32,
},
}

impl Display for ErrorWithContext<'_> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
let pos = self.pos();
let instr = self.instr();
match self.error.reason {
Reason::InvalidRegister { reg } => {
writeln!(
f,

Check warning on line 133 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L127-L133

Added lines #L127 - L133 were not covered by tests
"unexpected invalid register for instruction at {pos}:\n\
\t- instruction: {instr:?}\n\
\t- register: {reg:?}\
"
)
}
Reason::InvalidGlobal { invalid_global } => {
let len_globals = self.ctx.len_globals();
write!(
f,

Check warning on line 143 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L140-L143

Added lines #L140 - L143 were not covered by tests
"unexpected invalid global for instruction at {pos}:\n\
\t- instruction: {instr:?}\n\
\t- invalid global: {invalid_global:?}\n\
\t- number of globals in Wasm module: {len_globals}\
"
)
}
Reason::InvalidFunc { invalid_func } => {
let len_funcs = self.ctx.len_funcs();
write!(
f,

Check warning on line 154 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L151-L154

Added lines #L151 - L154 were not covered by tests
"unexpected invalid function for instruction at {pos}:\n\
\t- instruction: {instr:?}\n\
\t- invalid function: {invalid_func:?}\n\
\t- number of functions in Wasm module: {len_funcs}\
"
)
}
Reason::InvalidTable { invalid_table } => {
let len_tables = self.ctx.len_tables();
write!(
f,

Check warning on line 165 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L162-L165

Added lines #L162 - L165 were not covered by tests
"unexpected invalid table for instruction at {pos}:\n\
\t- instruction: {instr:?}\n\
\t- invalid table: {invalid_table:?}\n\
\t- number of tables in Wasm module: {len_tables}\
"
)
}
Reason::InvalidMemory { invalid_memory } => {
let len_memories = self.ctx.len_memories();
write!(
f,

Check warning on line 176 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L173-L176

Added lines #L173 - L176 were not covered by tests
"unexpected invalid linear memory for instruction at {pos}:\n\
\t- instruction: {instr:?}\n\
\t- invalid linear memory: {invalid_memory:?}\n\
\t- number of memories in Wasm module: {len_memories}\
"
)
}
Reason::InvalidBranchOffset { invalid_offset } => {
let fuel_metering_status = match self.ctx.is_fuel_metering_enabled() {
true => "enabled",
false => "disabled",

Check warning on line 187 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L184-L187

Added lines #L184 - L187 were not covered by tests
};
write!(
f,

Check warning on line 190 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L189-L190

Added lines #L189 - L190 were not covered by tests
"unexpected invalid branching offset for instruction at {pos}:\n\
\t- instruction: {instr:?}\n\
\t- invalid branch offset: {invalid_offset:?}\n\
\t- fuel metering: {fuel_metering_status}\
"
)
}
Reason::InvalidBranchTarget { invalid_target } => {
let invalid_target_pos = Self::instr_pos(invalid_target);
let invalid_target = self.ctx.resolve_instr(invalid_target);
let fuel_metering_status = match self.ctx.is_fuel_metering_enabled() {
true => "enabled",
false => "disabled",

Check warning on line 203 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L198-L203

Added lines #L198 - L203 were not covered by tests
};
let branch_kind = match invalid_target_pos.cmp(&pos) {
cmp::Ordering::Less => "backward",
cmp::Ordering::Equal => "self-loop",
cmp::Ordering::Greater => "forward",

Check warning on line 208 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L205-L208

Added lines #L205 - L208 were not covered by tests
};
write!(
f,

Check warning on line 211 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L210-L211

Added lines #L210 - L211 were not covered by tests
"unexpected invalid branching offset for instruction at {pos}:\n\
\t- instruction: {instr:?}\n\
\t- invalid target at: {invalid_target_pos:?}\n\
\t- invalid branch target: {invalid_target:?}\n\
\t- branch kind: {branch_kind}\n\
\t- fuel metering: {fuel_metering_status}\
"
)
}
Reason::InvalidConsumeFuel { invalid_fuel } => {
let fuel_metering_status = match self.ctx.is_fuel_metering_enabled() {
true => "enabled",
false => "disabled",

Check warning on line 224 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L221-L224

Added lines #L221 - L224 were not covered by tests
};
write!(
f,

Check warning on line 227 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L226-L227

Added lines #L226 - L227 were not covered by tests
"unexpected invalid fuel consumption for instruction at {pos}:\n\
\t- instruction: {instr:?}\n\
\t- invalid fuel consumption: {invalid_fuel:?}\n\
\t- fuel metering: {fuel_metering_status}\
"
)
}
Reason::InvalidInstructionParameter { invalid_param } => {
let invalid_param_pos = Self::instr_pos(invalid_param);
write!(
f,

Check warning on line 238 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L235-L238

Added lines #L235 - L238 were not covered by tests
"unexpected invalid instruction parameter for instruction at {pos}:\n\
\t- instruction: {instr:?}\n\
\t- invalid instruction parameter at: {invalid_param_pos}\
\t- invalid instruction parameter: {invalid_param:?}\
"
)
}
Reason::InvalidReturnValues { invalid_results } => {
write!(
f,

Check warning on line 248 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L246-L248

Added lines #L246 - L248 were not covered by tests
"unexpected invalid instruction parameter for instruction at {pos}:\n\
\t- instruction: {instr:?}\n\
\t- invalid number of results: {invalid_results}\
"
)
}
}
}
}

/// An error combined with contextual information to improve its [`Display`] implementation.
pub struct ErrorWithContext<'ctx> {
/// The contextual information for the error.
ctx: ErrorContext<'ctx>,
/// The underlying error.
error: Error,
}

/// A context to populate an [`Error`] with more information for its [`Display`] implementation.
#[derive(Copy, Clone)]
pub struct ErrorContext<'ctx> {
/// The underlying Wasmi function translator that has already finished its job.
translator: &'ctx FuncTranslator,
}

impl ErrorContext<'_> {
/// Returns `true` if fuel metering is enabled for the translation.
fn is_fuel_metering_enabled(&self) -> bool {
self.translator.fuel_costs.is_some()

Check warning on line 277 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L276-L277

Added lines #L276 - L277 were not covered by tests
}

/// Resolves the [`Instruction`] at `instr`.
///
/// # Panics
///
/// If `instr` is invalid for the underlying Wasmi translator.
fn resolve_instr(&self, instr: Instr) -> Instruction {
*self.translator.alloc.instr_encoder.instrs.get(instr)

Check warning on line 286 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L285-L286

Added lines #L285 - L286 were not covered by tests
}

/// Returns the number of global variables for the Wasm module of the compiled function.
fn len_globals(&self) -> usize {
self.translator.module.len_globals()

Check warning on line 291 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L290-L291

Added lines #L290 - L291 were not covered by tests
}

/// Returns the number of functions for the Wasm module of the compiled function.
fn len_funcs(&self) -> usize {
self.translator.module.len_funcs()

Check warning on line 296 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L295-L296

Added lines #L295 - L296 were not covered by tests
}

/// Returns the number of tables for the Wasm module of the compiled function.
fn len_tables(&self) -> usize {
self.translator.module.len_tables()

Check warning on line 301 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L300-L301

Added lines #L300 - L301 were not covered by tests
}

/// Returns the number of linear memories for the Wasm module of the compiled function.
fn len_memories(&self) -> usize {
self.translator.module.len_memories()

Check warning on line 306 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L305-L306

Added lines #L305 - L306 were not covered by tests
}
}

impl ErrorWithContext<'_> {
/// Returns the `u32` position of `instr` within the instruction sequence.
fn instr_pos(instr: Instr) -> u32 {
u32::from(ir::index::Instr::from(instr))

Check warning on line 313 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L312-L313

Added lines #L312 - L313 were not covered by tests
}

/// Returns the `u32` position of the error's `instr` within the instruction sequence.
fn pos(&self) -> u32 {
Self::instr_pos(self.error.instr)

Check warning on line 318 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L317-L318

Added lines #L317 - L318 were not covered by tests
}

/// Resolves the error's `instr` to [`Instruction`].
fn instr(&self) -> Instruction {
self.ctx.resolve_instr(self.error.instr)

Check warning on line 323 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L322-L323

Added lines #L322 - L323 were not covered by tests
}
}

/// Checks if the invariants of Wasmi function translation are uphold.
///
/// This function is called after Wasmi function translation has finished
/// and before the Wasmi engine's `CodeMap` is populated with the compiled
/// function.
///
/// The checking is designed to only be performed for builds with
/// `debug-assertions` enabled due to massive translation overhead.
///
/// # Errors
///
/// If a Wasmi translation invariant is broken.
pub fn verify_translation_invariants(translator: &FuncTranslator) -> Result<(), ErrorList> {
TranslationInvariantsChecker { translator }.verify_translation_invariants()
}

/// Encapsulates state required for translation invariants checking.
struct TranslationInvariantsChecker<'translator> {
/// The underlying Wasmi function translator which has already finished its job.
translator: &'translator FuncTranslator,
}

impl<'translator> TranslationInvariantsChecker<'translator> {
/// Checks if the invariants of Wasmi function translation are uphold.
///
/// Read more here: [`verify_translation_invariants`]
///
/// # Errors
///
/// If a Wasmi translation invariant is broken.
fn verify_translation_invariants(&self) -> Result<(), ErrorList<'translator>> {
let errors = Vec::new();
// TODO: perform invariant checking
if errors.is_empty() {
return Ok(());
}
Err(ErrorList::new(
ErrorContext {
translator: self.translator,

Check warning on line 365 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L363-L365

Added lines #L363 - L365 were not covered by tests
},
errors,

Check warning on line 367 in crates/wasmi/src/engine/translator/conditions.rs

View check run for this annotation

Codecov / codecov/patch

crates/wasmi/src/engine/translator/conditions.rs#L367

Added line #L367 was not covered by tests
))
}
}
4 changes: 2 additions & 2 deletions crates/wasmi/src/engine/translator/instr_encoder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ impl Instr {
#[derive(Debug, Default)]
pub struct InstrEncoder {
/// Already encoded [`Instruction`] words.
instrs: InstrSequence,
pub(super) instrs: InstrSequence,
/// Unresolved and unpinned labels created during function translation.
labels: LabelRegistry,
/// The last [`Instruction`] created via [`InstrEncoder::push_instr`].
Expand Down Expand Up @@ -173,7 +173,7 @@ impl InstrSequence {
/// # Panics
///
/// If no [`Instruction`] is associated to the [`Instr`] for this [`InstrSequence`].
fn get(&self, instr: Instr) -> &Instruction {
pub(super) fn get(&self, instr: Instr) -> &Instruction {
&self.instrs[instr.into_usize()]
}

Expand Down
Loading
Loading