From c2179e1354a2f4f1ede0f905d2fb3e2ccba0c056 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 20 Feb 2015 15:51:35 +0100
Subject: [PATCH] cleaner BigInt extractor front-end
---
.../scala/leon/frontends/scalac/ASTExtractors.scala | 6 +++---
.../scala/leon/frontends/scalac/CodeExtraction.scala | 7 ++++---
src/main/scala/leon/purescala/Trees.scala | 4 ----
.../verification/purescala/error/ConvertBigInt.scala | 7 +++++++
.../verification/purescala/error/LiteralBigInt.scala | 7 +++++++
.../verification/purescala/valid/FoolProofAdder.scala | 11 +++++++++++
6 files changed, 32 insertions(+), 10 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/error/ConvertBigInt.scala
create mode 100644 src/test/resources/regression/verification/purescala/error/LiteralBigInt.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/FoolProofAdder.scala
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index dfd099bcc..edd9e7dc8 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -220,9 +220,9 @@ trait ASTExtractors {
}
object ExBigIntLiteral {
- def unapply(tree: Tree): Option[Int] = tree match {
- case Apply(ExSelected("scala", "package", "BigInt", "apply"), (n: Literal) :: Nil) =>
- Some(n.value.intValue)
+ def unapply(tree: Tree): Option[Tree] = tree match {
+ case Apply(ExSelected("scala", "package", "BigInt", "apply"), n :: Nil) =>
+ Some(n)
case _ =>
None
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 7acbe7175..13aefc5b7 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1204,9 +1204,10 @@ trait CodeExtraction extends ASTExtractors {
val newValueRec = extractTree(newValue)
ArrayUpdate(lhsRec, indexRec, newValueRec)
- case ExBigIntLiteral(n) => {
- InfiniteIntegerLiteral(BigInt(n))
+ case ExBigIntLiteral(n: Literal) => {
+ InfiniteIntegerLiteral(BigInt(n.value.stringValue))
}
+ case ExBigIntLiteral(n) => outOfSubsetError(tr, "Non-literal BigInt constructor")
case ExIntToBigInt(tree) => {
val rec = extractTree(tree)
@@ -1214,7 +1215,7 @@ trait CodeExtraction extends ASTExtractors {
case IntLiteral(n) =>
InfiniteIntegerLiteral(BigInt(n))
case _ =>
- IntToBigInt(rec)
+ outOfSubsetError(tr, "Conversion from Int to BigInt")
}
}
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 60b6eb3fb..278d66f66 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -394,10 +394,6 @@ object Trees {
val getType = Int32Type
}
- case class IntToBigInt(expr: Expr) extends Expr {
- val getType = Int32Type
- }
-
/* Set expressions */
case class FiniteSet(elements: Set[Expr]) extends Expr with MutableTyped {
val tpe = if (elements.isEmpty) None else leastUpperBound(elements.toSeq.map(_.getType))
diff --git a/src/test/resources/regression/verification/purescala/error/ConvertBigInt.scala b/src/test/resources/regression/verification/purescala/error/ConvertBigInt.scala
new file mode 100644
index 000000000..41e209a10
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/error/ConvertBigInt.scala
@@ -0,0 +1,7 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object ConvertBigInt {
+
+ def safeInt(x: Int): BigInt = x
+
+}
diff --git a/src/test/resources/regression/verification/purescala/error/LiteralBigInt.scala b/src/test/resources/regression/verification/purescala/error/LiteralBigInt.scala
new file mode 100644
index 000000000..67783edc8
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/error/LiteralBigInt.scala
@@ -0,0 +1,7 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object LiteralBigInt {
+
+ def safeInt(x: Int): BigInt = BigInt(x)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/FoolProofAdder.scala b/src/test/resources/regression/verification/purescala/valid/FoolProofAdder.scala
new file mode 100644
index 000000000..4fd46f85f
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/FoolProofAdder.scala
@@ -0,0 +1,11 @@
+import leon.annotation._
+import leon.lang._
+
+object FoolProofAdder {
+
+ def foolProofAdder(x: BigInt): BigInt = {
+ require(x > 0)
+ x + BigInt(999999) + BigInt("999999999999999")
+ } ensuring(_ > 0)
+
+}
--
GitLab