#295, ignore non-heap arrays, bug hunting

ultimate-pa · Jan 26, 2018 · 580494a · 580494a
1 parent ca67c26
commit 580494a
Show file tree

Hide file tree

Showing 9 changed files with 253 additions and 118 deletions.
diff --git a/trunk/examples/programs/heapseparator/mem-separable.c b/trunk/examples/programs/heapseparator/mem-separable.c
@@ -1,10 +1,15 @@
-
+//#Safe
 int main() {
   int *p = malloc(4);
   int *q = malloc(4);
 
   *p = 0;
-  *q = 0;
+  *q = 1;
+
+  int x = *p;
+  int y = *q;
+
+  //@ assert p != q;
 
   free(p);
   free(q);

diff --git a/..._freiburg/informatik/ultimate/icfgtransformer/heapseparator/ArrayEqualityAllowStores.java b/..._freiburg/informatik/ultimate/icfgtransformer/heapseparator/ArrayEqualityAllowStores.java
@@ -132,6 +132,11 @@ public static List<ArrayEqualityAllowStores> extractArrayEqualityAllowStores(fin
 
 	}
 
+	/**
+	 * get the simple array on the left hand side of the equation
+	 *
+	 * @return
+	 */
 	public Term getLhsArray() {
 		if (mArrayUpdate != null) {
 			return mArrayUpdate.getNewArray();
@@ -145,6 +150,12 @@ public Term getLhsArray() {
 		throw new AssertionError();
 	}
 
+	/**
+	 *
+	 * get the simple array on the left hand side of the equation
+	 *
+	 * @return
+	 */
 	public Term getRhsArray() {
 		if (mArrayUpdate != null) {
 			return mArrayUpdate.getOldArray();

diff --git a/...mer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/ArrayGroup.java b/...mer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/ArrayGroup.java
@@ -28,4 +28,36 @@ public String toString() {
 	public int getDimensionality() {
 		return mDimensionality;
 	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((mArraysInThisGroup == null) ? 0 : mArraysInThisGroup.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(final Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (getClass() != obj.getClass()) {
+			return false;
+		}
+		final ArrayGroup other = (ArrayGroup) obj;
+		if (mArraysInThisGroup == null) {
+			if (other.mArraysInThisGroup != null) {
+				return false;
+			}
+		} else if (!mArraysInThisGroup.equals(other.mArraysInThisGroup)) {
+			return false;
+		}
+		return true;
+	}
+
+
 }
diff --git a/...ni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepIcfgTransformer.java b/...ni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepIcfgTransformer.java
@@ -1,9 +1,12 @@
 package de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator;
 
+import java.util.Arrays;
 import java.util.HashMap;
+import java.util.List;
 import java.util.Map;
 import java.util.Map.Entry;
 import java.util.Set;
+import java.util.stream.Collectors;
 
 import de.uni_freiburg.informatik.ultimate.core.model.models.ModelUtils;
 import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger;
@@ -39,6 +42,11 @@ public class HeapSepIcfgTransformer<INLOC extends IcfgLocation, OUTLOC extends I
 
 	private final Preprocessing mPreprocessing = Preprocessing.FREEZE_VARIABLES;
 
+	/**
+	 * The IProgramVarOrConsts that model the heap in our memory model.
+	 */
+	private final List<IProgramVarOrConst> mHeapArrays;
+
 	private final ILogger mLogger;
 
 	private final HeapSeparatorBenchmark mStatistics;
@@ -75,6 +83,12 @@ public HeapSepIcfgTransformer(final ILogger logger, final IIcfg<INLOC> originalI
 		mManagedScript = originalIcfg.getCfgSmtToolkit().getManagedScript();
 		mLogger = logger;
 
+		// TODO: complete, make nicer..
+		final List<String> heapArrayNames = Arrays.asList("#memory_int", "memory_$Pointer$");
+
+		mHeapArrays = originalIcfg.getCfgSmtToolkit().getSymbolTable().getGlobals().stream()
+				.filter(pvoc -> heapArrayNames.contains(pvoc.getGloballyUniqueId())).collect(Collectors.toList());
+
 		computeResult(originalIcfg, funLocFac, replacementVarFactory, backtranslationTracker, outLocationClass,
 				newIcfgIdentifier, equalityProvider, validArray);
 	}
@@ -181,13 +195,14 @@ private void computeResult(final IIcfg<INLOC> originalIcfg, final ILocationFacto
 		 *  <li> an array cell is accessed
 		 *  <li> two arrays are related
 		 */
-		final HeapSepPreAnalysis heapSepPreanalysis = new HeapSepPreAnalysis(mLogger, mManagedScript);
+		final HeapSepPreAnalysis heapSepPreanalysis = new HeapSepPreAnalysis(mLogger, mManagedScript, mHeapArrays);
 		new IcfgEdgeIterator(originalIcfg).forEachRemaining(edge -> heapSepPreanalysis.processEdge(edge));
 		heapSepPreanalysis.finish();
 
 		final Map<IProgramVarOrConst, ArrayGroup> arrayToArrayGroup = heapSepPreanalysis.getArrayToArrayGroup();
 
-		final PartitionManager partitionManager = new PartitionManager(arrayToArrayGroup, storeIndexInfoToFreezeVar);
+		final PartitionManager partitionManager = new PartitionManager(arrayToArrayGroup, storeIndexInfoToFreezeVar,
+				mHeapArrays);
 
 		/*
 		 * 3b. compute an array partitioning
@@ -213,7 +228,9 @@ private void computeResult(final IIcfg<INLOC> originalIcfg, final ILocationFacto
 						originalIcfg, funLocFac, backtranslationTracker,
 						partitionManager.getSelectInfoToDimensionToLocationBlock(),
 						edgeToIndexToStoreIndexInfo,
-						arrayToArrayGroup);
+						arrayToArrayGroup,
+						mHeapArrays,
+						mStatistics);
 		mResultIcfg = heapSeparatingTransformer.getResult();
 	}
 
@@ -318,8 +335,11 @@ class PartitionManager {
 
 	private boolean mIsFinished = false;
 
+	private final List<IProgramVarOrConst> mHeapArrays;
+
 	public PartitionManager(final Map<IProgramVarOrConst, ArrayGroup> arrayToArrayGroup,
-			final Map<StoreIndexInfo, IProgramNonOldVar> arrayAccessInfoToFreezeVar) {
+			final Map<StoreIndexInfo, IProgramNonOldVar> arrayAccessInfoToFreezeVar,
+			final List<IProgramVarOrConst> heapArrays) {
 
 //		mArrayToArrayGroup = new HashMap<>();
 //		for (final ArrayGroup ag : arrayGroups) {
@@ -338,6 +358,8 @@ public PartitionManager(final Map<IProgramVarOrConst, ArrayGroup> arrayToArrayGr
 		mSelectInfoToDimensionToLocationBlock = new NestedMap2<>();
 
 		mSelectInfoToDimensionToToSampleStoreIndexInfo = new NestedMap2<>();
+
+		mHeapArrays = heapArrays;
 	}
 
 	/**

diff --git a/...de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepPreAnalysis.java b/...de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepPreAnalysis.java
@@ -29,6 +29,7 @@
 import java.util.Collections;
 import java.util.HashMap;
 import java.util.HashSet;
+import java.util.List;
 import java.util.Map;
 import java.util.Map.Entry;
 import java.util.Set;
@@ -37,7 +38,6 @@
 import de.uni_freiburg.informatik.ultimate.logic.Term;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgEdge;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.transitions.UnmodifiableTransFormula;
-import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVar;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVarOrConst;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.arrays.ArrayUpdate;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.managedscript.ManagedScript;
@@ -69,25 +69,33 @@ public class HeapSepPreAnalysis {
 
 	private final HashRelation<EdgeInfo, ArrayEqualityAllowStores> mEdgeToArrayRelations;
 
-	private final HashRelation<EdgeInfo, ArrayCellAccess> mEdgeToArrayCellAccesses;
+//	private final HashRelation<EdgeInfo, ArrayCellAccess> mEdgeToArrayCellAccesses;
 
 	private final ManagedScript mMgdScript;
 
-	private Set<SelectInfo> mSelectInfos;
+	private final Set<SelectInfo> mSelectInfos;
 
 	private Set<ArrayGroup> mArrayGroups;
 
+	private final List<IProgramVarOrConst> mHeapArrays;
+
 	/**
 	 *
 	 * @param logger
+	 * @param heapArrays
 	 * @param equalityProvider
 	 */
-	public HeapSepPreAnalysis(final ILogger logger, final ManagedScript mgdScript) {
+	public HeapSepPreAnalysis(final ILogger logger, final ManagedScript mgdScript,
+			final List<IProgramVarOrConst> heapArrays) {
 		mMgdScript = mgdScript;
 
+		mHeapArrays = heapArrays;
+
 		mEdgeToCellUpdates = new HashRelation<>();
-		mEdgeToArrayCellAccesses = new HashRelation<>();
+//		mEdgeToArrayCellAccesses = new HashRelation<>();
 		mEdgeToArrayRelations = new HashRelation<>();
+
+		mSelectInfos = new HashSet<>();
 	}
 
 	public void processEdge(final IcfgEdge edge) {
@@ -107,7 +115,16 @@ public void processEdge(final IcfgEdge edge) {
 			assert au.getNewArray() != au.getOldArray() : "that would be a strange case, no?..";
 			assert !au.isNegatedEquality() : "strange case";
 
-			// we only keep array updates that have the same ProgramVar lhs und rhs
+			/*
+			 * only track updates to one of the heap arrays
+			 */
+			if (!mHeapArrays.contains(newArrayPv)) {
+				continue;
+			}
+
+			/* we only keep array updates that have the same ProgramVar lhs und rhs
+			 * (the others are processed as ArrayEqualityAllowStores')
+			 */
 			if (newArrayPv.equals(oldArrayPv)) {
 				mEdgeToCellUpdates.addPair(edgeInfo, au);
 				visitedSubTerms.add(au.getArrayUpdateTerm());
@@ -120,70 +137,37 @@ public void processEdge(final IcfgEdge edge) {
 				// term is already stored as a cell update
 				continue;
 			}
+
+			final IProgramVarOrConst lhsPvoc = edgeInfo.getProgramVarOrConstForTerm(aeas.getLhsArray());
+			final IProgramVarOrConst rhsPvoc = edgeInfo.getProgramVarOrConstForTerm(aeas.getRhsArray());
+			// filter out aeas that do not relate to a heap array
+			if (!mHeapArrays.contains(lhsPvoc) && !mHeapArrays.contains(rhsPvoc)) {
+				continue;
+			}
+
 			mEdgeToArrayRelations.addPair(edgeInfo, aeas);
 //			visitedSubTerms.add(aeas.getTerm(mMgdScript.getScript()));
 		}
 
 		for (final ArrayCellAccess aca : ArrayCellAccess.extractArrayCellAccesses(tf.getFormula())) {
 //			assert !visitedSubTerms.contains(aca.getTerm(mMgdScript.getScript()));
-			mEdgeToArrayCellAccesses.addPair(edgeInfo, aca);
-		}
-	}
 
-	// not used right now --> remove?
-	@Deprecated
-	Set<Term> getArraysAsTerms() {
-		assert false;
-		return null;
-	}
+			final SelectInfo selectInfo = new SelectInfo(aca, edgeInfo);
+			if (mHeapArrays.contains(selectInfo.getArrayPvoc())) {
+				mSelectInfos.add(selectInfo);
+			}
 
-	// not used right now --> remove?
-	@Deprecated
-	Set<IProgramVar> getArraysAsProgramVars() {
-		assert false;
-		return null;
+//			mEdgeToArrayCellAccesses.addPair(edgeInfo, aca);
+		}
 	}
 
-//	/**
-//	 * Helper to get a IProgramVar from a TermVariable via the In/OutVarsMapping
-//	 *
-//	 * @param tv
-//	 * @param map
-//	 * @return
-//	 */
-//	private static IProgramVar getVarForTerm(final TermVariable tv, final Map<IProgramVar, TermVariable> map) {
-//		for (final Entry<IProgramVar, TermVariable> en: map.entrySet()) {
-//			if (en.getValue() == tv) {
-//				return en.getKey();
-//			}
-//		}
-//		throw new IllegalArgumentException();
-//	}
-
-//	private static IProgramVarOrConst getVarOrConstForTerm(final TermVariable tv, final Map<IProgramVar, TermVariable> map) {
-//		final IProgramVar var = getVarForTerm(tv, map);
-//		if (var != null) {
-//			return var;
-//		}
-//
-//		throw new AssertionError();
-//
-//	}
-
 	public Set<SelectInfo> getSelectInfos() {
 		if (mSelectInfos == null) {
 			throw new IllegalStateException("call finish first");
 		}
 		return mSelectInfos;
 	}
 
-//	public Set<ArrayGroup> getArrayGroups() {
-//		if (mArrayGroups == null) {
-//			throw new IllegalStateException("call finish first");
-//		}
-//		return mArrayGroups;
-//	}
-
 	public Map<IProgramVarOrConst, ArrayGroup> getArrayToArrayGroup() {
 		if (mArrayGroups == null) {
 			throw new IllegalStateException("call finish first");
@@ -198,17 +182,21 @@ public Map<IProgramVarOrConst, ArrayGroup> getArrayToArrayGroup() {
 	}
 
 	public void finish() {
-		mSelectInfos = new HashSet<>();
-		for (final Entry<EdgeInfo, ArrayCellAccess> en : mEdgeToArrayCellAccesses) {
-			final SelectInfo selectInfo = new SelectInfo(en.getValue(), en.getKey());
-			mSelectInfos.add(selectInfo);
-		}
+//		mSelectInfos = new HashSet<>();
+//		for (final Entry<EdgeInfo, ArrayCellAccess> en : mEdgeToArrayCellAccesses) {
+//			final SelectInfo selectInfo = new SelectInfo(en.getValue(), en.getKey());
+//			mSelectInfos.add(selectInfo);
+//		}
 
 		/*
 		 * Compute the array groups. Rule: Whenever two arrays are related via "=" in any formula in the program, they
 		 *  must be in the same array group.
 		 */
 		final UnionFind<IProgramVarOrConst> arrayPartition = new UnionFind<>();
+
+		// base line for the array groups: the heap arrays
+		mHeapArrays.forEach(arrayPartition::findAndConstructEquivalenceClassIfNeeded);
+
 		for (final Entry<EdgeInfo, ArrayEqualityAllowStores> en : mEdgeToArrayRelations) {
 			final EdgeInfo edgeInfo = en.getKey();
 			final ArrayEqualityAllowStores aeas = en.getValue();