diff options
Diffstat (limited to 'org.eclipse.cdt.codan.extension/src/org/eclipse')
8 files changed, 477 insertions, 324 deletions
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java index 3b62b87..9e3ed5f 100644 --- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java @@ -10,17 +10,21 @@ *******************************************************************************/ package org.eclipse.cdt.codan.extension; +import java.util.HashMap; import java.util.HashSet; import java.util.List; +import java.util.Map; import java.util.Set; import org.eclipse.cdt.codan.extension.Minterm.Value; import org.eclipse.cdt.core.dom.ast.IVariable; public class ESSimplifier extends QuineMcCluskeySimplifier<IVariable> { + private Map<ExecutionState, Minterm<IVariable>> esMapping; - public ESSimplifier(ITruthTable<IVariable> tt) { + public ESSimplifier(ESTruthTable tt) { super(tt); + esMapping = new HashMap<ExecutionState, Minterm<IVariable>>(); } public Set<ExecutionState> getExecutionStateCover() { @@ -28,7 +32,7 @@ public class ESSimplifier extends QuineMcCluskeySimplifier<IVariable> { List<Minterm<IVariable>> implicantCover = getImplicantCover(); for (Minterm<IVariable> term : implicantCover) { ExecutionState es = new ExecutionState(); - for (IVariable var : variables) { + for (IVariable var : truthTable.getVariables()) { Value val = term.getValue(var); if (val == Value.TRUE) { es.addClause(new ExecutionStateClause(var, true)); @@ -38,6 +42,24 @@ public class ESSimplifier extends QuineMcCluskeySimplifier<IVariable> { } // Don't care about Don't cares } + // Add truth assignments from implied minterms + List<Minterm<IVariable>> implied = getImplications(term); + for (Minterm<IVariable> minterm : implied) { + ExecutionState e = ((ESTruthTable) truthTable).getExecutionState(minterm); + es.getTruthAssignments().putAll(e.getTruthAssignments()); + } + ret.add(es); + esMapping.put(es, term); + } + return ret; + } + + public Set<ExecutionState> getImplications(ExecutionState primeImplicant) { + Set<ExecutionState> ret = new HashSet<ExecutionState>(); + Minterm<IVariable> piTerm = esMapping.get(primeImplicant); + List<Minterm<IVariable>> impls = getImplications(piTerm); + for (Minterm<IVariable> term : impls) { + ExecutionState es = ((ESTruthTable) truthTable).getExecutionState(term); ret.add(es); } return ret; @@ -46,13 +68,13 @@ public class ESSimplifier extends QuineMcCluskeySimplifier<IVariable> { @Override public String toString() { StringBuffer buf = new StringBuffer(); - for (IVariable var : variables) { + for (IVariable var : truthTable.getVariables()) { buf.append(var.getName()); buf.append(" "); } buf.append("\n"); - for (Minterm<IVariable> term : minterms) { - for (IVariable var : variables) { + for (Minterm<IVariable> term : truthTable.getMinterms()) { + for (IVariable var : truthTable.getVariables()) { switch (term.getValue(var)) { case TRUE: buf.append("1"); diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java index 94e7574..1835015 100644 --- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java @@ -22,11 +22,13 @@ import org.eclipse.cdt.core.dom.ast.IVariable; public class ESTruthTable implements ITruthTable<IVariable> { private List<Minterm<IVariable>> minterms; + private Map<Minterm<IVariable>, ExecutionState> esMapping; private List<IVariable> variables; public ESTruthTable(Set<ExecutionState> es) { minterms = new ArrayList<Minterm<IVariable>>(); variables = new ArrayList<IVariable>(); + esMapping = new HashMap<Minterm<IVariable>, ExecutionState>(); for (ExecutionState e : es) { for (ExecutionStateClause c : e.getClauses()) { @@ -54,6 +56,7 @@ public class ESTruthTable implements ITruthTable<IVariable> { for (ExecutionStateClause c : e.getClauses()) { term.setValue(c.getVariable(), c.isTrue() ? Value.TRUE : Value.FALSE); } + esMapping.put(term, e); } } @@ -65,6 +68,10 @@ public class ESTruthTable implements ITruthTable<IVariable> { return variables; } + public ExecutionState getExecutionState(Minterm<IVariable> minterm) { + return esMapping.get(minterm); + } + @Override public String toString() { StringBuffer buf = new StringBuffer(); 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 c19970e..fd8032a 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 @@ -19,7 +19,7 @@ import org.eclipse.cdt.core.dom.ast.IVariable; public class ExecutionState { private Set<ExecutionStateClause> clauses; - private Map<IVariable, Boolean> truthAssignments; + private Map<IVariable, Boolean> truthAssignments; // FIXME this should be more robust, use SSA private boolean top; private boolean bottom; @@ -83,12 +83,6 @@ public class ExecutionState { } } - public static Set<ExecutionState> join(Set<ExecutionState> es) { - ESTruthTable tt = new ESTruthTable(es); - ESSimplifier simp = new ESSimplifier(tt); - return simp.getExecutionStateCover(); - } - public Set<ExecutionStateClause> getClauses() { return clauses; } diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/IPropertyFSM.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/IPropertyFSM.java new file mode 100644 index 0000000..a8ace1e --- /dev/null +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/IPropertyFSM.java @@ -0,0 +1,23 @@ +/******************************************************************************* + * 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 java.util.Set; + +public interface IPropertyFSM { + + public Set<PropertyState> getPropertyStates(); + + public PropertyState getUninitState(); + + public PropertyState getErrorState(); + +} 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 new file mode 100644 index 0000000..ffd3ada --- /dev/null +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java @@ -0,0 +1,361 @@ +/******************************************************************************* + * 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 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.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.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; +import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowEdge; +import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowGraph; + +public class PropertySimulator { + // Property simulation state info for CFG's edges + private Map<IControlFlowEdge, Set<SymbolicState>> edgeInfo; + private Queue<IBlock> worklist; + private IControlFlowGraph cfg; + private IPropertyFSM fsm; + + public PropertySimulator(IControlFlowGraph cfg, IPropertyFSM fsm) { + this.cfg = cfg; + this.fsm = fsm; + worklist = new LinkedList<IBlock>(); + edgeInfo = new HashMap<IControlFlowEdge, Set<SymbolicState>>(); + solve(); + } + + private void solve() { + 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(fsm.getUninitState()); + symStates.add(new SymbolicState(propStates, new ExecutionState())); + + 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)); + } + } + } + } + + public Set<SymbolicState> getEndStates() { + IControlFlowEdge exitEdge = cfg.getExit().getInEdges()[0]; + return edgeInfo.get(exitEdge); + } + + 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) { + Set<SymbolicState> ret = new HashSet<SymbolicState>(); + ret.addAll(ss1); + ret.addAll(ss2); + return group(ret); + } + + 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) { + return groupPropSim(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<SymbolicState>> statesPerProperty = new HashMap<PropertyState, Set<SymbolicState>>(); + for (SymbolicState s : ss) { + for (PropertyState ps : s.getPropertyStates()) { + if (!statesPerProperty.containsKey(ps)) { + statesPerProperty.put(ps, new HashSet<SymbolicState>()); + } + Set<SymbolicState> states = statesPerProperty.get(ps); + states.add(s); + } + } + + // 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); + Set<SymbolicState> ssForProperty = statesPerProperty.get(p); + Set<ExecutionState> esForProperty = new HashSet<ExecutionState>(); + for (SymbolicState s : ssForProperty) { + esForProperty.add(s.getExecutionState()); + } + if (ssForProperty.size() > 1) { + // Join execution states in this set + ESTruthTable tt = new ESTruthTable(esForProperty); + ESSimplifier simp = new ESSimplifier(tt); + esForProperty = simp.getExecutionStateCover(); + + for (ExecutionState e : esForProperty) { + SymbolicState newState = new SymbolicState(ps, e); + // Join corresponding error conditions + if (p.equals(fsm.getErrorState())) { + // Get original ExecutionStates implied by this prime implicant + Set<ExecutionState> implied = simp.getImplications(e); + // Find the appropriate SymbolicState + for (ExecutionState orig : implied) { + SymbolicState s = findSymbolicState(ssForProperty, orig); + // Add its error cause to the joined state + newState.getErrorCauses().addAll(s.getErrorCauses()); + } + } + ret.add(newState); + } + } + else { + // Nothing to do + SymbolicState s = ssForProperty.iterator().next(); + ret.add(s); + } + + } + + return ret; + } + + private SymbolicState findSymbolicState(Set<SymbolicState> ss, ExecutionState es) { + for (SymbolicState s : ss) { + if (s.getExecutionState().equals(es)) { + return s; + } + } + return null; + } + + private SymbolicState transferBranch(IBlock blk, SymbolicState s, boolean value) { + IASTNode node = blk.getContent(); + + SymbolicState ret = s.copy(); + if (node != null) { + // Modify execution state according to branch condition + ExecutionStateClause clause = null; + // *N.B.* content for condition IBlock is condition expression itself + 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; + } + + 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) { + PropertyState dest = state.transition(node); + // If we transition to from non-error to error, store the node that caused it + if (!state.equals(fsm.getErrorState()) && dest.equals(fsm.getErrorState())) { + s.getErrorCauses().add(node); + } + newStates.add(dest); + } + 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); + worklist.add(edge.getTo()); + } + } + + private boolean isBranch(IBlock blk) { + return blk.getOutEdges().length > 1; + } + + private boolean isMerge(IBlock blk) { + return blk.getInEdges().length > 1; + } + + // 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; + } +} diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java index d363028..45c41ab 100644 --- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java @@ -18,13 +18,13 @@ import java.util.Map; import java.util.Queue; public class QuineMcCluskeySimplifier<E> { - protected List<Minterm<E>> minterms; - protected List<E> variables; + protected ITruthTable<E> truthTable; protected List<Minterm<E>> implicantCover; + private Map<Minterm<E>, List<Minterm<E>>> implications; public QuineMcCluskeySimplifier(ITruthTable<E> tt) { - minterms = tt.getMinterms(); - variables = tt.getVariables(); + this.truthTable = tt; + List<Minterm<E>> minterms = tt.getMinterms(); List<Minterm<E>> inputMinterms = new ArrayList<Minterm<E>>(minterms); List<Minterm<E>> primeImplicants = new ArrayList<Minterm<E>>(minterms); @@ -56,8 +56,7 @@ public class QuineMcCluskeySimplifier<E> { } } - // Determine which prime implicants cover which original minterms - Map<Minterm<E>, List<Minterm<E>>> implications = new HashMap<Minterm<E>, List<Minterm<E>>>(); + implications = new HashMap<Minterm<E>, List<Minterm<E>>>(); for (Minterm<E> implicant : primeImplicants) { implications.put(implicant, new ArrayList<Minterm<E>>()); for (Minterm<E> minterm : inputMinterms) { @@ -110,5 +109,9 @@ public class QuineMcCluskeySimplifier<E> { public List<Minterm<E>> getImplicantCover() { return implicantCover; } + + public List<Minterm<E>> getImplications(Minterm<E> primeImplicant) { + return implications.get(primeImplicant); + } } 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 19dd6b3..76db5ea 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 @@ -16,15 +16,18 @@ import java.util.HashSet; import java.util.Map; import java.util.Set; +import org.eclipse.cdt.core.dom.ast.IASTNode; import org.eclipse.cdt.core.dom.ast.IVariable; public class SymbolicState { private Set<PropertyState> propertyStates; private ExecutionState executionState; + private Set<IASTNode> errorCauses; public SymbolicState(Set<PropertyState> propertyStates, ExecutionState executionState) { this.propertyStates = propertyStates; this.executionState = executionState; + errorCauses = new HashSet<IASTNode>(); } public ExecutionState getExecutionState() { @@ -49,7 +52,13 @@ public class SymbolicState { Map<IVariable, Boolean> truthAssignments = new HashMap<IVariable, Boolean>(executionState.getTruthAssignments()); es.setTruthAssignments(truthAssignments); - return new SymbolicState(ps, es); + SymbolicState ret = new SymbolicState(ps, es); + ret.errorCauses = new HashSet<IASTNode>(errorCauses); + return ret; + } + + public Set<IASTNode> getErrorCauses() { + return errorCauses; } @Override 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 491a481..d60889a 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 @@ -13,40 +13,26 @@ 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.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.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; 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; @@ -55,23 +41,16 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { 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; + private IPropertyFSM fsm; // 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(); + fsm = initFSM(); } public void processAst(IASTTranslationUnit ast) { @@ -96,248 +75,22 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { cfg.buildCFG(); // Search for error states using property simulation algorithm - solve(cfg); + PropertySimulator sim = new PropertySimulator(cfg, fsm); // Check if the exit edge of the CFG contains an error state - IControlFlowEdge exitEdge = cfg.getExit().getInEdges()[0]; - for (SymbolicState s : edgeInfo.get(exitEdge)) { + for (SymbolicState s : sim.getEndStates()) { if (s.getPropertyStates().contains(error)) { - // Report problem - reportProblem(errorNode, s.getExecutionState()); + // Report problems + for (IASTNode errorNode : s.getErrorCauses()) { + 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); - symStates.add(new SymbolicState(propStates, new ExecutionState())); - - 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) { - Set<SymbolicState> ret = new HashSet<SymbolicState>(); - ret.addAll(ss1); - ret.addAll(ss2); - return group(ret); - } - - 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) { - return groupPropSim(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); - Set<ExecutionState> es = statesPerProperty.get(p); - if (es.size() > 1) { - // Join execution states in this set - es = ExecutionState.join(es); - } - for (ExecutionState e : es) { - SymbolicState s = new SymbolicState(ps, e); - 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) { - // Modify execution state according to branch condition - ExecutionStateClause clause = null; - // *N.B.* content for condition IBlock is condition expression itself - 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; - } - - 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); - worklist.add(edge.getTo()); - } - } - private void initFSM() { + private IPropertyFSM initFSM() { uninit = new PropertyState("$u") { @Override public PropertyState transition(IASTNode node) { @@ -347,7 +100,6 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { } else if (containsClose(node)) { dest = error; - errorNode = node; } return dest; } @@ -359,7 +111,6 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { PropertyState dest = opened; if (containsOpen(node)) { dest = error; - errorNode = node; } if (containsClose(node)) { dest = uninit; @@ -375,6 +126,28 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { return error; } }; + + return new IPropertyFSM() { + + @Override + public PropertyState getUninitState() { + return uninit; + } + + @Override + public Set<PropertyState> getPropertyStates() { + Set<PropertyState> states = new HashSet<PropertyState>(); + states.add(uninit); + states.add(opened); + states.add(error); + return states; + } + + @Override + public PropertyState getErrorState() { + return error; + } + }; } protected boolean containsOpen(IASTNode node) { @@ -387,54 +160,15 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { 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); - } - - // 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); - } + String message; + if (condition.isTop()) { + message = "Improper use of open/close."; } - 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); + else { + message = MessageFormat.format("Improper use of open/close given {0}.", condition); } - return clause; + reportProblem(ERR_ID, node, message); } - 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; - } } |