Merge branch 'hotfix-1.8.1'

smackers · Aug 27, 2017 · 5d79b66 · 5d79b66
2 parents 9739700 + 3d8c4d3
commit 5d79b66
Show file tree

Hide file tree

Showing 9 changed files with 60 additions and 19 deletions.
diff --git 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
@@ -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/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
@@ -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 pointer bit width.");
+  s << Decl::axiom(Expr::eq(Expr::id(Naming::MALLOC_TOP),pointerLit(malloc_top))) << "\n";
   s << "\n";
 
   if (SmackOptions::MemorySafety) {
@@ -994,8 +1001,23 @@ 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 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";
 
   if (SmackOptions::BitPrecise) {

diff --git 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/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/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')

diff --git 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
@@ -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):
         """