Create abstract checker to use Property Simulation. Clean up code.

* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ConditionalVisitor.java: Added copyright notice.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java: Commented out groupPSA.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java: Added copyright notice.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/VariableAssignmentVisitor.java: Likewise.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractOpenCloseChecker.java: Extracted most code.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractPropSimChecker.java: New file.

6 files changed, 132 insertions, 61 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 8959675..651038a 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,3 +1,13 @@
+/*******************************************************************************
+ * 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 org.eclipse.cdt.core.dom.ast.ASTVisitor;
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 72efca2..e0b75df 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
@@ -239,10 +239,12 @@ public class PropertySimulator {
 	private Set<SymbolicState> group(Set<SymbolicState> ss) {
 		return groupPropSim(ss);
 	}
-	
+
+	/*
 	private Set<SymbolicState> groupPSA(Set<SymbolicState> ss) {
 		return ss;
 	}
+	*/
 	
 	private Set<SymbolicState> groupPropSim(Set<SymbolicState> ss) {
 		Set<SymbolicState> ret = new HashSet<SymbolicState>();
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
index ffc1502..c0505d9 100644
--- 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
@@ -1,3 +1,13 @@
+/*******************************************************************************
+ * 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 org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IBlock;
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 28c12f2..0f6a2ad 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
@@ -1,19 +1,24 @@
+/*******************************************************************************
+ * 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 org.eclipse.cdt.core.dom.ast.ASTTypeUtil;
 import org.eclipse.cdt.core.dom.ast.ASTVisitor;
 import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression;
-import org.eclipse.cdt.core.dom.ast.IASTCastExpression;
 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.IASTTypeId;
-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;
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractOpenCloseChecker.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractOpenCloseChecker.java
index 6bc453c..4b45994 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractOpenCloseChecker.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractOpenCloseChecker.java
@@ -10,31 +10,15 @@
  *******************************************************************************/
 package org.eclipse.cdt.codan.extension.checkers;
 
-import java.io.File;
-import java.net.URI;
 import java.util.HashSet;
 import java.util.Set;
 
-import org.eclipse.cdt.codan.core.model.AbstractIndexAstChecker;
 import org.eclipse.cdt.codan.extension.ExecutionState;
 import org.eclipse.cdt.codan.extension.IPropertyFSM;
-import org.eclipse.cdt.codan.extension.PropertySimulator;
 import org.eclipse.cdt.codan.extension.PropertyState;
-import org.eclipse.cdt.codan.extension.SymbolicState;
 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.core.resources.IProject;
-import org.eclipse.core.resources.IResource;
-import org.eclipse.core.resources.IWorkspaceRoot;
-import org.eclipse.core.resources.ResourcesPlugin;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.GraphCreator;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.ICallGraph;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.ICallGraphNode;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowGraph;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.impl.ControlFlowGraph;
 
-public abstract class AbstractOpenCloseChecker extends AbstractIndexAstChecker {	
+public abstract class AbstractOpenCloseChecker extends AbstractPropSimChecker {	
 	private IPropertyFSM fsm;
 	
 	// Property FSM states
@@ -44,44 +28,7 @@ public abstract class AbstractOpenCloseChecker extends AbstractIndexAstChecker {
 
 	public AbstractOpenCloseChecker() {
 		fsm = initFSM();
-	}
-
-	public void processAst(IASTTranslationUnit ast) {
-		GraphCreator creator = new GraphCreator();
-
-		// Retrieve resource corresponding to this translation unit
-		String path = ast.getFilePath();
-		URI fileURI = new File(path).toURI();
-		IWorkspaceRoot wsRoot = ResourcesPlugin.getWorkspace().getRoot();
-		IResource[] resources = wsRoot.findFilesForLocationURI(fileURI);
-		if (resources != null && resources.length > 0) {
-			IResource res = resources[0];
-
-			// Create call graph for resource
-			ICallGraph cg = creator.createCallGraph(res);
-			creator.computeCallGraph(cg);
-
-			// Create control flow graph for each function
-			for (ICallGraphNode node : cg.getAllNodes()) {
-				IASTStatement fnBody = node.getFuncDef().getBody();
-				IControlFlowGraph cfg = new ControlFlowGraph(fnBody);
-				cfg.buildCFG();
-
-				// Search for error states using property simulation algorithm
-				PropertySimulator sim = new PropertySimulator(cfg, fsm);
-
-				// Check if the exit edge of the CFG contains an error state
-				for (SymbolicState s : sim.getEndStates()) {
-					if (s.getPropertyStates().contains(error)) {
-						// Report problems
-						for (IASTNode errorNode : s.getErrorCauses()) {
-							reportProblem(errorNode, s.getExecutionState());
-						}
-					}
-				}
-			}
-		}		
-	}
+	}	
 	
 	private IPropertyFSM initFSM() {
 		uninit = new PropertyState("$u") {			
@@ -143,6 +90,11 @@ public abstract class AbstractOpenCloseChecker extends AbstractIndexAstChecker {
 		};
 	}
 	
+	@Override
+	protected IPropertyFSM getPropertyFSM() {
+		return fsm;
+	}
+	
 	protected abstract boolean containsOpen(IASTNode node);
 
 	protected abstract boolean containsClose(IASTNode node);
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractPropSimChecker.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractPropSimChecker.java
new file mode 100644
index 0000000..de8d818
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractPropSimChecker.java
@@ -0,0 +1,92 @@
+/*******************************************************************************
+ * 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.checkers;
+
+import java.io.File;
+import java.net.URI;
+
+import org.eclipse.cdt.codan.core.model.AbstractIndexAstChecker;
+import org.eclipse.cdt.codan.extension.ExecutionState;
+import org.eclipse.cdt.codan.extension.IPropertyFSM;
+import org.eclipse.cdt.codan.extension.PropertySimulator;
+import org.eclipse.cdt.codan.extension.SymbolicState;
+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.core.resources.IResource;
+import org.eclipse.core.resources.IWorkspaceRoot;
+import org.eclipse.core.resources.ResourcesPlugin;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.GraphCreator;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.ICallGraph;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.ICallGraphNode;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowGraph;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.impl.ControlFlowGraph;
+
+/**
+ * Abstract checker that uses intra-procedural Property Simulation for its analysis model.
+ * A control flow graph is constructed for each function in the project and each is analyzed
+ * using Property Simulation, an efficient path-sensitive static analysis technique.
+ */
+public abstract class AbstractPropSimChecker extends AbstractIndexAstChecker {
+
+	@Override
+	public void processAst(IASTTranslationUnit ast) {
+		GraphCreator creator = new GraphCreator();
+
+		// Retrieve resource corresponding to this translation unit
+		String path = ast.getFilePath();
+		URI fileURI = new File(path).toURI();
+		IWorkspaceRoot wsRoot = ResourcesPlugin.getWorkspace().getRoot();
+		IResource[] resources = wsRoot.findFilesForLocationURI(fileURI);
+		if (resources != null && resources.length > 0) {
+			IResource res = resources[0];
+
+			// Create call graph for resource
+			ICallGraph cg = creator.createCallGraph(res);
+			creator.computeCallGraph(cg);
+
+			// Create control flow graph for each function
+			for (ICallGraphNode node : cg.getAllNodes()) {
+				IASTStatement fnBody = node.getFuncDef().getBody();
+				IControlFlowGraph cfg = new ControlFlowGraph(fnBody);
+				cfg.buildCFG();
+
+				// Search for error states using property simulation algorithm
+				IPropertyFSM fsm = getPropertyFSM();
+				PropertySimulator sim = new PropertySimulator(cfg, fsm);
+
+				// Check if the exit edge of the CFG contains an error state
+				for (SymbolicState s : sim.getEndStates()) {
+					if (s.getPropertyStates().contains(fsm.getErrorState())) {
+						// Report problems
+						for (IASTNode errorNode : s.getErrorCauses()) {
+							reportProblem(errorNode, s.getExecutionState());
+						}
+					}
+				}
+			}
+		}		
+	}
+	
+	/**
+	 * Define a finite state machine that encapsulates the desired temporal property.
+	 * @return said finite state machine
+	 */
+	protected abstract IPropertyFSM getPropertyFSM();
+	
+	/**
+	 * Callback to report violations of the temporal property to the user.
+	 * @param node - the node in the AST that triggered the error.
+	 * @param condition - the {@link ExecutionState} that causes the error to occur.
+	 */
+	protected abstract void reportProblem(IASTNode node, ExecutionState condition);
+
+}