Class ArrayBoundsGraph

java.lang.Object
com.ibm.wala.analysis.arraybounds.hypergraph.DirectedHyperGraph<Integer>
com.ibm.wala.analysis.arraybounds.ArrayBoundsGraph
public class ArrayBoundsGraph extends DirectedHyperGraph<Integer>
Some thoughts about implementation details, not mentioned in [1]:

As it is written The paper describes, that the distance is equal to the shortest hyper path. But what if we don't know anything about a variable (i.e. it is returned by a method)? There will be no path at all, the distance should be unlimited.

Initializing all nodes with -infinity instead of infinity, seems to work at first glance, as we also have hyper edges with more than one source, which cause the maximum to be propagated instead of minimum. However, this will not work, as loops will not get updated properly.

We need to make sure, that only nodes, which are not connected to the source of shortest path computation are set to infinity. To do so, it is enough to set nodes, which don't have a predecessor to infinity. (Nodes in cycles will always have an ancestor, which is not part of the cycle. So all nodes are either connected to the source, or a node with no predecessor.)

In this implementation this is done, by adding an infinity node and connect all lose ends to it (see ArrayBoundsGraphBuilder.bundleDeadEnds(ArrayBoundsGraph)). Note, that array length and the zero node are dead ends, if they are not the source of a shortest path computation. To prevent changing the inequality graph, depending on which source is used, a kind of trap door construct is used (See createSourceVar(Integer)).

There are some variations, but these are minor changes to improve results:

[1] Bodík, Rastislav, Rajiv Gupta, and Vivek Sarkar. "ABCD: eliminating array bounds checks on demand." ACM SIGPLAN Notices. Vol. 35. No. 5. ACM, 2000.
Author:
Stephan Gocht <stephan@gobro.de>

  • Field Details

    • ZERO

      public static final Integer ZERO
      We need a ssa variable representing zero. So we just use an integer, which is never produced by ssa generation

    • ZERO_HELPER

      public static final Integer ZERO_HELPER

    • UNLIMITED

      public static final Integer UNLIMITED
      We need a ssa variable representing unlimited (values we don't know anything about). So we just use an integer, which is never produced by ssa generation

  • Constructor Details

    • ArrayBoundsGraph

      public ArrayBoundsGraph()

  • Method Details

    • postProcessConstants

      public void postProcessConstants()

    • addAdditionEdge

      public void addAdditionEdge(Integer src, Integer dst, Integer value)

    • addArray

      public void addArray(Integer array)

    • addConstant

      public void addConstant(Integer variable, Integer value)
      Add variable as constant with value value.

      This will create the following construct: [zero] -(value)-> [h1] -0- > [variable] -(-value)-> [h2] -0-> [zero].

      The bidirectional linking, allows things like 

       int[] a = new int[2]();
 a[0] = 1;
      to work properly. h1, h2 are helper nodes: [zero] and [variable] may have other predecessors, this will cause their in edges to be merged to a single hyper edge with weight zero. The helper nodes are inserted to keep the proper distance from [zero].

    • addEdge

      public void addEdge(Integer src, Integer dst)

    • addNode

      public HyperNode<Integer> addNode(Integer value)

    • addPhi

      public void addPhi(Integer dst)

    • addPi

      public void addPi(Integer dst, Integer src1, Integer src2)

    • createSourceVar

      public void createSourceVar(Integer var)
      Adds var as source var. A source var is a variable, which can be used as source for shortest path computation.

      This will create the following construct: [unlimited] -> [var] -> [var] -(unlimited)-> [unlimited]

      This is a trap door construct: if [var] is not set to 0 it will get the value unlimited, if [var] is set to 0 it will stay 0.

    • generateNewVar

      public Integer generateNewVar()

    • getArrayAccess

      public HashMap<Integer,Set<Integer>> getArrayAccess()

    • getArrayLength

      public HashMap<Integer,Integer> getArrayLength()

    • getArrayNode

      public Integer getArrayNode(Integer array)

    • getPhis

      public HashSet<Integer> getPhis()

    • markAsArrayAccess

      public void markAsArrayAccess(Integer array, Integer index)

    • markAsArrayLength

      public void markAsArrayLength(Integer array, Integer variable)
      Mark variable as length for array.

    • markAsDeadEnd

      public void markAsDeadEnd(Integer variable)

    • getVariableWeight

      public Weight getVariableWeight(Integer variable)

    • reset

      public void reset()
      Description copied from class: DirectedHyperGraph
      Resets the weight of all nodes.
      Overrides:
      reset in class DirectedHyperGraph<Integer>