blob: d066392fe4dc5f4943914d83c670c8c8b8d93ac5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
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.cxx.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);
}
|
