From de24011eb3f431cf9810be883b6d6ab6a71ada72 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 3 Jun 2015 19:17:09 +0200
Subject: [PATCH] detect mod and rem by 0
---
.../scala/leon/purescala/PrettyPrinter.scala | 4 ++--
.../leon/verification/DefaultTactic.scala | 4 ++++
.../leon/verification/InjectAsserts.scala | 18 +++++++++++++++++-
.../verification/VerificationCondition.scala | 2 ++
...VDivision.scala => BVDivisionByZero.scala} | 2 +-
.../purescala/invalid/BVRemainderByZero.scala | 11 +++++++++++
.../{Division.scala => DivisionByZero.scala} | 4 ++--
.../purescala/invalid/ModuloByZero.scala | 11 +++++++++++
.../purescala/invalid/RemainderByZero.scala | 11 +++++++++++
...VDivision.scala => BVDivisionByZero.scala} | 6 +++++-
...ivision2.scala => BVDivisionByZero2.scala} | 2 +-
.../purescala/valid/Division.scala | 11 -----------
.../purescala/valid/DivisionByZero.scala | 19 +++++++++++++++++++
13 files changed, 86 insertions(+), 19 deletions(-)
rename src/test/resources/regression/verification/purescala/invalid/{BVDivision.scala => BVDivisionByZero.scala} (82%)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/BVRemainderByZero.scala
rename src/test/resources/regression/verification/purescala/invalid/{Division.scala => DivisionByZero.scala} (84%)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/ModuloByZero.scala
create mode 100644 src/test/resources/regression/verification/purescala/invalid/RemainderByZero.scala
rename src/test/resources/regression/verification/purescala/valid/{BVDivision.scala => BVDivisionByZero.scala} (57%)
rename src/test/resources/regression/verification/purescala/valid/{BVDivision2.scala => BVDivisionByZero2.scala} (83%)
delete mode 100644 src/test/resources/regression/verification/purescala/valid/Division.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/DivisionByZero.scala
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 7b6ccdcd6..bbee52fbf 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -625,11 +625,11 @@ class PrettyPrinter(opts: PrinterOptions,
def precedence(ex: Expr): Int = ex match {
case (pa: PrettyPrintable) => pa.printPrecedence
case (_: ElementOfSet) => 0
- case (_: Or | BinaryMethodCall(_, "||", _)) => 1
+ case (_: Modulo) => 1
+ case (_: Or | BinaryMethodCall(_, "||", _)) => 2
case (_: And | BinaryMethodCall(_, "&&", _)) => 3
case (_: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan) => 4
case (_: Equals | _: Not) => 5
- case (_: Modulo) => 6
case (_: Plus | _: BVPlus | _: Minus | _: BVMinus | _: SetUnion| _: SetDifference | BinaryMethodCall(_, "+" | "-", _)) => 7
case (_: Times | _: BVTimes | _: Division | _: BVDivision | _: Remainder | _: BVRemainder | BinaryMethodCall(_, "*" | "/", _)) => 8
case _ => 9
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 2333c3191..43ef19dfd 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -60,6 +60,10 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
VCKinds.ArrayUsage
} else if (err.startsWith("Division ")) {
VCKinds.DivisionByZero
+ } else if (err.startsWith("Modulo ")) {
+ VCKinds.ModuloByZero
+ } else if (err.startsWith("Remainder ")) {
+ VCKinds.RemainderByZero
} else {
VCKinds.Assert
}
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index bacfbe140..fae6329c8 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -13,7 +13,7 @@ import xlang.Expressions._
object InjectAsserts extends LeonPhase[Program, Program] {
val name = "Asserts"
- val description = "Inject asserts for various corrected conditions (map accesses, array accesses, ..)"
+ val description = "Inject asserts for various correctness conditions (map accesses, array accesses, divisions by zero,..)"
def run(ctx: LeonContext)(pgm: Program): Program = {
def indexUpTo(i: Expr, e: Expr) = {
@@ -40,11 +40,27 @@ object InjectAsserts extends LeonPhase[Program, Program] {
Some("Division by zero"),
e
).setPos(e))
+ case e @ Remainder(_, d) =>
+ Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+ Some("Remainder by zero"),
+ e
+ ).setPos(e))
+ case e @ Modulo(_, d) =>
+ Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+ Some("Modulo by zero"),
+ e
+ ).setPos(e))
+
case e @ BVDivision(_, d) =>
Some(Assert(Not(Equals(d, IntLiteral(0))),
Some("Division by zero"),
e
).setPos(e))
+ case e @ BVRemainder(_, d) =>
+ Some(Assert(Not(Equals(d, IntLiteral(0))),
+ Some("Remainder by zero"),
+ e
+ ).setPos(e))
case _ =>
None
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 890a16d06..2063902c2 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -35,6 +35,8 @@ object VCKinds {
case object MapUsage extends VCKind("map usage", "map use")
case object ArrayUsage extends VCKind("array usage", "arr. use")
case object DivisionByZero extends VCKind("division by zero", "div 0")
+ case object ModuloByZero extends VCKind("modulo by zero", "mod 0")
+ case object RemainderByZero extends VCKind("remainder by zero", "rem 0")
}
case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option[Long]) {
diff --git a/src/test/resources/regression/verification/purescala/invalid/BVDivision.scala b/src/test/resources/regression/verification/purescala/invalid/BVDivisionByZero.scala
similarity index 82%
rename from src/test/resources/regression/verification/purescala/invalid/BVDivision.scala
rename to src/test/resources/regression/verification/purescala/invalid/BVDivisionByZero.scala
index a2572db84..54ac21fb6 100644
--- a/src/test/resources/regression/verification/purescala/invalid/BVDivision.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/BVDivisionByZero.scala
@@ -2,7 +2,7 @@ import leon.lang._
import leon.collection._
import leon._
-object BVDivision {
+object BVDivisionByZero {
def divByZero(x: Int): Boolean = {
(x / 0 == 10)
diff --git a/src/test/resources/regression/verification/purescala/invalid/BVRemainderByZero.scala b/src/test/resources/regression/verification/purescala/invalid/BVRemainderByZero.scala
new file mode 100644
index 000000000..ed3ebf22a
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/BVRemainderByZero.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object BVRemainderByZero {
+
+ def remByZero(x: Int): Boolean = {
+ (x % 0 == 10)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/Division.scala b/src/test/resources/regression/verification/purescala/invalid/DivisionByZero.scala
similarity index 84%
rename from src/test/resources/regression/verification/purescala/invalid/Division.scala
rename to src/test/resources/regression/verification/purescala/invalid/DivisionByZero.scala
index 6b505a773..7415f2e6a 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Division.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/DivisionByZero.scala
@@ -2,10 +2,10 @@ import leon.lang._
import leon.collection._
import leon._
-object Division {
+object DivisionByZero {
def divByZero(x: BigInt): Boolean = {
(x / BigInt(0) == BigInt(10))
}
-
+
}
diff --git a/src/test/resources/regression/verification/purescala/invalid/ModuloByZero.scala b/src/test/resources/regression/verification/purescala/invalid/ModuloByZero.scala
new file mode 100644
index 000000000..19eb0da32
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/ModuloByZero.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object ModuloByZero {
+
+ def modByZero(x: BigInt): Boolean = {
+ (x mod BigInt(0)) == BigInt(10)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/RemainderByZero.scala b/src/test/resources/regression/verification/purescala/invalid/RemainderByZero.scala
new file mode 100644
index 000000000..5fc587fe8
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/RemainderByZero.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object RemainderByZero {
+
+ def remByZero(x: BigInt): Boolean = {
+ (x % BigInt(0) == BigInt(10))
+ }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/BVDivision.scala b/src/test/resources/regression/verification/purescala/valid/BVDivisionByZero.scala
similarity index 57%
rename from src/test/resources/regression/verification/purescala/valid/BVDivision.scala
rename to src/test/resources/regression/verification/purescala/valid/BVDivisionByZero.scala
index 2121f416e..3de75f003 100644
--- a/src/test/resources/regression/verification/purescala/valid/BVDivision.scala
+++ b/src/test/resources/regression/verification/purescala/valid/BVDivisionByZero.scala
@@ -2,10 +2,14 @@ import leon.lang._
import leon.collection._
import leon._
-object BVDivision {
+object BVDivisionByZero {
def noDivByZero(x: Int): Boolean = {
(x / 10 == 10)
}
+
+ def noRemByZero(x: BigInt): Boolean = {
+ (x % 10 == 10)
+ }
}
diff --git a/src/test/resources/regression/verification/purescala/valid/BVDivision2.scala b/src/test/resources/regression/verification/purescala/valid/BVDivisionByZero2.scala
similarity index 83%
rename from src/test/resources/regression/verification/purescala/valid/BVDivision2.scala
rename to src/test/resources/regression/verification/purescala/valid/BVDivisionByZero2.scala
index 77d677753..382dbb191 100644
--- a/src/test/resources/regression/verification/purescala/valid/BVDivision2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/BVDivisionByZero2.scala
@@ -2,7 +2,7 @@ import leon.lang._
import leon.collection._
import leon._
-object BVDivision2 {
+object BVDivisionByZero2 {
def division(x: Int, y: Int): Int = {
require(y != 0)
diff --git a/src/test/resources/regression/verification/purescala/valid/Division.scala b/src/test/resources/regression/verification/purescala/valid/Division.scala
deleted file mode 100644
index 49337b86d..000000000
--- a/src/test/resources/regression/verification/purescala/valid/Division.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-import leon.lang._
-import leon.collection._
-import leon._
-
-object Division {
-
- def noDivByZero(x: BigInt): Boolean = {
- (x / BigInt(10) == BigInt(10))
- }
-
-}
diff --git a/src/test/resources/regression/verification/purescala/valid/DivisionByZero.scala b/src/test/resources/regression/verification/purescala/valid/DivisionByZero.scala
new file mode 100644
index 000000000..559e13591
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/DivisionByZero.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object DivisionByZero {
+
+ def noDivByZero(x: BigInt): Boolean = {
+ (x / BigInt(10) == BigInt(10))
+ }
+
+ def noRemByZero(x: BigInt): Boolean = {
+ (x % BigInt(10) == BigInt(10))
+ }
+
+ def noModByZero(x: BigInt): Boolean = {
+ (x mod BigInt(10)) == BigInt(10)
+ }
+
+}
--
GitLab