diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index cdbfc205c30cdf6fbc73cb7f4c15e291cbf53b93..7890d7a229da487e8ae8152ae92c7b0b066eb12e 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -399,14 +399,17 @@ trait ASTExtractors {
}.get.asInstanceOf[DefDef]
val valDefs = constructor.vparamss.flatten
+ //println("valDefs: " + valDefs)
//impl.children foreach println
val symbols = impl.children.collect {
- case df: DefDef if df.symbol.isStable && df.symbol.isAccessor &&
- df.symbol.isParamAccessor =>
- df.symbol
+ case df@DefDef(_, name, _, _, _, _) if
+ df.symbol.isAccessor && df.symbol.isParamAccessor
+ && !name.endsWith("_$eq") => df.symbol
}
+ //println("symbols: " + symbols)
+ //println("symbols accessed: " + symbols.map(_.accessed))
//if (symbols.size != valDefs.size) {
// println(" >>>>> " + cd.name)
@@ -500,6 +503,36 @@ trait ASTExtractors {
case _ => None
}
}
+
+ object ExMutatorAccessorFunction {
+ def unapply(dd: DefDef): Option[(Symbol, Seq[Symbol], Seq[ValDef], Type, Tree)] = dd match {
+ case DefDef(_, name, tparams, vparamss, tpt, rhs) if(
+ vparamss.size <= 1 && name != nme.CONSTRUCTOR &&
+ !dd.symbol.isSynthetic && dd.symbol.isAccessor && name.endsWith("_$eq")
+ ) =>
+ Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
+ case _ => None
+ }
+ }
+ object ExMutableFieldDef {
+
+ /** Matches a definition of a strict var field inside a class constructor */
+ def unapply(vd: SymTree) : Option[(Symbol, Type, Tree)] = {
+ val sym = vd.symbol
+ vd match {
+ // Implemented fields
+ case ValDef(mods, name, tpt, rhs) if (
+ !sym.isCaseAccessor && !sym.isParamAccessor &&
+ !sym.isLazy && !sym.isSynthetic && !sym.isAccessor && sym.isVar
+ ) =>
+ println("matched a var accessor field: sym is: " + sym)
+ println("getterIn is: " + sym.getterIn(sym.owner))
+ // Since scalac uses the accessor symbol all over the place, we pass that instead:
+ Some( (sym.getterIn(sym.owner),tpt.tpe,rhs) )
+ case _ => None
+ }
+ }
+ }
object ExFieldDef {
/** Matches a definition of a strict field inside a class constructor */
@@ -509,7 +542,7 @@ trait ASTExtractors {
// Implemented fields
case ValDef(mods, name, tpt, rhs) if (
!sym.isCaseAccessor && !sym.isParamAccessor &&
- !sym.isLazy && !sym.isSynthetic && !sym.isAccessor
+ !sym.isLazy && !sym.isSynthetic && !sym.isAccessor && !sym.isVar
) =>
// Since scalac uses the accessor symbol all over the place, we pass that instead:
Some( (sym.getterIn(sym.owner),tpt.tpe,rhs) )
@@ -695,6 +728,7 @@ trait ASTExtractors {
object ExAssign {
def unapply(tree: Assign): Option[(Symbol,Tree)] = tree match {
case Assign(id@Ident(_), rhs) => Some((id.symbol, rhs))
+ //case Assign(sym@Select(This(_), v), rhs) => Some((sym.symbol, rhs))
case _ => None
}
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 497cbb4f9ac70417744b0e6cf177797b1c322931..85e587444a41b59e38a057ac6fc8e1c6e616b8e5 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -133,6 +133,10 @@ trait CodeExtraction extends ASTExtractors {
def withNewMutableVar(nvar: (Symbol, () => LeonExpr)) = {
copy(mutableVars = mutableVars + nvar)
}
+
+ def withNewMutableVars(nvars: Traversable[(Symbol, () => LeonExpr)]) = {
+ copy(mutableVars = mutableVars ++ nvars)
+ }
}
private var currentFunDef: FunDef = null
@@ -281,6 +285,10 @@ trait CodeExtraction extends ASTExtractors {
case ExFieldDef(sym, _, _) =>
Some(defineFieldFunDef(sym, false)(DefContext()))
+ // var
+ case ExMutableFieldDef(sym, _, _) =>
+ Some(defineFieldFunDef(sym, false)(DefContext()))
+
// All these are expected, but useless
case ExCaseClassSyntheticJunk()
| ExConstructorDef()
@@ -290,6 +298,12 @@ trait CodeExtraction extends ASTExtractors {
case d if (d.symbol.isImplicit && d.symbol.isSynthetic) =>
None
+ //vars are never accessed directly so we extract accessors and mutators and
+ //ignore bare variables
+ case d if d.symbol.isVar =>
+ None
+
+
// Everything else is unexpected
case tree =>
println(tree)
@@ -463,6 +477,7 @@ trait CodeExtraction extends ASTExtractors {
}
private var isMethod = Set[Symbol]()
+ private var isMutator = Set[Symbol]()
private var methodToClass = Map[FunDef, LeonClassDef]()
private var classToInvariants = Map[Symbol, Set[Tree]]()
@@ -564,7 +579,7 @@ trait CodeExtraction extends ASTExtractors {
val tpe = leonType(t.tpt.tpe)(defCtx, fsym.pos)
val id = cachedWithOverrides(fsym, Some(ccd), tpe)
if (tpe != id.getType) println(tpe, id.getType)
- LeonValDef(id.setPos(t.pos)).setPos(t.pos)
+ LeonValDef(id.setPos(t.pos)).setPos(t.pos).setIsVar(fsym.accessed.isVar)
}
//println(s"Fields of $sym")
@@ -670,6 +685,25 @@ trait CodeExtraction extends ASTExtractors {
cd.registerMethod(fd)
+ case t @ ExMutableFieldDef(fsym, _, _) =>
+ //println(fsym + "matched as ExMutableFieldDef")
+ // we will be using the accessor method of this field everywhere
+ //isMethod += fsym
+ //val fd = defineFieldFunDef(fsym, false, Some(cd))(defCtx)
+ //methodToClass += fd -> cd
+
+ //cd.registerMethod(fd)
+
+ case t@ ExMutatorAccessorFunction(fsym, _, _, _, _) =>
+ //println("FOUND mutator: " + t)
+ //println("accessed: " + fsym.accessed)
+ isMutator += fsym
+ //val fd = defineFunDef(fsym, Some(cd))(defCtx)
+
+ //methodToClass += fd -> cd
+
+ //cd.registerMethod(fd)
+
case other =>
}
@@ -688,7 +722,7 @@ trait CodeExtraction extends ASTExtractors {
val topOfHierarchy = sym.overrideChain.last
funOrFieldSymsToIds.cachedB(topOfHierarchy){
- FreshIdentifier(sym.name.toString, tpe)
+ FreshIdentifier(sym.name.toString.trim, tpe) //trim because sometimes Scala names end with a trailing space, looks nicer without the space
}
}
@@ -827,6 +861,31 @@ trait CodeExtraction extends ASTExtractors {
extractFunBody(fd, Seq(), body)(DefContext(tparamsMap.toMap))
}
+ case t @ ExMutableFieldDef(sym, _, body) => // if !sym.isSynthetic && !sym.isAccessor =>
+ //val fd = defsToDefs(sym)
+ //val tparamsMap = ctparamsMap
+
+ //if(body != EmptyTree) {
+ // extractFunBody(fd, Seq(), body)(DefContext(tparamsMap.toMap))
+ //}
+
+ case ExMutatorAccessorFunction(sym, tparams, params, _, body) =>
+ //val fd = defsToDefs(sym)
+
+ //val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap ++ ctparamsMap
+
+ //val classSym = ocsym.get
+ //val cd = classesToClasses(classSym).asInstanceOf[CaseClassDef]
+ //val classVarDefs = seenClasses(classSym)._2
+ //val mutableFields = classVarDefs.zip(cd.varFields).map(p => (p._1._1, () => p._2.toVariable))
+
+ //val dctx = DefContext(tparamsMap)
+ //val pctx = dctx.withNewMutableVars(mutableFields)
+
+ //if(body != EmptyTree) {
+ // extractFunBody(fd, params, body)(pctx)
+ //}
+
case _ =>
}
}
@@ -1234,15 +1293,16 @@ trait CodeExtraction extends ASTExtractors {
LetVar(newID, valTree, restTree)
}
- case ExAssign(sym, rhs) => dctx.mutableVars.get(sym) match {
+ case a@ExAssign(sym, rhs) => {
+ dctx.mutableVars.get(sym) match {
case Some(fun) =>
val Variable(id) = fun()
val rhsTree = extractTree(rhs)
Assignment(id, rhsTree)
case None =>
- outOfSubsetError(tr, "Undeclared variable.")
- }
+ outOfSubsetError(a, "Undeclared variable.")
+ }}
case wh @ ExWhile(cond, body) =>
val condTree = extractTree(cond)
@@ -1563,7 +1623,7 @@ trait CodeExtraction extends ASTExtractors {
case c @ ExCall(rec, sym, tps, args) =>
// The object on which it is called is null if the symbol sym is a valid function in the scope and not a method.
val rrec = rec match {
- case t if (defsToDefs contains sym) && !isMethod(sym) =>
+ case t if (defsToDefs contains sym) && !isMethod(sym) && !isMutator(sym) =>
null
case _ =>
extractTree(rec)
@@ -1600,6 +1660,11 @@ trait CodeExtraction extends ASTExtractors {
caseClassSelector(cct, rec, fieldID)
+ //mutable variables
+ case (IsTyped(rec, cct: CaseClassType), name, List(e1)) if isMutator(sym) =>
+ val id = cct.classDef.fields.find(_.id.name == name.dropRight(2)).get.id
+ FieldAssignment(rec, id, e1)
+
//String methods
case (IsTyped(a1, StringType), "toString", List()) =>
a1
@@ -1793,6 +1858,7 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, CharType), "<=", List(IsTyped(a2, CharType))) =>
LessEquals(a1, a2)
+
case (a1, name, a2) =>
val typea1 = a1.getType
val typea2 = a2.map(_.getType).mkString(",")
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 649c84472f2399f6530b5762326a1f3d763bc5c4..1b9d146d15765fe88b3ebf8d034ba9ac66a361a6 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -711,4 +711,27 @@ object DefOps {
)
}
+ def augmentCaseClassFields(extras: Seq[(CaseClassDef, Seq[(ValDef, Expr)])])
+ (program: Program) = {
+
+ def updateBody(body: Expr): Expr = {
+ preMap({
+ case CaseClass(ct, args) => extras.find(p => p._1 == ct.classDef).map{
+ case (ccd, extraFields) =>
+ CaseClass(CaseClassType(ccd, ct.tps), args ++ extraFields.map{ case (_, v) => v })
+ }
+ case _ => None
+ })(body)
+ }
+
+ extras.foreach{ case (ccd, extraFields) => ccd.setFields(ccd.fields ++ extraFields.map(_._1)) }
+ for {
+ fd <- program.definedFunctions
+ } {
+ fd.body = fd.body.map(body => updateBody(body))
+ fd.precondition = fd.precondition.map(pre => updateBody(pre))
+ fd.postcondition = fd.postcondition.map(post => updateBody(post))
+ }
+ }
+
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 484745ae09d0f09340acaac5c83c5badd1c79762..98497afd31586ef8cff40eec4a68ef36da63162b 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -52,6 +52,10 @@ object Definitions {
var defaultValue : Option[FunDef] = None
+ var isVar: Boolean = false
+
+ def setIsVar(b: Boolean): this.type = { this.isVar = b; this }
+
def subDefinitions = Seq()
/** Transform this [[ValDef]] into a [[Expressions.Variable Variable]] */
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index 6743da68b8509e43192a825cf0a25cc6c1cdb3d2..957505f297b551ff0bab84955015de35b0a0d7e2 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -11,6 +11,7 @@ import ExprOps._
import Types._
import Constructors._
import TypeOps.instantiateType
+import xlang.Expressions._
object MethodLifting extends TransformationPhase {
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index d1975779e5690b27823a9ddfd0abc7af79e0aabe..3773ebce48b3c51e056cee01f1ed059288d25bc5 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -367,6 +367,8 @@ class PrettyPrinter(opts: PrinterOptions,
case Not(expr) => p"\u00AC$expr"
case vd @ ValDef(id) =>
+ if(vd.isVar)
+ p"var "
p"$id : ${vd.getType}"
vd.defaultValue.foreach { fd => p" = ${fd.body.get}" }
@@ -528,7 +530,7 @@ class PrettyPrinter(opts: PrinterOptions,
if (ccd.methods.nonEmpty) {
p"""| {
- | ${nary(ccd.methods, "\n\n")}
+ | ${nary(ccd.methods, "\n\n") }
|}"""
}
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 0ee936c813b942d3e55564506a200b31630f0283..b461a51c64d28a4f589f7182f4342ee58d08ddbd 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -98,7 +98,7 @@ object Types {
assert(classDef.tparams.size == tps.size)
- lazy val fields = {
+ def fields = {
val tmap = (classDef.tparams zip tps).toMap
if (tmap.isEmpty) {
classDef.fields
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index d2717f5ef6af6eba77245ff6c7910ba8955fb1bb..34b7b35f428bff701af9a25c06258da5a43443ed 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -219,7 +219,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
// id => expr && ... && expr
var guardedExprs = Map[Identifier, Seq[Expr]]()
def storeGuarded(guardVar: Identifier, expr: Expr) : Unit = {
- assert(expr.getType == BooleanType, expr.asString(Program.empty)(LeonContext.empty) + " is not of type Boolean." + (
+ assert(expr.getType == BooleanType, expr.asString(Program.empty)(LeonContext.empty) + " is not of type Boolean. " + (
purescala.ExprOps.fold[String]{ (e, se) =>
s"$e is of type ${e.getType}" + se.map(child => "\n " + "\n".r.replaceAllIn(child, "\n ")).mkString
}(expr)
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index 4d1e903fd8fc87673351e9b5a6d74929d935827b..d237c89d5089c13b4a8c6aa50e04dc7c3754e0fd 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -19,12 +19,14 @@ object AntiAliasingPhase extends TransformationPhase {
val description = "Make aliasing explicit"
override def apply(ctx: LeonContext, pgm: Program): Program = {
+
val fds = allFunDefs(pgm)
fds.foreach(fd => checkAliasing(fd)(ctx))
var updatedFunctions: Map[FunDef, FunDef] = Map()
val effects = effectsAnalysis(pgm)
+ //println("effects: " + effects.filter(e => e._2.size > 0).map(e => (e._1.id, e._2)))
//for each fun def, all the vars the the body captures. Only
//mutable types.
@@ -33,7 +35,7 @@ object AntiAliasingPhase extends TransformationPhase {
} yield {
val allFreeVars = fd.body.map(bd => variablesOf(bd)).getOrElse(Set())
val freeVars = allFreeVars -- fd.params.map(_.id)
- val mutableFreeVars = freeVars.filter(id => id.getType.isInstanceOf[ArrayType])
+ val mutableFreeVars = freeVars.filter(id => isMutableType(id.getType))
(fd, mutableFreeVars)
}).toMap
@@ -166,12 +168,25 @@ object AntiAliasingPhase extends TransformationPhase {
(None, bindings)
}
- case l@Let(id, IsTyped(v, ArrayType(_)), b) => {
+ case as@FieldAssignment(o, id, v) => {
+ findReceiverId(o) match {
+ case None =>
+ ctx.reporter.fatalError(as.getPos, "Unsupported form of field assignment: " + as)
+ case Some(oid) => {
+ if(bindings.contains(oid))
+ (Some(Assignment(oid, deepCopy(o, id, v))), bindings)
+ else
+ (None, bindings)
+ }
+ }
+ }
+
+ case l@Let(id, IsTyped(v, tpe), b) if isMutableType(tpe) => {
val varDecl = LetVar(id, v, b).setPos(l)
(Some(varDecl), bindings + id)
}
- case l@LetVar(id, IsTyped(v, ArrayType(_)), b) => {
+ case l@LetVar(id, IsTyped(v, tpe), b) if isMutableType(tpe) => {
(None, bindings + id)
}
@@ -199,18 +214,26 @@ object AntiAliasingPhase extends TransformationPhase {
val nfi = FunctionInvocation(nfd.typed(fd.tps), args).copiedFrom(fi)
val fiEffects = effects.getOrElse(fd.fd, Set())
if(fiEffects.nonEmpty) {
- val modifiedArgs: Seq[Variable] =
+ val modifiedArgs: Seq[(Identifier, Expr)] =// functionInvocationEffects(fi, fiEffects)
args.zipWithIndex.filter{ case (arg, i) => fiEffects.contains(i) }
- .map(_._1.asInstanceOf[Variable])
+ .map(arg => (findReceiverId(arg._1).get, arg._1))
val duplicatedParams = modifiedArgs.diff(modifiedArgs.distinct).distinct
if(duplicatedParams.nonEmpty)
ctx.reporter.fatalError(fi.getPos, "Illegal passing of aliased parameter: " + duplicatedParams.head)
- val freshRes = FreshIdentifier("res", nfd.returnType)
+ val freshRes = FreshIdentifier("res", nfd.typed(fd.tps).returnType)
val extractResults = Block(
- modifiedArgs.zipWithIndex.map(p => Assignment(p._1.id, TupleSelect(freshRes.toVariable, p._2 + 2))),
+ modifiedArgs.zipWithIndex.map{ case ((id, expr), index) => {
+ val resSelect = TupleSelect(freshRes.toVariable, index + 2)
+ expr match {
+ case CaseClassSelector(_, obj, mid) =>
+ Assignment(id, deepCopy(obj, mid, resSelect))
+ case _ =>
+ Assignment(id, resSelect)
+ }
+ }},
TupleSelect(freshRes.toVariable, 1))
@@ -228,9 +251,7 @@ object AntiAliasingPhase extends TransformationPhase {
})(body, aliasedParams.toSet)
}
- //TODO: in the future, any object with vars could be aliased and so
- // we will need a general property
-
+ //for each fundef, the set of modified params (by index)
private type Effects = Map[FunDef, Set[Int]]
/*
@@ -253,14 +274,8 @@ object AntiAliasingPhase extends TransformationPhase {
case None =>
effects += (fd -> Set())
case Some(body) => {
- val mutableParams = fd.params.filter(vd => vd.getType match {
- case ArrayType(_) => true
- case _ => false
- })
- val mutatedParams = mutableParams.filter(vd => exists {
- case ArrayUpdate(Variable(a), _, _) => a == vd.id
- case _ => false
- }(body))
+ val mutableParams = fd.params.filter(vd => isMutableType(vd.getType))
+ val mutatedParams = mutableParams.filter(vd => exists(expr => isMutationOf(expr, vd.id))(body))
val mutatedParamsIndices = fd.params.zipWithIndex.flatMap{
case (vd, i) if mutatedParams.contains(vd) => Some(i)
case _ => None
@@ -306,10 +321,7 @@ object AntiAliasingPhase extends TransformationPhase {
//TODO: the require should be fine once we consider nested functions as well
//require(effects.isDefinedAt(fi.tfd.fd)
val mutatedParams: Set[Int] = effects.get(fi.tfd.fd).getOrElse(Set())
- fi.args.zipWithIndex.flatMap{
- case (Variable(id), i) if mutatedParams.contains(i) => Some(id)
- case _ => None
- }.toSet
+ functionInvocationEffects(fi, mutatedParams).toSet
}
rec()
@@ -320,8 +332,11 @@ object AntiAliasingPhase extends TransformationPhase {
def checkAliasing(fd: FunDef)(ctx: LeonContext): Unit = {
def checkReturnValue(body: Expr, bindings: Set[Identifier]): Unit = {
getReturnedExpr(body).foreach{
- case IsTyped(v@Variable(id), ArrayType(_)) if bindings.contains(id) =>
- ctx.reporter.fatalError(v.getPos, "Cannot return a shared reference to a mutable object: " + v)
+ case expr if isMutableType(expr.getType) =>
+ findReceiverId(expr).foreach(id =>
+ if(bindings.contains(id))
+ ctx.reporter.fatalError(expr.getPos, "Cannot return a shared reference to a mutable object: " + expr)
+ )
case _ => ()
}
}
@@ -330,21 +345,23 @@ object AntiAliasingPhase extends TransformationPhase {
val params = fd.params.map(_.id).toSet
checkReturnValue(bd, params)
preMapWithContext[Set[Identifier]]((expr, bindings) => expr match {
- case l@Let(id, IsTyped(v, ArrayType(_)), b) => {
+ case l@Let(id, v, b) if isMutableType(v.getType) => {
v match {
case FiniteArray(_, _, _) => ()
case FunctionInvocation(_, _) => ()
case ArrayUpdated(_, _, _) => ()
- case _ => ctx.reporter.fatalError(l.getPos, "Cannot alias array: " + l)
+ case CaseClass(_, _) => ()
+ case _ => ctx.reporter.fatalError(v.getPos, "Illegal aliasing: " + v)
}
(None, bindings + id)
}
- case l@LetVar(id, IsTyped(v, ArrayType(_)), b) => {
+ case l@LetVar(id, v, b) if isMutableType(v.getType) => {
v match {
case FiniteArray(_, _, _) => ()
case FunctionInvocation(_, _) => ()
case ArrayUpdated(_, _, _) => ()
- case _ => ctx.reporter.fatalError(l.getPos, "Cannot alias array: " + l)
+ case CaseClass(_, _) => ()
+ case _ => ctx.reporter.fatalError(v.getPos, "Illegal aliasing: " + v)
}
(None, bindings + id)
}
@@ -380,4 +397,69 @@ object AntiAliasingPhase extends TransformationPhase {
pgm.definedFunctions.flatMap(fd =>
fd.body.toSet.flatMap((bd: Expr) =>
nestedFunDefsOf(bd)) + fd)
+
+
+ private def findReceiverId(o: Expr): Option[Identifier] = o match {
+ case Variable(id) => Some(id)
+ case CaseClassSelector(_, e, _) => findReceiverId(e)
+ case _ => None
+ }
+
+
+ private def isMutableType(tpe: TypeTree): Boolean = tpe match {
+ case (arr: ArrayType) => true
+ case CaseClassType(ccd, _) if ccd.fields.exists(vd => vd.isVar || isMutableType(vd.getType)) => true
+ case _ => false
+ }
+
+
+ /*
+ * Check if expr is mutating variable id
+ */
+ private def isMutationOf(expr: Expr, id: Identifier): Boolean = expr match {
+ case ArrayUpdate(Variable(a), _, _) => a == id
+ case FieldAssignment(obj, _, _) => findReceiverId(obj).exists(_ == id)
+ case _ => false
+ }
+
+ //return the set of modified variables arguments to a function invocation,
+ //given the effect of the fun def invoked.
+ private def functionInvocationEffects(fi: FunctionInvocation, effects: Set[Int]): Seq[Identifier] = {
+ fi.args.map(arg => findReceiverId(arg)).zipWithIndex.flatMap{
+ case (Some(id), i) if effects.contains(i) => Some(id)
+ case _ => None
+ }
+ }
+
+ //private def extractFieldPath(o: Expr): (Expr, List[Identifier]) = {
+ // def rec(o: Expr): List[Identifier] = o match {
+ // case CaseClassSelector(_, r, i) =>
+ // val res = toFieldPath(r)
+ // (res._1, i::res)
+ // case expr => (expr, Nil)
+ // }
+ // val res = rec(o)
+ // (res._1, res._2.reverse)
+ //}
+
+ private def deepCopy(rec: Expr, id: Identifier, nv: Expr): Expr = {
+ val sub = copy(rec, id, nv)
+ rec match {
+ case CaseClassSelector(_, r, i) =>
+ deepCopy(r, i, sub)
+ case expr => sub
+ }
+ }
+
+ private def copy(cc: Expr, id: Identifier, nv: Expr): Expr = {
+ val ct@CaseClassType(ccd, _) = cc.getType
+ val newFields = ccd.fields.map(vd =>
+ if(vd.id == id)
+ nv
+ else
+ CaseClassSelector(CaseClassType(ct.classDef, ct.tps), cc, vd.id)
+ )
+ CaseClass(CaseClassType(ct.classDef, ct.tps), newFields).setPos(cc.getPos)
+ }
+
}
diff --git a/src/main/scala/leon/xlang/Expressions.scala b/src/main/scala/leon/xlang/Expressions.scala
index 802fa217faa4e3803310f3c0950766b7dbdf4063..20e14ed1f0bd0badefa1ffd7c44168c4909b9b27 100644
--- a/src/main/scala/leon/xlang/Expressions.scala
+++ b/src/main/scala/leon/xlang/Expressions.scala
@@ -53,6 +53,18 @@ object Expressions {
}
}
+ case class FieldAssignment(obj: Expr, varId: Identifier, expr: Expr) extends XLangExpr with Extractable with PrettyPrintable {
+ val getType = UnitType
+
+ def extract: Option[(Seq[Expr], Seq[Expr]=>Expr)] = {
+ Some((Seq(obj, expr), (es: Seq[Expr]) => FieldAssignment(es(0), varId, es(1))))
+ }
+
+ def printWith(implicit pctx: PrinterContext) {
+ p"${obj}.${varId} = ${expr};"
+ }
+ }
+
case class While(cond: Expr, body: Expr) extends XLangExpr with Extractable with PrettyPrintable {
val getType = UnitType
var invariant: Option[Expr] = None
diff --git a/src/sphinx/xlang.rst b/src/sphinx/xlang.rst
index 3f88e3e26386064efd82ce4f881164b126d8309b..d2eace3b9120397fcc3bcad70ca79bc167593e23 100644
--- a/src/sphinx/xlang.rst
+++ b/src/sphinx/xlang.rst
@@ -39,35 +39,16 @@ The above example illustrates three new features introduced by XLang:
3. Assignments
You can use Scala variables with a few restrictions. The variables can only be
-declared and used locally in the same function, and inner functions cannot
-close over them. XLang introduces the possibility to use sequences of
-expressions (blocks) -- a feature not available in :ref:`Pure Scala
-<purescala>`, where you're only option is a sequence of ``val`` which
-essentially introduce nested ``let`` declarations.
-
-.. warning::
- Be careful when combining variables with nested functions from PureScala. Leon
- will reject code with nested functions accessing a variable from an outside scope:
-
- .. code-block:: scala
-
- def foo(x: Int) = {
- var a = 12
- def bar(y: Int): Int = {
- a = a + 1
- a + y
- }
- bar(17)
- }
-
- The problem with such code is the complications involved in representing closures as
- they need a pointer to an environment containing the variables. Leon is only able
- to handle closures with ``val``, where it is sufficient to explicitly pass the values
- as parameters.
+declared and used locally, no variable declaration outside of a function body.
+There is also support for variables in case classes constructors. XLang
+introduces the possibility to use sequences of expressions (blocks) -- a
+feature not available in :ref:`Pure Scala <purescala>`, where you're only
+option is a sequence of ``val`` which essentially introduce nested ``let``
+declarations.
While loops
-***********
+-----------
You can use the ``while`` keyword. While loops usually combine the ability to
declare variables and make a sequence of assignments in order to compute
@@ -123,7 +104,7 @@ verification condition is used to prove the invariant on initialization of the
loop.
Arrays
-******
+------
PureScala supports functional arrays, that is, the operations ``apply`` and
``updated`` which do not modify an array but only returns some result. In
@@ -146,8 +127,7 @@ XLang adds the usual ``update`` operation on arrays:
a(1) = 10
a(1) //10
-There are some limitations with what you can do with arrays. Leon simply
-rewrite arrays using ``update`` operation as assignment of function arrays
+Leon simply rewrite arrays using ``update`` operation as assignment of function arrays
using ``updated``. This leverages the built-in algorithm for functional array
and rely on the elimination procedure for assignments. Concretely, it would
transform the above on the following equivalent implementation:
@@ -161,8 +141,91 @@ transform the above on the following equivalent implementation:
Then Leon would apply the same process as for any other XLang program.
-Due to the way Leon handles side-effects, you cannot update arrays passed
-to a function as a parameter.
+Mutable Objects
+---------------
+
+A restricted form of mutable classes is supported via case classes with ``var``
+arguments:
+
+.. code-block:: scala
+
+ case class A(var x: Int)
+ def f(): Int = {
+ val a = new A(10)
+ a.x = 13
+ a.x
+ }
+
+Mutable case classes are behaving similarly to ``Array``, and are handled with a
+rewriting, where each field updates becomes essentially a copy of the object with
+the modified parameter changed.
+
+Aliasing
+--------
+
+With mutable data structures comes the problem of aliasing. In Leon, we
+maintain the invariant that in any scope, there is at most one pointer to some
+mutable structure. Leon will issue an error if you try to create an alias to
+some mutable structure in the same scope:
+
+.. code-block:: scala
+
+ val a = Array(1,2,3,4)
+ val b = a //error: illegal aliasing
+ b(0) = 10
+ assert(a(0) == 10)
+
+However, Leon correctly supports aliasing mutable structures when passing it
+as a parameter to a function (assuming its scope is not shared with the call
+site, i.e. not a nested function). Essentially you can do:
+
+.. code-block:: scala
+
+ case class A(var x: Int)
+ def updateA(a: A): Unit = {
+ a.x = 14
+ }
+ def f(): Unit = {
+ val a = A(10)
+ updateA(a)
+ assert(a.x == 14)
+ }
+
+The function ``updateA`` will have the side effect of updating its argument
+``a`` and this will be visible at the call site.
+
+Annotations for Imperative Programming
+--------------------------------------
+
+XLang introduces the special function ``old`` that can be used in postconditions to
+talk about the value of a variable before the execution of the block. When you refer to a variable
+or mutable structure in a post-condition, leon will always consider the current value of
+the object, so that in the case of a post-condition this would refer to the final value of the
+object. Using ``old``, you can refer to the original value of the variable and check some
+properties:
+
+.. code-block:: scala
+
+ case class A(var x: Int)
+ def inc(a: A): Unit = {
+ a.x = a.x + 1
+ } ensuring(_ => a.x == old(a).x + 1)
+
+``old`` can be wrapped around any identifier that is affected by the body. You can also use
+``old`` for variables in scope, in case of nested functions:
+
+.. code-block:: scala
+
+ def f(): Int = {
+ var x = 0
+ def inc(): Unit = {
+ x = x + 1
+ } ensuring(_ => x == old(x) + 1)
+
+ inc(); inc();
+ assert(x == 2)
+ }
+
Epsilon
-------
diff --git a/src/test/resources/regression/verification/xlang/invalid/FunctionCaching.scala b/src/test/resources/regression/verification/xlang/invalid/FunctionCaching.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1ba4c5b2855f504cc8b0e669678dfd3ba47edbba
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/FunctionCaching.scala
@@ -0,0 +1,33 @@
+import leon.lang._
+import leon.collection._
+
+object FunctionCaching {
+
+ case class FunCache(var cached: Map[BigInt, BigInt])
+
+ def fun(x: BigInt)(implicit funCache: FunCache): BigInt = {
+ funCache.cached.get(x) match {
+ case None() =>
+ val res = 2*x + 42
+ funCache.cached = funCache.cached.updated(x, res)
+ res
+ case Some(cached) =>
+ cached + 1
+ }
+ }
+
+ def funWronglyCached(x: BigInt, trash: List[BigInt]): Boolean = {
+ implicit val cache = FunCache(Map())
+ val res1 = fun(x)
+ multipleCalls(trash)
+ val res2 = fun(x)
+ res1 == res2
+ } holds
+
+
+ def multipleCalls(args: List[BigInt])(implicit funCache: FunCache): Unit = args match {
+ case Nil() => ()
+ case x::xs => fun(x); multipleCalls(xs)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/FunctionCaching.scala b/src/test/resources/regression/verification/xlang/valid/FunctionCaching.scala
new file mode 100644
index 0000000000000000000000000000000000000000..322cb592ee44a65add6f1eed42ba8fea7fba4155
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/FunctionCaching.scala
@@ -0,0 +1,40 @@
+import leon.lang._
+import leon.collection._
+
+object FunctionCaching {
+
+ case class FunCache(var cached: Map[BigInt, BigInt])
+
+ def fun(x: BigInt)(implicit funCache: FunCache): BigInt = {
+ funCache.cached.get(x) match {
+ case None() =>
+ val res = 2*x + 42
+ funCache.cached = funCache.cached.updated(x, res)
+ res
+ case Some(cached) =>
+ cached
+ }
+ } ensuring(res => old(funCache).cached.get(x) match {
+ case None() => true
+ case Some(v) => v == res
+ })
+
+ def funProperlyCached(x: BigInt, trash: List[BigInt]): Boolean = {
+ implicit val cache = FunCache(Map())
+ val res1 = fun(x)
+ multipleCalls(trash, x)
+ val res2 = fun(x)
+ res1 == res2
+ } holds
+
+ def multipleCalls(args: List[BigInt], x: BigInt)(implicit funCache: FunCache): Unit = {
+ require(funCache.cached.get(x).forall(_ == 2*x + 42))
+ args match {
+ case Nil() => ()
+ case y::ys =>
+ fun(y)
+ multipleCalls(ys, x)
+ }
+ } ensuring(_ => funCache.cached.get(x).forall(_ == 2*x + 42))
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation1.scala b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..52e7083346486740d2915835ea584a7fcb020f06
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation1.scala
@@ -0,0 +1,13 @@
+import leon.lang._
+
+object ObjectHierarchyMutation1 {
+
+ case class A(var y: Int)
+ case class B(a: A)
+
+ def update(b: B): Int = {
+ b.a.y = 17
+ b.a.y
+ } ensuring(res => res == 17)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation2.scala b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1d1df5dc47dc202cb502e252614dfd3293f8d2d3
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation2.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+
+object ObjectHierarchyMutation2 {
+
+ case class A(var y: Int)
+ case class B(a: A)
+
+ def update(b: B): Int = {
+ b.a.y = 17
+ b.a.y
+ }
+
+ def f(): Int = {
+ val b = B(A(10))
+ update(b)
+ b.a.y
+ } ensuring(res => res == 17)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation3.scala b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..67df97f0467312148b013569aede16c9c52f0480
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation3.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+
+object ObjectHierarchyMutation3 {
+
+ case class A(var x: Int, var y: Int, var z: Int)
+ case class B(a1: A, a2: A, a3: A)
+
+ def update(b: B): Int = {
+ b.a2.y = 17
+ b.a2.y
+ } ensuring(res => res == 17)
+
+ def f(): Int = {
+ val b = B(A(10, 11, 12), A(11, 12, 13), A(13, 14, 15))
+ update(b)
+ b.a2.y
+ } ensuring(res => res == 17)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation4.scala b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..807142699cf8fbf85b200759936a612379fad7ac
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation4.scala
@@ -0,0 +1,27 @@
+import leon.lang._
+
+object ObjectHierarchyMutation4 {
+
+ case class A(var x: Int, var y: Int)
+ case class B(a1: A, a2: A)
+ case class C(b1: B, b2: B)
+
+ def update(c: C): Int = {
+ c.b1.a2.y = 17
+ c.b1.a2.y
+ } ensuring(res => res == 17)
+
+ def f(): Int = {
+ val c = C(B(A(10, 10), A(12, 13)), B(A(10, 10), A(14, 15)))
+ update(c)
+ c.b1.a2.y
+ } ensuring(res => res == 17)
+
+ def multipleUpdate(c: C): Unit = {
+ c.b1.a2.y = 13
+ c.b1.a2.x = 10
+ c.b1.a1.x = 15
+ c.b2.a1.y = 22
+ } ensuring(_ => c.b1.a2.y == 13 && c.b1.a2.x == 10 && c.b1.a1.x == 15 && c.b2.a1.y == 22 && c.b2.a2.y == old(c).b2.a2.y)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation5.scala b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ab237ab281d60effcf078bd0c536dacd0edb8aad
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation5.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+
+object ObjectHierarchyMutation5 {
+
+ case class A(var x: Int)
+ case class B(a: A)
+ case class C(b: B)
+
+ def updateA(a: A): Unit = {
+ a.x = 43
+ }
+
+ def update(c: C): Int = {
+ updateA(c.b.a)
+ c.b.a.x
+ } ensuring(res => res == 43)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation6.scala b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7361adf0068fbad093382620c18c6aed40f9802e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation6.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+
+object ObjectHierarchyMutation6 {
+
+ case class A(var x: Int, var y: Int)
+ case class B(a1: A, a2: A)
+ case class C(b1: B, b2: B)
+
+ def updateA(a: A): Unit = {
+ a.x = 43
+ }
+
+ def update(c: C): Int = {
+ updateA(c.b2.a1)
+ c.b2.a1.x
+ } ensuring(res => res == 43)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation7.scala b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f9c7a9198dfb90cf3545e28beabdfe2489480983
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectHierarchyMutation7.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+
+object ObjectHierarchyMutation7 {
+
+ case class A(var x: Int, var y: Int)
+ case class B(a1: A, a2: A)
+ case class C(b1: B, b2: B)
+
+ def updateB(b: B): Unit = {
+ b.a1.x = 43
+ }
+
+ def update(c: C): Int = {
+ updateB(c.b2)
+ c.b2.a1.x
+ } ensuring(res => res == 43)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation1.scala b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b36fd6f1a3a59864c5cca195f17264b382b6652e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation1.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+
+object ObjectParamMutation1 {
+
+ case class A(var y: Int)
+
+ def update(a: A): Int = {
+ a.y = 12
+ a.y
+ } ensuring(res => res == 12)
+
+ def f(): Int = {
+ val a = A(10)
+ update(a)
+ a.y
+ } ensuring(res => res == 12)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation2.scala b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7a7590eb3644633ac479de81e3a046109aa48b4c
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation2.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object ObjectParamMutation2 {
+
+ case class A(var y: Int)
+
+ def update(a: A): Unit = {
+ a.y = 12
+ } ensuring(_ => a.y == 12)
+
+ def f(): Int = {
+ val a = A(10)
+ update(a)
+ a.y
+ } ensuring(res => res == 12)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation3.scala b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..95c88cb571e52e434155c052f0dba750a4fc81a6
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation3.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object ObjectParamMutation3 {
+
+ case class A(var y: Int)
+
+ def update(a: A): Unit = {
+ a.y = a.y + 3
+ } ensuring(_ => a.y == old(a).y + 3)
+
+ def f(): Int = {
+ val a = A(10)
+ update(a)
+ a.y
+ } ensuring(res => res == 13)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation4.scala b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5b50ddb63a9be4ee36cfb39a71ea19b766da9d70
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation4.scala
@@ -0,0 +1,22 @@
+import leon.lang._
+
+object ObjectParamMutation4 {
+
+ case class A(var y: Int)
+
+ def swapY(a1: A, a2: A): Unit = {
+ val tmp = a1.y
+ a1.y = a2.y
+ a2.y = tmp
+ } ensuring(_ => a1.y == old(a2).y && a2.y == old(a1).y)
+
+ def f(): (Int, Int) = {
+ val a1 = A(10)
+ val a2 = A(10)
+ a1.y = 12
+ a2.y = 42
+ swapY(a1, a2)
+ (a1.y, a2.y)
+ } ensuring(res => res._1 == 42 && res._2 == 12)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation5.scala b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..38580345d6540ab92625ba199da2f11b536ae3be
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation5.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+
+object ObjectParamMutation5 {
+
+ case class A(var x: Int, var y: Int)
+
+ def swap(a: A): Unit = {
+ val tmp = a.x
+ a.x = a.y
+ a.y = tmp
+ } ensuring(_ => a.x == old(a).y && a.y == old(a).x)
+
+ def f(): A = {
+ val a = A(10, 13)
+ swap(a)
+ a
+ } ensuring(res => res.x == 13 && res.y == 10)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation6.scala b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6c917ff1b4c85e6deabf41cfbadfd0097138c315
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation6.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object ObjectParamMutation6 {
+
+ case class A(var x: BigInt)
+
+ def inc(a: A): Unit = {
+ a.x += 1
+ } ensuring(_ => a.x == old(a).x + 1)
+
+ def f(): BigInt = {
+ val a = A(0)
+ inc(a); inc(a); inc(a)
+ a.x
+ } ensuring(res => res == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation7.scala b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9f664837e3cc56cdd78a9daab7b3587f907e9798
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation7.scala
@@ -0,0 +1,20 @@
+import leon.lang._
+
+object ObjectParamMutation7 {
+
+ case class A(a: Int, var x: BigInt, var y: BigInt, var z: BigInt)
+
+ def inc(a: A): Unit = {
+ require(a.x >= 0 && a.y >= 0 && a.z >= 0)
+ a.x += 1
+ a.y += 1
+ a.z += 1
+ } ensuring(_ => a.x == old(a).x + 1 && a.y == old(a).y + 1 && a.z == old(a).z + 1)
+
+ def f(): A = {
+ val a = A(0, 0, 0, 0)
+ inc(a); inc(a); inc(a)
+ a
+ } ensuring(res => res.x == res.y && res.y == res.z && res.z == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation8.scala b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..eb1d157c4d0936c8f28f37b8b69065e34d811253
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ObjectParamMutation8.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+
+object ObjectParamMutation8 {
+
+ case class A[B](var y: B)
+
+ def update[B](a: A[B], b: B): B = {
+ a.y = b
+ a.y
+ } ensuring(res => res == b)
+
+ def f(): Int = {
+ val a = A(10)
+ update(a, 12)
+ a.y
+ } ensuring(res => res == 12)
+
+}
diff --git a/src/test/resources/regression/xlang/error/MutableFieldAliasing1.scala b/src/test/resources/regression/xlang/error/MutableFieldAliasing1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1d3e7ed03fdf778f52b12912521e9436c0d88e2e
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/MutableFieldAliasing1.scala
@@ -0,0 +1,22 @@
+import leon.lang._
+
+object MutableFieldAliasing1 {
+
+ case class A(var x: Int)
+ case class B(a: A)
+
+ def f1(): Int = {
+ val b1 = B(A(10))
+ val b2 = b1
+ b2.a.x = 15
+ b1.a.x
+ } ensuring(_ == 15)
+
+
+ def build(x: Int): B = {
+ val a = A(x)
+ B(a)
+ }
+
+}
+
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing1.scala b/src/test/resources/regression/xlang/error/ObjectAliasing1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7634e1071e032719cbe6179300bc9dea50f11fc6
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing1.scala
@@ -0,0 +1,15 @@
+import leon.lang._
+
+object ObjectAliasing1 {
+
+ case class A(var x: Int)
+
+ def f1(): Int = {
+ val a = A(10)
+ val b = a
+ b.x = 15
+ a.x
+ } ensuring(_ == 15)
+
+}
+
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing2.scala b/src/test/resources/regression/xlang/error/ObjectAliasing2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..af39dba1e7612f64c0f1926d39f2fe601b2b36ae
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing2.scala
@@ -0,0 +1,13 @@
+import leon.lang._
+
+object ObjectAliasing2 {
+
+ case class A(var x: Int)
+
+ def f1(a: A): Int = {
+ val b = a
+ b.x = 10
+ a.x
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing3.scala b/src/test/resources/regression/xlang/error/ObjectAliasing3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9d419ea95e6e84d5f7b63f81cb2df5359ebe1711
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing3.scala
@@ -0,0 +1,13 @@
+import leon.lang._
+
+object ObjectAliasing3 {
+
+ case class A(var x: Int)
+
+ def f1(a: A, b: Boolean): Int = {
+ val c = if(b) a else A(42)
+ c.x = 10
+ a.x
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing4.scala b/src/test/resources/regression/xlang/error/ObjectAliasing4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..81cabf97be708e715245a27fb735e1a88ee00e82
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing4.scala
@@ -0,0 +1,12 @@
+import leon.lang._
+
+object ObjectAliasing4 {
+
+ case class A(var x: Int)
+
+ def f1(a: A): A = {
+ a.x = 10
+ a
+ } ensuring(res => res.x == 10)
+
+}
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing5.scala b/src/test/resources/regression/xlang/error/ObjectAliasing5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c94656fdb9fba7d52b8eef76a7acb547682a2cdc
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing5.scala
@@ -0,0 +1,12 @@
+import leon.lang._
+
+object ObjectAliasing5 {
+
+ case class A(var x: Int)
+ case class B(a: A)
+
+ def f1(b: B): A = {
+ b.a
+ }
+
+}
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing6.scala b/src/test/resources/regression/xlang/error/ObjectAliasing6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..793b9815d35635ae7539268e9b2d8878bc6a985d
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing6.scala
@@ -0,0 +1,14 @@
+import leon.lang._
+
+object ObjectAliasing6 {
+
+ case class A(var x: Int)
+ case class B(a: A)
+
+ def f1(b: B): Int = {
+ val a = b.a
+ a.x = 12
+ b.a.x
+ } ensuring(_ == 12)
+
+}
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing7.scala b/src/test/resources/regression/xlang/error/ObjectAliasing7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ea28fa5bb2e01970d64c0259fc4c8d97a6878584
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing7.scala
@@ -0,0 +1,22 @@
+package test.resources.regression.xlang.error
+
+import leon.lang._
+
+object ObjectAliasing7 {
+
+ case class A(var x: Int)
+ case class B(a: A)
+
+ def f1(a1: A, a2: A): Int = {
+ val tmp = a1.x
+ a2.x = a1.x
+ a1.x = tmp
+ a1.x + a2.x
+ }
+
+ def f(): Int = {
+ val b = B(A(10))
+ f1(b.a, b.a)
+ } ensuring(_ == 20)
+
+}
diff --git a/src/test/resources/regression/xlang/passing/FunctionCaching.scala b/src/test/resources/regression/xlang/passing/FunctionCaching.scala
new file mode 100644
index 0000000000000000000000000000000000000000..322cb592ee44a65add6f1eed42ba8fea7fba4155
--- /dev/null
+++ b/src/test/resources/regression/xlang/passing/FunctionCaching.scala
@@ -0,0 +1,40 @@
+import leon.lang._
+import leon.collection._
+
+object FunctionCaching {
+
+ case class FunCache(var cached: Map[BigInt, BigInt])
+
+ def fun(x: BigInt)(implicit funCache: FunCache): BigInt = {
+ funCache.cached.get(x) match {
+ case None() =>
+ val res = 2*x + 42
+ funCache.cached = funCache.cached.updated(x, res)
+ res
+ case Some(cached) =>
+ cached
+ }
+ } ensuring(res => old(funCache).cached.get(x) match {
+ case None() => true
+ case Some(v) => v == res
+ })
+
+ def funProperlyCached(x: BigInt, trash: List[BigInt]): Boolean = {
+ implicit val cache = FunCache(Map())
+ val res1 = fun(x)
+ multipleCalls(trash, x)
+ val res2 = fun(x)
+ res1 == res2
+ } holds
+
+ def multipleCalls(args: List[BigInt], x: BigInt)(implicit funCache: FunCache): Unit = {
+ require(funCache.cached.get(x).forall(_ == 2*x + 42))
+ args match {
+ case Nil() => ()
+ case y::ys =>
+ fun(y)
+ multipleCalls(ys, x)
+ }
+ } ensuring(_ => funCache.cached.get(x).forall(_ == 2*x + 42))
+
+}
diff --git a/src/test/resources/regression/xlang/passing/FunctionCachingInvalid.scala b/src/test/resources/regression/xlang/passing/FunctionCachingInvalid.scala
new file mode 100644
index 0000000000000000000000000000000000000000..07a889f780cd1ab911fc072a92d5508f17de2579
--- /dev/null
+++ b/src/test/resources/regression/xlang/passing/FunctionCachingInvalid.scala
@@ -0,0 +1,33 @@
+import leon.lang._
+import leon.collection._
+
+object FunctionCachingInvalid {
+
+ case class FunCache(var cached: Map[BigInt, BigInt])
+
+ def fun(x: BigInt)(implicit funCache: FunCache): BigInt = {
+ funCache.cached.get(x) match {
+ case None() =>
+ val res = 2*x + 42
+ funCache.cached = funCache.cached.updated(x, res)
+ res
+ case Some(cached) =>
+ cached + 1
+ }
+ }
+
+ def funWronglyCached(x: BigInt, trash: List[BigInt]): Boolean = {
+ implicit val cache = FunCache(Map())
+ val res1 = fun(x)
+ multipleCalls(trash)
+ val res2 = fun(x)
+ res1 == res2
+ } holds
+
+
+ def multipleCalls(args: List[BigInt])(implicit funCache: FunCache): Unit = args match {
+ case Nil() => ()
+ case x::xs => fun(x); multipleCalls(xs)
+ }
+
+}
diff --git a/src/test/resources/regression/xlang/passing/ObjectParamMutation1.scala b/src/test/resources/regression/xlang/passing/ObjectParamMutation1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b36fd6f1a3a59864c5cca195f17264b382b6652e
--- /dev/null
+++ b/src/test/resources/regression/xlang/passing/ObjectParamMutation1.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+
+object ObjectParamMutation1 {
+
+ case class A(var y: Int)
+
+ def update(a: A): Int = {
+ a.y = 12
+ a.y
+ } ensuring(res => res == 12)
+
+ def f(): Int = {
+ val a = A(10)
+ update(a)
+ a.y
+ } ensuring(res => res == 12)
+
+}
diff --git a/src/test/resources/regression/xlang/passing/ObjectParamMutation7.scala b/src/test/resources/regression/xlang/passing/ObjectParamMutation7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9f664837e3cc56cdd78a9daab7b3587f907e9798
--- /dev/null
+++ b/src/test/resources/regression/xlang/passing/ObjectParamMutation7.scala
@@ -0,0 +1,20 @@
+import leon.lang._
+
+object ObjectParamMutation7 {
+
+ case class A(a: Int, var x: BigInt, var y: BigInt, var z: BigInt)
+
+ def inc(a: A): Unit = {
+ require(a.x >= 0 && a.y >= 0 && a.z >= 0)
+ a.x += 1
+ a.y += 1
+ a.z += 1
+ } ensuring(_ => a.x == old(a).x + 1 && a.y == old(a).y + 1 && a.z == old(a).z + 1)
+
+ def f(): A = {
+ val a = A(0, 0, 0, 0)
+ inc(a); inc(a); inc(a)
+ a
+ } ensuring(res => res.x == res.y && res.y == res.z && res.z == 3)
+
+}
diff --git a/testcases/verification/xlang/BankSimpleTransactions.scala b/testcases/verification/xlang/BankSimpleTransactions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..46a4d6a2be909b548e9064455f10b6c095080b90
--- /dev/null
+++ b/testcases/verification/xlang/BankSimpleTransactions.scala
@@ -0,0 +1,73 @@
+import leon.lang._
+
+object BankSimpleTransactions {
+
+ def okTransaction(): Unit = {
+ var balance: BigInt = 0
+
+ def balanceInvariant: Boolean = balance >= 0
+
+ def deposit(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0)
+ balance += x
+ } ensuring(_ => balance == old(balance) + x && balanceInvariant)
+
+ def withdrawal(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0 && x <= balance)
+ balance -= x
+ } ensuring(_ => balance == old(balance) - x && balanceInvariant)
+
+ deposit(35)
+ withdrawal(30)
+ }
+
+ def invalidTransaction(): Unit = {
+ var balance: BigInt = 0
+
+ def balanceInvariant: Boolean = balance >= 0
+
+ def deposit(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0)
+ balance += x
+ } ensuring(_ => balance == old(balance) + x && balanceInvariant)
+
+ def withdrawal(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0 && x <= balance)
+ balance -= x
+ } ensuring(_ => balance == old(balance) - x && balanceInvariant)
+
+ deposit(35)
+ withdrawal(40)
+ }
+
+
+ def internalTransfer(): Unit = {
+ var checking: BigInt = 0
+ var saving: BigInt = 0
+
+ def balance = checking + saving
+
+ def balanceInvariant: Boolean = balance >= 0
+
+ def deposit(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0)
+ checking += x
+ } ensuring(_ => checking == old(checking) + x && balanceInvariant)
+
+ def withdrawal(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0 && x <= checking)
+ checking -= x
+ } ensuring(_ => checking == old(checking) - x && balanceInvariant)
+
+ def checkingToSaving(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0 && checking >= x)
+ checking -= x
+ saving += x
+ } ensuring(_ => checking + saving == old(checking) + old(saving) && balanceInvariant)
+
+ deposit(50)
+ withdrawal(30)
+ checkingToSaving(10)
+ }
+
+}
diff --git a/testcases/verification/xlang/BankTransfer.scala b/testcases/verification/xlang/BankTransfer.scala
index c533b4e08a6297446aad36d7a31fd04e148ccc37..2044df06ae01907a0df26e876ae4784feab6b0ce 100644
--- a/testcases/verification/xlang/BankTransfer.scala
+++ b/testcases/verification/xlang/BankTransfer.scala
@@ -2,72 +2,39 @@ import leon.lang._
object BankTransfer {
- def okTransaction(): Unit = {
- var balance: BigInt = 0
+ case class BankAccount(var checking: BigInt, var saving: BigInt) {
+ require(checking >= 0 && saving >= 0)
- def balanceInvariant: Boolean = balance >= 0
-
- def deposit(x: BigInt): Unit = {
- require(balanceInvariant && x >= 0)
- balance += x
- } ensuring(_ => balance == old(balance) + x && balanceInvariant)
-
- def withdrawal(x: BigInt): Unit = {
- require(balanceInvariant && x >= 0 && x <= balance)
- balance -= x
- } ensuring(_ => balance == old(balance) - x && balanceInvariant)
-
- deposit(35)
- withdrawal(30)
+ def balance: BigInt = checking + saving
}
- def invalidTransaction(): Unit = {
- var balance: BigInt = 0
+ //TODO: support for map references to mutable items
+ //case class Bank(accounts: Map[BigInt, BankAccount])
- def balanceInvariant: Boolean = balance >= 0
- def deposit(x: BigInt): Unit = {
- require(balanceInvariant && x >= 0)
- balance += x
- } ensuring(_ => balance == old(balance) + x && balanceInvariant)
-
- def withdrawal(x: BigInt): Unit = {
- require(balanceInvariant && x >= 0 && x <= balance)
- balance -= x
- } ensuring(_ => balance == old(balance) - x && balanceInvariant)
-
- deposit(35)
- withdrawal(40)
- }
+ def deposit(x: BigInt, account: BankAccount): Unit = {
+ require(x > 0)
+ account.checking = account.checking + x
+ } ensuring(_ => account.balance == old(account).balance + x)
+ def withdrawal(x: BigInt, account: BankAccount): Unit = {
+ require(x > 0 && account.checking >= x)
+ account.checking = account.checking - x
+ } ensuring(_ => account.balance == old(account).balance - x)
- def internalTransfer(): Unit = {
- var checking: BigInt = 0
- var saving: BigInt = 0
+ def transfer(x: BigInt, a1: BankAccount, a2: BankAccount): Unit = {
+ require(x > 0 && a1.checking >= x)
+ withdrawal(x, a1)
+ deposit(x, a2)
+ } ensuring(_ => a1.balance + a2.balance == old(a1).balance + old(a2).balance &&
+ a1.balance == old(a1).balance - x &&
+ a2.balance == old(a2).balance + x)
- def balance = checking + saving
- def balanceInvariant: Boolean = balance >= 0
-
- def deposit(x: BigInt): Unit = {
- require(balanceInvariant && x >= 0)
- checking += x
- } ensuring(_ => checking == old(checking) + x && balanceInvariant)
-
- def withdrawal(x: BigInt): Unit = {
- require(balanceInvariant && x >= 0 && x <= checking)
- checking -= x
- } ensuring(_ => checking == old(checking) - x && balanceInvariant)
-
- def checkingToSaving(x: BigInt): Unit = {
- require(balanceInvariant && x >= 0 && checking >= x)
- checking -= x
- saving += x
- } ensuring(_ => checking + saving == old(checking) + old(saving) && balanceInvariant)
-
- deposit(50)
- withdrawal(30)
- checkingToSaving(10)
- }
+ def save(x: BigInt, account: BankAccount): Unit = {
+ require(x > 0 && account.checking >= x)
+ account.checking = account.checking - x
+ account.saving = account.saving + x
+ } ensuring(_ => account.balance == old(account).balance)
}
diff --git a/testcases/verification/xlang/FunctionCaching.scala b/testcases/verification/xlang/FunctionCaching.scala
new file mode 100644
index 0000000000000000000000000000000000000000..75c73e822831a5d7da9a209f1964d36e10298359
--- /dev/null
+++ b/testcases/verification/xlang/FunctionCaching.scala
@@ -0,0 +1,40 @@
+import leon.lang._
+import leon.collection._
+
+object FunctionCaching {
+
+ case class CachedFun[A,B](fun: (A) => B, var cached: Map[A, B], var cacheHit: Set[A]) {
+
+ def call(a: A): B = {
+ cached.get(a) match {
+ case None() =>
+ val res = fun(a)
+ cached = cached.updated(a, res)
+ res
+ case Some(res) =>
+ cacheHit = cacheHit ++ Set(a)
+ res
+ }
+ }
+
+ }
+
+ def funProperlyCached(x: BigInt, fun: (BigInt) => BigInt, trash: List[BigInt]): Boolean = {
+ val cachedFun = CachedFun[BigInt, BigInt](fun, Map(), Set())
+ val res1 = cachedFun.call(x)
+ multipleCalls(trash, cachedFun, x)
+ val res2 = cachedFun.call(x)
+ res1 == res2 && cachedFun.cacheHit.contains(x)
+ } holds
+
+ def multipleCalls(args: List[BigInt], cachedFun: CachedFun[BigInt, BigInt], x: BigInt): Unit = {
+ require(cachedFun.cached.isDefinedAt(x))
+ args match {
+ case Nil() => ()
+ case y::ys =>
+ cachedFun.call(x)
+ multipleCalls(ys, cachedFun, x)
+ }
+ } ensuring(_ => old(cachedFun).cached.get(x) == cachedFun.cached.get(x))
+
+}