From a3209bbae1617a1030c46394faed122d359d3eec Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 17 Dec 2015 11:26:34 +0100
Subject: [PATCH] InjectAssert should not insert trivial asserts
Improve equality to detect equalities between literals
---
.../scala/leon/purescala/Constructors.scala | 22 ++++++++++++++++++-
.../leon/verification/InjectAsserts.scala | 12 +++++-----
2 files changed, 27 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 4b960a043..6a4981997 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -280,7 +280,27 @@ object Constructors {
if (a == b && isDeterministic(a)) {
BooleanLiteral(true)
} else {
- Equals(a, b)
+ (a, b) match {
+ case (a: Literal[_], b: Literal[_]) =>
+ if (a.value == b.value) {
+ BooleanLiteral(true)
+ } else {
+ BooleanLiteral(false)
+ }
+
+ case _ =>
+ Equals(a, b)
+ }
+ }
+ }
+
+ def assertion(c: Expr, err: Option[String], res: Expr) = {
+ if (c == BooleanLiteral(true)) {
+ res
+ } else if (c == BooleanLiteral(false)) {
+ Error(res.getType, err.getOrElse("Assertion failed"))
+ } else {
+ Assert(c, err, res)
}
}
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index 418da12eb..a2ba463a6 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -42,34 +42,34 @@ object InjectAsserts extends SimpleLeonPhase[Program, Program] {
).setPos(e))
case e @ Division(_, d) =>
- Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+ Some(assertion(not(equality(d, InfiniteIntegerLiteral(0))),
Some("Division by zero"),
e
).setPos(e))
case e @ Remainder(_, d) =>
- Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+ Some(assertion(not(equality(d, InfiniteIntegerLiteral(0))),
Some("Remainder by zero"),
e
).setPos(e))
case e @ Modulo(_, d) =>
- Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+ Some(assertion(not(equality(d, InfiniteIntegerLiteral(0))),
Some("Modulo by zero"),
e
).setPos(e))
case e @ BVDivision(_, d) =>
- Some(Assert(Not(Equals(d, IntLiteral(0))),
+ Some(assertion(not(equality(d, IntLiteral(0))),
Some("Division by zero"),
e
).setPos(e))
case e @ BVRemainder(_, d) =>
- Some(Assert(Not(Equals(d, IntLiteral(0))),
+ Some(assertion(not(equality(d, IntLiteral(0))),
Some("Remainder by zero"),
e
).setPos(e))
case e @ RealDivision(_, d) =>
- Some(Assert(Not(Equals(d, FractionalLiteral(0, 1))),
+ Some(assertion(not(equality(d, FractionalLiteral(0, 1))),
Some("Division by zero"),
e
).setPos(e))
--
GitLab