diff --git a/PERMISSIONS b/PERMISSIONS
index ace330f0c1edc8c871c960eeab6d0319836f2aae..20019048dd418bfd5e6eba56ffaa50c6a279e1d3 100755
--- a/PERMISSIONS
+++ b/PERMISSIONS
@@ -12,5 +12,5 @@ tail -2 "$0" | ssh git@laragit.epfl.ch setperms ${thisrepo}
exit $_
# **Do not** add new lines after the following two!
-WRITERS kuncak psuter rblanc edarulov
+WRITERS kuncak psuter rblanc edarulov hojjat
READERS @lara mazimmer hardy amin
diff --git a/run-tests.sh b/run-tests.sh
index cedaea2d3ec3e75c79161e5a33ac3225368a372d..951862c3e850e1ecb859d2385ed3726a22fddb0d 100755
--- a/run-tests.sh
+++ b/run-tests.sh
@@ -6,7 +6,7 @@ failedtests=""
for f in testcases/regression/valid/*.scala; do
echo -n "Running $f, expecting VALID, got: "
- res=`./leon --timeout=5 --oneline "$f"`
+ res=`./leon --timeout=10 --oneline "$f"`
echo $res | tr [a-z] [A-Z]
if [ $res = valid ]; then
nbsuccess=$((nbsuccess + 1))
@@ -17,7 +17,7 @@ done
for f in testcases/regression/invalid/*.scala; do
echo -n "Running $f, expecting INVALID, got: "
- res=`./leon --timeout=5 --oneline "$f"`
+ res=`./leon --timeout=10 --oneline "$f"`
echo $res | tr [a-z] [A-Z]
if [ $res = invalid ]; then
nbsuccess=$((nbsuccess + 1))
@@ -28,7 +28,7 @@ done
for f in testcases/regression/error/*.scala; do
echo -n "Running $f, expecting ERROR, got: "
- res=`./leon --timeout=5 --oneline "$f"`
+ res=`./leon --timeout=10 --oneline "$f"`
echo $res | tr [a-z] [A-Z]
if [ $res = error ]; then
nbsuccess=$((nbsuccess + 1))
diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index 8c950fd87215da16ebdebc1b13c88dbb78ba66e3..176cb96b1f9fe411be0553afca3a31895d7e962a 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -68,6 +68,7 @@ class Analysis(val program : Program, val reporter: Reporter = Settings.reporter
allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
allVCs ++= tactic.generatePostconditions(funDef)
allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
+ allVCs ++= tactic.generateArrayAccessChecks(funDef)
}
allVCs = allVCs.sortWith((vc1, vc2) => {
val id1 = vc1.funDef.id.name
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7d0d94458291b71381d8719a25e13751ca3cdd9f
--- /dev/null
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -0,0 +1,298 @@
+package leon
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
+
+object ArrayTransformation extends Pass {
+
+ val description = "Add bound checking for array access and remove array update with side effect"
+
+ def apply(pgm: Program): Program = {
+
+ val allFuns = pgm.definedFunctions
+ allFuns.foreach(fd => {
+ id2FreshId = Map()
+ fd.precondition = fd.precondition.map(transform)
+ fd.body = fd.body.map(transform)
+ fd.postcondition = fd.postcondition.map(transform)
+ })
+ pgm
+ }
+
+ private var id2FreshId = Map[Identifier, Identifier]()
+
+ def transform(expr: Expr): Expr = expr match {
+ case sel@ArraySelect(a, i) => {
+ val ra = transform(a)
+ val ri = transform(i)
+ val length = ArrayLength(ra)
+ val res = IfExpr(
+ And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)),
+ ArraySelect(ra, ri).setType(sel.getType).setPosInfo(sel),
+ Error("Index out of bound").setType(sel.getType).setPosInfo(sel)
+ ).setType(sel.getType)
+ res
+ }
+ case up@ArrayUpdate(a, i, v) => {
+ val ra = transform(a)
+ val ri = transform(i)
+ val rv = transform(v)
+ val Variable(id) = ra
+ val length = ArrayLength(ra)
+ val res = IfExpr(
+ And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)),
+ Assignment(id, ArrayUpdated(ra, ri, rv).setType(ra.getType).setPosInfo(up)),
+ Error("Index out of bound").setType(UnitType).setPosInfo(up)
+ ).setType(UnitType)
+ res
+ }
+ case up@ArrayUpdated(a, i, v) => {
+ val ra = transform(a)
+ val ri = transform(i)
+ val rv = transform(v)
+ val length = ArrayLength(ra)
+ val res = IfExpr(
+ And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)),
+ ArrayUpdated(ra, ri, rv).setType(ra.getType).setPosInfo(up),
+ Error("Index out of bound").setType(ra.getType).setPosInfo(up)
+ ).setType(ra.getType)
+ res
+ }
+ case ArrayClone(a) => {
+ val ra = transform(a)
+ ra
+ }
+ case Let(i, v, b) => {
+ v.getType match {
+ case ArrayType(_) => {
+ val freshIdentifier = FreshIdentifier("t").setType(i.getType)
+ id2FreshId += (i -> freshIdentifier)
+ LetVar(freshIdentifier, transform(v), transform(b))
+ }
+ case _ => Let(i, transform(v), transform(b))
+ }
+ }
+ case Variable(i) => {
+ val freshId = id2FreshId.get(i).getOrElse(i)
+ Variable(freshId)
+ }
+
+ case LetVar(id, e, b) => {
+ val er = transform(e)
+ val br = transform(b)
+ LetVar(id, er, br)
+ }
+ case wh@While(c, e) => {
+ val newWh = While(transform(c), transform(e))
+ newWh.invariant = wh.invariant.map(i => transform(i))
+ newWh.setPosInfo(wh)
+ newWh
+ }
+
+ case ite@IfExpr(c, t, e) => {
+ val rc = transform(c)
+ val rt = transform(t)
+ val re = transform(e)
+ IfExpr(rc, rt, re).setType(rt.getType)
+ }
+
+ case m @ MatchExpr(scrut, cses) => {
+ val scrutRec = transform(scrut)
+ val csesRec = cses.map{
+ case SimpleCase(pat, rhs) => SimpleCase(pat, transform(rhs))
+ case GuardedCase(pat, guard, rhs) => GuardedCase(pat, transform(guard), transform(rhs))
+ }
+ val tpe = csesRec.head.rhs.getType
+ MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
+ }
+ case LetDef(fd, b) => {
+ fd.precondition = fd.precondition.map(transform)
+ fd.body = fd.body.map(transform)
+ fd.postcondition = fd.postcondition.map(transform)
+ val rb = transform(b)
+ LetDef(fd, rb)
+ }
+ case n @ NAryOperator(args, recons) => recons(args.map(transform)).setType(n.getType)
+ case b @ BinaryOperator(a1, a2, recons) => recons(transform(a1), transform(a2)).setType(b.getType)
+ case u @ UnaryOperator(a, recons) => recons(transform(a)).setType(u.getType)
+
+ case (t: Terminal) => t
+ case unhandled => scala.sys.error("Non-terminal case should be handled in ArrayTransformation: " + unhandled)
+ }
+
+ //val newFuns: Seq[FunDef] = allFuns.map(fd => {
+ // if(fd.hasImplementation) {
+ // val args = fd.args
+ // if(args.exists(vd => containsArrayType(vd.tpe)) || containsArrayType(fd.returnType)) {
+ // val newArgs = args.map(vd => {
+ // val freshId = FreshIdentifier(vd.id.name).setType(transform(vd.tpe))
+ // id2id += (vd.id -> freshId)
+ // val newTpe = transform(vd.tpe)
+ // VarDecl(freshId, newTpe)
+ // })
+ // val freshFunName = FreshIdentifier(fd.id.name)
+ // val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
+ // fd2fd += (fd -> freshFunDef)
+ // freshFunDef.fromLoop = fd.fromLoop
+ // freshFunDef.parent = fd.parent
+ // freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ // freshFunDef
+ // } else fd
+ // } else fd
+ //})
+
+ //allFuns.zip(newFuns).foreach{ case (ofd, nfd) => ofd.body.map(body => {
+ // nfd.precondition = ofd.precondition.map(transform)
+ // nfd.postcondition = ofd.postcondition.map(transform)
+ // val newBody = transform(body)
+ // nfd.body = Some(newBody)
+ //})}
+
+ //val Program(id, ObjectDef(objId, _, invariants)) = pgm
+ //val allClasses: Seq[Definition] = pgm.definedClasses
+ //Program(id, ObjectDef(objId, allClasses ++ newFuns, invariants))
+
+
+ //private def transform(tpe: TypeTree): TypeTree = tpe match {
+ // case ArrayType(base) => TupleType(Seq(ArrayType(transform(base)), Int32Type))
+ // case TupleType(tpes) => TupleType(tpes.map(transform))
+ // case t => t
+ //}
+ //private def containsArrayType(tpe: TypeTree): Boolean = tpe match {
+ // case ArrayType(base) => true
+ // case TupleType(tpes) => tpes.exists(containsArrayType)
+ // case t => false
+ //}
+
+ //private var id2id: Map[Identifier, Identifier] = Map()
+ //private var fd2fd: Map[FunDef, FunDef] = Map()
+
+ //private def transform(expr: Expr): Expr = expr match {
+ // case fill@ArrayFill(length, default) => {
+ // var rLength = transform(length)
+ // val rDefault = transform(default)
+ // val rFill = ArrayMake(rDefault).setType(fill.getType)
+ // Tuple(Seq(rFill, rLength)).setType(TupleType(Seq(fill.getType, Int32Type)))
+ // }
+ // case sel@ArraySelect(a, i) => {
+ // val ar = transform(a)
+ // val ir = transform(i)
+ // val length = TupleSelect(ar, 2).setType(Int32Type)
+ // IfExpr(
+ // And(GreaterEquals(ir, IntLiteral(0)), LessThan(ir, length)),
+ // ArraySelect(TupleSelect(ar, 1).setType(ArrayType(sel.getType)), ir).setType(sel.getType).setPosInfo(sel),
+ // Error("Index out of bound").setType(sel.getType).setPosInfo(sel)
+ // ).setType(sel.getType)
+ // }
+ // case up@ArrayUpdate(a, i, v) => {
+ // val ar = transform(a)
+ // val ir = transform(i)
+ // val vr = transform(v)
+ // val Variable(id) = ar
+ // val length = TupleSelect(ar, 2).setType(Int32Type)
+ // val array = TupleSelect(ar, 1).setType(ArrayType(v.getType))
+ // IfExpr(
+ // And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
+ // Assignment(
+ // id,
+ // Tuple(Seq(
+ // ArrayUpdated(array, ir, vr).setType(array.getType).setPosInfo(up),
+ // length)
+ // ).setType(TupleType(Seq(array.getType, Int32Type)))),
+ // Error("Index out of bound").setType(UnitType).setPosInfo(up)
+ // ).setType(UnitType)
+ // }
+ // case ArrayLength(a) => {
+ // val ar = transform(a)
+ // TupleSelect(ar, 2).setType(Int32Type)
+ // }
+ // case Let(i, v, b) => {
+ // val vr = transform(v)
+ // v.getType match {
+ // case ArrayType(_) => {
+ // val freshIdentifier = FreshIdentifier("t").setType(vr.getType)
+ // id2id += (i -> freshIdentifier)
+ // val br = transform(b)
+ // LetVar(freshIdentifier, vr, br)
+ // }
+ // case _ => {
+ // val br = transform(b)
+ // Let(i, vr, br)
+ // }
+ // }
+ // }
+ // case LetVar(id, e, b) => {
+ // val er = transform(e)
+ // val br = transform(b)
+ // LetVar(id, er, br)
+ // }
+ // case wh@While(c, e) => {
+ // val newWh = While(transform(c), transform(e))
+ // newWh.invariant = wh.invariant.map(i => transform(i))
+ // newWh.setPosInfo(wh)
+ // }
+
+ // case ite@IfExpr(c, t, e) => {
+ // val rc = transform(c)
+ // val rt = transform(t)
+ // val re = transform(e)
+ // IfExpr(rc, rt, re).setType(rt.getType)
+ // }
+
+ // case m @ MatchExpr(scrut, cses) => {
+ // val scrutRec = transform(scrut)
+ // val csesRec = cses.map{
+ // case SimpleCase(pat, rhs) => SimpleCase(pat, transform(rhs))
+ // case GuardedCase(pat, guard, rhs) => GuardedCase(pat, transform(guard), transform(rhs))
+ // }
+ // val tpe = csesRec.head.rhs.getType
+ // MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
+ // }
+ // case LetDef(fd, b) => {
+ // val newFd = if(fd.hasImplementation) {
+ // val body = fd.body.get
+ // val args = fd.args
+ // val newFd =
+ // if(args.exists(vd => containsArrayType(vd.tpe)) || containsArrayType(fd.returnType)) {
+ // val newArgs = args.map(vd => {
+ // val freshId = FreshIdentifier(vd.id.name).setType(transform(vd.tpe))
+ // id2id += (vd.id -> freshId)
+ // val newTpe = transform(vd.tpe)
+ // VarDecl(freshId, newTpe)
+ // })
+ // val freshFunName = FreshIdentifier(fd.id.name)
+ // val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
+ // fd2fd += (fd -> freshFunDef)
+ // freshFunDef.fromLoop = fd.fromLoop
+ // freshFunDef.parent = fd.parent
+ // freshFunDef.precondition = fd.precondition.map(transform)
+ // freshFunDef.postcondition = fd.postcondition.map(transform)
+ // freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ // freshFunDef
+ // } else fd
+ // val newBody = transform(body)
+ // newFd.body = Some(newBody)
+ // newFd
+ // } else fd
+ // val rb = transform(b)
+ // LetDef(newFd, rb)
+ // }
+ // case FunctionInvocation(fd, args) => {
+ // val rargs = args.map(transform)
+ // val rfd = fd2fd.get(fd).getOrElse(fd)
+ // FunctionInvocation(rfd, rargs)
+ // }
+
+ // case n @ NAryOperator(args, recons) => recons(args.map(transform)).setType(n.getType)
+ // case b @ BinaryOperator(a1, a2, recons) => recons(transform(a1), transform(a2)).setType(b.getType)
+ // case u @ UnaryOperator(a, recons) => recons(transform(a)).setType(u.getType)
+
+ // case v @ Variable(id) => if(id2id.isDefinedAt(id)) Variable(id2id(id)) else v
+ // case (t: Terminal) => t
+ // case unhandled => scala.sys.error("Non-terminal case should be handled in ArrayTransformation: " + unhandled)
+
+ //}
+
+}
diff --git a/src/main/scala/leon/DefaultTactic.scala b/src/main/scala/leon/DefaultTactic.scala
index a01d025431c2ec3c704a1950410334fd322abae9..70ad17f36150a47f846fe67a8bf8db350e03a9bf 100644
--- a/src/main/scala/leon/DefaultTactic.scala
+++ b/src/main/scala/leon/DefaultTactic.scala
@@ -194,6 +194,35 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
toRet
}
+ def generateArrayAccessChecks(function: FunDef) : Seq[VerificationCondition] = {
+ val toRet = if (function.hasBody) {
+ val cleanBody = matchToIfThenElse(function.body.get)
+
+ val allPathConds = collectWithPathCondition((t => t match {
+ case Error("Index out of bound") => true
+ case _ => false
+ }), cleanBody)
+
+ def withPrecIfDefined(conds: Seq[Expr]) : Expr = if (function.hasPrecondition) {
+ Not(And(mapGetWithChecks(matchToIfThenElse(function.precondition.get)), And(conds)))
+ } else {
+ Not(And(conds))
+ }
+
+ allPathConds.map(pc =>
+ new VerificationCondition(
+ withPrecIfDefined(pc._1),
+ if(function.fromLoop) function.parent.get else function,
+ VCKind.ArrayAccess,
+ this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
+ ).toSeq
+ } else {
+ Seq.empty
+ }
+
+ toRet
+ }
+
def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition] = {
generateMapAccessChecks(function)
}
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index 004d03d6159e07d78dc0b508af3196a5970b66d6..c3e0ca1a6a40fdbf59da5508d076399346ceffe7 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -85,7 +85,9 @@ object Evaluator {
if(fd.hasPrecondition) {
rec(frame, matchToIfThenElse(fd.precondition.get)) match {
case BooleanLiteral(true) => ;
- case BooleanLiteral(false) => throw RuntimeErrorEx("Precondition violation for " + fd.id.name + " reached in evaluation.")
+ case BooleanLiteral(false) => {
+ throw RuntimeErrorEx("Precondition violation for " + fd.id.name + " reached in evaluation.: " + fd.precondition.get)
+ }
case other => throw TypeErrorEx(TypeError(other, BooleanType))
}
}
@@ -255,6 +257,37 @@ object Evaluator {
case e @ EmptySet(_) => e
case i @ IntLiteral(_) => i
case b @ BooleanLiteral(_) => b
+ case u @ UnitLiteral => u
+
+ case f @ ArrayFill(length, default) => {
+ val rDefault = rec(ctx, default)
+ val rLength = rec(ctx, length)
+ val IntLiteral(iLength) = rLength
+ FiniteArray((1 to iLength).map(_ => rDefault).toSeq)
+ }
+ case ArrayLength(a) => {
+ var ra = rec(ctx, a)
+ while(!ra.isInstanceOf[FiniteArray])
+ ra = ra.asInstanceOf[ArrayUpdated].array
+ IntLiteral(ra.asInstanceOf[FiniteArray].exprs.size)
+ }
+ case ArrayUpdated(a, i, v) => {
+ val ra = rec(ctx, a)
+ val ri = rec(ctx, i)
+ val rv = rec(ctx, v)
+
+ val IntLiteral(index) = ri
+ val FiniteArray(exprs) = ra
+ FiniteArray(exprs.updated(index, rv))
+ }
+ case ArraySelect(a, i) => {
+ val IntLiteral(index) = rec(ctx, i)
+ val FiniteArray(exprs) = rec(ctx, a)
+ exprs(index)
+ }
+ case FiniteArray(exprs) => {
+ FiniteArray(exprs.map(e => rec(ctx, e)))
+ }
case f @ FiniteMap(ss) => FiniteMap(ss.map(rec(ctx,_)).distinct.asInstanceOf[Seq[SingletonMap]]).setType(f.getType)
case e @ EmptyMap(_,_) => e
diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
index 7d8469998f53c9abb14c9c84dfa123fb462900c2..89cfe4492b914c630e5122993700f4945f1662b5 100644
--- a/src/main/scala/leon/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -46,6 +46,7 @@ object Extensions {
def generatePreconditions(function: FunDef) : Seq[VerificationCondition]
def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[VerificationCondition]
def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition]
+ def generateArrayAccessChecks(function: FunDef) : Seq[VerificationCondition]
}
// The rest of the code is for dynamically loading extensions
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index e56e82ac9d294a0f7ecf6e07504a402aa4614f60..8ec0984ee1994371ad95a95b7367887c923d2ff5 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -59,6 +59,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
fallbackSorts = Map.empty
mapSorts = Map.empty
+ arraySorts = Map.empty
funSorts = Map.empty
funDomainConstructors = Map.empty
funDomainSelectors = Map.empty
@@ -98,6 +99,9 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
private var setSorts: Map[TypeTree, Z3Sort] = Map.empty
private var mapSorts: Map[TypeTree, Z3Sort] = Map.empty
+ private var unitSort: Z3Sort = null
+ private var unitValue: Z3AST = null
+
protected[leon] var funSorts: Map[TypeTree, Z3Sort] = Map.empty
protected[leon] var funDomainConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
protected[leon] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
@@ -106,6 +110,11 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
protected[leon] var tupleConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
protected[leon] var tupleSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
+ private var arraySorts: Map[TypeTree, Z3Sort] = Map.empty
+ protected[leon] var arrayTupleCons: Map[TypeTree, Z3FuncDecl] = Map.empty
+ protected[leon] var arrayTupleSelectorArray: Map[TypeTree, Z3FuncDecl] = Map.empty
+ protected[leon] var arrayTupleSelectorLength: Map[TypeTree, Z3FuncDecl] = Map.empty
+
private var reverseTupleConstructors: Map[Z3FuncDecl, TupleType] = Map.empty
private var reverseTupleSelectors: Map[Z3FuncDecl, (TupleType, Int)] = Map.empty
@@ -192,6 +201,27 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
setSorts = Map.empty
setCardFuns = Map.empty
+ //unitSort = z3.mkUninterpretedSort("unit")
+ //unitValue = z3.mkFreshConst("Unit", unitSort)
+ //val bound = z3.mkBound(0, unitSort)
+ //val eq = z3.mkEq(bound, unitValue)
+ //val decls = Seq((z3.mkFreshStringSymbol("u"), unitSort))
+ //val unitAxiom = z3.mkForAll(0, Seq(), decls, eq)
+ //println(unitAxiom)
+ //println(unitValue)
+ //z3.assertCnstr(unitAxiom)
+ val Seq((us, Seq(unitCons), Seq(unitTester), _)) = z3.mkADTSorts(
+ Seq(
+ (
+ "Unit",
+ Seq("Unit"),
+ Seq(Seq())
+ )
+ )
+ )
+ unitSort = us
+ unitValue = unitCons()
+
val intSetSort = typeToSort(SetType(Int32Type))
intSetMinFun = z3.mkFreshFuncDecl("setMin", Seq(intSetSort), intSort)
intSetMaxFun = z3.mkFreshFuncDecl("setMax", Seq(intSetSort), intSort)
@@ -361,6 +391,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
def typeToSort(tt: TypeTree): Z3Sort = tt match {
case Int32Type => intSort
case BooleanType => boolSort
+ case UnitType => unitSort
case AbstractClassType(cd) => adtSorts(cd)
case CaseClassType(cd) => {
if (cd.hasParent) {
@@ -389,6 +420,21 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
ms
}
}
+ case at @ ArrayType(base) => arraySorts.get(at) match {
+ case Some(s) => s
+ case None => {
+ val intSort = typeToSort(Int32Type)
+ val toSort = typeToSort(base)
+ val as = z3.mkArraySort(intSort, toSort)
+ val tupleSortSymbol = z3.mkFreshStringSymbol("Array")
+ val (arrayTupleSort, arrayTupleCons_, Seq(arrayTupleSelectorArray_, arrayTupleSelectorLength_)) = z3.mkTupleSort(tupleSortSymbol, as, intSort)
+ arraySorts += (at -> arrayTupleSort)
+ arrayTupleCons += (at -> arrayTupleCons_)
+ arrayTupleSelectorArray += (at -> arrayTupleSelectorArray_)
+ arrayTupleSelectorLength += (at -> arrayTupleSelectorLength_)
+ arrayTupleSort
+ }
+ }
case ft @ FunctionType(fts, tt) => funSorts.get(ft) match {
case Some(s) => s
case None => {
@@ -406,7 +452,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
case Some(s) => s
case None => {
val tpesSorts = tpes.map(typeToSort)
- val sortSymbol = z3.mkFreshStringSymbol("TupleSort")
+ val sortSymbol = z3.mkFreshStringSymbol("Tuple")
val (tupleSort, consTuple, projsTuple) = z3.mkTupleSort(sortSymbol, tpesSorts: _*)
tupleSorts += (tt -> tupleSort)
tupleConstructors += (tt -> consTuple)
@@ -518,14 +564,11 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
reporter.info(" - Initial unrolling...")
val (clauses, guards) = unrollingBank.initialUnrolling(expandedVC)
- //for(clause <- clauses) {
- //println("we're getting a new clause " + clause)
- // z3.assertCnstr(toZ3Formula(z3, clause).get)
- //}
+ for(clause <- clauses) {
+ Logger.debug("we're getting a new clause " + clause, 4, "z3solver")
+ }
- //println("The blocking guards: " + guards)
val cc = toZ3Formula(z3, And(clauses)).get
- // println("CC : " + cc)
z3.assertCnstr(cc)
// these are the optional sequence of assumption literals
@@ -566,6 +609,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
(a, m, Seq.empty[Z3AST])
}
reporter.info(" - Finished search with blocked literals")
+ Logger.debug("The blocking guards are: " + blockingSet.mkString(", "), 4, "z3solver")
// if (Settings.useCores)
// reporter.info(" - Core is : " + core)
@@ -745,16 +789,13 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
reporter.info(" - more unrollings")
for((id,polarity) <- toReleaseAsPairs) {
val (newClauses,newBlockers) = unrollingBank.unlock(id, !polarity)
- //println("Unlocked : " + (id, !polarity))
for(clause <- newClauses) {
- //println("we're getting a new clause " + clause)
- // z3.assertCnstr(toZ3Formula(z3, clause).get)
+ Logger.debug("we're getting a new clause " + clause, 4, "z3solver")
}
for(ncl <- newClauses) {
z3.assertCnstr(toZ3Formula(z3, ncl).get)
}
- //z3.assertCnstr(toZ3Formula(z3, And(newClauses)).get)
blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
}
reporter.info(" - finished unrolling")
@@ -970,6 +1011,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
case Not(e) => z3.mkNot(rec(e))
case IntLiteral(v) => z3.mkInt(v, intSort)
case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
+ case UnitLiteral => unitValue
case Equals(l, r) => z3.mkEq(rec(l), rec(r))
case Plus(l, r) => if(USEBV) z3.mkBVAdd(rec(l), rec(r)) else z3.mkAdd(rec(l), rec(r))
case Minus(l, r) => if(USEBV) z3.mkBVSub(rec(l), rec(r)) else z3.mkSub(rec(l), rec(r))
@@ -1053,6 +1095,38 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
case MapType(ft, tt) => z3.mkDistinct(z3.mkSelect(rec(m), rec(k)), mapRangeNoneConstructors(tt)())
case errorType => scala.sys.error("Unexpected type for map: " + (ex, errorType))
}
+ case fill@ArrayFill(length, default) => {
+ val at@ArrayType(base) = fill.getType
+ typeToSort(at)
+ val cons = arrayTupleCons(at)
+ val ar = z3.mkConstArray(typeToSort(base), rec(default))
+ val res = cons(ar, rec(length))
+ res
+ }
+ case ArraySelect(a, index) => {
+ typeToSort(a.getType)
+ val ar = rec(a)
+ val getArray = arrayTupleSelectorArray(a.getType)
+ val res = z3.mkSelect(getArray(ar), rec(index))
+ res
+ }
+ case ArrayUpdated(a, index, newVal) => {
+ typeToSort(a.getType)
+ val ar = rec(a)
+ val getArray = arrayTupleSelectorArray(a.getType)
+ val getLength = arrayTupleSelectorLength(a.getType)
+ val cons = arrayTupleCons(a.getType)
+ val store = z3.mkStore(getArray(ar), rec(index), rec(newVal))
+ val res = cons(store, getLength(ar))
+ res
+ }
+ case ArrayLength(a) => {
+ typeToSort(a.getType)
+ val ar = rec(a)
+ val getLength = arrayTupleSelectorLength(a.getType)
+ val res = getLength(ar)
+ res
+ }
case AnonymousFunctionInvocation(id, args) => id.getType match {
case ft @ FunctionType(fts, tt) => {
val consFD = funDomainConstructors(ft)
@@ -1110,8 +1184,28 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
(if (elems.isEmpty) EmptySet(dt) else FiniteSet(elems.toSeq)).setType(expType.get)
}
}
+ case Some(ArrayType(dt)) => {
+ val Z3AppAST(decl, args) = z3.getASTKind(t)
+ assert(args.size == 2)
+ val IntLiteral(length) = rec(args(1), Some(Int32Type))
+ val array = model.getArrayValue(args(0)) match {
+ case None => throw new CantTranslateException(t)
+ case Some((map, elseValue)) => {
+ val exprs = map.foldLeft((1 to length).map(_ => rec(elseValue, Some(dt))).toSeq)((acc, p) => {
+ val IntLiteral(index) = rec(p._1, Some(Int32Type))
+ if(index >= 0 && index < length)
+ acc.updated(index, rec(p._2, Some(dt)))
+ else acc
+ })
+ FiniteArray(exprs)
+ }
+ }
+ array
+ }
case other =>
- z3.getASTKind(t) match {
+ if(t == unitValue)
+ UnitLiteral
+ else z3.getASTKind(t) match {
case Z3AppAST(decl, args) => {
val argsSize = args.size
if(argsSize == 0 && z3IdToExpr.isDefinedAt(t)) {
@@ -1148,7 +1242,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
val r1 = rargs(1)
val r2 = rargs(2)
try {
- IfExpr(r0, r1, r2).setType(leastUpperBound(r1.getType, r2.getType))
+ IfExpr(r0, r1, r2).setType(leastUpperBound(r1.getType, r2.getType).get)
} catch {
case e => {
println("I was asking for lub because of this.")
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index d9426510ee76f9703514df4219cff8761db26995..56239d319dca67c9614f0e7d9dd97a7640c8da49 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -9,121 +9,150 @@ object FunctionClosure extends Pass {
val description = "Closing function with its scoping variables"
- private var enclosingPreconditions: List[Expr] = Nil
-
private var pathConstraints: List[Expr] = Nil
+ private var enclosingLets: List[(Identifier, Expr)] = Nil
private var newFunDefs: Map[FunDef, FunDef] = Map()
+ private var topLevelFuns: Set[FunDef] = Set()
def apply(program: Program): Program = {
newFunDefs = Map()
val funDefs = program.definedFunctions
funDefs.foreach(fd => {
- enclosingPreconditions = fd.precondition.toList
pathConstraints = fd.precondition.toList
- fd.body = fd.body.map(b => functionClosure(b, fd.args.map(_.id).toSet))
- fd.postcondition = fd.postcondition.map(b => functionClosure(b, fd.args.map(_.id).toSet))
+ fd.body = fd.body.map(b => functionClosure(b, fd.args.map(_.id).toSet, Map(), Map()))
})
- program
+ val Program(id, ObjectDef(objId, defs, invariants)) = program
+ Program(id, ObjectDef(objId, defs ++ topLevelFuns, invariants))
}
- private def functionClosure(expr: Expr, bindedVars: Set[Identifier]): Expr = expr match {
+ private def functionClosure(expr: Expr, bindedVars: Set[Identifier], id2freshId: Map[Identifier, Identifier], fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = expr match {
case l @ LetDef(fd, rest) => {
-
- val id = fd.id
- val rt = fd.returnType
- val varDecl = fd.args
- val precondition = fd.precondition
- val postcondition = fd.postcondition
-
- val bodyVars: Set[Identifier] = variablesOf(fd.body.getOrElse(BooleanLiteral(true))) ++
- variablesOf(precondition.getOrElse(BooleanLiteral(true))) ++
- variablesOf(postcondition.getOrElse(BooleanLiteral(true)))
-
- val capturedVars = bodyVars.intersect(bindedVars)// this should be the variable used that are in the scope
- val (constraints, allCapturedVars) = filterConstraints(capturedVars) //all relevant path constraints
- val capturedVarsWithConstraints = allCapturedVars.toSeq
-
- val freshVars: Map[Identifier, Identifier] = capturedVarsWithConstraints.map(v => (v, FreshIdentifier(v.name).setType(v.getType))).toMap
- val freshVarsExpr: Map[Expr, Expr] = freshVars.map(p => (p._1.toVariable, p._2.toVariable))
-
- val extraVarDecls = freshVars.map{ case (_, v2) => VarDecl(v2, v2.getType) }
- val newVarDecls = varDecl ++ extraVarDecls
- val newFunId = FreshIdentifier(id.name)
- val newFunDef = new FunDef(newFunId, rt, newVarDecls).setPosInfo(fd)
+ val capturedVars: Set[Identifier] = bindedVars.diff(enclosingLets.map(_._1).toSet)
+ val capturedConstraints: Set[Expr] = pathConstraints.toSet
+
+ val freshIds: Map[Identifier, Identifier] = capturedVars.map(id => (id, FreshIdentifier(id.name).setType(id.getType))).toMap
+ val freshVars: Map[Expr, Expr] = freshIds.map(p => (p._1.toVariable, p._2.toVariable))
+
+ val extraVarDeclOldIds: Seq[Identifier] = capturedVars.toSeq
+ val extraVarDeclFreshIds: Seq[Identifier] = extraVarDeclOldIds.map(freshIds(_))
+ val extraVarDecls: Seq[VarDecl] = extraVarDeclFreshIds.map(id => VarDecl(id, id.getType))
+ val newVarDecls: Seq[VarDecl] = fd.args ++ extraVarDecls
+ val newBindedVars: Set[Identifier] = bindedVars ++ fd.args.map(_.id)
+ val newFunId = FreshIdentifier(fd.id.name)
+
+ val newFunDef = new FunDef(newFunId, fd.returnType, newVarDecls).setPosInfo(fd)
+ topLevelFuns += newFunDef
newFunDef.fromLoop = fd.fromLoop
newFunDef.parent = fd.parent
newFunDef.addAnnotation(fd.annotations.toSeq:_*)
- val freshPrecondition = precondition.map(expr => replace(freshVarsExpr, expr))
- val freshPostcondition = postcondition.map(expr => replace(freshVarsExpr, expr))
- val freshBody = fd.body.map(b => replace(freshVarsExpr, b))
- val freshConstraints = constraints.map(expr => replace(freshVarsExpr, expr))
-
- def substFunInvocInDef(expr: Expr): Option[Expr] = expr match {
- case fi@FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ extraVarDecls.map(_.id.toVariable)).setPosInfo(fi))
- case _ => None
+ def introduceLets(expr: Expr, fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = {
+ val (newExpr, _) = enclosingLets.foldLeft((expr, Map[Identifier, Identifier]()))((acc, p) => {
+ val newId = FreshIdentifier(p._1.name).setType(p._1.getType)
+ val newMap = acc._2 + (p._1 -> newId)
+ val newBody = functionClosure(acc._1, newBindedVars, freshIds ++ newMap, fd2FreshFd)
+ (Let(newId, p._2, newBody), newMap)
+ })
+ functionClosure(newExpr, newBindedVars, freshIds, fd2FreshFd)
}
- val oldPathConstraints = pathConstraints
- pathConstraints = (precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints).map(e => replace(freshVarsExpr, e))
- val recPrecondition = freshConstraints match { //Actually, we do not allow nested fundef in precondition
- case List() => freshPrecondition
- case precs => Some(And(freshPrecondition.getOrElse(BooleanLiteral(true)) +: precs))
- }
- val recBody = freshBody.map(b =>
- functionClosure(b, bindedVars ++ newVarDecls.map(_.id))
- ).map(b => searchAndReplaceDFS(substFunInvocInDef)(b))
- pathConstraints = oldPathConstraints
- newFunDef.precondition = recPrecondition
- newFunDef.body = recBody
+
+ val newPrecondition = simplifyLets(introduceLets(And((capturedConstraints ++ fd.precondition).toSeq), fd2FreshFd))
+ newFunDef.precondition = if(newPrecondition == BooleanLiteral(true)) None else Some(newPrecondition)
+
+ val freshPostcondition = fd.postcondition.map(post => introduceLets(post, fd2FreshFd))
newFunDef.postcondition = freshPostcondition
+
+ pathConstraints = fd.precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints
+ val freshBody = fd.body.map(body => introduceLets(body, fd2FreshFd + (fd -> ((newFunDef, extraVarDeclFreshIds.map(_.toVariable))))))
+ newFunDef.body = freshBody
+ pathConstraints = pathConstraints.tail
- def substFunInvocInRest(expr: Expr): Option[Expr] = expr match {
- case fi@FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVarsWithConstraints.map(_.toVariable)).setPosInfo(fi))
- case _ => None
- }
- val recRest = searchAndReplaceDFS(substFunInvocInRest)(functionClosure(rest, bindedVars))
- LetDef(newFunDef, recRest).setType(l.getType)
+ val freshRest = functionClosure(rest, bindedVars, id2freshId, fd2FreshFd + (fd ->
+ ((newFunDef, extraVarDeclOldIds.map(id => id2freshId.get(id).getOrElse(id).toVariable)))))
+ freshRest.setType(l.getType)
}
case l @ Let(i,e,b) => {
- val re = functionClosure(e, bindedVars)
- pathConstraints ::= Equals(Variable(i), re)
- val rb = functionClosure(b, bindedVars + i)
- pathConstraints = pathConstraints.tail
+ val re = functionClosure(e, bindedVars, id2freshId, fd2FreshFd)
+ //we need the enclosing lets to always refer to the original ids, because it might be expand later in a highly nested function
+ enclosingLets ::= (i, replace(id2freshId.map(p => (p._2.toVariable, p._1.toVariable)), re))
+ //pathConstraints :: Equals(i.toVariable, re)
+ val rb = functionClosure(b, bindedVars + i, id2freshId, fd2FreshFd)
+ enclosingLets = enclosingLets.tail
+ //pathConstraints = pathConstraints.tail
Let(i, re, rb).setType(l.getType)
}
+ case i @ IfExpr(cond,then,elze) => {
+ /*
+ when acumulating path constraints, take the condition without closing it first, so this
+ might not work well with nested fundef in if then else condition
+ */
+ val rCond = functionClosure(cond, bindedVars, id2freshId, fd2FreshFd)
+ pathConstraints ::= cond//rCond
+ val rThen = functionClosure(then, bindedVars, id2freshId, fd2FreshFd)
+ pathConstraints = pathConstraints.tail
+ pathConstraints ::= Not(cond)//Not(rCond)
+ val rElze = functionClosure(elze, bindedVars, id2freshId, fd2FreshFd)
+ pathConstraints = pathConstraints.tail
+ IfExpr(rCond, rThen, rElze).setType(i.getType)
+ }
+ case fi @ FunctionInvocation(fd, args) => fd2FreshFd.get(fd) match {
+ case None => FunctionInvocation(fd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd))).setPosInfo(fi)
+ case Some((nfd, extraArgs)) =>
+ FunctionInvocation(nfd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd)) ++ extraArgs).setPosInfo(fi)
+ }
case n @ NAryOperator(args, recons) => {
- var change = false
- val rargs = args.map(a => functionClosure(a, bindedVars))
+ val rargs = args.map(a => functionClosure(a, bindedVars, id2freshId, fd2FreshFd))
recons(rargs).setType(n.getType)
}
case b @ BinaryOperator(t1,t2,recons) => {
- val r1 = functionClosure(t1, bindedVars)
- val r2 = functionClosure(t2, bindedVars)
+ val r1 = functionClosure(t1, bindedVars, id2freshId, fd2FreshFd)
+ val r2 = functionClosure(t2, bindedVars, id2freshId, fd2FreshFd)
recons(r1,r2).setType(b.getType)
}
case u @ UnaryOperator(t,recons) => {
- val r = functionClosure(t, bindedVars)
+ val r = functionClosure(t, bindedVars, id2freshId, fd2FreshFd)
recons(r).setType(u.getType)
}
- case i @ IfExpr(cond,then,elze) => {
- val rCond = functionClosure(cond, bindedVars)
- pathConstraints ::= rCond
- val rThen = functionClosure(then, bindedVars)
- pathConstraints = pathConstraints.tail
- pathConstraints ::= Not(rCond)
- val rElze = functionClosure(elze, bindedVars)
- pathConstraints = pathConstraints.tail
- IfExpr(rCond, rThen, rElze).setType(i.getType)
+ case m @ MatchExpr(scrut,cses) => { //still needs to handle the new ids introduced by the patterns
+ val scrutRec = functionClosure(scrut, bindedVars, id2freshId, fd2FreshFd)
+ val csesRec = cses.map{
+ case SimpleCase(pat, rhs) => {
+ val binders = pat.binders
+ val cond = conditionForPattern(scrut, pat)
+ pathConstraints ::= cond
+ val rRhs = functionClosure(rhs, bindedVars ++ binders, id2freshId, fd2FreshFd)
+ pathConstraints = pathConstraints.tail
+ SimpleCase(pat, rRhs)
+ }
+ case GuardedCase(pat, guard, rhs) => {
+ val binders = pat.binders
+ val cond = conditionForPattern(scrut, pat)
+ pathConstraints ::= cond
+ val rRhs = functionClosure(rhs, bindedVars ++ binders, id2freshId, fd2FreshFd)
+ val rGuard = functionClosure(guard, bindedVars ++ binders, id2freshId, fd2FreshFd)
+ pathConstraints = pathConstraints.tail
+ GuardedCase(pat, rGuard, rRhs)
+ }
+ }
+ val tpe = csesRec.head.rhs.getType
+ MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
}
- case m @ MatchExpr(scrut,cses) => { //TODO: will not work if there are actual nested function in cases
- //val rScrut = functionClosure(scrut, bindedVars)
- m
+ case v @ Variable(id) => id2freshId.get(id) match {
+ case None => v
+ case Some(nid) => Variable(nid)
}
case t if t.isInstanceOf[Terminal] => t
case unhandled => scala.sys.error("Non-terminal case should be handled in FunctionClosure: " + unhandled)
}
+ def freshIdInPat(pat: Pattern, id2freshId: Map[Identifier, Identifier]): Pattern = pat match {
+ case InstanceOfPattern(binder, classTypeDef) => InstanceOfPattern(binder.map(id2freshId(_)), classTypeDef)
+ case WildcardPattern(binder) => WildcardPattern(binder.map(id2freshId(_)))
+ case CaseClassPattern(binder, caseClassDef, subPatterns) => CaseClassPattern(binder.map(id2freshId(_)), caseClassDef, subPatterns.map(freshIdInPat(_, id2freshId)))
+ case TuplePattern(binder, subPatterns) => TuplePattern(binder.map(id2freshId(_)), subPatterns.map(freshIdInPat(_, id2freshId)))
+ }
+
//filter the list of constraints, only keeping those relevant to the set of variables
def filterConstraints(vars: Set[Identifier]): (List[Expr], Set[Identifier]) = {
var allVars = vars
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index eb139f824166e44feda604bd36976689a3ae7541..3cc81b703e96179337090ec69b29a1effbcf738b 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -15,11 +15,9 @@ object ImperativeCodeElimination extends Pass {
def apply(pgm: Program): Program = {
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => fd.body.map(body => {
- Logger.debug("Transforming to functional code the following function:\n" + fd, 5, "imperative")
parent = fd
val (res, scope, _) = toFunction(body)
fd.body = Some(scope(res))
- Logger.debug("Resulting functional code is:\n" + fd, 5, "imperative")
}))
pgm
}
@@ -52,8 +50,10 @@ object ImperativeCodeElimination extends Pass {
val (tRes, tScope, tFun) = toFunction(tExpr)
val (eRes, eScope, eFun) = toFunction(eExpr)
+ val iteRType = leastUpperBound(tRes.getType, eRes.getType).get
+
val modifiedVars: Seq[Identifier] = (tFun.keys ++ eFun.keys).toSet.intersect(varInScope).toSeq
- val resId = FreshIdentifier("res").setType(ite.getType)
+ val resId = FreshIdentifier("res").setType(iteRType)
val freshIds = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
val iteType = if(modifiedVars.isEmpty) resId.getType else TupleType(resId.getType +: freshIds.map(_.getType))
@@ -76,7 +76,7 @@ object ImperativeCodeElimination extends Pass {
if(freshIds.isEmpty)
Let(resId, tupleId.toVariable, body)
else
- Let(resId, TupleSelect(tupleId.toVariable, 1),
+ Let(resId, TupleSelect(tupleId.toVariable, 1).setType(iteRType),
freshIds.zipWithIndex.foldLeft(body)((b, id) =>
Let(id._1,
TupleSelect(tupleId.toVariable, id._2 + 2).setType(id._1.getType),
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index e9818f16debfb19ccdbeaec6f1212f169918990f..9af1b41e731e32ff4b25942c4ec4f6ac63f91b0a 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -32,8 +32,9 @@ object Main {
private def defaultAction(program: Program, reporter: Reporter) : Unit = {
Logger.debug("Default action on program: " + program, 3, "main")
- val passManager = new PassManager(Seq(EpsilonElimination, ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator))
+ val passManager = new PassManager(Seq(ArrayTransformation, EpsilonElimination, ImperativeCodeElimination, /*UnitElimination,*/ FunctionClosure, /*FunctionHoisting,*/ Simplificator))
val program2 = passManager.run(program)
+ assert(program2.isPure)
val analysis = new Analysis(program2, reporter)
analysis.analyse
}
diff --git a/src/main/scala/leon/PassManager.scala b/src/main/scala/leon/PassManager.scala
index bebd985778beeda1a7995ebb9917712aa7403e25..307a227ffb0ce0decb39624b1dde34bc6a589a39 100644
--- a/src/main/scala/leon/PassManager.scala
+++ b/src/main/scala/leon/PassManager.scala
@@ -8,6 +8,7 @@ class PassManager(passes: Seq[Pass]) {
passes.foldLeft(program)((pgm, pass) => {
Logger.debug("Running Pass: " + pass.description, 1, "passman")
val newPgm = pass(pgm)
+ TypeChecking(newPgm)
Logger.debug("Resulting program: " + newPgm, 3, "passman")
newPgm
})
diff --git a/src/main/scala/leon/Simplificator.scala b/src/main/scala/leon/Simplificator.scala
index 5562c75db5965e7d5f5916aa8923da065b1e3bb6..d52d6fe0d380b90424c239f3d302fb3620d502c4 100644
--- a/src/main/scala/leon/Simplificator.scala
+++ b/src/main/scala/leon/Simplificator.scala
@@ -12,9 +12,11 @@ object Simplificator extends Pass {
def apply(pgm: Program): Program = {
val allFuns = pgm.definedFunctions
- allFuns.foreach(fd => fd.body.map(body => {
- fd.body = Some(simplifyLets(body))
- }))
+ allFuns.foreach(fd => {
+ fd.body = fd.body.map(simplifyLets)
+ fd.precondition = fd.precondition.map(simplifyLets)
+ fd.postcondition = fd.postcondition.map(simplifyLets)
+ })
pgm
}
diff --git a/src/main/scala/leon/TypeChecking.scala b/src/main/scala/leon/TypeChecking.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f6d4b259f19ab5e19e462cd4ba137d39bba16917
--- /dev/null
+++ b/src/main/scala/leon/TypeChecking.scala
@@ -0,0 +1,120 @@
+package leon
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
+
+object TypeChecking extends Pass {
+
+ val description = "Type check the AST"
+
+ def apply(pgm: Program): Program = {
+ val allFuns = pgm.definedFunctions
+
+ allFuns.foreach(fd => {
+ fd.precondition.foreach(typeCheck)
+ fd.postcondition.foreach(typeCheck)
+ fd.body.foreach(typeCheck)
+ })
+
+ pgm
+ }
+
+ private def typeCheck(expr: Expr): Unit = { //expr match {
+ //quick hack
+ //searchAndReplaceDFS(e => {
+ // if(e.getType == Untyped) {
+ // println("Expression is untyped: " + e)
+ // }
+ // None
+ //})(expr)
+
+ //case l@Let(i, v, b) => {
+ // if(l.getType == Untyp
+ // val vr = transform(v)
+ // v.getType match {
+ // case ArrayType(_) => {
+ // val freshIdentifier = FreshIdentifier("t").setType(vr.getType)
+ // id2id += (i -> freshIdentifier)
+ // val br = transform(b)
+ // LetVar(freshIdentifier, vr, br)
+ // }
+ // case _ => {
+ // val br = transform(b)
+ // Let(i, vr, br)
+ // }
+ // }
+ //}
+ //case LetVar(id, e, b) => {
+ // val er = transform(e)
+ // val br = transform(b)
+ // LetVar(id, er, br)
+ //}
+ //case wh@While(c, e) => {
+ // val newWh = While(transform(c), transform(e))
+ // newWh.invariant = wh.invariant.map(i => transform(i))
+ // newWh.setPosInfo(wh)
+ //}
+
+ //case ite@IfExpr(c, t, e) => {
+ // val rc = transform(c)
+ // val rt = transform(t)
+ // val re = transform(e)
+ // IfExpr(rc, rt, re).setType(rt.getType)
+ //}
+
+ //case m @ MatchExpr(scrut, cses) => {
+ // val scrutRec = transform(scrut)
+ // val csesRec = cses.map{
+ // case SimpleCase(pat, rhs) => SimpleCase(pat, transform(rhs))
+ // case GuardedCase(pat, guard, rhs) => GuardedCase(pat, transform(guard), transform(rhs))
+ // }
+ // val tpe = csesRec.head.rhs.getType
+ // MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
+ //}
+ //case LetDef(fd, b) => {
+ // val newFd = if(fd.hasImplementation) {
+ // val body = fd.body.get
+ // val args = fd.args
+ // val newFd =
+ // if(args.exists(vd => containsArrayType(vd.tpe)) || containsArrayType(fd.returnType)) {
+ // val newArgs = args.map(vd => {
+ // val freshId = FreshIdentifier(vd.id.name).setType(transform(vd.tpe))
+ // id2id += (vd.id -> freshId)
+ // val newTpe = transform(vd.tpe)
+ // VarDecl(freshId, newTpe)
+ // })
+ // val freshFunName = FreshIdentifier(fd.id.name)
+ // val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
+ // fd2fd += (fd -> freshFunDef)
+ // freshFunDef.fromLoop = fd.fromLoop
+ // freshFunDef.parent = fd.parent
+ // freshFunDef.precondition = fd.precondition.map(transform)
+ // freshFunDef.postcondition = fd.postcondition.map(transform)
+ // freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ // freshFunDef
+ // } else fd
+ // val newBody = transform(body)
+ // newFd.body = Some(newBody)
+ // newFd
+ // } else fd
+ // val rb = transform(b)
+ // LetDef(newFd, rb)
+ //}
+ //case FunctionInvocation(fd, args) => {
+ // val rargs = args.map(transform)
+ // val rfd = fd2fd.get(fd).getOrElse(fd)
+ // FunctionInvocation(rfd, rargs)
+ //}
+
+ //case n @ NAryOperator(args, recons) => recons(args.map(transform)).setType(n.getType)
+ //case b @ BinaryOperator(a1, a2, recons) => recons(transform(a1), transform(a2)).setType(b.getType)
+ //case u @ UnaryOperator(a, recons) => recons(transform(a)).setType(u.getType)
+
+ //case v @ Variable(id) => if(id2id.isDefinedAt(id)) Variable(id2id(id)) else v
+ //case (t: Terminal) => t
+ //case unhandled => scala.sys.error("Non-terminal case should be handled in ArrayTransformation: " + unhandled)
+ }
+
+}
diff --git a/src/main/scala/leon/VerificationCondition.scala b/src/main/scala/leon/VerificationCondition.scala
index 01545bc3e87bd3606591b464f59098a5b0d8dd8c..e5556f1acf52fa3f8472556bcc66d3572c032488 100644
--- a/src/main/scala/leon/VerificationCondition.scala
+++ b/src/main/scala/leon/VerificationCondition.scala
@@ -49,6 +49,7 @@ object VCKind extends Enumeration {
val Postcondition = Value("postcond.")
val ExhaustiveMatch = Value("match.")
val MapAccess = Value("map acc.")
+ val ArrayAccess = Value("arr. acc.")
val InvariantInit = Value("inv init.")
val InvariantInd = Value("inv ind.")
val InvariantPost = Value("inv post.")
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index b64d6cb05d58ad1dd0420d27f21cfd0b3955b2bd..4d3dab3d0f84fa215a588712bfe82e57f63abb51 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -17,6 +17,7 @@ trait CodeExtraction extends Extractors {
import StructuralExtractors._
import ExpressionExtractors._
+
private lazy val setTraitSym = definitions.getClass("scala.collection.immutable.Set")
private lazy val mapTraitSym = definitions.getClass("scala.collection.immutable.Map")
private lazy val multisetTraitSym = try {
@@ -28,6 +29,10 @@ trait CodeExtraction extends Extractors {
private lazy val someClassSym = definitions.getClass("scala.Some")
private lazy val function1TraitSym = definitions.getClass("scala.Function1")
+ private lazy val arraySym = definitions.getClass("scala.Array")
+
+ def isArrayClassSym(sym: Symbol): Boolean = sym == arraySym
+
def isTuple2(sym : Symbol) : Boolean = sym == tuple2Sym
def isTuple3(sym : Symbol) : Boolean = sym == tuple3Sym
def isTuple4(sym : Symbol) : Boolean = sym == tuple4Sym
@@ -245,6 +250,7 @@ trait CodeExtraction extends Extractors {
val newParams = params.map(p => {
val ptpe = st2ps(p.tpt.tpe)
val newID = FreshIdentifier(p.name.toString).setType(ptpe)
+ owners += (Variable(newID) -> None)
varSubsts(p.symbol) = (() => Variable(newID))
VarDecl(newID, ptpe)
})
@@ -255,6 +261,8 @@ trait CodeExtraction extends Extractors {
var realBody = body
var reqCont: Option[Expr] = None
var ensCont: Option[Expr] = None
+
+ currentFunDef = funDef
realBody match {
case ExEnsuredExpression(body2, resSym, contract) => {
@@ -285,15 +293,23 @@ trait CodeExtraction extends Extractors {
case e: ImpureCodeEncounteredException => None
}
+ bodyAttempt.foreach(e =>
+ if(e.getType.isInstanceOf[ArrayType]) {
+ //println(owners)
+ //println(getOwner(e))
+ getOwner(e) match {
+ case Some(Some(fd)) if fd == funDef =>
+ case None =>
+ case _ => unit.error(realBody.pos, "Function cannot return an array that is not locally defined")
+ }
+ })
reqCont.map(e =>
if(containsLetDef(e)) {
unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
- throw ImpureCodeEncounteredException(realBody)
})
ensCont.map(e =>
if(containsLetDef(e)) {
unit.error(realBody.pos, "Function postcondition should not contain nested function definition")
- throw ImpureCodeEncounteredException(realBody)
})
funDef.body = bodyAttempt
funDef.precondition = reqCont
@@ -335,6 +351,13 @@ trait CodeExtraction extends Extractors {
}
}
+
+ private var currentFunDef: FunDef = null
+
+ //This is a bit missleading, if an expr is not mapped then it has no owner, if it is mapped to None it means
+ //that it can have any owner
+ private var owners: Map[Expr, Option[FunDef]] = Map()
+
/** Forces conversion from scalac AST to purescala AST, throws an Exception
* if impossible. If not in 'silent mode', non-pure AST nodes are reported as
* errors. */
@@ -400,6 +423,7 @@ trait CodeExtraction extends Extractors {
val newParams = params.map(p => {
val ptpe = scalaType2PureScala(unit, silent) (p.tpt.tpe)
val newID = FreshIdentifier(p.name.toString).setType(ptpe)
+ owners += (Variable(newID) -> None)
varSubsts(p.symbol) = (() => Variable(newID))
VarDecl(newID, ptpe)
})
@@ -411,6 +435,8 @@ trait CodeExtraction extends Extractors {
var reqCont: Option[Expr] = None
var ensCont: Option[Expr] = None
+ currentFunDef = funDef
+
realBody match {
case ExEnsuredExpression(body2, resSym, contract) => {
varSubsts(resSym) = (() => ResultVariable().setType(funDef.returnType))
@@ -440,15 +466,22 @@ trait CodeExtraction extends Extractors {
case e: ImpureCodeEncounteredException => None
}
- reqCont.map(e =>
+ bodyAttempt.foreach(e =>
+ if(e.getType.isInstanceOf[ArrayType]) {
+ getOwner(e) match {
+ case Some(Some(fd)) if fd == funDef =>
+ case None =>
+ case _ => unit.error(realBody.pos, "Function cannot return an array that is not locally defined")
+ }
+ })
+
+ reqCont.foreach(e =>
if(containsLetDef(e)) {
unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
- throw ImpureCodeEncounteredException(realBody)
})
- ensCont.map(e =>
+ ensCont.foreach(e =>
if(containsLetDef(e)) {
unit.error(realBody.pos, "Function postcondition should not contain nested function definition")
- throw ImpureCodeEncounteredException(realBody)
})
funDef.body = bodyAttempt
funDef.precondition = reqCont
@@ -465,429 +498,525 @@ trait CodeExtraction extends Extractors {
case _ => (tr, None)
}
- var handleRest = true
- val psExpr = nextExpr match {
- case ExTuple(tpes, exprs) => {
- val tupleType = TupleType(tpes.map(tpe => scalaType2PureScala(unit, silent)(tpe)))
- val tupleExprs = exprs.map(e => rec(e))
- Tuple(tupleExprs).setType(tupleType)
- }
- case ExTupleExtract(tuple, index) => {
- val tupleExpr = rec(tuple)
- val TupleType(tpes) = tupleExpr.getType
- if(tpes.size < index)
- throw ImpureCodeEncounteredException(tree)
- else
- TupleSelect(tupleExpr, index).setType(tpes(index-1))
- }
- case ExValDef(vs, tpt, bdy) => {
- val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
- val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
- val valTree = rec(bdy)
- val restTree = rest match {
- case Some(rst) => {
- varSubsts(vs) = (() => Variable(newID))
- val res = rec(rst)
- varSubsts.remove(vs)
- res
- }
- case None => UnitLiteral
- }
- handleRest = false
- val res = Let(newID, valTree, restTree)
- res
- }
- case dd@ExFunctionDef(n, p, t, b) => {
- val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
- defsToDefs += (dd.symbol -> funDef)
- val oldMutableVarSubst = mutableVarSubsts.toMap //take an immutable snapshot of the map
- mutableVarSubsts.clear //reseting the visible mutable vars, we do not handle mutable variable closure in nested functions
- val funDefWithBody = extractFunDef(funDef, b)
- mutableVarSubsts ++= oldMutableVarSubst
- val restTree = rest match {
- case Some(rst) => rec(rst)
- case None => UnitLiteral
- }
- defsToDefs.remove(dd.symbol)
- handleRest = false
- LetDef(funDefWithBody, restTree)
- }
- case ExVarDef(vs, tpt, bdy) => {
- val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
- val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
- val valTree = rec(bdy)
- mutableVarSubsts += (vs -> (() => Variable(newID)))
- val restTree = rest match {
- case Some(rst) => {
- varSubsts(vs) = (() => Variable(newID))
- val res = rec(rst)
- varSubsts.remove(vs)
- res
- }
- case None => UnitLiteral
- }
- handleRest = false
- val res = LetVar(newID, valTree, restTree)
- res
- }
+ val e2: Option[Expr] = nextExpr match {
+ case ExParameterlessMethodCall(t,n) => {
+ val selector = rec(t)
+ val selType = selector.getType
- case ExAssign(sym, rhs) => mutableVarSubsts.get(sym) match {
- case Some(fun) => {
- val Variable(id) = fun()
- val rhsTree = rec(rhs)
- Assignment(id, rhsTree)
- }
- case None => {
- unit.error(tr.pos, "Undeclared variable.")
- throw ImpureCodeEncounteredException(tr)
+ if(!selType.isInstanceOf[CaseClassType])
+ None
+ else {
+
+ val selDef: CaseClassDef = selType.asInstanceOf[CaseClassType].classDef
+
+ val fieldID = selDef.fields.find(_.id.name == n.toString) match {
+ case None => {
+ if(!silent)
+ unit.error(tr.pos, "Invalid method or field invocation (not a case class arg?)")
+ throw ImpureCodeEncounteredException(tr)
+ }
+ case Some(vd) => vd.id
+ }
+
+ Some(CaseClassSelector(selDef, selector, fieldID).setType(fieldID.getType))
}
}
- case wh@ExWhile(cond, body) => {
- val condTree = rec(cond)
- val bodyTree = rec(body)
- While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
- }
- case wh@ExWhileWithInvariant(cond, body, inv) => {
- val condTree = rec(cond)
- val bodyTree = rec(body)
- val invTree = rec(inv)
- val w = While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
- w.invariant = Some(invTree)
- w
- }
-
- case ExInt32Literal(v) => IntLiteral(v).setType(Int32Type)
- case ExBooleanLiteral(v) => BooleanLiteral(v).setType(BooleanType)
- case ExUnitLiteral() => UnitLiteral
+ case _ => None
+ }
+ var handleRest = true
+ val psExpr = e2 match {
+ case Some(e3) => e3
+ case None => nextExpr match {
+ case ExTuple(tpes, exprs) => {
+ val tupleType = TupleType(tpes.map(tpe => scalaType2PureScala(unit, silent)(tpe)))
+ val tupleExprs = exprs.map(e => rec(e))
+ Tuple(tupleExprs).setType(tupleType)
+ }
+ case ExTupleExtract(tuple, index) => {
+ val tupleExpr = rec(tuple)
+ val TupleType(tpes) = tupleExpr.getType
+ if(tpes.size < index)
+ throw ImpureCodeEncounteredException(tree)
+ else
+ TupleSelect(tupleExpr, index).setType(tpes(index-1))
+ }
+ case ExValDef(vs, tpt, bdy) => {
+ val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
+ val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
+ val valTree = rec(bdy)
+ handleRest = false
+ if(valTree.getType.isInstanceOf[ArrayType]) {
+ getOwner(valTree) match {
+ case None =>
+ owners += (Variable(newID) -> Some(currentFunDef))
+ case Some(_) =>
+ unit.error(nextExpr.pos, "Cannot alias array")
+ throw ImpureCodeEncounteredException(nextExpr)
+ }
+ }
+ val restTree = rest match {
+ case Some(rst) => {
+ varSubsts(vs) = (() => Variable(newID))
+ val res = rec(rst)
+ varSubsts.remove(vs)
+ res
+ }
+ case None => UnitLiteral
+ }
+ val res = Let(newID, valTree, restTree)
+ res
+ }
+ case dd@ExFunctionDef(n, p, t, b) => {
+ val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
+ defsToDefs += (dd.symbol -> funDef)
+ val oldMutableVarSubst = mutableVarSubsts.toMap //take an immutable snapshot of the map
+ val oldCurrentFunDef = currentFunDef
+ mutableVarSubsts.clear //reseting the visible mutable vars, we do not handle mutable variable closure in nested functions
+ val funDefWithBody = extractFunDef(funDef, b)
+ mutableVarSubsts ++= oldMutableVarSubst
+ currentFunDef = oldCurrentFunDef
+ val restTree = rest match {
+ case Some(rst) => rec(rst)
+ case None => UnitLiteral
+ }
+ defsToDefs.remove(dd.symbol)
+ handleRest = false
+ LetDef(funDefWithBody, restTree)
+ }
+ case ExVarDef(vs, tpt, bdy) => {
+ val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
+ //binderTpe match {
+ // case ArrayType(_) =>
+ // unit.error(tree.pos, "Cannot declare array variables, only val are alllowed")
+ // throw ImpureCodeEncounteredException(tree)
+ // case _ =>
+ //}
+ val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
+ val valTree = rec(bdy)
+ mutableVarSubsts += (vs -> (() => Variable(newID)))
+ handleRest = false
+ if(valTree.getType.isInstanceOf[ArrayType]) {
+ getOwner(valTree) match {
+ case None =>
+ owners += (Variable(newID) -> Some(currentFunDef))
+ case Some(_) =>
+ unit.error(nextExpr.pos, "Cannot alias array")
+ throw ImpureCodeEncounteredException(nextExpr)
+ }
+ }
+ val restTree = rest match {
+ case Some(rst) => {
+ varSubsts(vs) = (() => Variable(newID))
+ val res = rec(rst)
+ varSubsts.remove(vs)
+ res
+ }
+ case None => UnitLiteral
+ }
+ val res = LetVar(newID, valTree, restTree)
+ res
+ }
- case ExTyped(e,tpt) => rec(e)
- case ExIdentifier(sym,tpt) => varSubsts.get(sym) match {
- case Some(fun) => fun()
- case None => mutableVarSubsts.get(sym) match {
- case Some(fun) => fun()
+ case ExAssign(sym, rhs) => mutableVarSubsts.get(sym) match {
+ case Some(fun) => {
+ val Variable(id) = fun()
+ val rhsTree = rec(rhs)
+ if(rhsTree.getType.isInstanceOf[ArrayType]) {
+ getOwner(rhsTree) match {
+ case None =>
+ case Some(_) =>
+ unit.error(nextExpr.pos, "Cannot alias array")
+ throw ImpureCodeEncounteredException(nextExpr)
+ }
+ }
+ Assignment(id, rhsTree)
+ }
case None => {
- unit.error(tr.pos, "Unidentified variable.")
+ unit.error(tr.pos, "Undeclared variable.")
throw ImpureCodeEncounteredException(tr)
}
}
- }
- case epsi@ExEpsilonExpression(tpe, varSym, predBody) => {
- val pstpe = scalaType2PureScala(unit, silent)(tpe)
- val previousVarSubst: Option[Function0[Expr]] = varSubsts.get(varSym) //save the previous in case of nested epsilon
- varSubsts(varSym) = (() => EpsilonVariable((epsi.pos.line, epsi.pos.column)).setType(pstpe))
- val c1 = rec(predBody)
- previousVarSubst match {
- case Some(f) => varSubsts(varSym) = f
- case None => varSubsts.remove(varSym)
- }
- if(containsEpsilon(c1)) {
- unit.error(epsi.pos, "Usage of nested epsilon is not allowed.")
- throw ImpureCodeEncounteredException(epsi)
- }
- Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
- }
- case ExSomeConstruction(tpe, arg) => {
- // println("Got Some !" + tpe + ":" + arg)
- val underlying = scalaType2PureScala(unit, silent)(tpe)
- OptionSome(rec(arg)).setType(OptionType(underlying))
- }
- case ExCaseClassConstruction(tpt, args) => {
- val cctype = scalaType2PureScala(unit, silent)(tpt.tpe)
- if(!cctype.isInstanceOf[CaseClassType]) {
- if(!silent) {
- unit.error(tr.pos, "Construction of a non-case class.")
+ case wh@ExWhile(cond, body) => {
+ val condTree = rec(cond)
+ val bodyTree = rec(body)
+ While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
+ }
+ case wh@ExWhileWithInvariant(cond, body, inv) => {
+ val condTree = rec(cond)
+ val bodyTree = rec(body)
+ val invTree = rec(inv)
+ val w = While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
+ w.invariant = Some(invTree)
+ w
+ }
+
+ case ExInt32Literal(v) => IntLiteral(v).setType(Int32Type)
+ case ExBooleanLiteral(v) => BooleanLiteral(v).setType(BooleanType)
+ case ExUnitLiteral() => UnitLiteral
+
+ case ExTyped(e,tpt) => rec(e)
+ case ExIdentifier(sym,tpt) => varSubsts.get(sym) match {
+ case Some(fun) => fun()
+ case None => mutableVarSubsts.get(sym) match {
+ case Some(fun) => fun()
+ case None => {
+ unit.error(tr.pos, "Unidentified variable.")
+ throw ImpureCodeEncounteredException(tr)
+ }
}
- throw ImpureCodeEncounteredException(tree)
}
- val nargs = args.map(rec(_))
- val cct = cctype.asInstanceOf[CaseClassType]
- CaseClass(cct.classDef, nargs).setType(cct)
- }
- case ExAnd(l, r) => And(rec(l), rec(r)).setType(BooleanType)
- case ExOr(l, r) => Or(rec(l), rec(r)).setType(BooleanType)
- case ExNot(e) => Not(rec(e)).setType(BooleanType)
- case ExUMinus(e) => UMinus(rec(e)).setType(Int32Type)
- case ExPlus(l, r) => Plus(rec(l), rec(r)).setType(Int32Type)
- case ExMinus(l, r) => Minus(rec(l), rec(r)).setType(Int32Type)
- case ExTimes(l, r) => Times(rec(l), rec(r)).setType(Int32Type)
- case ExDiv(l, r) => Division(rec(l), rec(r)).setType(Int32Type)
- case ExMod(l, r) => Modulo(rec(l), rec(r)).setType(Int32Type)
- case ExEquals(l, r) => {
- val rl = rec(l)
- val rr = rec(r)
- ((rl.getType,rr.getType) match {
- case (SetType(_), SetType(_)) => SetEquals(rl, rr)
- case (BooleanType, BooleanType) => Iff(rl, rr)
- case (_, _) => Equals(rl, rr)
- }).setType(BooleanType)
- }
- case ExNotEquals(l, r) => Not(Equals(rec(l), rec(r)).setType(BooleanType)).setType(BooleanType)
- case ExGreaterThan(l, r) => GreaterThan(rec(l), rec(r)).setType(BooleanType)
- case ExGreaterEqThan(l, r) => GreaterEquals(rec(l), rec(r)).setType(BooleanType)
- case ExLessThan(l, r) => LessThan(rec(l), rec(r)).setType(BooleanType)
- case ExLessEqThan(l, r) => LessEquals(rec(l), rec(r)).setType(BooleanType)
- case ExFiniteSet(tt, args) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- FiniteSet(args.map(rec(_))).setType(SetType(underlying))
- }
- case ExFiniteMultiset(tt, args) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- FiniteMultiset(args.map(rec(_))).setType(MultisetType(underlying))
- }
- case ExEmptySet(tt) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- EmptySet(underlying).setType(SetType(underlying))
- }
- case ExEmptyMultiset(tt) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- EmptyMultiset(underlying).setType(MultisetType(underlying))
- }
- case ExEmptyMap(ft, tt) => {
- val fromUnderlying = scalaType2PureScala(unit, silent)(ft.tpe)
- val toUnderlying = scalaType2PureScala(unit, silent)(tt.tpe)
- EmptyMap(fromUnderlying, toUnderlying).setType(MapType(fromUnderlying, toUnderlying))
- }
- case ExSetMin(t) => {
- val set = rec(t)
- if(!set.getType.isInstanceOf[SetType]) {
- if(!silent) unit.error(t.pos, "Min should be computed on a set.")
- throw ImpureCodeEncounteredException(tree)
+ case epsi@ExEpsilonExpression(tpe, varSym, predBody) => {
+ val pstpe = scalaType2PureScala(unit, silent)(tpe)
+ val previousVarSubst: Option[Function0[Expr]] = varSubsts.get(varSym) //save the previous in case of nested epsilon
+ varSubsts(varSym) = (() => EpsilonVariable((epsi.pos.line, epsi.pos.column)).setType(pstpe))
+ val c1 = rec(predBody)
+ previousVarSubst match {
+ case Some(f) => varSubsts(varSym) = f
+ case None => varSubsts.remove(varSym)
+ }
+ if(containsEpsilon(c1)) {
+ unit.error(epsi.pos, "Usage of nested epsilon is not allowed.")
+ throw ImpureCodeEncounteredException(epsi)
+ }
+ Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
}
- SetMin(set).setType(set.getType.asInstanceOf[SetType].base)
- }
- case ExSetMax(t) => {
- val set = rec(t)
- if(!set.getType.isInstanceOf[SetType]) {
- if(!silent) unit.error(t.pos, "Max should be computed on a set.")
- throw ImpureCodeEncounteredException(tree)
+ case ExSomeConstruction(tpe, arg) => {
+ // println("Got Some !" + tpe + ":" + arg)
+ val underlying = scalaType2PureScala(unit, silent)(tpe)
+ OptionSome(rec(arg)).setType(OptionType(underlying))
}
- SetMax(set).setType(set.getType.asInstanceOf[SetType].base)
- }
- case ExUnion(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SetUnion(rl, rr).setType(s)
- case m @ MultisetType(_) => MultisetUnion(rl, rr).setType(m)
- case _ => {
- if(!silent) unit.error(tree.pos, "Union of non set/multiset expressions.")
+ case ExCaseClassConstruction(tpt, args) => {
+ val cctype = scalaType2PureScala(unit, silent)(tpt.tpe)
+ if(!cctype.isInstanceOf[CaseClassType]) {
+ if(!silent) {
+ unit.error(tr.pos, "Construction of a non-case class.")
+ }
throw ImpureCodeEncounteredException(tree)
}
+ val nargs = args.map(rec(_))
+ val cct = cctype.asInstanceOf[CaseClassType]
+ CaseClass(cct.classDef, nargs).setType(cct)
}
- }
- case ExIntersection(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SetIntersection(rl, rr).setType(s)
- case m @ MultisetType(_) => MultisetIntersection(rl, rr).setType(m)
- case _ => {
- if(!silent) unit.error(tree.pos, "Intersection of non set/multiset expressions.")
+ case ExAnd(l, r) => And(rec(l), rec(r)).setType(BooleanType)
+ case ExOr(l, r) => Or(rec(l), rec(r)).setType(BooleanType)
+ case ExNot(e) => Not(rec(e)).setType(BooleanType)
+ case ExUMinus(e) => UMinus(rec(e)).setType(Int32Type)
+ case ExPlus(l, r) => Plus(rec(l), rec(r)).setType(Int32Type)
+ case ExMinus(l, r) => Minus(rec(l), rec(r)).setType(Int32Type)
+ case ExTimes(l, r) => Times(rec(l), rec(r)).setType(Int32Type)
+ case ExDiv(l, r) => Division(rec(l), rec(r)).setType(Int32Type)
+ case ExMod(l, r) => Modulo(rec(l), rec(r)).setType(Int32Type)
+ case ExEquals(l, r) => {
+ val rl = rec(l)
+ val rr = rec(r)
+ ((rl.getType,rr.getType) match {
+ case (SetType(_), SetType(_)) => SetEquals(rl, rr)
+ case (BooleanType, BooleanType) => Iff(rl, rr)
+ case (_, _) => Equals(rl, rr)
+ }).setType(BooleanType)
+ }
+ case ExNotEquals(l, r) => Not(Equals(rec(l), rec(r)).setType(BooleanType)).setType(BooleanType)
+ case ExGreaterThan(l, r) => GreaterThan(rec(l), rec(r)).setType(BooleanType)
+ case ExGreaterEqThan(l, r) => GreaterEquals(rec(l), rec(r)).setType(BooleanType)
+ case ExLessThan(l, r) => LessThan(rec(l), rec(r)).setType(BooleanType)
+ case ExLessEqThan(l, r) => LessEquals(rec(l), rec(r)).setType(BooleanType)
+ case ExFiniteSet(tt, args) => {
+ val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ FiniteSet(args.map(rec(_))).setType(SetType(underlying))
+ }
+ case ExFiniteMultiset(tt, args) => {
+ val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ FiniteMultiset(args.map(rec(_))).setType(MultisetType(underlying))
+ }
+ case ExEmptySet(tt) => {
+ val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ EmptySet(underlying).setType(SetType(underlying))
+ }
+ case ExEmptyMultiset(tt) => {
+ val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ EmptyMultiset(underlying).setType(MultisetType(underlying))
+ }
+ case ExEmptyMap(ft, tt) => {
+ val fromUnderlying = scalaType2PureScala(unit, silent)(ft.tpe)
+ val toUnderlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ EmptyMap(fromUnderlying, toUnderlying).setType(MapType(fromUnderlying, toUnderlying))
+ }
+ case ExSetMin(t) => {
+ val set = rec(t)
+ if(!set.getType.isInstanceOf[SetType]) {
+ if(!silent) unit.error(t.pos, "Min should be computed on a set.")
throw ImpureCodeEncounteredException(tree)
}
+ SetMin(set).setType(set.getType.asInstanceOf[SetType].base)
}
- }
- case ExSetContains(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => ElementOfSet(rr, rl)
- case _ => {
- if(!silent) unit.error(tree.pos, ".contains on non set expression.")
+ case ExSetMax(t) => {
+ val set = rec(t)
+ if(!set.getType.isInstanceOf[SetType]) {
+ if(!silent) unit.error(t.pos, "Max should be computed on a set.")
throw ImpureCodeEncounteredException(tree)
}
+ SetMax(set).setType(set.getType.asInstanceOf[SetType].base)
}
- }
- case ExSetSubset(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SubsetOf(rl, rr)
- case _ => {
- if(!silent) unit.error(tree.pos, "Subset on non set expression.")
- throw ImpureCodeEncounteredException(tree)
+ case ExUnion(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SetUnion(rl, rr).setType(s)
+ case m @ MultisetType(_) => MultisetUnion(rl, rr).setType(m)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Union of non set/multiset expressions.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExSetMinus(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SetDifference(rl, rr).setType(s)
- case m @ MultisetType(_) => MultisetDifference(rl, rr).setType(m)
- case _ => {
- if(!silent) unit.error(tree.pos, "Difference of non set/multiset expressions.")
- throw ImpureCodeEncounteredException(tree)
+ case ExIntersection(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SetIntersection(rl, rr).setType(s)
+ case m @ MultisetType(_) => MultisetIntersection(rl, rr).setType(m)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Intersection of non set/multiset expressions.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExSetCard(t) => {
- val rt = rec(t)
- rt.getType match {
- case s @ SetType(_) => SetCardinality(rt)
- case m @ MultisetType(_) => MultisetCardinality(rt)
- case _ => {
- if(!silent) unit.error(tree.pos, "Cardinality of non set/multiset expressions.")
- throw ImpureCodeEncounteredException(tree)
+ case ExSetContains(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => ElementOfSet(rr, rl)
+ case _ => {
+ if(!silent) unit.error(tree.pos, ".contains on non set expression.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExMultisetToSet(t) => {
- val rt = rec(t)
- rt.getType match {
- case m @ MultisetType(u) => MultisetToSet(rt).setType(SetType(u))
- case _ => {
- if(!silent) unit.error(tree.pos, "toSet can only be applied to multisets.")
- throw ImpureCodeEncounteredException(tree)
+ case ExSetSubset(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SubsetOf(rl, rr)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Subset on non set expression.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExMapUpdated(m,f,t) => {
- val rm = rec(m)
- val rf = rec(f)
- val rt = rec(t)
- val newSingleton = SingletonMap(rf, rt).setType(rm.getType)
- rm.getType match {
- case MapType(ft, tt) =>
- MapUnion(rm, FiniteMap(Seq(newSingleton)).setType(rm.getType)).setType(rm.getType)
- case _ => {
- if (!silent) unit.error(tree.pos, "updated can only be applied to maps.")
- throw ImpureCodeEncounteredException(tree)
+ case ExSetMinus(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SetDifference(rl, rr).setType(s)
+ case m @ MultisetType(_) => MultisetDifference(rl, rr).setType(m)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Difference of non set/multiset expressions.")
+ throw ImpureCodeEncounteredException(tree)
+ }
+ }
+ }
+ case ExSetCard(t) => {
+ val rt = rec(t)
+ rt.getType match {
+ case s @ SetType(_) => SetCardinality(rt)
+ case m @ MultisetType(_) => MultisetCardinality(rt)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Cardinality of non set/multiset expressions.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExMapIsDefinedAt(m,k) => {
- val rm = rec(m)
- val rk = rec(k)
- MapIsDefinedAt(rm, rk)
- }
-
- case ExPlusPlusPlus(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- MultisetPlus(rl, rr).setType(rl.getType)
- }
- case app@ExApply(lhs,args) => {
- val rlhs = rec(lhs)
- val rargs = args map rec
- rlhs.getType match {
- case MapType(_,tt) =>
- assert(rargs.size == 1)
- MapGet(rlhs, rargs.head).setType(tt).setPosInfo(app.pos.line, app.pos.column)
- case FunctionType(fts, tt) => {
- rlhs match {
- case Variable(id) =>
- AnonymousFunctionInvocation(id, rargs).setType(tt)
- case _ => {
- if (!silent) unit.error(tree.pos, "apply on non-variable or non-map expression")
- throw ImpureCodeEncounteredException(tree)
- }
+ case ExMultisetToSet(t) => {
+ val rt = rec(t)
+ rt.getType match {
+ case m @ MultisetType(u) => MultisetToSet(rt).setType(SetType(u))
+ case _ => {
+ if(!silent) unit.error(tree.pos, "toSet can only be applied to multisets.")
+ throw ImpureCodeEncounteredException(tree)
}
}
- case _ => {
- if (!silent) unit.error(tree.pos, "apply on unexpected type")
- throw ImpureCodeEncounteredException(tree)
+ }
+ case up@ExUpdated(m,f,t) => {
+ val rm = rec(m)
+ val rf = rec(f)
+ val rt = rec(t)
+ rm.getType match {
+ case MapType(ft, tt) => {
+ val newSingleton = SingletonMap(rf, rt).setType(rm.getType)
+ MapUnion(rm, FiniteMap(Seq(newSingleton)).setType(rm.getType)).setType(rm.getType)
+ }
+ case ArrayType(bt) => {
+ ArrayUpdated(rm, rf, rt).setType(rm.getType).setPosInfo(up.pos.line, up.pos.column)
+ }
+ case _ => {
+ if (!silent) unit.error(tree.pos, "updated can only be applied to maps.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExIfThenElse(t1,t2,t3) => {
- val r1 = rec(t1)
- val r2 = rec(t2)
- val r3 = rec(t3)
- IfExpr(r1, r2, r3).setType(leastUpperBound(r2.getType, r3.getType))
- }
-
- case ExIsInstanceOf(tt, cc) => {
- val ccRec = rec(cc)
- val checkType = scalaType2PureScala(unit, silent)(tt.tpe)
- checkType match {
- case CaseClassType(ccd) => {
- val rootType: ClassTypeDef = if(ccd.parent != None) ccd.parent.get else ccd
- if(!ccRec.getType.isInstanceOf[ClassType]) {
- unit.error(tr.pos, "isInstanceOf can only be used with a case class")
- throw ImpureCodeEncounteredException(tr)
- } else {
- val testedExprType = ccRec.getType.asInstanceOf[ClassType].classDef
- val testedExprRootType: ClassTypeDef = if(testedExprType.parent != None) testedExprType.parent.get else testedExprType
+ case ExMapIsDefinedAt(m,k) => {
+ val rm = rec(m)
+ val rk = rec(k)
+ MapIsDefinedAt(rm, rk)
+ }
- if(rootType != testedExprRootType) {
- unit.error(tr.pos, "isInstanceOf can only be used with compatible case classes")
- throw ImpureCodeEncounteredException(tr)
- } else {
- CaseClassInstanceOf(ccd, ccRec)
+ case ExPlusPlusPlus(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ MultisetPlus(rl, rr).setType(rl.getType)
+ }
+ case app@ExApply(lhs,args) => {
+ val rlhs = rec(lhs)
+ val rargs = args map rec
+ rlhs.getType match {
+ case MapType(_,tt) =>
+ assert(rargs.size == 1)
+ MapGet(rlhs, rargs.head).setType(tt).setPosInfo(app.pos.line, app.pos.column)
+ case FunctionType(fts, tt) => {
+ rlhs match {
+ case Variable(id) =>
+ AnonymousFunctionInvocation(id, rargs).setType(tt)
+ case _ => {
+ if (!silent) unit.error(tree.pos, "apply on non-variable or non-map expression")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
+ case ArrayType(bt) => {
+ assert(rargs.size == 1)
+ ArraySelect(rlhs, rargs.head).setType(bt).setPosInfo(app.pos.line, app.pos.column)
+ }
+ case _ => {
+ if (!silent) unit.error(tree.pos, "apply on unexpected type")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
- case _ => {
- unit.error(tr.pos, "isInstanceOf can only be used with a case class")
- throw ImpureCodeEncounteredException(tr)
+ }
+ // for now update only occurs on Array. later we might have to distinguished depending on the type of the lhs
+ case update@ExUpdate(lhs, index, newValue) => {
+ val lhsRec = rec(lhs)
+ lhsRec match {
+ case Variable(_) =>
+ case _ => {
+ unit.error(tree.pos, "array update only works on variables")
+ throw ImpureCodeEncounteredException(tree)
+ }
+ }
+ getOwner(lhsRec) match {
+ case Some(Some(fd)) if fd != currentFunDef =>
+ unit.error(nextExpr.pos, "cannot update an array that is not defined locally")
+ throw ImpureCodeEncounteredException(nextExpr)
+ case Some(None) =>
+ unit.error(nextExpr.pos, "cannot update an array that is not defined locally")
+ throw ImpureCodeEncounteredException(nextExpr)
+ case Some(_) =>
+ case None => sys.error("This array: " + lhsRec + " should have had an owner")
}
+ val indexRec = rec(index)
+ val newValueRec = rec(newValue)
+ ArrayUpdate(lhsRec, indexRec, newValueRec).setPosInfo(update.pos.line, update.pos.column)
}
- }
-
- case lc @ ExLocalCall(sy,nm,ar) => {
- if(defsToDefs.keysIterator.find(_ == sy).isEmpty) {
- if(!silent)
- unit.error(tr.pos, "Invoking an invalid function.")
- throw ImpureCodeEncounteredException(tr)
+ case ExArrayLength(t) => {
+ val rt = rec(t)
+ ArrayLength(rt)
}
- val fd = defsToDefs(sy)
- FunctionInvocation(fd, ar.map(rec(_))).setType(fd.returnType).setPosInfo(lc.pos.line,lc.pos.column)
- }
- case pm @ ExPatternMatching(sel, cses) => {
- val rs = rec(sel)
- val rc = cses.map(rewriteCaseDef(_))
- val rt: purescala.TypeTrees.TypeTree = rc.map(_.rhs.getType).reduceLeft(leastUpperBound(_,_))
- MatchExpr(rs, rc).setType(rt).setPosInfo(pm.pos.line,pm.pos.column)
- }
-
- // this one should stay after all others, cause it also catches UMinus
- // and Not, for instance.
- case ExParameterlessMethodCall(t,n) => {
- val selector = rec(t)
- val selType = selector.getType
-
- if(!selType.isInstanceOf[CaseClassType]) {
- if(!silent)
- unit.error(tr.pos, "Invalid method or field invocation (not purescala?)")
- throw ImpureCodeEncounteredException(tr)
+ case ExArrayClone(t) => {
+ val rt = rec(t)
+ ArrayClone(rt)
+ }
+ case ExArrayFill(baseType, length, defaultValue) => {
+ val underlying = scalaType2PureScala(unit, silent)(baseType.tpe)
+ val lengthRec = rec(length)
+ val defaultValueRec = rec(defaultValue)
+ ArrayFill(lengthRec, defaultValueRec).setType(ArrayType(underlying))
+ }
+ case ExIfThenElse(t1,t2,t3) => {
+ val r1 = rec(t1)
+ if(containsLetDef(r1)) {
+ unit.error(t1.pos, "Condition of if-then-else expression should not contain nested function definition")
+ throw ImpureCodeEncounteredException(t1)
+ }
+ val r2 = rec(t2)
+ val r3 = rec(t3)
+ val lub = leastUpperBound(r2.getType, r3.getType)
+ lub match {
+ case Some(lub) => IfExpr(r1, r2, r3).setType(lub)
+ case None =>
+ unit.error(nextExpr.pos, "Both branches of ifthenelse have incompatible types")
+ throw ImpureCodeEncounteredException(t1)
+ }
}
- val selDef: CaseClassDef = selType.asInstanceOf[CaseClassType].classDef
+ case ExIsInstanceOf(tt, cc) => {
+ val ccRec = rec(cc)
+ val checkType = scalaType2PureScala(unit, silent)(tt.tpe)
+ checkType match {
+ case CaseClassType(ccd) => {
+ val rootType: ClassTypeDef = if(ccd.parent != None) ccd.parent.get else ccd
+ if(!ccRec.getType.isInstanceOf[ClassType]) {
+ unit.error(tr.pos, "isInstanceOf can only be used with a case class")
+ throw ImpureCodeEncounteredException(tr)
+ } else {
+ val testedExprType = ccRec.getType.asInstanceOf[ClassType].classDef
+ val testedExprRootType: ClassTypeDef = if(testedExprType.parent != None) testedExprType.parent.get else testedExprType
+
+ if(rootType != testedExprRootType) {
+ unit.error(tr.pos, "isInstanceOf can only be used with compatible case classes")
+ throw ImpureCodeEncounteredException(tr)
+ } else {
+ CaseClassInstanceOf(ccd, ccRec)
+ }
+ }
+ }
+ case _ => {
+ unit.error(tr.pos, "isInstanceOf can only be used with a case class")
+ throw ImpureCodeEncounteredException(tr)
+ }
+ }
+ }
- val fieldID = selDef.fields.find(_.id.name == n.toString) match {
- case None => {
+ case lc @ ExLocalCall(sy,nm,ar) => {
+ if(defsToDefs.keysIterator.find(_ == sy).isEmpty) {
if(!silent)
- unit.error(tr.pos, "Invalid method or field invocation (not a case class arg?)")
+ unit.error(tr.pos, "Invoking an invalid function.")
throw ImpureCodeEncounteredException(tr)
}
- case Some(vd) => vd.id
+ val fd = defsToDefs(sy)
+ FunctionInvocation(fd, ar.map(rec(_))).setType(fd.returnType).setPosInfo(lc.pos.line,lc.pos.column)
+ }
+ case pm @ ExPatternMatching(sel, cses) => {
+ val rs = rec(sel)
+ val rc = cses.map(rewriteCaseDef(_))
+ val rt: purescala.TypeTrees.TypeTree = rc.map(_.rhs.getType).reduceLeft(leastUpperBound(_,_).get)
+ MatchExpr(rs, rc).setType(rt).setPosInfo(pm.pos.line,pm.pos.column)
}
- CaseClassSelector(selDef, selector, fieldID).setType(fieldID.getType)
- }
-
- // default behaviour is to complain :)
- case _ => {
- if(!silent) {
- println(tr)
- reporter.info(tr.pos, "Could not extract as PureScala.", true)
+
+ // default behaviour is to complain :)
+ case _ => {
+ if(!silent) {
+ println(tr)
+ reporter.info(tr.pos, "Could not extract as PureScala.", true)
+ }
+ throw ImpureCodeEncounteredException(tree)
}
- throw ImpureCodeEncounteredException(tree)
}
}
- if(handleRest) {
+ val res = if(handleRest) {
rest match {
case Some(rst) => {
val recRst = rec(rst)
- PBlock(Seq(psExpr), recRst).setType(recRst.getType)
+ val block = PBlock(Seq(psExpr), recRst).setType(recRst.getType)
+ block
}
case None => psExpr
}
} else {
psExpr
}
+
+ res
}
rec(tree)
}
@@ -897,6 +1026,7 @@ trait CodeExtraction extends Extractors {
def rec(tr: Type): purescala.TypeTrees.TypeTree = tr match {
case tpe if tpe == IntClass.tpe => Int32Type
case tpe if tpe == BooleanClass.tpe => BooleanType
+ case tpe if tpe == UnitClass.tpe => UnitType
case TypeRef(_, sym, btt :: Nil) if isSetTraitSym(sym) => SetType(rec(btt))
case TypeRef(_, sym, btt :: Nil) if isMultisetTraitSym(sym) => MultisetType(rec(btt))
case TypeRef(_, sym, btt :: Nil) if isOptionClassSym(sym) => OptionType(rec(btt))
@@ -906,6 +1036,7 @@ trait CodeExtraction extends Extractors {
case TypeRef(_, sym, List(t1,t2,t3,t4)) if isTuple4(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3),rec(t4)))
case TypeRef(_, sym, List(t1,t2,t3,t4,t5)) if isTuple5(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3),rec(t4),rec(t5)))
case TypeRef(_, sym, ftt :: ttt :: Nil) if isFunction1TraitSym(sym) => FunctionType(List(rec(ftt)), rec(ttt))
+ case TypeRef(_, sym, btt :: Nil) if isArrayClassSym(sym) => ArrayType(rec(btt))
case TypeRef(_, sym, Nil) if classesToClasses.keySet.contains(sym) => classDefToClassType(classesToClasses(sym))
case _ => {
if(!silent) {
@@ -928,4 +1059,27 @@ trait CodeExtraction extends Extractors {
def mkPosString(pos: scala.tools.nsc.util.Position) : String = {
pos.line + "," + pos.column
}
+
+ def getReturnedExpr(expr: Expr): Seq[Expr] = expr match {
+ case Let(_, _, rest) => getReturnedExpr(rest)
+ case LetVar(_, _, rest) => getReturnedExpr(rest)
+ case PBlock(_, rest) => getReturnedExpr(rest)
+ case IfExpr(_, then, elze) => getReturnedExpr(then) ++ getReturnedExpr(elze)
+ case _ => Seq(expr)
+ }
+
+ def getOwner(exprs: Seq[Expr]): Option[Option[FunDef]] = {
+ val exprOwners: Seq[Option[Option[FunDef]]] = exprs.map(owners.get(_))
+ if(exprOwners.exists(_ == None))
+ None
+ else if(exprOwners.exists(_ == Some(None)))
+ Some(None)
+ else if(exprOwners.exists(o1 => exprOwners.exists(o2 => o1 != o2)))
+ Some(None)
+ else
+ exprOwners(0)
+ }
+
+ def getOwner(expr: Expr): Option[Option[FunDef]] = getOwner(getReturnedExpr(expr))
+
}
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 04cece3d96670c4723fc09e13f0deaf2bf62dd09..a3313663baea11ad915e0229511f0a4426a27b5c 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -632,10 +632,13 @@ trait Extractors {
}
}
- object ExMapUpdated {
+ object ExUpdated {
def unapply(tree: Apply): Option[(Tree,Tree,Tree)] = tree match {
case Apply(TypeApply(Select(lhs, n), typeTreeList), List(from, to)) if (n.toString == "updated") =>
Some((lhs, from, to))
+ case Apply(
+ Apply(TypeApply(Select(Apply(_, Seq(lhs)), n), _), Seq(index, value)),
+ List(Apply(_, _))) if (n.toString == "updated") => Some((lhs, index, value))
case _ => None
}
}
@@ -646,6 +649,14 @@ trait Extractors {
case _ => None
}
}
+ object ExUpdate {
+ def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
+ case Apply(
+ Select(lhs, update),
+ index :: newValue :: Nil) if(update.toString == "update") => Some((lhs, index, newValue))
+ case _ => None
+ }
+ }
object ExMapIsDefinedAt {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
@@ -653,5 +664,42 @@ trait Extractors {
case _ => None
}
}
+
+ object ExArrayLength {
+ def unapply(tree: Select): Option[Tree] = tree match {
+ case Select(t, n) if (n.toString == "length") => Some(t)
+ case _ => None
+ }
+ }
+
+ object ExArrayClone {
+ def unapply(tree: Apply): Option[Tree] = tree match {
+ case Apply(Select(t, n), List()) if (n.toString == "clone") => Some(t)
+ case _ => None
+ }
+ }
+
+
+ object ExArrayFill {
+ def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
+ case Apply(
+ Apply(
+ Apply(
+ TypeApply(
+ Select(Select(Ident(scala), arrayObject), fillMethod),
+ baseType :: Nil
+ ),
+ length :: Nil
+ ),
+ defaultValue :: Nil
+ ),
+ manifest
+ ) if(scala.toString == "scala" &&
+ arrayObject.toString == "Array" &&
+ fillMethod.toString == "fill") => Some((baseType, length, defaultValue))
+ case _ => None
+ }
+ }
+
}
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index f2da8a7cef1f1f3b0290a35a260f40ceefbf6705..bc497dcdd318cdbd7809c357b811002f986908da 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -53,6 +53,7 @@ object Definitions {
def isCatamorphism(f1: FunDef) = mainObject.isCatamorphism(f1)
def caseClassDef(name: String) = mainObject.caseClassDef(name)
def allIdentifiers : Set[Identifier] = mainObject.allIdentifiers + id
+ def isPure: Boolean = definedFunctions.forall(fd => fd.body.forall(Trees.isPure) && fd.precondition.forall(Trees.isPure) && fd.postcondition.forall(Trees.isPure))
}
/** Objects work as containers for class definitions, functions (def's) and
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index d1a39f7172fafb612c2201b2c4322615a0aabdef..21a9393b142b177d49ba985988512c5dbe885c5f 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -139,8 +139,8 @@ object PrettyPrinter {
sb.append("\n")
}
- case Tuple(exprs) => ppNary(sb, exprs, "(", ", ", ")", lvl)
- case TupleSelect(t, i) => {
+ case t@Tuple(exprs) => ppNary(sb, exprs, "(", ", ", ")", lvl)
+ case s@TupleSelect(t, i) => {
pp(t, sb, lvl)
sb.append("._" + i)
sb
@@ -249,6 +249,50 @@ object PrettyPrinter {
nsb = ppNary(nsb, Seq(k), "(", ",", ")", lvl)
nsb
}
+ case ArrayLength(a) => {
+ pp(a, sb, lvl)
+ sb.append(".length")
+ }
+ case ArrayClone(a) => {
+ pp(a, sb, lvl)
+ sb.append(".clone")
+ }
+ case fill@ArrayFill(size, v) => {
+ sb.append("Array.fill(")
+ pp(size, sb, lvl)
+ sb.append(")(")
+ pp(v, sb, lvl)
+ sb.append(")")
+ }
+ case am@ArrayMake(v) => {
+ sb.append("Array.make(")
+ pp(v, sb, lvl)
+ sb.append(")")
+ }
+ case sel@ArraySelect(ar, i) => {
+ pp(ar, sb, lvl)
+ sb.append("(")
+ pp(i, sb, lvl)
+ sb.append(")")
+ }
+ case up@ArrayUpdate(ar, i, v) => {
+ pp(ar, sb, lvl)
+ sb.append("(")
+ pp(i, sb, lvl)
+ sb.append(") = ")
+ pp(v, sb, lvl)
+ }
+ case up@ArrayUpdated(ar, i, v) => {
+ pp(ar, sb, lvl)
+ sb.append(".updated(")
+ pp(i, sb, lvl)
+ sb.append(", ")
+ pp(v, sb, lvl)
+ sb.append(")")
+ }
+ case FiniteArray(exprs) => {
+ ppNary(sb, exprs, "Array(", ", ", ")", lvl)
+ }
case Distinct(exprs) => {
var nsb = sb
@@ -377,6 +421,7 @@ object PrettyPrinter {
case UnitType => sb.append("Unit")
case Int32Type => sb.append("Int")
case BooleanType => sb.append("Boolean")
+ case ArrayType(bt) => pp(bt, sb.append("Array["), lvl).append("]")
case SetType(bt) => pp(bt, sb.append("Set["), lvl).append("]")
case MapType(ft,tt) => pp(tt, pp(ft, sb.append("Map["), lvl).append(","), lvl).append("]")
case MultisetType(bt) => pp(bt, sb.append("Multiset["), lvl).append("]")
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index ee3daffb735a3fa97adb1600be050e3b3f258180..3716a41265b6399fc3ea06de189607a7415e2b8b 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -76,7 +76,13 @@ object Trees {
}
case class IfExpr(cond: Expr, then: Expr, elze: Expr) extends Expr
- case class Tuple(exprs: Seq[Expr]) extends Expr
+ case class Tuple(exprs: Seq[Expr]) extends Expr {
+ val subTpes = exprs.map(_.getType)
+ if(!subTpes.exists(_ == Untyped)) {
+ setType(TupleType(subTpes))
+ }
+
+ }
case class TupleSelect(tuple: Expr, index: Int) extends Expr
object MatchExpr {
@@ -379,6 +385,25 @@ object Trees {
val fixedType = BooleanType
}
+ /* Array operations */
+ case class ArrayFill(length: Expr, defaultValue: Expr) extends Expr
+ case class ArrayMake(defaultValue: Expr) extends Expr
+ case class ArraySelect(array: Expr, index: Expr) extends Expr with ScalacPositional
+ //the difference between ArrayUpdate and ArrayUpdated is that the former has a side effect while the latter is the function variant
+ //ArrayUpdate should be eliminated soon in the analysis while ArrayUpdated is keep all the way to the backend
+ case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends Expr with ScalacPositional with FixedType {
+ val fixedType = UnitType
+ }
+ case class ArrayUpdated(array: Expr, index: Expr, newValue: Expr) extends Expr with ScalacPositional
+ case class ArrayLength(array: Expr) extends Expr with FixedType {
+ val fixedType = Int32Type
+ }
+ case class FiniteArray(exprs: Seq[Expr]) extends Expr
+ case class ArrayClone(array: Expr) extends Expr {
+ if(array.getType != Untyped)
+ setType(array.getType)
+ }
+
/* List operations */
case class NilList(baseType: TypeTree) extends Expr with Terminal
case class Cons(head: Expr, tail: Expr) extends Expr
@@ -411,6 +436,9 @@ object Trees {
case CaseClassInstanceOf(cd, e) => Some((e, CaseClassInstanceOf(cd, _)))
case Assignment(id, e) => Some((e, Assignment(id, _)))
case TupleSelect(t, i) => Some((t, TupleSelect(_, i)))
+ case ArrayLength(a) => Some((a, ArrayLength))
+ case ArrayClone(a) => Some((a, ArrayClone))
+ case ArrayMake(t) => Some((t, ArrayMake))
case e@Epsilon(t) => Some((t, (expr: Expr) => Epsilon(expr).setType(e.getType).setPosInfo(e)))
case _ => None
}
@@ -446,6 +474,8 @@ object Trees {
case MapUnion(t1,t2) => Some((t1,t2,MapUnion))
case MapDifference(t1,t2) => Some((t1,t2,MapDifference))
case MapIsDefinedAt(t1,t2) => Some((t1,t2, MapIsDefinedAt))
+ case ArrayFill(t1, t2) => Some((t1, t2, ArrayFill))
+ case ArraySelect(t1, t2) => Some((t1, t2, ArraySelect))
case Concat(t1,t2) => Some((t1,t2,Concat))
case ListAt(t1,t2) => Some((t1,t2,ListAt))
case wh@While(t1, t2) => Some((t1,t2, (t1, t2) => While(t1, t2).setInvariant(wh.invariant).setPosInfo(wh)))
@@ -463,6 +493,9 @@ object Trees {
case FiniteSet(args) => Some((args, FiniteSet))
case FiniteMap(args) => Some((args, (as : Seq[Expr]) => FiniteMap(as.asInstanceOf[Seq[SingletonMap]])))
case FiniteMultiset(args) => Some((args, FiniteMultiset))
+ case ArrayUpdate(t1, t2, t3) => Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdate(as(0), as(1), as(2))))
+ case ArrayUpdated(t1, t2, t3) => Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdated(as(0), as(1), as(2))))
+ case FiniteArray(args) => Some((args, FiniteArray))
case Distinct(args) => Some((args, Distinct))
case Block(args, rest) => Some((args :+ rest, exprs => Block(exprs.init, exprs.last)))
case Tuple(args) => Some((args, Tuple))
@@ -598,7 +631,7 @@ object Trees {
case Some(newEx) => {
somethingChanged = true
if(newEx.getType == Untyped) {
- Settings.reporter.warning("REPLACING WITH AN UNTYPED EXPRESSION !")
+ Settings.reporter.warning("REPLACING [" + ex + "] WITH AN UNTYPED EXPRESSION !")
Settings.reporter.warning("Here's the new expression: " + newEx)
}
newEx
@@ -798,13 +831,19 @@ object Trees {
searchAndReplaceDFS(applyToTree)(expr)
}
- //checking whether the expr is pure, that is do not contains any non-pure construct: assign, while and blocks
+ //checking whether the expr is pure, that is do not contains any non-pure construct: assign, while, blocks, array, ...
+ //this is expected to be true when entering the "backend" of Leon
def isPure(expr: Expr): Boolean = {
def convert(t: Expr) : Boolean = t match {
case Block(_, _) => false
case Assignment(_, _) => false
case While(_, _) => false
case LetVar(_, _, _) => false
+ case LetDef(_, _) => false
+ case ArrayUpdate(_, _, _) => false
+ case ArrayMake(_) => false
+ case ArrayClone(_) => false
+ case Epsilon(_) => false
case _ => true
}
def combine(b1: Boolean, b2: Boolean) = b1 && b2
@@ -813,6 +852,11 @@ object Trees {
case Assignment(_, _) => false
case While(_, _) => false
case LetVar(_, _, _) => false
+ case LetDef(_, _) => false
+ case ArrayUpdate(_, _, _) => false
+ case ArrayMake(_) => false
+ case ArrayClone(_) => false
+ case Epsilon(_) => false
case _ => b
}
treeCatamorphism(convert, combine, compute, expr)
@@ -1241,6 +1285,24 @@ object Trees {
toRet
}
+ def conditionForPattern(in: Expr, pattern: Pattern) : Expr = pattern match {
+ case WildcardPattern(_) => BooleanLiteral(true)
+ case InstanceOfPattern(_,_) => scala.sys.error("InstanceOfPattern not yet supported.")
+ case CaseClassPattern(_, ccd, subps) => {
+ assert(ccd.fields.size == subps.size)
+ val pairs = ccd.fields.map(_.id).toList zip subps.toList
+ val subTests = pairs.map(p => conditionForPattern(CaseClassSelector(ccd, in, p._1), p._2))
+ val together = And(subTests)
+ And(CaseClassInstanceOf(ccd, in), together)
+ }
+ case TuplePattern(_, subps) => {
+ val TupleType(tpes) = in.getType
+ assert(tpes.size == subps.size)
+ val subTests = subps.zipWithIndex.map{case (p, i) => conditionForPattern(TupleSelect(in, i+1).setType(tpes(i)), p)}
+ And(subTests)
+ }
+ }
+
private def convertMatchToIfThenElse(expr: Expr) : Expr = {
def mapForPattern(in: Expr, pattern: Pattern) : Map[Identifier,Expr] = pattern match {
case WildcardPattern(None) => Map.empty
@@ -1270,24 +1332,6 @@ object Trees {
}
}
- def conditionForPattern(in: Expr, pattern: Pattern) : Expr = pattern match {
- case WildcardPattern(_) => BooleanLiteral(true)
- case InstanceOfPattern(_,_) => scala.sys.error("InstanceOfPattern not yet supported.")
- case CaseClassPattern(_, ccd, subps) => {
- assert(ccd.fields.size == subps.size)
- val pairs = ccd.fields.map(_.id).toList zip subps.toList
- val subTests = pairs.map(p => conditionForPattern(CaseClassSelector(ccd, in, p._1), p._2))
- val together = And(subTests)
- And(CaseClassInstanceOf(ccd, in), together)
- }
- case TuplePattern(_, subps) => {
- val TupleType(tpes) = in.getType
- assert(tpes.size == subps.size)
- val subTests = subps.zipWithIndex.map{case (p, i) => conditionForPattern(TupleSelect(in, i+1).setType(tpes(i)), p)}
- And(subTests)
- }
- }
-
def rewritePM(e: Expr) : Option[Expr] = e match {
case m @ MatchExpr(scrut, cases) => {
// println("Rewriting the following PM: " + e)
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 31947bf28177682e1376f0fd013944ef9dc37c05..01aea89f986c7263cb312763864006714581057c 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -18,7 +18,7 @@ object TypeTrees {
def setType(tt: TypeTree): self.type = _type match {
case None => _type = Some(tt); this
- case Some(o) if o != tt => scala.sys.error("Resetting type information.")
+ case Some(o) if o != tt => scala.sys.error("Resetting type information! Type [" + o + "] is modified to [" + tt)
case _ => this
}
}
@@ -47,7 +47,7 @@ object TypeTrees {
case other => other
}
- def leastUpperBound(t1: TypeTree, t2: TypeTree): TypeTree = (t1,t2) match {
+ def leastUpperBound(t1: TypeTree, t2: TypeTree): Option[TypeTree] = (t1,t2) match {
case (c1: ClassType, c2: ClassType) => {
import scala.collection.immutable.Set
var c: ClassTypeDef = c1.classDef
@@ -72,19 +72,19 @@ object TypeTrees {
}
if(found.isEmpty) {
- scala.sys.error("Asking for lub of unrelated class types : " + t1 + " and " + t2)
+ None
} else {
- classDefToClassType(found.get)
+ Some(classDefToClassType(found.get))
}
}
- case (o1, o2) if (o1 == o2) => o1
- case (o1,BottomType) => o1
- case (BottomType,o2) => o2
- case (o1,AnyType) => AnyType
- case (AnyType,o2) => AnyType
+ case (o1, o2) if (o1 == o2) => Some(o1)
+ case (o1,BottomType) => Some(o1)
+ case (BottomType,o2) => Some(o2)
+ case (o1,AnyType) => Some(AnyType)
+ case (AnyType,o2) => Some(AnyType)
- case _ => scala.sys.error("Asking for lub of unrelated types: " + t1 + " and " + t2)
+ case _ => None
}
// returns the number of distinct values that inhabit a type
@@ -100,6 +100,7 @@ object TypeTrees {
case UnitType => FiniteSize(1)
case Int32Type => InfiniteSize
case ListType(_) => InfiniteSize
+ case ArrayType(_) => InfiniteSize
case TupleType(bases) => {
val baseSizes = bases.map(domainSize(_))
baseSizes.find(_ == InfiniteSize) match {
@@ -148,6 +149,7 @@ object TypeTrees {
case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
case class OptionType(base: TypeTree) extends TypeTree
case class FunctionType(from: List[TypeTree], to: TypeTree) extends TypeTree
+ case class ArrayType(base: TypeTree) extends TypeTree
sealed abstract class ClassType extends TypeTree {
val classDef: ClassTypeDef
diff --git a/testcases/AbsFun.scala b/testcases/AbsFun.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8186824b03bca673a899a8505347c09c86e43360
--- /dev/null
+++ b/testcases/AbsFun.scala
@@ -0,0 +1,65 @@
+import leon.Utils._
+
+object AbsFun {
+
+
+ def isPositive(a : Array[Int], size : Int) : Boolean = {
+ require(a.length >= 0 && size <= a.length)
+ rec(0, a, size)
+ }
+
+ def rec(i: Int, a: Array[Int], size: Int) : Boolean = {
+ require(a.length >= 0 && size <= a.length && i >= 0)
+
+ if(i >= size) true
+ else {
+ if (a(i) < 0)
+ false
+ else
+ rec(i + 1, a, size)
+ }
+ }
+
+ def abs(tab: Array[Int]): Array[Int] = {
+ require(tab.length >= 0)
+ val t = while0(Array.fill(tab.length)(0), 0, tab)
+ t._1
+ } ensuring(res => isPositive(res, res.length))
+
+
+ def while0(t: Array[Int], k: Int, tab: Array[Int]): (Array[Int], Int) = {
+ require(tab.length >= 0 &&
+ t.length == tab.length &&
+ k >= 0 &&
+ k <= tab.length &&
+ isPositive(t, k))
+
+ if(k < tab.length) {
+ val nt = if(tab(k) < 0) {
+ t.updated(k, -tab(k))
+ } else {
+ t.updated(k, tab(k))
+ }
+ while0(nt, k+1, tab)
+ } else {
+ (t, k)
+ }
+ } ensuring(res =>
+ res._2 >= tab.length &&
+ res._1.length == tab.length &&
+ res._2 >= 0 &&
+ res._2 <= tab.length &&
+ isPositive(res._1, res._2))
+
+ def property(t: Array[Int], k: Int): Boolean = {
+ require(isPositive(t, k) && t.length >= 0 && k >= 0)
+ if(k < t.length) {
+ val nt = if(t(k) < 0) {
+ t.updated(k, -t(k))
+ } else {
+ t.updated(k, t(k))
+ }
+ isPositive(nt, k+1)
+ } else true
+ } holds
+}
diff --git a/testcases/BinarySearch.scala b/testcases/BinarySearch.scala
index 92d4cf0667fe0175b80ae0da34679e991efcc633..986ee41ae6a057065bc8520c5af010092b67b2b2 100644
--- a/testcases/BinarySearch.scala
+++ b/testcases/BinarySearch.scala
@@ -4,10 +4,10 @@ import leon.Utils._
object BinarySearch {
- def binarySearch(a: Map[Int, Int], size: Int, key: Int): Int = ({
- require(isArray(a, size) && size < 5 && sorted(a, size, 0, size - 1))
+ def binarySearch(a: Array[Int], key: Int): Int = ({
+ require(a.length > 0 && sorted(a, 0, a.length - 1))
var low = 0
- var high = size - 1
+ var high = a.length - 1
var res = -1
(while(low <= high && res == -1) {
@@ -21,13 +21,27 @@ object BinarySearch {
high = i - 1
else if(v < key)
low = i + 1
- }) invariant(0 <= low && low <= high + 1 && high < size && (if(res >= 0) a(res) == key else (!occurs(a, 0, low, key) && !occurs(a, high + 1, size, key))))
+ }) invariant(
+ res >= -1 &&
+ res < a.length &&
+ 0 <= low &&
+ low <= high + 1 &&
+ high >= -1 &&
+ high < a.length &&
+ (if (res >= 0)
+ a(res) == key else
+ (!occurs(a, 0, low, key) && !occurs(a, high + 1, a.length, key))
+ )
+ )
res
- }) ensuring(res => res >= -1 && res < size && (if(res >= 0) a(res) == key else !occurs(a, 0, size, key)))
+ }) ensuring(res =>
+ res >= -1 &&
+ res < a.length &&
+ (if(res >= 0) a(res) == key else !occurs(a, 0, a.length, key)))
- def occurs(a: Map[Int, Int], from: Int, to: Int, key: Int): Boolean = {
- require(isArray(a, to) && to < 5 && from >= 0)
+ def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
+ require(a.length >= 0 && to <= a.length && from >= 0)
def rec(i: Int): Boolean = {
require(i >= 0)
if(i >= to)
@@ -43,31 +57,16 @@ object BinarySearch {
}
- def isArray(a: Map[Int, Int], size: Int): Boolean = {
-
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size) true else {
- if(a.isDefinedAt(i)) rec(i+1) else false
- }
- }
-
- if(size < 0)
- false
- else
- rec(0)
- }
-
- def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
- require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
- val t = sortedWhile(true, l, l, u, a, size)
+ def sorted(a: Array[Int], l: Int, u: Int) : Boolean = {
+ require(a.length >= 0 && l >= 0 && l <= u && u < a.length)
+ val t = sortedWhile(true, l, l, u, a)
t._1
}
- def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
- require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Array[Int]): (Boolean, Int) = {
+ require(a.length >= 0 && l >= 0 && l <= u && u < a.length && k >= l && k <= u)
if(k < u) {
- sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a)
} else (isSorted, k)
}
}
diff --git a/testcases/BubbleSort.scala b/testcases/BubbleSort.scala
index 4e274e2707b0cff262e712ab4b78b53eee0db990..3551ebf16416f68bd932adc512177edc6f2611d8 100644
--- a/testcases/BubbleSort.scala
+++ b/testcases/BubbleSort.scala
@@ -2,44 +2,44 @@ import leon.Utils._
/* The calculus of Computation textbook */
-object Bubble {
+object BubbleSort {
- def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = ({
- require(size < 5 && isArray(a, size))
- var i = size - 1
+ def sort(a: Array[Int]): Array[Int] = ({
+ require(a.length >= 1)
+ var i = a.length - 1
var j = 0
- var sortedArray = a
+ val sa = a.clone
(while(i > 0) {
j = 0
(while(j < i) {
- if(sortedArray(j) > sortedArray(j+1)) {
- val tmp = sortedArray(j)
- sortedArray = sortedArray.updated(j, sortedArray(j+1))
- sortedArray = sortedArray.updated(j+1, tmp)
+ if(sa(j) > sa(j+1)) {
+ val tmp = sa(j)
+ sa(j) = sa(j+1)
+ sa(j+1) = tmp
}
j = j + 1
}) invariant(
j >= 0 &&
j <= i &&
- i < size &&
- isArray(sortedArray, size) &&
- partitioned(sortedArray, size, 0, i, i+1, size-1) &&
- sorted(sortedArray, size, i, size-1) &&
- partitioned(sortedArray, size, 0, j-1, j, j)
+ i < sa.length &&
+ sa.length >= 0 &&
+ partitioned(sa, 0, i, i+1, sa.length-1) &&
+ sorted(sa, i, sa.length-1) &&
+ partitioned(sa, 0, j-1, j, j)
)
i = i - 1
}) invariant(
i >= 0 &&
- i < size &&
- isArray(sortedArray, size) &&
- partitioned(sortedArray, size, 0, i, i+1, size-1) &&
- sorted(sortedArray, size, i, size-1)
+ i < sa.length &&
+ sa.length >= 0 &&
+ partitioned(sa, 0, i, i+1, sa.length-1) &&
+ sorted(sa, i, sa.length-1)
)
- sortedArray
- }) ensuring(res => sorted(res, size, 0, size-1))
+ sa
+ }) ensuring(res => sorted(res, 0, a.length-1))
- def sorted(a: Map[Int, Int], size: Int, l: Int, u: Int): Boolean = {
- require(isArray(a, size) && size < 5 && l >= 0 && u < size && l <= u)
+ def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
+ require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
var k = l
var isSorted = true
(while(k < u) {
@@ -49,57 +49,9 @@ object Bubble {
}) invariant(k <= u && k >= l)
isSorted
}
- /*
- // --------------------- sorted --------------------
- def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
- require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
- val t = sortedWhile(true, l, l, u, a, size)
- t._1
- }
-
- def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
- require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
- if(k < u) {
- sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
- } else (isSorted, k)
- }
- */
-
- /*
- // ------------- partitioned ------------------
- def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
- require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
- if(l2 > u2 || l1 > u1)
- true
- else {
- val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
- t._2
- }
- }
- def partitionedWhile(j: Int, isPartitionned: Boolean, i: Int, l1: Int, size: Int, u2: Int, l2: Int, u1: Int, a: Map[Int,Int]) : (Int, Boolean, Int) = {
- require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && i >= l1)
-
- if(i <= u1) {
- val t = partitionedNestedWhile(isPartitionned, l2, i, l1, u1, size, u2, a, l2)
- partitionedWhile(t._2, t._1, i + 1, l1, size, u2, l2, u1, a)
- } else (j, isPartitionned, i)
- }
- def partitionedNestedWhile(isPartitionned: Boolean, j: Int, i: Int, l1: Int, u1: Int, size: Int, u2: Int, a: Map[Int,Int], l2: Int): (Boolean, Int) = {
- require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && j >= l2 && i >= l1 && i <= u1)
- if (j <= u2) {
- partitionedNestedWhile(
- (if (a(i) > a(j))
- false
- else
- isPartitionned),
- j + 1, i, l1, u1, size, u2, a, l2)
- } else (isPartitionned, j)
- }
- */
-
- def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
- require(l1 >= 0 && u1 < l2 && u2 < size && isArray(a, size) && size < 5)
+ def partitioned(a: Array[Int], l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(a.length >= 0 && l1 >= 0 && u1 < l2 && u2 < a.length)
if(l2 > u2 || l1 > u1)
true
else {
@@ -119,14 +71,4 @@ object Bubble {
}
}
- def isArray(a: Map[Int, Int], size: Int): Boolean = {
- def rec(i: Int): Boolean = if(i >= size) true else {
- if(a.isDefinedAt(i)) rec(i+1) else false
- }
- if(size <= 0)
- false
- else
- rec(0)
- }
-
}
diff --git a/testcases/LinearSearch.scala b/testcases/LinearSearch.scala
index e91a3f2679b33b8b35e7d64989db1b7ade451d14..e18c4039c7d7f7418399ff16483d1b18cc6895a9 100644
--- a/testcases/LinearSearch.scala
+++ b/testcases/LinearSearch.scala
@@ -4,29 +4,29 @@ import leon.Utils._
object LinearSearch {
- def linearSearch(a: Map[Int, Int], size: Int, c: Int): Boolean = ({
- require(size <= 5 && isArray(a, size))
+ def linearSearch(a: Array[Int], c: Int): Boolean = ({
+ require(a.length >= 0)
var i = 0
var found = false
- (while(i < size) {
+ (while(i < a.length) {
if(a(i) == c)
found = true
i = i + 1
- }) invariant(i <= size &&
- i >= 0 &&
- (if(found) contains(a, i, c) else !contains(a, i, c))
- )
+ }) invariant(
+ i <= a.length &&
+ i >= 0 &&
+ (if(found) contains(a, i, c) else !contains(a, i, c))
+ )
found
- }) ensuring(res => if(res) contains(a, size, c) else !contains(a, size, c))
+ }) ensuring(res => if(res) contains(a, a.length, c) else !contains(a, a.length, c))
- def contains(a: Map[Int, Int], size: Int, c: Int): Boolean = {
- require(isArray(a, size) && size <= 5)
+ def contains(a: Array[Int], size: Int, c: Int): Boolean = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
content(a, size).contains(c)
}
-
- def content(a: Map[Int, Int], size: Int): Set[Int] = {
- require(isArray(a, size) && size <= 5)
+ def content(a: Array[Int], size: Int): Set[Int] = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
var set = Set.empty[Int]
var i = 0
(while(i < size) {
@@ -36,18 +36,4 @@ object LinearSearch {
set
}
- def isArray(a: Map[Int, Int], size: Int): Boolean = {
-
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size) true else {
- if(a.isDefinedAt(i)) rec(i+1) else false
- }
- }
-
- if(size < 0)
- false
- else
- rec(0)
- }
}
diff --git a/testcases/MaxSum.scala b/testcases/MaxSum.scala
index 07c5d12ab2450cc95af964c7078759a13fe8f0cb..ba724d255c23b782e1b4de716ccc8d50043e2059 100644
--- a/testcases/MaxSum.scala
+++ b/testcases/MaxSum.scala
@@ -4,44 +4,26 @@ import leon.Utils._
object MaxSum {
-
- def maxSum(a: Map[Int, Int], size: Int): (Int, Int) = ({
- require(isArray(a, size) && size < 5 && isPositive(a, size))
+ def maxSum(a: Array[Int]): (Int, Int) = ({
+ require(a.length >= 0 && isPositive(a))
var sum = 0
var max = 0
var i = 0
- (while(i < size) {
+ (while(i < a.length) {
if(max < a(i))
max = a(i)
sum = sum + a(i)
i = i + 1
- }) invariant (sum <= i * max && /*isGreaterEq(a, i, max) &&*/ /*(if(i == 0) max == 0 else true) &&*/ i >= 0 && i <= size)
+ }) invariant (sum <= i * max && i >= 0 && i <= a.length)
(sum, max)
- }) ensuring(res => res._1 <= size * res._2)
+ }) ensuring(res => res._1 <= a.length * res._2)
-/*
- def isGreaterEq(a: Map[Int, Int], size: Int, n: Int): Boolean = {
- require(size <= 5 && isArray(a, size))
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size)
- true
- else {
- if(a(i) > n)
- false
- else
- rec(i+1)
- }
- }
- rec(0)
- }
- */
- def isPositive(a: Map[Int, Int], size: Int): Boolean = {
- require(size <= 5 && isArray(a, size))
+ def isPositive(a: Array[Int]): Boolean = {
+ require(a.length >= 0)
def rec(i: Int): Boolean = {
require(i >= 0)
- if(i >= size)
+ if(i >= a.length)
true
else {
if(a(i) < 0)
@@ -53,18 +35,4 @@ object MaxSum {
rec(0)
}
- def isArray(a: Map[Int, Int], size: Int): Boolean = {
-
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size) true else {
- if(a.isDefinedAt(i)) rec(i+1) else false
- }
- }
-
- if(size < 0)
- false
- else
- rec(0)
- }
}
diff --git a/testcases/regression/InfiniteLoop.scala b/testcases/regression/InfiniteLoop.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e9e5d0d5c7e258a77fdb418df3b51194fd6a9594
--- /dev/null
+++ b/testcases/regression/InfiniteLoop.scala
@@ -0,0 +1,12 @@
+object InfiniteLoop {
+
+ def infinite(): Int = {
+ var i = 0
+ var sum = 0
+ while (i < 10) {
+ sum = sum + i
+ }
+ sum
+ }
+
+}
diff --git a/testcases/regression/error/Array1.scala b/testcases/regression/error/Array1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d0056f18864ba168abb5735daf0db1e0bb76eda5
--- /dev/null
+++ b/testcases/regression/error/Array1.scala
@@ -0,0 +1,8 @@
+object Array1 {
+
+ def foo(): Int = {
+ (Array.fill(5)(5))(2) = 3
+ 0
+ }
+
+}
diff --git a/testcases/regression/error/Array10.scala b/testcases/regression/error/Array10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9973626b83a01c7a8a944bcf808274d7989b3a66
--- /dev/null
+++ b/testcases/regression/error/Array10.scala
@@ -0,0 +1,12 @@
+object Array10 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ def rec(): Array[Int] = {
+ a
+ }
+ val b = rec()
+ b(0)
+ }
+
+}
diff --git a/testcases/regression/error/Array2.scala b/testcases/regression/error/Array2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9154460c37237761b6c8f2d0ecb0b34fb3ec0bf6
--- /dev/null
+++ b/testcases/regression/error/Array2.scala
@@ -0,0 +1,9 @@
+object Array2 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(5)
+ val b = a
+ b(3)
+ }
+
+}
diff --git a/testcases/regression/error/Array3.scala b/testcases/regression/error/Array3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a2c2fbd6ddfde2b3cca2dcc08fb61a79f0ae471c
--- /dev/null
+++ b/testcases/regression/error/Array3.scala
@@ -0,0 +1,12 @@
+object Array3 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(5)
+ if(a.length > 2)
+ a(1) = 2
+ else
+ 0
+ 0
+ }
+
+}
diff --git a/testcases/regression/error/Array4.scala b/testcases/regression/error/Array4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5ab0115af5e8737c6baab851822643490e79334f
--- /dev/null
+++ b/testcases/regression/error/Array4.scala
@@ -0,0 +1,8 @@
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ val b = a
+ b(3)
+ }
+
+}
diff --git a/testcases/regression/error/Array5.scala b/testcases/regression/error/Array5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..005d3d389dd1e748d139283a6fbdcb93aa8d525c
--- /dev/null
+++ b/testcases/regression/error/Array5.scala
@@ -0,0 +1,10 @@
+object Array5 {
+
+ def foo(a: Array[Int]): Int = {
+ a(2) = 4
+ a(2)
+ }
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/regression/error/Array6.scala b/testcases/regression/error/Array6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..15c87a08554c7e9563cbad9b47a881376e45a4c5
--- /dev/null
+++ b/testcases/regression/error/Array6.scala
@@ -0,0 +1,10 @@
+
+object Array6 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(5)
+ var b = a
+ b(0)
+ }
+
+}
diff --git a/testcases/regression/error/Array7.scala b/testcases/regression/error/Array7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..abb83e1c0bd931bf1d41a132fef6fb74ea25318b
--- /dev/null
+++ b/testcases/regression/error/Array7.scala
@@ -0,0 +1,9 @@
+object Array7 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(5)
+ var b = a
+ b(0)
+ }
+
+}
diff --git a/testcases/regression/error/Array8.scala b/testcases/regression/error/Array8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..89af32efdb89273ecf6b275b5a8f2f787bb73a1f
--- /dev/null
+++ b/testcases/regression/error/Array8.scala
@@ -0,0 +1,7 @@
+object Array8 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ a
+ }
+
+}
diff --git a/testcases/regression/error/Array9.scala b/testcases/regression/error/Array9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5dc9d3aea24f7c38b8a374659058c9d0ca7fb336
--- /dev/null
+++ b/testcases/regression/error/Array9.scala
@@ -0,0 +1,11 @@
+object Array9 {
+
+ def foo(a: Array[Int]): Int = {
+ def rec(): Array[Int] = {
+ a
+ }
+ val b = rec()
+ b(0)
+ }
+
+}
diff --git a/testcases/regression/invalid/Array1.scala b/testcases/regression/invalid/Array1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a8451250c8f9e9c95684b4ea10490aced2a23f6e
--- /dev/null
+++ b/testcases/regression/invalid/Array1.scala
@@ -0,0 +1,9 @@
+object Array1 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a(2)
+ } ensuring(_ == 0)
+
+}
diff --git a/testcases/regression/invalid/Array2.scala b/testcases/regression/invalid/Array2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..54ab5e3c27918596af58c427fabedd2016a33db9
--- /dev/null
+++ b/testcases/regression/invalid/Array2.scala
@@ -0,0 +1,9 @@
+object Array2 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a.length
+ } ensuring(_ == 4)
+
+}
diff --git a/testcases/regression/invalid/Array3.scala b/testcases/regression/invalid/Array3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0c1bb76fdce099bd095c59d8c03fe8e6508a9776
--- /dev/null
+++ b/testcases/regression/invalid/Array3.scala
@@ -0,0 +1,16 @@
+import leon.Utils._
+
+object Array3 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(3)
+ var i = 0
+ var sum = 0
+ (while(i <= a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ } ensuring(_ == 15)
+
+}
diff --git a/testcases/regression/invalid/Array4.scala b/testcases/regression/invalid/Array4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5b5e7406165ad214a7d5d5fffd85d2d4fce226e0
--- /dev/null
+++ b/testcases/regression/invalid/Array4.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ a(2)
+ }
+
+}
diff --git a/testcases/regression/invalid/Array5.scala b/testcases/regression/invalid/Array5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ecb00334971f3ecf19f3b6e6f9c25a5082f2d2d7
--- /dev/null
+++ b/testcases/regression/invalid/Array5.scala
@@ -0,0 +1,10 @@
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 2)
+ a(2)
+ } ensuring(_ == 0)
+
+}
diff --git a/testcases/regression/invalid/Epsilon1.scala b/testcases/regression/invalid/Epsilon1.scala
index 859ced1c19b0c3688ad8eef433fbc290c672fbe9..c3c0a48be96f594fe725518a7289333bb587ef40 100644
--- a/testcases/regression/invalid/Epsilon1.scala
+++ b/testcases/regression/invalid/Epsilon1.scala
@@ -2,8 +2,11 @@ import leon.Utils._
object Epsilon1 {
- def greaterWrong(x: Int): Int = {
- epsilon((y: Int) => y >= x)
- } ensuring(_ > x)
+ def rand2(x: Int): Int = epsilon((y: Int) => true)
+
+ //this should not hold
+ def property2(x: Int): Boolean = {
+ rand2(x) == rand2(x+1)
+ } holds
}
diff --git a/testcases/regression/invalid/Epsilon4.scala b/testcases/regression/invalid/Epsilon4.scala
index 52ee6dbe66c2d5b3517d5d84f90f35f8f10aa38d..6619e59d6f9d9721c4bc7587b47dac79f48bf437 100644
--- a/testcases/regression/invalid/Epsilon4.scala
+++ b/testcases/regression/invalid/Epsilon4.scala
@@ -23,5 +23,5 @@ object Epsilon4 {
def wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds
- def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
+ //def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
}
diff --git a/testcases/regression/invalid/Epsilon6.scala b/testcases/regression/invalid/Epsilon6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bc5aca78c3818a94df43146aba16077ffab50a71
--- /dev/null
+++ b/testcases/regression/invalid/Epsilon6.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon6 {
+
+ def greaterWrong(x: Int): Int = {
+ epsilon((y: Int) => y >= x)
+ } ensuring(_ > x)
+
+}
diff --git a/testcases/regression/invalid/Unit1.scala b/testcases/regression/invalid/Unit1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..789a8f058cd8145a0dd3b7bb0d72d44fb92ee94e
--- /dev/null
+++ b/testcases/regression/invalid/Unit1.scala
@@ -0,0 +1,7 @@
+object Unit1 {
+
+ def foo(u: Unit): Unit = ({
+ u
+ }) ensuring(_ != ())
+
+}
diff --git a/testcases/regression/valid/Array1.scala b/testcases/regression/valid/Array1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3815f03443448a28fb60475b49c09c981a1377f9
--- /dev/null
+++ b/testcases/regression/valid/Array1.scala
@@ -0,0 +1,9 @@
+object Array1 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a(2)
+ } ensuring(_ == 3)
+
+}
diff --git a/testcases/regression/valid/Array10.scala b/testcases/regression/valid/Array10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ebb60ad6e0ba7556c55c74e1b1b624e6c34b4311
--- /dev/null
+++ b/testcases/regression/valid/Array10.scala
@@ -0,0 +1,9 @@
+object Array10 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 0)
+ val b = a.clone
+ b(0)
+ } ensuring(res => res == a(0))
+
+}
diff --git a/testcases/regression/valid/Array2.scala b/testcases/regression/valid/Array2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4f149a9305cb4b53a4a9353b82e25468c898bdc8
--- /dev/null
+++ b/testcases/regression/valid/Array2.scala
@@ -0,0 +1,9 @@
+object Array2 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a.length
+ } ensuring(_ == 5)
+
+}
diff --git a/testcases/regression/valid/Array3.scala b/testcases/regression/valid/Array3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bbb1845b80c0ca747cb0c830828bacdc9668943f
--- /dev/null
+++ b/testcases/regression/valid/Array3.scala
@@ -0,0 +1,16 @@
+import leon.Utils._
+
+object Array3 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(3)
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ } ensuring(_ == 15)
+
+}
diff --git a/testcases/regression/valid/Array4.scala b/testcases/regression/valid/Array4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fd76e02faa83f8fd1bda5fef7c91e7df7fc29864
--- /dev/null
+++ b/testcases/regression/valid/Array4.scala
@@ -0,0 +1,15 @@
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ }
+
+}
diff --git a/testcases/regression/valid/Array5.scala b/testcases/regression/valid/Array5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..14bed6eff332db69600353001488c46a3e56aa5d
--- /dev/null
+++ b/testcases/regression/valid/Array5.scala
@@ -0,0 +1,20 @@
+import leon.Utils._
+
+object Array5 {
+
+ def foo(a: Array[Int]): Int = {
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ }
+
+ def bar(): Int = {
+ val a = Array.fill(5)(5)
+ foo(a)
+ }
+
+}
diff --git a/testcases/regression/valid/Array6.scala b/testcases/regression/valid/Array6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bdd6b0c5d9bee06eec14b9f5917762c67af4751b
--- /dev/null
+++ b/testcases/regression/valid/Array6.scala
@@ -0,0 +1,15 @@
+import leon.Utils._
+
+object Array6 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 2 && a(2) == 5)
+ a(2)
+ } ensuring(_ == 5)
+
+ def bar(): Int = {
+ val a = Array.fill(5)(5)
+ foo(a)
+ }
+
+}
diff --git a/testcases/regression/valid/Array7.scala b/testcases/regression/valid/Array7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..55bbbb72908e2b192152162d82d2ed9fea67923b
--- /dev/null
+++ b/testcases/regression/valid/Array7.scala
@@ -0,0 +1,17 @@
+import leon.Utils._
+
+object Array7 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ require(a.length > 0)
+ val a2 = Array.fill(a.length)(0)
+ var i = 0
+ (while(i < a.length) {
+ a2(i) = a(i)
+ i = i + 1
+ }) invariant(a.length == a2.length && i >= 0 && (if(i > 0) a2(0) == a(0) else true))
+ a2
+ } ensuring(_(0) == a(0))
+
+
+}
diff --git a/testcases/regression/valid/Array8.scala b/testcases/regression/valid/Array8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..270b181220b55af1588f63e7953221ae71f9bde3
--- /dev/null
+++ b/testcases/regression/valid/Array8.scala
@@ -0,0 +1,8 @@
+object Array8 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ require(a.length >= 2)
+ a.updated(1, 3)
+ } ensuring(res => res.length == a.length && res(1) == 3)
+
+}
diff --git a/testcases/regression/valid/Array9.scala b/testcases/regression/valid/Array9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f49333236abfaf63caa278405a89670b1c9c115d
--- /dev/null
+++ b/testcases/regression/valid/Array9.scala
@@ -0,0 +1,15 @@
+object Array9 {
+
+ def foo(i: Int): Array[Int] = {
+ require(i > 0)
+ val a = Array.fill(i)(0)
+ a
+ } ensuring(res => res.length == i)
+
+ def bar(i: Int): Int = {
+ require(i > 0)
+ val b = foo(i)
+ b(0)
+ }
+
+}
diff --git a/testcases/regression/valid/Epsilon2.scala b/testcases/regression/valid/Epsilon2.scala
index b4f53f36bf3b5c76a7c2fad5a4f1cdfed12587a9..36e5268e2b1ccdbc710dc8d6410ce6968231c7d1 100644
--- a/testcases/regression/valid/Epsilon2.scala
+++ b/testcases/regression/valid/Epsilon2.scala
@@ -3,16 +3,11 @@ import leon.Utils._
object Epsilon1 {
def rand(): Int = epsilon((x: Int) => true)
- def rand2(x: Int): Int = epsilon((y: Int) => true)
//this should hold, that is the expected semantic of our epsilon
def property1(): Boolean = {
rand() == rand()
} holds
- //this should hold, that is the expected semantic of our epsilon
- def property2(x: Int): Boolean = {
- rand2(x) == rand2(x+1)
- } holds
}
diff --git a/testcases/regression/valid/Field1.scala b/testcases/regression/valid/Field1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..116557ab7b883d01a10168aeaf529d5300ee5f19
--- /dev/null
+++ b/testcases/regression/valid/Field1.scala
@@ -0,0 +1,11 @@
+object Field1 {
+
+ abstract sealed class A
+ case class B(size: Int) extends A
+
+ def foo(): Int = {
+ val b = B(3)
+ b.size
+ } ensuring(_ == 3)
+
+}
diff --git a/testcases/regression/valid/Field2.scala b/testcases/regression/valid/Field2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9a96610235a68754b84e58f73f5e435ce642ebc9
--- /dev/null
+++ b/testcases/regression/valid/Field2.scala
@@ -0,0 +1,11 @@
+object Field2 {
+
+ abstract sealed class A
+ case class B(length: Int) extends A
+
+ def foo(): Int = {
+ val b = B(3)
+ b.length
+ } ensuring(_ == 3)
+
+}
diff --git a/testcases/regression/valid/Nested2.scala b/testcases/regression/valid/Nested2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cc7220b02109c394e71c127e4cd3f53d6714ed7f
--- /dev/null
+++ b/testcases/regression/valid/Nested2.scala
@@ -0,0 +1,13 @@
+object Nested2 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ val b = a + 2
+ def rec1(c: Int): Int = {
+ require(c >= 0)
+ b + c
+ }
+ rec1(2)
+ } ensuring(_ > 0)
+
+}
diff --git a/testcases/regression/valid/Nested3.scala b/testcases/regression/valid/Nested3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..be6e6d04a335d12d079a9e3dc1a4b14ec0164014
--- /dev/null
+++ b/testcases/regression/valid/Nested3.scala
@@ -0,0 +1,15 @@
+object Nested3 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0 && a <= 50)
+ val b = a + 2
+ val c = a + b
+ def rec1(d: Int): Int = {
+ require(d >= 0 && d <= 50)
+ val e = d + b + c
+ e
+ }
+ rec1(2)
+ } ensuring(_ > 0)
+
+}
diff --git a/testcases/regression/valid/Nested4.scala b/testcases/regression/valid/Nested4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ea1e6066c6f4b7aaf6df23065e3011b86471b7f4
--- /dev/null
+++ b/testcases/regression/valid/Nested4.scala
@@ -0,0 +1,19 @@
+object Nested4 {
+
+ def foo(a: Int, a2: Int): Int = {
+ require(a >= 0 && a <= 50)
+ val b = a + 2
+ val c = a + b
+ if(a2 > a) {
+ def rec1(d: Int): Int = {
+ require(d >= 0 && d <= 50)
+ val e = d + b + c + a2
+ e
+ } ensuring(_ > 0)
+ rec1(2)
+ } else {
+ 5
+ }
+ } ensuring(_ > 0)
+
+}
diff --git a/testcases/regression/valid/Nested5.scala b/testcases/regression/valid/Nested5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6ba128f415ecc3c61ebcccb42b65100d15373982
--- /dev/null
+++ b/testcases/regression/valid/Nested5.scala
@@ -0,0 +1,12 @@
+object Nested5 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ def bar(b: Int): Int = {
+ require(b > 0)
+ b + 3
+ } ensuring(a >= 0 && _ == b + 3)
+ bar(2)
+ } ensuring(a >= 0 && _ == 5)
+
+}
diff --git a/testcases/regression/valid/Nested6.scala b/testcases/regression/valid/Nested6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1c0220c0447dba10ccd710d60e5f19b1c1ec6e18
--- /dev/null
+++ b/testcases/regression/valid/Nested6.scala
@@ -0,0 +1,14 @@
+object Nested5 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ def bar(b: Int): Int = {
+ require(b > 0)
+ b + 3
+ } ensuring(prop(a, b) && a >= 0 && _ == b + 3)
+ bar(2)
+ } ensuring(a >= 0 && _ == 5)
+
+ def prop(x: Int, y: Int): Boolean = x + y > 0
+
+}
diff --git a/testcases/regression/valid/Nested7.scala b/testcases/regression/valid/Nested7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..62f5a567f49be174873a24711e630f69e8469a22
--- /dev/null
+++ b/testcases/regression/valid/Nested7.scala
@@ -0,0 +1,19 @@
+object Nested2 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ val b = a + 2
+ def rec1(c: Int): Int = {
+ require(c >= 0)
+ b + c + bar(a) + bar(b) + bar(c)
+ }
+ rec1(2) + bar(a)
+ } ensuring(_ > 0)
+
+
+ def bar(x: Int): Int = {
+ require(x >= 0)
+ x
+ } ensuring(_ >= 0)
+
+}
diff --git a/testcases/regression/valid/Nested8.scala b/testcases/regression/valid/Nested8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e8a05e40e6cd1b2428e03bcf1a9f96c67797c698
--- /dev/null
+++ b/testcases/regression/valid/Nested8.scala
@@ -0,0 +1,43 @@
+import leon.Utils._
+
+object Nested8 {
+
+ def foo(a: Int): Int = {
+ require(a > 0)
+
+ def bar(b: Int): Int = {
+ if(a < b) {
+ def rec(c: Int): Int = {
+ require(c > 0)
+ c + b
+ } ensuring(_ > 0)
+ rec(2)
+ } else 3
+ }
+ bar(1)
+ } ensuring(_ > 0)
+
+ /*
+ def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
+ }
+ */
+
+}
diff --git a/testcases/regression/valid/Nested9.scala b/testcases/regression/valid/Nested9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3344a2c7973bed9da2c42208742c34c184b458ac
--- /dev/null
+++ b/testcases/regression/valid/Nested9.scala
@@ -0,0 +1,23 @@
+object Nested4 {
+
+ def foo(a: Int, a2: Int): Int = {
+ require(a >= 0 && a <= 50)
+ val b = a + 2
+ val c = a + b
+ if(a2 > a) {
+ def rec1(d: Int): Int = {
+ require(d >= 0 && d <= 50)
+ val e = d + b + c + a2
+ def rec2(f: Int): Int = {
+ require(f >= c)
+ f + e
+ } ensuring(_ > 0)
+ rec2(c+1)
+ } ensuring(_ > 0)
+ rec1(2)
+ } else {
+ 5
+ }
+ } ensuring(_ > 0)
+
+}
diff --git a/testcases/regression/valid/Unit1.scala b/testcases/regression/valid/Unit1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a7b890d762648cba480c817506c7eee22259860d
--- /dev/null
+++ b/testcases/regression/valid/Unit1.scala
@@ -0,0 +1,7 @@
+object Unit1 {
+
+ def foo(): Unit = ({
+ ()
+ }) ensuring(_ == ())
+
+}
diff --git a/testcases/regression/valid/Unit2.scala b/testcases/regression/valid/Unit2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ac659589af503a8a79f261f9eb05be095e2e0943
--- /dev/null
+++ b/testcases/regression/valid/Unit2.scala
@@ -0,0 +1,7 @@
+object Unit2 {
+
+ def foo(u: Unit): Unit = {
+ u
+ } ensuring(_ == ())
+
+}