From e8e1b598eb7ee8641c279e197bb8a1d46a75e949 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 29 May 2015 18:31:05 +0200
Subject: [PATCH] Implement char comparison (<,<=,>,>=)
---
.../leon/evaluators/RecursiveEvaluator.scala | 4 ++++
.../leon/frontends/scalac/CodeExtraction.scala | 15 ++++++++++++++-
.../scala/leon/solvers/smtlib/SMTLIBSolver.scala | 7 +++++++
.../scala/leon/solvers/z3/AbstractZ3Solver.scala | 4 ++++
.../purescala/invalid/CharCompare.scala | 5 +++++
5 files changed, 34 insertions(+), 1 deletion(-)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/CharCompare.scala
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index d5bf1facf..86e6ef578 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -356,6 +356,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 < i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 < i2)
+ case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 < c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -363,6 +364,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 > i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 > i2)
+ case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 > c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -370,6 +372,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 <= i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 <= i2)
+ case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 <= c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -377,6 +380,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 >= i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 >= i2)
+ case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 >= c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index ce7661ceb..b37b6672f 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1715,7 +1715,20 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, mt1: MapType), "++", List(IsTyped(a2, mt2: MapType))) if mt1 == mt2 =>
MapUnion(a1, a2)
-
+
+ // Char operations
+ case (IsTyped(a1, CharType), ">", List(IsTyped(a2, CharType))) =>
+ GreaterThan(a1, a2)
+
+ case (IsTyped(a1, CharType), ">=", List(IsTyped(a2, CharType))) =>
+ GreaterEquals(a1, a2)
+
+ case (IsTyped(a1, CharType), "<", List(IsTyped(a2, CharType))) =>
+ LessThan(a1, a2)
+
+ case (IsTyped(a1, CharType), "<=", List(IsTyped(a2, CharType))) =>
+ LessEquals(a1, a2)
+
case (_, name, _) =>
outOfSubsetError(tr, "Unknown call to "+name)
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index c0dbf1e9a..3df3f89e5 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -651,18 +651,22 @@ abstract class SMTLIBSolver(val context: LeonContext,
case LessThan(a,b) => a.getType match {
case Int32Type => FixedSizeBitVectors.SLessThan(toSMT(a), toSMT(b))
case IntegerType => Ints.LessThan(toSMT(a), toSMT(b))
+ case CharType => FixedSizeBitVectors.SLessThan(toSMT(a), toSMT(b))
}
case LessEquals(a,b) => a.getType match {
case Int32Type => FixedSizeBitVectors.SLessEquals(toSMT(a), toSMT(b))
case IntegerType => Ints.LessEquals(toSMT(a), toSMT(b))
+ case CharType => FixedSizeBitVectors.SLessEquals(toSMT(a), toSMT(b))
}
case GreaterThan(a,b) => a.getType match {
case Int32Type => FixedSizeBitVectors.SGreaterThan(toSMT(a), toSMT(b))
case IntegerType => Ints.GreaterThan(toSMT(a), toSMT(b))
+ case CharType => FixedSizeBitVectors.SGreaterThan(toSMT(a), toSMT(b))
}
case GreaterEquals(a,b) => a.getType match {
case Int32Type => FixedSizeBitVectors.SGreaterEquals(toSMT(a), toSMT(b))
case IntegerType => Ints.GreaterEquals(toSMT(a), toSMT(b))
+ case CharType => FixedSizeBitVectors.SGreaterEquals(toSMT(a), toSMT(b))
}
case BVPlus(a,b) => FixedSizeBitVectors.Add(toSMT(a), toSMT(b))
case BVMinus(a,b) => FixedSizeBitVectors.Sub(toSMT(a), toSMT(b))
@@ -701,6 +705,9 @@ abstract class SMTLIBSolver(val context: LeonContext,
case (_, UnitType) =>
UnitLiteral()
+ case (FixedSizeBitVectors.BitVectorConstant(n, b), CharType) if b == BigInt(32) =>
+ CharLiteral(n.toInt.toChar)
+
case (SHexadecimal(h), CharType) =>
CharLiteral(h.toInt.toChar)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 4a5e6ed57..42d53fc24 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -596,18 +596,22 @@ trait AbstractZ3Solver
case LessThan(l, r) => l.getType match {
case IntegerType => z3.mkLT(rec(l), rec(r))
case Int32Type => z3.mkBVSlt(rec(l), rec(r))
+ case CharType => z3.mkBVSlt(rec(l), rec(r))
}
case LessEquals(l, r) => l.getType match {
case IntegerType => z3.mkLE(rec(l), rec(r))
case Int32Type => z3.mkBVSle(rec(l), rec(r))
+ case CharType => z3.mkBVSle(rec(l), rec(r))
}
case GreaterThan(l, r) => l.getType match {
case IntegerType => z3.mkGT(rec(l), rec(r))
case Int32Type => z3.mkBVSgt(rec(l), rec(r))
+ case CharType => z3.mkBVSgt(rec(l), rec(r))
}
case GreaterEquals(l, r) => l.getType match {
case IntegerType => z3.mkGE(rec(l), rec(r))
case Int32Type => z3.mkBVSge(rec(l), rec(r))
+ case CharType => z3.mkBVSge(rec(l), rec(r))
}
case c @ CaseClass(ct, args) =>
diff --git a/src/test/resources/regression/verification/purescala/invalid/CharCompare.scala b/src/test/resources/regression/verification/purescala/invalid/CharCompare.scala
new file mode 100644
index 000000000..8dade4ccc
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/CharCompare.scala
@@ -0,0 +1,5 @@
+import leon.lang._
+
+object foo {
+ def cmp(c1: Char, c2: Char): Boolean = { c1 < c2 }.holds
+}
--
GitLab