From 673f4faebd6bcc0c797a2c16539edf354bb685df Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 26 May 2015 15:44:07 +0200
Subject: [PATCH] fix codegen evaluator for Modulo
---
.../java/leon/codegen/runtime/BigInt.java | 4 ++
.../scala/leon/codegen/CodeGeneration.scala | 3 +-
.../test/evaluators/EvaluatorsTests.scala | 43 +++++++++++++++++++
3 files changed, 49 insertions(+), 1 deletion(-)
diff --git a/src/main/java/leon/codegen/runtime/BigInt.java b/src/main/java/leon/codegen/runtime/BigInt.java
index 03f12972c..83de0fbb4 100644
--- a/src/main/java/leon/codegen/runtime/BigInt.java
+++ b/src/main/java/leon/codegen/runtime/BigInt.java
@@ -35,6 +35,10 @@ public final class BigInt {
return new BigInt(_underlying.divide(that.underlying()));
}
+ public BigInt rem(BigInt that) {
+ return new BigInt(_underlying.remainder(that.underlying()));
+ }
+
public BigInt mod(BigInt that) {
return new BigInt(_underlying.mod(that.underlying()));
}
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 34cd1a9db..1d5dee8b4 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -644,10 +644,11 @@ trait CodeGeneration {
mkExpr(r, ch)
ch << InvokeVirtual(BigIntClass, "div", s"(L$BigIntClass;)L$BigIntClass;")
+ //Modulo in Leon corresponds to the "rem" operator on java/Scala BigInt
case Modulo(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << InvokeVirtual(BigIntClass, "mod", s"(L$BigIntClass;)L$BigIntClass;")
+ ch << InvokeVirtual(BigIntClass, "rem", s"(L$BigIntClass;)L$BigIntClass;")
case UMinus(e) =>
mkExpr(e, ch)
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 81eee7077..9c4418137 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -161,6 +161,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
private def T = BooleanLiteral(true)
private def F = BooleanLiteral(false)
private def IL(i : Int) = IntLiteral(i)
+ private def BIL(i : Int) = InfiniteIntegerLiteral(i)
test("Arithmetic") {
val p = """|object Program {
@@ -195,6 +196,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
checkComp(e, mkCall("mod", IL(7), IL(-5)), IL(2))
checkComp(e, mkCall("mod", IL(-7), IL(5)), IL(-2))
checkComp(e, mkCall("mod", IL(-7), IL(-5)), IL(-2))
+ checkComp(e, mkCall("mod", IL(-1), IL(5)), IL(-1))
// Things that should crash.
checkError(e, mkCall("div", IL(42), IL(0)))
@@ -202,6 +204,47 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
}
}
+ test("BigInt Arithmetic") {
+ val p = """|object Program {
+ | def plus(x : BigInt, y : BigInt) : BigInt = x + y
+ | def max(x : BigInt, y : BigInt) : BigInt = if(x >= y) x else y
+ | def square(i : BigInt) : BigInt = { val j = i; j * i }
+ | def abs(i : BigInt) : BigInt = if(i < 0) -i else i
+ | def intSqrt(n : BigInt) : BigInt = intSqrt0(abs(n), 0)
+ | def intSqrt0(n : BigInt, c : BigInt) : BigInt = {
+ | val s = square(c+1)
+ | if(s > n) c else intSqrt0(n, c+1)
+ | }
+ | def div(x : BigInt, y : BigInt) : BigInt = (x / y)
+ | def mod(x : BigInt, y : BigInt) : BigInt = (x % y)
+ |}
+ |""".stripMargin
+
+ implicit val prog = parseString(p)
+ val evaluators = prepareEvaluators
+
+ for(e <- evaluators) {
+ // Some simple math.
+ checkComp(e, mkCall("plus", BIL(60), UMinus(BIL(18))), BIL(42))
+ checkComp(e, mkCall("max", BIL(4), BIL(42)), BIL(42))
+ checkComp(e, mkCall("max", BIL(42), UMinus(BIL(42))), BIL(42))
+ checkComp(e, mkCall("intSqrt", UMinus(BIL(1800))), BIL(42))
+ checkComp(e, mkCall("div", BIL(7), BIL(5)), BIL(1))
+ checkComp(e, mkCall("div", BIL(7), BIL(-5)), BIL(-1))
+ checkComp(e, mkCall("div", BIL(-7), BIL(5)), BIL(-1))
+ checkComp(e, mkCall("div", BIL(-7), BIL(-5)), BIL(1))
+ checkComp(e, mkCall("mod", BIL(7), BIL(5)), BIL(2))
+ checkComp(e, mkCall("mod", BIL(7), BIL(-5)), BIL(2))
+ checkComp(e, mkCall("mod", BIL(-7), BIL(5)), BIL(-2))
+ checkComp(e, mkCall("mod", BIL(-7), BIL(-5)), BIL(-2))
+ checkComp(e, mkCall("mod", BIL(-1), BIL(5)), BIL(-1))
+
+ // Things that should crash.
+ checkError(e, mkCall("div", BIL(42), BIL(0)))
+ checkError(e, mkCall("mod", BIL(42), BIL(0)))
+ }
+ }
+
test("Booleans") {
val p = """|object Program {
|def and1(x : Boolean, y : Boolean) : Boolean = x && y
--
GitLab