From 8c3cd18a05d15f3c9b13ec87250decd318665f0e Mon Sep 17 00:00:00 2001 From: Elliott Baron Date: Sun, 25 Oct 2009 19:19:48 -0400 Subject: PSA working for simple variable assignments and conditionals. PropSim implemented, but needs proper join op. * org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java: Store/bind truth assignments. * org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionStateClause.java: Use IVariable as atom. * org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java: Modified for truth assignments. * org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/VariableAssignmentVisitor.java: Determine truth value from assignment statement. * org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java: Analyze every function; parse conditional expressions and determine feasible branches; PropSim grouping method (not used ATM). --- .../cdt/codan/extension/ExecutionState.java | 89 +++++++++-- .../cdt/codan/extension/ExecutionStateClause.java | 38 +++-- .../eclipse/cdt/codan/extension/SymbolicState.java | 7 + .../codan/extension/VariableAssignmentVisitor.java | 48 +++++- .../checkers/CloseOpenedFilesChecker.java | 166 ++++++++++++++++++--- 5 files changed, 300 insertions(+), 48 deletions(-) (limited to 'org.eclipse.cdt.codan.extension') diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java index 6f4f496..208f9f0 100644 --- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java @@ -11,29 +11,89 @@ package org.eclipse.cdt.codan.extension; import java.util.ArrayList; +import java.util.HashMap; import java.util.List; +import java.util.Map; + +import org.eclipse.cdt.core.dom.ast.IVariable; public class ExecutionState { private List clauses; + private Map truthAssignments; private boolean top; private boolean bottom; public ExecutionState() { + truthAssignments = new HashMap(); clauses = new ArrayList(); + top = true; + bottom = false; } - public void addClause(ExecutionStateClause node) { - setTop(false); - setBottom(false); - clauses.add(node); + public void addClause(ExecutionStateClause clause) { + // Cannot get out of bottom, do not add duplicate clauses + if (!bottom && !clauses.contains(clause)) { + top = false; // T AND x = x + if (clauses.contains(clause.getNegation())) { + clauses.clear(); + bottom = true; // x AND NOT x = F + } + else { + clauses.add(clause); + } + } } public void removeClause(ExecutionStateClause node) { clauses.remove(node); if (clauses.size() == 0) { - setTop(true); - setBottom(false); + setTop(); + } + } + + public void addTruthAssignment(IVariable var, boolean value) { + truthAssignments.put(var, value); + } + + public Map getTruthAssignments() { + return truthAssignments; + } + + public void setTruthAssignments(Map truthAssignments) { + this.truthAssignments = truthAssignments; + } + + public void bindTruthAssignments() { + boolean unsatisfiable = false; + List clausesCopy = new ArrayList(clauses); + for (ExecutionStateClause c : clausesCopy) { + Boolean truth = truthAssignments.get(c.getVariable()); + if (truth != null) { + if (truth == c.isTrue()) { // does truth value of clause match truth assignment? + removeClause(c); + } + else { + unsatisfiable = true; + } + } + } + + if (unsatisfiable) { + setBottom(); + } + } + + //FIXME + public ExecutionState join(ExecutionState other) { + // Add clauses from other, canceling out negating clauses + for (ExecutionStateClause clause : other.getClauses()) { + ExecutionStateClause negation = clause.getNegation(); + if (clauses.contains(negation)) { + removeClause(negation); + other.removeClause(clause); + } } + return this; } public ExecutionStateClause[] getClauses() { @@ -48,12 +108,16 @@ public class ExecutionState { return bottom; } - public void setTop(boolean top) { - this.top = top; + public void setTop() { + top = true; + bottom = false; + clauses.clear(); } - public void setBottom(boolean bottom) { - this.bottom = bottom; + public void setBottom() { + bottom = true; + top = false; + clauses.clear(); } @Override @@ -69,10 +133,7 @@ public class ExecutionState { StringBuffer buf = new StringBuffer(); if (clauses.size() > 0) { for (ExecutionStateClause c : clauses) { - if (!c.isTrue()) { - buf.append("NOT "); - } - buf.append(c.getNode().getRawSignature()); + buf.append(c); buf.append(" AND "); } buf.delete(buf.length() - 5 /* " AND ".length() */, buf.length()); diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionStateClause.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionStateClause.java index adb4e62..ab44d93 100644 --- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionStateClause.java +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionStateClause.java @@ -10,37 +10,55 @@ *******************************************************************************/ package org.eclipse.cdt.codan.extension; -import org.eclipse.cdt.core.dom.ast.IASTNode; +import org.eclipse.cdt.core.dom.ast.IVariable; public class ExecutionStateClause { - private IASTNode node; - private boolean truthValue; + protected IVariable var; + protected boolean truthValue; - public ExecutionStateClause(IASTNode node) { - this(node, true); + public ExecutionStateClause(IVariable var) { + this(var, true); } - public ExecutionStateClause(IASTNode node, boolean truthValue) { - this.node = node; + public ExecutionStateClause(IVariable var, boolean truthValue) { + this.var = var; this.truthValue = truthValue; } - public IASTNode getNode() { - return node; + public IVariable getVariable() { + return var; } public boolean isTrue() { return truthValue; } + public ExecutionStateClause getNegation() { + return new ExecutionStateClause(var, !truthValue); + } + + @Override + public boolean equals(Object obj) { + if (obj instanceof ExecutionStateClause) { + ExecutionStateClause other = (ExecutionStateClause) obj; + return var.equals(other.getVariable()) && truthValue == other.isTrue(); + } + return false; + } + + @Override + public int hashCode() { + return var.hashCode() + (truthValue ? 1 : 0); + } + @Override public String toString() { StringBuffer buf = new StringBuffer(); if (!truthValue) { buf.append("NOT "); } - buf.append(node.getRawSignature()); + buf.append(var.getName()); return buf.toString(); } diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java index ad932ac..93bf3be 100644 --- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java @@ -11,9 +11,13 @@ package org.eclipse.cdt.codan.extension; import java.util.Collections; +import java.util.HashMap; import java.util.HashSet; +import java.util.Map; import java.util.Set; +import org.eclipse.cdt.core.dom.ast.IVariable; + public class SymbolicState { private Set propertyStates; private ExecutionState executionState; @@ -45,6 +49,9 @@ public class SymbolicState { for (ExecutionStateClause cl : executionState.getClauses()) { es.addClause(cl); } + Map truthAssignments = new HashMap(executionState.getTruthAssignments()); + es.setTruthAssignments(truthAssignments); + return new SymbolicState(ps, es); } 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 ebe4ce4..2530210 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 @@ -4,8 +4,14 @@ import org.eclipse.cdt.core.dom.ast.ASTVisitor; import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression; 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.IBinding; +import org.eclipse.cdt.core.dom.ast.IVariable; /******************************************************************************* * Copyright (c) 2009 Elliott Baron @@ -31,7 +37,11 @@ public class VariableAssignmentVisitor extends ASTVisitor { public int visit(IASTInitializer initializer) { IASTNode parent = initializer.getParent(); if (parent instanceof IASTDeclarator) { - es.addClause(new ExecutionStateClause(parent)); + if (initializer instanceof IASTInitializerExpression) { + IASTDeclarator decl = (IASTDeclarator) parent; + IASTExpression expr = ((IASTInitializerExpression) initializer).getExpression(); + parseAssignment(parent, decl.getName(), expr); + } return PROCESS_SKIP; } return PROCESS_CONTINUE; @@ -44,13 +54,43 @@ public class VariableAssignmentVisitor extends ASTVisitor { int op = binExpr.getOperator(); // Check operator is an assignment operator - if (op >= IASTBinaryExpression.op_assign - && op <= IASTBinaryExpression.op_binaryOrAssign) { - es.addClause(new ExecutionStateClause(binExpr)); + if (op == IASTBinaryExpression.op_assign) { // FIXME other ops + IASTExpression o1 = binExpr.getOperand1(); + if (o1 instanceof IASTIdExpression) { + IASTName name = ((IASTIdExpression) o1).getName(); + parseAssignment(binExpr, name, binExpr.getOperand2()); + } return PROCESS_SKIP; } } return PROCESS_CONTINUE; } + private void parseAssignment(IASTNode parent, IASTName name, IASTExpression valueExpr) { + IBinding binding = name.resolveBinding(); + if (binding instanceof IVariable) { + IVariable var = (IVariable) binding; + Boolean truth = getTruthValue(valueExpr); + if (truth != null) { + es.addTruthAssignment(var, truth); + } + } + } + + 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; + } + } 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 symStates = edgeInfo.get(entryEdge); Set propStates = new HashSet(); 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 group(Set ss) { - // FIXME Fully Path Sensitive + return groupPSA(ss); + } + + private Set groupPSA(Set ss) { return ss; } + + private Set groupPropSim(Set ss) { + Set ret = new HashSet(); + + // Group SymbolicStates by PropertyState + Map> statesPerProperty = new HashMap>(); + for (SymbolicState s : ss) { + for (PropertyState ps : s.getPropertyStates()) { + if (!statesPerProperty.containsKey(ps)) { + statesPerProperty.put(ps, new HashSet()); + } + Set 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 ps = new HashSet(); + 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; + } } -- cgit