From ee9dc4955d5ba10f47a1deb235976e0b23134431 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 3 May 2012 22:51:12 +0000
Subject: [PATCH] generate verification conditions for array access
---
src/main/scala/leon/Analysis.scala | 1 +
src/main/scala/leon/ArrayTransformation.scala | 4 +--
src/main/scala/leon/DefaultTactic.scala | 29 +++++++++++++++++++
src/main/scala/leon/Extensions.scala | 1 +
.../scala/leon/VerificationCondition.scala | 1 +
5 files changed, 34 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index 8c950fd87..176cb96b1 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
index 06c31189a..5ff33521d 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -35,7 +35,7 @@ object ArrayTransformation extends Pass {
IfExpr(
And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
ArraySelect(TupleSelect(ar, 1), ir).setType(sel.getType),
- Error("Array out of bound access").setType(sel.getType)
+ Error("Index out of bound").setType(sel.getType)
).setType(sel.getType)
}
case ArrayUpdate(a, i, v) => {
@@ -49,7 +49,7 @@ object ArrayTransformation extends Pass {
IfExpr(
And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
Block(Seq(Assignment(id, Tuple(Seq(ArrayUpdated(array, i, v).setType(array.getType), length)).setType(TupleType(Seq(array.getType, Int32Type))))), IntLiteral(0)),
- Error("Array out of bound access").setType(Int32Type)
+ Error("Index out of bound").setType(Int32Type)
).setType(Int32Type)
}
diff --git a/src/main/scala/leon/DefaultTactic.scala b/src/main/scala/leon/DefaultTactic.scala
index a01d02543..70ad17f36 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/Extensions.scala b/src/main/scala/leon/Extensions.scala
index 5905ec998..1ddb97e7c 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/VerificationCondition.scala b/src/main/scala/leon/VerificationCondition.scala
index 01545bc3e..e5556f1ac 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.")
--
GitLab