From 25eebecd10f8bfa9810e73f4efdc5b0be4a305a2 Mon Sep 17 00:00:00 2001 From: Elliott Baron Date: Sun, 1 Nov 2009 00:02:17 -0400 Subject: 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. --- .../eclipse/cdt/codan/extension/ESSimplifier.java | 72 +++++++++++++ .../eclipse/cdt/codan/extension/ESTruthTable.java | 86 +++++++++++++++ .../cdt/codan/extension/ExecutionState.java | 100 ++++++++++-------- .../eclipse/cdt/codan/extension/ITruthTable.java | 21 ++++ .../org/eclipse/cdt/codan/extension/Minterm.java | 117 +++++++++++++++++++++ .../codan/extension/QuineMcCluskeySimplifier.java | 114 ++++++++++++++++++++ .../eclipse/cdt/codan/extension/SymbolicState.java | 19 +++- .../checkers/CloseOpenedFilesChecker.java | 15 +-- 8 files changed, 492 insertions(+), 52 deletions(-) create mode 100644 org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java create mode 100644 org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java create mode 100644 org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ITruthTable.java create mode 100644 org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Minterm.java create mode 100644 org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java 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 { + + public ESSimplifier(ITruthTable tt) { + super(tt); + } + + public Set getExecutionStateCover() { + Set ret = new HashSet(); + List> implicantCover = getImplicantCover(); + for (Minterm 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 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 { + private List> minterms; + private List variables; + + public ESTruthTable(Set es) { + minterms = new ArrayList>(); + variables = new ArrayList(); + + 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 values = new HashMap(); + for (IVariable var : variables) { + values.put(var, Value.DONTCARE); + } + minterms.add(new Minterm(values)); + } + + // Set actual truth values + Iterator it = es.iterator(); + for (int i = 0; i < es.size(); i++) { + Minterm 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> getMinterms() { + return minterms; + } + + public List 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 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 clauses; + private Set clauses; private Map truthAssignments; private boolean top; private boolean bottom; public ExecutionState() { truthAssignments = new HashMap(); - clauses = new ArrayList(); + clauses = new HashSet(); 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 getTruthAssignments() { return truthAssignments; } - + public void setTruthAssignments(Map truthAssignments) { this.truthAssignments = truthAssignments; } - + public void bindTruthAssignments() { boolean unsatisfiable = false; - List clausesCopy = new ArrayList(clauses); + 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? + 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 join(Set 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 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 { + + List> getMinterms(); + + List 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 { + private Map values; + + public enum Value { + TRUE, + FALSE, + DONTCARE + } + + public Minterm(Map 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 copy() { + return new Minterm(new HashMap(values)); + } + + public Minterm combineTerms(Minterm other) { + Minterm 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 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 { + protected List> minterms; + protected List variables; + protected List> implicantCover; + + public QuineMcCluskeySimplifier(ITruthTable tt) { + minterms = tt.getMinterms(); + variables = tt.getVariables(); + List> inputMinterms = new ArrayList>(minterms); + List> primeImplicants = new ArrayList>(minterms); + + boolean change = true; + while (change && minterms.size() > 1) { // Iterate until we achieve a steady state + change = false; + Queue> primary = new LinkedList>(); + primary.addAll(minterms); + while (!primary.isEmpty()) { // Iterate through all combinations + Minterm one = primary.remove(); + Queue> secondary = new LinkedList>(); + secondary.addAll(minterms); + while (!secondary.isEmpty()) { + Minterm two = secondary.remove(); + Minterm 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, List>> implications = new HashMap, List>>(); + for (Minterm implicant : primeImplicants) { + implications.put(implicant, new ArrayList>()); + for (Minterm minterm : inputMinterms) { + if (implicant.implies(minterm)) { + implications.get(implicant).add(minterm); + } + } + } + + implicantCover = new ArrayList>(); + // remove minterms which are implied by an essential implicant + List> mintermsCopy = new ArrayList>(inputMinterms); + for (Minterm minterm : mintermsCopy) { + Minterm implicant = null; + int numImplications = 0; + for (Minterm pi : primeImplicants) { + List> 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 maxImplicant = null; + for (Minterm 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> 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 ps = new HashSet(propertyStates); - ExecutionState es = new ExecutionState(); - for (ExecutionStateClause cl : executionState.getClauses()) { - es.addClause(cl); - } + ExecutionState es = executionState.copy(); Map truthAssignments = new HashMap(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 group(Set ss) { - return groupPSA(ss); + return groupPropSim(ss); } private Set groupPSA(Set ss) { @@ -236,12 +236,15 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker { for (PropertyState p : statesPerProperty.keySet()) { Set ps = new HashSet(); ps.add(p); - ExecutionState es = new ExecutionState(); - for (ExecutionState e : statesPerProperty.get(p)) { - es.join(e); + Set 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; -- cgit