diff --git a/src/main/java/leon/codegen/runtime/ArrayBox.java b/src/main/java/leon/codegen/runtime/ArrayBox.java
index 87bb7aade1d3068d4a193a2531095f3fd644e432..b4dee425546953998a22527a54640c554c2d73cb 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 3ea170a05732901467b31f939d87406433719895..a616a1a0b77f3a36f35e3ebba4624e5f9ccb35a8 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 a8c513a0cba6354b625446eb575fafeef34037b0..d14b02f95c5b63f287d5b685bf73545748dd6980 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 e24c0e364dfca43be0da185aab0a4d549d2ff785..9d14bd3dfcc0eb6f08f5273b98ac1448038b363e 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 913e6efbd22bfe8479be9e2b5ea067227bd418e8..728b602f9fa343ae8657a2922ca03a3dfe1ada3f 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 bfe78acb38b7d33fb25cb44046f0bdfed8016bcc..3db4d0bb7628f527dc125d9ac3deba238906244e 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 9c6979ca1992728b4aaefbaa0d9d3465a34558bb..419d37dbb2ed023adb713353b89d4c85a5077a1e 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 cfda6e0ce030d8f6b8d80aff0ea603278aaaf147..0072da45d8f6556100410f733685c5c8f7177b89 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 {