jingle 0.6.0

SMT Modeling for Ghidra's PCODE
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

pub mod state;

use crate::analysis::cpa::residue::EmptyResidue;
use crate::analysis::cpa::{ConfigurableProgramAnalysis, IntoState};
use crate::analysis::location::bound::state::BoundedBranchState;
use crate::modeling::machine::cpu::concrete::ConcretePcodeAddress;

pub struct BoundedBranchAnalysis {
    max_steps: usize,
}

impl BoundedBranchAnalysis {
    pub fn new(max_steps: usize) -> Self {
        Self { max_steps }
    }
}

impl ConfigurableProgramAnalysis for BoundedBranchAnalysis {
    type State = BoundedBranchState;
    type Reducer<'op> = EmptyResidue<Self::State>;
}

impl IntoState<BoundedBranchAnalysis> for ConcretePcodeAddress {
    fn into_state(self, c: &BoundedBranchAnalysis) -> BoundedBranchState {
        BoundedBranchState::new(c.max_steps)
    }
}