Java 类soot.jimple.Expr 实例源码

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);
}

/**
 * Add "hs = new HandleStmt()" expression to Jimplecode.
 */
public static void invokeHS() {
    logger.log(Level.INFO, "Invoke HandleStmt in method {0}", b.getMethod().getName());

    locals.add(hs);
    Unit in = Jimple.v().newAssignStmt(hs, Jimple.v().newNewExpr(
            RefType.v(HANDLE_CLASS)));
    ArrayList<Type> paramTypes = new ArrayList<Type>();
    Expr specialIn = Jimple.v().newSpecialInvokeExpr(
            hs, Scene.v().makeConstructorRef(
            Scene.v().getSootClass(HANDLE_CLASS), paramTypes));

    Unit inv = Jimple.v().newInvokeStmt(specialIn);

    unitStore_Before.insertElement(unitStore_Before.new Element(inv, lastPos));
    unitStore_Before.insertElement(unitStore_Before.new Element(in, inv));
    lastPos = inv;
}

/**
 * Add a new local.
 * @param local The Local
 */
public static void addLocal(Local local) {
    logger.log(Level.INFO, "Add Local {0} in method {1}",new Object[] {
            getSignatureForLocal(local), b.getMethod().getName()});

    ArrayList<Type> paramTypes = new ArrayList<Type>();
    paramTypes.add(RefType.v("java.lang.String"));

    String signature = getSignatureForLocal(local);
    Stmt sig = Jimple.v().newAssignStmt(local_for_Strings, StringConstant.v(signature));

    Expr invokeAddLocal = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS), 
            "addLocal", paramTypes, VoidType.v(),   false), local_for_Strings);
    Unit ass = Jimple.v().newInvokeStmt(invokeAddLocal);


    unitStore_After.insertElement(unitStore_After.new Element(sig, lastPos));
    unitStore_After.insertElement(unitStore_After.new Element(ass, sig));
    lastPos = ass;
}

/**
 * Add a class object. Needed for static fields.
 * @param sc SootClass.
 */
public static void addClassObjectToObjectMap(SootClass sc) {

    logger.log(Level.INFO, "Add object {0} to ObjectMap in method {1}",
            new Object[] {sc.getName(), b.getMethod().getName()} );

    ArrayList<Type> parameterTypes = new ArrayList<Type>();
    parameterTypes.add(RefType.v("java.lang.Object"));

    System.out.println("Adding class Object:" + sc.getName().replace(".", "/"));    
    ClassConstant cc = ClassConstant.v(sc.getName().replace(".", "/"));
    System.out.println("Value: " + cc.value); 

    Expr addObj = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(
            Scene.v().getSootClass(HANDLE_CLASS), "addObjectToObjectMap", 
            parameterTypes, VoidType.v(), false), 
            ClassConstant.v(sc.getName().replace(".", "/"))); 
    Unit assignExpr = Jimple.v().newInvokeStmt(addObj);

    unitStore_After.insertElement(unitStore_After.new Element(assignExpr, lastPos));
    lastPos = assignExpr;
}

/**
 * Add a new array to objectMap.
 * @param a The Local where the array is stored.
 * @param pos Unit where the array occurs.
 */
public static void addArrayToObjectMap(Local a, Unit pos) {
    logger.log(Level.INFO, "Add array {0} to ObjectMap in method {1}",
            new Object[] {a, b.getMethod().getName()} );

    logger.log(Level.INFO, "Object type of array: " + a.getType() 
            + " and type " + a.getClass());
    logger.log(Level.FINEST, "at position {0}", pos.toString());

    ArrayList<Type> parameterTypes = new ArrayList<Type>();
    parameterTypes.add(ArrayType.v(
            RefType.v("java.lang.Object"), 1));



    Expr addObj = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(
                 Scene.v().getSootClass(HANDLE_CLASS),"addArrayToObjectMap",
                 parameterTypes, VoidType.v(), false), a); 
    Unit assignExpr = Jimple.v().newInvokeStmt(addObj);

    unitStore_After.insertElement(unitStore_After.new Element(assignExpr, pos));
    lastPos = assignExpr;       
}

/**
 * Set the security-level of a local to HIGH.
 * @param local Local
 * @param pos Unit where this local occurs
 */
public static void makeLocalHigh(Local local, Unit pos) {
    logger.log(Level.INFO, "Make Local {0} high in method {1}",
        new Object[] {getSignatureForLocal(local), b.getMethod().getName()});

    ArrayList<Type> paramTypes = new ArrayList<Type>();
    paramTypes.add(RefType.v("java.lang.String"));

    String signature = getSignatureForLocal(local);
    Stmt sig = Jimple.v().newAssignStmt(local_for_Strings, StringConstant.v(signature));

    Expr invokeAddLocal = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS), 
            "makeLocalHigh", paramTypes, VoidType.v(),false),
            local_for_Strings);
    Unit ass = Jimple.v().newInvokeStmt(invokeAddLocal);


    unitStore_After.insertElement(unitStore_After.new Element(sig, pos));
    unitStore_After.insertElement(unitStore_After.new Element(ass, sig));
    lastPos = ass;
}

/**
 * Set the security-level of a local to LOW.
 * @param local Local
 * @param pos Unit where this local occurs
 */
public static void makeLocalLow(Local local, Unit pos) {
    logger.log(Level.INFO, "Make Local {0} low in method {1}",
        new Object[] {getSignatureForLocal(local), b.getMethod().getName()});

    ArrayList<Type> paramTypes = new ArrayList<Type>();
    paramTypes.add(RefType.v("java.lang.String"));

    String signature = getSignatureForLocal(local);
    Stmt sig = Jimple.v().newAssignStmt(local_for_Strings, StringConstant.v(signature));

    Expr invokeAddLocal = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS), 
            "makeLocalLow", paramTypes, VoidType.v(),false), local_for_Strings);
    Unit ass = Jimple.v().newInvokeStmt(invokeAddLocal);


    unitStore_After.insertElement(unitStore_After.new Element(sig, pos));
    unitStore_After.insertElement(unitStore_After.new Element(ass, sig));
    lastPos = ass;
}

/**
 * Add the level of a local on the right side of an assign statement.
 * @param local Local
 * @param pos Unit where the local occurs
 */
public static void addLevelInAssignStmt(Local local, Unit pos) {
    logger.info("Adding level in assign statement");

    ArrayList<Type> paramTypes = new ArrayList<Type>();
    paramTypes.add(RefType.v("java.lang.String"));

    String signature = getSignatureForLocal(local);

    Stmt assignSignature = Jimple.v().newAssignStmt(
            local_for_Strings, StringConstant.v(signature));

    Expr invokeAddLevel = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS), 
            "joinLevelOfLocalAndAssignmentLevel", paramTypes, 
            Scene.v().getObjectType(),
            false), local_for_Strings);
    Unit invoke = Jimple.v().newInvokeStmt(invokeAddLevel);


    unitStore_Before.insertElement(unitStore_Before.new Element(assignSignature, pos));
    unitStore_Before.insertElement(unitStore_Before.new Element(invoke, pos));
    lastPos = pos;
}

/**
 * Add the level of a read array field to the security-level-list. 
 * @param a -ArrayRef- The referenced array field
 * @param pos -Unit- The position where this reference occurs
 */
public static void addLevelInAssignStmt(ArrayRef a, Unit pos) {
    logger.info( "Add Level of Array " + a.toString() + " in assign stmt");

    ArrayList<Type> parameterTypes = new ArrayList<Type>();
    parameterTypes.add(RefType.v("java.lang.Object"));
    parameterTypes.add(RefType.v("java.lang.String"));

    String signature = getSignatureForArrayField(a);
    Unit assignSignature = Jimple.v().newAssignStmt(
            local_for_Strings, StringConstant.v(signature));

    unitStore_Before.insertElement(unitStore_Before.new Element(assignSignature, pos));
    lastPos = assignSignature;

    Expr addObj = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS),
            "joinLevelOfArrayFieldAndAssignmentLevel", parameterTypes, 
            Scene.v().getObjectType(), false),
            a.getBase(), local_for_Strings);

    Unit assignExpr = Jimple.v().newInvokeStmt(addObj);

    unitStore_Before.insertElement(unitStore_Before.new Element(assignExpr, pos));
    lastPos = pos;
}

/**
 * @param l
 * @param pos
 */
public static void assignReturnLevelToLocal(Local l, Unit pos) {
    logger.log(Level.INFO, "Assign return level of invoked method to local {0}", 
            getSignatureForLocal(l));

    ArrayList<Type> parameterTypes = new ArrayList<Type>();
    parameterTypes.add(RefType.v("java.lang.String"));

    Expr assignRet = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(
            Scene.v().getSootClass(HANDLE_CLASS), "assignReturnLevelToLocal", 
            parameterTypes , VoidType.v(), false), 
            StringConstant.v(getSignatureForLocal(l)));
    Unit assignExpr = Jimple.v().newInvokeStmt(assignRet);

    unitStore_After.insertElement(unitStore_After.new Element(assignExpr, pos));
    lastPos = assignExpr;
}

/**
 * @param posInArgList
 * @param local
 * @param actualPos
 */
public static void assignArgumentToLocal(int posInArgList, Local local, Unit actualPos) {
    logger.log(Level.INFO, "Assign argument level to local " + local.toString());

    ArrayList<Type> parameterTypes = new ArrayList<Type>();
    parameterTypes.add(IntType.v());
    parameterTypes.add(RefType.v("java.lang.String"));
    Expr assignArg = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(
            Scene.v().getSootClass(HANDLE_CLASS), "assignArgumentToLocal",
            parameterTypes, Scene.v().getObjectType(), false),
            IntConstant.v(posInArgList), 
            StringConstant.v(getSignatureForLocal(local))
    );

    Unit assignExpr = Jimple.v().newInvokeStmt(assignArg);

    unitStore_After.insertElement(unitStore_After.new Element(assignExpr, lastPos));
    lastPos = assignExpr;
}

/**
 * Method to check that PC is not high. Called when calling System.out.println(), 
 * which must always be called in low context because of its side effects.
 * @param pos
 */
public static void checkThatPCNotHigh(Unit pos) {
    logger.info("Check that context is not high");

    if (pos == null) {
        throw new InternalAnalyzerException("Position is Null");
    }

    Expr checkPC = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS),
                    "checkThatPCNotHigh", new ArrayList<Type>(), VoidType.v(), false));
    Unit invoke = Jimple.v().newInvokeStmt(checkPC);

    unitStore_Before.insertElement(unitStore_Before.new Element(invoke, pos));
    lastPos = pos;
}

public void         outANonstaticInvokeExpr(ANonstaticInvokeExpr node)
   {
       List args;

       if(node.getArgList() != null)                           
    args = (List) mProductions.removeLast();
       else
           args = new ArrayList();

SootMethodRef method = (SootMethodRef) mProductions.removeLast();

String local = (String) mProductions.removeLast();


       Local l = mLocals.get(local);
       if(l ==        null) throw new RuntimeException("did not find local: " + local);


       Node invokeType = node.getNonstaticInvoke();
       Expr invokeExpr;

       if(invokeType instanceof ASpecialNonstaticInvoke){
           invokeExpr = Jimple.v().newSpecialInvokeExpr(l, method, args);
       } else if(invokeType instanceof AVirtualNonstaticInvoke){
           invokeExpr = Jimple.v().newVirtualInvokeExpr(l, method, args);
       } else {
           if(debug)if(!(invokeType instanceof AInterfaceNonstaticInvoke)) throw new RuntimeException("expected interface invoke.");
           invokeExpr = Jimple.v().newInterfaceInvokeExpr(l, method, args);
       }

mProductions.addLast(invokeExpr);  

   }

private void javafy(ValueBox vb) {
    Value v = vb.getValue();

    if (v instanceof Expr)
        javafy_expr(vb);
    else if (v instanceof Ref)
        javafy_ref(vb);
    else if (v instanceof Local)
        javafy_local(vb);
    else if (v instanceof Constant)
        javafy_constant(vb);
}

/**
 * Injects the constructor call of HandleStmt into the analyzed method.
 */
public static void initHS() {
    logger.log(Level.INFO, "Initialize HandleStmt in method {0}", 
            b.getMethod().getName());

    ArrayList<Type> paramTypes = new ArrayList<Type>();
    Expr invokeInit = Jimple.v().newStaticInvokeExpr(
            Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS), 
            "init", paramTypes, VoidType.v(), true));
    Unit init = Jimple.v().newInvokeStmt(invokeInit);
    unitStore_After.insertElement(unitStore_After.new Element(init, lastPos));
    lastPos = init;
}

/**
 * Injects the HandleStmt.close() method. This method should be injected at the
 * end of every analyzed method.
 */
public static void closeHS() {
    logger.log(Level.INFO, "Close HandleStmt in method {0} {1}", 
            new Object[] {b.getMethod().getName(), 
            System.getProperty("line.separator")});

    ArrayList<Type> paramTypes = new ArrayList<Type>();
    Expr invokeClose = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS), 
            "close", paramTypes, VoidType.v(), false));
    units.insertBefore(Jimple.v().newInvokeStmt(invokeClose), units.getLast());
}

/**
 * Add the instance of the actual class-object to the object map. 
 * This is only done in "init".
 */
public static void addInstanceObjectToObjectMap() {

    // Check if the first unit is a reference to the actual object
    if (!(units.getFirst() instanceof IdentityStmt) 
            || !(units.getFirst().getUseBoxes().get(0).getValue() 
            instanceof ThisRef)) {
        throw new InternalAnalyzerException("Expected @this reference");
    }

    String thisObj = units.getFirst().getUseBoxes().get(0).getValue().toString();

    logger.log(Level.INFO, "Add object {0} to ObjectMap in method {1}",
            new Object[] {thisObj, b.getMethod().getName()} );

    ArrayList<Type> parameterTypes = new ArrayList<Type>();
    parameterTypes.add(RefType.v("java.lang.Object"));

    Expr addObj = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(
            Scene.v().getSootClass(HANDLE_CLASS), "addObjectToObjectMap", 
            parameterTypes, VoidType.v(), false), 
            units.getFirst().getDefBoxes().get(0).getValue()); 
    Unit assignExpr = Jimple.v().newInvokeStmt(addObj);

    unitStore_After.insertElement(unitStore_After.new Element(assignExpr, lastPos));
    lastPos = assignExpr;

}

/**
 * Add a field to the object map.
 * @param field the SootField.
 */
public static void addInstanceFieldToObjectMap(SootField field) {
    logger.log(Level.INFO, "Adding field {0} to ObjectMap in method {1}", 
            new Object[] { field.getSignature() ,b.getMethod().getName()});

    if (!(units.getFirst() instanceof IdentityStmt) 
            || !(units.getFirst().getUseBoxes().get(0).getValue() 
            instanceof ThisRef)) {
        throw new InternalAnalyzerException("Expected @this reference");
    }

    String fieldSignature = getSignatureForField(field);


    ArrayList<Type> parameterTypes = new ArrayList<Type>();
    parameterTypes.add(RefType.v("java.lang.Object"));
    parameterTypes.add(RefType.v("java.lang.String"));

    Local tmpLocal = (Local) units.getFirst().getDefBoxes().get(0).getValue();

    Unit assignSignature = Jimple.v().newAssignStmt(local_for_Strings,
            StringConstant.v(fieldSignature));


    Expr addObj = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(
            Scene.v().getSootClass(HANDLE_CLASS), "addFieldToObjectMap", 
            parameterTypes, Scene.v().getObjectType(), false), 
            tmpLocal, local_for_Strings);
    Unit assignExpr = Jimple.v().newInvokeStmt(addObj);

    unitStore_After.insertElement(
            unitStore_After.new Element(assignSignature, lastPos));
    unitStore_After.insertElement(
            unitStore_After.new Element(assignExpr, assignSignature));
    lastPos = assignExpr;
}

/**
 * Add a static field. This field is added to its corresponding class object.
 * @param field SootField
 */
public static void addStaticFieldToObjectMap(SootField field) {
    logger.info( "Adding static Field " + field.toString() + " to Object Map");

    String signature = getSignatureForField(field);

    ArrayList<Type> parameterTypes = new ArrayList<Type>();
    parameterTypes.add(RefType.v("java.lang.Object"));
    parameterTypes.add(RefType.v("java.lang.String"));

    SootClass sc = field.getDeclaringClass();

    Unit assignDeclaringClass   = Jimple.v().newAssignStmt(
            local_for_Objects, ClassConstant.v(sc.getName().replace(".", "/")));

    Unit assignSignature = Jimple.v().newAssignStmt(
            local_for_Strings, StringConstant.v(signature));

    Expr addObj = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS),
            "addFieldToObjectMap", parameterTypes, 
            Scene.v().getObjectType(), false),
            local_for_Objects, local_for_Strings);
    Unit assignExpr = Jimple.v().newInvokeStmt(addObj);

    unitStore_After.insertElement(
            unitStore_After.new Element(assignDeclaringClass, lastPos));
    unitStore_After.insertElement(
            unitStore_After.new Element(assignSignature, assignDeclaringClass));
    unitStore_After.insertElement(
            unitStore_After.new Element(assignExpr, assignSignature));
    lastPos = assignExpr;

}

/**
 * Add the level of a field of an object. It can be the field of the actually
 * analyzed object or the field
 * @param f Reference to the instance field
 * @param pos The statement where this field occurs
 */
public static void addLevelInAssignStmt(InstanceFieldRef f, Unit pos) {
    logger.log(Level.INFO, "Adding level of field {0} in assignStmt in method {1}", 
            new Object[] {f.getField().getSignature(),b.getMethod().getName()});

    String fieldSignature = getSignatureForField(f.getField());

    ArrayList<Type> parameterTypes = new ArrayList<Type>();
    parameterTypes.add(RefType.v("java.lang.Object"));
    parameterTypes.add(RefType.v("java.lang.String"));

    // units.getFirst is already a reference to @this
    // Local tmpLocal = (Local) units.getFirst().getDefBoxes().get(0).getValue();
    Unit assignBase = Jimple.v().newAssignStmt(local_for_Objects, f.getBase());
    System.out.println("Base " + f.getBase());

    Unit assignSignature = Jimple.v().newAssignStmt(
            local_for_Strings, StringConstant.v(fieldSignature));

    Expr addObj = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(
            Scene.v().getSootClass(HANDLE_CLASS), "joinLevelOfFieldAndAssignmentLevel", 
            parameterTypes, Scene.v().getObjectType(), false), 
            local_for_Objects, local_for_Strings);
    Unit assignExpr = Jimple.v().newInvokeStmt(addObj);

    unitStore_Before.insertElement(unitStore_Before.new Element(assignBase, pos));
    unitStore_Before.insertElement(unitStore_Before.new Element(assignSignature, pos));
    unitStore_Before.insertElement(unitStore_Before.new Element(assignExpr, pos));
    lastPos = pos;
}

/**
 * @param f
 * @param pos
 */
public static void addLevelInAssignStmt(StaticFieldRef f, Unit pos) {
    logger.info( "Adding Level of static Field " + f.toString() + " in assign stmt");

    SootField field = f.getField();

    String signature = getSignatureForField(field);

    ArrayList<Type> parameterTypes = new ArrayList<Type>();
    parameterTypes.add(RefType.v("java.lang.Object"));
    parameterTypes.add(RefType.v("java.lang.String"));

    SootClass sc = field.getDeclaringClass();

    Unit assignDeclaringClass   = Jimple.v().newAssignStmt(
            local_for_Objects, ClassConstant.v(sc.getName().replace(".", "/")));

    Unit assignSignature = Jimple.v().newAssignStmt(
            local_for_Strings, StringConstant.v(signature));

    Expr addObj = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS),
            "joinLevelOfFieldAndAssignmentLevel", parameterTypes, 
            Scene.v().getObjectType(), false),
            local_for_Objects, local_for_Strings);
    Unit assignExpr = Jimple.v().newInvokeStmt(addObj);

    unitStore_Before.insertElement(
            unitStore_Before.new Element(assignDeclaringClass, pos));
    unitStore_Before.insertElement(unitStore_Before.new Element(assignSignature, pos));
    unitStore_Before.insertElement(unitStore_Before.new Element(assignExpr, pos));
    lastPos = pos;
}

/**
 * @param l
 * @param pos
 */
public static void setLevelOfAssignStmt(Local l, Unit pos) {
    logger.info("Setting level in assign statement");

    ArrayList<Type> paramTypes = new ArrayList<Type>();
    paramTypes.add(RefType.v("java.lang.String"));

    String signature = getSignatureForLocal(l);

    Stmt assignSignature = Jimple.v().newAssignStmt(
            local_for_Strings, StringConstant.v(signature));

    // insert setLevelOfLOcal
    Expr invokeSetLevel = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS), 
            "setLocalToCurrentAssingmentLevel", paramTypes,
            Scene.v().getObjectType(),
            false), local_for_Strings);
    Unit invoke = Jimple.v().newInvokeStmt(invokeSetLevel);

    // insert checkLocalPC
    Expr checkLocalPC = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS), 
            "checkLocalPC", paramTypes, 
            VoidType.v(),
            false), local_for_Strings);
    Unit checkLocalPCExpr = Jimple.v().newInvokeStmt(checkLocalPC);

    unitStore_Before.insertElement(unitStore_Before.new Element(assignSignature, pos));
    unitStore_Before.insertElement(unitStore_Before.new Element(checkLocalPCExpr, pos));
    unitStore_Before.insertElement(unitStore_Before.new Element(invoke, pos));
    lastPos = pos;
}

/**
 * @param retStmt
 */
public static void returnConstant(Unit retStmt) {
    logger.log(Level.INFO, "Return a constant value");

    ArrayList<Type> parameterTypes = new ArrayList<Type>();

    Expr returnConst = Jimple.v().newVirtualInvokeExpr(hs, Scene.v().makeMethodRef(
            Scene.v().getSootClass(HANDLE_CLASS), "returnConstant", 
            parameterTypes, VoidType.v(), false));

    unitStore_Before.insertElement(unitStore_Before.new Element(
            Jimple.v().newInvokeStmt(returnConst), retStmt));
}

/**
 * Insert the following check: If Local l is high, throw new IFCError
 * @param pos
 * @param l
 */
public static void checkThatNotHigh(Unit pos, Local l) {
    logger.info("Check that " + l + " is not high");

    if (l == null)  {
        throw new InternalAnalyzerException("Argument is null");
    }

    ArrayList<Type> paramTypes = new ArrayList<Type>();
    paramTypes.add(RefType.v("java.lang.String"));

    String signature = getSignatureForLocal(l);

    Stmt assignSignature = Jimple.v().newAssignStmt(
            local_for_Strings, StringConstant.v(signature));

    Expr invokeSetLevel = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS), 
            "checkThatNotHigh", paramTypes, VoidType.v(),   false), 
            local_for_Strings);
    Unit invoke = Jimple.v().newInvokeStmt(invokeSetLevel);


    unitStore_Before.insertElement(unitStore_Before.new Element(assignSignature, pos));
    unitStore_Before.insertElement(unitStore_Before.new Element(invoke, pos));
    lastPos = pos;
}

/**
 * If a stmt is a postdominator of an ifStmt then the if-context ends before this stmt.
 * The method exitInnerScope pops the localPCs for all ifStmts which end here.
 * @param pos The position of this stmt.
 */
public static void exitInnerScope(Unit pos) {
    logger.log(Level.INFO, "Exit inner scope in method {0}", b.getMethod().getName());

    ArrayList<Type> paramTypes = new ArrayList<Type>();
    paramTypes.add(RefType.v("java.lang.String"));

    String domIdentity = DominatorFinder.getIdentityForUnit(pos);
    logger.info("Dominator \"" + pos.toString()
            + "\" has identity " + domIdentity);

    Stmt assignHashVal = Jimple.v().newAssignStmt(
            local_for_Strings, StringConstant.v(domIdentity));


    Expr specialIn = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS),
            "exitInnerScope", paramTypes, VoidType.v(), false), 
            local_for_Strings);

    Unit inv = Jimple.v().newInvokeStmt(specialIn);

    unitStore_Before.insertElement(
            unitStore_Before.new Element(assignHashVal, pos));
    unitStore_Before.insertElement(unitStore_Before.new Element(inv, pos));
    lastPos = pos;
}

private void processIfStmt(IfStmt s, AbstractState inState,
        AbstractState ifStmtFalse, AbstractState ifStmtTrue) {
    ConditionExpr condExpr = (ConditionExpr)s.getCondition();
    Value lhs = condExpr.getOp1();
    Value rhs = condExpr.getOp2();
    //make sure this is an integer conditional stmt
    if(isAnyIntType(lhs)){
        //add it to the tracked states
        outputStmt.add(s);
        //create the set of variables to be tracked
        Set<Value> track = new HashSet<Value>();
        changedVariables.put(s, track);
        //precondition of the IfStmt
        Set<Expr> precond = new HashSet<Expr>();
        Set<Value> valuesToEval = new HashSet<Value>();//there should be one value only
        addNotNull(findLocal(lhs), valuesToEval);
        addNotNull(findLocal(rhs), valuesToEval);
        //need to make a special case when valuesToEval is empty
        //it means that both sides are concrete values
        //hence no need call for the solver
        for(Value v : valuesToEval){
            precond.addAll(evaluateStates(inState, v));
        }

        precond.addAll(evaluateStates(inState, null));//to evaluate symbolic state only
        //otherwise symbolic state can be evaluated twice -- equality of BinOp has not been implemented
        //it looks like in Jimple only statement of the same object are equal, but not
        //if they have the same semantics, assuming that locals are of the same object

        //do for true branch
        //add the current expression
        BinopExpr symbState = condExpr;
        BinopExpr symbNotState = negate(condExpr);
        for(Expr be : precond){
            symbState = new GAndExpr(symbState, be);
            symbNotState = new GAndExpr(symbNotState,be);
        }

        //at this point we have precondition set
        //make sure lhs is not a constant
        if(lhs instanceof JimpleLocal){
            //find new values for lhs
            updateStateCond(lhs,symbState, condExpr, ifStmtTrue, s);//s is only used for the symbolic state
            updateStateCond(lhs, symbNotState,negate(condExpr), ifStmtFalse, s);
            condExpr = null; //so no need to update the symbolic state twice
            track.add(lhs);
        }
        //make sure rhs is not a constant
        if(rhs instanceof JimpleLocal){
            updateStateCond(rhs, symbState, condExpr, ifStmtTrue, s);
            updateStateCond(rhs, symbNotState, negate(condExpr), ifStmtFalse,s );
            track.add(rhs);
        }
        //created the negated one
    } // end if this is an integer conditional stmt

}

/**
     * Set the level of a field of an object. It can be the field of the actually
     * analyzed object or the field
     * @param f Reference to the instance field
     * @param pos The statement where this field occurs
     */
    public static void setLevelOfAssignStmt(InstanceFieldRef f, Unit pos) {
        logger.log(Level.INFO, "Set level to field {0} in assignStmt in method {1}", 
                new Object[] {f.getField().getSignature(),b.getMethod().getName()});

//      if (!(units.getFirst() instanceof IdentityStmt) 
//              || !(units.getFirst().getUseBoxes().get(0).getValue() 
//              instanceof ThisRef)) {
//          System.out.println(units.getFirst().getUseBoxes().toString());
//          throw new InternalAnalyzerException("Expected @this reference");
//      }

        String fieldSignature = getSignatureForField(f.getField());

        ArrayList<Type> parameterTypes = new ArrayList<Type>();
        parameterTypes.add(RefType.v("java.lang.Object"));
        parameterTypes.add(RefType.v("java.lang.String"));

        // units.getFirst is already a reference to @this
        // Local tmpLocal = (Local) units.getFirst().getDefBoxes().get(0).getValue();

        // Retrieve the object it belongs to
        Local tmpLocal = (Local) f.getBase();

        Unit assignSignature = Jimple.v().newAssignStmt(
                local_for_Strings, StringConstant.v(fieldSignature));

        // insert: checkGlobalPC(Object, String)
        Expr checkGlobalPC  = Jimple.v().newVirtualInvokeExpr(
                hs, Scene.v().makeMethodRef(
                Scene.v().getSootClass(HANDLE_CLASS), "checkGlobalPC", 
                parameterTypes, VoidType.v(), false), 
                tmpLocal, local_for_Strings);
        Unit checkGlobalPCExpr = Jimple.v().newInvokeStmt(checkGlobalPC);

        // insert setLevelOfField
        Expr addObj = Jimple.v().newVirtualInvokeExpr(
                hs, Scene.v().makeMethodRef(
                Scene.v().getSootClass(HANDLE_CLASS), "setLevelOfField", 
                parameterTypes, Scene.v().getObjectType(), false), 
                tmpLocal, local_for_Strings);
        Unit assignExpr = Jimple.v().newInvokeStmt(addObj);

        unitStore_Before.insertElement(unitStore_After.new Element(checkGlobalPCExpr, pos));
        unitStore_Before.insertElement(unitStore_Before.new Element(assignSignature, pos));
        unitStore_Before.insertElement(unitStore_After.new Element(assignExpr, pos));
        lastPos = pos;
    }

/**
 * @param f
 * @param pos
 */
public static void setLevelOfAssignStmt(StaticFieldRef f, Unit pos) {
    logger.info( "Set Level of static Field " + f.toString() + " in assign stmt");

    SootField field = f.getField();

    String signature = getSignatureForField(field);
    System.out.println("Signature of static field in jimple injector " + signature);

    ArrayList<Type> parameterTypes = new ArrayList<Type>();
    parameterTypes.add(RefType.v("java.lang.Object"));
    parameterTypes.add(RefType.v("java.lang.String"));

    SootClass sc = field.getDeclaringClass();

    Unit assignDeclaringClass   = Jimple.v().newAssignStmt(
            local_for_Objects, ClassConstant.v(sc.getName().replace(".", "/")));

    Unit assignSignature = Jimple.v().newAssignStmt(
            local_for_Strings, StringConstant.v(signature));

    // insert: checkGlobalPC(Object, String)
    Expr checkGlobalPC  = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(
            Scene.v().getSootClass(HANDLE_CLASS), "checkGlobalPC", 
            parameterTypes, VoidType.v(), false), 
            local_for_Objects, local_for_Strings);
    Unit checkGlobalPCExpr = Jimple.v().newInvokeStmt(checkGlobalPC);

    // Add setLevelOfField
    Expr addObj = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS),
            "setLevelOfField", parameterTypes, 
            Scene.v().getObjectType(), false),
            local_for_Objects, local_for_Strings);
    Unit assignExpr = Jimple.v().newInvokeStmt(addObj);

    unitStore_Before.insertElement(
            unitStore_Before.new Element(assignDeclaringClass, pos));
    unitStore_Before.insertElement(unitStore_Before.new Element(assignSignature, pos));
    unitStore_Before.insertElement(unitStore_Before.new Element(checkGlobalPCExpr, pos));
    unitStore_Before.insertElement(unitStore_Before.new Element(assignExpr, pos));
    lastPos = pos;
}

/**
 * Store the levels of all arguments in a list in ObjectMap. If an
 * argument is a constant, then the argument is stored as "DEFAULT_LOW".
 * @param pos position of actual statement
 * @param lArguments list of arguments
 */
public static void storeArgumentLevels(Unit pos, Local... lArguments) {

    logger.log(Level.INFO, "Store Arguments for next method in method {0}",
            b.getMethod().getName());

    int length = lArguments.length;

    ArrayList<Type> parameterTypes = new ArrayList<Type>();
    parameterTypes.add(ArrayType.v(RefType.v("java.lang.String"), 1));

    Expr paramArray = Jimple.v().newNewArrayExpr(RefType.v(
            "java.lang.String"), IntConstant.v(length));

    Unit assignNewStringArray = Jimple.v().newAssignStmt(
            local_for_String_Arrays, paramArray);

    Unit[] tmpUnitArray = new Unit[length];

    for (int i = 0; i < length; i++) {

        // It's possible to get a null vector as an argument. This happens,
        // if a constant is set as argument.
        if (lArguments[i] != null) {
            String signature = getSignatureForLocal(lArguments[i]);
            tmpUnitArray[i] = Jimple.v().newAssignStmt(Jimple.v().newArrayRef(
                    local_for_String_Arrays, IntConstant.v(i)), 
                    StringConstant.v(signature));
        } else {
            tmpUnitArray[i] = Jimple.v().newAssignStmt(Jimple.v().newArrayRef(
                    local_for_String_Arrays, IntConstant.v(i)), 
                    StringConstant.v("DEFAULT_LOW"));
        }
    }

    Expr storeArgs = Jimple.v().newVirtualInvokeExpr(hs, Scene.v().makeMethodRef(
            Scene.v().getSootClass(HANDLE_CLASS), "storeArgumentLevels", 
            parameterTypes, VoidType.v(), false), local_for_String_Arrays);
    Stmt invokeStoreArgs = Jimple.v().newInvokeStmt(storeArgs);



    unitStore_Before.insertElement(
            unitStore_Before.new Element(assignNewStringArray, pos));
    for (Unit el : tmpUnitArray) {
        unitStore_Before.insertElement(unitStore_Before.new Element(el, pos));
    }
    unitStore_Before.insertElement(unitStore_Before.new Element(invokeStoreArgs, pos));
    lastPos = pos;

}

/**
 * Check condition of if statements. Needed parameters are all locals (no constants)
 * which occur in the if statement. If the result is high, then the lpc of the if-context
 * is set to high.
 * @param pos Position of the ifStmt in the method body.
 * @param locals An array of all locals which appear in the condition.
 */
public static void checkCondition(Unit pos, Local... locals) {

    logger.log(Level.INFO, "Check condition in method {0}", b.getMethod());
    logger.log(Level.INFO, "IfStmt: {0}", pos.toString());

    int numberOfLocals = locals.length;
    ArrayList<Type> paramTypes = new ArrayList<Type>();
    paramTypes.add(RefType.v("java.lang.String"));
    paramTypes.add(ArrayType.v(RefType.v("java.lang.String"), numberOfLocals));

    // Add hashvalue for immediate dominator
    String domIdentity = DominatorFinder.getImmediateDominatorIdentity(pos);
    logger.info("Identity of Dominator of \"" + pos.toString()
            + "\" is " + domIdentity);
    Stmt assignHashVal = Jimple.v().newAssignStmt(
            local_for_Strings, StringConstant.v(domIdentity));

    // Add all locals to string array
    Expr newStringArray = Jimple.v().newNewArrayExpr(
            RefType.v("java.lang.String"), IntConstant.v(numberOfLocals));

    Unit assignNewArray = Jimple.v().newAssignStmt(
            local_for_String_Arrays, newStringArray);

    ArrayList<Unit> tmpUnitList = new ArrayList<Unit>();

    for (int i = 0; i < numberOfLocals; i ++) {
        Unit assignSignature = Jimple.v().newAssignStmt(
                Jimple.v().newArrayRef(local_for_String_Arrays, 
                IntConstant.v(i)), 
                StringConstant.v(getSignatureForLocal(locals[i])));
        tmpUnitList.add(assignSignature);
    }

    // Invoke HandleStmt.checkCondition(String domHash, String... locals)
    Expr invokeCheckCondition = Jimple.v().newVirtualInvokeExpr(
            hs, Scene.v().makeMethodRef(Scene.v().getSootClass(HANDLE_CLASS), 
            "checkCondition", paramTypes, VoidType.v(), false),
            local_for_Strings, local_for_String_Arrays);
    Unit invokeCC = Jimple.v().newInvokeStmt(invokeCheckCondition);

    unitStore_Before.insertElement(unitStore_Before.new Element(assignNewArray, pos));
    lastPos = assignNewArray;
    for (Unit u : tmpUnitList) {
        unitStore_After.insertElement(unitStore_After.new Element(u, lastPos));
        lastPos = u;
    }
    unitStore_After.insertElement(unitStore_After.new Element(assignHashVal, lastPos));
    lastPos = assignHashVal;
    unitStore_After.insertElement(unitStore_After.new Element(invokeCC, lastPos));
    lastPos = invokeCC;

}