From 35199099d32443f7e6c35fe93d29442fcea6078a Mon Sep 17 00:00:00 2001 From: Elliott Baron Date: Mon, 9 Nov 2009 21:12:05 -0500 Subject: Remove truth assignments at merge points, based on dominance in CFG. * org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java: Change to truth assignments map. * org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java: Likewise. * org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java: Remove truth assigments in flowMerge(). * org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java: New file. * org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/VariableAssignmentVisitor.java: Store IBlock corresponding to TA. --- .../cdt/codan/extension/ExecutionState.java | 30 +++++++++++--------- .../cdt/codan/extension/PropertySimulator.java | 33 ++++++++++++++++++++-- .../eclipse/cdt/codan/extension/SymbolicState.java | 2 +- .../cdt/codan/extension/TruthAssignment.java | 22 +++++++++++++++ .../codan/extension/VariableAssignmentVisitor.java | 8 ++++-- 5 files changed, 75 insertions(+), 20 deletions(-) create mode 100644 org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java 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 fd8032a..3ea27b6 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 @@ -16,15 +16,16 @@ import java.util.Map; import java.util.Set; import org.eclipse.cdt.core.dom.ast.IVariable; +import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IBlock; public class ExecutionState { private Set clauses; - private Map truthAssignments; // FIXME this should be more robust, use SSA + private Map truthAssignments; // FIXME this should be more robust, use SSA private boolean top; private boolean bottom; public ExecutionState() { - truthAssignments = new HashMap(); + truthAssignments = new HashMap(); clauses = new HashSet(); top = true; bottom = false; @@ -50,15 +51,15 @@ public class ExecutionState { } } - public void addTruthAssignment(IVariable var, boolean value) { - truthAssignments.put(var, value); + public void addTruthAssignment(IVariable var, boolean value, IBlock blk) { + truthAssignments.put(var, new TruthAssignment(blk, value)); } - public Map getTruthAssignments() { + public Map getTruthAssignments() { return truthAssignments; } - public void setTruthAssignments(Map truthAssignments) { + public void setTruthAssignments(Map truthAssignments) { this.truthAssignments = truthAssignments; } @@ -67,13 +68,16 @@ public class ExecutionState { Set clausesCopy = new HashSet( 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; + TruthAssignment ta = truthAssignments.get(c.getVariable()); + if (ta != null) { + Boolean truth = ta.getValue(); + if (truth != null) { + if (truth == c.isTrue()) { // does truth value of clause match + // truth assignment? + removeClause(c); + } else { + unsatisfiable = true; + } } } } 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 ffd3ada..ba9199f 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 @@ -13,9 +13,11 @@ package org.eclipse.cdt.codan.extension; import java.util.HashMap; import java.util.HashSet; import java.util.LinkedList; +import java.util.List; import java.util.Map; import java.util.Queue; import java.util.Set; +import java.util.Map.Entry; import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression; import org.eclipse.cdt.core.dom.ast.IASTExpression; @@ -122,11 +124,36 @@ public class PropertySimulator { private Set flowMerge(IBlock blk, Set ss1, Set ss2) { Set ret = new HashSet(); - ret.addAll(ss1); - ret.addAll(ss2); + ret.addAll(filterTruthAssignments(blk, ss1)); + ret.addAll(filterTruthAssignments(blk, ss2)); return group(ret); } + private Set filterTruthAssignments(IBlock blk, Set ss) { + Set ret = new HashSet(ss.size()); + for (SymbolicState s : ss) { + SymbolicState copy = s.copy(); + Set toRemove = new HashSet(); + Map truthAssignments = copy.getExecutionState().getTruthAssignments(); + for (Entry ta : truthAssignments.entrySet()) { + // FIXME could be better + // Remove truth assignments that were added by a block that doesn't dominate this one + List dominators = blk.getDOM(); + IBlock origin = ta.getValue().getOrigin(); + if (!dominators.contains(origin)) { + // Schedule removal + toRemove.add(ta.getKey()); + } + } + // Actually remove + for (IVariable var : toRemove) { + truthAssignments.remove(var); + } + ret.add(copy); + } + return ret; + } + private Set flowBranch(IBlock blk, Set ss, boolean value) { Set ret = new HashSet(); for (SymbolicState s : ss) { @@ -300,7 +327,7 @@ public class PropertySimulator { s.setPropertyStates(newStates); // Modify execution state according to variable assignments - node.accept(new VariableAssignmentVisitor(s.getExecutionState())); + node.accept(new VariableAssignmentVisitor(blk, s.getExecutionState())); } return s; } 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 76db5ea..db551aa 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 @@ -49,7 +49,7 @@ public class SymbolicState { public SymbolicState copy() { Set ps = new HashSet(propertyStates); ExecutionState es = executionState.copy(); - Map truthAssignments = new HashMap(executionState.getTruthAssignments()); + Map truthAssignments = new HashMap(executionState.getTruthAssignments()); es.setTruthAssignments(truthAssignments); SymbolicState ret = new SymbolicState(ps, es); diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java new file mode 100644 index 0000000..a9c50dc --- /dev/null +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java @@ -0,0 +1,22 @@ +package org.eclipse.cdt.codan.extension; + +import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IBlock; + +public class TruthAssignment { + private IBlock blk; + private Boolean value; + + public TruthAssignment(IBlock blk, Boolean value) { + this.blk = blk; + this.value = value; + } + + public IBlock getOrigin() { + return blk; + } + + public Boolean getValue() { + return value; + } + +} 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 2530210..c167129 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 @@ -12,6 +12,7 @@ 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; +import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IBlock; /******************************************************************************* * Copyright (c) 2009 Elliott Baron @@ -24,10 +25,11 @@ import org.eclipse.cdt.core.dom.ast.IVariable; * Elliott Baron - initial API and implementation *******************************************************************************/ public class VariableAssignmentVisitor extends ASTVisitor { - + private IBlock blk; private ExecutionState es; - public VariableAssignmentVisitor(ExecutionState es) { + public VariableAssignmentVisitor(IBlock blk, ExecutionState es) { + this.blk = blk; this.es = es; shouldVisitInitializers = true; shouldVisitExpressions = true; @@ -72,7 +74,7 @@ public class VariableAssignmentVisitor extends ASTVisitor { IVariable var = (IVariable) binding; Boolean truth = getTruthValue(valueExpr); if (truth != null) { - es.addTruthAssignment(var, truth); + es.addTruthAssignment(var, truth, blk); } } } -- cgit