Remove truth assignments at merge points, based on dominance in CFG.

* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java: Change to truth assignments map.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java: Likewise.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java: Remove truth assigments in flowMerge().
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/VariableAssignmentVisitor.java: Store IBlock corresponding to TA.

5 files changed, 75 insertions, 20 deletions

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 fd8032a..3ea27b6 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
@@ -16,15 +16,16 @@ import java.util.Map;
 import java.util.Set;
 
 import org.eclipse.cdt.core.dom.ast.IVariable;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IBlock;
 
 public class ExecutionState {
 	private Set<ExecutionStateClause> clauses;
-	private Map<IVariable, Boolean> truthAssignments; // FIXME this should be more robust, use SSA
+	private Map<IVariable, TruthAssignment> truthAssignments; // FIXME this should be more robust, use SSA
 	private boolean top;
 	private boolean bottom;
 
 	public ExecutionState() {
-		truthAssignments = new HashMap<IVariable, Boolean>();
+		truthAssignments = new HashMap<IVariable, TruthAssignment>();
 		clauses = new HashSet<ExecutionStateClause>();
 		top = true;
 		bottom = false;
@@ -50,15 +51,15 @@ public class ExecutionState {
 		}
 	}
 
-	public void addTruthAssignment(IVariable var, boolean value) {
-		truthAssignments.put(var, value);
+	public void addTruthAssignment(IVariable var, boolean value, IBlock blk) {
+		truthAssignments.put(var, new TruthAssignment(blk, value));
 	}
 
-	public Map<IVariable, Boolean> getTruthAssignments() {
+	public Map<IVariable, TruthAssignment> getTruthAssignments() {
 		return truthAssignments;
 	}
 
-	public void setTruthAssignments(Map<IVariable, Boolean> truthAssignments) {
+	public void setTruthAssignments(Map<IVariable, TruthAssignment> truthAssignments) {
 		this.truthAssignments = truthAssignments;
 	}
 
@@ -67,13 +68,16 @@ public class ExecutionState {
 		Set<ExecutionStateClause> clausesCopy = new HashSet<ExecutionStateClause>(
 				clauses);
 		for (ExecutionStateClause c : clausesCopy) {
-			Boolean truth = truthAssignments.get(c.getVariable());
-			if (truth != null) {
-				if (truth == c.isTrue()) { // does truth value of clause match
-											// truth assignment?
-					removeClause(c);
-				} else {
-					unsatisfiable = true;
+			TruthAssignment ta = truthAssignments.get(c.getVariable());
+			if (ta != null) {
+				Boolean truth = ta.getValue();
+				if (truth != null) {
+					if (truth == c.isTrue()) { // does truth value of clause match
+						// truth assignment?
+						removeClause(c);
+					} else {
+						unsatisfiable = true;
+					}
 				}
 			}
 		}
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
index ffd3ada..ba9199f 100644
--- 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
@@ -13,9 +13,11 @@ package org.eclipse.cdt.codan.extension;
 import java.util.HashMap;
 import java.util.HashSet;
 import java.util.LinkedList;
+import java.util.List;
 import java.util.Map;
 import java.util.Queue;
 import java.util.Set;
+import java.util.Map.Entry;
 
 import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression;
 import org.eclipse.cdt.core.dom.ast.IASTExpression;
@@ -122,11 +124,36 @@ public class PropertySimulator {
 	private Set<SymbolicState> flowMerge(IBlock blk, Set<SymbolicState> ss1,
 			Set<SymbolicState> ss2) {
 		Set<SymbolicState> ret = new HashSet<SymbolicState>();
-		ret.addAll(ss1);
-		ret.addAll(ss2);
+		ret.addAll(filterTruthAssignments(blk, ss1));
+		ret.addAll(filterTruthAssignments(blk, ss2));
 		return group(ret);
 	}
 
+	private Set<SymbolicState> filterTruthAssignments(IBlock blk, Set<SymbolicState> ss) {
+		Set<SymbolicState> ret = new HashSet<SymbolicState>(ss.size());
+		for (SymbolicState s : ss) {
+			SymbolicState copy = s.copy();
+			Set<IVariable> toRemove = new HashSet<IVariable>();
+			Map<IVariable, TruthAssignment> truthAssignments = copy.getExecutionState().getTruthAssignments();
+			for (Entry<IVariable, TruthAssignment> ta : truthAssignments.entrySet()) {
+				// FIXME could be better
+				// Remove truth assignments that were added by a block that doesn't dominate this one
+				List<IBlock> dominators = blk.getDOM();
+				IBlock origin = ta.getValue().getOrigin();
+				if (!dominators.contains(origin)) {
+					// Schedule removal
+					toRemove.add(ta.getKey());
+				}
+			}
+			// Actually remove
+			for (IVariable var : toRemove) {
+				truthAssignments.remove(var);
+			}
+			ret.add(copy);
+		}
+		return ret;
+	}
+
 	private Set<SymbolicState> flowBranch(IBlock blk, Set<SymbolicState> ss, boolean value) {
 		Set<SymbolicState> ret = new HashSet<SymbolicState>();
 		for (SymbolicState s : ss) {
@@ -300,7 +327,7 @@ public class PropertySimulator {
 			s.setPropertyStates(newStates);
 			
 			// Modify execution state according to variable assignments
-			node.accept(new VariableAssignmentVisitor(s.getExecutionState()));
+			node.accept(new VariableAssignmentVisitor(blk, s.getExecutionState()));
 		}
 		return s;
 	}
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 76db5ea..db551aa 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
@@ -49,7 +49,7 @@ public class SymbolicState {
 	public SymbolicState copy() {
 		Set<PropertyState> ps = new HashSet<PropertyState>(propertyStates);
 		ExecutionState es = executionState.copy();
-		Map<IVariable, Boolean> truthAssignments = new HashMap<IVariable, Boolean>(executionState.getTruthAssignments());
+		Map<IVariable, TruthAssignment> truthAssignments = new HashMap<IVariable, TruthAssignment>(executionState.getTruthAssignments());
 		es.setTruthAssignments(truthAssignments);
 		
 		SymbolicState ret = new SymbolicState(ps, es);
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java
new file mode 100644
index 0000000..a9c50dc
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java
@@ -0,0 +1,22 @@
+package org.eclipse.cdt.codan.extension;
+
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IBlock;
+
+public class TruthAssignment {	
+	private IBlock blk;
+	private Boolean value;
+
+	public TruthAssignment(IBlock blk, Boolean value) {
+		this.blk = blk;
+		this.value = value;
+	}
+	
+	public IBlock getOrigin() {
+		return blk;
+	}
+	
+	public Boolean getValue() {
+		return value;
+	}
+
+}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/VariableAssignmentVisitor.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/VariableAssignmentVisitor.java
index 2530210..c167129 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/VariableAssignmentVisitor.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/VariableAssignmentVisitor.java
@@ -12,6 +12,7 @@ import org.eclipse.cdt.core.dom.ast.IASTName;
 import org.eclipse.cdt.core.dom.ast.IASTNode;
 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;
 
 /*******************************************************************************
  * Copyright (c) 2009 Elliott Baron
@@ -24,10 +25,11 @@ import org.eclipse.cdt.core.dom.ast.IVariable;
  *    Elliott Baron - initial API and implementation
  *******************************************************************************/
 public class VariableAssignmentVisitor extends ASTVisitor {
-	
+	private IBlock blk;
 	private ExecutionState es;
 
-	public VariableAssignmentVisitor(ExecutionState es) {
+	public VariableAssignmentVisitor(IBlock blk, ExecutionState es) {
+		this.blk = blk;
 		this.es = es;
 		shouldVisitInitializers = true;
 		shouldVisitExpressions = true;		
@@ -72,7 +74,7 @@ public class VariableAssignmentVisitor extends ASTVisitor {
 			IVariable var = (IVariable) binding;
 			Boolean truth = getTruthValue(valueExpr);
 			if (truth != null) {
-				es.addTruthAssignment(var, truth);
+				es.addTruthAssignment(var, truth, blk);
 			}
 		}
 	}