diff options
Diffstat (limited to 'org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java')
| -rw-r--r-- | org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java | 166 |
1 files changed, 146 insertions, 20 deletions
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java index 04348ab..a38ef13 100644 --- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java @@ -27,9 +27,17 @@ 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.IASTBinaryExpression; +import org.eclipse.cdt.core.dom.ast.IASTExpression; +import org.eclipse.cdt.core.dom.ast.IASTIdExpression; +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.IASTStatement; import org.eclipse.cdt.core.dom.ast.IASTTranslationUnit; +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.core.resources.IProject; import org.eclipse.core.resources.IResource; import org.eclipse.core.resources.IWorkspaceRoot; @@ -81,19 +89,22 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { 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(); + // Create control flow graph for each function + for (ICallGraphNode node : cg.getAllNodes()) { + IASTStatement fnBody = node.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()); + // Search for error states using property simulation algorithm + solve(cfg); + + // Check if the exit edge of the CFG contains an error state + IControlFlowEdge exitEdge = cfg.getExit().getInEdges()[0]; + for (SymbolicState s : edgeInfo.get(exitEdge)) { + if (s.getPropertyStates().contains(error)) { + // Report problem + reportProblem(errorNode, s.getExecutionState()); + } } } } @@ -112,9 +123,7 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { 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)); + symStates.add(new SymbolicState(propStates, new ExecutionState())); worklist.add(entryEdge.getTo()); // XXX Debug @@ -199,20 +208,99 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { } private Set<SymbolicState> group(Set<SymbolicState> ss) { - // FIXME Fully Path Sensitive + return groupPSA(ss); + } + + private Set<SymbolicState> groupPSA(Set<SymbolicState> ss) { return ss; } + + private Set<SymbolicState> groupPropSim(Set<SymbolicState> ss) { + Set<SymbolicState> ret = new HashSet<SymbolicState>(); + + // Group SymbolicStates by PropertyState + Map<PropertyState, Set<ExecutionState>> statesPerProperty = new HashMap<PropertyState, Set<ExecutionState>>(); + for (SymbolicState s : ss) { + for (PropertyState ps : s.getPropertyStates()) { + if (!statesPerProperty.containsKey(ps)) { + statesPerProperty.put(ps, new HashSet<ExecutionState>()); + } + Set<ExecutionState> states = statesPerProperty.get(ps); + states.add(s.getExecutionState()); + } + } + + // Iterate through result and create SymbolicStates per PropertyState with ExecutionStates joined + for (PropertyState p : statesPerProperty.keySet()) { + Set<PropertyState> ps = new HashSet<PropertyState>(); + ps.add(p); + ExecutionState es = new ExecutionState(); + for (ExecutionState e : statesPerProperty.get(p)) { + es.join(e); + } + SymbolicState s = new SymbolicState(ps, es); + ret.add(s); + } + + return ret; + } 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 - + if (node != null) { // Modify execution state according to branch condition + ExecutionStateClause clause = null; // *N.B.* content for condition IBlock is condition expression itself - ret.getExecutionState().addClause(new ExecutionStateClause(node, value)); + if (node instanceof IASTBinaryExpression) { + // FIXME compound conditionals + IASTBinaryExpression binExpr = (IASTBinaryExpression) node; + int op = binExpr.getOperator(); + + // FIXME other ops + // Check operator is an equality operator + if (op == IASTBinaryExpression.op_equals) { // if (x == 0) + IASTExpression o1 = binExpr.getOperand1(); + if (o1 instanceof IASTIdExpression) { + IASTName name = ((IASTIdExpression) o1).getName(); + clause = parseConditional(clause, name, binExpr.getOperand2(), value); + } + } + else if (op == IASTBinaryExpression.op_notequals) { // if (x != 0) + IASTExpression o1 = binExpr.getOperand1(); + if (o1 instanceof IASTIdExpression) { + IASTName name = ((IASTIdExpression) o1).getName(); + clause = parseConditional(clause, name, binExpr.getOperand2(), !value); // Negation + } + } + } + else if (node instanceof IASTUnaryExpression) { // if (!x) + IASTUnaryExpression uExpr = (IASTUnaryExpression) node; + int op = uExpr.getOperator(); + + // Check operator is a negation operator + if (op == IASTUnaryExpression.op_not) { + IASTExpression operand = uExpr.getOperand(); + if (operand instanceof IASTIdExpression) { + IASTName name = ((IASTIdExpression) operand).getName(); + clause = parseConditional(clause, name, !value); // Negation + } + } + } + else if (node instanceof IASTIdExpression) { // if (x) + IASTName name = ((IASTIdExpression) node).getName(); + clause = parseConditional(clause, name, value); + } + + if (clause != null) { + ret.getExecutionState().addClause(clause); + // TODO Theorem Prover goes here! / Determine if branch is feasible + ret.getExecutionState().bindTruthAssignments(); + } + else { + // FIXME Handle unresolvable case + } } return ret; @@ -313,4 +401,42 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { String message = MessageFormat.format("Improper use of open/close given {0}.", condition); reportProblem(ERR_ID, node, message); } + + // FIXME REFACTOR + private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, IASTExpression valueExpr, boolean branchTruth) { + IBinding binding = name.resolveBinding(); + if (binding instanceof IVariable) { + IVariable var = (IVariable) binding; + Boolean truth = getTruthValue(valueExpr); + if (truth != null) { + clause = new ExecutionStateClause(var, truth == branchTruth); + } + } + return clause; + } + + private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, boolean branchTruth) { + IBinding binding = name.resolveBinding(); + if (binding instanceof IVariable) { + IVariable var = (IVariable) binding; + clause = new ExecutionStateClause(var, branchTruth); + } + return clause; + } + + private Boolean getTruthValue(IASTExpression valueExpr) { + Boolean result = null; + // Handle assignment from literals + if (valueExpr instanceof IASTLiteralExpression) { + int kind = ((IASTLiteralExpression) valueExpr).getKind(); + String value = String.valueOf(((IASTLiteralExpression) valueExpr).getValue()); + switch (kind) { + case IASTLiteralExpression.lk_integer_constant: + // 0 = False, > 0 = True + result = !value.equals("0"); + } + } + // TODO other variable assignments + return result; + } } |