public class JvmDefaultExpandOperator<StateT extends LatticeAbstractState<StateT>> extends java.lang.Object implements ExpandOperator<JvmCfaNode,JvmCfaEdge,MethodSignature>, JvmAbstractStateFactory<StateT>
ExpandOperator
simulates the JVM behavior on a method exit.
In case of exit with a return instruction it takes the heap and the frame from the exit state of the called function and the local variables of the caller. Then pops the arguments of the call from the stack, pushes the return value, and creates an abstract state at the target of the intra-procedural call edge.
In case of exit with an exception besides performing the same reconstruction for local variables, heap, and static fields, it discards the operand stack of the caller and pushes the exception. The abstract successor location is either the first applicable catch node of the caller, if exists, or the exception exit node of the caller.
Constructor and Description |
---|
JvmDefaultExpandOperator(JvmCfa cfa)
Create the default expand operator for the JVM.
|
JvmDefaultExpandOperator(JvmCfa cfa,
boolean expandHeap)
Create the default expand operator for the JVM.
|
Modifier and Type | Method and Description |
---|---|
protected java.util.List<StateT> |
calculateReturnValues(AbstractState reducedExitState,
Instruction returnInstruction,
Call call)
Calculates the returned state.
|
JvmAbstractState<StateT> |
expand(AbstractState expandedInitialState,
AbstractState reducedExitState,
JvmCfaNode blockEntryNode,
Call call)
Reconstructs the state of the caller of a procedure using the information of the expanded
initial state, the reduced exit state, the block entry node (that can be used to retrieve the
CFA subgraph of the function), and the call to the procedure.
|
protected void |
expandHeap(JvmHeapAbstractState<StateT> heap,
JvmHeapAbstractState<StateT> callerHeap) |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
createJvmAbstractState
public JvmDefaultExpandOperator(JvmCfa cfa)
cfa
- the control flow automaton of the analyzed programpublic JvmDefaultExpandOperator(JvmCfa cfa, boolean expandHeap)
cfa
- the control flow automaton of the analyzed programexpandHeap
- whether expansion of the heap is performedpublic JvmAbstractState<StateT> expand(AbstractState expandedInitialState, AbstractState reducedExitState, JvmCfaNode blockEntryNode, Call call)
ExpandOperator
expand
in interface ExpandOperator<JvmCfaNode,JvmCfaEdge,MethodSignature>
expandedInitialState
- the entry state of the called procedure before any reductionreducedExitState
- the state of the called procedure in its exit nodeblockEntryNode
- the entry node of the called procedurecall
- the information of the call to the procedureRebuildOperator
to be solvedprotected java.util.List<StateT> calculateReturnValues(AbstractState reducedExitState, Instruction returnInstruction, Call call)
protected void expandHeap(JvmHeapAbstractState<StateT> heap, JvmHeapAbstractState<StateT> callerHeap)