1 files changed, 92 insertions, 0 deletions
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);
+
+}