From f9aa132c461fd911d32742e26b5cbf9247eeba70 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 29 Sep 2015 15:56:20 +0200
Subject: [PATCH] Support FiniteArray in CodeGen
NonEmptyArray is required to be nonempty
Allow arbitrary expression as length in CodeGeneration
Handle FiniteArray in valueToJVM
Add integration tests
finiteArray makes EmptyArray for arrays of size 0
Fail when z3 returns negative size array
---
.../java/leon/codegen/runtime/ArrayBox.java | 2 -
.../scala/leon/codegen/CodeGeneration.scala | 28 +++++--
.../scala/leon/codegen/CompilationUnit.scala | 39 +++++++++
.../scala/leon/evaluators/Evaluator.scala | 2 +-
.../scala/leon/purescala/Constructors.scala | 2 +-
.../scala/leon/purescala/Expressions.scala | 1 +
.../leon/solvers/z3/AbstractZ3Solver.scala | 5 ++
.../evaluators/CodegenEvaluatorSuite.scala | 81 +++++++++++--------
8 files changed, 115 insertions(+), 45 deletions(-)
diff --git a/src/main/java/leon/codegen/runtime/ArrayBox.java b/src/main/java/leon/codegen/runtime/ArrayBox.java
index 87bb7aade..b4dee4255 100644
--- a/src/main/java/leon/codegen/runtime/ArrayBox.java
+++ b/src/main/java/leon/codegen/runtime/ArrayBox.java
@@ -4,8 +4,6 @@ package leon.codegen.runtime;
import java.util.Arrays;
-/** If someone wants to make it an efficient implementation of immutable
- * sets, go ahead. */
public final class ArrayBox {
private final Object[] obj1;
private final int[] obj2;
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 3ea170a05..a616a1a0b 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -1054,8 +1054,8 @@ trait CodeGeneration {
//returns targetArray
case a @ FiniteArray(elems, default, length) =>
- val IntLiteral(l) = length
- ch << Ldc(l)
+ mkExpr(length, ch)
+
val storeInstr = a.getType match {
case ArrayType(CharType) => ch << NewArray.primitive("T_CHAR"); CASTORE
case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
@@ -1064,11 +1064,27 @@ trait CodeGeneration {
case other => throw CompilationException(s"Cannot compile finite array expression whose type is $other.")
}
- for (i <- 0 until l) {
- val v = elems.get(i).orElse(default).getOrElse {
- throw CompilationException(s"No valuation for key '$i' in array")
- }
+ // Fill up with default
+ default foreach { df =>
+ val loop = ch.getFreshLabel("array_loop")
+ val loopOut = ch.getFreshLabel("array_loop_out")
+ ch << Ldc(0)
+ // (array, index)
+ ch << Label(loop)
+ ch << DUP2 << SWAP
+ // (array, index, index, array)
+ ch << ARRAYLENGTH
+ // (array, index, index, length)
+ ch << If_ICmpGe(loopOut) << DUP2
+ // (array, index, array, index)
+ mkExpr(df, ch)
+ ch << storeInstr
+ ch << Ldc(1) << IADD << Goto(loop)
+ ch << Label(loopOut) << POP
+ }
+ // Replace present elements with correct value
+ for ((i,v) <- elems ) {
ch << DUP << Ldc(i)
mkExpr(v, ch)
ch << storeInstr
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index a8c513a0c..d14b02f95 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -211,6 +211,45 @@ class CompilationUnit(val ctx: LeonContext,
}
l
+ case f @ IsTyped(FiniteArray(elems, default, IntLiteral(length)), ArrayType(underlying)) =>
+ if (length < 0) {
+ throw LeonFatalError(
+ s"Whoops! Array ${f.asString(ctx)} has length $length. " +
+ default.map { df => s"default: ${df.asString(ctx)}" }.getOrElse("")
+ )
+ }
+
+ import scala.reflect.ClassTag
+
+ def allocArray[A: ClassTag](f: Expr => A): Array[A] = {
+ val arr = new Array[A](length)
+ for {
+ df <- default.toSeq
+ v = f(df)
+ i <- 0 until length
+ } {
+ arr(i) = v
+ }
+ for ((ind, v) <- elems) {
+ arr(ind) = f(v)
+ }
+ arr
+
+ }
+
+ underlying match {
+ case Int32Type =>
+ allocArray { case IntLiteral(v) => v }
+ case BooleanType =>
+ allocArray { case BooleanLiteral(b) => b }
+ case UnitType =>
+ allocArray { case UnitLiteral() => true }
+ case CharType =>
+ allocArray { case CharLiteral(c) => c }
+ case _ =>
+ allocArray(valueToJVM)
+ }
+
case _ =>
throw CompilationException(s"Unexpected expression $e in valueToJVM")
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index e24c0e364..9d14bd3df 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -15,7 +15,7 @@ abstract class Evaluator(val context: LeonContext, val program: Program) extends
type EvaluationResult = EvaluationResults.Result
- /** Evaluates an expression, using `mapping` as a valuation function for the free variables. */
+ /** Evaluates an expression, using [[Model.mapping]] as a valuation function for the free variables. */
def eval(expr: Expr, model: Model) : EvaluationResult
/** Evaluates an expression given a simple model (assumes expr is quantifier-free).
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 913e6efbd..728b602f9 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -263,7 +263,7 @@ object Constructors {
* @see [[purescala.Expressions.EmptyArray EmptyArray]]
*/
def finiteArray(els: Map[Int, Expr], defaultLength: Option[(Expr, Expr)], tpe: TypeTree): Expr = {
- if (els.isEmpty && defaultLength.isEmpty) EmptyArray(tpe)
+ if (els.isEmpty && (defaultLength.isEmpty || defaultLength.get._2 == IntLiteral(0))) EmptyArray(tpe)
else NonemptyArray(els, defaultLength)
}
/** $encodingof simplified `Array(...)` (array length and default element defined at run-time).
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index bfe78acb3..3db4d0bb7 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -846,6 +846,7 @@ object Expressions {
* with a default value (as genereted with `Array.fill` in Scala).
*/
case class NonemptyArray(elems: Map[Int, Expr], defaultLength: Option[(Expr, Expr)]) extends Expr {
+ require(elems.nonEmpty || (defaultLength.nonEmpty && defaultLength.get._2 != IntLiteral(0)))
private val elements = elems.values.toList ++ defaultLength.map(_._1)
val getType = ArrayType(optionToType(leastUpperBound(elements map { _.getType }))).unveilUntyped
}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 9c6979ca1..419d37dbb 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -611,7 +611,12 @@ trait AbstractZ3Solver extends Solver {
val map = rec(args(1), RawArrayType(Int32Type, to))
(size, map) match {
+
case (s : IntLiteral, RawArrayValue(_, elems, default)) =>
+
+ if (s.value < 0)
+ unsupported(s, s"Z3 returned array of negative size")
+
val entries = elems.map {
case (IntLiteral(i), v) => i -> v
case _ => reporter.fatalError("Translation from Z3 to Array failed")
diff --git a/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala
index cfda6e0ce..0072da45d 100644
--- a/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala
@@ -4,15 +4,9 @@ package leon.integration.evaluators
import leon.test._
import leon.evaluators._
-
-import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Expressions._
-import leon.purescala.DefOps._
import leon.purescala.Types._
-import leon.purescala.Extractors._
-import leon.purescala.Constructors._
-
import leon.codegen._
class CodegenEvaluatorSuite extends LeonTestSuiteWithProgram {
@@ -274,38 +268,55 @@ class CodegenEvaluatorSuite extends LeonTestSuiteWithProgram {
def test = (B().x, C().x)
}
+ object Arrays1 {
+ def test = {
+ val x = 1
+ val y = 42
+ val a = Array.fill(y)(x)
+ a(0) + a(41)
+ }
+ }
+
+ object Arrays2 {
+ def test = {
+ val x = 1
+ val a = Array(x, x+1, x+2, x+3)
+ a(0) + a(1) + a(2) + a(3)
+ }
+ }
""")
val results = Seq(
- ("simple", IntLiteral(1)),
- ("simple2", InfiniteIntegerLiteral(1)),
- ("eager", IntLiteral(43)),
- ("thiss", IntLiteral(42) ),
- ("oldStuff", IntLiteral(1)),
- ("methSimple", IntLiteral(10)),
- ("methSimple2", InfiniteIntegerLiteral(42)),
- ("methSimple3", InfiniteIntegerLiteral(10)),
- ("methSimple4", InfiniteIntegerLiteral(BigInt("4000000000"))),
- ("bigint1", InfiniteIntegerLiteral(BigInt(7))),
- ("bigint2", BooleanLiteral(true)),
- ("bigint3", InfiniteIntegerLiteral(BigInt(17))),
- ("bigint4", InfiniteIntegerLiteral(BigInt(12))),
- ("bigint5", InfiniteIntegerLiteral(BigInt(-7))),
- ("methods", IntLiteral(15)),
- ("lazyFields", IntLiteral(1 + 5 + 1 + 6 + 2) ),
- ("modules", IntLiteral(1 + 2 + 0) ),
- ("lazyISLazy" , IntLiteral(42) ),
- ("ListWithSize" , IntLiteral(3) ),
- ("ListWithSumMono" , IntLiteral(1 + 2 + 3) ),
- ("poly" , IntLiteral(42) ),
- ("ListHead" , IntLiteral(1)),
- ("ListWithSum" , IntLiteral(1 + 2 + 3) ),
- // This one loops!
- ("lazyLoops" , Error(Untyped, "Looping") ),
- ("Lazier" , IntLiteral(1 + 2 + 3) ),
- ("SetToList", BooleanLiteral(true) ),
- ("Overrides1", Tuple(Seq(BooleanLiteral(false), BooleanLiteral(true))) ),
- ("Overrides2", Tuple(Seq(BooleanLiteral(false), BooleanLiteral(true))) )
+ "simple" -> IntLiteral(1),
+ "simple2" -> InfiniteIntegerLiteral(1),
+ "eager" -> IntLiteral(43),
+ "thiss" -> IntLiteral(42) ,
+ "oldStuff" -> IntLiteral(1),
+ "methSimple" -> IntLiteral(10),
+ "methSimple2" -> InfiniteIntegerLiteral(42),
+ "methSimple3" -> InfiniteIntegerLiteral(10),
+ "methSimple4" -> InfiniteIntegerLiteral(BigInt("4000000000")),
+ "bigint1" -> InfiniteIntegerLiteral(BigInt(7)),
+ "bigint2" -> BooleanLiteral(true),
+ "bigint3" -> InfiniteIntegerLiteral(BigInt(17)),
+ "bigint4" -> InfiniteIntegerLiteral(BigInt(12)),
+ "bigint5" -> InfiniteIntegerLiteral(BigInt(-7)),
+ "methods" -> IntLiteral(15),
+ "lazyFields" -> IntLiteral(1 + 5 + 1 + 6 + 2),
+ "modules" -> IntLiteral(1 + 2 + 0),
+ "lazyISLazy" -> IntLiteral(42),
+ "ListWithSize" -> IntLiteral(3),
+ "ListWithSumMono" -> IntLiteral(1 + 2 + 3),
+ "poly" -> IntLiteral(42),
+ "ListHead" -> IntLiteral(1),
+ "ListWithSum" -> IntLiteral(1 + 2 + 3),
+ "lazyLoops" -> Error(Untyped, "Looping"),// This one loops!
+ "Lazier" -> IntLiteral(1 + 2 + 3),
+ "SetToList" -> BooleanLiteral(true),
+ "Overrides1" -> Tuple(Seq(BooleanLiteral(false), BooleanLiteral(true))),
+ "Overrides2" -> Tuple(Seq(BooleanLiteral(false), BooleanLiteral(true))),
+ "Arrays1" -> IntLiteral(2),
+ "Arrays2" -> IntLiteral(6)
)
for {
--
GitLab