Backend support for SMTLib types (particularly bitvectors and floats)

Author: marcoeilers

src/main/scala/viper/silver/ast/Expression.scala

@@ -387,6 +387,18 @@ object DomainFuncApp {
     DomainFuncApp(func.name,args,typVarMap)(pos, info, func.typ.substitute(typVarMap), func.domainName, errT)
 }
 
+// --- References to built-in SMT Lib functions
+
+case class SMTFuncApp(smtfunc: SMTFunc, args: Seq[Exp])
+                     (val pos: Position, val info: Info, override val typ : Type, val errT: ErrorTrafo)
+  extends AbstractDomainFuncApp with PossibleTrigger {
+  override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure)
+  def getArgs = args
+  def withArgs(newArgs: Seq[Exp]) = SMTFuncApp(smtfunc, newArgs)(pos,info,typ, errT)
+  override def func = (p: Program) => smtfunc
+  def funcname = smtfunc.name
+}
+
 // --- Field and predicate accesses
 
 /** A common trait for expressions accessing a location. */

src/main/scala/viper/silver/ast/Program.scala

@@ -705,3 +705,7 @@ case object NotOp extends UnOp with BoolDomainFunc {
   lazy val priority = 10
   lazy val fixity = Prefix
 }
+
+
+case class SMTFunc(name: String, smtName: String, override val typ: Type, override val formalArgs: Seq[LocalVarDecl]) extends Node with AbstractDomainFunc with BuiltinDomainFunc
+

src/main/scala/viper/silver/ast/Type.scala

@@ -183,3 +183,5 @@ case class TypeVar(name: String) extends Type {
 
   //def !=(other: TypeVar) = name != other
 }
+
+case class SMTType(boogieName: String, smtName: String) extends AtomicType

src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala

@@ -618,6 +618,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
       case dt@DomainType(domainName, typVarsMap) =>
         val typArgs = dt.typeParameters map (t => show(typVarsMap.getOrElse(t, t)))
         text(domainName) <> (if (typArgs.isEmpty) nil else brackets(ssep(typArgs, char (',') <> space)))
+      case SMTType(boogieName, _) => boogieName
     }
   }
 
@@ -766,6 +767,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
       text(funcname) <> parens(ssep(args map show, char (',') <> space))
     case DomainFuncApp(funcname, args, _) =>
       text(funcname) <> parens(ssep(args map show, char (',') <> space))
+    case SMTFuncApp(func, args) =>
+      text(func.name) <> parens(ssep(args map show, char(',') <> space))
 
     case EmptySeq(elemTyp) =>
       text("Seq[") <> showType(elemTyp) <> "]()"

src/main/scala/viper/silver/ast/utility/Expressions.scala

@@ -32,6 +32,7 @@ object Expressions {
          | _: PermExp
          | _: FuncApp
          | _: DomainFuncApp
+         | _: SMTFuncApp
          | _: LocationAccess
          | _: AbstractLocalVar
          | _: SeqExp

src/main/scala/viper/silver/ast/utility/Nodes.scala

@@ -106,6 +106,7 @@ object Nodes {
           case FuncApp(_, args) => args
           case DomainFuncApp(_, args, m) =>
             args ++ m.keys ++ m.values
+          case SMTFuncApp(_, args) => args
 
           case EmptySeq(elemTyp) => Seq(elemTyp)
           case ExplicitSeq(elems) => elems

src/main/scala/viper/silver/ast/utility/SMTTypeFactories.scala

@@ -0,0 +1,73 @@
+package viper.silver.ast.utility
+
+import viper.silver.ast.{Bool, Int, LocalVarDecl, SMTFunc, SMTType}
+
+/**
+  * A factory for fixed-size bitvectors that offers convenient access to bitvector types, as well as
+  * function definitions for unary and binary functions on bitvectors, as well as conversions from and
+  * to integers.
+  */
+case class BVFactory(size: Int) {
+  lazy val typ = SMTType(s"bv${size}", s"(_ BitVec ${size})")
+
+  def xor(name: String) = SMTFunc(name, "bvxor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def and(name: String) = SMTFunc(name, "bvand", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def or(name: String) = SMTFunc(name, "bvor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def add(name: String) = SMTFunc(name, "bvadd", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def mul(name: String) = SMTFunc(name, "bvmul", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def shl(name: String) = SMTFunc(name, "bvshl", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def shr(name: String) = SMTFunc(name, "bvshr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+
+  def not(name: String) = SMTFunc(name, "bvnot", typ, Seq(LocalVarDecl("x", typ)()))
+  def neg(name: String) = SMTFunc(name, "bvneg", typ, Seq(LocalVarDecl("x", typ)()))
+
+  def from_int(name: String) = SMTFunc(name, s"(_ int2bv ${size})", typ, Seq(LocalVarDecl("x", Int)()))
+  def to_int(name: String) = SMTFunc(name, s"(_ bv2int ${size})", Int, Seq(LocalVarDecl("x", typ)()))
+  def from_nat(name: String) = SMTFunc(name, s"(_ nat2bv ${size})", typ, Seq(LocalVarDecl("x", Int)()))
+  def to_nat(name: String) = SMTFunc(name, s"(_ bv2nat ${size})", Int, Seq(LocalVarDecl("x", typ)()))
+}
+
+/**
+  * Rounding modes for floating point operations.
+  */
+object RoundingMode extends Enumeration {
+  type RoundingMode = Value
+  val RNE, RNA, RTP, RTN, RTZ = Value
+}
+import RoundingMode._
+
+/**
+  * A factory for IEEE floating point numbers with "exp" bits for the exponent, "mant" bits for the significant,
+  * including the hidden bit, and a given rounding mode for all operations that use one.
+  * Offers access to types, unary and binary operations, comparisons, and conversions from and to
+  * bitvectors of size exp + mant.
+  */
+case class FloatFactory(mant: Int, exp: Int, roundingMode: RoundingMode) {
+
+  lazy val typ = SMTType(s"float${mant}e${exp}", s"(_ FloatingPoint ${exp} ${mant})")
+
+  def neg(name: String) = SMTFunc(name, "fp.neg", typ, Seq(LocalVarDecl("x", typ)()))
+  def abs(name: String) = SMTFunc(name, "fp.abs", typ, Seq(LocalVarDecl("x", typ)()))
+
+  def add(name: String) = SMTFunc(name, s"fp.add ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def sub(name: String) = SMTFunc(name, s"fp.sub ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def mul(name: String) = SMTFunc(name, s"fp.mul ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def div(name: String) = SMTFunc(name, s"fp.div ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def min(name: String) = SMTFunc(name, s"fp.min ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def max(name: String) = SMTFunc(name, s"fp.max ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+
+  def eq(name: String) = SMTFunc(name, s"fp.eq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def leq(name: String) = SMTFunc(name, s"fp.leq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def geq(name: String) = SMTFunc(name, s"fp.geq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def lt(name: String) = SMTFunc(name, s"fp.lt", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def gt(name: String) = SMTFunc(name, s"fp.gt", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+
+  def isZero(name: String) = SMTFunc(name, s"fp.isZero", Bool, Seq(LocalVarDecl("x", typ)()))
+  def isInfinite(name: String) = SMTFunc(name, s"fp.isInfinite", Bool, Seq(LocalVarDecl("x", typ)()))
+  def isNaN(name: String) = SMTFunc(name, s"fp.isNaN", Bool, Seq(LocalVarDecl("x", typ)()))
+  def isNegative(name: String) = SMTFunc(name, s"fp.isNegative", Bool, Seq(LocalVarDecl("x", typ)()))
+  def isPositive(name: String) = SMTFunc(name, s"fp.isPositive", Bool, Seq(LocalVarDecl("x", typ)()))
+
+  def from_bv(name: String) = SMTFunc(name, s"(_ to_fp ${exp} ${mant}) ", typ, Seq(LocalVarDecl("x", BVFactory(mant+exp).typ)()))
+  def to_bv(name: String) = SMTFunc(name, s"(_ fp.to_sbv ${exp+mant}) ${roundingMode} ", BVFactory(mant+exp).typ, Seq(LocalVarDecl("x", typ)()))
+}

src/main/scala/viper/silver/ast/utility/Types.scala

@@ -69,7 +69,7 @@ object Types {
     * @return The list of transitive type constituents of `typ`.
     */
   def typeConstituents(typ: Type): List[Type] = typ match {
-    case Int | Bool | Perm | Ref | InternalType | _: TypeVar | Wand => Nil
+    case Int | Bool | Perm | Ref | InternalType | _: TypeVar | Wand | _: SMTType => Nil
     case dt: DomainType => dt.typeParameters.map(_.substitute(dt.typVarsMap)).toList
     case SeqType(elementType) => elementType :: typeConstituents(elementType)
     case SetType(elementType) => elementType :: typeConstituents(elementType)