From efdc33905802b19057d1f377773c5e06dd1036d4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Wed, 18 May 2016 10:49:12 +0200
Subject: [PATCH] Fixed a bug in bytecode for calling bigSubstring Added
copiedFrom when extracting pre and postconditions. Added lookup functions for
extracting similar expressions. Fixed a bug when converting substring to CVC4
target.
---
.../scala/leon/codegen/CodeGeneration.scala | 2 +-
src/main/scala/leon/purescala/ExprOps.scala | 4 ++--
src/main/scala/leon/purescala/GenTreeOps.scala | 17 +++++++++++++++++
.../leon/solvers/smtlib/SMTLIBCVC4Target.scala | 2 +-
.../verification/VerificationCondition.scala | 11 +++++++++++
5 files changed, 32 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 199fd8669..40f745a33 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -904,7 +904,7 @@ trait CodeGeneration {
mkExpr(a, ch)
mkExpr(start, ch)
mkExpr(end, ch)
- ch << InvokeStatic(StrOpsClass, "bigSubstring", s"(L$JavaStringClass;II)L$JavaStringClass;")
+ ch << InvokeStatic(StrOpsClass, "bigSubstring", s"(L$JavaStringClass;L$BigIntClass;L$BigIntClass;)L$JavaStringClass;")
// Arithmetic
case Plus(l, r) =>
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 63afebf48..ae2774a7e 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1934,7 +1934,7 @@ object ExprOps extends GenTreeOps[Expr] {
/** Returns the precondition of an expression wrapped in Option */
def preconditionOf(expr: Expr): Option[Expr] = expr match {
- case Let(i, e, b) => preconditionOf(b).map(Let(i, e, _))
+ case Let(i, e, b) => preconditionOf(b).map(Let(i, e, _).copiedFrom(expr))
case Require(pre, _) => Some(pre)
case Ensuring(Require(pre, _), _) => Some(pre)
case b => None
@@ -1942,7 +1942,7 @@ object ExprOps extends GenTreeOps[Expr] {
/** Returns the postcondition of an expression wrapped in Option */
def postconditionOf(expr: Expr): Option[Expr] = expr match {
- case Let(i, e, b) => postconditionOf(b).map(Let(i, e, _))
+ case Let(i, e, b) => postconditionOf(b).map(Let(i, e, _).copiedFrom(expr))
case Ensuring(_, post) => Some(post)
case _ => None
}
diff --git a/src/main/scala/leon/purescala/GenTreeOps.scala b/src/main/scala/leon/purescala/GenTreeOps.scala
index a8ced2704..286b1ae23 100644
--- a/src/main/scala/leon/purescala/GenTreeOps.scala
+++ b/src/main/scala/leon/purescala/GenTreeOps.scala
@@ -415,6 +415,23 @@ trait GenTreeOps[SubTree <: Tree] {
fold[Int]{ (_, sub) => 1 + (0 +: sub).max }(e)
}
+ /** Given a tree `toSearch` present in `treeToLookInto`, if `treeToLookInto` has the same shape as `treeToExtract`,
+ * returns the matching expression in `treeToExtract``.*/
+ def lookup[T](checker: SubTree => Boolean, toExtract: SubTree => T)(treeToLookInto: SubTree, treeToExtract: SubTree): Option[T] = {
+ if(checker(treeToLookInto)) return Some(toExtract(treeToExtract))
+
+ val Deconstructor(childrenToLookInto, _) = treeToLookInto
+ val Deconstructor(childrenToReturn, _) = treeToExtract
+ if(childrenToLookInto.size != childrenToReturn.size) return None
+ for((l, r) <- childrenToLookInto.zip(childrenToReturn)) {
+ lookup(checker, toExtract)(l, r) match {
+ case s@Some(n) => return s
+ case _ =>
+ }
+ }
+ return None
+ }
+
object Same {
def unapply(tt: (SubTree, SubTree)): Option[(SubTree, SubTree)] = {
if (tt._1.getClass == tt._2.getClass) {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index bd1ef5448..4e24f6c8e 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -178,7 +178,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
case StringConcat(a, b) => Strings.Concat(toSMT(a), toSMT(b))
case SubString(a, start, BVPlus(start2, length)) if start == start2 =>
Strings.Substring(toSMT(a),toSMT(start),toSMT(length))
- case SubString(a, start, end) => Strings.Substring(toSMT(a),toSMT(start),toSMT(Minus(end, start)))
+ case SubString(a, start, end) => Strings.Substring(toSMT(a),toSMT(start),toSMT(BVMinus(end, start)))
case BigSubString(a, start, Plus(start2, length)) if start == start2 =>
Strings.Substring(toSMT(a),toSMT(start),toSMT(length))
case BigSubString(a, start, end) => Strings.Substring(toSMT(a),toSMT(start),toSMT(Minus(end, start)))
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index d7850d079..117380725 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -6,6 +6,7 @@ import leon.purescala.Expressions._
import leon.purescala.Definitions._
import leon.purescala.Types._
import leon.purescala.PrettyPrinter
+import leon.purescala.ExprOps
import leon.utils.Positioned
import leon.solvers._
import leon.LeonContext
@@ -16,6 +17,16 @@ case class VC(condition: Expr, fd: FunDef, kind: VCKind) extends Positioned {
override def toString = {
fd.id.name +" - " +kind.toString
}
+ // If the two functions are the same but have different positions, used to transfer one to the other.
+ def copyTo(newFun: FunDef) = {
+ val thisPos = this.getPos
+ val newPos = ExprOps.lookup(_.getPos == thisPos, _.getPos)(fd.fullBody, newFun.fullBody) match {
+ case Some(position) => position
+ case None => newFun.getPos
+ }
+ val newCondition = ExprOps.lookup(condition == _, i => i)(fd.fullBody, newFun.fullBody).getOrElse(condition)
+ VC(newCondition, newFun, kind).setPos(newPos)
+ }
}
abstract class VCKind(val name: String, val abbrv: String) {
--
GitLab