Added an array out of bounds analysis.

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/ArrayBoundsGraph.java

@@ -0,0 +1,269 @@
+package com.ibm.wala.analysis.arraybounds;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Set;
+
+import com.ibm.wala.analysis.arraybounds.hypergraph.DirectedHyperEdge;
+import com.ibm.wala.analysis.arraybounds.hypergraph.DirectedHyperGraph;
+import com.ibm.wala.analysis.arraybounds.hypergraph.HyperNode;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight.Type;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.edgeweights.AdditiveEdgeWeight;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.edgeweights.EdgeWeight;
+
+/**
+ * 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
+ * {@link 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
+ * {@link ArrayBoundsGraph#createSourceVar(Integer)}).
+ *
+ * There are some variations, but these are minor changes to improve results:
+ * <ul>
+ * <li>handling of constants (see
+ * {@link ArrayBoundsGraph#addConstant(Integer, Integer)})
+ * <li>pi nodes (see {@link ArrayBoundsGraph#addPhi(Integer, Integer, Integer)})
+ * <li>array length nodes (see {@link ArrayBoundsGraph#arrayLength})
+ * </ul>
+ *
+ * [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>
+ */
+public class ArrayBoundsGraph extends DirectedHyperGraph<Integer> {
+	/**
+	 * We need a ssa variable representing zero. So we just use an integer,
+	 * which is never produced by ssa generation
+	 */
+	public final static Integer ZERO = -1;
+	/**
+	 * 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
+	 */
+	public final static Integer UNLIMITED = -2;
+
+	/**
+	 * Maps each array variable to a set of variables, which are used as Index
+	 * for accessing that array
+	 */
+	private final HashMap<Integer, Set<Integer>> arrayAccess;
+
+	/**
+	 * Maps each array variable to a node which is parent to all variables, that
+	 * contain the array length
+	 */
+	private final HashMap<Integer, Integer> arrayLength;
+
+	private final HashSet<Integer> phis;
+
+	/**
+	 * For simplicity we introduce extra variables, for arrayLength, to have a
+	 * unique node representing the array length, even if the length is accessed
+	 * more than once in the code.
+	 *
+	 * Start with -3 so it is unequal to other constants
+	 */
+	private Integer arrayCounter = -3;
+
+	public ArrayBoundsGraph() {
+		this.arrayAccess = new HashMap<>();
+		this.arrayLength = new HashMap<>();
+		this.phis = new HashSet<>();
+		this.addNode(UNLIMITED);
+		this.phis.add(UNLIMITED);
+		this.createSourceVar(ZERO);
+	}
+
+	public void addAdditionEdge(Integer src, Integer dst, Integer value) {
+		this.addNode(src);
+		final HyperNode<Integer> srcNode = this.getNodes().get(src);
+
+		this.addNode(dst);
+		final HyperNode<Integer> dstNode = this.getNodes().get(dst);
+
+		Weight weight;
+		if (value == 0) {
+			weight = Weight.ZERO;
+		} else {
+			weight = new Weight(Type.NUMBER, value);
+		}
+
+		final EdgeWeight edgeWeight = new AdditiveEdgeWeight(weight);
+
+		final DirectedHyperEdge<Integer> edge = new DirectedHyperEdge<Integer>();
+		edge.getDestination().add(dstNode);
+		edge.getSource().add(srcNode);
+		edge.setWeight(edgeWeight);
+
+		this.getEdges().add(edge);
+	}
+
+	public void addArray(Integer array) {
+		this.getArrayNode(array);
+	}
+
+	/**
+	 * 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
+	 *
+	 * <pre>
+	 * int[] a = new int[2]();
+	 * a[0] = 1;
+	 * </pre>
+	 *
+	 * 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].
+	 *
+	 * @param variable
+	 * @param value
+	 */
+	public void addConstant(Integer variable, Integer value) {
+		final Integer helper1 = this.generateNewVar();
+		final Integer helper2 = this.generateNewVar();
+
+		this.addAdditionEdge(ZERO, helper1, value);
+		this.addEdge(helper1, variable);
+		this.addAdditionEdge(variable, helper2, -value);
+		this.addEdge(helper2, ZERO);
+	}
+
+	public void addEdge(Integer src, Integer dst) {
+		this.addAdditionEdge(src, dst, 0);
+	}
+
+	public HyperNode<Integer> addNode(Integer value) {
+		HyperNode<Integer> result;
+		if (!this.getNodes().keySet().contains(value)) {
+			result = new HyperNode<Integer>(value);
+			this.getNodes().put(value, result);
+		} else {
+			result = this.getNodes().get(value);
+		}
+		return result;
+	}
+
+	public void addPhi(Integer dst, Integer src1, Integer src2) {
+		this.phis.add(dst);
+		this.addEdge(src1, dst);
+		this.addEdge(src2, dst);
+	}
+
+	public void addPi(Integer dst, Integer src1, Integer src2) {
+		this.addEdge(src1, dst);
+		this.addEdge(src2, dst);
+	}
+
+	/**
+	 * 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.
+	 *
+	 * @param var
+	 */
+	public void createSourceVar(Integer var) {
+		this.addNode(var);
+
+		final HyperNode<Integer> arrayNode = this.getNodes().get(var);
+		final HyperNode<Integer> unlimitedNode = this.getNodes().get(UNLIMITED);
+
+		final DirectedHyperEdge<Integer> edge = new DirectedHyperEdge<>();
+		edge.setWeight(new AdditiveEdgeWeight(Weight.UNLIMITED));
+		edge.getSource().add(arrayNode);
+		edge.getDestination().add(unlimitedNode);
+		this.getEdges().add(edge);
+
+		this.addEdge(UNLIMITED, var);
+		this.addEdge(var, var);
+	}
+
+	public Integer generateNewVar() {
+		final int result = this.arrayCounter;
+		this.arrayCounter += -1;
+		return result;
+	}
+
+	public HashMap<Integer, Set<Integer>> getArrayAccess() {
+		return this.arrayAccess;
+	}
+
+	public HashMap<Integer, Integer> getArrayLength() {
+		return this.arrayLength;
+	}
+
+	public Integer getArrayNode(Integer array) {
+		Integer arrayVar;
+		if (!this.arrayLength.containsKey(array)) {
+			arrayVar = this.generateNewVar();
+			this.arrayLength.put(array, arrayVar);
+			this.createSourceVar(arrayVar);
+		} else {
+			arrayVar = this.arrayLength.get(array);
+		}
+		return arrayVar;
+	}
+
+	public HashSet<Integer> getPhis() {
+		return this.phis;
+	}
+
+	public void markAsArrayAccess(Integer array, Integer index) {
+		Set<Integer> indices;
+		if (!this.arrayAccess.containsKey(array)) {
+			indices = new HashSet<Integer>();
+			this.arrayAccess.put(array, indices);
+		} else {
+			indices = this.arrayAccess.get(array);
+		}
+		indices.add(index);
+		this.addArray(array);
+	}
+
+	/**
+	 * Mark variable as length for array.
+	 *
+	 * @param array
+	 * @param variable
+	 */
+	public void markAsArrayLength(Integer array, Integer variable) {
+		this.addEdge(this.getArrayNode(array), variable);
+	}
+
+	public void markAsDeadEnd(Integer variable) {
+		this.addEdge(UNLIMITED, variable);
+	}
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/ArrayBoundsGraphBuilder.java

@@ -0,0 +1,390 @@
+package com.ibm.wala.analysis.arraybounds;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+import java.util.Stack;
+
+import com.ibm.wala.analysis.arraybounds.hypergraph.DirectedHyperEdge;
+import com.ibm.wala.analysis.arraybounds.hypergraph.HyperNode;
+import com.ibm.wala.shrikeBT.IBinaryOpInstruction;
+import com.ibm.wala.shrikeBT.IConditionalBranchInstruction.Operator;
+import com.ibm.wala.ssa.DefUse;
+import com.ibm.wala.ssa.IR;
+import com.ibm.wala.ssa.SSAArrayLengthInstruction;
+import com.ibm.wala.ssa.SSAArrayLoadInstruction;
+import com.ibm.wala.ssa.SSAArrayReferenceInstruction;
+import com.ibm.wala.ssa.SSAArrayStoreInstruction;
+import com.ibm.wala.ssa.SSABinaryOpInstruction;
+import com.ibm.wala.ssa.SSACFG.BasicBlock;
+import com.ibm.wala.ssa.SSAConditionalBranchInstruction;
+import com.ibm.wala.ssa.SSAInstruction;
+import com.ibm.wala.ssa.SSAInstruction.Visitor;
+import com.ibm.wala.ssa.SSANewInstruction;
+import com.ibm.wala.ssa.SSAPhiInstruction;
+import com.ibm.wala.ssa.SSAPiInstruction;
+
+/**
+ * @see ArrayBoundsGraph
+ * @author Stephan Gocht <stephan@gobro.de>
+ */
+public class ArrayBoundsGraphBuilder {
+	private final IR ir;
+	/** Variables, which were already explored. */
+	private final HashSet<Integer> foundVariables;
+	private final DefUse defUse;
+
+	private final ArrayBoundsGraph lowerBoundGraph;
+
+	private final ArrayBoundsGraph upperBoundGraph;
+	private final Set<SSAArrayReferenceInstruction> arrayReferenceInstructions;
+	private final IBinaryOpInstruction.Operator SUB = IBinaryOpInstruction.Operator.SUB;
+
+	private final IBinaryOpInstruction.Operator ADD = IBinaryOpInstruction.Operator.ADD;
+
+	public ArrayBoundsGraphBuilder(IR ir) {
+		this.ir = ir;
+
+		this.foundVariables = new HashSet<Integer>();
+		this.defUse = new DefUse(ir);
+
+		this.arrayReferenceInstructions = new HashSet<>();
+		this.lowerBoundGraph = new ArrayBoundsGraph();
+		this.upperBoundGraph = new ArrayBoundsGraph();
+
+		this.findArrayAccess();
+		this.exploreIr();
+		this.addConstructionLength();
+
+		this.bundleDeadEnds(this.lowerBoundGraph);
+		this.bundleDeadEnds(this.upperBoundGraph);
+
+		this.collapseNonPhiEdges(this.lowerBoundGraph);
+		this.collapseNonPhiEdges(this.upperBoundGraph);
+
+		this.lowerBoundGraph.updateNodeEdges();
+		this.upperBoundGraph.updateNodeEdges();
+	}
+
+	private void addConstructionLength() {
+
+		for (final Integer array : this.lowerBoundGraph.getArrayLength()
+				.keySet()) {
+			final Integer tmp = array;
+
+			final SSAInstruction instruction = this.defUse.getDef(array);
+			if (instruction != null) {
+				instruction.visit(new Visitor() {
+					@Override
+					public void visitNew(SSANewInstruction instruction) {
+						assert instruction.getNumberOfUses() == 1;
+						final int constructionLength = instruction.getUse(0);
+						Integer arraysNode = ArrayBoundsGraphBuilder.this.lowerBoundGraph
+								.getArrayLength().get(tmp);
+						ArrayBoundsGraphBuilder.this.lowerBoundGraph.addEdge(
+								arraysNode, constructionLength);
+						arraysNode = ArrayBoundsGraphBuilder.this.upperBoundGraph
+								.getArrayLength().get(tmp);
+						ArrayBoundsGraphBuilder.this.upperBoundGraph.addEdge(
+								arraysNode, constructionLength);
+
+						ArrayBoundsGraphBuilder.this
+						.addPossibleConstant(constructionLength);
+					}
+				});
+			}
+		}
+
+	}
+
+	/**
+	 * Case 1: piRestrictor restricts the pi variable for upper/ lower bounds graph
+	 * Given this code below, we want to create a hyper edge
+	 * {piParent, piRestrictor} --> {piVar}.
+	 *
+	 * If is op in {<, >} we now, that the distance from piRestrictor to piVar
+	 * is +-1 as ( a < b ) <==> ( a <= b - 1), same with "<".
+	 * To be more precise we introduce a helper node and add
+	 * {piRestrictor} -- (-)1 --> {helper}
+	 * {piParent, helper} --> {piVar}
+	 *
+	 * Case 2: no restriction is given by the branch (i.e. the operator is not equal)
+	 * {piParent} --> {piVar}
+	 *
+	 * <code>if (piParent op piRestrictor) {piVar = piParent}</code>
+	 *
+	 * @param piVar
+	 * @param piParent
+	 * @param piRestrictor
+	 * @param op
+	 */
+	private void addPiStructure(Integer piVar, Integer piParent,
+			Integer piRestrictor, Operator op) {
+
+		Integer helper;
+		switch (op) {
+		case EQ:
+			this.upperBoundGraph.addPi(piVar, piParent, piRestrictor);
+			this.lowerBoundGraph.addPi(piVar, piParent, piRestrictor);
+			break;
+		case NE:
+			this.upperBoundGraph.addEdge(piParent, piVar);
+			this.lowerBoundGraph.addEdge(piParent, piVar);
+			break;
+		case LE: // piVar <= piRestrictor
+			this.upperBoundGraph.addPi(piVar, piParent, piRestrictor);
+
+			this.lowerBoundGraph.addEdge(piParent, piVar);
+			break;
+		case GE: // piVar >= piRestrictor
+			this.lowerBoundGraph.addPi(piVar, piParent, piRestrictor);
+
+			this.upperBoundGraph.addEdge(piParent, piVar);
+			break;
+		case LT: // piVar < piRestrictor
+			helper = this.upperBoundGraph.generateNewVar();
+			this.upperBoundGraph.addAdditionEdge(piRestrictor, helper, -1);
+			this.upperBoundGraph.addPi(piVar, piParent, helper);
+
+			this.lowerBoundGraph.addEdge(piParent, piVar);
+			break;
+		case GT: // piVar > piRestrictor
+			helper = this.lowerBoundGraph.generateNewVar();
+			this.lowerBoundGraph.addAdditionEdge(piRestrictor, helper, 1);
+			this.lowerBoundGraph.addPi(piVar, piParent, helper);
+
+			this.upperBoundGraph.addEdge(piParent, piVar);
+			break;
+		}
+
+	}
+
+	private void addPossibleConstant(int handle) {
+		if (this.ir.getSymbolTable().isIntegerConstant(handle)) {
+			final int value = this.ir.getSymbolTable().getIntValue(handle);
+			this.lowerBoundGraph.addConstant(handle, value);
+			this.upperBoundGraph.addConstant(handle, value);
+		}
+	}
+
+	/**
+	 * Connect all lose ends to the infinity node. See the description of
+	 * {@link ArrayBoundsGraph} for why this is necessary.
+	 *
+	 * @param graph
+	 */
+	private void bundleDeadEnds(ArrayBoundsGraph graph) {
+		final Set<HyperNode<Integer>> nodes = new HashSet<>();
+		nodes.addAll(graph.getNodes().values());
+
+		for (final DirectedHyperEdge<Integer> edge : graph.getEdges()) {
+			for (final HyperNode<Integer> node : edge.getDestination()) {
+				nodes.remove(node);
+			}
+		}
+
+		for (final HyperNode<Integer> node : nodes) {
+			graph.markAsDeadEnd(node.getValue());
+		}
+	}
+
+	/**
+	 * To make construction of the hyper-graph more easy, we always add single
+	 * edges and fuse them into one hyper-edge. Where necessary (Everywhere but
+	 * incoming edges of phi nodes.)
+	 *
+	 * @param graph
+	 */
+	private void collapseNonPhiEdges(ArrayBoundsGraph graph) {
+		final Map<HyperNode<Integer>, DirectedHyperEdge<Integer>> inEdges = new HashMap<HyperNode<Integer>, DirectedHyperEdge<Integer>>();
+		final Set<DirectedHyperEdge<Integer>> edges = new HashSet<>();
+		edges.addAll(graph.getEdges());
+		for (final DirectedHyperEdge<Integer> edge : edges) {
+			assert edge.getDestination().size() == 1;
+
+			final HyperNode<Integer> node = edge.getDestination().iterator()
+					.next();
+			if (!graph.getPhis().contains(node.getValue())) {
+				if (inEdges.containsKey(node)) {
+					final DirectedHyperEdge<Integer> inEdge = inEdges.get(node);
+					assert inEdge.getWeight().equals(edge.getWeight());
+					for (final HyperNode<Integer> src : edge.getSource()) {
+						inEdge.getSource().add(src);
+					}
+					graph.getEdges().remove(edge);
+				} else {
+					inEdges.put(node, edge);
+				}
+			}
+		}
+	}
+
+	/**
+	 * Discovers predecessors and adds them to the graph.
+	 *
+	 * @param todo
+	 * @param handle
+	 */
+	private void discoverPredecessors(final Stack<Integer> todo, int handle) {
+		final SSAInstruction def = this.defUse.getDef(handle);
+		if (def == null) {
+			this.addPossibleConstant(handle);
+		} else {
+			def.visit(new Visitor() {
+				@Override
+				public void visitArrayLength(
+						SSAArrayLengthInstruction instruction) {
+					ArrayBoundsGraphBuilder.this.lowerBoundGraph
+					.markAsArrayLength(instruction.getArrayRef(),
+							instruction.getDef());
+					ArrayBoundsGraphBuilder.this.upperBoundGraph
+					.markAsArrayLength(instruction.getArrayRef(),
+							instruction.getDef());
+				}
+
+				@Override
+				public void visitBinaryOp(SSABinaryOpInstruction instruction) {
+					if (instruction.getOperator() == ArrayBoundsGraphBuilder.this.SUB
+							|| instruction.getOperator() == ArrayBoundsGraphBuilder.this.ADD) {
+						final BinaryOpWithConstant op = BinaryOpWithConstant
+								.create(instruction,
+										ArrayBoundsGraphBuilder.this.ir);
+
+						if (op != null) {
+							todo.push(op.getOtherVar());
+							int value = op.getConstantValue();
+							if (instruction.getOperator() == ArrayBoundsGraphBuilder.this.SUB) {
+								value = -value;
+							}
+							ArrayBoundsGraphBuilder.this.lowerBoundGraph
+							.addAdditionEdge(op.getOtherVar(),
+									instruction.getDef(), value);
+							ArrayBoundsGraphBuilder.this.upperBoundGraph
+							.addAdditionEdge(op.getOtherVar(),
+									instruction.getDef(), value);
+
+						}
+					}
+				}
+
+				@Override
+				public void visitPhi(SSAPhiInstruction instruction) {
+					assert instruction.getNumberOfUses() == 2;
+					todo.push(instruction.getUse(0));
+					todo.push(instruction.getUse(1));
+
+					ArrayBoundsGraphBuilder.this.lowerBoundGraph.addPhi(
+							instruction.getDef(), instruction.getUse(0),
+							instruction.getUse(1));
+					ArrayBoundsGraphBuilder.this.upperBoundGraph.addPhi(
+							instruction.getDef(), instruction.getUse(0),
+							instruction.getUse(1));
+				}
+
+				@Override
+				public void visitPi(SSAPiInstruction instruction) {
+					final SSAConditionalBranchInstruction branch = (SSAConditionalBranchInstruction) instruction
+							.getCause();
+					assert branch.getNumberOfUses() == 2;
+
+					final Integer piVar = instruction.getDef();
+					final Integer piParent = instruction.getUse(0);
+
+					final ConditionNormalizer cnd = new ConditionNormalizer(
+							branch, piParent, ArrayBoundsGraphBuilder.this
+							.isBranchTaken(instruction, branch));
+
+					final Integer piRestrictor = cnd.getRhs();
+
+					todo.push(piParent);
+					todo.push(piRestrictor);
+
+					ArrayBoundsGraphBuilder.this.addPiStructure(piVar,
+							piParent, piRestrictor, cnd.getOp());
+				}
+			});
+		}
+	}
+
+	private void exploreIr() {
+		final Set<Integer> variablesUsedAsIndex = new HashSet<Integer>();
+		for (final Set<Integer> variables : this.lowerBoundGraph
+				.getArrayAccess().values()) {
+			variablesUsedAsIndex.addAll(variables);
+		}
+
+		for (final Integer variable : variablesUsedAsIndex) {
+			this.startDFS(variable);
+		}
+	}
+
+	private void findArrayAccess() {
+		this.ir.visitNormalInstructions(new Visitor() {
+			@Override
+			public void visitArrayLoad(SSAArrayLoadInstruction instruction) {
+				ArrayBoundsGraphBuilder.this.lowerBoundGraph.markAsArrayAccess(
+						instruction.getArrayRef(), instruction.getIndex());
+				ArrayBoundsGraphBuilder.this.upperBoundGraph.markAsArrayAccess(
+						instruction.getArrayRef(), instruction.getIndex());
+
+				ArrayBoundsGraphBuilder.this.arrayReferenceInstructions
+				.add(instruction);
+			}
+
+			@Override
+			public void visitArrayStore(SSAArrayStoreInstruction instruction) {
+				ArrayBoundsGraphBuilder.this.lowerBoundGraph.markAsArrayAccess(
+						instruction.getArrayRef(), instruction.getIndex());
+				ArrayBoundsGraphBuilder.this.upperBoundGraph.markAsArrayAccess(
+						instruction.getArrayRef(), instruction.getIndex());
+
+				ArrayBoundsGraphBuilder.this.arrayReferenceInstructions
+				.add(instruction);
+			}
+		});
+
+	}
+
+	public Set<SSAArrayReferenceInstruction> getArrayReferenceInstructions() {
+		return this.arrayReferenceInstructions;
+	}
+
+	public ArrayBoundsGraph getLowerBoundGraph() {
+		return this.lowerBoundGraph;
+	}
+
+	public ArrayBoundsGraph getUpperBoundGraph() {
+		return this.upperBoundGraph;
+	}
+
+	private boolean isBranchTaken(SSAPiInstruction pi,
+			SSAConditionalBranchInstruction cnd) {
+		final BasicBlock branchTargetBlock = this.ir.getControlFlowGraph()
+				.getBlockForInstruction(cnd.getTarget());
+
+		return branchTargetBlock.getNumber() == pi.getSuccessor();
+	}
+
+	/**
+	 * Explore the DefUse-Chain with depth-first-search to add constraints to
+	 * the given variable.
+	 */
+	private void startDFS(int index) {
+		final Stack<Integer> todo = new Stack<Integer>();
+		todo.push(index);
+
+		while (!todo.isEmpty()) {
+			final int next = todo.pop();
+			if (!this.foundVariables.contains(next)) {
+				this.foundVariables.add(next);
+				this.lowerBoundGraph.addNode(next);
+				this.upperBoundGraph.addNode(next);
+
+				this.discoverPredecessors(todo, next);
+			}
+		}
+
+	}
+
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/ArrayOutOfBoundsAnalysis.java

@@ -0,0 +1,138 @@
+package com.ibm.wala.analysis.arraybounds;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+
+import com.ibm.wala.analysis.arraybounds.hypergraph.HyperNode;
+import com.ibm.wala.analysis.arraybounds.hypergraph.algorithms.ShortestPath;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.NormalOrder;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.ReverseOrder;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight;
+import com.ibm.wala.ssa.IR;
+import com.ibm.wala.ssa.SSAArrayReferenceInstruction;
+
+/**
+ * The array out of bounds analysis uses the inequality graph as described in
+ * [1]. And a shortest path computation as suggested ibid. as possible solver
+ * for the inequality graph.
+ *
+ * [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>
+ *
+ */
+public class ArrayOutOfBoundsAnalysis {
+  public enum UnnecessaryCheck {
+    NONE, UPPER, LOWER, BOTH;
+
+    public UnnecessaryCheck union(UnnecessaryCheck other) {
+      final Set<UnnecessaryCheck> set = new HashSet<>();
+      set.add(this);
+      set.add(other);
+      set.remove(NONE);
+      if (set.contains(BOTH) || (set.contains(UPPER) && set.contains(LOWER))) {
+        return BOTH;
+      } else if (set.size() == 0) {
+        return NONE;
+      } else if (set.size() == 1) {
+        return set.iterator().next();
+      } else {
+        throw new RuntimeException("Case that should not happen, this method is implemented wrong.");
+      }
+    }
+  }
+
+  private ArrayBoundsGraph lowerBoundGraph;
+  private ArrayBoundsGraph upperBoundGraph;
+
+  /**
+   * List of variables, that are used for array access and if they are
+   * neccessary
+   */
+  private final Map<SSAArrayReferenceInstruction, UnnecessaryCheck> boundsCheckUnnecessary;
+
+  /**
+   * Create and perform the array out of bounds analysis.
+   * 
+   * Make sure, the given IR was created with pi nodes for each variable, that
+   * is part of a branch instruction! Otherwise the results will be poor.
+   * 
+   * @param ir
+   */
+  public ArrayOutOfBoundsAnalysis(IR ir) {
+    this.boundsCheckUnnecessary = new HashMap<>();
+    this.buildInequalityGraphs(ir);
+
+    this.computeLowerBound();
+    this.computeUpperBounds();
+
+    this.lowerBoundGraph = null;
+    this.upperBoundGraph = null;
+  }
+
+  private void addUnnecessaryCheck(SSAArrayReferenceInstruction instruction, UnnecessaryCheck checkToAdd) {
+    final UnnecessaryCheck oldCheck = this.boundsCheckUnnecessary.get(instruction);
+    final UnnecessaryCheck newCheck = oldCheck.union(checkToAdd);
+    this.boundsCheckUnnecessary.put(instruction, newCheck);
+  }
+
+  private void buildInequalityGraphs(IR ir) {
+    ArrayBoundsGraphBuilder builder = new ArrayBoundsGraphBuilder(ir);
+    this.lowerBoundGraph = builder.getLowerBoundGraph();
+    this.upperBoundGraph = builder.getUpperBoundGraph();
+
+    for (final SSAArrayReferenceInstruction instruction : builder.getArrayReferenceInstructions()) {
+      this.boundsCheckUnnecessary.put(instruction, UnnecessaryCheck.NONE);
+    }
+    builder = null;
+  }
+
+  /**
+   * compute lower bound
+   */
+  private void computeLowerBound() {
+    final HyperNode<Integer> zero = this.lowerBoundGraph.getNodes().get(ArrayBoundsGraph.ZERO);
+    ShortestPath.compute(this.lowerBoundGraph, zero, new NormalOrder());
+
+    for (final SSAArrayReferenceInstruction instruction : this.boundsCheckUnnecessary.keySet()) {
+      final HyperNode<Integer> node = this.lowerBoundGraph.getNodes().get(instruction.getIndex());
+      if (node.getWeight().getType() == Weight.Type.NUMBER && node.getWeight().getNumber() >= 0) {
+        this.addUnnecessaryCheck(instruction, UnnecessaryCheck.LOWER);
+      }
+    }
+  }
+
+  /**
+   * compute upper bound for each array
+   */
+  private void computeUpperBounds() {
+    final Map<Integer, Integer> arrayLengths = this.upperBoundGraph.getArrayLength();
+    for (final Integer array : arrayLengths.keySet()) {
+      final HyperNode<Integer> arrayNode = this.upperBoundGraph.getNodes().get(arrayLengths.get(array));
+
+      ShortestPath.compute(this.upperBoundGraph, arrayNode, new ReverseOrder());
+
+      for (final SSAArrayReferenceInstruction instruction : this.boundsCheckUnnecessary.keySet()) {
+        if (instruction.getArrayRef() == array) {
+          final HyperNode<Integer> node = this.upperBoundGraph.getNodes().get(instruction.getIndex());
+          if (node.getWeight().getType() == Weight.Type.NUMBER && node.getWeight().getNumber() <= -1) {
+
+            this.addUnnecessaryCheck(instruction, UnnecessaryCheck.UPPER);
+          }
+        }
+      }
+    }
+  }
+
+  /**
+   * @return for each array reference instruction (load or store), if both,
+   *         lower bound, upper bound or no check is unnecessary.
+   */
+  public Map<SSAArrayReferenceInstruction, UnnecessaryCheck> getBoundsCheckNecessary() {
+    return this.boundsCheckUnnecessary;
+  }
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/BinaryOpWithConstant.java

@@ -0,0 +1,87 @@
+package com.ibm.wala.analysis.arraybounds;
+
+import com.ibm.wala.shrikeBT.IBinaryOpInstruction.IOperator;
+import com.ibm.wala.shrikeBT.IBinaryOpInstruction.Operator;
+import com.ibm.wala.ssa.IR;
+import com.ibm.wala.ssa.SSABinaryOpInstruction;
+
+/**
+ * Normalizes a binary operation with a constant by providing direct access to
+ * assigned = other op constant.
+ *
+ * @author Stephan Gocht <stephan@gobro.de>
+ *
+ */
+public class BinaryOpWithConstant {
+	/**
+	 *
+	 * @param instruction
+	 * @param ir
+	 * @return normalized BinaryOpWithConstant or null, if normalization was not
+	 *         successful.
+	 */
+	public static BinaryOpWithConstant create(
+			SSABinaryOpInstruction instruction, IR ir) {
+		BinaryOpWithConstant result = null;
+
+		if (instruction.mayBeIntegerOp()) {
+			assert instruction.getNumberOfUses() == 2;
+			Integer other = null;
+			Integer value = null;
+
+			int constantPos = -1;
+			for (int i = 0; i < instruction.getNumberOfUses(); i++) {
+				final int constant = instruction.getUse(i);
+				if (ir.getSymbolTable().isIntegerConstant(constant)) {
+					other = instruction.getUse((i + 1) % 2);
+					value = ir.getSymbolTable().getIntValue(constant);
+					constantPos = i;
+				}
+			}
+
+			final IOperator op = instruction.getOperator();
+
+			if (constantPos != -1) {
+				if (op == Operator.ADD || op == Operator.SUB
+						&& constantPos == 1) {
+					result = new BinaryOpWithConstant(op, other, value,
+							instruction.getDef());
+				}
+			}
+		}
+
+		return result;
+	}
+
+	private final IOperator op;
+	private final Integer other;
+
+	private final Integer value;
+
+	private final Integer assigned;
+
+	private BinaryOpWithConstant(IOperator op, Integer other, Integer value,
+			Integer assigned) {
+		super();
+		this.op = op;
+		this.other = other;
+		this.value = value;
+		this.assigned = assigned;
+	}
+
+	public Integer getAssignedVar() {
+		return this.assigned;
+	}
+
+	public Integer getConstantValue() {
+		return this.value;
+	}
+
+	public IOperator getOp() {
+		return this.op;
+	}
+
+	public Integer getOtherVar() {
+		return this.other;
+	}
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/ConditionNormalizer.java

@@ -0,0 +1,115 @@
+package com.ibm.wala.analysis.arraybounds;
+
+import com.ibm.wala.shrikeBT.IConditionalBranchInstruction.Operator;
+import com.ibm.wala.ssa.SSAConditionalBranchInstruction;
+
+/**
+ * ConditionNormalizer normalizes a branch condition. See Constructor for more
+ * information.
+ *
+ * @author Stephan Gocht <stephan@gobro.de>
+ *
+ */
+public class ConditionNormalizer {
+	private final int lhs;
+	private int rhs;
+	private Operator op;
+
+	/**
+	 * Creates a normalization of cnd such that lhs op rhs is true.
+	 *
+	 * Normalization means, that the given variable lhs, will be on the left
+	 * hand side of the comparison, also if the branch is not taken, the
+	 * operation needs to be negated.
+	 *
+	 * p.a. the condition is !(rhs >= lhs), it will be normalized to lhs > rhs
+	 *
+	 * @param cnd
+	 *            condition to normalize
+	 * @param lhs
+	 *            variable, that should be on the left hand side
+	 * @param branchIsTaken
+	 *            if the condition is for the branching case or not
+	 */
+	public ConditionNormalizer(SSAConditionalBranchInstruction cnd, int lhs,
+			boolean branchIsTaken) {
+		this.lhs = lhs;
+
+		if (cnd.getNumberOfUses() != 2) {
+			throw new IllegalArgumentException(
+					"Condition uses not exactly two variables.");
+		}
+
+		this.op = (Operator) cnd.getOperator();
+		for (int i = 0; i < cnd.getNumberOfUses(); i++) {
+			final int var = cnd.getUse(i);
+			if ((var != lhs)) {
+				if (cnd.getUse((i + 1) % 2) != lhs) {
+					throw new IllegalArgumentException(
+							"Lhs not contained in condition.");
+				}
+
+				if (i == 0) {
+					// make sure the other is lhs
+					this.op = this.swapOperator(this.op);
+				}
+				if (!branchIsTaken) {
+					this.op = this.negateOperator(this.op);
+				}
+				this.rhs = var;
+			}
+		}
+	}
+
+	public int getLhs() {
+		return this.lhs;
+	}
+
+	public Operator getOp() {
+		return this.op;
+	}
+
+	public int getRhs() {
+		return this.rhs;
+	}
+
+	private Operator negateOperator(Operator op) {
+		switch (op) {
+		case EQ:
+			return Operator.NE;
+		case NE:
+			return Operator.EQ;
+		case LT:
+			return Operator.GE;
+		case GE:
+			return Operator.LT;
+		case GT:
+			return Operator.LE;
+		case LE:
+			return Operator.GT;
+		default:
+			throw new RuntimeException(
+					"Programming Error: Got unknown operator.");
+		}
+	}
+
+	private Operator swapOperator(Operator op) {
+		switch (op) {
+		case EQ:
+			return op;
+		case NE:
+			return op;
+		case LT:
+			return Operator.GT;
+		case GE:
+			return Operator.LE;
+		case GT:
+			return Operator.LT;
+		case LE:
+			return Operator.GE;
+		default:
+			throw new RuntimeException(
+					"Programming Error: Got unknown operator.");
+		}
+	}
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/hypergraph/DirectedHyperEdge.java

@@ -0,0 +1,46 @@
+package com.ibm.wala.analysis.arraybounds.hypergraph;
+
+import java.util.HashSet;
+import java.util.Set;
+
+import com.ibm.wala.analysis.arraybounds.hypergraph.DirectedHyperGraph;
+import com.ibm.wala.analysis.arraybounds.hypergraph.HyperNode;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.edgeweights.EdgeWeight;
+
+/**
+ * A DirectedHyperEdge is an edge of a {@link DirectedHyperGraph}.
+ *
+ * @author Stephan Gocht <stephan@gobro.de>
+ *
+ * @param <T>
+ *            Type used in HyperNodes (HyperNode<T>)
+ */
+public class DirectedHyperEdge<T> {
+	/** Contains all destinations of this HyperEdge */
+	private final Set<HyperNode<T>> tail;
+	/** Contains multiple sources of this HyperEdge */
+	private final Set<HyperNode<T>> head;
+	private EdgeWeight weight;
+
+	public DirectedHyperEdge() {
+		this.tail = new HashSet<HyperNode<T>>();
+		this.head = new HashSet<HyperNode<T>>();
+	}
+
+	public Set<HyperNode<T>> getDestination() {
+		return this.head;
+	}
+
+	public Set<HyperNode<T>> getSource() {
+		return this.tail;
+	}
+
+	public EdgeWeight getWeight() {
+		return this.weight;
+	}
+
+	public void setWeight(EdgeWeight weight) {
+		this.weight = weight;
+	}
+
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/hypergraph/DirectedHyperGraph.java

@@ -0,0 +1,80 @@
+package com.ibm.wala.analysis.arraybounds.hypergraph;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+
+import com.ibm.wala.analysis.arraybounds.hypergraph.DirectedHyperEdge;
+import com.ibm.wala.analysis.arraybounds.hypergraph.HyperNode;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight;
+
+/**
+ * Implementation of a directed hyper graph. In a hyper graph an edge can have
+ * more than one head and more than one tail.
+ *
+ * @author Stephan Gocht <stephan@gobro.de>
+ *
+ * @param <T>
+ */
+public class DirectedHyperGraph<T> {
+	private final Map<T, HyperNode<T>> nodes;
+	private final Set<DirectedHyperEdge<T>> edges;
+
+	public DirectedHyperGraph() {
+		this.nodes = new HashMap<>();
+		this.edges = new HashSet<>();
+	}
+
+	public Set<DirectedHyperEdge<T>> getEdges() {
+		return this.edges;
+	}
+
+	public Map<T, HyperNode<T>> getNodes() {
+		return this.nodes;
+	}
+
+	/**
+	 * Resets the weight of all nodes.
+	 */
+	public void reset() {
+		for (final HyperNode<T> node : this.getNodes().values()) {
+			node.setWeight(Weight.NOT_SET);
+			node.setNewWeight(Weight.NOT_SET);
+		}
+	}
+
+	@Override
+	public String toString() {
+		final StringBuffer buffer = new StringBuffer();
+		for (final DirectedHyperEdge<T> edge : this.getEdges()) {
+			buffer.append(edge.getSource());
+			buffer.append(" -- ");
+			buffer.append(edge.getWeight());
+			buffer.append(" --> ");
+			buffer.append(edge.getDestination());
+			buffer.append("\n");
+		}
+		return buffer.toString();
+	}
+
+	/**
+	 * The outdEdges of a node may not have been set on construction. Use this
+	 * method to set them based on the edges of this HyperGraph.
+	 */
+	public void updateNodeEdges() {
+		for (final HyperNode<T> node : this.getNodes().values()) {
+			node.setOutEdges(new HashSet<DirectedHyperEdge<T>>());
+			node.setInEdges(new HashSet<DirectedHyperEdge<T>>());
+		}
+
+		for (final DirectedHyperEdge<T> edge : this.edges) {
+			for (final HyperNode<T> node : edge.getSource()) {
+				node.getOutEdges().add(edge);
+			}
+			for (final HyperNode<T> node : edge.getDestination()) {
+				node.getInEdges().add(edge);
+			}
+		}
+	}
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/hypergraph/HyperNode.java

@@ -0,0 +1,89 @@
+package com.ibm.wala.analysis.arraybounds.hypergraph;
+
+import java.util.HashSet;
+import java.util.Set;
+
+import com.ibm.wala.analysis.arraybounds.hypergraph.DirectedHyperEdge;
+import com.ibm.wala.analysis.arraybounds.hypergraph.DirectedHyperGraph;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight;
+
+/**
+ * A HyperNode is a node of a {@link DirectedHyperGraph}.
+ * 
+ * @author Stephan Gocht <stephan@gobro.de>
+ *
+ * @param <T>
+ */
+public class HyperNode<T> {
+	private Weight weight;
+	private Weight newWeight;
+
+	/**
+	 * Set of edges, which have this node as source, can be set automatically
+	 * with {@link DirectedHyperGraph#updateNodeEdges()}
+	 */
+	private Set<DirectedHyperEdge<T>> outEdges;
+	/**
+	 * Set of edges, which have this node as source, can be set automatically
+	 * with {@link DirectedHyperGraph#updateNodeEdges()}
+	 */
+	private Set<DirectedHyperEdge<T>> inEdges;
+
+	private T value;
+
+	public HyperNode(T value) {
+		this.value = value;
+		this.outEdges = new HashSet<DirectedHyperEdge<T>>();
+		this.weight = Weight.NOT_SET;
+		this.newWeight = Weight.NOT_SET;
+	}
+
+	public Set<DirectedHyperEdge<T>> getInEdges() {
+		return this.inEdges;
+	}
+
+	public Weight getNewWeight() {
+		return this.newWeight;
+	}
+
+	public Set<DirectedHyperEdge<T>> getOutEdges() {
+		return this.outEdges;
+	}
+
+	public T getValue() {
+		return this.value;
+	}
+
+	public Weight getWeight() {
+		return this.weight;
+	}
+
+	public void setInEdges(Set<DirectedHyperEdge<T>> inEdges) {
+		this.inEdges = inEdges;
+	}
+
+	public void setNewWeight(Weight newWeight) {
+		this.newWeight = newWeight;
+	}
+
+	public void setOutEdges(Set<DirectedHyperEdge<T>> outEdges) {
+		this.outEdges = outEdges;
+	}
+
+	public void setValue(T value) {
+		this.value = value;
+	}
+
+	public void setWeight(Weight weight) {
+		this.weight = weight;
+	}
+
+	@Override
+	public String toString() {
+		if (this.weight == Weight.NOT_SET) {
+			return this.value.toString();
+		} else {
+			return this.value.toString() + ": " + this.weight;
+		}
+	}
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/hypergraph/algorithms/ShortestPath.java

@@ -0,0 +1,229 @@
+package com.ibm.wala.analysis.arraybounds.hypergraph.algorithms;
+
+import java.util.Comparator;
+import java.util.HashSet;
+import java.util.Set;
+
+import com.ibm.wala.analysis.arraybounds.hypergraph.DirectedHyperEdge;
+import com.ibm.wala.analysis.arraybounds.hypergraph.DirectedHyperGraph;
+import com.ibm.wala.analysis.arraybounds.hypergraph.HyperNode;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight.Type;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.edgeweights.EdgeWeight;
+
+/**
+ *
+ * @author Stephan Gocht <stephan@gobro.de>
+ *
+ * @param <T>
+ *            NodeValueType
+ * @see ShortestPath#compute(DirectedHyperGraph, HyperNode, Comparator)
+ */
+public class ShortestPath<T> {
+	/**
+	 * Computes all shortest paths from source. The result is stored in
+	 * {@link HyperNode#getWeight()}.
+	 *
+	 * This is using a variation of Bellman-Ford for hyper graphs.
+	 *
+	 * @param graph
+	 * @param source
+	 * @param comparator
+	 *            defines order on weights.
+	 */
+	public static <NodeValueType> void compute(
+			DirectedHyperGraph<NodeValueType> graph,
+			HyperNode<NodeValueType> source, Comparator<Weight> comparator) {
+		graph.reset();
+		source.setWeight(Weight.ZERO);
+		new ShortestPath<>(graph, comparator);
+	}
+
+	private Set<DirectedHyperEdge<T>> updatedEdges;
+	private final Comparator<Weight> comparator;
+	private final DirectedHyperGraph<T> graph;
+	private boolean setUnlimitedOnChange = false;
+
+	private boolean hasNegativeCycle = false;
+
+	/**
+	 * @param graph
+	 *            Source nodes for shortest path computation should be set to 0,
+	 *            other nodes should be set to {@link Weight#NOT_SET}.
+	 * @param comparator
+	 *            defines order on weights.
+	 */
+	private ShortestPath(DirectedHyperGraph<T> graph,
+			Comparator<Weight> comparator) {
+		this.comparator = comparator;
+		this.graph = graph;
+
+		this.computeShortestPaths();
+		this.hasNegativeCycle = (this.updatedEdges.size() > 0);
+		if (this.hasNegativeCycle) {
+			// trigger, that changing values are set to infty in writeChanges:
+			this.setUnlimitedOnChange = true;
+
+			// we need to propagate negative cycle to all connected nodes
+			this.computeShortestPaths();
+		}
+	}
+
+	private void computeShortestPaths() {
+		this.updatedEdges = this.graph.getEdges();
+		final int nodeCount = this.graph.getNodes().size();
+		for (int i = 0; i < nodeCount - 1; i++) {
+			this.updateAllEdges();
+			if (this.updatedEdges.size() == 0) {
+				break;
+			}
+		}
+	}
+
+	/**
+	 * @param weight
+	 * @param otherWeight
+	 * @return weight > otherWeight
+	 */
+	private boolean greaterThen(Weight weight, Weight otherWeight) {
+		return otherWeight.getType() == Type.NOT_SET
+				|| this.comparator.compare(weight, otherWeight) > 0;
+	}
+
+	/**
+	 * @param weight
+	 * @param otherWeight
+	 * @return weight < otherWeight
+	 */
+	private boolean lessThen(Weight weight, Weight otherWeight) {
+		return otherWeight.getType() == Type.NOT_SET
+				|| this.comparator.compare(weight, otherWeight) < 0;
+	}
+
+	/**
+	 * Maximum of source weights, modified by the value of the edge. Note that
+	 * every weight is larger than {@link Weight#NOT_SET} for max computation.
+	 * This allows distances to propagate, even if not all nodes are connected
+	 * to the source of the shortest path computation. Otherwise (source,
+	 * other)->(sink) would not have a path from source to sink.
+	 *
+	 * @param edge
+	 * @return max{edgeValue.newValue(sourceWeight) | sourceWeight \in
+	 *         edge.getSources()}
+	 */
+	private Weight maxOfSources(final DirectedHyperEdge<T> edge) {
+		final EdgeWeight edgeValue = edge.getWeight();
+		Weight newWeight = Weight.NOT_SET;
+		for (final HyperNode<T> node : edge.getSource()) {
+
+			final Weight nodeWeight = node.getWeight();
+			if (nodeWeight.getType() != Type.NOT_SET) {
+
+				final Weight temp = edgeValue.newValue(nodeWeight);
+				if (this.greaterThen(temp, newWeight)) {
+					newWeight = temp;
+				}
+			}
+		}
+		return newWeight;
+	}
+
+	/**
+	 * We do not need to iterate all edges, but edges of which the source weight
+	 * was changed, other edges will not lead to a change of the destination
+	 * weight. For correct updating of the destination weight, we need to
+	 * consider all incoming edges. (The minimum of in edges is computed per
+	 * round, not global - see
+	 * {@link ShortestPath#updateDestinationsWithMin(HashSet, DirectedHyperEdge, Weight)}
+	 * )
+	 *
+	 * @return A set of edges, that may lead to changes of weights.
+	 */
+	private HashSet<DirectedHyperEdge<T>> selectEdgesToIterate() {
+		final HashSet<DirectedHyperEdge<T>> edgesToIterate = new HashSet<>();
+		for (final DirectedHyperEdge<T> edge : this.updatedEdges) {
+			for (final HyperNode<T> node : edge.getDestination()) {
+				edgesToIterate.addAll(node.getInEdges());
+			}
+		}
+		return edgesToIterate;
+	}
+
+	private void updateAllEdges() {
+
+		for (final DirectedHyperEdge<T> edge : this.selectEdgesToIterate()) {
+			final Weight maxOfSources = this.maxOfSources(edge);
+
+			if (maxOfSources.getType() != Type.NOT_SET) {
+				this.updateDestinationsWithMin(edge, maxOfSources);
+			}
+		}
+
+		this.writeChanges();
+	}
+
+	/**
+	 * Updates Nodes with the minimum of all incoming edges. The minimum is
+	 * computed over the minimum of all edges that were processed in this round
+	 * ({@link ShortestPath#selectEdgesToIterate()}).
+	 *
+	 * This is necessary for the feature described in
+	 * {@link ShortestPath#maxOfSources(DirectedHyperEdge)} to work properly:
+	 * The result of different rounds is not always monotonous, p.a.:
+	 *
+	 * <pre>
+	 * (n1, n2)->(n3)
+	 * Round 1: n1 = unset, n2 = -3 -> n3 = max(unset,-3) = -3
+	 * Round 2: n1 = 1, n2 = -3 -> n3 = max(1,-3) = 1
+	 * </pre>
+	 *
+	 * Would we compute the minimum of n3 over all rounds, it would be -3, but 1
+	 * is correct.
+	 *
+	 * Note: that every weight is smaller than {@link Weight#NOT_SET} for min
+	 * computation. This allows distances to propagate, even if not all nodes
+	 * are connected to the source of the shortest path computation. Otherwise
+	 * (source)->(sink), (other)->(sink), would not have a path from source to
+	 * sink.
+	 *
+	 * @param edge
+	 * @param newWeight
+	 */
+	private void updateDestinationsWithMin(final DirectedHyperEdge<T> edge,
+			Weight newWeight) {
+		for (final HyperNode<T> node : edge.getDestination()) {
+			if (this.lessThen(newWeight, node.getNewWeight())) {
+				node.setNewWeight(newWeight);
+			}
+		}
+	}
+
+	/**
+	 * This method is necessary, as the min is updated per round. (See
+	 * {@link ShortestPath#updateDestinationsWithMin(DirectedHyperEdge, Weight)}
+	 * )
+	 */
+	private void writeChanges() {
+		final HashSet<DirectedHyperEdge<T>> newUpdatedEdges = new HashSet<>();
+
+		for (final HyperNode<T> node : this.graph.getNodes().values()) {
+			final Weight oldWeight = node.getWeight();
+			final Weight newWeight = node.getNewWeight();
+			if (!newWeight.equals(Weight.NOT_SET)
+					&& !oldWeight.equals(newWeight)) {
+				// node weight has changed, so out edges have to be updated next
+				// round:
+				newUpdatedEdges.addAll(node.getOutEdges());
+
+				if (this.setUnlimitedOnChange) {
+					node.setWeight(Weight.UNLIMITED);
+				} else {
+					node.setWeight(node.getNewWeight());
+				}
+			}
+			node.setNewWeight(Weight.NOT_SET);
+		}
+
+		this.updatedEdges = newUpdatedEdges;
+	}
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/hypergraph/package-info.java

@@ -0,0 +1,6 @@
+package com.ibm.wala.analysis.arraybounds.hypergraph;
+
+/**
+ * This package contains a generic implementation of directed hypergraphs.
+ * The implementation is optimized for shortest path search, with {@link de.gobro.wala.test.analyse.hypergraph.algorithms.ShortestPath#compute() ShortestPath}
+ */

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/hypergraph/weight/NormalOrder.java

@@ -0,0 +1,46 @@
+package com.ibm.wala.analysis.arraybounds.hypergraph.weight;
+
+import java.util.Comparator;
+
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight.Type;
+
+/**
+ * Defines a normal Order on Weight: unlimited < ... < -1 < 0 < 1 < ... not_set
+ * is not comparable
+ *
+ * @author Stephan Gocht <stephan@gobro.de>
+ *
+ */
+public class NormalOrder implements Comparator<Weight> {
+
+	@Override
+	public int compare(Weight o1, Weight o2) {
+		int result = 0;
+
+		if (o1.getType() == Type.NOT_SET || o2.getType() == Type.NOT_SET) {
+			throw new IllegalArgumentException(
+					"Tried to compare weights, which are not set yet.");
+		}
+
+		if (o1.getType() == o2.getType()) {
+			if (o1.getType() == Type.NUMBER) {
+				result = o1.getNumber() - o2.getNumber();
+			} else {
+				result = 0;
+			}
+		} else {
+			if (o1.getType() == Type.UNLIMITED) {
+				result = -1;
+			} else if (o2.getType() == Type.UNLIMITED) {
+				result = 1;
+			} else {
+				throw new IllegalArgumentException(
+						"Programming error, expected no cases to be left.");
+			}
+		}
+
+		return result;
+	}
+
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/hypergraph/weight/ReverseOrder.java

@@ -0,0 +1,38 @@
+package com.ibm.wala.analysis.arraybounds.hypergraph.weight;
+
+import java.util.Comparator;
+
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.NormalOrder;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight.Type;
+
+/**
+ * Defines a reverse Order on Weight: ... > 1 > 0 > -1 > ... > unlimited not_set
+ * is not comparable
+ *
+ * @author Stephan Gocht <stephan@gobro.de>
+ *
+ */
+public class ReverseOrder implements Comparator<Weight> {
+
+	private final NormalOrder normalOrder;
+
+	public ReverseOrder() {
+		this.normalOrder = new NormalOrder();
+	}
+
+	@Override
+	public int compare(Weight o1, Weight o2) {
+		int result;
+		if (o1.getType() == Type.UNLIMITED) {
+			result = -1;
+		} else if (o2.getType() == Type.UNLIMITED) {
+			result = 1;
+		} else {
+			result = -this.normalOrder.compare(o1, o2);
+		}
+
+		return result;
+	}
+
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/hypergraph/weight/Weight.java

@@ -0,0 +1,114 @@
+package com.ibm.wala.analysis.arraybounds.hypergraph.weight;
+
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.NormalOrder;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.ReverseOrder;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight;
+
+/**
+ * A weight may be not set, a number or unlimited, note that the meaning of
+ * unlimited is given by the chosen order (see {@link NormalOrder} and
+ * {@link ReverseOrder}).
+ *
+ * @author Stephan Gocht <stephan@gobro.de>
+ */
+public class Weight {
+	public enum Type {
+		NUMBER, NOT_SET, UNLIMITED
+	}
+
+	public static final Weight UNLIMITED = new Weight(Type.UNLIMITED, 0);
+	public static final Weight NOT_SET = new Weight(Type.NOT_SET, 0);
+
+	public static final Weight ZERO = new Weight(Type.NUMBER, 0);
+
+	private final Type type;
+	private final int number;
+
+	public Weight(int number) {
+		this.type = Type.NUMBER;
+		this.number = number;
+	}
+
+	public Weight(Type type, int number) {
+		super();
+		this.type = type;
+		this.number = number;
+	}
+
+	/**
+	 * Returns this + other. If this is not Number this will be returned, if
+	 * other is not number other will be returned
+	 *
+	 * @param other
+	 * @return this + other
+	 */
+	public Weight add(Weight other) {
+		Weight result = null;
+		if (this.getType() == Type.NUMBER) {
+			if (other.getType() == Type.NUMBER) {
+				result = new Weight(Type.NUMBER, this.getNumber()
+						+ other.getNumber());
+			} else {
+				result = other;
+			}
+		} else {
+			result = this;
+		}
+
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (this.getClass() != obj.getClass()) {
+			return false;
+		}
+		final Weight other = (Weight) obj;
+		if (this.number != other.number) {
+			return false;
+		}
+		if (this.type != other.type) {
+			return false;
+		}
+		return true;
+	}
+
+	public int getNumber() {
+		return this.number;
+	}
+
+	public Type getType() {
+		return this.type;
+	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + this.number;
+		result = prime * result
+				+ ((this.type == null) ? 0 : this.type.hashCode());
+		return result;
+	}
+
+	@Override
+	public String toString() {
+		if (this.type == Type.NUMBER) {
+			return Integer.toString(this.number);
+		} else {
+			if (this.type == Type.NOT_SET) {
+				return "NOT_SET";
+			} else if (this.type == Type.UNLIMITED) {
+				return "UNLIMITED";
+			} else {
+				return "Type: " + this.type;
+			}
+		}
+	}
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/hypergraph/weight/edgeweights/AdditiveEdgeWeight.java

@@ -0,0 +1,60 @@
+package com.ibm.wala.analysis.arraybounds.hypergraph.weight.edgeweights;
+
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.edgeweights.AdditiveEdgeWeight;
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.edgeweights.EdgeWeight;
+
+/**
+ * EdgeWeight that adds a specific value.
+ *
+ * @author Stephan Gocht <stephan@gobro.de>
+ *
+ */
+public class AdditiveEdgeWeight implements EdgeWeight {
+	private final Weight value;
+
+	public AdditiveEdgeWeight(Weight value) {
+		this.value = value;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (this.getClass() != obj.getClass()) {
+			return false;
+		}
+		final AdditiveEdgeWeight other = (AdditiveEdgeWeight) obj;
+		if (this.value == null) {
+			if (other.value != null) {
+				return false;
+			}
+		} else if (!this.value.equals(other.value)) {
+			return false;
+		}
+		return true;
+	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result
+				+ ((this.value == null) ? 0 : this.value.hashCode());
+		return result;
+	}
+
+	@Override
+	public Weight newValue(Weight weight) {
+		return weight.add(this.value);
+	}
+
+	@Override
+	public String toString() {
+		return this.value.toString();
+	}
+}

com.ibm.wala.core/src/com/ibm/wala/analysis/arraybounds/hypergraph/weight/edgeweights/EdgeWeight.java

@@ -0,0 +1,13 @@
+package com.ibm.wala.analysis.arraybounds.hypergraph.weight.edgeweights;
+
+import com.ibm.wala.analysis.arraybounds.hypergraph.weight.Weight;
+
+/**
+ * The weight of an edge can produce a new value for the tail nodes given the
+ * head nodes.
+ *
+ * @author Stephan Gocht <stephan@gobro.de>
+ */
+public interface EdgeWeight {
+	public Weight newValue(Weight weight);
+}