From 41a7ba30477b72196d97da1d7e43ab2e875816cc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Mon, 7 May 2012 14:19:20 +0200
Subject: [PATCH] improve verification of the correctness of the tree

---
 src/main/scala/leon/Main.scala                  |  1 +
 src/main/scala/leon/plugin/CodeExtraction.scala |  4 ++++
 src/main/scala/leon/purescala/Definitions.scala |  1 +
 src/main/scala/leon/purescala/Trees.scala       | 11 ++++++++++-
 4 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 68161e9e4..b532c2e7c 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -34,6 +34,7 @@ object Main {
     Logger.debug("Default action on program: " + program, 3, "main")
     val passManager = new PassManager(Seq(ArrayTransformation, EpsilonElimination, ImperativeCodeElimination, /*UnitElimination,*/ FunctionClosure, FunctionHoisting, Simplificator))
     val program2 = passManager.run(program)
+    assert(program2.isPure)
     val analysis = new Analysis(program2, reporter)
     analysis.analyse
   }
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 6b9ef14e5..70ad6d68f 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -830,6 +830,10 @@ trait CodeExtraction extends Extractors {
         }
         case ExIfThenElse(t1,t2,t3) => {
           val r1 = rec(t1)
+          if(containsLetDef(r1)) {
+            unit.error(t1.pos, "Condition of if-then-else expression should not contain nested function definition")
+            throw ImpureCodeEncounteredException(t1)
+          }
           val r2 = rec(t2)
           val r3 = rec(t3)
           IfExpr(r1, r2, r3).setType(leastUpperBound(r2.getType, r3.getType))
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index df83d6b19..f73530c40 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -53,6 +53,7 @@ object Definitions {
     def isCatamorphism(f1: FunDef) = mainObject.isCatamorphism(f1)
     def caseClassDef(name: String) = mainObject.caseClassDef(name)
     def allIdentifiers : Set[Identifier] = mainObject.allIdentifiers + id
+    def isPure: Boolean = definedFunctions.forall(fd => fd.body.forall(Trees.isPure) && fd.precondition.forall(Trees.isPure) && fd.postcondition.forall(Trees.isPure))
   }
 
   /** Objects work as containers for class definitions, functions (def's) and
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 93bf6fd97..5dc158b42 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -816,13 +816,18 @@ object Trees {
     searchAndReplaceDFS(applyToTree)(expr)
   }
 
-  //checking whether the expr is pure, that is do not contains any non-pure construct: assign, while and blocks
+  //checking whether the expr is pure, that is do not contains any non-pure construct: assign, while, blocks, array, ...
+  //this is expected to be true when entering the "backend" of Leon
   def isPure(expr: Expr): Boolean = {
     def convert(t: Expr) : Boolean = t match {
       case Block(_, _) => false
       case Assignment(_, _) => false
       case While(_, _) => false
       case LetVar(_, _, _) => false
+      case LetDef(_, _) => false
+      case ArrayUpdate(_, _, _) => false
+      case ArrayFill(_, _) => false
+      case Epsilon(_) => false
       case _ => true
     }
     def combine(b1: Boolean, b2: Boolean) = b1 && b2
@@ -831,6 +836,10 @@ object Trees {
       case Assignment(_, _) => false
       case While(_, _) => false
       case LetVar(_, _, _) => false
+      case LetDef(_, _) => false
+      case ArrayUpdate(_, _, _) => false
+      case ArrayFill(_, _) => false
+      case Epsilon(_) => false
       case _ => b
     }
     treeCatamorphism(convert, combine, compute, expr)
-- 
GitLab