PSA working for simple variable assignments and conditionals. PropSim implemented, but needs proper join op.

* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java: Store/bind truth assignments.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionStateClause.java: Use IVariable as atom.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java: Modified for truth assignments.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/VariableAssignmentVisitor.java: Determine truth value from assignment statement.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java: Analyze every function;
	parse conditional expressions and determine feasible branches; PropSim grouping method (not used ATM).

5 files changed, 300 insertions, 48 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 6f4f496..208f9f0 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
@@ -11,29 +11,89 @@
 package org.eclipse.cdt.codan.extension;
 
 import java.util.ArrayList;
+import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
+
+import org.eclipse.cdt.core.dom.ast.IVariable;
 
 public class ExecutionState {
 	private List<ExecutionStateClause> clauses;
+	private Map<IVariable, Boolean> truthAssignments;
 	private boolean top;
 	private boolean bottom;
 
 	public ExecutionState() {
+		truthAssignments = new HashMap<IVariable, Boolean>();
 		clauses = new ArrayList<ExecutionStateClause>();
+		top = true;
+		bottom = false;
 	}
 	
-	public void addClause(ExecutionStateClause node) {
-		setTop(false);
-		setBottom(false);
-		clauses.add(node);
+	public void addClause(ExecutionStateClause clause) {
+		// Cannot get out of bottom, do not add duplicate clauses
+		if (!bottom && !clauses.contains(clause)) {
+			top = false; // T AND x = x
+			if (clauses.contains(clause.getNegation())) {
+				clauses.clear();
+				bottom = true; // x AND NOT x = F
+			}
+			else {
+				clauses.add(clause);
+			}
+		}
 	}
 	
 	public void removeClause(ExecutionStateClause node) {
 		clauses.remove(node);
 		if (clauses.size() == 0) {
-			setTop(true);
-			setBottom(false);
+			setTop();
+		}
+	}
+	
+	public void addTruthAssignment(IVariable var, boolean value) {
+		truthAssignments.put(var, value);
+	}
+	
+	public Map<IVariable, Boolean> getTruthAssignments() {
+		return truthAssignments;
+	}
+	
+	public void setTruthAssignments(Map<IVariable, Boolean> truthAssignments) {
+		this.truthAssignments = truthAssignments;
+	}
+	
+	public void bindTruthAssignments() {
+		boolean unsatisfiable = false;
+		List<ExecutionStateClause> clausesCopy = new ArrayList<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;
+				}
+			}
+		}
+		
+		if (unsatisfiable) {
+			setBottom();
+		}
+	}
+	
+	//FIXME
+	public ExecutionState join(ExecutionState other) {
+		// Add clauses from other, canceling out negating clauses
+		for (ExecutionStateClause clause : other.getClauses()) {
+			ExecutionStateClause negation = clause.getNegation();
+			if (clauses.contains(negation)) {
+				removeClause(negation);
+				other.removeClause(clause);
+			}
 		}
+		return this;
 	}
 	
 	public ExecutionStateClause[] getClauses() {
@@ -48,12 +108,16 @@ public class ExecutionState {
 		return bottom;
 	}
 	
-	public void setTop(boolean top) {
-		this.top = top;
+	public void setTop() {
+		top = true;
+		bottom = false;
+		clauses.clear();
 	}
 	
-	public void setBottom(boolean bottom) {
-		this.bottom = bottom;
+	public void setBottom() {
+		bottom = true;
+		top = false;
+		clauses.clear();
 	}
 	
 	@Override
@@ -69,10 +133,7 @@ public class ExecutionState {
 			StringBuffer buf = new StringBuffer();
 			if (clauses.size() > 0) {
 				for (ExecutionStateClause c : clauses) {
-					if (!c.isTrue()) {
-						buf.append("NOT ");
-					}
-					buf.append(c.getNode().getRawSignature());
+					buf.append(c);
 					buf.append(" AND ");
 				}
 				buf.delete(buf.length() - 5 /* " AND ".length() */, buf.length());
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionStateClause.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionStateClause.java
index adb4e62..ab44d93 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionStateClause.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionStateClause.java
@@ -10,37 +10,55 @@
  *******************************************************************************/
 package org.eclipse.cdt.codan.extension;
 
-import org.eclipse.cdt.core.dom.ast.IASTNode;
+import org.eclipse.cdt.core.dom.ast.IVariable;
 
 public class ExecutionStateClause {
 	
-	private IASTNode node;
-	private boolean truthValue;
+	protected IVariable var;
+	protected boolean truthValue;
 
-	public ExecutionStateClause(IASTNode node) {
-		this(node, true);
+	public ExecutionStateClause(IVariable var) {
+		this(var, true);
 	}
 	
-	public ExecutionStateClause(IASTNode node, boolean truthValue) {
-		this.node = node;
+	public ExecutionStateClause(IVariable var, boolean truthValue) {
+		this.var = var;
 		this.truthValue = truthValue;
 	}
 
-	public IASTNode getNode() {
-		return node;
+	public IVariable getVariable() {
+		return var;
 	}
 	
 	public boolean isTrue() {
 		return truthValue;
 	}
 	
+	public ExecutionStateClause getNegation() {
+		return new ExecutionStateClause(var, !truthValue);
+	}
+	
+	@Override
+	public boolean equals(Object obj) {
+		if (obj instanceof ExecutionStateClause) {
+			ExecutionStateClause other = (ExecutionStateClause) obj;
+			return var.equals(other.getVariable()) && truthValue == other.isTrue();
+		}
+		return false;
+	}
+	
+	@Override
+	public int hashCode() {
+		return var.hashCode() + (truthValue ? 1 : 0);
+	}
+	
 	@Override
 	public String toString() {
 		StringBuffer buf = new StringBuffer();
 		if (!truthValue) {
 			buf.append("NOT ");
 		}
-		buf.append(node.getRawSignature());
+		buf.append(var.getName());
 		return buf.toString();
 	}
 	
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 ad932ac..93bf3be 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
@@ -11,9 +11,13 @@
 package org.eclipse.cdt.codan.extension;
 
 import java.util.Collections;
+import java.util.HashMap;
 import java.util.HashSet;
+import java.util.Map;
 import java.util.Set;
 
+import org.eclipse.cdt.core.dom.ast.IVariable;
+
 public class SymbolicState {
 	private Set<PropertyState> propertyStates;
 	private ExecutionState executionState;
@@ -45,6 +49,9 @@ public class SymbolicState {
 		for (ExecutionStateClause cl : executionState.getClauses()) {
 			es.addClause(cl);
 		}
+		Map<IVariable, Boolean> truthAssignments = new HashMap<IVariable, Boolean>(executionState.getTruthAssignments());
+		es.setTruthAssignments(truthAssignments);
+		
 		return new SymbolicState(ps, es);
 	}
 	
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 ebe4ce4..2530210 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
@@ -4,8 +4,14 @@ import org.eclipse.cdt.core.dom.ast.ASTVisitor;
 import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression;
 import org.eclipse.cdt.core.dom.ast.IASTDeclarator;
 import org.eclipse.cdt.core.dom.ast.IASTExpression;
+import org.eclipse.cdt.core.dom.ast.IASTIdExpression;
 import org.eclipse.cdt.core.dom.ast.IASTInitializer;
+import org.eclipse.cdt.core.dom.ast.IASTInitializerExpression;
+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.IBinding;
+import org.eclipse.cdt.core.dom.ast.IVariable;
 
 /*******************************************************************************
  * Copyright (c) 2009 Elliott Baron
@@ -31,7 +37,11 @@ public class VariableAssignmentVisitor extends ASTVisitor {
 	public int visit(IASTInitializer initializer) {
 		IASTNode parent = initializer.getParent();
 		if (parent instanceof IASTDeclarator) {
-			es.addClause(new ExecutionStateClause(parent));
+			if (initializer instanceof IASTInitializerExpression) {
+				IASTDeclarator decl = (IASTDeclarator) parent;
+				IASTExpression expr = ((IASTInitializerExpression) initializer).getExpression();
+				parseAssignment(parent, decl.getName(), expr);
+			}
 			return PROCESS_SKIP;
 		}
 		return PROCESS_CONTINUE;
@@ -44,13 +54,43 @@ public class VariableAssignmentVisitor extends ASTVisitor {
 			int op = binExpr.getOperator();
 
 			// Check operator is an assignment operator
-			if (op >= IASTBinaryExpression.op_assign
-					&& op <= IASTBinaryExpression.op_binaryOrAssign) {
-				es.addClause(new ExecutionStateClause(binExpr));					
+			if (op == IASTBinaryExpression.op_assign) { // FIXME other ops
+				IASTExpression o1 = binExpr.getOperand1();
+				if (o1 instanceof IASTIdExpression) {
+					IASTName name = ((IASTIdExpression) o1).getName();
+					parseAssignment(binExpr, name, binExpr.getOperand2());
+				}
 				return PROCESS_SKIP;
 			}
 		}		
 		return PROCESS_CONTINUE;
 	}
 
+	private void parseAssignment(IASTNode parent, IASTName name, IASTExpression valueExpr) {
+		IBinding binding = name.resolveBinding();
+		if (binding instanceof IVariable) {
+			IVariable var = (IVariable) binding;
+			Boolean truth = getTruthValue(valueExpr);
+			if (truth != null) {
+				es.addTruthAssignment(var, truth);
+			}
+		}
+	}
+
+	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/checkers/CloseOpenedFilesChecker.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java
index 04348ab..a38ef13 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
@@ -27,9 +27,17 @@ import org.eclipse.cdt.codan.extension.ExecutionStateClause;
 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;
@@ -81,19 +89,22 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
 			ICallGraph cg = creator.createCallGraph(proj);
 			creator.computeCallGraph(cg);
 
-			// Create control flow graph
-			ICallGraphNode cgRoot = cg.topEntry();
-			IASTStatement fnBody = cgRoot.getFuncDef().getBody();
-			IControlFlowGraph cfg = new ControlFlowGraph(fnBody);
-			cfg.buildCFG();
+			// Create control flow graph for each function
+			for (ICallGraphNode node : cg.getAllNodes()) {
+				IASTStatement fnBody = node.getFuncDef().getBody();
+				IControlFlowGraph cfg = new ControlFlowGraph(fnBody);
+				cfg.buildCFG();
 
-			solve(cfg);
-			
-			IControlFlowEdge exitEdge = cfg.getExit().getInEdges()[0];
-			for (SymbolicState s : edgeInfo.get(exitEdge)) {
-				if (s.getPropertyStates().contains(error)) {
-					// Report problem
-					reportProblem(errorNode, s.getExecutionState());
+				// Search for error states using property simulation algorithm
+				solve(cfg);
+
+				// Check if the exit edge of the CFG contains an error state
+				IControlFlowEdge exitEdge = cfg.getExit().getInEdges()[0];
+				for (SymbolicState s : edgeInfo.get(exitEdge)) {
+					if (s.getPropertyStates().contains(error)) {
+						// Report problem
+						reportProblem(errorNode, s.getExecutionState());
+					}
 				}
 			}
 		}		
@@ -112,9 +123,7 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
 		Set<SymbolicState> symStates = edgeInfo.get(entryEdge);
 		Set<PropertyState> propStates = new HashSet<PropertyState>();
 		propStates.add(uninit);
-		ExecutionState es = new ExecutionState();
-		es.setTop(true);
-		symStates.add(new SymbolicState(propStates, es));
+		symStates.add(new SymbolicState(propStates, new ExecutionState()));
 
 		worklist.add(entryEdge.getTo());
 		// XXX Debug
@@ -199,20 +208,99 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
 	}
 
 	private Set<SymbolicState> group(Set<SymbolicState> ss) {
-		// FIXME Fully Path Sensitive
+		return groupPSA(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);
+			ExecutionState es = new ExecutionState();
+			for (ExecutionState e : statesPerProperty.get(p)) {
+				es.join(e);
+			}
+			SymbolicState s = new SymbolicState(ps, es);
+			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) {
-			// TODO Theorem Prover goes here! / Determine if branch is feasible
-			
+		if (node != null) {			
 			// Modify execution state according to branch condition
+			ExecutionStateClause clause = null;
 			// *N.B.* content for condition IBlock is condition expression itself
-			ret.getExecutionState().addClause(new ExecutionStateClause(node, value)); 
+			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;
@@ -313,4 +401,42 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
 		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);
+			}
+		}
+		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;
+	}
 }