Java 类soot.jimple.internal.JimpleLocal 实例源码

public static Abstraction getZeroAbstraction(boolean flowSensitiveAliasing) {
    Abstraction zeroValue = new Abstraction(
            new AccessPath(new JimpleLocal("zero", NullType.v()), false),
            null,
            false,
            false);
    Abstraction.flowSensitiveAliasing = flowSensitiveAliasing;
    return zeroValue;
}

public void fill() {
    DomL domL = (DomL) doms[0];
    int numL = domL.size();
    for (int lIdx = 0; lIdx < numL; lIdx++) {
        Unit i = domL.get(lIdx);
        if (i instanceof JEnterMonitorStmt) {
            JEnterMonitorStmt em = (JEnterMonitorStmt) i;
            Value op = em.getOp();
            if (op instanceof JimpleLocal) {
                add(em, op);
            }
        }
    }
}

private Value findLocal(Value expr){
    Value ret = null;
    if(expr instanceof JimpleLocal){
        ret = expr;
    }
    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
                }
            }
        }
    }
}

public Pair<Value, Set<DefinitionStmt>> createZeroValue() {
    System.err.println("calling createZeroValue");
    return new Pair<Value, Set<DefinitionStmt>>(new JimpleLocal("<<zero>>",
            NullType.v()), Collections.<DefinitionStmt> emptySet());
}

public Pair<Value, Set<DefinitionStmt>> createZeroValue() {
    return new Pair<Value, Set<DefinitionStmt>>(new JimpleLocal("<<zero>>", NullType.v()), Collections.<DefinitionStmt> emptySet());
}

public TaintFact createZeroValue() {
    return new TaintFact(new JimpleLocal("<<zero>>", NullType.v()),Collections.<DefinitionStmt> emptySet());
}

public Pair<Value, Set<DefinitionStmt>> createZeroValue() {
    return new Pair<Value, Set<DefinitionStmt>>(new JimpleLocal("<<zero>>", NullType.v()), Collections.<DefinitionStmt> emptySet());
}

public Value createZeroValue() {
    return new JimpleLocal("<<zero>>", NullType.v());
}

@Override
public Local createZeroValue() {
    return new JimpleLocal("zero", NullType.v());
}

@Override
public Local createZeroValue() {
    return new JimpleLocal("<<zero>>", NullType.v());
}

public Register asTmpReg(Type regType) {
    String tmpRegName = "tmp" + getRegCount();
    return asLocal(new JimpleLocal(tmpRegName, regType));
}

public TrackFact createZeroValue() {
    return new TrackFact(new JimpleLocal("<<zero>>", NullType.v()) , null);
}

@Override
public Value createZeroValue() {
  return new JimpleLocal("zero", NullType.v());
}

@Override
public void visit(Value e) {
    if (e instanceof JimpleLocal) {
        add(e,(JimpleLocal) e);
    }
}

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

}

public static Abstraction getZeroAbstraction(boolean flowSensitiveAliasing) {
    if (zeroValue == null)
        zeroValue = new Abstraction(new JimpleLocal("zero", NullType.v()), null,
                null, false, true, null, flowSensitiveAliasing);
    return zeroValue;
}

@Override
public Value createZeroValue() {
  return new JimpleLocal("zero", NullType.v());
}