Skip to content

Commit

Permalink
#295, incremental improvements, solving corner cases
Browse files Browse the repository at this point in the history
  • Loading branch information
@alexandernutz
alexandernutz committed Jan 27, 2018
1 parent 7372fef commit 51c630c
Show file tree
Hide file tree
Showing 5 changed files with 106 additions and 46 deletions.
19 changes: 15 additions & 4 deletions ...ik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/EqState.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@
import java.util.Set;
import java.util.stream.Collectors;

import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger;
import de.uni_freiburg.informatik.ultimate.logic.Script;
import de.uni_freiburg.informatik.ultimate.logic.Term;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.IAbstractState;
Expand Down Expand Up @@ -61,13 +62,15 @@ public class EqState implements IAbstractState<EqState>, IEqualityProvidingState
private final EqConstraint<EqNode> mConstraint;

private final EqStateFactory mFactory;
private final ILogger mLogger;

public EqState(final EqConstraint<EqNode> constraint,
final EqNodeAndFunctionFactory eqNodeAndFunctionFactory, final EqStateFactory eqStateFactory,
final Set<IProgramVarOrConst> variables) {
mConstraint = constraint;
mFactory = eqStateFactory;
mPvocs = Collections.unmodifiableSet(new HashSet<>(variables));
mLogger = mFactory.getLogger();
assert assertPvocsAreComplete(constraint);
}

Expand Down Expand Up @@ -244,8 +247,12 @@ public boolean areUnequal(final EqNode node1, final EqNode node2) {
public boolean areEqual(final Term term1, final Term term2) {
final EqNode node1 = mFactory.getEqNodeAndFunctionFactory().getExistingNode(term1);
final EqNode node2 = mFactory.getEqNodeAndFunctionFactory().getExistingNode(term2);
if (node1 == null || node2 == null) {
// we did not track at least one of the nodes
if (node1 == null) {
mLogger.debug("areEqual request: Term " + term1 + " is not known to this EqState, returning false");
return false;
}
if (node2 == null) {
mLogger.debug("areEqual request: Term " + term2 + " is not known to this EqState, returning false");
return false;
}
return mConstraint.areEqual(node1, node2);
Expand All @@ -255,8 +262,12 @@ public boolean areEqual(final Term term1, final Term term2) {
public boolean areUnequal(final Term term1, final Term term2) {
final EqNode node1 = mFactory.getEqNodeAndFunctionFactory().getExistingNode(term1);
final EqNode node2 = mFactory.getEqNodeAndFunctionFactory().getExistingNode(term2);
if (node1 == null || node2 == null) {
// we did not track at least one of the nodes
if (node1 == null) {
mLogger.debug("areUnequal request: Term " + term1 + " is not known to this EqState, returning false");
return false;
}
if (node2 == null) {
mLogger.debug("areUnequal request: Term " + term2 + " is not known to this EqState, returning false");
return false;
}
return mConstraint.areUnequal(node1, node2);
Expand Down
7 changes: 7 additions & 0 deletions ...mate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/EqStateFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
import java.util.Set;
import java.util.stream.Collectors;

import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger;
import de.uni_freiburg.informatik.ultimate.logic.Term;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain.EqConstraint;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain.EqConstraintFactory;
Expand All @@ -57,6 +58,7 @@ public class EqStateFactory {
private final IIcfgSymbolTable mSymbolTable;
private EqState mTopStateWithEmptyPvocs;
private final ManagedScript mMgdScript;
private final ILogger mLogger;

public EqStateFactory(final EqNodeAndFunctionFactory eqNodeAndFunctionFactory,
final EqConstraintFactory<EqNode> eqConstraintFactory,
Expand All @@ -65,6 +67,7 @@ public EqStateFactory(final EqNodeAndFunctionFactory eqNodeAndFunctionFactory,
mEqConstraintFactory = eqConstraintFactory;
mSymbolTable = symbolTable;
mMgdScript = mgdScript;
mLogger = mEqConstraintFactory.getLogger();
}

public EqState disjoinAll(final Set<EqState> statesForCurrentEc) {
Expand Down Expand Up @@ -145,4 +148,8 @@ public EqState getBottomState() {
return getEqState(mEqConstraintFactory.getBottomConstraint(), Collections.emptySet());
}

public ILogger getLogger() {
return mLogger;
}

}
114 changes: 80 additions & 34 deletions ...ni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepIcfgTransformer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -289,7 +289,7 @@ public HeapSeparatorBenchmark getStatistics() {
}

/**
* (almost) a copy from IcfgTranformationObserver
* (almost) a copy from IcfgTransformationObserver
* --> should probably replace this with a less ad-hoc solution some time
*
* @return
Expand Down Expand Up @@ -392,8 +392,9 @@ void processSelect(final SelectInfo selectInfo, final IEqualityProvidingIntermed
*/
continue;
}

if (eps.areUnequal(selectIndex.get(dim), freezeVar.getTerm())) {
final Term selectIndexNormalized =
selectInfo.getEdgeInfo().getProgramVarOrConstForTerm(selectIndex.get(dim)).getTerm();
if (eps.areUnequal(selectIndexNormalized, freezeVar.getTerm())) {
// nothing to do
} else {
// select index and freezeVar may be equal at this location
Expand All @@ -403,27 +404,72 @@ void processSelect(final SelectInfo selectInfo, final IEqualityProvidingIntermed
}


for (int i = 0; i < selectIndex.size(); i++) {
final Set<StoreIndexInfo> mayEqualStoreIndexInfos = dimensionToMayEqualStoreIndexInfos.getImage(i);
for (int dim = 0; dim < selectIndex.size(); dim++) {
final Set<StoreIndexInfo> mayEqualStoreIndexInfos = dimensionToMayEqualStoreIndexInfos.getImage(dim);

if (mayEqualStoreIndexInfos.size() <= 1) {
// nothing to do
} else {
final StoreIndexInfo sample = mayEqualStoreIndexInfos.iterator().next();

mSelectInfoToDimensionToToSampleStoreIndexInfo.put(selectInfo, i, sample);
if (mayEqualStoreIndexInfos.size() == 0) {
/* there is no array write/StoreIndexInfo that has a data flow to this array read/SelectInfo
* --> this is a special case, we can replace the array that is read here with an uninitialized array
* of the correct sort
*/
//TODO
assert false;
continue;
}
// } else if (mayEqualStoreIndexInfos.size() <= 1) {
// // nothing to do
// final StoreIndexInfo sample = mayEqualStoreIndexInfos.iterator().next();
// mSelectInfoToDimensionToToSampleStoreIndexInfo.put(selectInfo, i, sample);
// } else {
final StoreIndexInfo sample = mayEqualStoreIndexInfos.iterator().next();

for (final StoreIndexInfo sii : mayEqualStoreIndexInfos) {
mLogger.debug("merging partition blocks for array " + selectInfo.getArrayPvoc() + " :");
mLogger.debug("\t" + sii);
mLogger.debug("\t and");
mLogger.debug("\t" + sample);
mLogger.debug("\t because of possible aliasing at dimension " + i);
mLogger.debug("\t at array read " + selectInfo + ".");
mergeBlocks(selectInfo, i, sii, sample);
mSelectInfoToDimensionToToSampleStoreIndexInfo.put(selectInfo, dim, sample);

createPartitionAndBlockIfNecessary(selectInfo, dim, sample);

for (final StoreIndexInfo sii : mayEqualStoreIndexInfos) {
if (sii == sample) {
// no need to merge sii with itself
continue;
}
mLogger.debug("merging partition blocks for array " + selectInfo.getArrayPvoc() + " :");
mLogger.debug("\t" + sii);
mLogger.debug("\t and");
mLogger.debug("\t" + sample);
mLogger.debug("\t because of possible aliasing at dimension " + dim);
mLogger.debug("\t at array read " + selectInfo + ".");
mergeBlocks(selectInfo, dim, sii, sample);
}
// }
}
}

private void createPartitionAndBlockIfNecessary(final SelectInfo selectInfo, final int dim, final StoreIndexInfo sample) {
final IProgramVarOrConst array = selectInfo.getArrayPvoc();
final ArrayGroup arrayGroup = mArrayToArrayGroup.get(array);

UnionFind<StoreIndexInfo> partition = mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim);
if (partition == null) {
partition = new UnionFind<>();
mArrayGroupToDimensionToStoreIndexInfoPartition.put(arrayGroup, dim, partition);
}
partition.findAndConstructEquivalenceClassIfNeeded(sample);
}

private void mergeBlocks(final SelectInfo selectInfo, final int dim, final StoreIndexInfo sii1,
final StoreIndexInfo sii2) {
final IProgramVarOrConst array = selectInfo.getArrayPvoc();
final ArrayGroup arrayGroup = mArrayToArrayGroup.get(array);

final UnionFind<StoreIndexInfo> partition = mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim);
if (partition == null) {
throw new AssertionError("should have been created in createBlockIfNecessary");
}

partition.findAndConstructEquivalenceClassIfNeeded(sii1);
partition.findAndConstructEquivalenceClassIfNeeded(sii2);
partition.union(sii1, sii2);
}

public void finish() {
Expand Down Expand Up @@ -452,6 +498,22 @@ public void finish() {
}
mIsFinished = true;

mLogger.info("partitioning result:");
for (final ArrayGroup arrayGroup : mArrayToArrayGroup.values()) {
mLogger.info("\t location blocks for array group + " + arrayGroup);
for (int dim = 0; dim < arrayGroup.getDimensionality(); dim++) {
mLogger.info("\t at dimension " + dim);
mLogger.info("\t # array writes :" +
mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim).getAllElements().size());
mLogger.info("\t # location blocks :" +
mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim).getAllEquivalenceClasses().size());
// mLogger.info("\t the location blocks are :" +
// mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim).getAllEquivalenceClasses().size());
}


}

assert sanityCheck();
}

Expand Down Expand Up @@ -496,22 +558,6 @@ private boolean sanityCheck() {
return true;
}

private void mergeBlocks(final SelectInfo selectInfo, final int dim, final StoreIndexInfo sii1,
final StoreIndexInfo sii2) {
final IProgramVarOrConst array = selectInfo.getArrayPvoc();
final ArrayGroup arrayGroup = mArrayToArrayGroup.get(array);

UnionFind<StoreIndexInfo> partition = mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim);
if (partition == null) {
partition = new UnionFind<>();
mArrayGroupToDimensionToStoreIndexInfoPartition.put(arrayGroup, dim, partition);
}

partition.findAndConstructEquivalenceClassIfNeeded(sii1);
partition.findAndConstructEquivalenceClassIfNeeded(sii2);
partition.union(sii1, sii2);
}

public NestedMap2<SelectInfo, Integer, LocationBlock> getSelectInfoToDimensionToLocationBlock() {
if (!mIsFinished) {
throw new AssertionError();
Expand Down
5 changes: 4 additions & 1 deletion ...informatik/ultimate/icfgtransformer/heapseparator/PartitionProjectionTermTransformer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,10 @@ public PartitionProjectionTermTransformer(final ManagedScript mgdScript, final S

// mSelectIndexTermToLocationBlock = selectIndexTermToLocationBlock;

// assert Objects.nonNull(arrayCellAccessToDimensionToLocationBlock);
assert Objects.nonNull(arrayCellAccessToDimensionToLocationBlock)
|| !ArrayCellAccess.extractArrayCellAccesses(edgeInfo.getEdge().getTransformula().getFormula()).stream()
.anyMatch(aca -> mHeapArrays.contains(edgeInfo.getProgramVarOrConstForTerm(aca.getSimpleArray())))
: "this input map must be non-null if we have a select on a heap array inside the edge";
mArrayCellAccessToIntegerToLocationBlock = arrayCellAccessToDimensionToLocationBlock;

mArrayGroupToDimensionToLocationBlocks = arrayGroupToDimensionToLocationBlocks;
Expand Down
7 changes: 0 additions & 7 deletions ...atik/ultimate/icfgtransformer/heapseparator/PartitionProjectionTransitionTransformer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -129,18 +129,11 @@ public IcfgEdge transform(final IcfgEdge edge, final OUTLOC newSource, final OUT
final NestedMap2<ArrayCellAccess, Integer, LocationBlock> arrayCellAccessToDimensionToLocationBlock =
mEdgeInfoToArrayCellAccessToDimensionToLocationBlock.get(edgeInfo);

// maps each term in a storeindexInfo sii of the current edge to the locationBlock that sii occurs in
// final Map<Term, LocationBlock> indexTermToLocationBlock = new HashMap<>();
// for (final Entry<Term, StoreIndexInfo> en : mEdgeToIndexToStoreIndexInfo.get(edgeInfo).entrySet()) {
// indexTermToLocationBlock.put(en.getKey(), mStoreIndexInfoToLocationBlock.get(en.getValue()));
// }

final PartitionProjectionTermTransformer ppttf =
new PartitionProjectionTermTransformer(mMgdScript, mSubArrayManager,
arrayCellAccessToDimensionToLocationBlock,
edgeInfo, mArrayGroupToDimensionToLocationBlocks, mArrayToArrayGroup,
mEdgeToIndexToStoreIndexInfo, mHeapArrays);//,
//indexTermToLocationBlock);
final Term transformedFormula = ppttf.transform(tf.getFormula());

final Map<IProgramVar, TermVariable> inVars = ppttf.getNewInVars();
Expand Down

0 comments on commit 51c630c

Please sign in to comment.