jingle 0.5.4

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
125
126
127
128

use crate::error::JingleError;
use crate::modeling::ModelingContext;
use crate::modeling::branch::BlockEndBehavior::{Fallthrough, UnconditionalBranch};
use crate::sleigh::{GeneralizedVarNode, VarNode};
use serde::{Deserialize, Serialize};
use std::ops::Not;
use z3::ast::{Ast, BV};

#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
pub struct BlockConditionalBranchInfo {
    pub condition: VarNode,
    pub destination: GeneralizedVarNode,
}

#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
pub struct BranchConstraint {
    pub last: BlockEndBehavior,
    pub conditional_branches: Vec<BlockConditionalBranchInfo>,
}

#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
pub enum BlockEndBehavior {
    Fallthrough(VarNode),
    UnconditionalBranch(GeneralizedVarNode),
}

#[deprecated]
impl BlockEndBehavior {
    pub fn read_dest_metadata<T: ModelingContext>(&self, ctx: &T) -> Result<BV, JingleError> {
        match self {
            Fallthrough(f) => Ok(BV::from_u64(0, (f.size * 8) as u32)),
            UnconditionalBranch(b) => {
                match b {
                    // Direct branch
                    GeneralizedVarNode::Direct(d) => ctx.get_final_state().read_varnode_metadata(d),
                    // Indirect branch, we want to only inspect the pointer
                    GeneralizedVarNode::Indirect(i) => ctx
                        .get_final_state()
                        .read_varnode_metadata(&i.pointer_location),
                }
            }
        }
    }
    pub fn read_dest<T: ModelingContext>(&self, ctx: &T) -> Result<BV, JingleError> {
        match self {
            Fallthrough(f) => Ok(BV::from_u64(f.offset, (f.size * 8) as u32)),
            UnconditionalBranch(b) => {
                match b {
                    // Direct branch
                    GeneralizedVarNode::Direct(d) => {
                        Ok(BV::from_u64(d.offset, (d.size * 8) as u32))
                    }
                    // Indirect branch, we want to only inspect the pointer
                    GeneralizedVarNode::Indirect(i) => ctx
                        .get_final_state()
                        .read_varnode(&i.pointer_location)
                        .map(|f| f.simplify()),
                }
            }
        }
    }
}

#[expect(deprecated)]
impl BranchConstraint {
    pub fn new(last: &VarNode) -> Self {
        Self {
            last: Fallthrough(last.clone()),
            conditional_branches: Default::default(),
        }
    }

    pub fn with_same_final_branch(other: &Self) -> Self {
        Self {
            conditional_branches: vec![],
            last: other.last.clone(),
        }
    }

    pub fn has_branch(&self) -> bool {
        match self.last {
            Fallthrough(_) => !self.conditional_branches.is_empty(),
            UnconditionalBranch(_) => true,
        }
    }
    pub fn push_conditional(&mut self, cond: &BlockConditionalBranchInfo) {
        self.conditional_branches.push(cond.clone());
    }

    pub fn set_last(&mut self, new_last: &GeneralizedVarNode) {
        self.last = UnconditionalBranch(new_last.clone())
    }

    #[deprecated]
    pub fn build_bv<T: ModelingContext>(&self, ctx: &T) -> Result<BV, JingleError> {
        let mut dest_bv = self.last.read_dest(ctx)?;
        for cond_branch in self.conditional_branches.iter().rev() {
            let condition_bv = ctx
                .get_final_state()
                .read_varnode(&cond_branch.condition)?
                ._eq(BV::from_i64(0, (cond_branch.condition.size * 8) as u32))
                .not();
            let branch_dest = match &cond_branch.destination {
                GeneralizedVarNode::Direct(d) => BV::from_u64(d.offset, (d.size * 8) as u32),
                GeneralizedVarNode::Indirect(a) => ctx.get_final_state().read(a.into())?,
            };
            dest_bv = condition_bv.ite(&branch_dest, &dest_bv);
        }
        Ok(dest_bv)
    }

    #[deprecated]
    pub fn build_bv_metadata<T: ModelingContext>(&self, ctx: &T) -> Result<BV, JingleError> {
        let mut dest_bv = self.last.read_dest_metadata(ctx)?;
        for cond_branch in self.conditional_branches.iter().rev() {
            let condition_bv = ctx
                .get_final_state()
                .read_varnode(&cond_branch.condition)?
                ._eq(BV::from_i64(0, (&cond_branch.condition.size * 8) as u32))
                .not();
            let branch_dest = ctx
                .get_final_state()
                .read_metadata(cond_branch.destination.clone())?;
            dest_bv = condition_bv.ite(&branch_dest, &dest_bv);
        }
        Ok(dest_bv)
    }
}