jingle 0.6.3

SMT Modeling for Ghidra's PCODE
Documentation
use crate::modeling::{BranchConstraint, ModelingContext, State};
use crate::varnode::ResolvedVarnode;
use jingle_sleigh::{PcodeOperation, SleighArchInfo};
use std::collections::HashSet;

impl<T: ModelingContext> ModelingContext for &[T] {
    fn get_arch_info(&self) -> &SleighArchInfo {
        self[0].get_arch_info()
    }

    fn get_address(&self) -> u64 {
        self[0].get_address()
    }

    fn get_original_state(&self) -> &State {
        self[0].get_original_state()
    }

    fn get_final_state(&self) -> &State {
        self.last().unwrap().get_final_state()
    }

    fn get_ops(&self) -> Vec<&PcodeOperation> {
        let mut vec = vec![];
        for thing in self.iter() {
            vec.extend(thing.get_ops())
        }
        vec
    }

    fn get_inputs(&self) -> HashSet<ResolvedVarnode> {
        // todo: this can have some inputs removed if they exist as outputs of a previous thing
        let mut hash_set = HashSet::new();
        for thing in self.iter() {
            hash_set.extend(thing.get_inputs());
        }
        hash_set
    }

    fn get_outputs(&self) -> HashSet<ResolvedVarnode> {
        let mut hash_set = HashSet::new();
        for thing in self.iter() {
            hash_set.extend(thing.get_outputs());
        }
        hash_set
    }

    fn get_branch_constraint(&self) -> &BranchConstraint {
        self.last().unwrap().get_branch_constraint()
    }
}