From a083e33535ff0d364634b313945f58b59d4fb412 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 20 Feb 2015 18:55:08 +0100
Subject: [PATCH] implement BigInt code generation
---
.../java/leon/codegen/runtime/BigInt.java | 82 ++++++++++++++++++
.../scala/leon/codegen/CodeGeneration.scala | 85 ++++++++++++-------
.../scala/leon/codegen/CompilationUnit.scala | 12 +--
.../leon/test/codegen/CodeGenTests.scala | 76 ++++++++++++++++-
4 files changed, 217 insertions(+), 38 deletions(-)
create mode 100644 src/main/java/leon/codegen/runtime/BigInt.java
diff --git a/src/main/java/leon/codegen/runtime/BigInt.java b/src/main/java/leon/codegen/runtime/BigInt.java
new file mode 100644
index 000000000..7506b70b7
--- /dev/null
+++ b/src/main/java/leon/codegen/runtime/BigInt.java
@@ -0,0 +1,82 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+package leon.codegen.runtime;
+
+import java.math.BigInteger;
+
+public final class BigInt {
+
+ private final BigInteger _underlying;
+
+ public final BigInteger underlying() {
+ return _underlying;
+ }
+
+ private BigInt(BigInteger value) {
+ _underlying = value;
+ }
+ public BigInt(String value) {
+ _underlying = new BigInteger(value);
+ }
+
+ public BigInt add(BigInt that) {
+ return new BigInt(_underlying.add(that.underlying()));
+ }
+
+ public BigInt sub(BigInt that) {
+ return new BigInt(_underlying.subtract(that.underlying()));
+ }
+
+ public BigInt mult(BigInt that) {
+ return new BigInt(_underlying.multiply(that.underlying()));
+ }
+
+ public BigInt div(BigInt that) {
+ return new BigInt(_underlying.divide(that.underlying()));
+ }
+
+ public BigInt mod(BigInt that) {
+ return new BigInt(_underlying.mod(that.underlying()));
+ }
+
+ public BigInt neg() {
+ return new BigInt(_underlying.negate());
+ }
+
+
+ public boolean lessThan(BigInt that) {
+ return _underlying.compareTo(that.underlying()) < 0;
+ }
+
+ public boolean lessEquals(BigInt that) {
+ return _underlying.compareTo(that.underlying()) <= 0;
+ }
+
+ public boolean greaterThan(BigInt that) {
+ return _underlying.compareTo(that.underlying()) > 0;
+ }
+
+ public boolean greaterEquals(BigInt that) {
+ return _underlying.compareTo(that.underlying()) >= 0;
+ }
+
+
+ @Override
+ public boolean equals(Object that) {
+ if(that == this) return true;
+ if(!(that instanceof BigInt)) return false;
+
+ BigInt other = (BigInt)that;
+ return this.underlying().equals(other.underlying());
+ }
+
+ @Override
+ public String toString() {
+ return _underlying.toString();
+ }
+
+ @Override
+ public int hashCode() {
+ return _underlying.hashCode();
+ }
+
+}
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 75e15d5ac..bfea7dabe 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -66,6 +66,7 @@ trait CodeGeneration {
private[codegen] val TupleClass = "leon/codegen/runtime/Tuple"
private[codegen] val SetClass = "leon/codegen/runtime/Set"
private[codegen] val MapClass = "leon/codegen/runtime/Map"
+ private[codegen] val BigIntClass = "leon/codegen/runtime/BigInt"
private[codegen] val CaseClassClass = "leon/codegen/runtime/CaseClass"
private[codegen] val LambdaClass = "leon/codegen/runtime/Lambda"
private[codegen] val ErrorClass = "leon/codegen/runtime/LeonCodeGenRuntimeException"
@@ -84,7 +85,6 @@ trait CodeGeneration {
/** Return the respective JVM type from a Leon type */
def typeToJVM(tpe : TypeTree) : String = tpe match {
case Int32Type => "I"
- case IntegerType => "I"
case BooleanType => "Z"
@@ -104,6 +104,9 @@ trait CodeGeneration {
case _ : MapType =>
"L" + MapClass + ";"
+ case IntegerType =>
+ "L" + BigIntClass + ";"
+
case _ : FunctionType =>
"L" + LambdaClass + ";"
@@ -119,7 +122,6 @@ trait CodeGeneration {
/** Return the respective boxed JVM type from a Leon type */
def typeToJVMBoxed(tpe : TypeTree) : String = tpe match {
case Int32Type => s"L$BoxedIntClass;"
- case IntegerType => s"L$BoxedIntClass;"
case BooleanType | UnitType => s"L$BoxedBoolClass;"
case CharType => s"L$BoxedCharClass;"
case other => typeToJVM(other)
@@ -192,10 +194,10 @@ trait CodeGeneration {
mkExpr(bodyWithPost, ch)(Locals(newMapping, Map.empty, Map.empty, isStatic))
funDef.returnType match {
- case IntegerType | Int32Type | BooleanType | UnitType =>
+ case Int32Type | BooleanType | UnitType =>
ch << IRETURN
- case _ : ClassType | _ : TupleType | _ : SetType | _ : MapType | _ : ArrayType | _ : FunctionType | _ : TypeParameter =>
+ case IntegerType | _ : ClassType | _ : TupleType | _ : SetType | _ : MapType | _ : ArrayType | _ : FunctionType | _ : TypeParameter =>
ch << ARETURN
case other =>
@@ -220,7 +222,7 @@ trait CodeGeneration {
mkExpr(d, ch)
val slot = ch.getFreshVar
val instr = i.getType match {
- case IntegerType | Int32Type | CharType | BooleanType | UnitType => IStore(slot)
+ case Int32Type | CharType | BooleanType | UnitType => IStore(slot)
case _ => AStore(slot)
}
ch << instr
@@ -228,8 +230,6 @@ trait CodeGeneration {
case IntLiteral(v) =>
ch << Ldc(v)
- case InfiniteIntegerLiteral(v) =>
- ch << Ldc(v.toInt)
case CharLiteral(v) =>
ch << Ldc(v)
@@ -240,6 +240,11 @@ trait CodeGeneration {
case UnitLiteral() =>
ch << Ldc(1)
+ case InfiniteIntegerLiteral(v) =>
+ ch << New(BigIntClass) << DUP
+ ch << Ldc(v.toString)
+ ch << InvokeSpecial(BigIntClass, constructorName, "(Ljava/lang/String;)V")
+
// Case classes
case CaseClass(cct, as) =>
val (ccName, ccApplySig) = leonClassToJVMInfo(cct.classDef).getOrElse {
@@ -572,31 +577,31 @@ trait CodeGeneration {
case Plus(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << IADD
+ ch << InvokeVirtual(BigIntClass, "add", "(L%s;)L%s;".format(BigIntClass, BigIntClass))
case Minus(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << ISUB
+ ch << InvokeVirtual(BigIntClass, "sub", "(L%s;)L%s;".format(BigIntClass, BigIntClass))
case Times(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << IMUL
+ ch << InvokeVirtual(BigIntClass, "mult", "(L%s;)L%s;".format(BigIntClass, BigIntClass))
case Division(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << IDIV
+ ch << InvokeVirtual(BigIntClass, "div", "(L%s;)L%s;".format(BigIntClass, BigIntClass))
case Modulo(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << IREM
+ ch << InvokeVirtual(BigIntClass, "mod", "(L%s;)L%s;".format(BigIntClass, BigIntClass))
case UMinus(e) =>
mkExpr(e, ch)
- ch << INEG
+ ch << InvokeVirtual(BigIntClass, "neg", "()L%s;".format(BigIntClass))
//BV arithmetic
case BVPlus(l, r) =>
@@ -674,7 +679,6 @@ trait CodeGeneration {
case Untyped => throw CompilationException("Cannot compile untyped array access.")
case CharType => CALOAD
case Int32Type => IALOAD
- case IntegerType => IALOAD
case BooleanType => BALOAD
case _ => AALOAD
})
@@ -686,7 +690,6 @@ trait CodeGeneration {
val storeInstr = a.getType match {
case ArrayType(CharType) => ch << NewArray.primitive("T_CHAR"); CASTORE
case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
- case ArrayType(IntegerType) => ch << NewArray.primitive("T_INT"); IASTORE
case ArrayType(BooleanType) => ch << NewArray.primitive("T_BOOLEAN"); BASTORE
case ArrayType(other) => ch << NewArray(typeToJVM(other)); AASTORE
case other => throw CompilationException("Cannot compile finite array expression whose type is %s.".format(other))
@@ -711,7 +714,6 @@ trait CodeGeneration {
val storeInstr = a.getType match {
case ArrayType(CharType) => ch << NewArray.primitive("T_CHAR"); CASTORE
case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
- case ArrayType(IntegerType) => ch << NewArray.primitive("T_INT"); IASTORE
case ArrayType(BooleanType) => ch << NewArray.primitive("T_BOOLEAN"); BASTORE
case ArrayType(other) => ch << NewArray(typeToJVM(other)); AASTORE
case other => throw CompilationException("Cannot compile finite array expression whose type is %s.".format(other))
@@ -794,10 +796,6 @@ trait CodeGeneration {
ch << New(BoxedIntClass) << DUP
mkExpr(e, ch)
ch << InvokeSpecial(BoxedIntClass, constructorName, "(I)V")
- case IntegerType =>
- ch << New(BoxedIntClass) << DUP
- mkExpr(e, ch)
- ch << InvokeSpecial(BoxedIntClass, constructorName, "(I)V")
case BooleanType | UnitType =>
ch << New(BoxedBoolClass) << DUP
@@ -825,8 +823,6 @@ trait CodeGeneration {
tpe match {
case Int32Type =>
ch << New(BoxedIntClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedIntClass, constructorName, "(I)V")
- case IntegerType =>
- ch << New(BoxedIntClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedIntClass, constructorName, "(I)V")
case BooleanType | UnitType =>
ch << New(BoxedBoolClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedBoolClass, constructorName, "(Z)V")
@@ -845,8 +841,6 @@ trait CodeGeneration {
tpe match {
case Int32Type =>
ch << CheckCast(BoxedIntClass) << InvokeVirtual(BoxedIntClass, "intValue", "()I")
- case IntegerType =>
- ch << CheckCast(BoxedIntClass) << InvokeVirtual(BoxedIntClass, "intValue", "()I")
case BooleanType | UnitType =>
ch << CheckCast(BoxedBoolClass) << InvokeVirtual(BoxedBoolClass, "booleanValue", "()Z")
@@ -860,6 +854,9 @@ trait CodeGeneration {
}
ch << CheckCast(cn)
+ case IntegerType =>
+ ch << CheckCast(BigIntClass)
+
case tt : TupleType =>
ch << CheckCast(TupleClass)
@@ -917,7 +914,7 @@ trait CodeGeneration {
mkExpr(l, ch)
mkExpr(r, ch)
l.getType match {
- case Int32Type | IntegerType | BooleanType | UnitType | CharType =>
+ case Int32Type | BooleanType | UnitType | CharType =>
ch << If_ICmpEq(thenn) << Goto(elze)
case _ =>
@@ -928,22 +925,46 @@ trait CodeGeneration {
case LessThan(l,r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << If_ICmpLt(thenn) << Goto(elze)
+ l.getType match {
+ case Int32Type =>
+ ch << If_ICmpLt(thenn) << Goto(elze)
+ case IntegerType =>
+ ch << InvokeVirtual(BigIntClass, "lessThan", "(L%s;)Z".format(BigIntClass))
+ ch << IfEq(elze) << Goto(thenn)
+ }
case GreaterThan(l,r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << If_ICmpGt(thenn) << Goto(elze)
+ l.getType match {
+ case Int32Type =>
+ ch << If_ICmpGt(thenn) << Goto(elze)
+ case IntegerType =>
+ ch << InvokeVirtual(BigIntClass, "greaterThan", "(L%s;)Z".format(BigIntClass))
+ ch << IfEq(elze) << Goto(thenn)
+ }
case LessEquals(l,r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << If_ICmpLe(thenn) << Goto(elze)
+ l.getType match {
+ case Int32Type =>
+ ch << If_ICmpLe(thenn) << Goto(elze)
+ case IntegerType =>
+ ch << InvokeVirtual(BigIntClass, "lessEquals", "(L%s;)Z".format(BigIntClass))
+ ch << IfEq(elze) << Goto(thenn)
+ }
case GreaterEquals(l,r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << If_ICmpGe(thenn) << Goto(elze)
+ l.getType match {
+ case Int32Type =>
+ ch << If_ICmpGe(thenn) << Goto(elze)
+ case IntegerType =>
+ ch << InvokeVirtual(BigIntClass, "greaterEquals", "(L%s;)Z".format(BigIntClass))
+ ch << IfEq(elze) << Goto(thenn)
+ }
case IfExpr(c, t, e) =>
val innerThen = ch.getFreshLabel("then")
@@ -977,7 +998,7 @@ trait CodeGeneration {
case None => locals.varToLocal(id) match {
case Some(slot) =>
val instr = id.getType match {
- case IntegerType | Int32Type | CharType | BooleanType | UnitType => ILoad(slot)
+ case Int32Type | CharType | BooleanType | UnitType => ILoad(slot)
case _ => ALoad(slot)
}
ch << instr
@@ -1068,11 +1089,11 @@ trait CodeGeneration {
ch << Label(initLabel) // return lzy
//newValue
lzy.returnType match {
- case Int32Type | IntegerType | BooleanType | UnitType | CharType =>
+ case Int32Type | BooleanType | UnitType | CharType =>
// Since the underlying field only has boxed types, we have to unbox them to return them
mkUnbox(lzy.returnType, ch)(NoLocals(isStatic))
ch << IRETURN
- case _ : ClassType | _ : TupleType | _ : SetType | _ : MapType | _ : ArrayType | _: TypeParameter =>
+ case IntegerType | _ : ClassType | _ : TupleType | _ : SetType | _ : MapType | _ : ArrayType | _: TypeParameter =>
ch << ARETURN
case other => throw CompilationException("Unsupported return type : " + other.getClass)
}
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index b24a5f0f9..52509ab71 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -125,8 +125,9 @@ class CompilationUnit(val ctx: LeonContext,
def exprToJVM(e: Expr)(implicit monitor : LeonCodeGenRuntimeMonitor): AnyRef = e match {
case IntLiteral(v) =>
new java.lang.Integer(v)
+
case InfiniteIntegerLiteral(v) =>
- new java.lang.Integer(v.toInt)
+ new leon.codegen.runtime.BigInt(v.toString)
case BooleanLiteral(v) =>
new java.lang.Boolean(v)
@@ -186,8 +187,9 @@ class CompilationUnit(val ctx: LeonContext,
def jvmToExpr(e: AnyRef, tpe: TypeTree): Expr = (e, tpe) match {
case (i: Integer, Int32Type) =>
IntLiteral(i.toInt)
- case (i: Integer, IntegerType) =>
- InfiniteIntegerLiteral(i.toInt)
+
+ case (c: runtime.BigInt, IntegerType) =>
+ InfiniteIntegerLiteral(BigInt(c.underlying))
case (b: java.lang.Boolean, BooleanType) =>
BooleanLiteral(b.booleanValue)
@@ -288,10 +290,10 @@ class CompilationUnit(val ctx: LeonContext,
mkExpr(e, ch)(Locals(newMapping, Map.empty, Map.empty, true))
e.getType match {
- case IntegerType | Int32Type | BooleanType =>
+ case Int32Type | BooleanType =>
ch << IRETURN
- case UnitType | _: TupleType | _: SetType | _: MapType | _: AbstractClassType | _: CaseClassType | _: ArrayType | _: FunctionType | _: TypeParameter =>
+ case IntegerType | UnitType | _: TupleType | _: SetType | _: MapType | _: AbstractClassType | _: CaseClassType | _: ArrayType | _: FunctionType | _: TypeParameter =>
ch << ARETURN
case other =>
diff --git a/src/test/scala/leon/test/codegen/CodeGenTests.scala b/src/test/scala/leon/test/codegen/CodeGenTests.scala
index 1e0ad3a11..5640cf1bb 100644
--- a/src/test/scala/leon/test/codegen/CodeGenTests.scala
+++ b/src/test/scala/leon/test/codegen/CodeGenTests.scala
@@ -170,8 +170,19 @@ class CodeGenTests extends test.LeonTestSuite {
}""",
IntLiteral(10)
),
+
+ TestCase("methMakeBigInt", """
+ object methSimple {
+
+ val x: BigInt = 42
+
+ def test = x
+
+ }""",
+ InfiniteIntegerLiteral(42)
+ ),
- TestCase("methSimpleBignt", """
+ TestCase("methSimpleBigInt", """
object methSimple {
sealed abstract class Ab {
@@ -183,6 +194,69 @@ class CodeGenTests extends test.LeonTestSuite {
}""",
InfiniteIntegerLiteral(10)
),
+
+ TestCase("BigIntNoOverflow", """
+ object methSimple {
+
+ sealed abstract class Ab {
+ def f2(x : BigInt): BigInt = x + BigInt(2000000000)
+ }
+ case class Con() extends Ab { }
+
+ def test = Con().f2(2000000000)
+ }""",
+ InfiniteIntegerLiteral(BigInt("4000000000"))
+ ),
+
+
+ TestCase("BigIntOps", """
+ object methSimple {
+
+ def f(x: BigInt): BigInt = ((x * 2) - 10)/2
+
+ def test = f(12)
+ }""",
+ InfiniteIntegerLiteral(BigInt(7))
+ ),
+
+
+ TestCase("BigIntComp0", """
+ object methSimple {
+
+ def f(x: BigInt): Boolean = x == BigInt(17)
+
+ def test = f(17)
+ }""",
+ BooleanLiteral(true)
+ ),
+
+ TestCase("BigIntComp1", """
+ object methSimple {
+
+ def f(x: BigInt): BigInt = if(x <= 0) -x else x
+
+ def test = f(-17)
+ }""",
+ InfiniteIntegerLiteral(BigInt(17))
+ ),
+ TestCase("BigIntComp2", """
+ object methSimple {
+
+ def f(x: BigInt): BigInt = if(x < 0) -x else x
+
+ def test = f(-12)
+ }""",
+ InfiniteIntegerLiteral(BigInt(12))
+ ),
+ TestCase("BigIntComp3", """
+ object methSimple {
+
+ def f(x: BigInt): BigInt = if(x >= 0) -x else x
+
+ def test = f(-7)
+ }""",
+ InfiniteIntegerLiteral(BigInt(-7))
+ ),
TestCase("methods", """
object methods {
--
GitLab