From 3e223b3de1d911981f45869d30a2bef6ed9f0256 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Mon, 27 Jan 2014 16:47:21 +0100
Subject: [PATCH] implement missing ArrayUpdated in codegen
---
.../scala/leon/codegen/CodeGeneration.scala | 24 +++++++++++++++++++
.../purescala/valid/ArrayUpdated.scala | 11 +++++++++
.../test/evaluators/EvaluatorsTests.scala | 10 +++++++-
3 files changed, 44 insertions(+), 1 deletion(-)
create mode 100644 src/test/resources/regression/verification/purescala/valid/ArrayUpdated.scala
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 1a846991f..ffb30cbb2 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -346,6 +346,30 @@ trait CodeGeneration {
case _ => AALOAD
})
+ case au @ ArrayUpdated(a, i, v) =>
+ mkExpr(a, ch)
+ ch << DUP
+ ch << ARRAYLENGTH
+ val storeInstr = a.getType match {
+ case ArrayType(Int32Type) => 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))
+ }
+ //srcArrary and targetArray is on the stack
+ ch << DUP_X1 //insert targetArray under srcArray
+ ch << Ldc(0) << SWAP //srcArray, 0, targetArray
+ ch << DUP << ARRAYLENGTH //targetArray, length on stack
+ ch << Ldc(0) << SWAP //final arguments: src, 0, target, 0, length
+ ch << InvokeStatic("java/lang/System", "arraycopy", "(Ljava/lang/Object;ILjava/lang/Object;II)V")
+
+ //targetArray remains on the stack
+ ch << DUP
+ mkExpr(i, ch)
+ mkExpr(v, ch)
+ ch << storeInstr
+ //returns targetArray
+
case a @ FiniteArray(es) =>
ch << Ldc(es.size)
val storeInstr = a.getType match {
diff --git a/src/test/resources/regression/verification/purescala/valid/ArrayUpdated.scala b/src/test/resources/regression/verification/purescala/valid/ArrayUpdated.scala
new file mode 100644
index 000000000..67d4af25d
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/ArrayUpdated.scala
@@ -0,0 +1,11 @@
+import leon.Utils._
+
+object Test {
+
+ def test(a: Array[Int]): Int = {
+ require(a.length > 0)
+ val a2 = a.updated(0, 2)
+ a2(0)
+ } ensuring(res => res == 2)
+
+}
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 6967f38de..51894fc06 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -377,7 +377,12 @@ class EvaluatorsTests extends LeonTestSuite {
val p = """|object Program {
| def boolArrayRead(bools : Array[Boolean], index : Int) : Boolean = bools(index)
|
- | def intArrayRead(bools : Array[Int], index : Int) : Int = bools(index)
+ | def intArrayRead(ints : Array[Int], index : Int) : Int = ints(index)
+ |
+ | def intArrayUpdate(ints : Array[Int], index : Int, value: Int) : Int = {
+ | val na = ints.updated(index, value)
+ | na(index)
+ | }
|}
|""".stripMargin
@@ -394,6 +399,9 @@ class EvaluatorsTests extends LeonTestSuite {
checkComp(e, mkCall("intArrayRead", ia, IL(1)), IL(42))
checkComp(e, ArrayLength(ia), IL(3))
+ checkComp(e, mkCall("intArrayUpdate", ia, IL(0), IL(13)), IL(13))
+ checkComp(e, mkCall("intArrayUpdate", ia, IL(1), IL(17)), IL(17))
+
checkError(e, mkCall("boolArrayRead", ba, IL(2)))
}
}
--
GitLab