Backend support for SMTLib types (particularly bitvectors and floats)

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

@@ -385,6 +385,17 @@ 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 = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos)
+  extends AbstractDomainFuncApp {
+  override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure)
+  override def func = (p: Program) => smtFunc
+  def funcname = smtFunc.name
+  override def typ = smtFunc.typ
+}
+
 // --- Field and predicate accesses
 
 /** A common trait for expressions accessing a location. */

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

@@ -733,9 +733,13 @@ case object NotOp extends UnOp with BoolDomainFunc {
   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
+
 /**
   * The Extension Member trait provides the way to expand the Ast to include new Top Level declarations
   */
 trait ExtensionMember extends Member{
   def extensionSubnodes: Seq[Node]
-}
+}

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

@@ -184,6 +184,8 @@ case class TypeVar(name: String) extends Type {
   //def !=(other: TypeVar) = name != other
 }
 
+case class SMTType(boogieName: String, smtName: String) extends AtomicType
+
 trait ExtensionType extends Type{
   def getAstType: Type = ???
 }

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

@@ -624,6 +624,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
     }
   }
 
@@ -770,11 +771,12 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
       text(funcname) <> parens(ssep(args map show, char (',') <> space))
     case dfa@DomainFuncApp(funcname, args, tvMap) =>
       if (tvMap.nonEmpty)
-        // Type may be underconstrained, so to be safe we explicitly print out the type.
+      // Type may be underconstrained, so to be safe we explicitly print out the type.
         parens(text(funcname) <> parens(ssep(args map show, char (',') <> space)) <> char(':') <+> show(dfa.typ))
       else
         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) <> "]()"
     case ExplicitSeq(elems) =>

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

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

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

@@ -105,6 +105,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)

src/main/scala/viper/silver/testing/SMTTypeTest.scala

@@ -0,0 +1,208 @@
+package viper.silver.testing
+
+import org.scalatest.{BeforeAndAfterAllConfigMap, ConfigMap, FunSuite, Matchers}
+import viper.silver.ast.{AnySetContains, Assert, EqCmp, Exp, Field, FieldAccess, FieldAccessPredicate, FullPerm, Function, Inhale, IntLit, LocalVarAssign, LocalVarDecl, Method, Program, Ref, Result, SMTFuncApp, Seqn, SetType, Stmt}
+import viper.silver.ast.utility.{BVFactory, FloatFactory, RoundingMode}
+import viper.silver.verifier.{Failure, Success, Verifier}
+import viper.silver.verifier.errors.{AssertFailed, PostconditionViolated}
+
+trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap {
+
+  def generateTypeCombinationTest(success: Boolean) : (Program, Assert) = {
+    val t = if (success) BVFactory(23).typ else FloatFactory(23, 11, RoundingMode.RNE).typ
+    val p1_decl = LocalVarDecl("three", t)()
+    val p1_ref = p1_decl.localVar
+    val p2_decl = LocalVarDecl("lol", SetType(t))()
+    val p2_ref= p2_decl.localVar
+    val element_in_param = AnySetContains(p1_ref, p2_ref)()
+
+    val assume = Inhale(element_in_param)()
+    val assert = Assert(element_in_param)()
+    val body = if (success) Seq(assume, assert) else Seq(assert)
+    (wrapInProgram(body, Seq(p1_decl, p2_decl), Seq()), assert)
+  }
+
+  def generateFieldTypeTest(success: Boolean) : (Program, Assert) = {
+    val t = if (!success) BVFactory(23).typ else FloatFactory(23, 11, RoundingMode.RNE).typ
+    val field = Field("f", t)()
+    val p1_decl = LocalVarDecl("three", Ref)()
+    val p1_ref = p1_decl.localVar
+    val p2_decl = LocalVarDecl("lol", SetType(t))()
+    val p2_ref= p2_decl.localVar
+    val fieldAcc = FieldAccess(p1_ref, field)()
+    val perm = FieldAccessPredicate(fieldAcc, FullPerm()())()
+    val element_in_param = AnySetContains(fieldAcc, p2_ref)()
+
+    val getPerm = Inhale(perm)()
+    val assume = Inhale(element_in_param)()
+    val assert = Assert(element_in_param)()
+    val body = if (success) Seq(getPerm, assume, assert) else Seq(getPerm, assert)
+    (wrapInProgram(body, Seq(p1_decl, p2_decl), Seq(), fields = Seq(field)), assert)
+  }
+
+  def generateFloatOpTest(success: Boolean) : (Program, Assert) = {
+    val rne = RoundingMode.RNE
+    val fp = FloatFactory(24, 8, rne)
+    val first = 1081081856 // 3.75
+    val second = 1103888384 // 25.5
+    val result = 1105854464 // 29.25
+    val bv32 = BVFactory(32)
+    val from_int = bv32.from_int("toBV32")
+    val to_fp = fp.from_bv("tofp")
+    val fp_eq = fp.eq("fp_eq")
+    val fp_add = fp.add("fp_add")
+
+    val first_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(first)()))()))()
+    val second_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(second)()))()))()
+    val result_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(result)()))()))()
+
+    val zero_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(0)()))()))()
+
+    val addition = SMTFuncApp(fp_add, Seq(first_float, second_float))()
+    val result_addition = SMTFuncApp(fp_add, Seq(result_float, if (success) zero_float else first_float))()
+
+    val equality = SMTFuncApp(fp_eq, Seq(addition, result_addition))()
+    val assert = Assert(equality)()
+    (wrapInProgram(Seq(assert), Seq(), Seq()), assert)
+  }
+
+  def generateFloatOpFunctionTest(success: Boolean) : (Program, Function, Exp) = {
+    val rne = RoundingMode.RNE
+    val fp = FloatFactory(24, 8, rne)
+    val first = 1081081856 // 3.75
+    val second = 1103888384 // 25.5
+    val result = 1105854464 // 29.25
+    val bv32 = BVFactory(32)
+    val from_int = bv32.from_int("toBV32")
+    val to_fp = fp.from_bv("tofp")
+    val fp_eq = fp.eq("fp_eq")
+    val fp_add = fp.add("fp_add")
+
+    val first_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(first)()))()))()
+    val second_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(second)()))()))()
+    val result_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(result)()))()))()
+
+    val zero_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(0)()))()))()
+
+    val addition = SMTFuncApp(fp_add, Seq(first_float, second_float))()
+    val result_addition = SMTFuncApp(fp_add, Seq(result_float, if (success) zero_float else first_float))()
+
+    val equality = SMTFuncApp(fp_eq, Seq(Result(fp.typ)(), result_addition))()
+
+    val fun = Function("test", Seq(), fp.typ, Seq(), Seq(equality), Some(addition))()
+    val program = Program(Seq(), Seq(), Seq(fun), Seq(), Seq(), Seq())()
+    (program, fun, equality)
+  }
+
+  def generateBvOpTest(success: Boolean) : (Program, Assert) = {
+    val bv23 = BVFactory(23)
+    val from_int = bv23.from_int("toBV23")
+    val two_lit = IntLit(2)()
+    val three_lit = IntLit(3)()
+    val one_lit = IntLit(1) ()
+    val two = SMTFuncApp(from_int, Seq(two_lit))()
+    val three = SMTFuncApp(from_int, Seq(three_lit))()
+    val one = SMTFuncApp(from_int, Seq(one_lit))()
+    val result_decl = LocalVarDecl("three", bv23.typ)()
+    val result_ref = result_decl.localVar
+    val assign = LocalVarAssign(result_ref, if (success) three else one)()
+    val xor = bv23.xor("xorBV23")
+    val xor_app = SMTFuncApp(xor, Seq(one, two))()
+    val equality1 = EqCmp(result_ref, xor_app)()
+    val assertion1 = Assert(equality1)()
+    (wrapInProgram(Seq(assign, assertion1), Seq(), Seq(result_decl)), assertion1)
+  }
+
+  def wrapInProgram(stmts: Seq[Stmt], params: Seq[LocalVarDecl], vars: Seq[LocalVarDecl], fields: Seq[Field] = Seq()): Program = {
+    val block = Seqn(stmts, vars)()
+    val method = Method("test", params, Seq(), Seq(), Seq(), Some(block))()
+    Program(Seq(), fields, Seq(), Seq(), Seq(method), Seq())()
+  }
+
+  val verifier : Verifier
+
+  override def beforeAll(configMap: ConfigMap) {
+    verifier.parseCommandLine(Seq("dummy.vpr"))
+    verifier.start()
+  }
+
+  override def afterAll(configMap: ConfigMap) {
+    verifier.stop()
+  }
+
+  test("typeCombinationSuccess") {
+    val (prog, assertNode) = generateTypeCombinationTest(true)
+    val res  = verifier.verify(prog)
+    assert(res == Success)
+  }
+
+  test("typeCombinationFail") {
+    val (prog, assertNode) = generateTypeCombinationTest(false)
+    val res  = verifier.verify(prog)
+    assert(res match {
+      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
+      case _ => false
+    })
+  }
+
+  test("fieldTypeSuccess") {
+    val (prog, assertNode) = generateFieldTypeTest(true)
+    val res  = verifier.verify(prog)
+    assert(res == Success)
+  }
+
+  test("fieldTypeFail") {
+    val (prog, assertNode) = generateFieldTypeTest(false)
+    val res  = verifier.verify(prog)
+    assert(res match {
+      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
+      case _ => false
+    })
+  }
+
+  test("bvOpSuccess") {
+    val (prog, assertNode) = generateBvOpTest(true)
+    val res  = verifier.verify(prog)
+    assert(res == Success)
+  }
+
+  test("bvOpFail") {
+    val (prog, assertNode) = generateBvOpTest(false)
+    val res  = verifier.verify(prog)
+    assert(res match {
+      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
+      case _ => false
+    })
+  }
+
+  test("floatOpSuccess") {
+    val (prog, assertNode) = generateFloatOpTest(true)
+    val res  = verifier.verify(prog)
+    assert(res == Success)
+  }
+
+  test("floatOpFail") {
+    val (prog, assertNode) = generateFloatOpTest(false)
+    val res  = verifier.verify(prog)
+    assert(res match {
+      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
+      case _ => false
+    })
+  }
+
+  test("floatOpFunctionSuccess") {
+    val (prog, fun, exp) = generateFloatOpFunctionTest(true)
+    val res  = verifier.verify(prog)
+    assert(res == Success)
+  }
+
+  test("floatOpFunctionFail") {
+    val (prog, fun, exp) = generateFloatOpFunctionTest(false)
+    val res  = verifier.verify(prog)
+    assert(res match {
+      case Failure(Seq(PostconditionViolated(e, f, _, _))) if e == exp && fun == f => true
+      case _ => false
+    })
+  }
+
+}