Attempt to parse disjunctions into execution states. Most likely does not work.disjunct-exp

* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ConditionalVisitor.java: Recurse on disjunctions.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java: Expect Set of SymbolicStates from
	ConditionalVisitor.

2 files changed, 54 insertions, 24 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..8b3b15e 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
@@ -1,5 +1,17 @@
+/*******************************************************************************
+ * 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;
+
 import org.eclipse.cdt.core.dom.ast.ASTVisitor;
 import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression;
 import org.eclipse.cdt.core.dom.ast.IASTExpression;
@@ -10,11 +22,13 @@ import org.eclipse.cdt.core.dom.ast.IBinding;
 import org.eclipse.cdt.core.dom.ast.IVariable;
 
 public class ConditionalVisitor extends ASTVisitor {
-	private ExecutionState es;
+	private Set<SymbolicState> output;
+	private SymbolicState input;
 	private boolean value;
 
-	public ConditionalVisitor(ExecutionState es, boolean value) {
-		this.es = es;
+	public ConditionalVisitor(SymbolicState s, Set<SymbolicState> ret, boolean value) {
+		output = ret;
+		input = s;
 		this.value = value;
 		shouldVisitExpressions = true;
 	}
@@ -36,16 +50,29 @@ public class ConditionalVisitor extends ASTVisitor {
 				IASTExpression o1 = binExpr.getOperand1();
 				if (o1 instanceof IASTIdExpression) {
 					IASTName name = ((IASTIdExpression) o1).getName();
-					clause = parseConditional(clause, name, binExpr.getOperand2(), value);
+					clause = parseConditional(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
+					clause = parseConditional(name, binExpr.getOperand2(), !value); // Negation
 				}
 			}
+			else if (op == IASTBinaryExpression.op_logicalOr) {
+				// Disjunction creates two possible execution states
+				SymbolicState s1 = input.copy();
+				SymbolicState s2 = input.copy();
+				ConditionalVisitor cv1 = new ConditionalVisitor(s1, output, value);
+				ConditionalVisitor cv2 = new ConditionalVisitor(s2, output, value);
+				IASTExpression o1 = binExpr.getOperand1();
+				IASTExpression o2 = binExpr.getOperand2();
+				o1.accept(cv1);
+				o2.accept(cv2);
+				// don't process anymore, children will take care of this
+				ret = PROCESS_SKIP;
+			}
 		}
 		else if (node instanceof IASTUnaryExpression) { // if (!x)
 			IASTUnaryExpression uExpr = (IASTUnaryExpression) node;
@@ -56,19 +83,20 @@ public class ConditionalVisitor extends ASTVisitor {
 				IASTExpression operand = uExpr.getOperand();
 				if (operand instanceof IASTIdExpression) {
 					IASTName name = ((IASTIdExpression) operand).getName();
-					clause = parseConditional(clause, name, !value); // Negation
+					clause = parseConditional(name, !value); // Negation
 				}
 			}
 		}
 		else if (node instanceof IASTIdExpression) { // if (x)
 			IASTName name = ((IASTIdExpression) node).getName();
-			clause = parseConditional(clause, name, value);
+			clause = parseConditional(name, value);
 		}
 		
 		if (clause != null) {
-			es.addClause(clause);
+			// Add clause to input
+			input.getExecutionState().addClause(clause);
 			// TODO Theorem Prover goes here! / Determine if branch is feasible
-			es.bindTruthAssignments();
+			input.getExecutionState().bindTruthAssignments();
 			ret = PROCESS_SKIP;
 		}
 		else {
@@ -77,7 +105,12 @@ public class ConditionalVisitor extends ASTVisitor {
 		return ret;
 	}
 	
-	private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, IASTExpression valueExpr, boolean branchTruth) {
+	public Set<SymbolicState> getOutput() {
+		return output;
+	}
+	
+	private ExecutionStateClause parseConditional(IASTName name, IASTExpression valueExpr, boolean branchTruth) {
+		ExecutionStateClause clause = null;
 		IBinding binding = name.resolveBinding();
 		if (binding instanceof IVariable) {
 			IVariable var = (IVariable) binding;
@@ -89,7 +122,8 @@ public class ConditionalVisitor extends ASTVisitor {
 		return clause;
 	}
 	
-	private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, boolean branchTruth) {
+	private ExecutionStateClause parseConditional(IASTName name, boolean branchTruth) {
+		ExecutionStateClause clause = null;
 		IBinding binding = name.resolveBinding();
 		if (binding instanceof IVariable) {
 			IVariable var = (IVariable) binding;
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..c7a8107 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;
@@ -213,9 +206,11 @@ public class PropertySimulator {
 	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);
+			Set<SymbolicState> ss0 = transferBranch(blk, s, value);
+			for (SymbolicState s0 : ss0) {
+				if (!s0.getExecutionState().isBottom()) {
+					ret.add(s0);
+				}
 			}
 		}
 		return group(ret);
@@ -304,12 +299,13 @@ public class PropertySimulator {
 		return null;
 	}
 
-	private SymbolicState transferBranch(IBlock blk, SymbolicState s, boolean value) {
+	private Set<SymbolicState> transferBranch(IBlock blk, SymbolicState s, boolean value) {
 		IASTNode node = blk.getContent();
 		
-		SymbolicState ret = s.copy();
+		Set<SymbolicState> ret = new HashSet<SymbolicState>();
+		ret.add(s.copy());
 		if (node != null) {			
-			ConditionalVisitor visitor = new ConditionalVisitor(ret.getExecutionState(), value);
+			ConditionalVisitor visitor = new ConditionalVisitor(s, ret, value);
 			node.accept(visitor);
 		}