From e7ad02a58b579ed777924839642f7feafdd1b986 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 24 Feb 2015 18:21:14 +0100
Subject: [PATCH] front-end only accepts != with comparable types
---
.../leon/frontends/scalac/ASTExtractors.scala | 7 ++++++
.../frontends/scalac/CodeExtraction.scala | 22 ++++++++++++++++---
.../purescala/error/NotEquals.scala | 8 +++++++
.../purescala/valid/Rational.scala | 19 ++++++++++++++++
4 files changed, 53 insertions(+), 3 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/error/NotEquals.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/Rational.scala
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index edd9e7dc8..b37fd59a6 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -736,6 +736,13 @@ trait ASTExtractors {
}
}
+ object ExNotEquals {
+ def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
+ case Apply(Select(lhs, n), List(rhs)) if (n == nme.NE) => Some((lhs,rhs))
+ case _ => None
+ }
+ }
+
object ExUMinus {
def unapply(tree: Select): Option[Tree] = tree match {
case Select(t, n) if (n == nme.UNARY_- && hasBigIntType(t)) => Some(t)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 67126c0d5..86d7247ef 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1332,6 +1332,25 @@ trait CodeExtraction extends ASTExtractors {
case ExBVUMinus(e) => BVUMinus(extractTree(e))
case ExBVNot(e) => BVNot(extractTree(e))
+ case ExNotEquals(l, r) => {
+ val rl = extractTree(l)
+ val rr = extractTree(r)
+
+ (rl, rr) match {
+ case (IsTyped(_, rt), IsTyped(_, lt)) if isSubtypeOf(rt, lt) || isSubtypeOf(lt, rt) =>
+ Not(Equals(rl, rr))
+
+ case (IntLiteral(v), IsTyped(_, IntegerType)) =>
+ Not(Equals(InfiniteIntegerLiteral(v), rr))
+
+ case (IsTyped(_, IntegerType), IntLiteral(v)) =>
+ Not(Equals(rl, InfiniteIntegerLiteral(v)))
+
+ case (IsTyped(_, rt), IsTyped(_, lt)) =>
+ outOfSubsetError(tr, "Invalid comparison: (_: "+rt+") != (_: "+lt+")")
+ }
+ }
+
case ExEquals(l, r) =>
val rl = extractTree(l)
val rr = extractTree(r)
@@ -1521,9 +1540,6 @@ trait CodeExtraction extends ASTExtractors {
CaseClassSelector(cct, rec, fieldID)
- case (a1, "!=", List(a2)) =>
- Not(Equals(a1, a2))
-
//BigInt methods
case (IsTyped(a1, IntegerType), "+", List(IsTyped(a2, IntegerType))) =>
Plus(a1, a2)
diff --git a/src/test/resources/regression/verification/purescala/error/NotEquals.scala b/src/test/resources/regression/verification/purescala/error/NotEquals.scala
new file mode 100644
index 000000000..af102929e
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/error/NotEquals.scala
@@ -0,0 +1,8 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object NotEquals {
+
+ //should not pass front-end
+ def isDifferent(x: Int, s: String): Boolean = x != s
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/Rational.scala b/src/test/resources/regression/verification/purescala/valid/Rational.scala
new file mode 100644
index 000000000..4979d970a
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Rational.scala
@@ -0,0 +1,19 @@
+import leon.annotation._
+import leon.lang._
+
+object Rationals {
+ // Represents n/d
+ case class Q(n: BigInt, d: BigInt)
+
+ def +(a: Q, b: Q) = {
+ require(isRational(a) && isRational(b))
+
+ Q(a.n*b.d + b.n*a.d, a.d*b.d)
+ } ensuring {
+ isRational(_)
+ }
+
+ //def isRational(a: Q) = a.d != 0
+ def isRational(a: Q) = a.d != 0
+
+}
--
GitLab