summaryrefslogtreecommitdiffstats
path: root/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java
blob: 04348ab8ccd7c1c2a4a33a9c8828087c3e2ece28 (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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
/*******************************************************************************
 * 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 java.text.MessageFormat;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.Map;
import java.util.Queue;
import java.util.Set;

import org.eclipse.cdt.codan.core.model.AbstractIndexAstChecker;
import org.eclipse.cdt.codan.extension.Activator;
import org.eclipse.cdt.codan.extension.ExecutionState;
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.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.IBlock;
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.IControlFlowEdge;
import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowGraph;
import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.impl.ControlFlowGraph;

public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
	private static final String ERR_ID = Activator.PLUGIN_ID + ".CloseOpenedFilesProblem";
	
	private static final String OPEN = "open";
	private static final String CLOSE = "close";
	private Queue<IBlock> worklist;
	
	// Property simulation state info for CFG's edges
	private Map<IControlFlowEdge, Set<SymbolicState>> edgeInfo;
	
	// Property FSM states
	private PropertyState uninit;
	private PropertyState error;
	private PropertyState opened;
	
	// Most recent node to cause transition to error state
	private IASTNode errorNode;

	public CloseOpenedFilesChecker() {
		worklist = new LinkedList<IBlock>();
		edgeInfo = new HashMap<IControlFlowEdge, Set<SymbolicState>>();
		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) {
			IProject proj = resources[0].getProject();

			// Create call graph for project
			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();

			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());
				}
			}
		}		
	}


	private void solve(IControlFlowGraph cfg) {
		for (IControlFlowEdge edge : cfg.getEdges()) {
			// Initialize edgeInfo for each edge
			Set<SymbolicState> set = new HashSet<SymbolicState>();
			edgeInfo.put(edge, set);
		}

		// Create edgeInfo for entry edge
		IControlFlowEdge entryEdge = cfg.getEntry().getOutEdges()[0];
		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));

		worklist.add(entryEdge.getTo());
		// XXX Debug
		printStates(entryEdge, symStates);

		while (!worklist.isEmpty()) {
			IBlock blk = worklist.remove();
			if (isMerge(blk)) {
				// Apply flow function for a merge block
				Set<SymbolicState> newStates = flowMerge(blk, edgeInfo.get(blk.getInEdges()[0]), edgeInfo.get(blk.getInEdges()[1]));
				add(blk.getOutEdges()[0], newStates);
				
				// XXX Debug
				System.out.println("MRG: " + printStates(blk.getOutEdges()[0], newStates));
			}
			else if (isBranch(blk)) {
				// Apply flow function for a branch block
				Set<SymbolicState> oldStates = edgeInfo.get(blk.getInEdges()[0]);
				Set<SymbolicState> newStatesTrue = flowBranch(blk, oldStates, true);
				Set<SymbolicState> newStatesFalse = flowBranch(blk, oldStates, false);

				// Assumes 0th out-edge is true branch, 1st out-edge is false branch 
				add(blk.getOutEdges()[0], newStatesTrue);
				add(blk.getOutEdges()[1], newStatesFalse);
				
				// XXX Debug
				System.out.println("BR (T): " + printStates(blk.getOutEdges()[0], newStatesTrue));
				System.out.println("BR (F): " + printStates(blk.getOutEdges()[1], newStatesFalse));
			}
			else {
				// Apply flow function for a normal block
				Set<SymbolicState> newStates = flowOther(blk, edgeInfo.get(blk.getInEdges()[0]));
				
				// Don't process the null exit block
				if (!blk.equals(cfg.getExit())) {
					add(blk.getOutEdges()[0], newStates);
					// XXX Debug
					System.out.println("OTH: " + printStates(blk.getOutEdges()[0], newStates));
				}
			}
		}
	}


	private String printStates(IControlFlowEdge edge, Set<SymbolicState> states) {
		StringBuffer buf = new StringBuffer();
		IASTNode from = edge.getFrom().getContent();
		IASTNode to = edge.getTo().getContent();
		buf.append("{");
		buf.append(from == null ? from : from.getRawSignature());
		buf.append(" -> ");
		buf.append(to == null ? to : to.getRawSignature());
		buf.append("} = ");
		buf.append(states);
		return buf.toString();		
	}

	private Set<SymbolicState> flowMerge(IBlock blk, Set<SymbolicState> ss1,
			Set<SymbolicState> ss2) {
		ss1.addAll(ss2);
		return group(ss1);
	}

	private Set<SymbolicState> flowBranch(IBlock blk, Set<SymbolicState> ss, boolean value) {
		Set<SymbolicState> ret = new HashSet<SymbolicState>();
		for (SymbolicState s : ss) {
			SymbolicState s0 = transferBranch(blk, s, value);
			if (!s0.getExecutionState().isBottom()) {
				ret.add(s0);
			}
		}
		return group(ret);
	}

	private Set<SymbolicState> flowOther(IBlock blk, Set<SymbolicState> ss) {
		Set<SymbolicState> ret = new HashSet<SymbolicState>();
		for (SymbolicState s : ss) {
			SymbolicState s0 = transferOther(blk, s);
			ret.add(s0);
		}
		return group(ret);
	}

	private Set<SymbolicState> group(Set<SymbolicState> ss) {
		// FIXME Fully Path Sensitive
		return ss;
	}

	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
			
			// Modify execution state according to branch condition
			// *N.B.* content for condition IBlock is condition expression itself
			ret.getExecutionState().addClause(new ExecutionStateClause(node, value)); 
		}
		
		return ret;
	}

	private SymbolicState transferOther(IBlock blk, SymbolicState s) {
		IASTNode node = blk.getContent();		
		
		if (node != null) {
			// Process property state transition
			Set<PropertyState> oldStates = s.getPropertyStates();
			Set<PropertyState> newStates = new HashSet<PropertyState>();
			for (PropertyState state : oldStates) {
				newStates.add(state.transition(node));
			}
			s.setPropertyStates(newStates);
			
			// Modify execution state according to variable assignments
			node.accept(new VariableAssignmentVisitor(s.getExecutionState()));
		}
		return s;
	}

	private void add(IControlFlowEdge edge,
			Set<SymbolicState> ss) {
		if (!edgeInfo.get(edge).equals(ss)) {
			edgeInfo.put(edge, ss);
			
			// No duplicates
			IBlock next = edge.getTo();
			if (!worklist.contains(next)) {
				worklist.add(next);
			}
		}
	}
	
	private void initFSM() {
		uninit = new PropertyState("$u") {			
			@Override
			public PropertyState transition(IASTNode node) {
				PropertyState dest = uninit;
				if (containsOpen(node)) {
					dest = opened;
				}
				else if (containsClose(node)) {
					dest = error;
					errorNode = node;
				}
				return dest;
			}
		};
		
		opened = new PropertyState("o") {			
			@Override
			public PropertyState transition(IASTNode node) {
				PropertyState dest = opened;
				if (containsOpen(node)) {
					dest = error;
					errorNode = node;
				}
				if (containsClose(node)) {
					dest = uninit;
				}
				return dest;
			}
		};
		
		error = new PropertyState("$e") {
			
			@Override
			public PropertyState transition(IASTNode node) {
				return error;
			}
		};
	}

	protected boolean containsOpen(IASTNode node) {
		// TODO Examine more than just name
		FunctionNameParser parser = new FunctionNameParser(node, OPEN);
		return parser.matches();
	}

	protected boolean containsClose(IASTNode node) {
		// TODO Examine more than just name
		FunctionNameParser parser = new FunctionNameParser(node, CLOSE);
		return parser.matches();
	}

	private boolean isBranch(IBlock blk) {
		return blk.getOutEdges().length > 1;
	}

	private boolean isMerge(IBlock blk) {
		return blk.getInEdges().length > 1;
	}

	private void reportProblem(IASTNode node, ExecutionState condition) {
		String message = MessageFormat.format("Improper use of open/close given {0}.", condition);
		reportProblem(ERR_ID, node, message);
	}
}