diff options
Diffstat (limited to 'org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java')
-rw-r--r-- | org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java | 74 |
1 files changed, 61 insertions, 13 deletions
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 index ba9199f..80e393f 100644 --- 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 @@ -21,6 +21,7 @@ import java.util.Map.Entry; import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression; import org.eclipse.cdt.core.dom.ast.IASTExpression; +import org.eclipse.cdt.core.dom.ast.IASTFileLocation; import org.eclipse.cdt.core.dom.ast.IASTIdExpression; import org.eclipse.cdt.core.dom.ast.IASTLiteralExpression; import org.eclipse.cdt.core.dom.ast.IASTName; @@ -39,12 +40,25 @@ public class PropertySimulator { private IControlFlowGraph cfg; private IPropertyFSM fsm; + //XXX + private Map<IBlock, Integer> exploreCount; public PropertySimulator(IControlFlowGraph cfg, IPropertyFSM fsm) { this.cfg = cfg; this.fsm = fsm; worklist = new LinkedList<IBlock>(); edgeInfo = new HashMap<IControlFlowEdge, Set<SymbolicState>>(); + exploreCount = new HashMap<IBlock, Integer>(); + for (IBlock blk : cfg.getBlocks()) { + exploreCount.put(blk, 0); + } solve(); + for (Entry<IBlock, Integer> entry : exploreCount.entrySet()) { + if (entry.getValue().equals(0)) { + IBlock blk = entry.getKey(); + System.out.println("Unprocessed block " + blk.getID() + ": "); + blk.print(); + } + } } private void solve() { @@ -63,17 +77,26 @@ public class PropertySimulator { worklist.add(entryEdge.getTo()); // XXX Debug - printStates(entryEdge, symStates); + System.out.println(printStates(entryEdge, symStates)); while (!worklist.isEmpty()) { IBlock blk = worklist.remove(); + if (!blk.equals(cfg.getEntry()) && !blk.equals(cfg.getExit())) { + Integer count = exploreCount.get(blk); + exploreCount.put(blk, ++count); + } + 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)); + // Don't process the null exit block + if (!blk.equals(cfg.getExit())) { + 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 @@ -102,7 +125,26 @@ public class PropertySimulator { } } } - + + private void add(IControlFlowEdge edge, + Set<SymbolicState> ss) { + //XXX +// IBlock from = edge.getFrom(); +// if (from.getContent() != null +// && from.getContent().getRawSignature().contains("nextarg (\">\")") +// && edgeInfo.get(edge).size() > 0) { +// System.out.println(printStates(edge, ss)); +// SymbolicState oldInfo = edgeInfo.get(edge).iterator().next(); +// SymbolicState newInfo = ss.iterator().next(); +// System.out.println("equals: " + oldInfo.equals(newInfo)); +// System.out.println("hashCode: " + (oldInfo.hashCode() == newInfo.hashCode())); +// } + if (!edgeInfo.get(edge).equals(ss)) { + edgeInfo.put(edge, ss); + worklist.add(edge.getTo()); + } + } + public Set<SymbolicState> getEndStates() { IControlFlowEdge exitEdge = cfg.getExit().getInEdges()[0]; return edgeInfo.get(exitEdge); @@ -112,6 +154,20 @@ public class PropertySimulator { StringBuffer buf = new StringBuffer(); IASTNode from = edge.getFrom().getContent(); IASTNode to = edge.getTo().getContent(); + if (from != null) { + IASTFileLocation loc = from.getFileLocation(); + if (loc != null) { + int start = loc.getStartingLineNumber(); + int end = loc.getEndingLineNumber(); + if (start != end) { + buf.append("lines " + start + " - " + end); + } + else { + buf.append("line " + start); + } + buf.append(" "); + } + } buf.append("{"); buf.append(from == null ? from : from.getRawSignature()); buf.append(" -> "); @@ -332,14 +388,6 @@ public class PropertySimulator { 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; } |