airbender_host/
machine.rs

1use riscv_transpiler::ir::{
2    preprocess_bytecode, DecodingOptions, FullUnsignedMachineDecoderConfig, Instruction,
3    ReducedMachineDecoderConfig,
4};
5
6/// Airbender Platform machine profiles with stable host-side semantics.
7///
8/// The upstream Airbender crates model machines as Rust types, which is useful
9/// internally but brittle as a public platform API. This enum is the small set
10/// of machine configurations that `airbender-host` is willing to name and keep
11/// stable for normal users.
12///
13/// Full-signed decoding is intentionally omitted from the stable profile set for
14/// now: upstream decoding can name signed multiplication/division instructions,
15/// but the host runner does not execute those instruction variants.
16#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
17#[non_exhaustive]
18pub enum MachineProfile {
19    /// Full machine without signed multiplication/division support.
20    #[default]
21    FullUnsigned,
22    /// Reduced machine used by recursive verifier workloads.
23    Reduced,
24}
25
26type PreprocessBytecodeFn = fn(&[u32]) -> Vec<Instruction>;
27
28#[derive(Clone, Copy)]
29pub(crate) struct TranspilerDecoderConfig {
30    name: &'static str,
31    preprocess_bytecode: PreprocessBytecodeFn,
32    pub(crate) stable_profile: Option<MachineProfile>,
33}
34
35impl TranspilerDecoderConfig {
36    pub(crate) fn from_profile(profile: MachineProfile) -> Self {
37        match profile {
38            MachineProfile::FullUnsigned => Self {
39                name: "full unsigned",
40                preprocess_bytecode: preprocess_bytecode::<FullUnsignedMachineDecoderConfig>,
41                stable_profile: Some(profile),
42            },
43            MachineProfile::Reduced => Self {
44                name: "reduced",
45                preprocess_bytecode: preprocess_bytecode::<ReducedMachineDecoderConfig>,
46                stable_profile: Some(profile),
47            },
48        }
49    }
50
51    pub(crate) fn unstable_raw<D>(name: &'static str) -> Self
52    where
53        D: DecodingOptions,
54    {
55        Self {
56            name,
57            preprocess_bytecode: preprocess_bytecode::<D>,
58            stable_profile: None,
59        }
60    }
61
62    pub(crate) fn name(&self) -> &'static str {
63        self.name
64    }
65
66    pub(crate) fn preprocess(&self, bytecode: &[u32]) -> Vec<Instruction> {
67        (self.preprocess_bytecode)(bytecode)
68    }
69}
70
71impl Default for TranspilerDecoderConfig {
72    fn default() -> Self {
73        Self::from_profile(MachineProfile::default())
74    }
75}
76
77impl std::fmt::Debug for TranspilerDecoderConfig {
78    fn fmt(&self, formatter: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
79        formatter
80            .debug_struct("TranspilerDecoderConfig")
81            .field("name", &self.name)
82            .field("stable_profile", &self.stable_profile)
83            .finish_non_exhaustive()
84    }
85}
86
87#[cfg(test)]
88mod tests {
89    use super::{MachineProfile, TranspilerDecoderConfig};
90    use riscv_transpiler::ir::{
91        DebugReducedMachineDecoderConfig, FullMachineDecoderConfig, InstructionName,
92    };
93
94    const DIV_X3_X1_X2: u32 = 0x0220c1b3;
95    const LBU_X1_FROM_X0: u32 = 0x00004083;
96
97    #[test]
98    fn raw_decoder_can_opt_into_full_signed_decoding() {
99        let full_signed =
100            TranspilerDecoderConfig::unstable_raw::<FullMachineDecoderConfig>("test full signed")
101                .preprocess(&[DIV_X3_X1_X2]);
102        let full_unsigned = TranspilerDecoderConfig::from_profile(MachineProfile::FullUnsigned)
103            .preprocess(&[DIV_X3_X1_X2]);
104
105        assert_eq!(full_signed[0].name, InstructionName::Div);
106        assert_eq!(full_unsigned[0].name, InstructionName::Illegal);
107    }
108
109    #[test]
110    fn profile_controls_subword_memory_decoding() {
111        let full_unsigned = TranspilerDecoderConfig::from_profile(MachineProfile::FullUnsigned)
112            .preprocess(&[LBU_X1_FROM_X0]);
113        let reduced = TranspilerDecoderConfig::from_profile(MachineProfile::Reduced)
114            .preprocess(&[LBU_X1_FROM_X0]);
115
116        assert_eq!(full_unsigned[0].name, InstructionName::Lbu);
117        assert_eq!(reduced[0].name, InstructionName::Illegal);
118    }
119
120    #[test]
121    fn raw_decoder_accepts_upstream_decoder_configurations() {
122        let instructions =
123            TranspilerDecoderConfig::unstable_raw::<DebugReducedMachineDecoderConfig>(
124                "debug reduced",
125            )
126            .preprocess(&[LBU_X1_FROM_X0]);
127
128        assert_eq!(instructions[0].name, InstructionName::Lbu);
129    }
130}
airbender_host/machine.rs

airbender_host/
machine.rs
