jingle 0.6.8

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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124

use crate::modeling::{ModelingContext, TranslationContext};
use jingle_sleigh::Instruction;
use jingle_sleigh::{PcodeOperation, SleighArchInfo};
use std::borrow::Borrow;

use crate::modeling::branch::BranchConstraint;
use crate::modeling::state::State;
use std::collections::HashSet;
use z3::{Context, Translate};

use crate::JingleError;
use crate::varnode::ResolvedVarnode;

/// A `jingle` model of an individual SLEIGH instruction
#[derive(Debug, Clone)]
pub struct ModeledInstruction {
    info: SleighArchInfo,
    pub instr: Instruction,
    state: State,
    original_state: State,
    inputs: HashSet<ResolvedVarnode>,
    outputs: HashSet<ResolvedVarnode>,
    branch_builder: BranchConstraint,
}

impl ModeledInstruction {
    pub fn new<T: Borrow<SleighArchInfo>>(
        instr: Instruction,
        info: T,
    ) -> Result<Self, JingleError> {
        let info = info.borrow().clone();
        let original_state = State::new(&info);
        let state = original_state.clone();
        let next_vn = state.get_default_code_space_info().make_varnode(
            instr.next_addr(),
            state.get_default_code_space_info().index_size_bytes as usize,
        );
        let mut model = Self {
            info: info.borrow().clone(),
            instr,
            state,
            original_state,
            inputs: Default::default(),
            outputs: Default::default(),
            branch_builder: BranchConstraint::new(&next_vn),
        };
        for x in model.instr.clone().ops.iter() {
            model.model_pcode_op(x)?;
        }
        Ok(model)
    }

    pub fn fresh(&self) -> Result<Self, JingleError> {
        ModeledInstruction::new(self.instr.clone(), &self.info)
    }
}
impl ModelingContext for ModeledInstruction {
    fn get_arch_info(&self) -> &SleighArchInfo {
        &self.info
    }

    fn get_address(&self) -> u64 {
        self.instr.address
    }

    fn get_original_state(&self) -> &State {
        &self.original_state
    }

    fn get_final_state(&self) -> &State {
        &self.state
    }

    fn get_ops(&self) -> Vec<&PcodeOperation> {
        let mut result = vec![];
        for x in self.instr.ops.iter() {
            result.push(x);
        }
        result
    }

    fn get_inputs(&self) -> HashSet<ResolvedVarnode> {
        self.inputs.clone()
    }

    fn get_outputs(&self) -> HashSet<ResolvedVarnode> {
        self.outputs.clone()
    }

    fn get_branch_constraint(&self) -> &BranchConstraint {
        &self.branch_builder
    }
}

unsafe impl Translate for ModeledInstruction {
    fn translate(&self, dest: &Context) -> Self {
        Self {
            info: self.info.clone(),
            instr: self.instr.clone(),
            state: self.state.translate(dest),
            original_state: self.state.translate(dest),
            inputs: self.inputs.clone(),
            outputs: self.outputs.clone(),
            branch_builder: self.branch_builder.clone(),
        }
    }
}

impl TranslationContext for ModeledInstruction {
    fn track_input(&mut self, input: &ResolvedVarnode) {
        self.inputs.insert(input.clone());
    }
    fn track_output(&mut self, output: &ResolvedVarnode) {
        self.outputs.insert(output.clone());
    }

    fn get_final_state_mut(&mut self) -> &mut State {
        &mut self.state
    }

    fn get_branch_builder(&mut self) -> &mut BranchConstraint {
        &mut self.branch_builder
    }
}