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

use crate::JingleError;
use crate::modeling::machine::cpu::symbolic::SymbolicPcodeAddress;
use crate::modeling::machine::memory::MemoryState;
use jingle_sleigh::PcodeOperation;

impl SymbolicPcodeAddress {
    pub(crate) fn apply_op(
        &self,
        memory: &MemoryState,
        op: &PcodeOperation,
    ) -> Result<Self, JingleError> {
        match op {
            PcodeOperation::Branch { input }
            | PcodeOperation::Call { dest: input, .. }
            | PcodeOperation::Fallthrough { input } => {
                Ok(self.interpret_branch_dest_varnode(input))
            }
            PcodeOperation::CBranch { input0, input1 } => {
                let fallthrough = self.increment_pcode();
                let dest = self.interpret_branch_dest_varnode(input0);
                let take_branch = memory.read(input1)?.extract(0, 0).eq(1);
                let machine = take_branch.ite(&dest.machine, &fallthrough.machine);
                let pcode = take_branch.ite(&dest.pcode, &fallthrough.pcode);
                Ok(SymbolicPcodeAddress { machine, pcode })
            }
            PcodeOperation::BranchInd { input }
            | PcodeOperation::CallInd { input }
            | PcodeOperation::Return { input } => {
                let dest = memory.read(input)?;
                SymbolicPcodeAddress::try_from_symbolic_dest(&dest)
            }
            _ => Ok(self.increment_pcode()),
        }
    }
}