From b6334653524dffa1b727925ad76c9ffb950a4b00 Mon Sep 17 00:00:00 2001 From: Mario Bucev Date: Mon, 22 Apr 2024 08:20:50 +0200 Subject: [PATCH] AntiAliasing: restore var binding in mapApplication --- .larabot.conf | 2 +- .../extraction/imperative/AntiAliasing.scala | 21 ++++++++++++++++++- 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/.larabot.conf b/.larabot.conf index e5276a448..918de8d56 100644 --- a/.larabot.conf +++ b/.larabot.conf @@ -1,6 +1,6 @@ commands = [ "sbt -batch -Dtestsuite-parallelism=5 test" - "sbt -batch -Dtestsuite-parallelism=3 -Dtestcase-parallelism=5 \"stainless-dotty / IntegrationTest / testOnly stainless.GhostRewriteSuite stainless.GenCSuite stainless.LibrarySuite stainless.verification.VerificationSuite stainless.verification.UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.termination.TerminationSuite stainless.evaluators.EvaluatorComponentTest\"" + "sbt -batch -Dtestsuite-parallelism=3 -Dtestcase-parallelism=5 \"stainless-dotty / IntegrationTest / testOnly stainless.DottyExtractionSuite stainless.GhostRewriteSuite stainless.GenCSuite stainless.LibrarySuite stainless.verification.VerificationSuite stainless.verification.UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.termination.TerminationSuite stainless.evaluators.EvaluatorComponentTest\"" ] nightly { diff --git a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala index a93df2aff..76a74c4bc 100644 --- a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala +++ b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala @@ -256,6 +256,17 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override } // NOTE: `args` must refer to the arguments of the function invocation before transformation (the original args) + // IMPORTANT NOTICE: + // In the `Let` case transformation of `transform`, we need to compute the targets of the transformed binding. + // If this binding happens to contain a function call, the returned targets may be invalid because + // `getTargets` works on functions prior to the AntiAliasing function purification, not after (as it's done it this `Let` case). + // + // It turns out that if we bind the result of the function call to a `var` (for mutable type) the target computation + // will fail which will result in rejection (with the message "Unsupported `val` definition in AntiAliasing"). + // Not doing so will very likely result in a crash later on in unrelated part of the code (due to invalid targets being applied). + // + // To properly fix this, we would need to distinguish pre/post transformation `getTargets` computation, + // which would require significant changes to EffectsAnalyzer. def mapApplication(formalArgs: Seq[ValDef], args: Seq[Expr], nfi: Expr, nfiType: Type, fiEffects: Set[Effect], isOpaqueOrExtern: Boolean, env: Env): Expr = { def affectedBindings(updTarget: Target, isReplacement: Boolean): Map[ValDef, Set[Target]] = { @@ -436,7 +447,15 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override } val extractResults = Block(assgns, TupleSelect(freshRes.toVariable, 1)) - Let(freshRes, nfi, extractResults) + // FIXME: This should be `Let` and not `LetVar`, however doing so will cause a crash in e.g. `MapAliasing1` + // because `getAllTargetsDealiased` in the `Let` case will result in an invalid target due to + // this function not supporting targets computation on function application *post-transformation* + // (see important notice on above). + if (isMutableType(nfiType)) { + LetVar(freshRes, nfi, extractResults) + } else { + Let(freshRes, nfi, extractResults) + } } else { nfi }