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

use crate::JingleError;
use crate::modeling::concretize::ConcretizationIterator;
use crate::modeling::machine::cpu::concrete::{
    ConcretePcodeAddress, PcodeMachineAddress, PcodeOffset,
};
use jingle_sleigh::VarNode;
use z3::ast::{Ast, BV, Bool};

pub type SymbolicPcodeMachineAddress = BV;
pub type SymbolicPcodeOffset = BV;

// todo: add PcodeAddressSpace to Concrete and Symbolic addresses?
// probably necessary for harvard architecture modeling.
// ALSO: could be useful for callother.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct SymbolicPcodeAddress {
    pub(crate) machine: BV,
    pub(crate) pcode: BV,
}

impl SymbolicPcodeAddress {
    const MACHINE_SIZE_BITS: u32 = size_of::<PcodeMachineAddress>() as u32 * 8;
    const PCODE_SIZE_BITS: u32 = size_of::<PcodeOffset>() as u32 * 8;

    pub fn fresh_const() -> Self {
        Self {
            machine: BV::fresh_const("pc", Self::MACHINE_SIZE_BITS),
            pcode: BV::fresh_const("ppc", Self::PCODE_SIZE_BITS),
        }
    }

    pub fn new_const<S: AsRef<str>>(s: S) -> Self {
        let pc = format!("{}_pc", s.as_ref());
        let ppc = format!("{}_ppc", s.as_ref());
        Self {
            machine: BV::new_const(pc, Self::MACHINE_SIZE_BITS),
            pcode: BV::new_const(ppc, Self::PCODE_SIZE_BITS),
        }
    }

    pub fn try_from_symbolic_dest(bv: &BV) -> Result<Self, JingleError> {
        if bv.get_size() != Self::MACHINE_SIZE_BITS {
            Err(JingleError::InvalidBranchTargetSize)
        } else {
            Ok(SymbolicPcodeAddress {
                machine: bv.clone(),
                pcode: BV::from_u64(0u64, size_of::<PcodeOffset>() as u32 * 8),
            })
        }
    }

    fn extract_pcode(&self) -> &BV {
        &self.pcode
    }

    fn extract_machine(&self) -> &BV {
        &self.machine
    }

    pub fn concretize_with_assertions<T: Iterator<Item = Bool>>(
        &self,
        s: T,
    ) -> ConcretizationIterator<Self> {
        ConcretizationIterator::new_with_assertions(s, self)
    }

    pub fn interpret_branch_dest_varnode(&self, vn: &VarNode) -> Self {
        match vn.is_const() {
            true => self.add_pcode_offset(vn.offset()),
            false => ConcretePcodeAddress::from(vn.offset()).symbolize(),
        }
    }
    pub fn increment_pcode(&self) -> SymbolicPcodeAddress {
        self.add_pcode_offset(1)
    }
    fn add_pcode_offset(&self, offset: u64) -> SymbolicPcodeAddress {
        let pcode = self.extract_pcode() + offset;
        let machine = self.extract_machine().clone();
        SymbolicPcodeAddress { machine, pcode }
    }

    pub fn eq(&self, other: &Self) -> Bool {
        self.machine.eq(&other.machine) & self.pcode.eq(&other.pcode)
    }

    pub fn simplify(&self) -> Self {
        let machine = self.machine.simplify();
        let pcode = self.pcode.simplify();
        SymbolicPcodeAddress { machine, pcode }
    }

    pub fn as_concrete(&self) -> Option<ConcretePcodeAddress> {
        if let Some(machine) = self.machine.simplify().as_u64() {
            if let Some(pcode) = self.pcode.simplify().as_u64() {
                return Some(ConcretePcodeAddress {
                    machine,
                    pcode: pcode as PcodeOffset,
                });
            }
        }
        None
    }
}