From 14211eccb07d7d7146e64a96921147a2ec925ae9 Mon Sep 17 00:00:00 2001 From: Vytautas Astrauskas Date: Fri, 30 Jul 2021 12:54:15 +0200 Subject: [PATCH 1/3] Fix bvlshr name and add a test. --- .../ast/utility/BackendTypeFactories.scala | 6 ++-- .../silver/testing/BackendTypeTest.scala | 29 +++++++++++++++++++ 2 files changed, 33 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala b/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala index abc62eec0..88a771a14 100644 --- a/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala +++ b/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala @@ -15,8 +15,10 @@ case class BVFactory(size: Int) { def or(name: String) = BackendFunc(name, "bvor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) def add(name: String) = BackendFunc(name, "bvadd", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) def mul(name: String) = BackendFunc(name, "bvmul", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + def udiv(name: String) = BackendFunc(name, "bvudiv", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + def urem(name: String) = BackendFunc(name, "bvurem", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) def shl(name: String) = BackendFunc(name, "bvshl", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) - def shr(name: String) = BackendFunc(name, "bvshr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + def lshr(name: String) = BackendFunc(name, "bvlshr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) def not(name: String) = BackendFunc(name, "bvnot", typ, Seq(LocalVarDecl("x", typ)())) def neg(name: String) = BackendFunc(name, "bvneg", typ, Seq(LocalVarDecl("x", typ)())) @@ -71,4 +73,4 @@ case class FloatFactory(mant: Int, exp: Int, roundingMode: RoundingMode) { def from_bv(name: String) = BackendFunc(name, s"(_ to_fp ${exp} ${mant}) ", typ, Seq(LocalVarDecl("x", BVFactory(mant+exp).typ)())) def to_bv(name: String) = BackendFunc(name, s"(_ fp.to_sbv ${exp+mant}) ${roundingMode} ", BVFactory(mant+exp).typ, Seq(LocalVarDecl("x", typ)())) -} \ No newline at end of file +} diff --git a/src/main/scala/viper/silver/testing/BackendTypeTest.scala b/src/main/scala/viper/silver/testing/BackendTypeTest.scala index 361690f9f..62fae1b95 100644 --- a/src/main/scala/viper/silver/testing/BackendTypeTest.scala +++ b/src/main/scala/viper/silver/testing/BackendTypeTest.scala @@ -167,6 +167,29 @@ trait BackendTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfi (wrapInProgram(Seq(assign, assertion1), Seq(), Seq(result_decl)), assertion1) } + def generateBvOpTest2() : Program = { + val bv23 = BVFactory(23) + val from_int = bv23.from_int("toBV23") + val two_lit = IntLit(2)() + val one_lit = IntLit(1) () + val two = BackendFuncApp(from_int, Seq(two_lit))() + val one = BackendFuncApp(from_int, Seq(one_lit))() + val res_decl = LocalVarDecl("res", bv23.typ)() + val res = res_decl.localVar + wrapInProgram( + Seq( + LocalVarAssign(res, BackendFuncApp(bv23.xor("xorBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.and("andBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.or("orBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.add("addBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.mul("mulBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.udiv("udivBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.urem("uremBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.shl("shlBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.lshr("lshrBV23"), Seq(one, two))())(), + ), Seq(), Seq(res_decl)) + } + 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))() @@ -229,6 +252,12 @@ trait BackendTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfi }) } + test("bvOp2Success") { + val prog = generateBvOpTest2() + val res = verifier.verify(prog) + assert(res == Success) + } + test("floatOpSuccess") { val (prog, _) = generateFloatOpTest(true) val res = verifier.verify(prog) From 20f6d578ed065f1f06018f21017375d85d9354ba Mon Sep 17 00:00:00 2001 From: Vytautas Astrauskas Date: Fri, 30 Jul 2021 13:11:19 +0200 Subject: [PATCH 2/3] Add bvashr. --- .../scala/viper/silver/ast/utility/BackendTypeFactories.scala | 1 + src/main/scala/viper/silver/testing/BackendTypeTest.scala | 1 + 2 files changed, 2 insertions(+) diff --git a/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala b/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala index 88a771a14..086896273 100644 --- a/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala +++ b/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala @@ -19,6 +19,7 @@ case class BVFactory(size: Int) { def urem(name: String) = BackendFunc(name, "bvurem", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) def shl(name: String) = BackendFunc(name, "bvshl", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) def lshr(name: String) = BackendFunc(name, "bvlshr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + def ashr(name: String) = BackendFunc(name, "bvashr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) def not(name: String) = BackendFunc(name, "bvnot", typ, Seq(LocalVarDecl("x", typ)())) def neg(name: String) = BackendFunc(name, "bvneg", typ, Seq(LocalVarDecl("x", typ)())) diff --git a/src/main/scala/viper/silver/testing/BackendTypeTest.scala b/src/main/scala/viper/silver/testing/BackendTypeTest.scala index 62fae1b95..1c8732cc5 100644 --- a/src/main/scala/viper/silver/testing/BackendTypeTest.scala +++ b/src/main/scala/viper/silver/testing/BackendTypeTest.scala @@ -187,6 +187,7 @@ trait BackendTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfi LocalVarAssign(res, BackendFuncApp(bv23.urem("uremBV23"), Seq(one, two))())(), LocalVarAssign(res, BackendFuncApp(bv23.shl("shlBV23"), Seq(one, two))())(), LocalVarAssign(res, BackendFuncApp(bv23.lshr("lshrBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.ashr("ashrBV23"), Seq(one, two))())(), ), Seq(), Seq(res_decl)) } From 27b138210512a4ea3df790b602408b73c669c861 Mon Sep 17 00:00:00 2001 From: Vytautas Astrauskas Date: Fri, 30 Jul 2021 15:07:33 +0200 Subject: [PATCH 3/3] Add missing bitvector operations from Z3 documentation and their documentation. --- .../ast/utility/BackendTypeFactories.scala | 60 +++++++++++++++++++ .../silver/testing/BackendTypeTest.scala | 6 ++ 2 files changed, 66 insertions(+) diff --git a/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala b/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala index 086896273..14b9bc6a4 100644 --- a/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala +++ b/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala @@ -10,18 +10,78 @@ import viper.silver.ast.{Bool, Int, LocalVarDecl, BackendFunc, BackendType} case class BVFactory(size: Int) { lazy val typ = BackendType(s"bv${size}", s"(_ BitVec ${size})") + /** + * bit vector bitwise xor + */ def xor(name: String) = BackendFunc(name, "bvxor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector bitwise bvxnor + */ + def xnor(name: String) = BackendFunc(name, "bvxnor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector bitwise and + */ def and(name: String) = BackendFunc(name, "bvand", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector bitwise nand + */ + def nand(name: String) = BackendFunc(name, "bvnand", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector bitwise or + */ def or(name: String) = BackendFunc(name, "bvor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector bitwise nor + */ + def nor(name: String) = BackendFunc(name, "bvnor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector addition + */ def add(name: String) = BackendFunc(name, "bvadd", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector subtraction + */ + def sub(name: String) = BackendFunc(name, "bvsub", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector multiplication + */ def mul(name: String) = BackendFunc(name, "bvmul", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector signed modulo + */ + def smod(name: String) = BackendFunc(name, "bvsmod", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector unsigned division + */ def udiv(name: String) = BackendFunc(name, "bvudiv", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector unsigned remainder + */ def urem(name: String) = BackendFunc(name, "bvurem", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector signed remainder + */ + def srem(name: String) = BackendFunc(name, "bvsrem", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector shift left + */ def shl(name: String) = BackendFunc(name, "bvshl", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector unsigned (logical) shift right + */ def lshr(name: String) = BackendFunc(name, "bvlshr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector signed (arithmetical) shift right + */ def ashr(name: String) = BackendFunc(name, "bvashr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)())) + /** + * bit vector bitwise not + */ def not(name: String) = BackendFunc(name, "bvnot", typ, Seq(LocalVarDecl("x", typ)())) + /** + * bit vector unary minus + */ def neg(name: String) = BackendFunc(name, "bvneg", typ, Seq(LocalVarDecl("x", typ)())) def from_int(name: String) = BackendFunc(name, s"(_ int2bv ${size})", typ, Seq(LocalVarDecl("x", Int)())) diff --git a/src/main/scala/viper/silver/testing/BackendTypeTest.scala b/src/main/scala/viper/silver/testing/BackendTypeTest.scala index 1c8732cc5..3fe153f98 100644 --- a/src/main/scala/viper/silver/testing/BackendTypeTest.scala +++ b/src/main/scala/viper/silver/testing/BackendTypeTest.scala @@ -179,10 +179,16 @@ trait BackendTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfi wrapInProgram( Seq( LocalVarAssign(res, BackendFuncApp(bv23.xor("xorBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.xnor("xnorBV23"), Seq(one, two))())(), LocalVarAssign(res, BackendFuncApp(bv23.and("andBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.nand("nandBV23"), Seq(one, two))())(), LocalVarAssign(res, BackendFuncApp(bv23.or("orBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.nor("norBV23"), Seq(one, two))())(), LocalVarAssign(res, BackendFuncApp(bv23.add("addBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.sub("subBV23"), Seq(one, two))())(), LocalVarAssign(res, BackendFuncApp(bv23.mul("mulBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.smod("smodBV23"), Seq(one, two))())(), + LocalVarAssign(res, BackendFuncApp(bv23.srem("sremBV23"), Seq(one, two))())(), LocalVarAssign(res, BackendFuncApp(bv23.udiv("udivBV23"), Seq(one, two))())(), LocalVarAssign(res, BackendFuncApp(bv23.urem("uremBV23"), Seq(one, two))())(), LocalVarAssign(res, BackendFuncApp(bv23.shl("shlBV23"), Seq(one, two))())(),