#295, first implementations of aspects of the freeze-var transformati…

…on: adding freeze var updates at array updates, initializing freeze vars with freeze var literals (still missing: initializing valid at freeze var literals), announcing freeze var literals to the equality domain

trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/VPDomain.java

@@ -29,6 +29,7 @@
 package de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.domain.transformula.vp;
 
 import java.util.Map.Entry;
+import java.util.Set;
 
 import de.uni_freiburg.informatik.ultimate.core.lib.results.StatisticsResult;
 import de.uni_freiburg.informatik.ultimate.core.model.preferences.IPreferenceProvider;
@@ -46,6 +47,7 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.IIcfgSymbolTable;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfgTransition;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocation;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramConst;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.managedscript.ManagedScript;
 import de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.Activator;
 
@@ -77,7 +79,8 @@ public class VPDomain<ACTION extends IIcfgTransition<IcfgLocation>>
 
 	private final VPDomainBenchmark mBenchmark;
 
-	public VPDomain(final ILogger logger, final IUltimateServiceProvider services, final CfgSmtToolkit csToolkit) {
+	public VPDomain(final ILogger logger, final IUltimateServiceProvider services, final CfgSmtToolkit csToolkit,
+			final Set<IProgramConst> additionalLiterals) {
 		mLogger = logger;
 		mManagedScript = csToolkit.getManagedScript();
 		mMerge = new VPMergeOperator();

trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/tool/AbstractInterpreter.java

@@ -44,6 +44,7 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgEdge;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocation;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocationIterator;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramConst;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVarOrConst;
 import de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.Activator;
 import de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.algorithm.AbsIntResult;
@@ -195,15 +196,16 @@ private AbstractInterpreter() {
 	 * settings but hardcoded
 	 *
 	 * @param logger
+	 * @param additionalLiterals
 	 *
 	 */
 	public static IAbstractInterpretationResult<EqState, IcfgEdge, IcfgLocation> runFutureEqualityDomain(
 			final IIcfg<?> root, final IProgressAwareTimer timer, final IUltimateServiceProvider services,
-			final boolean isSilent, final ILogger logger) {
+			final boolean isSilent, final ILogger logger, final Set<IProgramConst> additionalLiterals) {
 		final FixpointEngineParameters<EqState, IcfgEdge, IProgramVarOrConst, IcfgLocation> params =
 				new FixpointEngineParameters<>(services, IProgramVarOrConst.class);
 		return runFuture(root, services, logger, isSilent,
-				params.setDomain(FixpointEngineFutureParameterFactory.createEqualityDomain(logger, root, services))
+				params.setDomain(FixpointEngineFutureParameterFactory.createEqualityDomain(logger, root, services, additionalLiterals))
 						.setTimer(timer),
 				p -> new FixpointEngine<>(p));
 	}

trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/tool/initializer/FixpointEngineFutureParameterFactory.java

@@ -2,6 +2,7 @@
 
 import java.util.Collections;
 import java.util.Objects;
+import java.util.Set;
 
 import de.uni_freiburg.informatik.ultimate.core.model.preferences.IPreferenceProvider;
 import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger;
@@ -13,6 +14,7 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfg;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgEdge;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocation;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramConst;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVarOrConst;
 import de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.Activator;
 import de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.algorithm.FixpointEngineParameters;
@@ -111,7 +113,8 @@ FixpointEngineParameters<STATE, IcfgEdge, IProgramVarOrConst, IcfgLocation> addD
 					final ILoopDetector<IcfgEdge> loopDetector) {
 		final ILogger logger = mServices.getLoggingService().getLogger(Activator.PLUGIN_ID);
 		final IAbstractDomain<STATE, IcfgEdge> domain =
-				(IAbstractDomain<STATE, IcfgEdge>) createEqualityDomain(logger, mRoot, mServices);
+				(IAbstractDomain<STATE, IcfgEdge>) createEqualityDomain(logger, mRoot, mServices,
+						Collections.emptySet());
 		final IAbstractStateStorage<STATE, IcfgEdge, IcfgLocation> storageProvider =
 				new IcfgAbstractStateStorageProvider<>(mServices, transitionProvider);
 		final IVariableProvider<STATE, IcfgEdge> variableProvider =
@@ -140,7 +143,8 @@ public static <STATE extends IAbstractState<STATE>> IAbstractDomain<STATE, IcfgE
 		} else if (DataflowDomain.class.getSimpleName().equals(domainName)) {
 			return (IAbstractDomain<STATE, IcfgEdge>) new DataflowDomain<IcfgEdge>(logger);
 		} else if (VPDomain.class.getSimpleName().equals(domainName)) {
-			return (IAbstractDomain<STATE, IcfgEdge>) createEqualityDomain(logger, root, services);
+			return (IAbstractDomain<STATE, IcfgEdge>) createEqualityDomain(logger, root, services,
+					Collections.emptySet());
 		} else if (SMTTheoryDomain.class.getSimpleName().equals(domainName)) {
 			return (IAbstractDomain<STATE, IcfgEdge>) new SMTTheoryDomain(services, root.getCfgSmtToolkit());
 		} else if (LiveVariableDomain.class.getSimpleName().equals(domainName)) {
@@ -161,10 +165,10 @@ IAbstractDomain<STATE, IcfgEdge> selectDomainFutureCfg(final Class<DOM> domain,
 	}
 
 	public static VPDomain<IcfgEdge> createEqualityDomain(final ILogger logger, final IIcfg<?> root,
-			final IUltimateServiceProvider services) {
+			final IUltimateServiceProvider services, final Set<IProgramConst> additionalLiterals) {
 		// final VPTfStateBuilderPreparer tfPreparer =
 		// new VPTfStateBuilderPreparer(preAnalysis, root, logger);
-		return new VPDomain<>(logger, services, root.getCfgSmtToolkit());
+		return new VPDomain<>(logger, services, root.getCfgSmtToolkit(), additionalLiterals);
 	}
 
 	private static String getFailureString(final String selectedDomain) {

trunk/source/IcfgTransformation/src/de/uni_freiburg/informatik/ultimate/plugins/icfgtransformation/AbsIntEqualityProvider.java

@@ -26,6 +26,7 @@
  */
 package de.uni_freiburg.informatik.ultimate.plugins.icfgtransformation;
 
+import java.util.Collection;
 import java.util.HashSet;
 import java.util.Map;
 import java.util.Set;
@@ -38,6 +39,7 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfg;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgEdge;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocation;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramConst;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.equalityanalysis.EqualityAnalysisResult;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.equalityanalysis.IEqualityAnalysisResultProvider;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.equalityanalysis.IEqualityProvidingState;
@@ -58,9 +60,18 @@ public class AbsIntEqualityProvider implements IEqualityAnalysisResultProvider<I
 
 	private boolean mPreprocessed;
 
+	private final Set<IProgramConst> mAdditionalLiterals;
+
 	public AbsIntEqualityProvider(final IUltimateServiceProvider services) {
 		mServices = services;
 		mLogger = services.getLoggingService().getLogger(Activator.PLUGIN_ID);
+
+		mAdditionalLiterals = new HashSet<>();
+	}
+
+	@Override
+	public void announceAdditionalLiterals(final Collection<IProgramConst> literals) {
+		mAdditionalLiterals.addAll(literals);
 	}
 
 	@Override
@@ -69,7 +80,7 @@ public void preprocess(final IIcfg<?> icfg) {
 
 		final IAbstractInterpretationResult<? extends IEqualityProvidingState, IcfgEdge, IcfgLocation> absIntResult =
 				// AbstractInterpreter.runFutureSMTDomain(icfg, timer, mServices, true, mLogger);
-				AbstractInterpreter.runFutureEqualityDomain(icfg, timer, mServices, true, mLogger);
+				AbstractInterpreter.runFutureEqualityDomain(icfg, timer, mServices, true, mLogger, mAdditionalLiterals);
 		final Map<IcfgLocation, ?> loc2states = absIntResult.getLoc2States();
 		mTopState = absIntResult.getUsedDomain().createTopState();
 		mLoc2States = (Map<IcfgLocation, Set<IEqualityProvidingState>>) loc2states;

trunk/source/IcfgTransformation/src/de/uni_freiburg/informatik/ultimate/plugins/icfgtransformation/IcfgTransformationObserver.java

@@ -47,7 +47,7 @@
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.IcfgTransformerSequence;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.LocalTransformer;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.MapEliminationTransformer;
-import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.HeapSepTransFormulaTransformer;
+import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.HeapSepIcfgTransformer;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.loopacceleration.ExampleLoopAccelerationTransformulaTransformer;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.loopacceleration.ahmed.AhmedLoopAccelerationIcfgTransformer;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.loopacceleration.biesenbach.IcfgLoopAcceleration;
@@ -191,40 +191,23 @@ private <INLOC extends IcfgLocation, OUTLOC extends IcfgLocation> IIcfg<OUTLOC>
 		}
 	}
 
-	@SuppressWarnings("unchecked")
 	private <INLOC extends IcfgLocation, OUTLOC extends IcfgLocation> IIcfg<OUTLOC> applyHeapSeparator(
 			final IIcfg<INLOC> icfg, final ILocationFactory<INLOC, OUTLOC> locFac, final Class<OUTLOC> outlocClass,
 			final IBacktranslationTracker backtranslationTracker, final ReplacementVarFactory fac,
 			final IUltimateServiceProvider services,
 			final IEqualityAnalysisResultProvider<IcfgLocation, IIcfg<?>> equalityProvider) {
 
-//		final List<ITransformulaTransformer> transformers = new ArrayList<>();
-//
-//		final ArrayIndexExposer sie = new ArrayIndexExposer(icfg.getCfgSmtToolkit());
-//		transformers.add(sie);
-//
-//		final HeapSepTransFormulaTransformer hstftf =
-//				new HeapSepTransFormulaTransformer(icfg.getCfgSmtToolkit(), mServices, equalityProvider);
-//		transformers.add(hstftf);
-//
-//		final IcfgTransformerSequence<INLOC, OUTLOC> transformerSequence = new IcfgTransformerSequence<>(icfg, locFac,
-//				(ILocationFactory<OUTLOC, OUTLOC>) locFac, backtranslationTracker, outlocClass,
-//				icfg.getIdentifier() + "HeapSeparatorResult", transformers);
-
-		final HeapSepTransFormulaTransformer hstftf =
-				new HeapSepTransFormulaTransformer(icfg.getCfgSmtToolkit(), mServices, equalityProvider);
-
-		 final IcfgTransformer<INLOC, OUTLOC> icfgTransformer =
-				 new IcfgTransformer<>(icfg, locFac, backtranslationTracker, outlocClass, "IcfgWithHeapSeparation",
-				 hstftf);
+		final HeapSepIcfgTransformer<INLOC, OUTLOC> icfgTransformer =
+				new HeapSepIcfgTransformer<>(icfg, locFac, backtranslationTracker, outlocClass, "heap_separated_icfg",
+						equalityProvider);
 
 		mServices.getResultService().reportResult(Activator.PLUGIN_ID, new GenericResult(Activator.PLUGIN_ID,
-				"HeapSeparationSummary", hstftf.getHeapSeparationSummary(), Severity.INFO));
+				"HeapSeparationSummary", icfgTransformer.getHeapSeparationSummary(), Severity.INFO));
 		mServices.getResultService().reportResult(Activator.PLUGIN_ID,
-				new StatisticsResult<>(Activator.PLUGIN_ID, "HeapSeparatorStatistics", hstftf.getStatistics()));
+				new StatisticsResult<>(Activator.PLUGIN_ID, "HeapSeparatorStatistics",
+						icfgTransformer.getStatistics()));
 
 		return icfgTransformer.getResult();
-//		return transformerSequence.getResult();
 	}
 
 	private <INLOC extends IcfgLocation, OUTLOC extends IcfgLocation> IIcfg<OUTLOC> applyLoopAccelerationAhmed(

trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/IcfgTransitionTransformer.java

@@ -2,18 +2,23 @@
 
 import java.util.ArrayList;
 import java.util.List;
+import java.util.Map;
 
 import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.loopacceleration.ExampleLoopAccelerationTransformulaTransformer;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.BasicIcfg;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.CfgSmtToolkit;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfg;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfgReturnTransition;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgCallTransition;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgEdge;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgEdgeFactory;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgInternalTransition;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocation;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocationIterator;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgReturnTransition;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.transformations.ReplacementVarFactory;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.transitions.UnmodifiableTransFormula;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.managedscript.ManagedScript;
 import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple;
 
@@ -25,40 +30,51 @@
  * @param <OUTLOC>
  */
 public abstract class IcfgTransitionTransformer<INLOC extends IcfgLocation, OUTLOC extends IcfgLocation>
-	implements IIcfgTransformer<OUTLOC> {
+		implements IIcfgTransformer<OUTLOC> {
 
-	protected final CfgSmtToolkit mCsToolkit;
+	protected final CfgSmtToolkit mInputCfgCsToolkit;
 
 	protected final IcfgEdgeFactory mEdgeFactory;
 	protected final ManagedScript mMgdScript;
 	protected final ILogger mLogger;
 
-	private final IIcfg<INLOC> mInputIcfg;
+	/**
+	 * TODO: it is important that any override of transform updates this map! (not nice, as it is now..)
+	 */
+	protected Map<IcfgCallTransition, IcfgCallTransition> mOldCallToNewCall;
+
+	protected final IIcfg<INLOC> mInputIcfg;
 
 	private final TransformedIcfgBuilder<INLOC, OUTLOC> mTransformedIcfgBuilder;
 	private final BasicIcfg<OUTLOC> mResult;
 
-	public IcfgTransitionTransformer(final ILogger logger, final CfgSmtToolkit csToolkit, final String resultName,
-			final Class<OUTLOC> outLocClazz, final IIcfg<INLOC> inputCfg, final ILocationFactory<INLOC, OUTLOC> funLocFac,
+	public IcfgTransitionTransformer(final ILogger logger, final String resultName,
+			final Class<OUTLOC> outLocClazz, final IIcfg<INLOC> inputCfg,
+			final ILocationFactory<INLOC, OUTLOC> funLocFac,
 			final IBacktranslationTracker backtranslationTracker) {
-		mCsToolkit = csToolkit;
+		mInputCfgCsToolkit = inputCfg.getCfgSmtToolkit();
 		mLogger = logger;
 		mInputIcfg = inputCfg;
 
-		mMgdScript = csToolkit.getManagedScript();
-		mEdgeFactory = csToolkit.getIcfgEdgeFactory();
+		mMgdScript = mInputCfgCsToolkit.getManagedScript();
+		mEdgeFactory = mInputCfgCsToolkit.getIcfgEdgeFactory();
 
-		mResult = new BasicIcfg<>(resultName, mCsToolkit, outLocClazz);
+		/*
+		 * the csToolkit will be replaced in mResult by mTransformedIcfgBuilder.finish() (not a fan of this solution..)
+		 * the new csToolkit constructed there will get a new symbol table, too..
+		 */
+		mResult = new BasicIcfg<>(resultName, mInputCfgCsToolkit, outLocClazz);
 
 		final ITransformulaTransformer noopTransformer =
-				new ExampleLoopAccelerationTransformulaTransformer(mLogger, mCsToolkit.getManagedScript(),
-						mCsToolkit.getSymbolTable(), new ReplacementVarFactory(mCsToolkit, false));
+				new ExampleLoopAccelerationTransformulaTransformer(mLogger, mInputCfgCsToolkit.getManagedScript(),
+						mInputCfgCsToolkit.getSymbolTable(), new ReplacementVarFactory(mInputCfgCsToolkit, false));
 		mTransformedIcfgBuilder = new TransformedIcfgBuilder<>(funLocFac,
 				backtranslationTracker, noopTransformer, mInputIcfg, mResult);
-		computeResult();
+		processGraph();
+		mTransformedIcfgBuilder.finish();
 	}
 
-	private void computeResult() {
+	private void processGraph() {
 		// we need to create new return transitions after new call transitions have been created
 		final List<Triple<OUTLOC, OUTLOC, IcfgEdge>> rtrTransitions = new ArrayList<>();
 
@@ -84,8 +100,48 @@ private void computeResult() {
 				a -> mTransformedIcfgBuilder.createNewTransition(a.getFirst(), a.getSecond(), a.getThird()));
 	}
 
-	protected abstract IcfgEdge transform(IcfgEdge oldTransition, OUTLOC newSource, OUTLOC newTarget);
+	/**
+	 * Creates a new edge from newSource to newTarget with the unchanged transformula from the input icfg.
+	 *
+	 * @param oldTransition
+	 * @param newSource
+	 * @param newTarget
+	 * @return
+	 */
+	protected IcfgEdge transform(final IcfgEdge oldTransition, final OUTLOC newSource, final OUTLOC newTarget) {
+		final UnmodifiableTransFormula newTransformula = oldTransition.getTransformula();
+		return transform(oldTransition, newSource, newTarget, newTransformula);
+	}
 
+	/**
+	 *
+	 * @param oldTransition
+	 * @param newSource
+	 * @param newTarget
+	 * @param newTransformula
+	 * @return
+	 */
+	protected IcfgEdge transform(final IcfgEdge oldTransition, final OUTLOC newSource, final OUTLOC newTarget,
+			final UnmodifiableTransFormula newTransformula) {
+		if (oldTransition instanceof IcfgInternalTransition) {
+			// TODO: is this the right payload?
+			return mEdgeFactory.createInternalTransition(newSource, newTarget, oldTransition.getPayload(),
+					newTransformula);
+		} else if (oldTransition instanceof IcfgCallTransition) {
+			final IcfgCallTransition newCallTransition = mEdgeFactory.createCallTransition(newSource, newTarget,
+					oldTransition.getPayload(), newTransformula);
+			mOldCallToNewCall.put((IcfgCallTransition) oldTransition, newCallTransition);
+			return newCallTransition;
+		} else if (oldTransition instanceof IcfgReturnTransition) {
+			final IcfgCallTransition correspondingNewCall =
+					mOldCallToNewCall.get(((IcfgReturnTransition) oldTransition).getCorrespondingCall());
+			assert correspondingNewCall != null;
+			return mEdgeFactory.createReturnTransition(newSource, newTarget, correspondingNewCall,
+					oldTransition.getPayload(), newTransformula, correspondingNewCall.getLocalVarsAssignment());
+		} else {
+			throw new IllegalArgumentException("unknown transition type");
+		}
+	}
 
 	@Override
 	public final IIcfg<OUTLOC> getResult() {

trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/TransformedIcfgBuilder.java

@@ -72,6 +72,9 @@
  * The {@link TransformedIcfgBuilder} constructs and adds locations and transitions to a {@link BasicIcfg} based on some
  * input {@link IIcfg}.
  *
+ * (Alexander Nutz:) Note that the symbol table is updated automatically according to new program variables or constants
+ *  that occur in the newly created TransFormulas.
+ *
  * @author Daniel Dietsch (dietsch@informatik.uni-freiburg.de)
  *
  * @param <INLOC>