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.

1 files changed, 30 insertions, 3 deletions

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;
 	}