Properly handle binary expressions, improved debugging output, handle property transitions in branch nodes.

* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ConditionalVisitor.java: Don't assume binary expressions are &&.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java: Better debug, property transitions.

2 files changed, 45 insertions, 30 deletions

diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ConditionalVisitor.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ConditionalVisitor.java
index 0cbc11a..8959675 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ConditionalVisitor.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ConditionalVisitor.java
@@ -21,7 +21,7 @@ public class ConditionalVisitor extends ASTVisitor {
 
 	@Override
 	public int visit(IASTExpression node) {
-		int ret = PROCESS_CONTINUE;
+		int ret = PROCESS_SKIP;
 		// Modify execution state according to branch condition
 		ExecutionStateClause clause = null;
 		// *N.B.* content for condition IBlock is condition expression itself
@@ -46,6 +46,9 @@ public class ConditionalVisitor extends ASTVisitor {
 					clause = parseConditional(clause, name, binExpr.getOperand2(), !value); // Negation
 				}
 			}
+			else if (op == IASTBinaryExpression.op_logicalAnd) {
+				ret = PROCESS_CONTINUE; // Continue processing conjunctions
+			}
 		}
 		else if (node instanceof IASTUnaryExpression) { // if (!x)
 			IASTUnaryExpression uExpr = (IASTUnaryExpression) node;
@@ -69,7 +72,6 @@ public class ConditionalVisitor extends ASTVisitor {
 			es.addClause(clause);
 			// TODO Theorem Prover goes here! / Determine if branch is feasible
 			es.bindTruthAssignments();
-			ret = PROCESS_SKIP;
 		}
 		else {
 			// FIXME Handle unresolvable case
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 1cd6911..72efca2 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
@@ -19,15 +19,8 @@ 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;
 import org.eclipse.cdt.core.dom.ast.IASTFileLocation;
-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;
@@ -77,7 +70,7 @@ public class PropertySimulator {
 
 		worklist.add(entryEdge.getTo());
 		// XXX Debug
-		System.out.println(printStates(entryEdge, symStates));
+		System.out.println(printStates(entryEdge, symStates, symStates));
 
 		while (!worklist.isEmpty()) {
 			IBlock blk = worklist.remove();
@@ -88,14 +81,17 @@ public class PropertySimulator {
 			
 			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]));
+				Set<SymbolicState> oldStatesTrue = edgeInfo.get(blk.getInEdges()[0]);
+				Set<SymbolicState> oldStatesFalse = edgeInfo.get(blk.getInEdges()[1]);
+				Set<SymbolicState> newStates = flowMerge(blk, oldStatesTrue, oldStatesFalse);
 				
 				// Don't process the null exit block
 				if (!blk.equals(cfg.getExit())) {
 					add(blk.getOutEdges()[0], newStates);
 
 					// XXX Debug
-					System.out.println("MRG: " + printStates(blk.getOutEdges()[0], newStates));
+					System.out.println("MRG: " + printStates(blk.getOutEdges()[0], oldStatesTrue, newStates));
+					System.out.println("MRG: " + printStates(blk.getOutEdges()[0], oldStatesFalse, newStates));
 				}
 			}
 			else if (isBranch(blk)) {
@@ -109,18 +105,19 @@ public class PropertySimulator {
 				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));
+				System.out.println("BR (T): " + printStates(blk.getOutEdges()[0], oldStates, newStatesTrue));
+				System.out.println("BR (F): " + printStates(blk.getOutEdges()[1], oldStates, newStatesFalse));
 			}
 			else {
 				// Apply flow function for a normal block
-				Set<SymbolicState> newStates = flowOther(blk, edgeInfo.get(blk.getInEdges()[0]));
+				Set<SymbolicState> oldStates = edgeInfo.get(blk.getInEdges()[0]);
+				Set<SymbolicState> newStates = flowOther(blk, oldStates);
 				
 				// 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));
+					System.out.println("OTH: " + printStates(blk.getOutEdges()[0], oldStates, newStates));
 				}
 			}
 		}
@@ -150,7 +147,7 @@ public class PropertySimulator {
 		return edgeInfo.get(exitEdge);
 	}
 	
-	private String printStates(IControlFlowEdge edge, Set<SymbolicState> states) {
+	private String printStates(IControlFlowEdge edge, Set<SymbolicState> oldStates, Set<SymbolicState> newStates) {
 		StringBuffer buf = new StringBuffer();
 		IASTNode from = edge.getFrom().getContent();
 		IASTNode to = edge.getTo().getContent();
@@ -169,11 +166,17 @@ public class PropertySimulator {
 			}
 		}
 		buf.append("{");
+		buf.append("[" + edge.getFrom().getID() + "] ");
 		buf.append(from == null ? from : from.getRawSignature());
 		buf.append(" -> ");
+		buf.append("[" + edge.getTo().getID() + "] ");
 		buf.append(to == null ? to : to.getRawSignature());
 		buf.append("} = ");
-		buf.append(states);
+		buf.append("\n");
+		buf.append("From: " + oldStates);
+		buf.append("\n");
+		buf.append("To: " + newStates);
+		buf.append("\n");
 		return buf.toString();		
 	}
 
@@ -211,6 +214,9 @@ public class PropertySimulator {
 	}
 
 	private Set<SymbolicState> flowBranch(IBlock blk, Set<SymbolicState> ss, boolean value) {
+		if (blk.getContent() != null && blk.getContent().getRawSignature().equals("is_stdin && fclose (fp) != 0")) {
+			System.out.println("ZOMG");
+		}
 		Set<SymbolicState> ret = new HashSet<SymbolicState>();
 		for (SymbolicState s : ss) {
 			SymbolicState s0 = transferBranch(blk, s, value);
@@ -308,7 +314,10 @@ public class PropertySimulator {
 		IASTNode node = blk.getContent();
 		
 		SymbolicState ret = s.copy();
-		if (node != null) {			
+		if (node != null) {	
+			// Process property state transition
+			propertyTransition(s, node);
+			
 			ConditionalVisitor visitor = new ConditionalVisitor(ret.getExecutionState(), value);
 			node.accept(visitor);
 		}
@@ -321,17 +330,7 @@ public class PropertySimulator {
 		
 		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);
+			propertyTransition(s, node);
 			
 			// Modify execution state according to variable assignments
 			node.accept(new VariableAssignmentVisitor(blk, s.getExecutionState()));
@@ -339,6 +338,20 @@ public class PropertySimulator {
 		return s;
 	}
 
+	private void propertyTransition(SymbolicState s, IASTNode node) {
+		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);
+	}
+
 	private boolean isBranch(IBlock blk) {
 		return blk.getOutEdges().length > 1;
 	}