#295, extra variant of LocArrayInfo, namely LocArrayReadInfo, for whe…

…n a loc-array is not touched during loc-array-preprocessing, but one of its values is queried, during partition computation
ultimate-pa · Aug 27, 2018 · c312d3a · c312d3a
1 parent ee5830d
commit c312d3a
Show file tree

Hide file tree

Showing 4 changed files with 92 additions and 41 deletions.
diff --git a/.../uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapPartitionManager.java b/.../uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapPartitionManager.java
@@ -135,8 +135,10 @@ void processSelect(final SelectInfo selectInfo, final IEqualityProvidingIntermed
 			// i_dim is the index prefix up to the current dimension
 			final ArrayIndex indexForCurrentDim = selectIndex.getFirst(dim);
 
-			final LocArrayInfo locArray = mMemLocArrayManager.getLocArray(selectInfo.getEdgeInfo(),
-					selectInfo.getArrayCellAccess().getArray(), dim);
+//			final LocArrayInfo locArray = mMemLocArrayManager.getLocArray(selectInfo.getEdgeInfo(),
+			final LocArrayInfo locArray = mMemLocArrayManager.getOrConstructLocArray(selectInfo.getEdgeInfo(),
+//					selectInfo.getArrayCellAccess().getArray(), dim);
+					selectInfo.getArrayCellAccess().getArray(), dim, true);
 
 			// build the term a-loc-dim[i_dim]
 			mMgdScript.lock(this);
@@ -174,10 +176,11 @@ private void mergeBlocks(final SelectInfo selectInfo, final int dim,
 			throw new AssertionError("should have been created in createBlockIfNecessary");
 		}
 
+		partition.findAndConstructEquivalenceClassIfNeeded(setConstraintAsStoreInfos.get(0));
 		for (int i = 1; i < setConstraintAsStoreInfos.size(); i++) {
 			final StoreInfo si1 = setConstraintAsStoreInfos.get(i - 1);
 			final StoreInfo si2 = setConstraintAsStoreInfos.get(i);
-			partition.findAndConstructEquivalenceClassIfNeeded(si1);
+			partition.findAndConstructEquivalenceClassIfNeeded(si2);
 			if (si1 instanceof NoStoreInfo || si2 instanceof NoStoreInfo) {
 				// partition intersection on "uninitialized/havoc array writes" does not trigger a merge
 				continue;
@@ -232,7 +235,7 @@ public void finish() {
 
 			mLogger.info("\t location blocks for array group " + arrayGroup);
 
-			for (int dim = 0; dim < arrayGroup.getDimensionality(); dim++) {
+			for (int dim = 1; dim <= arrayGroup.getDimensionality(); dim++) {
 				final UnionFind<StoreInfo> partition =
 						mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim);
 				final int noWrites = partition == null ? 0 : partition.getAllElements().size();

diff --git a/...r/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/LocArrayInfo.java b/...r/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/LocArrayInfo.java
@@ -26,6 +26,7 @@ public LocArrayInfo(final EdgeInfo edge, final IProgramVarOrConst pvoc, final Te
 		mEdge = edge;
 		mPvoc = pvoc;
 		mTerm = term;
+		assert this instanceof LocArrayReadInfo || initializingConstantArray != null;
 		mInitializingConstantArray = initializingConstantArray;
 	}
 

diff --git a/...c/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/LocArrayReadInfo.java b/...c/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/LocArrayReadInfo.java
@@ -0,0 +1,13 @@
+package de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator;
+
+import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.EdgeInfo;
+import de.uni_freiburg.informatik.ultimate.logic.Term;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVarOrConst;
+
+public class LocArrayReadInfo extends LocArrayInfo {
+
+	public LocArrayReadInfo(final EdgeInfo edge, final IProgramVarOrConst pvoc, final Term term) {
+		super(edge, pvoc, term, null);
+	}
+
+}
diff --git a/...de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/MemlocArrayManager.java b/...de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/MemlocArrayManager.java
@@ -88,50 +88,84 @@ public Set<HeapSepProgramConst> getInitLocLits() {
 	}
 
 	public LocArrayInfo getOrConstructLocArray(final EdgeInfo edgeInfo, final Term baseArrayTerm, final int dim) {
+		return getOrConstructLocArray(edgeInfo, baseArrayTerm, dim, false);
+	}
+
+	/**
+	 *
+	 * @param edgeInfo
+	 * @param baseArrayTerm
+	 * @param dim
+	 * @param calledFromProcessSelect not called during preprocessing before abstract interpretation but because
+	 *   of an array read..
+	 * @return
+	 */
+	public LocArrayInfo getOrConstructLocArray(final EdgeInfo edgeInfo, final Term baseArrayTerm, final int dim,
+			final boolean calledFromProcessSelect) {
 		LocArrayInfo result = mEdgeToArrayTermToDimToLocArray.get(edgeInfo, baseArrayTerm, dim);
 		if (result == null) {
-			assert !mFrozen;
-
-			mMgdScript.lock(this);
-			final Sort locArraySort = computeLocArraySort(baseArrayTerm.getSort());
-
-			final IProgramVarOrConst pvoc;
-			final Term term;
-			{
-				if (baseArrayTerm instanceof TermVariable) {
-					final IProgramVar invar = edgeInfo.getInVar(baseArrayTerm);
-					final IProgramVar outvar = edgeInfo.getOutVar(baseArrayTerm);
-					final boolean isAuxVar = edgeInfo.getAuxVars().contains(baseArrayTerm);
-
-					if (invar != null) {
-						pvoc = getLocArrayPvocForArrayPvoc(invar, dim, locArraySort);
-						term = mMgdScript.constructFreshTermVariable(
-								sanitizeVarName(LOC_ARRAY_PREFIX + baseArrayTerm + "_" + dim),
-								locArraySort);
-					} else if (outvar != null) {
-						pvoc = getLocArrayPvocForArrayPvoc(outvar, dim, locArraySort);
-						term = mMgdScript.constructFreshTermVariable(
-								sanitizeVarName(LOC_ARRAY_PREFIX + baseArrayTerm + "_" + dim),
-								locArraySort);
-					} else if (isAuxVar) {
-						pvoc = null;
-						term = mMgdScript.constructFreshTermVariable(
-								sanitizeVarName(LOC_ARRAY_PREFIX + baseArrayTerm + "_" + dim),
-								locArraySort);
+			if (calledFromProcessSelect) {
+				// called from after-ai querying --> no update to the array should happen in the edge
+				final IProgramVarOrConst pvoc = edgeInfo.getProgramVarOrConstForTerm(baseArrayTerm);
+				// pvoc should be in an out, with tv baseArrayTerm
+				assert edgeInfo.getOutVar(baseArrayTerm) == pvoc;
+				assert edgeInfo.getInVar(baseArrayTerm) == pvoc;
+				assert !edgeInfo.getEdge().getTransformula().getAssignedVars().contains(pvoc);
+
+				final Sort locArraySort = computeLocArraySort(baseArrayTerm.getSort());
+				final IProgramVarOrConst locPvoc = getLocArrayPvocForArrayPvoc(pvoc, dim, locArraySort);
+
+				/*
+				 *  because there is no update to the array, no LocArray was constructed here during pre-ai-processing
+				 *  also, the loc-array is not updated, and not read in the ai-preprocessed program, thus, in the
+				 *  EqualityProvidingIntermediateState, it must be queried via the standard-pvoc-term
+				 */
+				result = new LocArrayReadInfo(edgeInfo, locPvoc, locPvoc.getTerm());
+				mEdgeToArrayTermToDimToLocArray.put(edgeInfo, baseArrayTerm, dim, result);
+			} else {
+				assert !mFrozen;
+
+				mMgdScript.lock(this);
+				final Sort locArraySort = computeLocArraySort(baseArrayTerm.getSort());
+
+				final IProgramVarOrConst pvoc;
+				final Term term;
+				{
+					if (baseArrayTerm instanceof TermVariable) {
+						final IProgramVar invar = edgeInfo.getInVar(baseArrayTerm);
+						final IProgramVar outvar = edgeInfo.getOutVar(baseArrayTerm);
+						final boolean isAuxVar = edgeInfo.getAuxVars().contains(baseArrayTerm);
+
+						if (invar != null) {
+							pvoc = getLocArrayPvocForArrayPvoc(invar, dim, locArraySort);
+							term = mMgdScript.constructFreshTermVariable(
+									sanitizeVarName(LOC_ARRAY_PREFIX + baseArrayTerm + "_" + dim),
+									locArraySort);
+						} else if (outvar != null) {
+							pvoc = getLocArrayPvocForArrayPvoc(outvar, dim, locArraySort);
+							term = mMgdScript.constructFreshTermVariable(
+									sanitizeVarName(LOC_ARRAY_PREFIX + baseArrayTerm + "_" + dim),
+									locArraySort);
+						} else if (isAuxVar) {
+							pvoc = null;
+							term = mMgdScript.constructFreshTermVariable(
+									sanitizeVarName(LOC_ARRAY_PREFIX + baseArrayTerm + "_" + dim),
+									locArraySort);
+						} else {
+							throw new AssertionError();
+						}
 					} else {
-						throw new AssertionError();
+						throw new UnsupportedOperationException("todo: deal with constants");
 					}
-				} else {
-					throw new UnsupportedOperationException("todo: deal with constants");
 				}
-			}
-			final HeapSepProgramConst initLocLit = getOrConstructInitLocLitForLocArraySort(locArraySort, dim);
-			result = new LocArrayInfo(edgeInfo, pvoc, term,
-					computeInitConstantArrayForLocArray(initLocLit, locArraySort));
+				final HeapSepProgramConst initLocLit = getOrConstructInitLocLitForLocArraySort(locArraySort, dim);
+				result = new LocArrayInfo(edgeInfo, pvoc, term,
+						computeInitConstantArrayForLocArray(initLocLit, locArraySort));
 
-			mMgdScript.unlock(this);
+				mMgdScript.unlock(this);
 
-			mEdgeToArrayTermToDimToLocArray.put(edgeInfo, baseArrayTerm, dim, result);
+				mEdgeToArrayTermToDimToLocArray.put(edgeInfo, baseArrayTerm, dim, result);
+			}
 		}
 		return result;
 	}