@@ -0,0 +1,2952 @@
+package wcanalysis.heuristic.model;%0A%0Aimport gov.nasa.jpf.symbc.numeric.PathCondition;%0Aimport gov.nasa.jpf.vm.ElementInfo;%0Aimport gov.nasa.jpf.vm.Heap;%0Aimport gov.nasa.jpf.vm.Instruction;%0Aimport gov.nasa.jpf.vm.ThreadInfo;%0Aimport gov.nasa.jpf.vm.VM;%0A%0A/**%0A * @author Kasper Luckow%0A * Simple statebuilder for tracking memory allocations along paths%0A */%0Apublic final class MaxLiveHeapState extends State %7B%0A  public final static class MaxLiveHeapStateBuilder extends StateBuilderAdapter %7B%0A%0A    private long maxLiveHeap = 0;%0A    %0A    public MaxLiveHeapStateBuilder() %7B%7D%0A    %0A    private MaxLiveHeapStateBuilder(long maxLiveHeap) %7B%0A      this.maxLiveHeap = maxLiveHeap;%0A    %7D%0A    %0A%0A    @Override%0A    public void handleObjectCreated(VM vm, ThreadInfo ti, ElementInfo ei) %7B%0A      %0A    %7D%0A    %0A    /**%0A     * This is extremely expensive: the size of the live objects in the heap, are analyzed%0A     * every time an instruction has been executed.%0A     * A much better idea is to only conduct this check whenever a scope will be exited%0A     * after the instruction is executed.%0A     * One way of doing that, is to generate the cfg of the method (with proper caching,%0A     * lazy construction, etc) and then to check if the instruction executed is the last%0A     * in a basic block and if the next block has multiple incoming edges. In that case%0A     * it is a candidate for checking live objects (still an over-approximation though -- %0A     * but better than now)%0A     */%0A    @Override%0A    public void handleInstructionExecuted(VM vm, ThreadInfo currentThread, Instruction nextInstruction,%0A        Instruction executedInstruction) %7B%0A      %0A      Heap heap = vm.getHeap();%0A      int currHeapSize = 0;%0A      for(ElementInfo info : heap.liveObjects()) %7B%0A        currHeapSize += info.getHeapSize();%0A      %7D%0A      if(currHeapSize %3E maxLiveHeap)%0A        maxLiveHeap = currHeapSize;%0A    %7D%0A    %0A    @Override%0A    public StateBuilder copy() %7B%0A      return new MaxLiveHeapStateBuilder(maxLiveHeap);%0A    %7D%0A    %0A    @Override%0A    public State build(PathCondition resultingPC) %7B%0A      return new MaxLiveHeapState(maxLiveHeap, resultingPC);%0A    %7D%0A  %7D%0A  %0A  private final long maxLiveHeap;%0A  %0A  private MaxLiveHeapState(long maxLiveHeap, PathCondition pc) %7B%0A    super(pc);%0A    this.maxLiveHeap = maxLiveHeap;%0A  %7D%0A%0A  @Override%0A  public String getCSVHeader() %7B%0A    return %22maxLiveHeap%22;%0A  %7D%0A%0A  @Override%0A  public String getCSV() %7B%0A    return String.valueOf(maxLiveHeap);%0A  %7D%0A%0A  @Override%0A  public int compareTo(State o) %7B%0A    if(!(o instanceof MaxLiveHeapState)) %7B%0A      throw new IllegalStateException(%22Expected state of type %22 + MaxLiveHeapState.class.getName());%0A    %7D%0A    %0A    MaxLiveHeapState other = (MaxLiveHeapState)o;%0A    return this.maxLiveHeap %3C other.maxLiveHeap ? -1:%0A      this.maxLiveHeap %3E other.maxLiveHeap ? 1 : 0;%0A  %7D%0A%0A  public long getMaxHeapSize() %7B%0A    return this.maxLiveHeap;%0A  %7D%0A  %0A  @Override%0A  public double getWC() %7B%0A    return this.getMaxHeapSize();%0A  %7D%0A%7D%0A

Add max live object heap size cost model