From f75c49c335b47b5d9bf55286bcf4132ec3a24e2f 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 +- .../stainless/extraction/imperative/AntiAliasing.scala | 9 ++++++++- 2 files changed, 9 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..28a32766a 100644 --- a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala +++ b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala @@ -436,7 +436,14 @@ 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*. + if (isMutableType(nfiType)) { + LetVar(freshRes, nfi, extractResults) + } else { + Let(freshRes, nfi, extractResults) + } } else { nfi }