From 14807e0d157e64a50ebd8df4e6f3b2897081296f Mon Sep 17 00:00:00 2001 From: Elliott Baron Date: Mon, 14 Dec 2009 23:22:52 -0500 Subject: 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. --- .../cdt/codan/extension/ConditionalVisitor.java | 10 +++ .../cdt/codan/extension/PropertySimulator.java | 4 +- .../cdt/codan/extension/TruthAssignment.java | 10 +++ .../codan/extension/VariableAssignmentVisitor.java | 15 ++-- .../checkers/AbstractOpenCloseChecker.java | 62 ++------------- .../extension/checkers/AbstractPropSimChecker.java | 92 ++++++++++++++++++++++ 6 files changed, 132 insertions(+), 61 deletions(-) create mode 100644 org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractPropSimChecker.java 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 group(Set ss) { return groupPropSim(ss); } - + + /* private Set groupPSA(Set ss) { return ss; } + */ private Set groupPropSim(Set ss) { Set ret = new HashSet(); 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); + +} -- cgit