diff options
author | Elliott Baron <ebaron@fedoraproject.org> | 2009-11-01 00:02:17 -0400 |
---|---|---|
committer | Elliott Baron <ebaron@fedoraproject.org> | 2009-11-01 00:02:17 -0400 |
commit | 25eebecd10f8bfa9810e73f4efdc5b0be4a305a2 (patch) | |
tree | aefdf9c9a5a1d9b878d647a2265c2bbfccb00d03 | |
parent | f4fd87f6b05de1a67c5d2d09f1813ddce6de4879 (diff) | |
download | codan-25eebecd10f8bfa9810e73f4efdc5b0be4a305a2.tar.gz codan-25eebecd10f8bfa9810e73f4efdc5b0be4a305a2.tar.xz codan-25eebecd10f8bfa9810e73f4efdc5b0be4a305a2.zip |
Implemented Quine-McCluskey algorithm to join execution states. Property simulation working!
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java: Join execution states.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ITruthTable.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Minterm.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java: Implement equals and hashCode.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java: Use PropSim.
8 files changed, 492 insertions, 52 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 new file mode 100644 index 0000000..3b62b87 --- /dev/null +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java @@ -0,0 +1,72 @@ +/******************************************************************************* + * 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.HashSet; +import java.util.List; +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> { + + public ESSimplifier(ITruthTable<IVariable> tt) { + super(tt); + } + + public Set<ExecutionState> getExecutionStateCover() { + Set<ExecutionState> ret = new HashSet<ExecutionState>(); + List<Minterm<IVariable>> implicantCover = getImplicantCover(); + for (Minterm<IVariable> term : implicantCover) { + ExecutionState es = new ExecutionState(); + for (IVariable var : variables) { + Value val = term.getValue(var); + if (val == Value.TRUE) { + es.addClause(new ExecutionStateClause(var, true)); + } + else if (val == Value.FALSE) { + es.addClause(new ExecutionStateClause(var, false)); + } + // Don't care about Don't cares + } + ret.add(es); + } + return ret; + } + + @Override + public String toString() { + StringBuffer buf = new StringBuffer(); + for (IVariable var : variables) { + buf.append(var.getName()); + buf.append(" "); + } + buf.append("\n"); + for (Minterm<IVariable> term : minterms) { + for (IVariable var : variables) { + switch (term.getValue(var)) { + case TRUE: + buf.append("1"); + break; + case FALSE: + buf.append("0"); + break; + default: + buf.append("-"); + } + buf.append(" "); + } + buf.append("\n"); + } + return buf.toString(); + } +} 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 new file mode 100644 index 0000000..94e7574 --- /dev/null +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java @@ -0,0 +1,86 @@ +/******************************************************************************* + * 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.ArrayList; +import java.util.HashMap; +import java.util.Iterator; +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 ESTruthTable implements ITruthTable<IVariable> { + private List<Minterm<IVariable>> minterms; + private List<IVariable> variables; + + public ESTruthTable(Set<ExecutionState> es) { + minterms = new ArrayList<Minterm<IVariable>>(); + variables = new ArrayList<IVariable>(); + + for (ExecutionState e : es) { + for (ExecutionStateClause c : e.getClauses()) { + IVariable var = c.getVariable(); + if (!variables.contains(var)) { + variables.add(var); + } + } + } + + // Initialize with Don't Cares + for (int i = 0; i < es.size(); i++) { + Map<IVariable, Value> values = new HashMap<IVariable, Value>(); + for (IVariable var : variables) { + values.put(var, Value.DONTCARE); + } + minterms.add(new Minterm<IVariable>(values)); + } + + // Set actual truth values + Iterator<ExecutionState> it = es.iterator(); + for (int i = 0; i < es.size(); i++) { + Minterm<IVariable> term = minterms.get(i); + ExecutionState e = it.next(); + for (ExecutionStateClause c : e.getClauses()) { + term.setValue(c.getVariable(), c.isTrue() ? Value.TRUE : Value.FALSE); + } + } + } + + public List<Minterm<IVariable>> getMinterms() { + return minterms; + } + + public List<IVariable> getVariables() { + return variables; + } + + @Override + public String toString() { + StringBuffer buf = new StringBuffer(); + for (IVariable var : variables) { + buf.append(var.getName()); + buf.append(" "); + } + buf.append("\n"); + for (Minterm<IVariable> term : minterms) { + for (IVariable var : variables) { + buf.append(term.getValue(var)); + buf.append(" "); + } + buf.append("\n"); + } + return buf.toString(); + } + +} 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 208f9f0..c19970e 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 @@ -10,26 +10,26 @@ *******************************************************************************/ package org.eclipse.cdt.codan.extension; -import java.util.ArrayList; import java.util.HashMap; -import java.util.List; +import java.util.HashSet; import java.util.Map; +import java.util.Set; import org.eclipse.cdt.core.dom.ast.IVariable; public class ExecutionState { - private List<ExecutionStateClause> clauses; + private Set<ExecutionStateClause> clauses; private Map<IVariable, Boolean> truthAssignments; private boolean top; private boolean bottom; public ExecutionState() { truthAssignments = new HashMap<IVariable, Boolean>(); - clauses = new ArrayList<ExecutionStateClause>(); + clauses = new HashSet<ExecutionStateClause>(); top = true; bottom = false; } - + public void addClause(ExecutionStateClause clause) { // Cannot get out of bottom, do not add duplicate clauses if (!bottom && !clauses.contains(clause)) { @@ -37,110 +37,126 @@ public class ExecutionState { if (clauses.contains(clause.getNegation())) { clauses.clear(); bottom = true; // x AND NOT x = F - } - else { + } else { clauses.add(clause); } } } - + public void removeClause(ExecutionStateClause node) { clauses.remove(node); if (clauses.size() == 0) { setTop(); } } - + public void addTruthAssignment(IVariable var, boolean value) { truthAssignments.put(var, value); } - + public Map<IVariable, Boolean> getTruthAssignments() { return truthAssignments; } - + public void setTruthAssignments(Map<IVariable, Boolean> truthAssignments) { this.truthAssignments = truthAssignments; } - + public void bindTruthAssignments() { boolean unsatisfiable = false; - List<ExecutionStateClause> clausesCopy = new ArrayList<ExecutionStateClause>(clauses); + 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? + if (truth == c.isTrue()) { // does truth value of clause match + // truth assignment? removeClause(c); - } - else { + } 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 static Set<ExecutionState> join(Set<ExecutionState> es) { + ESTruthTable tt = new ESTruthTable(es); + ESSimplifier simp = new ESSimplifier(tt); + return simp.getExecutionStateCover(); } - - public ExecutionStateClause[] getClauses() { - return clauses.toArray(new ExecutionStateClause[clauses.size()]); + + public Set<ExecutionStateClause> getClauses() { + return clauses; } - + public boolean isTop() { return top; } - + public boolean isBottom() { return bottom; } - + public void setTop() { top = true; bottom = false; clauses.clear(); } - + public void setBottom() { bottom = true; top = false; clauses.clear(); } - + @Override public String toString() { String ret; if (top) { ret = "[TOP]"; - } - else if (bottom) { + } else if (bottom) { ret = "[BOTTOM]"; - } - else { + } else { StringBuffer buf = new StringBuffer(); if (clauses.size() > 0) { for (ExecutionStateClause c : clauses) { buf.append(c); buf.append(" AND "); } - buf.delete(buf.length() - 5 /* " AND ".length() */, buf.length()); + buf.delete(buf.length() - 5 /* " AND ".length() */, buf + .length()); } ret = buf.toString(); } return ret; } + public ExecutionState copy() { + ExecutionState ret = new ExecutionState(); + for (ExecutionStateClause cl : clauses) { + ret.addClause(cl); + } + return ret; + } + + @Override + public boolean equals(Object obj) { + if (obj instanceof ExecutionState) { + ExecutionState other = (ExecutionState) obj; + return clauses.equals(other.getClauses()) + && truthAssignments.equals(other.getTruthAssignments()) + && top == other.isTop() && bottom == other.isBottom(); + } + return false; + } + + @Override + public int hashCode() { + return clauses.hashCode() + truthAssignments.hashCode() + (top ? 1 : 0) + (bottom ? 1 : 0); + } + } diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ITruthTable.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ITruthTable.java new file mode 100644 index 0000000..dd15f2d --- /dev/null +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ITruthTable.java @@ -0,0 +1,21 @@ +/******************************************************************************* + * 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.List; + +public interface ITruthTable<E> { + + List<Minterm<E>> getMinterms(); + + List<E> getVariables(); + +} diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Minterm.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Minterm.java new file mode 100644 index 0000000..1aeb0a2 --- /dev/null +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Minterm.java @@ -0,0 +1,117 @@ +/******************************************************************************* + * 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.Map; + +public class Minterm<E> { + private Map<E, Value> values; + + public enum Value { + TRUE, + FALSE, + DONTCARE + } + + public Minterm(Map<E, Value> values) { + this.values = values; + } + + public void setValue(E var, Value val) { + values.put(var, val); + } + + public Value getValue(E var) { + return values.get(var); + } + + public int length() { + return values.size(); + } + + public Minterm<E> copy() { + return new Minterm<E>(new HashMap<E, Value>(values)); + } + + public Minterm<E> combineTerms(Minterm<E> other) { + Minterm<E> ret = null; + E diff = null; + for (E var : values.keySet()) { + if (!values.get(var).equals(other.getValue(var))) { + if (diff != null) { + // More than one difference + diff = null; + break; + } + diff = var; + } + } + + // One difference, combine + if (diff != null) { + ret = copy(); + // Set the differing value to don't care + ret.setValue(diff, Value.DONTCARE); + } + + return ret; + } + + public boolean implies(Minterm<E> other) { + boolean result = true; + for (E var : values.keySet()) { + Value value = values.get(var); + if (value != Value.DONTCARE && value != other.getValue(var)) { + result = false; + } + } + return result; + } + + @Override + public boolean equals(Object obj) { + if (obj instanceof Minterm<?>) { + Minterm<?> other = (Minterm<?>) obj; + return values.equals(other.values); + } + return false; + } + + @Override + public int hashCode() { + return values.hashCode(); + } + + @Override + public String toString() { + StringBuffer buf = new StringBuffer(); + for (E k : values.keySet()) { + buf.append(k); + buf.append(" "); + } + buf.append("\n"); + for (Value v : values.values()) { + switch (v) { + case TRUE: + buf.append("1"); + break; + case FALSE: + buf.append("0"); + break; + default: + buf.append("-"); + } + buf.append(" "); + } + return buf.toString(); + } +} 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 new file mode 100644 index 0000000..d363028 --- /dev/null +++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java @@ -0,0 +1,114 @@ +/******************************************************************************* + * 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.ArrayList; +import java.util.HashMap; +import java.util.LinkedList; +import java.util.List; +import java.util.Map; +import java.util.Queue; + +public class QuineMcCluskeySimplifier<E> { + protected List<Minterm<E>> minterms; + protected List<E> variables; + protected List<Minterm<E>> implicantCover; + + public QuineMcCluskeySimplifier(ITruthTable<E> tt) { + minterms = tt.getMinterms(); + variables = tt.getVariables(); + List<Minterm<E>> inputMinterms = new ArrayList<Minterm<E>>(minterms); + List<Minterm<E>> primeImplicants = new ArrayList<Minterm<E>>(minterms); + + boolean change = true; + while (change && minterms.size() > 1) { // Iterate until we achieve a steady state + change = false; + Queue<Minterm<E>> primary = new LinkedList<Minterm<E>>(); + primary.addAll(minterms); + while (!primary.isEmpty()) { // Iterate through all combinations + Minterm<E> one = primary.remove(); + Queue<Minterm<E>> secondary = new LinkedList<Minterm<E>>(); + secondary.addAll(minterms); + while (!secondary.isEmpty()) { + Minterm<E> two = secondary.remove(); + Minterm<E> combined = one.combineTerms(two); + if (combined != null) { + if (!minterms.contains(combined)) { + change = true; + minterms.add(combined); + } + // Combined one and two so neither are prime implicants + primeImplicants.remove(one); + primeImplicants.remove(two); + if (!primeImplicants.contains(combined)) { + primeImplicants.add(combined); + } + } + } + } + } + + // Determine which prime implicants cover which original minterms + Map<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) { + if (implicant.implies(minterm)) { + implications.get(implicant).add(minterm); + } + } + } + + implicantCover = new ArrayList<Minterm<E>>(); + // remove minterms which are implied by an essential implicant + List<Minterm<E>> mintermsCopy = new ArrayList<Minterm<E>>(inputMinterms); + for (Minterm<E> minterm : mintermsCopy) { + Minterm<E> implicant = null; + int numImplications = 0; + for (Minterm<E> pi : primeImplicants) { + List<Minterm<E>> impl = implications.get(pi); + if (impl.contains(minterm)) { + implicant = pi; + numImplications++; + } + } + // essential implicant + if (numImplications == 1) { + inputMinterms.removeAll(implications.get(implicant)); + if (!implicantCover.contains(implicant)) { + implicantCover.add(implicant); + } + } + } + + // Remove essential implicants from our list + primeImplicants.removeAll(implicantCover); + + // find a cover for the remaining minterms + while (inputMinterms.size() > 0) { + Minterm<E> maxImplicant = null; + for (Minterm<E> pi : primeImplicants) { + if (maxImplicant == null + || implications.get(pi).size() >= implications.get(maxImplicant).size()) { + maxImplicant = pi; + } + } + inputMinterms.removeAll(implications.get(maxImplicant)); + primeImplicants.remove(maxImplicant); + implicantCover.add(maxImplicant); + } + } + + public List<Minterm<E>> getImplicantCover() { + return implicantCover; + } + +} 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 93bf3be..19dd6b3 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 @@ -45,10 +45,7 @@ public class SymbolicState { public SymbolicState copy() { Set<PropertyState> ps = new HashSet<PropertyState>(propertyStates); - ExecutionState es = new ExecutionState(); - for (ExecutionStateClause cl : executionState.getClauses()) { - es.addClause(cl); - } + ExecutionState es = executionState.copy(); Map<IVariable, Boolean> truthAssignments = new HashMap<IVariable, Boolean>(executionState.getTruthAssignments()); es.setTruthAssignments(truthAssignments); @@ -65,4 +62,18 @@ public class SymbolicState { buf.append("]"); return buf.toString(); } + + @Override + public boolean equals(Object obj) { + if (obj instanceof SymbolicState) { + SymbolicState other = (SymbolicState) obj; + return propertyStates.equals(other.getPropertyStates()) && executionState.equals(other.getExecutionState()); + } + return false; + } + + @Override + public int hashCode() { + return propertyStates.hashCode() + executionState.hashCode(); + } } 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 5ea8e79..491a481 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 @@ -210,7 +210,7 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { } private Set<SymbolicState> group(Set<SymbolicState> ss) { - return groupPSA(ss); + return groupPropSim(ss); } private Set<SymbolicState> groupPSA(Set<SymbolicState> ss) { @@ -236,12 +236,15 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { for (PropertyState p : statesPerProperty.keySet()) { Set<PropertyState> ps = new HashSet<PropertyState>(); ps.add(p); - ExecutionState es = new ExecutionState(); - for (ExecutionState e : statesPerProperty.get(p)) { - es.join(e); + 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); } - SymbolicState s = new SymbolicState(ps, es); - ret.add(s); } return ret; |