jingle 0.5.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
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

pub mod concrete;
mod concretization;
mod relations;
pub mod symbolic;

#[cfg(test)]
mod tests {
    use crate::modeling::machine::cpu::concrete::{ConcretePcodeAddress, PcodeOffset};
    use crate::modeling::machine::cpu::symbolic::SymbolicPcodeAddress;
    use std::iter::empty;
    use z3::ast::BV;

    #[test]
    fn address_round_trip() {
        let addr = ConcretePcodeAddress {
            machine: 0xdeadbeefcafebabe,
            pcode: 0x50,
        };
        let symbolized = addr.symbolize();
        let new_concrete: Vec<_> = symbolized.concretize_with_assertions(empty()).collect();
        assert_eq!(addr, new_concrete[0])
    }

    #[test]
    fn increment_pcode_addr() {
        let addr = ConcretePcodeAddress {
            machine: 0,
            pcode: 0,
        };
        let symbolized = addr.symbolize();
        let new_concrete: Vec<_> = symbolized.concretize_with_assertions(empty()).collect();
        assert_eq!(
            new_concrete[0],
            ConcretePcodeAddress {
                machine: 0,
                pcode: 0
            }
        );
        let plus_1 = symbolized.increment_pcode();
        let new_concrete: Vec<_> = plus_1.concretize_with_assertions(empty()).collect();
        assert_eq!(
            new_concrete[0],
            ConcretePcodeAddress {
                machine: 0,
                pcode: 1
            }
        );
        let symbolized = ConcretePcodeAddress {
            machine: 0,
            pcode: 0xff,
        }
        .symbolize();
        let plus_1 = symbolized.increment_pcode();
        let new_concrete: Vec<_> = plus_1.concretize_with_assertions(empty()).collect();
        assert_eq!(
            new_concrete[0],
            ConcretePcodeAddress {
                machine: 0,
                pcode: 0
            }
        );
    }

    #[test]
    fn create_symbolic_addr() {
        let addr = BV::from_u64(0xdeadbeef, 64);
        let wrong = BV::from_u64(0xdeadbeef, 65);

        let sym = SymbolicPcodeAddress::try_from_symbolic_dest(&addr).unwrap();
        let concrete: Vec<_> = sym.concretize_with_assertions(empty()).collect();
        assert_eq!(
            concrete[0],
            ConcretePcodeAddress {
                machine: 0xdeadbeef,
                pcode: 0
            }
        );

        let sym = SymbolicPcodeAddress::try_from_symbolic_dest(&wrong);
        assert!(sym.is_err());
    }

    #[test]
    fn test_relative_math() {
        let addr = ConcretePcodeAddress {
            machine: 4,
            pcode: 4,
        };
        let dec1 = addr.add_pcode_offset(-1i8 as PcodeOffset);
        let add1 = addr.add_pcode_offset(1i8 as PcodeOffset);
        let add255 = addr.add_pcode_offset(255);

        assert_eq!(
            dec1,
            ConcretePcodeAddress {
                machine: 4,
                pcode: 3
            }
        );
        assert_eq!(
            add1,
            ConcretePcodeAddress {
                machine: 4,
                pcode: 5
            }
        );
        assert_eq!(dec1, add255);
    }
}