Java 类soot.jimple.BinopExpr 实例源码

/**
 * Performs kills by generating a killSet and then performing<br/>
 * outSet <- inSet - killSet<br/>
 * The kill set is generated by iterating over the def-boxes
 * of the unit. For each local defined in the unit we iterate
 * over the binopExps in the inSet, and check whether they use
 * that local. If so, it is added to the kill set.
 * @param inSet the set flowing into the unit
 * @param u the unit being flown through
 * @param outSet the set flowing out of the unit
 */
private void kill(FlowSet inSet, Unit u, FlowSet outSet) {
    FlowSet kills = emptySet.clone();
    for (ValueBox defBox : u.getDefBoxes()) {

        if (defBox.getValue() instanceof Local) {
            Iterator<BinopExpr> inIt = inSet.iterator();
            while (inIt.hasNext()) {
                BinopExpr e = inIt.next();
                Iterator<ValueBox> eIt = e.getUseBoxes().iterator();
                while (eIt.hasNext()) {
                    ValueBox useBox = eIt.next();
                    if (useBox.getValue() instanceof Local &&
                            useBox.getValue().equivTo(defBox.getValue()))
                        kills.add(e);
                }
            }
        }
    }
    inSet.difference(kills, outSet);
}

protected IfStmt ifStatement(DexBody body) {
      Instruction22t i = (Instruction22t) instruction;
      Local one = body.getRegisterLocal(i.getRegisterA());
      Local other = body.getRegisterLocal(i.getRegisterB());
      BinopExpr condition = getComparisonExpr(one, other);
      jif = (JIfStmt)Jimple.v().newIfStmt(condition, targetInstruction.getUnit());
      // setUnit() is called in ConditionalJumpInstruction

if (IDalvikTyper.ENABLE_DVKTYPER) {
    Debug.printDbg(IDalvikTyper.DEBUG, "constraint if: "+ jif +" condition: "+ condition);
    DalvikTyper.v().addConstraint(condition.getOp1Box(), condition.getOp2Box());
      }


      return jif;

  }

private void javafy_expr(ValueBox vb) {
    Expr e = (Expr) vb.getValue();

    if (e instanceof BinopExpr)
        javafy_binop_expr(vb);
    else if (e instanceof UnopExpr)
        javafy_unop_expr(vb);
    else if (e instanceof CastExpr)
        javafy_cast_expr(vb);
    else if (e instanceof NewArrayExpr)
        javafy_newarray_expr(vb);
    else if (e instanceof NewMultiArrayExpr)
        javafy_newmultiarray_expr(vb);
    else if (e instanceof InstanceOfExpr)
        javafy_instanceof_expr(vb);
    else if (e instanceof InvokeExpr)
        javafy_invoke_expr(vb);
    else if (e instanceof NewExpr)
        javafy_new_expr(vb);
}

public void outExprOrRefValueBox(ValueBox vb){
    //System.out.println("here"+vb);
    Value v = vb.getValue();
    if(! (v instanceof BinopExpr )){
        return;
    }

    BinopExpr binop = (BinopExpr)v;
    if(DEBUG)
        System.out.println("calling getResult");
    NumericConstant constant = getResult(binop);

    if(constant ==null)
        return;
    if(DEBUG)
        System.out.println("Changin"+vb+" to...."+constant);
    vb.setValue(constant);
}

private void caseBinopDivExpr(BinopExpr expr) {
    // Factors out code common to caseDivExpr and caseRemExpr.
    // The checks against constant divisors would perhaps be
    // better performed in a later pass, post-constant-propagation.
    Value divisor = expr.getOp2();
    Type divisorType = divisor.getType();
    if (divisorType instanceof UnknownType) {
    result = result.add(mgr.ARITHMETIC_EXCEPTION);
    } else if ((divisorType instanceof IntegerType) &&
    ((! (divisor instanceof IntConstant)) ||
     (((IntConstant) divisor).equals(INT_CONSTANT_ZERO)))) {
    result = result.add(mgr.ARITHMETIC_EXCEPTION);
    } else if ((divisorType == LongType.v()) &&
           ((! (divisor instanceof LongConstant)) ||
        (((LongConstant) divisor).equals(LONG_CONSTANT_ZERO)))) {
    result = result.add(mgr.ARITHMETIC_EXCEPTION);
    }
    caseBinopExpr(expr);
}

/**
 * This is a helper function to suppress false positives: Sometimes,
 * when try-catch with resources is being used
 * @param v
 * @return
 */
private boolean isTrivialNullCheck(Value v) {
     if (v instanceof BinopExpr) {
         BinopExpr bo = (BinopExpr)v;
         if (bo.getOp2() instanceof NullConstant && bo.getSymbol().equals(" == ")) {
             //now it gets itchy. We want to catch only that case
             //where the bytecode introduces a renaming of null and
             //does this unreachable null check.
             if (bo.getOp1() instanceof Local) {
                 Local l = (Local)bo.getOp1();
                 if (l.getType() instanceof NullType) {                      
                     return true;
                 } 
             }
         }
     }
     return false;
}

private void translateBinOp(BinopExpr arg0) {
    this.isLeftHandSide = false;
    arg0.getOp1().apply(this);
    Expression lhs = this.expressionStack.pop();
    arg0.getOp2().apply(this);
    Expression rhs = this.expressionStack.pop();

    // cast if necessary. This has to be done because soot treats boolean as
    // integers
    if (lhs.getType() != rhs.getType()) {
        rhs = TranslationHelpers.castBoogieTypes(rhs, lhs.getType());
    }

    if (arg0.getType() instanceof FloatType
            || arg0.getType() instanceof DoubleType) {
        FunctionDeclaration fun = SootPrelude.v().lookupRealOperator(
                arg0.getSymbol());
        Expression[] arguments = { lhs, rhs };
        this.expressionStack.push(this.pf.mkFunctionApplication(fun,
                arguments));
        return;
    }
    // if it is not Float or Double, proceed normally.
    createBinOp(arg0.getSymbol(), lhs, rhs);
}

public boolean equals(BinopExpr expr1, BinopExpr expr2){
    BoolExpr z3Formula1 = generate(expr1);
    BoolExpr z3Formula2 = generate(expr2);
    BoolExpr z3Formula = null;;
    try {
        BoolExpr lhs = ctx.MkImplies(z3Formula1, z3Formula2);
        BoolExpr rhs = ctx.MkImplies(z3Formula2, z3Formula1);
        z3Formula = ctx.MkAnd(new BoolExpr[]{lhs, rhs});
        Expr [] forall = new Expr[sootVarToZ3Var.size()];
        int i = 0;
        for(IntExpr var : sootVarToZ3Var.values()){
            forall[i] = var;
            i++;
        }
        z3Formula = ctx.MkForall(forall, z3Formula, 0, null, null, null, null);
    } catch (Z3Exception e) {
        // TODO Auto-generated catch block
        e.printStackTrace();
    }
    boolean ret = solve(z3Formula);
    return ret;
}

public BinopExpr instantiate(BitSet state, Value var){
    BinopExpr ret = null;
    Iterator<BaseElement> iter = getElements(state).iterator();
    //at least one base elements
    if(iter.hasNext()){
        ret = iter.next().instantiate(var);
        //if more than one - do either disjunction (default) or 
        //conjunction of negated base elements -- use DNotExpr, it is an expression so
        //but Binop takes Value, so it should work
        while(iter.hasNext()){
            if(disjoint){
                ret = new GOrExpr(ret, iter.next().instantiate(var));
            } else {
                //negated conjoint -- implement later
                //using for instantiating unstructured domain
                ret = new GAndExpr(ret, iter.next().instantiate(var));
            }
        }
    }
    return ret;
}

/**
 * This is a helper function to suppress false positives: Sometimes,
 * when try-catch with resources is being used
 * @param v
 * @return
 */
private boolean isTrivialNullCheck(Value v) {
     if (v instanceof BinopExpr) {
         BinopExpr bo = (BinopExpr)v;
         if (bo.getOp2() instanceof NullConstant && bo.getSymbol().equals(" == ")) {
             //now it gets itchy. We want to catch only that case
             //where the bytecode introduces a renaming of null and
             //does this unreachable null check.
             if (bo.getOp1() instanceof Local) {
                 Local l = (Local)bo.getOp1();
                 if (l.getType() instanceof NullType) {                      
                     return true;
                 } 
             }
         }
     }
     return false;
}

private void translateBinOp(BinopExpr arg0) {
    this.isLeftHandSide = false;
    arg0.getOp1().apply(this);
    Expression lhs = this.expressionStack.pop();
    arg0.getOp2().apply(this);
    Expression rhs = this.expressionStack.pop();

    // cast if necessary. This has to be done because soot treats boolean as
    // integers
    if (lhs.getType() != rhs.getType()) {
        rhs = TranslationHelpers.castBoogieTypes(rhs, lhs.getType());
    }

    if (arg0.getType() instanceof FloatType
            || arg0.getType() instanceof DoubleType) {
        FunctionDeclaration fun = SootPrelude.v().lookupRealOperator(
                arg0.getSymbol());
        Expression[] arguments = { lhs, rhs };
        this.expressionStack.push(this.pf.mkFunctionApplication(fun,
                arguments));
        return;
    }
    // if it is not Float or Double, proceed normally.
    createBinOp(arg0.getSymbol(), lhs, rhs);
}

/**
 * Performs gens by iterating over the units use-boxes.
 * If the value of a use-box is a binopExp then we add
 * it to the outSet.
 * @param outSet the set flowing out of the unit
 * @param u the unit being flown through
 */
private void gen(FlowSet outSet, Unit u) {
    for (ValueBox useBox : u.getUseBoxes()) {

        if (useBox.getValue() instanceof BinopExpr)
            outSet.add(useBox.getValue());
    }
}

public void outABinopExpr(ABinopExpr node)
   {
Value right = (Value) mProductions.removeLast();
BinopExpr expr = (BinopExpr) mProductions.removeLast();
Value left = (Value) mProductions.removeLast();


       expr.setOp1(left);
       expr.setOp2(right);
mProductions.addLast(expr);
   }

public void internalTransform(Body body, String phaseName, Map<String,String> options) {

    // really, the analysis should be able to use its own results to determine
    // that some branches are dead, but since it doesn't we just iterate.
    boolean changed;
    do {
        changed=false;

        NullnessAnalysis analysis=analysisFactory.newAnalysis(new ExceptionalUnitGraph(body));

        Chain<Unit> units=body.getUnits();
        Stmt s;
        for(s=(Stmt) units.getFirst();s!=null;s=(Stmt) units.getSuccOf(s)) {
        if(!(s instanceof IfStmt)) continue;
        IfStmt is=(IfStmt) s;
        Value c=is.getCondition();
        if(!(c instanceof EqExpr || c instanceof NeExpr)) continue;
        BinopExpr e=(BinopExpr) c;
        Immediate i=null;
        if(e.getOp1() instanceof NullConstant) i=(Immediate) e.getOp2();
        if(e.getOp2() instanceof NullConstant) i=(Immediate) e.getOp1();
        if(i==null) continue;
        boolean alwaysNull = analysis.isAlwaysNullBefore(s, i);
        boolean alwaysNonNull = analysis.isAlwaysNonNullBefore(s, i);
        int elim=0; // -1 => condition is false, 1 => condition is true
        if(alwaysNonNull) elim=c instanceof EqExpr ? -1 : 1;
        if(alwaysNull) elim=c instanceof EqExpr ? 1 : -1;
        Stmt newstmt=null;
        if(elim==-1) newstmt=Jimple.v().newNopStmt();
        if(elim==1) newstmt=Jimple.v().newGotoStmt(is.getTarget());
        if(newstmt!=null) {
            units.swapWith(s,newstmt);
            s=newstmt;
            changed=true;
        }
        }
    } while(changed);
    }

public void jimplify (DexBody body) {
     if(!(instruction instanceof Instruction23x))
         throw new IllegalArgumentException("Expected Instruction23x but got: "+instruction.getClass());

     Instruction23x binOpInstr = (Instruction23x)instruction;
     int dest = binOpInstr.getRegisterA();

     Local source1 = body.getRegisterLocal(binOpInstr.getRegisterB());
     Local source2 = body.getRegisterLocal(binOpInstr.getRegisterC());

     expr = getExpression(source1, source2);

     assign = Jimple.v().newAssignStmt(body.getRegisterLocal(dest), expr);
     assign.addTag(getTag());

     setUnit(assign);
     addTags(assign);
     body.add(assign);

     if (IDalvikTyper.ENABLE_DVKTYPER) {
Debug.printDbg(IDalvikTyper.DEBUG, "constraint: "+ assign);
       int op = (int)instruction.getOpcode().value;
       BinopExpr bexpr = (BinopExpr)expr;
       JAssignStmt jassign = (JAssignStmt)assign;
       DalvikTyper.v().setType(bexpr.getOp1Box(), op1BinType[op-0x90], true);
       DalvikTyper.v().setType(bexpr.getOp2Box(), op2BinType[op-0x90], true);
       DalvikTyper.v().setType(jassign.leftBox, resBinType[op-0x90], false);
     }
 }

public void jimplify (DexBody body) {
     if(!(instruction instanceof Instruction22s) && !(instruction instanceof Instruction22b))
         throw new IllegalArgumentException("Expected Instruction22s or Instruction22b but got: "+instruction.getClass());

     NarrowLiteralInstruction binOpLitInstr = (NarrowLiteralInstruction) this.instruction;
     int dest = ((TwoRegisterInstruction) instruction).getRegisterA();
     int source = ((TwoRegisterInstruction) instruction).getRegisterB();

     Local source1 = body.getRegisterLocal(source);

     IntConstant constant = IntConstant.v((int)binOpLitInstr.getNarrowLiteral());

     expr = getExpression(source1, constant);

     assign = Jimple.v().newAssignStmt(body.getRegisterLocal(dest), expr);
     assign.addTag(getTag());

     setUnit(assign);
     addTags(assign);
     body.add(assign);

     if (IDalvikTyper.ENABLE_DVKTYPER) {
Debug.printDbg(IDalvikTyper.DEBUG, "constraint: "+ assign);
         int op = (int)instruction.getOpcode().value;
       if (op >= 0xd8) {
         op -= 0xd8;
       } else {
         op -= 0xd0;
       }
       BinopExpr bexpr = (BinopExpr)expr;
       //body.dvkTyper.setType((op == 1) ? bexpr.getOp2Box() : bexpr.getOp1Box(), op1BinType[op]);
       DalvikTyper.v().setType(((JAssignStmt)assign).leftBox, op1BinType[op], false);
     }
 }

public void jimplify (DexBody body) {
     if(!(instruction instanceof Instruction12x))
         throw new IllegalArgumentException("Expected Instruction12x but got: "+instruction.getClass());

     Instruction12x binOp2AddrInstr = (Instruction12x)instruction;
     int dest = binOp2AddrInstr.getRegisterA();

     Local source1 = body.getRegisterLocal(binOp2AddrInstr.getRegisterA());
     Local source2 = body.getRegisterLocal(binOp2AddrInstr.getRegisterB());

     expr = getExpression(source1, source2);

     assign = Jimple.v().newAssignStmt(body.getRegisterLocal(dest), expr);
     assign.addTag(getTag());

     setUnit(assign);
     addTags(assign);
     body.add(assign);

     if (IDalvikTyper.ENABLE_DVKTYPER) {
Debug.printDbg(IDalvikTyper.DEBUG, "constraint: "+ assign);
       BinopExpr bexpr = (BinopExpr)expr;
       short op = instruction.getOpcode().value;
       DalvikTyper.v().setType(bexpr.getOp1Box(), op1BinType[op-0xb0], true);
       DalvikTyper.v().setType(bexpr.getOp2Box(), op2BinType[op-0xb0], true);
       DalvikTyper.v().setType(assign.getLeftOpBox(), resBinType[op-0xb0], false);
     }
 }

protected IfStmt ifStatement(DexBody body) {
      Instruction21t i = (Instruction21t) instruction;
      BinopExpr condition = getComparisonExpr(body, i.getRegisterA());
      jif = (JIfStmt) Jimple.v().newIfStmt(condition,
                                  targetInstruction.getUnit());
      // setUnit() is called in ConditionalJumpInstruction


if (IDalvikTyper.ENABLE_DVKTYPER) {
    Debug.printDbg(IDalvikTyper.DEBUG, "constraint: "+ jif);
         int op = instruction.getOpcode().value;
         switch (op) {
         case 0x38:
         case 0x39:
           //DalvikTyper.v().addConstraint(condition.getOp1Box(), condition.getOp2Box());
           break;
         case 0x3a:
         case 0x3b:
         case 0x3c:
         case 0x3d:
           DalvikTyper.v().setType(condition.getOp1Box(), BooleanType.v(), true);
           break;
         default:
           throw new RuntimeException("error: unknown op: 0x"+ Integer.toHexString(op));
         }
      }

return jif;

  }

private void javafy_binop_expr(ValueBox vb) {
    BinopExpr boe = (BinopExpr) vb.getValue();

    ValueBox leftOpBox = boe.getOp1Box(), rightOpBox = boe.getOp2Box();
    Value leftOp = leftOpBox.getValue(), rightOp = rightOpBox.getValue();

    if (rightOp instanceof IntConstant) {
        if ((leftOp instanceof IntConstant) == false) {
            javafy(leftOpBox);
            leftOp = leftOpBox.getValue();

            if (boe instanceof ConditionExpr)
                rightOpBox.setValue(DIntConstant.v(
                        ((IntConstant) rightOp).value, leftOp.getType()));
            else
                rightOpBox.setValue(DIntConstant.v(
                        ((IntConstant) rightOp).value, null));
        }
    } 
    else if (leftOp instanceof IntConstant) {
        javafy(rightOpBox);
        rightOp = rightOpBox.getValue();

        if (boe instanceof ConditionExpr)
            leftOpBox.setValue(DIntConstant.v(((IntConstant) leftOp).value,
                    rightOp.getType()));
        else
            leftOpBox.setValue(DIntConstant.v(((IntConstant) leftOp).value,
                    null));
    } else {
        javafy(rightOpBox);
        rightOp = rightOpBox.getValue();

        javafy(leftOpBox);
        leftOp = leftOpBox.getValue();
    }

    if (boe instanceof CmpExpr)
        vb.setValue(new DCmpExpr(leftOp, rightOp));

    else if (boe instanceof CmplExpr)
        vb.setValue(new DCmplExpr(leftOp, rightOp));

    else if (boe instanceof CmpgExpr)
        vb.setValue(new DCmpgExpr(leftOp, rightOp));
}

private Value normalizeNegations(Value v) {
    if (v instanceof NegExpr) {
        return ((NegExpr)v).getOp();
    } else if (v instanceof BinopExpr) {
        BinopExpr bo = (BinopExpr)v;
        if (bo instanceof NeExpr) {
            return new JEqExpr(bo.getOp1(), bo.getOp2());
        }
    }
    return v;
}

@Override
public State copy() {
    Set<Stmt> newSet = new HashSet<Stmt>();
    newSet.addAll(reachedStmt);
    Map<Value,Set<Stmt>> newUsed = new HashMap<Value,Set<Stmt>>();
    for(Entry<Value, Set<Stmt>> es : usedVars.entrySet()){
        Set<Stmt> newStmtSet = new HashSet<Stmt>();
        newStmtSet.addAll(es.getValue());
        newUsed.put(es.getKey(), newStmtSet);
    }
    Map<Stmt,BinopExpr> newCond = new HashMap<Stmt, BinopExpr>();
    newCond.putAll(condToExpr);
    SymbolicState ret = new SymbolicState(newSet, newUsed, newCond);
    return ret;
}

public void add(IfStmt newStmt, BinopExpr expr) {
    reachedStmt.add(newStmt);
    //get Values from rhs and lhs
    List<ValueBox> used = newStmt.getCondition().getUseBoxes();
    addUsedVars(used, newStmt);
    //add to map 
    condToExpr.put(newStmt, expr);

}

public boolean evaluateNot(BinopExpr expr){
    boolean ret = false;
    BoolExpr z3Formula = generate(expr);
    BoolExpr z3FormulaNot;
    try {
        z3FormulaNot = ctx.MkNot(z3Formula);
        ret = solve(z3FormulaNot);
    } catch (Z3Exception e) {
        e.printStackTrace();
    }
    return ret;

}

public List<Long> evaluateSol(BinopExpr expr, BinopExpr a, Value ... unknown) {
    List<Long> ret = null;
    //("expr " + expr + " " + " a " + a);
    BoolExpr z3Formula = generate(expr);
    try {
        BoolExpr z3ForA = a==null? ctx.MkFalse() : generate(a);
        //negate a
        BoolExpr negA = ctx.MkNot(z3ForA);
        //("negA " + negA);
        z3Formula = ctx.MkAnd(new BoolExpr[]{z3Formula, negA});
        Solver solver = ctx.MkSolver();
        Params p = ctx.MkParams();
        p.Add("soft_timeout", timeout);
        solver.setParameters(p);
        solver.Assert(z3Formula);
        Status result = solver.Check();
        if(result.equals(Status.SATISFIABLE)){
            ret = new ArrayList<Long>();
            Model m = solver.Model();
            for(Value v : unknown){
                IntExpr res = (IntExpr)m.ConstInterp(sootVarToZ3Var.get(v));
                if(res.toString().contains("mod") || res.toString().contains("div")){
                    System.out.println("Z3Formula  " + z3Formula);
                    return null;
                }
                ret.add(Long.parseLong(res.toString()));
            }
        } else if (result.equals(Status.UNSATISFIABLE)){
            ret = new ArrayList<Long>();
        } else {
            //unknown
            System.out.println("Warning: " + result + " for " + z3Formula);
        }
    } catch (Z3Exception e) {
        e.printStackTrace();
    }
    return ret;
}

private Set<BaseElement> transferDisjoint(BinopExpr symbState,
        Value lhs, Set<BaseElement> values) {
    Set<BaseElement> ret = new HashSet<BaseElement>();
    for(BaseElement be : values){
        //evaluate the whole formula
        BinopExpr newSymbState = new GAndExpr(symbState, be.instantiate(lhs));
        boolean sat = solver.evaluate(newSymbState);
        if(sat){
            ret.add(be);
        }
    }
    return ret;
}

public BinopExpr getSatPredicates(List<Long> sol, Value lhs) {
    BinopExpr ret = null;
    for(BaseElement be : element){
        if(be.evaluate(sol.get(0))){
            BinopExpr current = be.instantiate(lhs);
            if(ret != null){
                ret = new GAndExpr(current,ret);
            } else {
                //first time around
                ret = current;
            }
        }
    }
    return ret;
}

public BinopExpr top(Value lhs){
    BinopExpr ret = null;
    for(BaseElement be : element){
        BinopExpr current = be.instantiate(lhs);
        if(ret != null){
            ret = new GOrExpr(current, ret);
        } else {
            ret = current;
        }
    }
    return ret;
}

public BinopExpr bot(Value lhs){
    BinopExpr ret = null;
    for(BaseElement be : element){
        BinopExpr current = be.instantiate(lhs);
        if(ret != null){
            ret = new GAndExpr(current, ret);
        } else {
            ret = current;
        }
    }
    return ret;
}

public BinopExpr instantiate(Set<BaseElement> current, Value var) {
    BinopExpr ret = null;
    Iterator<BaseElement> iter = current.iterator();
    //at least one base elements
    if(iter.hasNext()){
        ret = iter.next().instantiate(var);
        while(iter.hasNext()){
            ret = new GOrExpr(ret, iter.next().instantiate(var));
        }
    }
    return ret;
}

public BinopExpr instantiateCNFSingle(Set<BaseElement> current, Value var) {
    BinopExpr ret = null;
    Iterator<BaseElement> iter = current.iterator();
    //at least one base elements
    if(iter.hasNext()){
        ret = iter.next().instantiate(var);
        while(iter.hasNext()){
            ret = new GAndExpr(ret, iter.next().instantiate(var));
        }
    }
    return ret;
}

public BinopExpr instantiateCNF(Set<Set<BaseElement>> lowerCNF, Value lhs) {
    BinopExpr ret = null;
    for(Set<BaseElement> conj : lowerCNF){
        if(ret == null){
            ret = instantiate(conj,lhs);
        } else {
            ret = new GAndExpr(ret, instantiate(conj,lhs));
        }
    }
    return ret;
}

public BinopExpr instantiate(Value var){
    Iterator<Predicate> iter = pred.iterator();
    //should have at least one predicate
    BinopExpr ret = iter.next().instantitate(var);
    while(iter.hasNext()){
        BinopExpr predExpr = iter.next().instantitate(var);
        // if more than one they are conjoint together, i.e., logical and
        ret = new GAndExpr(ret,predExpr);
    }
    return ret;
}

private void checkCompleteAndDisjoint(){
    //check whether the domain is complete, get the 
    //negation of the disjunction of all predicate
    JimpleLocal temp = new JimpleLocal("temp", IntType.v());
    BinopExpr complete = domain.top(temp);
    SolverWrapper solver = StartAnalysis.getSolver(); //new SolverWrapperZ3();
    boolean sat = solver.evaluateNot(complete);
    if(sat){
        System.out.println("Domain " + domain + " is incomplete !");
        System.exit(2);
    }
    //check whether the domain is pairwise disjoint
    //by default set that domain is disjoint
    domain.setDisjoint();
    for(BaseElement be1 : domain.getBaseElements()){
        for(BaseElement be2 : domain.getBaseElements()){
            if(!be1.equals(be2)){
                //create a conjunction of those two base elements
                BinopExpr disjoint = new GAndExpr(be1.instantiate(temp), be2.instantiate(temp));
                sat = solver.evaluate(disjoint);
                //disjoint predicates do not have a solution in common
                if(sat){
                    domain.setNotDisjoint();
                    return; //we're done -- found at lest one pair of predicates that are not pair-wise disjoint
                }
            }
        }
    }
}

private Value normalizeNegations(Value v) {
    if (v instanceof NegExpr) {
        return ((NegExpr)v).getOp();
    } else if (v instanceof BinopExpr) {
        BinopExpr bo = (BinopExpr)v;
        if (bo instanceof NeExpr) {
            return new JEqExpr(bo.getOp1(), bo.getOp2());
        }
    }
    return v;
}

/**
 * the operations that are not relevant for analysis like "not" or casts
 * are removed - array refs are only removed if explicitly stated
 * BinOpExpr are divided into two values
 * @param val the value which should be pruned
 * @param keepArrayRef if false then array refs are pruned to the base array object
 * @return one or more values 
 */
public static Set<Value> selectBaseList(Value val, boolean keepArrayRef){
    if (val instanceof BinopExpr) {
        Set<Value> set = new HashSet<Value>();
        BinopExpr expr = (BinopExpr) val;
        set.add(expr.getOp1());
        set.add(expr.getOp2());
        return set;
    }
    return Collections.singleton(selectBase(val, keepArrayRef));
}

private void printBinaryExpr(BinopExpr v) {
    String className = v.getClass().getSimpleName();
    if(className.charAt(0)=='J') className = className.substring(1);

    String oldName = varName;

    Value left = v.getOp1();
    String v1 = printValueAssignment(left, "left");

    Value right = v.getOp2();
    String v2 = printValueAssignment(right, "right");

    p.println("Value "+oldName+" = Jimple.v().new"+className+"("+v1+","+v2+");");

    varName = oldName;      
}

private void handleBinopExpr(BinopExpr be, Stmt stmt, Type tlhs)
{
    Value opl = be.getOp1(), opr = be.getOp2();
    Type tl = AugEvalFunction.eval_(this.tg, opl, stmt, this.jb),
        tr = AugEvalFunction.eval_(this.tg, opr, stmt, this.jb);

    if ( be instanceof AddExpr
        || be instanceof SubExpr
        || be instanceof MulExpr
        || be instanceof DivExpr
        || be instanceof RemExpr
        || be instanceof GeExpr
        || be instanceof GtExpr
        || be instanceof LeExpr
        || be instanceof LtExpr
        || be instanceof ShlExpr
        || be instanceof ShrExpr
        || be instanceof UshrExpr )
    {
        if ( tlhs instanceof IntegerType )
        {
            be.setOp1(this.uv.visit(opl, IntType.v(), stmt));
            be.setOp2(this.uv.visit(opr, IntType.v(), stmt));
        }
    }
    else if ( be instanceof CmpExpr
        || be instanceof CmpgExpr
        || be instanceof CmplExpr )
    {
        // No checks in the original assigner
    }
    else if ( be instanceof AndExpr
        || be instanceof OrExpr
        || be instanceof XorExpr )
    {
        be.setOp1(this.uv.visit(opl, tlhs, stmt));
        be.setOp2(this.uv.visit(opr, tlhs, stmt));
    }
    else if ( be instanceof EqExpr
        || be instanceof NeExpr )
    {
        if ( tl instanceof BooleanType && tr instanceof BooleanType )
        { }
        else if ( tl instanceof Integer1Type || tr instanceof Integer1Type )
        { }
        else if ( tl instanceof IntegerType )
        {
            be.setOp1(this.uv.visit(opl, IntType.v(), stmt));
            be.setOp2(this.uv.visit(opr, IntType.v(), stmt));
        }
    }
}

public void caseIfStmt(IfStmt stmt)
{
    this.handleBinopExpr((BinopExpr)stmt.getCondition(), stmt,
        BooleanType.v());
}

public void caseIfStmt(IfStmt stmt) {
    if (uses) {
        ConditionExpr cond = (ConditionExpr) stmt.getCondition();

        BinopExpr expr = cond;
        Value lv = expr.getOp1();
        Value rv = expr.getOp2();

        TypeVariable lop;
        TypeVariable rop;

        // ******** LEFT ********
        if (lv instanceof Local) {
            lop = resolver.typeVariable((Local) lv);
        } else if (lv instanceof DoubleConstant) {
            lop = resolver.typeVariable(DoubleType.v());
        } else if (lv instanceof FloatConstant) {
            lop = resolver.typeVariable(FloatType.v());
        } else if (lv instanceof IntConstant) {
            lop = resolver.typeVariable(IntType.v());
        } else if (lv instanceof LongConstant) {
            lop = resolver.typeVariable(LongType.v());
        } else if (lv instanceof NullConstant) {
            lop = resolver.typeVariable(NullType.v());
        } else if (lv instanceof StringConstant) {
            lop = resolver.typeVariable(RefType.v("java.lang.String"));
        } else if (lv instanceof ClassConstant) {
            lop = resolver.typeVariable(RefType.v("java.lang.Class"));
        } else {
            throw new RuntimeException("Unhandled binary expression left operand type: " + lv.getClass());
        }

        // ******** RIGHT ********
        if (rv instanceof Local) {
            rop = resolver.typeVariable((Local) rv);
        } else if (rv instanceof DoubleConstant) {
            rop = resolver.typeVariable(DoubleType.v());
        } else if (rv instanceof FloatConstant) {
            rop = resolver.typeVariable(FloatType.v());
        } else if (rv instanceof IntConstant) {
            rop = resolver.typeVariable(IntType.v());
        } else if (rv instanceof LongConstant) {
            rop = resolver.typeVariable(LongType.v());
        } else if (rv instanceof NullConstant) {
            rop = resolver.typeVariable(NullType.v());
        } else if (rv instanceof StringConstant) {
            rop = resolver.typeVariable(RefType.v("java.lang.String"));
        } else if (rv instanceof ClassConstant) {
            rop = resolver.typeVariable(RefType.v("java.lang.Class"));
        } else {
            throw new RuntimeException("Unhandled binary expression right operand type: " + rv.getClass());
        }

        TypeVariable common = resolver.typeVariable();
        rop.addParent(common);
        lop.addParent(common);
    }
}

public void jimplify (DexBody body) {
      if(!(instruction instanceof Instruction23x))
          throw new IllegalArgumentException("Expected Instruction23x but got: "+instruction.getClass());

      Instruction23x cmpInstr = (Instruction23x)instruction;
      int dest = cmpInstr.getRegisterA();

      Local first = body.getRegisterLocal(cmpInstr.getRegisterB());
      Local second = body.getRegisterLocal(cmpInstr.getRegisterC());

      //Expr cmpExpr;
      //Type type = null
      Opcode opcode = instruction.getOpcode();
      switch (opcode) {
      case CMPL_DOUBLE:
        setTag (new DoubleOpTag());
        type = DoubleType.v();
        cmpExpr = Jimple.v().newCmplExpr(first, second);
        break;
      case CMPL_FLOAT:
        setTag (new FloatOpTag());
        type = FloatType.v();
          cmpExpr = Jimple.v().newCmplExpr(first, second);
          break;
      case CMPG_DOUBLE:
        setTag (new DoubleOpTag());
        type = DoubleType.v();
        cmpExpr = Jimple.v().newCmpgExpr(first, second);
        break;
      case CMPG_FLOAT:
        setTag (new FloatOpTag());
        type = FloatType.v();
          cmpExpr = Jimple.v().newCmpgExpr(first, second);
          break;
      case CMP_LONG:
        setTag (new LongOpTag());
        type = LongType.v();
        cmpExpr = Jimple.v().newCmpExpr(first, second);
        break;
      default:
          throw new RuntimeException("no opcode for CMP: 0x"+ Integer.toHexString(opcode.value));
      }

      assign = Jimple.v().newAssignStmt(body.getRegisterLocal(dest), cmpExpr);
      assign.addTag(getTag());

      setUnit(assign);
      addTags(assign);
      body.add(assign);

if (IDalvikTyper.ENABLE_DVKTYPER) {
    Debug.printDbg(IDalvikTyper.DEBUG, "constraint: "+ assign);
        getTag().getName();
        BinopExpr bexpr = (BinopExpr)cmpExpr;
        DalvikTyper.v().setType(bexpr.getOp1Box(), type, true);
        DalvikTyper.v().setType(bexpr.getOp2Box(), type, true);
        DalvikTyper.v().setType(((JAssignStmt)assign).leftBox, IntType.v(), false);
      }
  }