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

use crate::modeling::concretize::Concretize;
use crate::modeling::machine::cpu::concrete::{ConcretePcodeAddress, PcodeOffset};
use crate::modeling::machine::cpu::symbolic::SymbolicPcodeAddress;
use z3::Model;
use z3::ast::Bool;

impl Concretize for SymbolicPcodeAddress {
    type Concretized = ConcretePcodeAddress;

    fn eval(&self, model: &Model, model_completion: bool) -> Option<Self::Concretized> {
        let machine = model.eval(&self.machine, model_completion)?.as_u64()?;
        let pcode = model.eval(&self.pcode, model_completion)?.as_u64()?;
        Some(ConcretePcodeAddress {
            machine,
            pcode: pcode as PcodeOffset,
        })
    }

    fn make_counterexample(&self, c: &Self::Concretized) -> Bool {
        self.eq(&c.symbolize()).not()
    }
}