Add support for signed/unsigned conversions

Author: jad-hamza

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,

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 */
 

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}}"

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 =>

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)
     }
 

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))

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))

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),