From 5a527dd15e7f38460a6c9e6b687a20c23c3effd7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 4 May 2012 11:29:47 +0200
Subject: [PATCH] path constraint of let in function closure might cause issues
with array equality
---
src/main/scala/leon/ArrayTransformation.scala | 13 ++++++-------
src/main/scala/leon/FunctionClosure.scala | 4 ++--
2 files changed, 8 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 09fcec912..552bf38a3 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -28,18 +28,18 @@ object ArrayTransformation extends Pass {
})
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:_*)
- fd2fd += (fd -> freshFunDef)
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)
})}
@@ -76,7 +76,7 @@ object ArrayTransformation extends Pass {
val ir = transform(i)
val length = TupleSelect(ar, 2).setType(Int32Type)
IfExpr(
- And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
+ And(GreaterEquals(ir, IntLiteral(0)), LessThan(ir, length)),
ArraySelect(TupleSelect(ar, 1), ir).setType(sel.getType).setPosInfo(sel),
Error("Index out of bound").setType(sel.getType).setPosInfo(sel)
).setType(sel.getType)
@@ -88,14 +88,13 @@ object ArrayTransformation extends Pass {
val Variable(id) = ar
val length = TupleSelect(ar, 2).setType(Int32Type)
val array = TupleSelect(ar, 1).setType(ArrayType(v.getType))
- //val Tuple(Seq(Variable(id), length)) = ar
IfExpr(
And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
Block(Seq(
Assignment(
id,
Tuple(Seq(
- ArrayUpdated(array, i, v).setType(array.getType).setPosInfo(up),
+ ArrayUpdated(array, ir, vr).setType(array.getType).setPosInfo(up),
length)
).setType(TupleType(Seq(array.getType, Int32Type))))),
IntLiteral(0)),
@@ -162,12 +161,12 @@ object ArrayTransformation extends Pass {
})
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:_*)
- fd2fd += (fd -> freshFunDef)
freshFunDef
} else fd
val newBody = transform(body)
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index d9426510e..f89ed4b3b 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -87,9 +87,9 @@ object FunctionClosure extends Pass {
}
case l @ Let(i,e,b) => {
val re = functionClosure(e, bindedVars)
- pathConstraints ::= Equals(Variable(i), re)
+ //pathConstraints ::= Equals(Variable(i), re)
val rb = functionClosure(b, bindedVars + i)
- pathConstraints = pathConstraints.tail
+ //pathConstraints = pathConstraints.tail
Let(i, re, rb).setType(l.getType)
}
case n @ NAryOperator(args, recons) => {
--
GitLab