diff options
author | Elliott Baron <ebaron@fedoraproject.org> | 2009-11-09 21:12:05 -0500 |
---|---|---|
committer | Elliott Baron <ebaron@fedoraproject.org> | 2009-11-09 21:12:05 -0500 |
commit | 35199099d32443f7e6c35fe93d29442fcea6078a (patch) | |
tree | b1286b49519977b8e9983793c8d5ab990f242789 | |
parent | 4e991b89471d65f4f02e1ad54f2b85759ad80586 (diff) | |
download | codan-35199099d32443f7e6c35fe93d29442fcea6078a.tar.gz codan-35199099d32443f7e6c35fe93d29442fcea6078a.tar.xz codan-35199099d32443f7e6c35fe93d29442fcea6078a.zip |
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.
5 files changed, 75 insertions, 20 deletions
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<ExecutionStateClause> clauses; - private Map<IVariable, Boolean> truthAssignments; // FIXME this should be more robust, use SSA + private Map<IVariable, TruthAssignment> truthAssignments; // FIXME this should be more robust, use SSA private boolean top; private boolean bottom; public ExecutionState() { - truthAssignments = new HashMap<IVariable, Boolean>(); + truthAssignments = new HashMap<IVariable, TruthAssignment>(); clauses = new HashSet<ExecutionStateClause>(); 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<IVariable, Boolean> getTruthAssignments() { + public Map<IVariable, TruthAssignment> getTruthAssignments() { return truthAssignments; } - public void setTruthAssignments(Map<IVariable, Boolean> truthAssignments) { + public void setTruthAssignments(Map<IVariable, TruthAssignment> truthAssignments) { this.truthAssignments = truthAssignments; } @@ -67,13 +68,16 @@ public class ExecutionState { Set<ExecutionStateClause> clausesCopy = new HashSet<ExecutionStateClause>( 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<SymbolicState> flowMerge(IBlock blk, Set<SymbolicState> ss1, Set<SymbolicState> ss2) { Set<SymbolicState> ret = new HashSet<SymbolicState>(); - ret.addAll(ss1); - ret.addAll(ss2); + ret.addAll(filterTruthAssignments(blk, ss1)); + ret.addAll(filterTruthAssignments(blk, ss2)); return group(ret); } + private Set<SymbolicState> filterTruthAssignments(IBlock blk, Set<SymbolicState> ss) { + Set<SymbolicState> ret = new HashSet<SymbolicState>(ss.size()); + for (SymbolicState s : ss) { + SymbolicState copy = s.copy(); + Set<IVariable> toRemove = new HashSet<IVariable>(); + Map<IVariable, TruthAssignment> truthAssignments = copy.getExecutionState().getTruthAssignments(); + for (Entry<IVariable, TruthAssignment> ta : truthAssignments.entrySet()) { + // FIXME could be better + // Remove truth assignments that were added by a block that doesn't dominate this one + List<IBlock> 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<SymbolicState> flowBranch(IBlock blk, Set<SymbolicState> ss, boolean value) { Set<SymbolicState> ret = new HashSet<SymbolicState>(); 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<PropertyState> ps = new HashSet<PropertyState>(propertyStates); ExecutionState es = executionState.copy(); - Map<IVariable, Boolean> truthAssignments = new HashMap<IVariable, Boolean>(executionState.getTruthAssignments()); + Map<IVariable, TruthAssignment> truthAssignments = new HashMap<IVariable, TruthAssignment>(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); } } } |