synth-verify 0.29.0

SMT translation validation for the Synth compiler (ordeal QF_BV engine; optional Z3 differential oracle)
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32

//! Verification traits for backend-agnostic translation validation
//!
//! These traits allow any backend to provide SMT semantics for its target
//! instruction set. The translation validator is generic over source and
//! target semantics.
//!
//! Semantics encode into the solver-agnostic [`crate::term::BV`] terms, so
//! implementations are independent of the SMT engine behind
//! [`crate::solver::BvSolver`].

use crate::term::BV;

/// Encodes source (WASM) operation semantics as SMT formulas
pub trait SourceSemantics {
    /// Encode a source operation, returning the result as a bitvector
    fn encode_op(&self, op_name: &str, inputs: &[BV]) -> Option<BV>;
}

/// Encodes target (ARM, RISC-V, etc.) operation semantics as SMT formulas
pub trait TargetSemantics {
    /// The target state type (registers, flags, memory)
    type State;

    /// Create a fresh symbolic state
    fn fresh_state(&self) -> Self::State;

    /// Apply a target operation to the state, returning updated state
    fn apply_op(&self, state: &Self::State, op_name: &str, inputs: &[BV]) -> Option<Self::State>;

    /// Extract the result bitvector from a state (e.g. read Rd register)
    fn extract_result(&self, state: &Self::State, result_loc: &str) -> Option<BV>;
}