From 15f660106a4b82546714a0f42bd4a4d085baea30 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 3 Mar 2015 15:21:15 +0100
Subject: [PATCH] no-xlang checking phase
---
src/main/scala/leon/Main.scala | 9 +++-
.../leon/xlang/NoXlangFeaturesChecking.scala | 51 +++++++++++++++++++
.../purescala/error/Asserts.scala | 16 ++++++
.../PureScalaVerificationRegression.scala | 5 +-
4 files changed, 78 insertions(+), 3 deletions(-)
create mode 100644 src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala
create mode 100644 src/test/resources/regression/verification/purescala/error/Asserts.scala
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 49ab85e95..46b37eaf6 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -211,9 +211,16 @@ object Main {
import verification.AnalysisPhase
import repair.RepairPhase
+ val pipeSanityCheck : Pipeline[Program, Program] =
+ if(!settings.xlang)
+ xlang.NoXlangFeaturesChecking
+ else
+ NoopPhase()
+
val pipeBegin : Pipeline[List[String],Program] =
ExtractionPhase andThen
- PreprocessingPhase
+ PreprocessingPhase andThen
+ pipeSanityCheck
val pipeProcess: Pipeline[Program, Any] = {
if (settings.synthesis) {
diff --git a/src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala b/src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala
new file mode 100644
index 000000000..2bc7d702e
--- /dev/null
+++ b/src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala
@@ -0,0 +1,51 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package xlang
+
+import purescala.Common._
+import purescala.TypeTrees._
+import purescala.Trees._
+import purescala.Definitions._
+import purescala.Constructors._
+
+import purescala.TreeOps.exists
+import xlang.Trees._
+
+object NoXlangFeaturesChecking extends UnitPhase[Program] {
+
+ val name = "no-xlang"
+ val description = "Ensure and enforce that no xlang features are used"
+
+ private def isXlangExpr(expr: Expr): Boolean = expr match {
+
+ case Block(_, _) => true
+
+ case Assignment(_, _) => true
+
+ case While(_, _) => true
+
+ case Epsilon(_, _) => true
+
+ case EpsilonVariable(_, _) => true
+
+ case LetVar(_, _, _) => true
+
+ case Waypoint(_, _, _) => true
+
+ case ArrayUpdate(_, _, _) => true
+
+ case _ => false
+
+ }
+
+ override def apply(ctx: LeonContext, pgm: Program): Unit = {
+ pgm.definedFunctions.foreach(fd => {
+ if(exists(isXlangExpr)(fd.fullBody)) {
+ ctx.reporter.fatalError(fd.fullBody.getPos, "Expr is using xlang features")
+ }
+ })
+ }
+
+}
+
diff --git a/src/test/resources/regression/verification/purescala/error/Asserts.scala b/src/test/resources/regression/verification/purescala/error/Asserts.scala
new file mode 100644
index 000000000..e19e8f282
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/error/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 71148aa5d..b4f119ad8 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -23,8 +23,9 @@ class PureScalaVerificationRegression extends LeonTestSuite {
private case class Output(report : VerificationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String], VerificationReport] =
- ExtractionPhase andThen
- PreprocessingPhase andThen
+ ExtractionPhase andThen
+ PreprocessingPhase andThen
+ xlang.NoXlangFeaturesChecking andThen
AnalysisPhase
private def mkTest(file : File, leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = {
--
GitLab