#[cfg(not(feature = "std"))]
use alloc::vec::Vec;
#[cfg(feature = "std")]
use std::collections::HashMap;
#[cfg(not(feature = "std"))]
use hashbrown::HashMap;
use crate::Program;
use crate::VerifierError;
use crate::bytecode::InstructionStream;
use crate::dataflow::analysis::Analysis;
use crate::dataflow::bytecode::{BlockId, CfgContext, build_cfg};
use crate::dataflow::cfg::Cfg;
use crate::dataflow::direction::Forward;
use crate::dataflow::lattice::Lattice;
use crate::dataflow::solver::solve;
use crate::verifier::reg_type::{RegType, apply_writes, check_reads, write_effect};
#[derive(Clone, PartialEq, Eq)]
pub struct RegTypeValue(pub [RegType; 256]);
impl Lattice for RegTypeValue {
fn top() -> Self {
Self([RegType::Any; 256])
}
fn meet(&self, other: &Self) -> Self {
let mut result = Self::top();
for (out, (&a, &b)) in result.0.iter_mut().zip(self.0.iter().zip(other.0.iter())) {
*out = meet_reg(a, b);
}
result
}
}
fn meet_reg(a: RegType, b: RegType) -> RegType {
match (a, b) {
(RegType::Any, x) | (x, RegType::Any) => x,
(x, y) if x == y => x,
_ => RegType::Any,
}
}
pub struct RegTypeAnalysis {
block_writes: HashMap<BlockId, Vec<(u8, RegType)>>,
}
impl Analysis for RegTypeAnalysis {
type Value = RegTypeValue;
type Node = BlockId;
type Dir = Forward;
fn boundary_value(&self) -> RegTypeValue {
RegTypeValue([RegType::Unset; 256])
}
fn transfer(&self, node: &BlockId, input: &RegTypeValue) -> RegTypeValue {
let mut state = input.clone();
if let Some(writes) = self.block_writes.get(node) {
for &(slot, reg_type) in writes {
if let Some(entry) = state.0.get_mut(usize::from(slot)) {
*entry = reg_type;
}
}
}
state
}
}
fn collect_block_writes(code: &[u8], block_start: usize, block_end: usize) -> Vec<(u8, RegType)> {
let block_code = match code.get(block_start..block_end) {
Some(s) if !s.is_empty() => s,
_ => return Vec::new(),
};
let mut writes: Vec<(u8, RegType)> = Vec::new();
let mut stream = InstructionStream::new(block_code);
while let Some(Ok((_, _, instr))) = stream.next_instruction() {
if let Some((reg, rt)) = write_effect(&instr) {
writes.push((reg.slot(), rt));
}
}
writes
}
fn block_ranges(cfg: &Cfg<BlockId>, code_len: usize) -> Vec<(usize, usize)> {
let mut starts: Vec<BlockId> = cfg.nodes().to_vec();
starts.sort_unstable();
starts
.iter()
.enumerate()
.map(|(i, &s)| {
let end = starts.get(i + 1).copied().unwrap_or(code_len);
(s, end)
})
.collect()
}
pub(crate) fn check_register_types_with_cfg(
program: &Program,
cfg: &Cfg<BlockId>,
) -> Result<(), VerifierError> {
let code = program.code();
let ranges = block_ranges(cfg, code.len());
let block_writes: HashMap<BlockId, Vec<(u8, RegType)>> = ranges
.iter()
.filter_map(|&(start, end)| {
let writes = collect_block_writes(code, start, end);
if writes.is_empty() {
None
} else {
Some((start, writes))
}
})
.collect();
let analysis = RegTypeAnalysis { block_writes };
let result = solve(&analysis, cfg);
let top = RegTypeValue::top();
for &(block_start, block_end) in &ranges {
let before = result
.before(&block_start)
.cloned()
.unwrap_or_else(RegTypeValue::top);
if before == top {
continue;
}
let block_code = code.get(block_start..block_end).unwrap_or(&[]);
let mut state = before.0;
let mut stream = InstructionStream::new(block_code);
while let Some(item) = stream.next_instruction() {
let Ok((rel_pos, _, instr)) = item else { break };
let abs_pos = block_start + rel_pos;
check_reads(abs_pos, &instr, &state)?;
apply_writes(&instr, &mut state);
}
}
Ok(())
}
pub fn check_register_types(program: &Program) -> Result<(), VerifierError> {
let code = program.code();
if code.is_empty() {
return Ok(());
}
let Some(CfgContext { cfg, .. }) = build_cfg(code, program.jump_table()) else {
return Ok(());
};
check_register_types_with_cfg(program, &cfg)
}
#[cfg(test)]
mod tests {
use super::*;
use crate::bytecode::codec;
use crate::{Instruction, Register};
fn prog(instrs: &[Instruction]) -> Program {
Program::new(instrs.iter().flat_map(codec::encode).collect())
}
#[test]
fn empty_program_ok() {
assert!(check_register_types(&Program::new(vec![])).is_ok());
}
#[test]
fn stow_then_load_ok() {
let p = prog(&[
Instruction::Push1 { val: [7] },
Instruction::Stow { reg: Register(0) },
Instruction::Load { reg: Register(0) },
Instruction::Halt {},
]);
assert!(check_register_types(&p).is_ok());
}
#[test]
fn load_unset_register_is_error() {
let p = prog(&[Instruction::Load { reg: Register(1) }, Instruction::Halt {}]);
let err = check_register_types(&p).unwrap_err();
assert_eq!(err.variant_name(), "ReadUnsetRegister");
}
#[test]
fn wrong_type_for_load() {
let p = prog(&[
Instruction::Push1 { val: [4] },
Instruction::Bqmx { reg: Register(0) },
Instruction::Load { reg: Register(0) },
Instruction::Halt {},
]);
let err = check_register_types(&p).unwrap_err();
assert_eq!(err.variant_name(), "RegisterTypeMismatch");
}
#[test]
fn drop_clears_register() {
let p = prog(&[
Instruction::Push1 { val: [1] },
Instruction::Stow { reg: Register(0) },
Instruction::Drop { reg: Register(0) },
Instruction::Load { reg: Register(0) },
Instruction::Halt {},
]);
let err = check_register_types(&p).unwrap_err();
assert_eq!(err.variant_name(), "ReadUnsetRegister");
}
#[test]
fn unreachable_write_after_jump_no_false_positive() {
let p = prog(&[
Instruction::Push1 { val: [4] },
Instruction::Bqmx { reg: Register(0) }, Instruction::Jump2 { label: 0 }, Instruction::VecI { reg: Register(0) }, Instruction::Target {}, Instruction::GetLine { reg: Register(0) }, Instruction::Halt {},
]);
assert!(check_register_types(&p).is_ok());
}
#[test]
fn type_mismatch_on_taken_path_caught_linear_misses() {
let p = prog(&[
Instruction::VecI { reg: Register(0) }, Instruction::JumpI1 { label: 0 }, Instruction::Push1 { val: [4] }, Instruction::Bqmx { reg: Register(0) }, Instruction::Jump2 { label: 1 }, Instruction::Target {}, Instruction::GetLine { reg: Register(0) }, Instruction::Target {}, Instruction::Halt {},
]);
let err = check_register_types(&p).unwrap_err();
assert_eq!(err.variant_name(), "RegisterTypeMismatch");
}
#[test]
fn both_branches_same_type_ok() {
let p = prog(&[
Instruction::Push1 { val: [4] },
Instruction::Bqmx { reg: Register(0) }, Instruction::JumpI1 { label: 0 }, Instruction::Target {}, Instruction::GetLine { reg: Register(0) }, Instruction::Halt {},
]);
assert!(check_register_types(&p).is_ok());
}
#[test]
fn one_branch_writes_join_is_any_permissive() {
let p = prog(&[
Instruction::JumpI1 { label: 0 }, Instruction::Push1 { val: [4] }, Instruction::Bqmx { reg: Register(0) },
Instruction::Target {}, Instruction::GetLine { reg: Register(0) },
Instruction::Halt {},
]);
assert!(check_register_types(&p).is_ok());
}
}