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

Impl verification pass EndInTerminator #77

Open
wants to merge 15 commits into
base: main
Choose a base branch
from
Open
39 changes: 39 additions & 0 deletions crates/verifier/src/ctx.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
//! Verification context

use sonatina_ir::{module::FuncRef, ControlFlowGraph, Function};

use crate::{
error::{ErrorData, ErrorKind, TraceInfo},
ErrorStack,
};

pub struct VerificationCtx<'a> {
pub func_ref: FuncRef,
pub func: &'a Function,
pub cfg: ControlFlowGraph,
pub error_stack: ErrorStack,
}

impl<'a> VerificationCtx<'a> {
pub fn new(func_ref: FuncRef, func: &'a Function) -> Self {
let mut cfg = ControlFlowGraph::new();
cfg.compute(func);

Self {
func_ref,
func,
cfg,
error_stack: ErrorStack::default(),
}
}

pub fn report_nonfatal(&mut self, errs: &[ErrorData]) {
for e in errs {
let _err_ref = self.error_stack.push(*e);
}
}

pub fn report_fatal(&mut self, kind: ErrorKind, trace_info: TraceInfo) {
self.error_stack.fatal_error = Some(ErrorData::new(kind, trace_info));
}
}
17 changes: 13 additions & 4 deletions crates/verifier/src/error_stack.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,21 +5,30 @@ use crate::error::{Error, ErrorData, ErrorRef};

#[derive(Debug, Default)]
pub struct ErrorStack {
pub errors: PrimaryMap<ErrorRef, ErrorData>,
pub fatal_error: Option<ErrorData>,
pub non_fatal_errors: PrimaryMap<ErrorRef, ErrorData>,
}

impl ErrorStack {
pub fn push(&mut self, err: ErrorData) -> ErrorRef {
self.errors.push(err)
self.non_fatal_errors.push(err)
}

pub fn into_errs_iter(
self,
func: &Function,
func_ref: FuncRef,
) -> impl IntoIterator<Item = Error<'_>> {
self.errors
.into_iter()
let Self {
fatal_error,
non_fatal_errors: mut errs,
} = self;

if let Some(err) = fatal_error {
errs.push(err);
}

errs.into_iter()
.map(move |(_, err)| Error::new(err, func, func_ref))
}
}
7 changes: 7 additions & 0 deletions crates/verifier/src/lib.rs
Original file line number Diff line number Diff line change
@@ -1,2 +1,9 @@
pub mod ctx;
pub mod error;
pub mod error_stack;
pub mod pass;
pub mod passes;

pub use ctx::VerificationCtx;
pub use error_stack::ErrorStack;
pub use pass::VerificationPass;
14 changes: 14 additions & 0 deletions crates/verifier/src/pass.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
//! Verification pass

use crate::VerificationCtx;

pub trait VerificationPass {
fn run(&mut self, ctx: &mut VerificationCtx) -> VerificationResult;
}

#[derive(Debug, PartialEq, Eq)]
pub enum VerificationResult {
Pass,
Fail,
FailFatal,
}
137 changes: 137 additions & 0 deletions crates/verifier/src/passes/block/end_in_terminator.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,137 @@
use crate::{
error::{
ErrorKind::{NotEndedByTerminator, TerminatorBeforeEnd},
TraceInfoBuilder,
},
pass::VerificationResult,
VerificationCtx, VerificationPass,
};

pub struct EndInTerminator;

impl VerificationPass for EndInTerminator {
fn run(&mut self, ctx: &mut VerificationCtx) -> VerificationResult {
let layout = &ctx.func.layout;
let dfg = &ctx.func.dfg;

for block in layout.iter_block() {
let last_inst = layout.last_inst_of(block).expect("pass dependency error");

// check last instruction in block is terminator
if !dfg.is_terminator(last_inst) {
let trace_info = TraceInfoBuilder::new(ctx.func_ref).block(block).build();
ctx.report_fatal(NotEndedByTerminator(last_inst), trace_info);

return VerificationResult::FailFatal;
}

// check no instruction mid-block is terminator
for inst in layout.iter_inst(block) {
if inst == last_inst {
break;
}

if dfg.is_terminator(inst) {
let trace_info = TraceInfoBuilder::new(ctx.func_ref).block(block).build();
ctx.report_fatal(TerminatorBeforeEnd(inst), trace_info);

return VerificationResult::FailFatal;
}
}
}

VerificationResult::Pass
}
}

#[cfg(test)]
mod tests {
use sonatina_ir::{
builder::test_util::test_func_builder,
inst::{
control_flow::{Jump, Return},
logic::Xor,
},
isa::Isa,
Type,
};

use super::*;

#[test]
fn last_inst_not_terminator() {
let (evm, mut builder) = test_func_builder(&[Type::I1], Type::Unit);
let is = evm.inst_set();

let b0 = builder.append_block();

let arg = builder.args()[0];

builder.switch_to_block(b0);
let c1 = builder.make_imm_value(false);
builder.insert_inst_with(|| Xor::new(is, arg, c1), Type::I1);

builder.seal_all();

let module = builder.finish().build();
let func_ref = module.iter_functions().next().unwrap();
let func = &module.funcs[func_ref];

let mut ctx = VerificationCtx::new(func_ref, func);
let res = EndInTerminator.run(&mut ctx);
assert_eq!(res, VerificationResult::FailFatal);

let errs = ctx
.error_stack
.into_errs_iter(func, func_ref)
.into_iter()
.collect::<Vec<_>>();
assert_eq!(1, errs.len());

assert_eq!(
"last instruction not terminator, xor v0 0.i1
trace_info:
0: block0
1: func public %test_func(i1) -> unit",
errs[0].to_string()
);
}

#[test]
fn terminator_mid_block() {
let (evm, mut builder) = test_func_builder(&[], Type::Unit);
let is = evm.inst_set();

let b0 = builder.append_block();
let b1 = builder.append_block();

builder.switch_to_block(b0);
builder.insert_inst_no_result(Jump::new(is, b1));
builder.insert_inst_no_result_with(|| Return::new(is, None));

builder.seal_all();

let module = builder.finish().build();
let func_ref = module.iter_functions().next().unwrap();
let func = &module.funcs[func_ref];

let mut ctx = VerificationCtx::new(func_ref, func);
let res = EndInTerminator.run(&mut ctx);
assert_eq!(res, VerificationResult::FailFatal);

let errs = ctx
.error_stack
.into_errs_iter(func, func_ref)
.into_iter()
.collect::<Vec<_>>();
assert_eq!(1, errs.len());

assert_eq!(
"terminator instruction mid-block, jump block1
trace_info:
0: block0
1: func public %test_func() -> unit",
errs[0].to_string()
);
}
}
5 changes: 5 additions & 0 deletions crates/verifier/src/passes/block/mod.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//! Passes to verify block integrity

pub mod end_in_terminator;

pub use end_in_terminator::EndInTerminator;
1 change: 1 addition & 0 deletions crates/verifier/src/passes/mod.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
pub mod block;