Moved property simulation code to PropertySimulator class. Improved resolving errors to IASTNodes that caused them.

* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java: Added getImplications(ExecutionState), join truth assignments.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java: Added getExecutionState for a Minterm.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java: Moved join into PropertSimulator.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/IPropertyFSM.java: Interface to formalize definition for FSM of property states.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java: New file; extracted all common propsim functionality.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java: Added getImplications(Minterm<E>).
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java: Maintain set of IASTNodes that led to error transition.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java: Moved most code to PropertySimulator.

8 files changed, 477 insertions, 324 deletions

diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java
index 3b62b87..9e3ed5f 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java
@@ -10,17 +10,21 @@
  *******************************************************************************/
 package org.eclipse.cdt.codan.extension;
 
+import java.util.HashMap;
 import java.util.HashSet;
 import java.util.List;
+import java.util.Map;
 import java.util.Set;
 
 import org.eclipse.cdt.codan.extension.Minterm.Value;
 import org.eclipse.cdt.core.dom.ast.IVariable;
 
 public class ESSimplifier extends QuineMcCluskeySimplifier<IVariable> {
+	private Map<ExecutionState, Minterm<IVariable>> esMapping;
 
-	public ESSimplifier(ITruthTable<IVariable> tt) {
+	public ESSimplifier(ESTruthTable tt) {
 		super(tt);
+		esMapping = new HashMap<ExecutionState, Minterm<IVariable>>();
 	}
 
 	public Set<ExecutionState> getExecutionStateCover() {
@@ -28,7 +32,7 @@ public class ESSimplifier extends QuineMcCluskeySimplifier<IVariable> {
 		List<Minterm<IVariable>> implicantCover = getImplicantCover();
 		for (Minterm<IVariable> term : implicantCover) {
 			ExecutionState es = new ExecutionState();
-			for (IVariable var : variables) {
+			for (IVariable var : truthTable.getVariables()) {
 				Value val = term.getValue(var);
 				if (val == Value.TRUE) {
 					es.addClause(new ExecutionStateClause(var, true));
@@ -38,6 +42,24 @@ public class ESSimplifier extends QuineMcCluskeySimplifier<IVariable> {
 				}
 				// Don't care about Don't cares
 			}
+			// Add truth assignments from implied minterms
+			List<Minterm<IVariable>> implied = getImplications(term);
+			for (Minterm<IVariable> minterm : implied) {
+				ExecutionState e = ((ESTruthTable) truthTable).getExecutionState(minterm);
+				es.getTruthAssignments().putAll(e.getTruthAssignments());
+			}
+			ret.add(es);
+			esMapping.put(es, term);
+		}
+		return ret;
+	}
+	
+	public Set<ExecutionState> getImplications(ExecutionState primeImplicant) {
+		Set<ExecutionState> ret = new HashSet<ExecutionState>();
+		Minterm<IVariable> piTerm = esMapping.get(primeImplicant);
+		List<Minterm<IVariable>> impls = getImplications(piTerm);
+		for (Minterm<IVariable> term : impls) {
+			ExecutionState es = ((ESTruthTable) truthTable).getExecutionState(term);
 			ret.add(es);
 		}
 		return ret;
@@ -46,13 +68,13 @@ public class ESSimplifier extends QuineMcCluskeySimplifier<IVariable> {
 	@Override
 	public String toString() {
 		StringBuffer buf = new StringBuffer();
-		for (IVariable var : variables) {
+		for (IVariable var : truthTable.getVariables()) {
 			buf.append(var.getName());
 			buf.append(" ");
 		}
 		buf.append("\n");
-		for (Minterm<IVariable> term : minterms) {
-			for (IVariable var : variables) {
+		for (Minterm<IVariable> term : truthTable.getMinterms()) {
+			for (IVariable var : truthTable.getVariables()) {
 				switch (term.getValue(var)) {
 				case TRUE:
 					buf.append("1");
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java
index 94e7574..1835015 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java
@@ -22,11 +22,13 @@ import org.eclipse.cdt.core.dom.ast.IVariable;
 
 public class ESTruthTable implements ITruthTable<IVariable> {
 	private List<Minterm<IVariable>> minterms;
+	private Map<Minterm<IVariable>, ExecutionState> esMapping;
 	private List<IVariable> variables;
 	
 	public ESTruthTable(Set<ExecutionState> es) {
 		minterms = new ArrayList<Minterm<IVariable>>();
 		variables = new ArrayList<IVariable>();
+		esMapping = new HashMap<Minterm<IVariable>, ExecutionState>();
 		
 		for (ExecutionState e : es) {
 			for (ExecutionStateClause c : e.getClauses()) {
@@ -54,6 +56,7 @@ public class ESTruthTable implements ITruthTable<IVariable> {
 			for (ExecutionStateClause c : e.getClauses()) {
 				term.setValue(c.getVariable(), c.isTrue() ? Value.TRUE : Value.FALSE);
 			}
+			esMapping.put(term, e);
 		}		
 	}
 	
@@ -65,6 +68,10 @@ public class ESTruthTable implements ITruthTable<IVariable> {
 		return variables;
 	}
 	
+	public ExecutionState getExecutionState(Minterm<IVariable> minterm) {
+		return esMapping.get(minterm);
+	}
+	
 	@Override
 	public String toString() {
 		StringBuffer buf = new StringBuffer();
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java
index c19970e..fd8032a 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java
@@ -19,7 +19,7 @@ import org.eclipse.cdt.core.dom.ast.IVariable;
 
 public class ExecutionState {
 	private Set<ExecutionStateClause> clauses;
-	private Map<IVariable, Boolean> truthAssignments;
+	private Map<IVariable, Boolean> truthAssignments; // FIXME this should be more robust, use SSA
 	private boolean top;
 	private boolean bottom;
 
@@ -83,12 +83,6 @@ public class ExecutionState {
 		}
 	}
 
-	public static Set<ExecutionState> join(Set<ExecutionState> es) {
-		ESTruthTable tt = new ESTruthTable(es);
-		ESSimplifier simp = new ESSimplifier(tt);
-		return simp.getExecutionStateCover();
-	}
-
 	public Set<ExecutionStateClause> getClauses() {
 		return clauses;
 	}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/IPropertyFSM.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/IPropertyFSM.java
new file mode 100644
index 0000000..a8ace1e
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/IPropertyFSM.java
@@ -0,0 +1,23 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.cdt.codan.extension;
+
+import java.util.Set;
+
+public interface IPropertyFSM {
+	
+	public Set<PropertyState> getPropertyStates();
+	
+	public PropertyState getUninitState();
+	
+	public PropertyState getErrorState();
+
+}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java
new file mode 100644
index 0000000..ffd3ada
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java
@@ -0,0 +1,361 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.cdt.codan.extension;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.LinkedList;
+import java.util.Map;
+import java.util.Queue;
+import java.util.Set;
+
+import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression;
+import org.eclipse.cdt.core.dom.ast.IASTExpression;
+import org.eclipse.cdt.core.dom.ast.IASTIdExpression;
+import org.eclipse.cdt.core.dom.ast.IASTLiteralExpression;
+import org.eclipse.cdt.core.dom.ast.IASTName;
+import org.eclipse.cdt.core.dom.ast.IASTNode;
+import org.eclipse.cdt.core.dom.ast.IASTUnaryExpression;
+import org.eclipse.cdt.core.dom.ast.IBinding;
+import org.eclipse.cdt.core.dom.ast.IVariable;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IBlock;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowEdge;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowGraph;
+
+public class PropertySimulator {
+	// Property simulation state info for CFG's edges
+	private Map<IControlFlowEdge, Set<SymbolicState>> edgeInfo;
+	private Queue<IBlock> worklist;
+	private IControlFlowGraph cfg;
+	private IPropertyFSM fsm;
+	
+	public PropertySimulator(IControlFlowGraph cfg, IPropertyFSM fsm) {
+		this.cfg = cfg;
+		this.fsm = fsm;
+		worklist = new LinkedList<IBlock>();
+		edgeInfo = new HashMap<IControlFlowEdge, Set<SymbolicState>>();
+		solve();
+	}
+
+	private void solve() {
+		for (IControlFlowEdge edge : cfg.getEdges()) {
+			// Initialize edgeInfo for each edge
+			Set<SymbolicState> set = new HashSet<SymbolicState>();
+			edgeInfo.put(edge, set);
+		}
+
+		// Create edgeInfo for entry edge
+		IControlFlowEdge entryEdge = cfg.getEntry().getOutEdges()[0];
+		Set<SymbolicState> symStates = edgeInfo.get(entryEdge);
+		Set<PropertyState> propStates = new HashSet<PropertyState>();
+		propStates.add(fsm.getUninitState());
+		symStates.add(new SymbolicState(propStates, new ExecutionState()));
+
+		worklist.add(entryEdge.getTo());
+		// XXX Debug
+		printStates(entryEdge, symStates);
+
+		while (!worklist.isEmpty()) {
+			IBlock blk = worklist.remove();
+			if (isMerge(blk)) {
+				// Apply flow function for a merge block
+				Set<SymbolicState> newStates = flowMerge(blk, edgeInfo.get(blk.getInEdges()[0]), edgeInfo.get(blk.getInEdges()[1]));
+				add(blk.getOutEdges()[0], newStates);
+				
+				// XXX Debug
+				System.out.println("MRG: " + printStates(blk.getOutEdges()[0], newStates));
+			}
+			else if (isBranch(blk)) {
+				// Apply flow function for a branch block
+				Set<SymbolicState> oldStates = edgeInfo.get(blk.getInEdges()[0]);
+				Set<SymbolicState> newStatesTrue = flowBranch(blk, oldStates, true);
+				Set<SymbolicState> newStatesFalse = flowBranch(blk, oldStates, false);
+
+				// Assumes 0th out-edge is true branch, 1st out-edge is false branch 
+				add(blk.getOutEdges()[0], newStatesTrue);
+				add(blk.getOutEdges()[1], newStatesFalse);
+				
+				// XXX Debug
+				System.out.println("BR (T): " + printStates(blk.getOutEdges()[0], newStatesTrue));
+				System.out.println("BR (F): " + printStates(blk.getOutEdges()[1], newStatesFalse));
+			}
+			else {
+				// Apply flow function for a normal block
+				Set<SymbolicState> newStates = flowOther(blk, edgeInfo.get(blk.getInEdges()[0]));
+				
+				// Don't process the null exit block
+				if (!blk.equals(cfg.getExit())) {
+					add(blk.getOutEdges()[0], newStates);
+					// XXX Debug
+					System.out.println("OTH: " + printStates(blk.getOutEdges()[0], newStates));
+				}
+			}
+		}
+	}
+	
+	public Set<SymbolicState> getEndStates() {
+		IControlFlowEdge exitEdge = cfg.getExit().getInEdges()[0];
+		return edgeInfo.get(exitEdge);
+	}
+	
+	private String printStates(IControlFlowEdge edge, Set<SymbolicState> states) {
+		StringBuffer buf = new StringBuffer();
+		IASTNode from = edge.getFrom().getContent();
+		IASTNode to = edge.getTo().getContent();
+		buf.append("{");
+		buf.append(from == null ? from : from.getRawSignature());
+		buf.append(" -> ");
+		buf.append(to == null ? to : to.getRawSignature());
+		buf.append("} = ");
+		buf.append(states);
+		return buf.toString();		
+	}
+
+	private Set<SymbolicState> flowMerge(IBlock blk, Set<SymbolicState> ss1,
+			Set<SymbolicState> ss2) {
+		Set<SymbolicState> ret = new HashSet<SymbolicState>();
+		ret.addAll(ss1);
+		ret.addAll(ss2);
+		return group(ret);
+	}
+
+	private Set<SymbolicState> flowBranch(IBlock blk, Set<SymbolicState> ss, boolean value) {
+		Set<SymbolicState> ret = new HashSet<SymbolicState>();
+		for (SymbolicState s : ss) {
+			SymbolicState s0 = transferBranch(blk, s, value);
+			if (!s0.getExecutionState().isBottom()) {
+				ret.add(s0);
+			}
+		}
+		return group(ret);
+	}
+
+	private Set<SymbolicState> flowOther(IBlock blk, Set<SymbolicState> ss) {
+		Set<SymbolicState> ret = new HashSet<SymbolicState>();
+		for (SymbolicState s : ss) {
+			SymbolicState s0 = transferOther(blk, s);
+			ret.add(s0);
+		}
+		return group(ret);
+	}
+
+	private Set<SymbolicState> group(Set<SymbolicState> ss) {
+		return groupPropSim(ss);
+	}
+	
+	private Set<SymbolicState> groupPSA(Set<SymbolicState> ss) {
+		return ss;
+	}
+	
+	private Set<SymbolicState> groupPropSim(Set<SymbolicState> ss) {
+		Set<SymbolicState> ret = new HashSet<SymbolicState>();
+		
+		// Group SymbolicStates by PropertyState
+		Map<PropertyState, Set<SymbolicState>> statesPerProperty = new HashMap<PropertyState, Set<SymbolicState>>();
+		for (SymbolicState s : ss) {
+			for (PropertyState ps : s.getPropertyStates()) {
+				if (!statesPerProperty.containsKey(ps)) {
+					statesPerProperty.put(ps, new HashSet<SymbolicState>());
+				}
+				Set<SymbolicState> states = statesPerProperty.get(ps);
+				states.add(s);
+			}
+		}
+		
+		// Iterate through result and create SymbolicStates per PropertyState with ExecutionStates joined
+		for (PropertyState p : statesPerProperty.keySet()) {
+			Set<PropertyState> ps = new HashSet<PropertyState>();
+			ps.add(p);
+			Set<SymbolicState> ssForProperty = statesPerProperty.get(p);
+			Set<ExecutionState> esForProperty = new HashSet<ExecutionState>();
+			for (SymbolicState s : ssForProperty) {
+				esForProperty.add(s.getExecutionState());
+			}
+			if (ssForProperty.size() > 1) {
+				// Join execution states in this set
+				ESTruthTable tt = new ESTruthTable(esForProperty);
+				ESSimplifier simp = new ESSimplifier(tt);
+				esForProperty = simp.getExecutionStateCover();
+				
+				for (ExecutionState e : esForProperty) {
+					SymbolicState newState = new SymbolicState(ps, e);
+					// Join corresponding error conditions
+					if (p.equals(fsm.getErrorState())) {
+						// Get original ExecutionStates implied by this prime implicant
+						Set<ExecutionState> implied = simp.getImplications(e);
+						// Find the appropriate SymbolicState
+						for (ExecutionState orig : implied) {
+							SymbolicState s = findSymbolicState(ssForProperty, orig);
+							// Add its error cause to the joined state
+							newState.getErrorCauses().addAll(s.getErrorCauses());
+						}
+					}
+					ret.add(newState);
+				}
+			}
+			else {
+				// Nothing to do
+				SymbolicState s = ssForProperty.iterator().next();
+				ret.add(s);
+			}
+			
+		}		
+		
+		return ret;
+	}
+
+	private SymbolicState findSymbolicState(Set<SymbolicState> ss, ExecutionState es) {
+		for (SymbolicState s : ss) {
+			if (s.getExecutionState().equals(es)) {
+				return s;
+			}
+		}
+		return null;
+	}
+
+	private SymbolicState transferBranch(IBlock blk, SymbolicState s, boolean value) {
+		IASTNode node = blk.getContent();
+		
+		SymbolicState ret = s.copy();
+		if (node != null) {			
+			// Modify execution state according to branch condition
+			ExecutionStateClause clause = null;
+			// *N.B.* content for condition IBlock is condition expression itself
+			if (node instanceof IASTBinaryExpression) {
+				// FIXME compound conditionals
+				IASTBinaryExpression binExpr = (IASTBinaryExpression) node;
+				int op = binExpr.getOperator();
+
+				// FIXME other ops
+				// Check operator is an equality operator
+				if (op == IASTBinaryExpression.op_equals) { // if (x == 0)
+					IASTExpression o1 = binExpr.getOperand1();
+					if (o1 instanceof IASTIdExpression) {
+						IASTName name = ((IASTIdExpression) o1).getName();
+						clause = parseConditional(clause, name, binExpr.getOperand2(), value);
+					}
+				}
+				else if (op == IASTBinaryExpression.op_notequals) { // if (x != 0)
+					IASTExpression o1 = binExpr.getOperand1();
+					if (o1 instanceof IASTIdExpression) {
+						IASTName name = ((IASTIdExpression) o1).getName();
+						clause = parseConditional(clause, name, binExpr.getOperand2(), !value); // Negation
+					}
+				}
+			}
+			else if (node instanceof IASTUnaryExpression) { // if (!x)
+				IASTUnaryExpression uExpr = (IASTUnaryExpression) node;
+				int op = uExpr.getOperator();
+				
+				// Check operator is a negation operator
+				if (op == IASTUnaryExpression.op_not) {
+					IASTExpression operand = uExpr.getOperand();
+					if (operand instanceof IASTIdExpression) {
+						IASTName name = ((IASTIdExpression) operand).getName();
+						clause = parseConditional(clause, name, !value); // Negation
+					}
+				}
+			}
+			else if (node instanceof IASTIdExpression) { // if (x)
+				IASTName name = ((IASTIdExpression) node).getName();
+				clause = parseConditional(clause, name, value);
+			}
+			
+			if (clause != null) {
+				ret.getExecutionState().addClause(clause);
+				// TODO Theorem Prover goes here! / Determine if branch is feasible
+				ret.getExecutionState().bindTruthAssignments();
+			}
+			else {
+				// FIXME Handle unresolvable case
+			}
+		}
+		
+		return ret;
+	}
+
+	private SymbolicState transferOther(IBlock blk, SymbolicState s) {
+		IASTNode node = blk.getContent();		
+		
+		if (node != null) {
+			// Process property state transition
+			Set<PropertyState> oldStates = s.getPropertyStates();
+			Set<PropertyState> newStates = new HashSet<PropertyState>();
+			for (PropertyState state : oldStates) {
+				PropertyState dest = state.transition(node);
+				// If we transition to from non-error to error, store the node that caused it
+				if (!state.equals(fsm.getErrorState()) && dest.equals(fsm.getErrorState())) {
+					s.getErrorCauses().add(node);
+				}
+				newStates.add(dest);
+			}
+			s.setPropertyStates(newStates);
+			
+			// Modify execution state according to variable assignments
+			node.accept(new VariableAssignmentVisitor(s.getExecutionState()));
+		}
+		return s;
+	}
+
+	private void add(IControlFlowEdge edge,
+			Set<SymbolicState> ss) {
+		if (!edgeInfo.get(edge).equals(ss)) {
+			edgeInfo.put(edge, ss);
+			worklist.add(edge.getTo());
+		}
+	}
+	
+	private boolean isBranch(IBlock blk) {
+		return blk.getOutEdges().length > 1;
+	}
+
+	private boolean isMerge(IBlock blk) {
+		return blk.getInEdges().length > 1;
+	}
+	
+	// FIXME REFACTOR
+	private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, IASTExpression valueExpr, boolean branchTruth) {
+		IBinding binding = name.resolveBinding();
+		if (binding instanceof IVariable) {
+			IVariable var = (IVariable) binding;
+			Boolean truth = getTruthValue(valueExpr);
+			if (truth != null) {
+				clause = new ExecutionStateClause(var, truth == branchTruth);
+			}
+		}
+		return clause;
+	}
+	
+	private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, boolean branchTruth) {
+		IBinding binding = name.resolveBinding();
+		if (binding instanceof IVariable) {
+			IVariable var = (IVariable) binding;
+			clause = new ExecutionStateClause(var, branchTruth);
+		}
+		return clause;
+	}
+
+	private Boolean getTruthValue(IASTExpression valueExpr) {
+		Boolean result = null;
+		// Handle assignment from literals
+		if (valueExpr instanceof IASTLiteralExpression) {
+			int kind = ((IASTLiteralExpression) valueExpr).getKind();
+			String value = String.valueOf(((IASTLiteralExpression) valueExpr).getValue());
+			switch (kind) {
+			case IASTLiteralExpression.lk_integer_constant:
+				// 0 = False, > 0 = True
+				result = !value.equals("0");
+			}
+		}
+		// TODO other variable assignments
+		return result;
+	}
+}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java
index d363028..45c41ab 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java
@@ -18,13 +18,13 @@ import java.util.Map;
 import java.util.Queue;
 
 public class QuineMcCluskeySimplifier<E> {
-	protected List<Minterm<E>> minterms;
-	protected List<E> variables;
+	protected ITruthTable<E> truthTable;
 	protected List<Minterm<E>> implicantCover;
+	private Map<Minterm<E>, List<Minterm<E>>> implications;
 	
 	public QuineMcCluskeySimplifier(ITruthTable<E> tt) {
-		minterms = tt.getMinterms();
-		variables = tt.getVariables();
+		this.truthTable = tt;
+		List<Minterm<E>> minterms = tt.getMinterms();
 		List<Minterm<E>> inputMinterms = new ArrayList<Minterm<E>>(minterms);
 		List<Minterm<E>> primeImplicants = new ArrayList<Minterm<E>>(minterms);
 				
@@ -56,8 +56,7 @@ public class QuineMcCluskeySimplifier<E> {
 			}
 		}
 		
-		// Determine which prime implicants cover which original minterms
-		Map<Minterm<E>, List<Minterm<E>>> implications = new HashMap<Minterm<E>, List<Minterm<E>>>();
+		implications = new HashMap<Minterm<E>, List<Minterm<E>>>();
 		for (Minterm<E> implicant : primeImplicants) {
 			implications.put(implicant, new ArrayList<Minterm<E>>());
 			for (Minterm<E> minterm : inputMinterms) {
@@ -110,5 +109,9 @@ public class QuineMcCluskeySimplifier<E> {
 	public List<Minterm<E>> getImplicantCover() {
 		return implicantCover;
 	}
+	
+	public List<Minterm<E>> getImplications(Minterm<E> primeImplicant) {
+		return implications.get(primeImplicant);
+	}
 
 }
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java
index 19dd6b3..76db5ea 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java
@@ -16,15 +16,18 @@ import java.util.HashSet;
 import java.util.Map;
 import java.util.Set;
 
+import org.eclipse.cdt.core.dom.ast.IASTNode;
 import org.eclipse.cdt.core.dom.ast.IVariable;
 
 public class SymbolicState {
 	private Set<PropertyState> propertyStates;
 	private ExecutionState executionState;
+	private Set<IASTNode> errorCauses;
 	
 	public SymbolicState(Set<PropertyState> propertyStates, ExecutionState executionState) {
 		this.propertyStates = propertyStates;
 		this.executionState = executionState;
+		errorCauses = new HashSet<IASTNode>();
 	}
 
 	public ExecutionState getExecutionState() {
@@ -49,7 +52,13 @@ public class SymbolicState {
 		Map<IVariable, Boolean> truthAssignments = new HashMap<IVariable, Boolean>(executionState.getTruthAssignments());
 		es.setTruthAssignments(truthAssignments);
 		
-		return new SymbolicState(ps, es);
+		SymbolicState ret = new SymbolicState(ps, es);
+		ret.errorCauses = new HashSet<IASTNode>(errorCauses);
+		return ret;
+	}
+	
+	public Set<IASTNode> getErrorCauses() {
+		return errorCauses;
 	}
 	
 	@Override
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java
index 491a481..d60889a 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java
@@ -13,40 +13,26 @@ package org.eclipse.cdt.codan.extension.checkers;
 import java.io.File;
 import java.net.URI;
 import java.text.MessageFormat;
-import java.util.HashMap;
 import java.util.HashSet;
-import java.util.LinkedList;
-import java.util.Map;
-import java.util.Queue;
 import java.util.Set;
 
 import org.eclipse.cdt.codan.core.model.AbstractIndexAstChecker;
 import org.eclipse.cdt.codan.extension.Activator;
 import org.eclipse.cdt.codan.extension.ExecutionState;
-import org.eclipse.cdt.codan.extension.ExecutionStateClause;
+import org.eclipse.cdt.codan.extension.IPropertyFSM;
+import org.eclipse.cdt.codan.extension.PropertySimulator;
 import org.eclipse.cdt.codan.extension.PropertyState;
 import org.eclipse.cdt.codan.extension.SymbolicState;
-import org.eclipse.cdt.codan.extension.VariableAssignmentVisitor;
-import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression;
-import org.eclipse.cdt.core.dom.ast.IASTExpression;
-import org.eclipse.cdt.core.dom.ast.IASTIdExpression;
-import org.eclipse.cdt.core.dom.ast.IASTLiteralExpression;
-import org.eclipse.cdt.core.dom.ast.IASTName;
 import org.eclipse.cdt.core.dom.ast.IASTNode;
 import org.eclipse.cdt.core.dom.ast.IASTStatement;
 import org.eclipse.cdt.core.dom.ast.IASTTranslationUnit;
-import org.eclipse.cdt.core.dom.ast.IASTUnaryExpression;
-import org.eclipse.cdt.core.dom.ast.IBinding;
-import org.eclipse.cdt.core.dom.ast.IVariable;
 import org.eclipse.core.resources.IProject;
 import org.eclipse.core.resources.IResource;
 import org.eclipse.core.resources.IWorkspaceRoot;
 import org.eclipse.core.resources.ResourcesPlugin;
 import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.GraphCreator;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IBlock;
 import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.ICallGraph;
 import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.ICallGraphNode;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowEdge;
 import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowGraph;
 import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.impl.ControlFlowGraph;
 
@@ -55,23 +41,16 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
 	
 	private static final String OPEN = "open";
 	private static final String CLOSE = "close";
-	private Queue<IBlock> worklist;
 	
-	// Property simulation state info for CFG's edges
-	private Map<IControlFlowEdge, Set<SymbolicState>> edgeInfo;
+	private IPropertyFSM fsm;
 	
 	// Property FSM states
 	private PropertyState uninit;
 	private PropertyState error;
 	private PropertyState opened;
-	
-	// Most recent node to cause transition to error state
-	private IASTNode errorNode;
 
 	public CloseOpenedFilesChecker() {
-		worklist = new LinkedList<IBlock>();
-		edgeInfo = new HashMap<IControlFlowEdge, Set<SymbolicState>>();
-		initFSM();
+		fsm = initFSM();
 	}
 
 	public void processAst(IASTTranslationUnit ast) {
@@ -96,248 +75,22 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
 				cfg.buildCFG();
 
 				// Search for error states using property simulation algorithm
-				solve(cfg);
+				PropertySimulator sim = new PropertySimulator(cfg, fsm);
 
 				// Check if the exit edge of the CFG contains an error state
-				IControlFlowEdge exitEdge = cfg.getExit().getInEdges()[0];
-				for (SymbolicState s : edgeInfo.get(exitEdge)) {
+				for (SymbolicState s : sim.getEndStates()) {
 					if (s.getPropertyStates().contains(error)) {
-						// Report problem
-						reportProblem(errorNode, s.getExecutionState());
+						// Report problems
+						for (IASTNode errorNode : s.getErrorCauses()) {
+							reportProblem(errorNode, s.getExecutionState());
+						}
 					}
 				}
 			}
 		}		
 	}
-
-
-	private void solve(IControlFlowGraph cfg) {
-		for (IControlFlowEdge edge : cfg.getEdges()) {
-			// Initialize edgeInfo for each edge
-			Set<SymbolicState> set = new HashSet<SymbolicState>();
-			edgeInfo.put(edge, set);
-		}
-
-		// Create edgeInfo for entry edge
-		IControlFlowEdge entryEdge = cfg.getEntry().getOutEdges()[0];
-		Set<SymbolicState> symStates = edgeInfo.get(entryEdge);
-		Set<PropertyState> propStates = new HashSet<PropertyState>();
-		propStates.add(uninit);
-		symStates.add(new SymbolicState(propStates, new ExecutionState()));
-
-		worklist.add(entryEdge.getTo());
-		// XXX Debug
-		printStates(entryEdge, symStates);
-
-		while (!worklist.isEmpty()) {
-			IBlock blk = worklist.remove();
-			if (isMerge(blk)) {
-				// Apply flow function for a merge block
-				Set<SymbolicState> newStates = flowMerge(blk, edgeInfo.get(blk.getInEdges()[0]), edgeInfo.get(blk.getInEdges()[1]));
-				add(blk.getOutEdges()[0], newStates);
-				
-				// XXX Debug
-				System.out.println("MRG: " + printStates(blk.getOutEdges()[0], newStates));
-			}
-			else if (isBranch(blk)) {
-				// Apply flow function for a branch block
-				Set<SymbolicState> oldStates = edgeInfo.get(blk.getInEdges()[0]);
-				Set<SymbolicState> newStatesTrue = flowBranch(blk, oldStates, true);
-				Set<SymbolicState> newStatesFalse = flowBranch(blk, oldStates, false);
-
-				// Assumes 0th out-edge is true branch, 1st out-edge is false branch 
-				add(blk.getOutEdges()[0], newStatesTrue);
-				add(blk.getOutEdges()[1], newStatesFalse);
-				
-				// XXX Debug
-				System.out.println("BR (T): " + printStates(blk.getOutEdges()[0], newStatesTrue));
-				System.out.println("BR (F): " + printStates(blk.getOutEdges()[1], newStatesFalse));
-			}
-			else {
-				// Apply flow function for a normal block
-				Set<SymbolicState> newStates = flowOther(blk, edgeInfo.get(blk.getInEdges()[0]));
-				
-				// Don't process the null exit block
-				if (!blk.equals(cfg.getExit())) {
-					add(blk.getOutEdges()[0], newStates);
-					// XXX Debug
-					System.out.println("OTH: " + printStates(blk.getOutEdges()[0], newStates));
-				}
-			}
-		}
-	}
-
-
-	private String printStates(IControlFlowEdge edge, Set<SymbolicState> states) {
-		StringBuffer buf = new StringBuffer();
-		IASTNode from = edge.getFrom().getContent();
-		IASTNode to = edge.getTo().getContent();
-		buf.append("{");
-		buf.append(from == null ? from : from.getRawSignature());
-		buf.append(" -> ");
-		buf.append(to == null ? to : to.getRawSignature());
-		buf.append("} = ");
-		buf.append(states);
-		return buf.toString();		
-	}
-
-	private Set<SymbolicState> flowMerge(IBlock blk, Set<SymbolicState> ss1,
-			Set<SymbolicState> ss2) {
-		Set<SymbolicState> ret = new HashSet<SymbolicState>();
-		ret.addAll(ss1);
-		ret.addAll(ss2);
-		return group(ret);
-	}
-
-	private Set<SymbolicState> flowBranch(IBlock blk, Set<SymbolicState> ss, boolean value) {
-		Set<SymbolicState> ret = new HashSet<SymbolicState>();
-		for (SymbolicState s : ss) {
-			SymbolicState s0 = transferBranch(blk, s, value);
-			if (!s0.getExecutionState().isBottom()) {
-				ret.add(s0);
-			}
-		}
-		return group(ret);
-	}
-
-	private Set<SymbolicState> flowOther(IBlock blk, Set<SymbolicState> ss) {
-		Set<SymbolicState> ret = new HashSet<SymbolicState>();
-		for (SymbolicState s : ss) {
-			SymbolicState s0 = transferOther(blk, s);
-			ret.add(s0);
-		}
-		return group(ret);
-	}
-
-	private Set<SymbolicState> group(Set<SymbolicState> ss) {
-		return groupPropSim(ss);
-	}
-	
-	private Set<SymbolicState> groupPSA(Set<SymbolicState> ss) {
-		return ss;
-	}
-	
-	private Set<SymbolicState> groupPropSim(Set<SymbolicState> ss) {
-		Set<SymbolicState> ret = new HashSet<SymbolicState>();
-		
-		// Group SymbolicStates by PropertyState
-		Map<PropertyState, Set<ExecutionState>> statesPerProperty = new HashMap<PropertyState, Set<ExecutionState>>();
-		for (SymbolicState s : ss) {
-			for (PropertyState ps : s.getPropertyStates()) {
-				if (!statesPerProperty.containsKey(ps)) {
-					statesPerProperty.put(ps, new HashSet<ExecutionState>());
-				}
-				Set<ExecutionState> states = statesPerProperty.get(ps);
-				states.add(s.getExecutionState());
-			}
-		}
-		
-		// Iterate through result and create SymbolicStates per PropertyState with ExecutionStates joined
-		for (PropertyState p : statesPerProperty.keySet()) {
-			Set<PropertyState> ps = new HashSet<PropertyState>();
-			ps.add(p);
-			Set<ExecutionState> es = statesPerProperty.get(p);
-			if (es.size() > 1) {
-				// Join execution states in this set
-				es = ExecutionState.join(es);
-			}
-			for (ExecutionState e : es) {
-				SymbolicState s = new SymbolicState(ps, e);
-				ret.add(s);
-			}
-		}		
-		
-		return ret;
-	}
-
-	private SymbolicState transferBranch(IBlock blk, SymbolicState s, boolean value) {
-		IASTNode node = blk.getContent();
-		
-		SymbolicState ret = s.copy();
-		if (node != null) {			
-			// Modify execution state according to branch condition
-			ExecutionStateClause clause = null;
-			// *N.B.* content for condition IBlock is condition expression itself
-			if (node instanceof IASTBinaryExpression) {
-				// FIXME compound conditionals
-				IASTBinaryExpression binExpr = (IASTBinaryExpression) node;
-				int op = binExpr.getOperator();
-
-				// FIXME other ops
-				// Check operator is an equality operator
-				if (op == IASTBinaryExpression.op_equals) { // if (x == 0)
-					IASTExpression o1 = binExpr.getOperand1();
-					if (o1 instanceof IASTIdExpression) {
-						IASTName name = ((IASTIdExpression) o1).getName();
-						clause = parseConditional(clause, name, binExpr.getOperand2(), value);
-					}
-				}
-				else if (op == IASTBinaryExpression.op_notequals) { // if (x != 0)
-					IASTExpression o1 = binExpr.getOperand1();
-					if (o1 instanceof IASTIdExpression) {
-						IASTName name = ((IASTIdExpression) o1).getName();
-						clause = parseConditional(clause, name, binExpr.getOperand2(), !value); // Negation
-					}
-				}
-			}
-			else if (node instanceof IASTUnaryExpression) { // if (!x)
-				IASTUnaryExpression uExpr = (IASTUnaryExpression) node;
-				int op = uExpr.getOperator();
-				
-				// Check operator is a negation operator
-				if (op == IASTUnaryExpression.op_not) {
-					IASTExpression operand = uExpr.getOperand();
-					if (operand instanceof IASTIdExpression) {
-						IASTName name = ((IASTIdExpression) operand).getName();
-						clause = parseConditional(clause, name, !value); // Negation
-					}
-				}
-			}
-			else if (node instanceof IASTIdExpression) { // if (x)
-				IASTName name = ((IASTIdExpression) node).getName();
-				clause = parseConditional(clause, name, value);
-			}
-			
-			if (clause != null) {
-				ret.getExecutionState().addClause(clause);
-				// TODO Theorem Prover goes here! / Determine if branch is feasible
-				ret.getExecutionState().bindTruthAssignments();
-			}
-			else {
-				// FIXME Handle unresolvable case
-			}
-		}
-		
-		return ret;
-	}
-
-	private SymbolicState transferOther(IBlock blk, SymbolicState s) {
-		IASTNode node = blk.getContent();		
-		
-		if (node != null) {
-			// Process property state transition
-			Set<PropertyState> oldStates = s.getPropertyStates();
-			Set<PropertyState> newStates = new HashSet<PropertyState>();
-			for (PropertyState state : oldStates) {
-				newStates.add(state.transition(node));
-			}
-			s.setPropertyStates(newStates);
-			
-			// Modify execution state according to variable assignments
-			node.accept(new VariableAssignmentVisitor(s.getExecutionState()));
-		}
-		return s;
-	}
-
-	private void add(IControlFlowEdge edge,
-			Set<SymbolicState> ss) {
-		if (!edgeInfo.get(edge).equals(ss)) {
-			edgeInfo.put(edge, ss);
-			worklist.add(edge.getTo());
-		}
-	}
 	
-	private void initFSM() {
+	private IPropertyFSM initFSM() {
 		uninit = new PropertyState("$u") {			
 			@Override
 			public PropertyState transition(IASTNode node) {
@@ -347,7 +100,6 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
 				}
 				else if (containsClose(node)) {
 					dest = error;
-					errorNode = node;
 				}
 				return dest;
 			}
@@ -359,7 +111,6 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
 				PropertyState dest = opened;
 				if (containsOpen(node)) {
 					dest = error;
-					errorNode = node;
 				}
 				if (containsClose(node)) {
 					dest = uninit;
@@ -375,6 +126,28 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
 				return error;
 			}
 		};
+		
+		return new IPropertyFSM() {
+			
+			@Override
+			public PropertyState getUninitState() {
+				return uninit;
+			}
+			
+			@Override
+			public Set<PropertyState> getPropertyStates() {
+				Set<PropertyState> states = new HashSet<PropertyState>();
+				states.add(uninit);
+				states.add(opened);
+				states.add(error);
+				return states;
+			}
+			
+			@Override
+			public PropertyState getErrorState() {
+				return error;
+			}
+		};
 	}
 
 	protected boolean containsOpen(IASTNode node) {
@@ -387,54 +160,15 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
 		return parser.matches();
 	}
 
-	private boolean isBranch(IBlock blk) {
-		return blk.getOutEdges().length > 1;
-	}
-
-	private boolean isMerge(IBlock blk) {
-		return blk.getInEdges().length > 1;
-	}
-
 	private void reportProblem(IASTNode node, ExecutionState condition) {
-		String message = MessageFormat.format("Improper use of open/close given {0}.", condition);
-		reportProblem(ERR_ID, node, message);
-	}
-	
-	// FIXME REFACTOR
-	private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, IASTExpression valueExpr, boolean branchTruth) {
-		IBinding binding = name.resolveBinding();
-		if (binding instanceof IVariable) {
-			IVariable var = (IVariable) binding;
-			Boolean truth = getTruthValue(valueExpr);
-			if (truth != null) {
-				clause = new ExecutionStateClause(var, truth == branchTruth);
-			}
+		String message;
+		if (condition.isTop()) {
+			message = "Improper use of open/close.";	
 		}
-		return clause;
-	}
-	
-	private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, boolean branchTruth) {
-		IBinding binding = name.resolveBinding();
-		if (binding instanceof IVariable) {
-			IVariable var = (IVariable) binding;
-			clause = new ExecutionStateClause(var, branchTruth);
+		else {
+			message = MessageFormat.format("Improper use of open/close given {0}.", condition);			
 		}
-		return clause;
+		reportProblem(ERR_ID, node, message);
 	}
 
-	private Boolean getTruthValue(IASTExpression valueExpr) {
-		Boolean result = null;
-		// Handle assignment from literals
-		if (valueExpr instanceof IASTLiteralExpression) {
-			int kind = ((IASTLiteralExpression) valueExpr).getKind();
-			String value = String.valueOf(((IASTLiteralExpression) valueExpr).getValue());
-			switch (kind) {
-			case IASTLiteralExpression.lk_integer_constant:
-				// 0 = False, > 0 = True
-				result = !value.equals("0");
-			}
-		}
-		// TODO other variable assignments
-		return result;
-	}
 }