From f28331b97a414128348f9fde0a64e1ad1a01bd37 Mon Sep 17 00:00:00 2001 From: Jad Hamza Date: Tue, 30 Mar 2021 14:24:37 +0200 Subject: [PATCH] Add support for signed/unsigned conversions --- src/main/scala/inox/ast/Deconstructors.scala | 10 ++++++++++ src/main/scala/inox/ast/Expressions.scala | 20 +++++++++++++++++-- src/main/scala/inox/ast/Printers.scala | 2 ++ .../inox/evaluators/RecursiveEvaluator.scala | 12 +++++++++++ .../princess/AbstractPrincessSolver.scala | 6 ++++++ .../inox/solvers/smtlib/SMTLIBTarget.scala | 3 +++ src/main/scala/inox/solvers/z3/Z3Native.scala | 3 +++ src/main/scala/inox/utils/Serialization.scala | 6 ++++-- 8 files changed, 58 insertions(+), 4 deletions(-) diff --git a/src/main/scala/inox/ast/Deconstructors.scala b/src/main/scala/inox/ast/Deconstructors.scala index bec23e207..76ce15d2d 100644 --- a/src/main/scala/inox/ast/Deconstructors.scala +++ b/src/main/scala/inox/ast/Deconstructors.scala @@ -287,6 +287,16 @@ trait TreeDeconstructor { (NoIdentifiers, NoVariables, Seq(e), Seq(bvt), NoFlags, (_, _, es, tps, _) => t.BVWideningCast(es(0), tps(0).asInstanceOf[t.BVType])) }, + classOf[s.BVUnsignedToSigned] -> { expr => + val s.BVUnsignedToSigned(e) = expr + (NoIdentifiers, NoVariables, Seq(e), NoTypes, NoFlags, + (_, _, es, _, _) => t.BVUnsignedToSigned(es(0))) + }, + classOf[s.BVSignedToUnsigned] -> { expr => + val s.BVSignedToUnsigned(e) = expr + (NoIdentifiers, NoVariables, Seq(e), NoTypes, NoFlags, + (_, _, es, _, _) => t.BVSignedToUnsigned(es(0))) + }, classOf[s.Tuple] -> { expr => val s.Tuple(args) = expr (NoIdentifiers, NoVariables, args, NoTypes, NoFlags, diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala index 79d0322fd..47f867d62 100644 --- a/src/main/scala/inox/ast/Expressions.scala +++ b/src/main/scala/inox/ast/Expressions.scala @@ -532,7 +532,7 @@ trait Expressions { self: Trees => /** $encodingof `... .toByte` and other narrowing casts */ sealed case class BVNarrowingCast(expr: Expr, newType: BVType) extends Expr with CachingTyped { - // The expression is well types iff `expr` is well typed and the BVTypes' size match a narrowing cast. + // The expression is well typed iff `expr` is well typed and the BVTypes' size match a narrowing cast. override protected def computeType(implicit s: Symbols): Type = cast match { case Some((from, to)) => newType case _ => Untyped @@ -547,7 +547,7 @@ trait Expressions { self: Trees => /** $encodingof `... .toInt` and other widening casts */ sealed case class BVWideningCast(expr: Expr, newType: BVType) extends Expr with CachingTyped { - // The expression is well types iff `expr` is well typed and the BVTypes' size match a widening cast. + // The expression is well typed iff `expr` is well typed and the BVTypes' size match a widening cast. override protected def computeType(implicit s: Symbols): Type = cast match { case Some((from, to)) => newType case _ => Untyped @@ -560,6 +560,22 @@ trait Expressions { self: Trees => } } + /** Bitvector conversion from unsigned to signed */ + sealed case class BVUnsignedToSigned(expr: Expr) extends Expr with CachingTyped { + override protected def computeType(implicit s: Symbols): Type = getBVType(expr) match { + case BVType(false, size) => BVType(true, size) + case _ => Untyped + } + } + + /** Bitvector conversion from signed to unsigned */ + sealed case class BVSignedToUnsigned(expr: Expr) extends Expr with CachingTyped { + override protected def computeType(implicit s: Symbols): Type = getBVType(expr) match { + case BVType(true, size) => BVType(false, size) + case _ => Untyped + } + } + /* Tuple operations */ diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala index 10ffc22cf..834defbb2 100644 --- a/src/main/scala/inox/ast/Printers.scala +++ b/src/main/scala/inox/ast/Printers.scala @@ -260,6 +260,8 @@ trait Printer { case BVWideningCast(e, Int32Type()) => p"$e.toInt" case BVWideningCast(e, Int64Type()) => p"$e.toLong" case BVWideningCast(e, BVType(_, size)) => p"$e.toBV($size)" + case BVUnsignedToSigned(e) => p"$e.toSigned" + case BVSignedToUnsigned(e) => p"$e.toUnsigned" case fs @ FiniteSet(rs, _) => p"{${rs}}" case fs @ FiniteBag(rs, _) => p"{${rs.toSeq}}" diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala index 75d50b95d..6f8a7311f 100644 --- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala +++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala @@ -325,6 +325,18 @@ trait RecursiveEvaluator case x => throw EvalError(typeErrorMsg(x, BVType(bvt.signed, bvt.size - 1))) // or any smaller BVType } + case BVUnsignedToSigned(expr) => + e(expr) match { + case BVLiteral(false, bits, size) => BVLiteral(true, bits, size) + case x => throw EvalError("Expected unsigned bitvector type") + } + + case BVSignedToUnsigned(expr) => + e(expr) match { + case BVLiteral(true, bits, size) => BVLiteral(false, bits, size) + case x => throw EvalError("Expected signed bitvector type") + } + case LessThan(l,r) => (e(l), e(r)) match { case (b1 @ BVLiteral(sig1, _, s1), b2 @ BVLiteral(sig2, _, s2)) if sig1 == sig2 && s1 == s2 => diff --git a/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala b/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala index 49d133e27..7edc5afb0 100644 --- a/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala +++ b/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala @@ -364,6 +364,12 @@ trait AbstractPrincessSolver extends AbstractSolver with ADTManagers { val Some((from, to)) = c.cast Mod.extract(to - 1, 0, parseTerm(e)) + case BVUnsignedToSigned(e) => + parseTerm(e) + + case BVSignedToUnsigned(e) => + parseTerm(e) + case _ => unsupported(expr, "Unexpected formula " + expr) } diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala index 38f29db7a..dd09d1bd7 100644 --- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala +++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala @@ -446,6 +446,9 @@ trait SMTLIBTarget extends SMTLIBParser with Interruptible with ADTManagers { val Some((from, to)) = c.cast FixedSizeBitVectors.Extract(to - 1, 0, toSMT(e)) + case BVUnsignedToSigned(e) => toSMT(e) + case BVSignedToUnsigned(e) => toSMT(e) + case And(sub) => SmtLibConstructors.and(sub.map(toSMT)) case Or(sub) => SmtLibConstructors.or(sub.map(toSMT)) case IfExpr(cond, thenn, elze) => Core.ITE(toSMT(cond), toSMT(thenn), toSMT(elze)) diff --git a/src/main/scala/inox/solvers/z3/Z3Native.scala b/src/main/scala/inox/solvers/z3/Z3Native.scala index 0835ca6fb..8e0071790 100644 --- a/src/main/scala/inox/solvers/z3/Z3Native.scala +++ b/src/main/scala/inox/solvers/z3/Z3Native.scala @@ -327,6 +327,9 @@ trait Z3Native extends ADTManagers with Interruptible { self: AbstractSolver => val Some((from, to)) = c.cast z3.mkExtract(to - 1, 0, rec(e)) + case BVUnsignedToSigned(e) => rec(e) + case BVSignedToUnsigned(e) => rec(e) + case LessThan(l, r) => l.getType match { case IntegerType() => z3.mkLT(rec(l), rec(r)) case RealType() => z3.mkLT(rec(l), rec(r)) diff --git a/src/main/scala/inox/utils/Serialization.scala b/src/main/scala/inox/utils/Serialization.scala index 47b336685..718346116 100644 --- a/src/main/scala/inox/utils/Serialization.scala +++ b/src/main/scala/inox/utils/Serialization.scala @@ -523,10 +523,10 @@ class InoxSerializer(val trees: ast.Trees, serializeProducts: Boolean = false) e /** A mapping from `Class[_]` to `Serializer[_]` for classes that commonly * occur within Stainless programs. * - * The `Serializer[_]` identifiers in this mapping range from 10 to 102 + * The `Serializer[_]` identifiers in this mapping range from 10 to 105 * (ignoring special identifiers that are smaller than 10). * - * NEXT ID: 104 + * NEXT ID: 106 */ protected def classSerializers: Map[Class[_], Serializer[_]] = Map( // Inox Expressions @@ -598,6 +598,8 @@ class InoxSerializer(val trees: ast.Trees, serializeProducts: Boolean = false) e classSerializer[FiniteMap] (72), classSerializer[MapApply] (73), classSerializer[MapUpdated] (74), + classSerializer[BVUnsignedToSigned](104), + classSerializer[BVSignedToUnsigned](105), // Inox Types classSerializer[Untyped.type] (75),