Skip to content

Fix bvlshr name and add a test. #537

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
vakaras merged 3 commits into from
Jul 30, 2021
Merged

Fix bvlshr name and add a test. #537

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
14211ec
Fix bvlshr name and add a test.
vakaras Jul 30, 2021
20f6d57
Add bvashr.
vakaras Jul 30, 2021
27b1382
Add missing bitvector operations from Z3 documentation and their docu…
vakaras Jul 30, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)()))
Comment thread
vakaras marked this conversation as resolved.

def not(name: String) = BackendFunc(name, "bvnot", typ, Seq(LocalVarDecl("x", typ)()))
def neg(name: String) = BackendFunc(name, "bvneg", typ, Seq(LocalVarDecl("x", typ)()))
Expand Down Expand Up @@ -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)()))
}
}
29 changes: 29 additions & 0 deletions src/main/scala/viper/silver/testing/BackendTypeTest.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))()
Expand Down Expand Up @@ -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)
Expand Down
⚡