diff --git a/src/main/scala/leon/genc/CAST.scala b/src/main/scala/leon/genc/CAST.scala index a8b7b835f07997ce76c7019e72e4997dd35004f7..9baa9d86948afb45fb2ef6109112fbb552d7a814 100644 --- a/src/main/scala/leon/genc/CAST.scala +++ b/src/main/scala/leon/genc/CAST.scala @@ -73,7 +73,7 @@ object CAST { // C Abstract Syntax Tree } case class Assign(lhs: Stmt, rhs: Stmt) extends Stmt { - require(rhs.isValue) + require(lhs.isValue && rhs.isValue) } // Note: we don't need to differentiate between specific @@ -185,10 +185,10 @@ object CAST { // C Abstract Syntax Tree } // True if statement can be used as a value - def isValue = isLiteral || { + def isValue: Boolean = isLiteral || { stmt match { //case _: Assign => true it's probably the case but for now let's ignore it - case c: Compound => c.stmts.size == 1 + case c: Compound => c.stmts.size == 1 && c.stmts.head.isValue case _: UnOp => true case _: MultiOp => true case _: SubscriptOp => true diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala index d8a52687c353a5f0aac4d64b9230719b516c240f..9ccad62cd9348131eb178608a1dd2ad833c4d7e7 100644 --- a/src/main/scala/leon/genc/CConverter.scala +++ b/src/main/scala/leon/genc/CConverter.scala @@ -245,8 +245,8 @@ class CConverter(val ctx: LeonContext, val prog: Program) { f.body ~~ assign - case t @ Tuple(exprs) => - val struct = convertToStruct(t.getType) + case tuple @ Tuple(exprs) => + val struct = convertToStruct(tuple.getType) val types = struct.fields map { _.typ } val fs = convertAndNormaliseExecution(exprs, types) val args = fs.values.zipWithIndex map { @@ -255,37 +255,50 @@ class CConverter(val ctx: LeonContext, val prog: Program) { fs.bodies ~~ CAST.StructInit(args, struct) - case TupleSelect(tuple, idx) => // here idx is already 1-based - CAST.AccessField(convertToStmt(tuple), CAST.Tuple.getNthId(idx)) + case TupleSelect(tuple1, idx) => // here idx is already 1-based + val struct = convertToStruct(tuple1.getType) + val tuple2 = convertToStmt(tuple1) - case ArrayLength(array) => - CAST.AccessField(convertToStmt(array), CAST.Array.lengthId) + val fs = normaliseExecution((tuple2, struct) :: Nil) - case ArraySelect(array1, index) => - val arrayF = convertAndFlatten(array1) - val idxF = convertAndFlatten(index) - val ptr = CAST.AccessField(arrayF.value, CAST.Array.dataId) + val tuple = fs.values.head - val select = if (idxF.value.isValue) { - CAST.SubscriptOp(ptr, idxF.value) - } else { - val tmp = CAST.FreshVar(CAST.Int32, "index") - val decl = CAST.DeclVar(tmp) - val set = injectAssign(tmp, idxF.value) + fs.bodies ~~ CAST.AccessField(tuple, CAST.Tuple.getNthId(idx)) - decl ~ set ~ CAST.SubscriptOp(ptr, CAST.AccessVar(tmp.id)) - } + case ArrayLength(array1) => + val array2 = convertToStmt(array1) + val arrayType = convertToType(array1.getType) + + val fs = normaliseExecution((array2, arrayType) :: Nil) + + val array = fs.values.head + + fs.bodies ~~ CAST.AccessField(array, CAST.Array.lengthId) + + case ArraySelect(array1, index1) => + val array2 = convertToStmt(array1) + val arrayType = convertToType(array1.getType) + val index2 = convertToStmt(index1) + + val fs = normaliseExecution((array2, arrayType) :: (index2, CAST.Int32) :: Nil) - arrayF.body ~~~ idxF.body ~ select + val array = fs.values(0) + val index = fs.values(1) + val ptr = CAST.AccessField(array, CAST.Array.dataId) + val select = CAST.SubscriptOp(ptr, index) - case NonemptyArray(elems, Some((defaultValue, length))) if elems.isEmpty => - val lengthF = convertAndFlatten(length) - val typ = convertToType(defaultValue.getType) - val valueF = convertAndFlatten(defaultValue) - // TODO the value (which can be a function call) should be saved into - // a local variable to prevent calling it many times + fs.bodies ~~ select - lengthF.body ~~~ valueF.body ~ CAST.ArrayInit(lengthF.value, typ, valueF.value) + case NonemptyArray(elems, Some((value1, length1))) if elems.isEmpty => + val length2 = convertToStmt(length1) + val valueType = convertToType(value1.getType) + val value2 = convertToStmt(value1) + + val fs = normaliseExecution((length2, CAST.Int32) :: (value2, valueType) :: Nil) + val length = fs.values(0) + val value = fs.values(1) + + fs.bodies ~~ CAST.ArrayInit(length, valueType, value) case NonemptyArray(elems, Some(_)) => fatalError("NonemptyArray with non empty elements is not supported") @@ -305,11 +318,24 @@ class CConverter(val ctx: LeonContext, val prog: Program) { fs.bodies ~~ CAST.ArrayInitWithValues(typ, fs.values) - case ArrayUpdate(array, index, newValue) => - val lhsF = convertAndFlatten(ArraySelect(array, index)) - val rhsF = convertAndFlatten(newValue) + case ArrayUpdate(array1, index1, newValue1) => + val arrayType = convertToType(array1.getType) + val indexType = CAST.Int32 + val valueType = convertToType(newValue1.getType) + val values = array1 :: index1 :: newValue1 :: Nil + val types = arrayType :: indexType :: valueType :: Nil + + val fs = convertAndNormaliseExecution(values, types) - lhsF.body ~~~ rhsF.body ~ CAST.Assign(lhsF.value, rhsF.value) + val array = fs.values(0) + val index = fs.values(1) + val newValue = fs.values(2) + + val ptr = CAST.AccessField(array, CAST.Array.dataId) + val select = CAST.SubscriptOp(ptr, index) + val assign = CAST.Assign(select, newValue) + + fs.bodies ~~ assign case CaseClass(typ, args1) => val struct = convertToStruct(typ) @@ -590,7 +616,10 @@ class CConverter(val ctx: LeonContext, val prog: Program) { normaliseExecution(exprs map convertToStmt, types) } - private def normaliseExecution(stmts: Seq[CAST.Stmt], types: Seq[CAST.Type]) = { + private def normaliseExecution(typedStmts: Seq[(CAST.Stmt, CAST.Type)]): FlattenedSeq = + normaliseExecution(typedStmts map { _._1 }, typedStmts map { _._2 }) + + private def normaliseExecution(stmts: Seq[CAST.Stmt], types: Seq[CAST.Type]): FlattenedSeq = { require(stmts.length == types.length) // Create temporary variables if needed diff --git a/src/test/resources/regression/genc/valid/ExpressionOrder.scala b/src/test/resources/regression/genc/valid/ExpressionOrder.scala index f86f3e8d25919e18e6efa329e08ce71951fe6d78..2969729a6f8a33736c6f6f1d263afe1727db3d21 100644 --- a/src/test/resources/regression/genc/valid/ExpressionOrder.scala +++ b/src/test/resources/regression/genc/valid/ExpressionOrder.scala @@ -9,7 +9,7 @@ object ExpressionOrder { def bar(i: Int) = i * 2 def baz(i: Int, j: Int) = bar(i) - bar(j) - def syntaxCheck { + def syntaxCheck(i: Int) { val p = Pixel(fun) val m = Matrix(Array(0, 1, 2, 3), 2, 2) @@ -17,6 +17,21 @@ object ExpressionOrder { val a = Array(0, 1, foo / 2, 3, bar(2), z / 1) val t = (true, foo, bar(a(0))) + + val a2 = Array.fill(4)(2) + val a3 = Array.fill(if (i <= 0) 1 else i)(bar(i)) + val b = Array(1, 2, 0) + b(1) = if (bar(b(1)) % 2 == 0) 42 else 58 + + def f1 = (if (i < 0) a else b)(0) + def f2 = (if (i < 0) a else b).length + + //def f3 = (if (i < 0) a else b)(0) = 0 // <- not supported + + val c = (0, true, 2) + val d = (if (i > 0) i else -i, false, 0) + + def f4 = (if (i < 0) d else c)._2 // expression result unused } def main =