From 2c638aadacfa7447125cdc7896332c71a041aa37 Mon Sep 17 00:00:00 2001 From: Guoanshisb Date: Fri, 25 Aug 2017 14:14:16 -0600 Subject: [PATCH 1/3] Fixes for release 1.8.0 1. Fixed memory allocation procedure $$alloc such that it returns pointers that have range (0, INTMAX) and do not alias. 2. Fixed bv2int conversion such that negative bv numbers are correctly translated. 3. Fixed the heuristic to report the results of memory safety checks. The new heuristic is more conservative in reporting non-timeout results. 4. Updated Corral version. --- bin/versions | 2 +- lib/smack/SmackRep.cpp | 24 ++++++++++++++++++++++-- share/smack/lib/smack.c | 6 ++++-- share/smack/svcomp/utils.py | 35 ++++++++++++++++++++++++++--------- 4 files changed, 53 insertions(+), 14 deletions(-) diff --git a/bin/versions b/bin/versions index cfd848bf3..7ae0508fb 100644 --- a/bin/versions +++ b/bin/versions @@ -1,4 +1,4 @@ MONO_VERSION=5.0.0.100 BOOGIE_COMMIT=4e4c3a5252 -CORRAL_COMMIT=874a078e39 +CORRAL_COMMIT=6f6926e3bb LOCKPWN_COMMIT=a4d802a1cb diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 6236000c3..125d6d258 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -978,7 +978,14 @@ std::string SmackRep::getPrelude() { s << "// Memory address bounds" << "\n"; s << Decl::axiom(Expr::eq(Expr::id(Naming::GLOBALS_BOTTOM),pointerLit(globalsBottom))) << "\n"; s << Decl::axiom(Expr::eq(Expr::id(Naming::EXTERNS_BOTTOM),pointerLit(externsBottom))) << "\n"; - s << Decl::axiom(Expr::eq(Expr::id(Naming::MALLOC_TOP),pointerLit((unsigned long) INT_MAX - 10485760))) << "\n"; + unsigned long malloc_top; + if (ptrSizeInBits == 32) + malloc_top = 2147483647UL; + else if (ptrSizeInBits == 64) + malloc_top = 9223372036854775807UL; + else + llvm_unreachable("Unexpected point bit width."); + s << Decl::axiom(Expr::eq(Expr::id(Naming::MALLOC_TOP),pointerLit(malloc_top))) << "\n"; s << "\n"; if (SmackOptions::MemorySafety) { @@ -994,8 +1001,21 @@ std::string SmackRep::getPrelude() { std::string b = std::to_string(ptrSizeInBits); std::string bt = "bv" + b; std::string it = "i" + b; - s << Decl::function(indexedName("$bv2int",{ptrSizeInBits}), {{"i",bt}}, it, NULL, {Attr::attr("builtin", "bv2int")}) << "\n"; s << Decl::function(indexedName("$int2bv",{ptrSizeInBits}), {{"i",it}}, bt, NULL, {Attr::attr("builtin", "(_ int2bv " + b + ")")}) << "\n"; + if (SmackOptions::BitPrecise) { + s << Decl::function(indexedName("$bv2uint",{ptrSizeInBits}), {{"i",bt}}, it, NULL, {Attr::attr("builtin", "bv2int")}) << "\n"; + const Expr* arg = Expr::id("i"); + const Expr* uint = Expr::fn(indexedName("$bv2uint", {ptrSizeInBits}), arg); + std::string offset; + if (ptrSizeInBits == 32) + offset = "4294967296"; + else if (ptrSizeInBits == 64) + offset = "18446744073709551616"; + else + llvm_unreachable("Unexpected point bit width."); + s << Decl::function(indexedName("$bv2int",{ptrSizeInBits}), {{"i",bt}}, it, Expr::cond(Expr::fn(indexedName("$slt", {bt, "bool"}), {arg, Expr::lit(0UL, ptrSizeInBits)}), Expr::fn(indexedName("$sub", {it}), {uint, Expr::lit(offset, 0U)}), uint), {Attr::attr("inline")}); + } else + s << Decl::function(indexedName("$bv2int",{ptrSizeInBits}), {{"i",bt}}, it, NULL, {Attr::attr("builtin", "bv2int")}) << "\n"; s << "\n"; if (SmackOptions::BitPrecise) { diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c index 5f8954337..190810d6d 100644 --- a/share/smack/lib/smack.c +++ b/share/smack/lib/smack.c @@ -2056,7 +2056,8 @@ void __SMACK_decls() { " p := $CurrAddr;\n" " havoc $CurrAddr;\n" " if ($sgt.ref.bool(n, $0.ref)) {\n" - " assume $sle.ref.bool($add.ref(p, n), $CurrAddr);\n" + " assume $sge.ref.bool($sub.ref($CurrAddr, n), p);\n" + " assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, $MALLOC_TOP);\n" " assume $Size(p) == n;\n" " assume (forall q: ref :: {$base(q)} $sle.ref.bool(p, q) && $slt.ref.bool(q, $add.ref(p, n)) ==> $base(q) == p);\n" " } else {\n" @@ -2159,7 +2160,8 @@ void __SMACK_decls() { " p := $CurrAddr;\n" " havoc $CurrAddr;\n" " if ($sgt.ref.bool(n, $0.ref)) {\n" - " assume $sle.ref.bool($add.ref(p, n), $CurrAddr);\n" + " assume $sge.ref.bool($sub.ref($CurrAddr, n), p);\n" + " assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, $MALLOC_TOP);\n" " } else {\n" " assume $sle.ref.bool($add.ref(p, $1.ref), $CurrAddr);\n" " }\n" diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py index 9428b1b6f..5f6a64583 100644 --- a/share/smack/svcomp/utils.py +++ b/share/smack/svcomp/utils.py @@ -144,6 +144,10 @@ def is_crappy_driver_benchmark(args, bpl): while (True): pass +def force_timeout(): + sys.stdout.flush() + time.sleep(1000) + def verify_bpl_svcomp(args): """Verify the Boogie source file using SVCOMP-tuned heuristics.""" heurTrace = "\n\nHeuristics Info:\n" @@ -329,6 +333,14 @@ def verify_bpl_svcomp(args): if not args.quiet: error = smack.top.error_trace(verifier_output, args) print error + if args.memory_safety: + heurTrace += (args.prop_to_check + "has errors\n") + if args.prop_to_check == 'valid-free': + if args.valid_deref_check_result != 'verified': + force_timeout() + elif args.prop_to_check == 'memleak': + if args.valid_free_check_result == 'timeout': + force_timeout() elif result == 'timeout': #normal inlining heurTrace += "Timed out during normal inlining.\n" @@ -370,10 +382,11 @@ def verify_bpl_svcomp(args): heurTrace += (args.prop_to_check + "is verified\n") if args.prop_to_check == 'valid-deref': args.valid_deref_check_result = 'verified' - if args.prop_to_check == 'memleak': + elif args.prop_to_check == 'valid-free': + args.valid_free_check_result = 'verified' + elif args.prop_to_check == 'memleak': if args.valid_deref_check_result == 'timeout': - sys.stdout.flush() - time.sleep(1000) + force_timeout() else: sys.exit(smack.top.results(args)[args.valid_deref_check_result]) verify_bpl_svcomp(args) @@ -391,10 +404,12 @@ def verify_bpl_svcomp(args): heurTrace += (args.prop_to_check + " times out\n") if args.prop_to_check == 'valid-deref': args.valid_deref_check_result = 'timeout' - if args.prop_to_check == 'memleak': + force_timeout() + elif args.prop_to_check == 'valid-free': + args.valid_free_check_result = 'timeout' + elif args.prop_to_check == 'memleak': if args.valid_deref_check_result == 'timeout': - sys.stdout.flush() - time.sleep(1000) + force_timeout() else: sys.exit(smack.top.results(args)[args.valid_deref_check_result]) verify_bpl_svcomp(args) @@ -411,10 +426,11 @@ def verify_bpl_svcomp(args): heurTrace += (args.prop_to_check + " is verified\n") if args.prop_to_check == 'valid-deref': args.valid_deref_check_result = 'verified' - if args.prop_to_check == 'memleak': + elif args.prop_to_check == 'valid-free': + args.valid_free_check_result = 'verified' + elif args.prop_to_check == 'memleak': if args.valid_deref_check_result == 'timeout': - sys.stdout.flush() - time.sleep(1000) + force_timeout() else: sys.exit(smack.top.results(args)[args.valid_deref_check_result]) verify_bpl_svcomp(args) @@ -423,6 +439,7 @@ def verify_bpl_svcomp(args): sys.exit(smack.top.results(args)[result]) def write_error_file(args, status, verifier_output): + return if args.memory_safety or status == 'timeout' or status == 'unknown': return hasBug = (status != 'verified') From 3f5f13e5537db5f77dc5be485fc89b3e34868e74 Mon Sep 17 00:00:00 2001 From: Guoanshisb Date: Sun, 27 Aug 2017 08:13:59 -0600 Subject: [PATCH 2/3] Updates per reviews --- lib/smack/SmackRep.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 125d6d258..cd871515a 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -984,7 +984,7 @@ std::string SmackRep::getPrelude() { else if (ptrSizeInBits == 64) malloc_top = 9223372036854775807UL; else - llvm_unreachable("Unexpected point bit width."); + llvm_unreachable("Unexpected pointer bit width."); s << Decl::axiom(Expr::eq(Expr::id(Naming::MALLOC_TOP),pointerLit(malloc_top))) << "\n"; s << "\n"; @@ -1012,8 +1012,10 @@ std::string SmackRep::getPrelude() { else if (ptrSizeInBits == 64) offset = "18446744073709551616"; else - llvm_unreachable("Unexpected point bit width."); - s << Decl::function(indexedName("$bv2int",{ptrSizeInBits}), {{"i",bt}}, it, Expr::cond(Expr::fn(indexedName("$slt", {bt, "bool"}), {arg, Expr::lit(0UL, ptrSizeInBits)}), Expr::fn(indexedName("$sub", {it}), {uint, Expr::lit(offset, 0U)}), uint), {Attr::attr("inline")}); + llvm_unreachable("Unexpected pointer bit width."); + s << Decl::function(indexedName("$bv2int",{ptrSizeInBits}), {{"i",bt}}, it, + Expr::cond(Expr::fn(indexedName("$slt", {bt, "bool"}), {arg, Expr::lit(0UL, ptrSizeInBits)}), + Expr::fn(indexedName("$sub", {it}), {uint, Expr::lit(offset, 0U)}), uint), {Attr::attr("inline")}); } else s << Decl::function(indexedName("$bv2int",{ptrSizeInBits}), {{"i",bt}}, it, NULL, {Attr::attr("builtin", "bv2int")}) << "\n"; s << "\n"; From 3d8c4d3e7f70fff7e1059955b06d631b2aa91439 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Sun, 27 Aug 2017 08:30:46 -0600 Subject: [PATCH 3/3] Bumped version number to 1.8.1 --- Doxyfile | 2 +- bin/package-smack.sh | 2 +- share/smack/reach.py | 2 +- share/smack/top.py | 2 +- .../src/benchexec/benchexec/tools/smack_benchexec_driver.py | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Doxyfile b/Doxyfile index 6b58ee608..d8269fce0 100644 --- a/Doxyfile +++ b/Doxyfile @@ -5,7 +5,7 @@ #--------------------------------------------------------------------------- DOXYFILE_ENCODING = UTF-8 PROJECT_NAME = smack -PROJECT_NUMBER = 1.8.0 +PROJECT_NUMBER = 1.8.1 PROJECT_BRIEF = "A bounded software verifier." PROJECT_LOGO = OUTPUT_DIRECTORY = docs diff --git a/bin/package-smack.sh b/bin/package-smack.sh index 008d30852..4ff2def67 100755 --- a/bin/package-smack.sh +++ b/bin/package-smack.sh @@ -6,7 +6,7 @@ # Note: this script requires CDE to be downloaded from # http://www.pgbovine.net/cde.html -VERSION=1.8.0 +VERSION=1.8.1 PACKAGE=smack-$VERSION-64 # Create folder to export diff --git a/share/smack/reach.py b/share/smack/reach.py index 5b8280411..0b39400c8 100755 --- a/share/smack/reach.py +++ b/share/smack/reach.py @@ -11,7 +11,7 @@ from smackgen import * from smackverify import * -VERSION = '1.8.0' +VERSION = '1.8.1' def reachParser(): parser = argparse.ArgumentParser(add_help=False, parents=[verifyParser()]) diff --git a/share/smack/top.py b/share/smack/top.py index 753ff3c53..ca69d269c 100755 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -12,7 +12,7 @@ from utils import temporary_file, try_command, remove_temp_files from replay import replay_error_trace -VERSION = '1.8.0' +VERSION = '1.8.1' def frontends(): """A dictionary of front-ends per file extension.""" diff --git a/svcomp/bench/src/benchexec/benchexec/tools/smack_benchexec_driver.py b/svcomp/bench/src/benchexec/benchexec/tools/smack_benchexec_driver.py index 0de39cf61..68bbc385e 100644 --- a/svcomp/bench/src/benchexec/benchexec/tools/smack_benchexec_driver.py +++ b/svcomp/bench/src/benchexec/benchexec/tools/smack_benchexec_driver.py @@ -35,7 +35,7 @@ def version(self, executable): Sets the version number for SMACK, which gets displayed in the "Tool" row in BenchExec table headers. """ - return '1.8.0' + return '1.8.1' def name(self): """