From 563fcbfc5d39330ee046a51e0fb2145eb18b9a4b Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 3 Mar 2015 15:52:14 +0100
Subject: [PATCH] xlang does not eliminate side effect in blocks
Function invocation not attached to any value in
a statement block should be kept for potential
side effects. The committed regression test
illustrates the issue.
Additionally, become consistent in the name XLang
in various files of Leon.
---
src/main/scala/leon/Main.scala | 8 ++++----
.../leon/xlang/ImperativeCodeElimination.scala | 12 ++++++++++++
...cking.scala => NoXLangFeaturesChecking.scala} | 2 +-
...lysisPhase.scala => XLangAnalysisPhase.scala} | 2 +-
.../verification/xlang/invalid/Asserts.scala | 16 ++++++++++++++++
.../PureScalaVerificationRegression.scala | 2 +-
.../XLangVerificationRegression.scala | 4 ++--
7 files changed, 37 insertions(+), 9 deletions(-)
rename src/main/scala/leon/xlang/{NoXlangFeaturesChecking.scala => NoXLangFeaturesChecking.scala} (94%)
rename src/main/scala/leon/xlang/{XlangAnalysisPhase.scala => XLangAnalysisPhase.scala} (98%)
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Asserts.scala
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 46b37eaf6..dd177e7e2 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -18,7 +18,7 @@ object Main {
xlang.EpsilonElimination,
xlang.ImperativeCodeElimination,
purescala.FunctionClosure,
- xlang.XlangAnalysisPhase,
+ xlang.XLangAnalysisPhase,
synthesis.SynthesisPhase,
termination.TerminationPhase,
verification.AnalysisPhase,
@@ -207,13 +207,13 @@ object Main {
import frontends.scalac.ExtractionPhase
import synthesis.SynthesisPhase
import termination.TerminationPhase
- import xlang.XlangAnalysisPhase
+ import xlang.XLangAnalysisPhase
import verification.AnalysisPhase
import repair.RepairPhase
val pipeSanityCheck : Pipeline[Program, Program] =
if(!settings.xlang)
- xlang.NoXlangFeaturesChecking
+ xlang.NoXLangFeaturesChecking
else
NoopPhase()
@@ -230,7 +230,7 @@ object Main {
} else if (settings.termination) {
TerminationPhase
} else if (settings.xlang) {
- XlangAnalysisPhase
+ XLangAnalysisPhase
} else if (settings.verify) {
purescala.FunctionClosure andThen AnalysisPhase
} else {
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 1be1f99ab..a7de9904e 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -254,6 +254,17 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
//Recall that Choose cannot mutate variables from the scope
(c, (b2: Expr) => b2, Map())
}
+
+ case i @ FunctionInvocation(fd, args) =>
+ //function invocation can have side effects so we should keep them as local
+ //val names.
+ val scope = (body: Expr) => {
+ Let(FreshIdentifier("tmp", fd.returnType),
+ i,
+ body)
+ }
+ (i, scope, Map())
+
case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
case n @ NAryOperator(args, recons) => {
val (recArgs, scope, fun) = args.foldRight((Seq[Expr](), (body: Expr) => body, Map[Identifier, Identifier]()))((arg, acc) => {
@@ -278,6 +289,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val (argVal, argScope, argFun) = toFunction(a)
(recons(argVal).copiedFrom(u), argScope, argFun)
}
+
case (t: Terminal) => (t, (body: Expr) => body, Map())
diff --git a/src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
similarity index 94%
rename from src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala
rename to src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
index 2bc7d702e..08425aada 100644
--- a/src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala
+++ b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
@@ -12,7 +12,7 @@ import purescala.Constructors._
import purescala.TreeOps.exists
import xlang.Trees._
-object NoXlangFeaturesChecking extends UnitPhase[Program] {
+object NoXLangFeaturesChecking extends UnitPhase[Program] {
val name = "no-xlang"
val description = "Ensure and enforce that no xlang features are used"
diff --git a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
similarity index 98%
rename from src/main/scala/leon/xlang/XlangAnalysisPhase.scala
rename to src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index 03c8d2e71..ff8e5a34c 100644
--- a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -6,7 +6,7 @@ package xlang
import leon.purescala.Definitions._
import leon.verification._
-object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
+object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
val name = "xlang analysis"
val description = "apply analysis on xlang"
diff --git a/src/test/resources/regression/verification/xlang/invalid/Asserts.scala b/src/test/resources/regression/verification/xlang/invalid/Asserts.scala
new file mode 100644
index 000000000..e19e8f282
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Asserts.scala
@@ -0,0 +1,16 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang._
+
+object Asserts {
+
+ def assert1(i: BigInt): BigInt = { // we might define assert like so
+ require(i >= 0)
+ i
+ }
+
+ def sum(to: BigInt): BigInt = {
+ assert1(to)
+ to
+ }
+}
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index b4f119ad8..0be138d6d 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -25,7 +25,7 @@ class PureScalaVerificationRegression extends LeonTestSuite {
private def mkPipeline : Pipeline[List[String], VerificationReport] =
ExtractionPhase andThen
PreprocessingPhase andThen
- xlang.NoXlangFeaturesChecking andThen
+ xlang.NoXLangFeaturesChecking andThen
AnalysisPhase
private def mkTest(file : File, leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = {
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index 680948c28..5569f6c57 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -6,7 +6,7 @@ import leon._
import leon.test._
import leon.verification.VerificationReport
-import leon.xlang.XlangAnalysisPhase
+import leon.xlang.XLangAnalysisPhase
import leon.frontends.scalac.ExtractionPhase
import leon.utils.PreprocessingPhase
@@ -23,7 +23,7 @@ class XLangVerificationRegression extends LeonTestSuite {
private def mkPipeline : Pipeline[List[String],VerificationReport] =
ExtractionPhase andThen
PreprocessingPhase andThen
- XlangAnalysisPhase
+ XLangAnalysisPhase
private def mkTest(file : File, forError: Boolean = false)(block: Output=>Unit) = {
val fullName = file.getPath()
--
GitLab