ablation_b fix

Author: toolCHAINZ

src/gadget/library/builder.rs

@@ -38,6 +38,7 @@ fn default_blacklist() -> HashSet<OpCode> {
         // it from consideration
         OpCode::CPUI_BRANCH,
         OpCode::CPUI_CALL,
+        OpCode::CPUI_CALLOTHER,
         // The following operations are not yet modeled by jingle, so let's save some trees
         // and not even try to model them for the time being
         OpCode::CPUI_CBRANCH,

src/lib.rs

@@ -1,5 +1,5 @@
 pub use crate::synthesis::pcode_theory::pcode_assignment::{
-    assert_compatible_semantics, assert_concat, assert_state_constraints,
+    assert_concat, assert_pointer_invariant, assert_state_constraints,
 };
 
 #[cfg(feature = "bin")]

src/synthesis/pcode_theory/mod.rs

@@ -12,7 +12,7 @@ use crate::error::CrackersError;
 use crate::error::CrackersError::TheoryTimeout;
 use crate::synthesis::builder::{StateConstraintGenerator, TransitionConstraintGenerator};
 use crate::synthesis::pcode_theory::pcode_assignment::{
-    assert_compatible_semantics, assert_concat, assert_state_constraints,
+    assert_concat, assert_pointer_invariant, assert_state_constraints,
 };
 use crate::synthesis::pcode_theory::theory_constraint::{
     gen_conflict_clauses, ConjunctiveConstraint, TheoryStage,
@@ -130,6 +130,10 @@ impl<'ctx> PcodeTheory<'ctx> {
             post_bool,
             TheoryStage::Postcondition,
         ));
+        for g in &gadgets{
+        let b = assert_pointer_invariant(&self.j, g, &self.pointer_invariants)?;
+            self.solver.assert(&b);
+        }
         event!(Level::TRACE, "Evaluating chain:");
         for x in &gadgets {
             for i in &x.instructions {

src/synthesis/pcode_theory/pcode_assignment.rs

@@ -1,4 +1,4 @@
-use jingle::modeling::{ModeledBlock, ModeledInstruction, ModelingContext, State};
+use jingle::modeling::{ModeledBlock, ModelingContext, State};
 use jingle::JingleContext;
 use std::sync::Arc;
 use z3::ast::Bool;
@@ -73,21 +73,12 @@ pub fn assert_concat<'ctx, T: ModelingContext<'ctx>>(
     Ok(Bool::and(z3, &bools))
 }
 
-pub fn assert_compatible_semantics<'ctx, S: ModelingContext<'ctx>>(
+pub fn assert_pointer_invariant<'ctx>(
     jingle: &JingleContext<'ctx>,
-    spec: &S,
     item: &ModeledBlock<'ctx>,
     invariants: &[Arc<TransitionConstraintGenerator>],
 ) -> Result<Bool<'ctx>, CrackersError> {
     let mut bools = vec![];
-    // First, all outputs of the item under test must be assignable to the same values
-    // as in our specification computation
-    bools.push(item.upholds_postcondition(spec)?);
-    // Secondly, if the specification has some control flow behavior, the item must be able
-    // to have the same control flow behavior
-    if let Some(b) = spec.branch_comparison(item)? {
-        bools.push(b)
-    }
     // Thirdly, every input and output address must pass our pointer constraints
     for invariant in invariants.iter() {
         let inv = invariant(jingle, item)?;

src/synthesis/pcode_theory/theory_constraint.rs

@@ -5,7 +5,6 @@ use crate::synthesis::Decision;
 
 #[derive(Debug, Copy, Clone, PartialEq, Eq)]
 pub enum TheoryStage {
-    CombinedSemantics,
     Consistency,
     Branch,
     Precondition,