jingle 0.6.6

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

use crate::{
    analysis::{
        cpa::{lattice::pcode::PcodeAddressLattice, state::AbstractState},
        location::basic::state::BasicLocationState,
    },
    modeling::machine::cpu::concrete::ConcretePcodeAddress,
};

use super::*;
use jingle_sleigh::{PcodeOperation, VarNode};

#[test]
fn test_call_behavior_branch() {
    let state =
        BasicLocationState::location(ConcretePcodeAddress::from(0x1000), CallBehavior::Branch);

    let call_op = PcodeOperation::Call {
        dest: VarNode::new(0x2000, 8u32, 0u32),
        args: vec![],
        call_info: None,
    };

    let successors: Vec<_> = state.transfer(&call_op).into_iter().collect();
    assert_eq!(successors.len(), 1);
    assert_eq!(
        successors[0].inner(),
        &PcodeAddressLattice::Const(ConcretePcodeAddress::from(0x2000))
    );
}

#[test]
fn test_call_behavior_step_over() {
    let state =
        BasicLocationState::location(ConcretePcodeAddress::from(0x1000), CallBehavior::StepOver);

    let call_op = PcodeOperation::Call {
        dest: VarNode::new(0x2000, 8u32, 0u32),
        args: vec![],
        call_info: None,
    };

    let successors: Vec<_> = state.transfer(&call_op).into_iter().collect();
    assert_eq!(successors.len(), 1);
    // Should step over to next pcode address (machine: 0x1000, pcode: 1)
    let expected = ConcretePcodeAddress::from(0x1000).next_pcode();
    assert_eq!(successors[0].inner(), &PcodeAddressLattice::Const(expected));
}

#[test]
fn test_call_behavior_terminate() {
    let state =
        BasicLocationState::location(ConcretePcodeAddress::from(0x1000), CallBehavior::Terminate);

    let call_op = PcodeOperation::Call {
        dest: VarNode::new(0x2000, 8u32, 0u32),
        args: vec![],
        call_info: None,
    };

    let successors: Vec<_> = state.transfer(&call_op).into_iter().collect();
    assert_eq!(
        successors.len(),
        0,
        "Terminate should produce no successors"
    );
}