From 0f28af85038477f4d1d49f4bcb56c1cb02f54e3f Mon Sep 17 00:00:00 2001
From: Shaobo <polarishehn@gmail.com>
Date: Mon, 16 Jul 2018 09:30:55 -0600
Subject: [PATCH 01/60] Attempt to validate input/output file arguments

Previously SMACK exits with an argument parsing error when the input
file is not valid. This commit rewrites the logic and puts it as an
action class. Moreover, the action class added also handles the validation
of output files.
---
 share/smack/top.py | 55 +++++++++++++++++++++++++++++++++-------------
 1 file changed, 40 insertions(+), 15 deletions(-)

diff --git a/share/smack/top.py b/share/smack/top.py
index 7ec999804..a181f9d15 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -65,27 +65,52 @@ def inlined_procedures():
     '__SMACK_check_overflow'
   ]
 
-def validate_input_file(file):
-  """Check whether the given input file is valid, returning a reason if not."""
+class FileAction(argparse.Action):
+  def __init__(self, option_strings, dest, **kwargs):
+    super(FileAction, self).__init__(option_strings, dest, **kwargs)
+  def __call__(self, parser, namespace, values, option_string=None):
+    if option_string is None:
+      validate_input_files(values)
+    else:
+      # presumably output files (e.g., .bc, .ll, etc)
+      validate_output_file(values)
+    setattr(namespace, self.dest, values)
 
-  file_extension = os.path.splitext(file)[1][1:]
-  if not os.path.isfile(file):
-    return ("Cannot find file %s." % file)
+def exit_with_error(error):
+  sys.exit('Error: %s.' % error)
 
-  elif not file_extension in frontends():
-    return ("Unexpected source file extension '%s'." % file_extension)
+def validate_input_files(files):
+  def validate_input_file(file):
+    """Check whether the given input file is valid, returning a reason if not."""
 
-  else:
-    return None
+    file_extension = os.path.splitext(file)[1][1:]
+    if not os.path.isfile(file):
+      exit_with_error("Cannot find file %s" % file)
+
+    if not os.access(file, os.R_OK):
+      exit_with_error("Cannot read file %s" % file)
+
+    elif not file_extension in frontends():
+      exit_with_error("Unexpected source file extension '%s'" % file_extension)
+  map(validate_input_file, files)
+
+def validate_output_file(file):
+  file_extension = os.path.splitext(file)[1][1:]
+
+  try:
+    f = open(file, 'w')
+  except OSError:
+    exit_with_error("file %s may not be writeable" % file)
+  finally:
+    f.close()
 
 def arguments():
   """Parse command-line arguments"""
 
   parser = argparse.ArgumentParser()
 
-  parser.add_argument('input_files', metavar='input-files', nargs='+',
-    type = lambda x: (lambda r: x if r is None else parser.error(r))(validate_input_file(x)),
-    help = 'source file to be translated/verified')
+  parser.add_argument('input_files', metavar='input-files', nargs='+', action=FileAction,
+    type = str, help = 'source file to be translated/verified')
 
   parser.add_argument('--version', action='version',
     version='SMACK version ' + VERSION)
@@ -117,7 +142,7 @@ def arguments():
     choices=frontends().keys(), default=None,
     help='Treat input files as having type LANG.')
 
-  frontend_group.add_argument('-bc', '--bc-file', metavar='FILE', default=None,
+  frontend_group.add_argument('-bc', '--bc-file', metavar='FILE', default=None, action=FileAction,
     type=str, help='save initial LLVM bitcode to FILE')
 
   frontend_group.add_argument('--linked-bc-file', metavar='FILE', default=None,
@@ -129,7 +154,7 @@ def arguments():
   frontend_group.add_argument('--replay-exe-file', metavar='FILE', default='replay-exe',
     type=str, help=argparse.SUPPRESS)
 
-  frontend_group.add_argument('-ll', '--ll-file', metavar='FILE', default=None,
+  frontend_group.add_argument('-ll', '--ll-file', metavar='FILE', default=None, action=FileAction,
     type=str, help='save final LLVM IR to FILE')
 
   frontend_group.add_argument('--clang-options', metavar='OPTIONS', default='',
@@ -138,7 +163,7 @@ def arguments():
 
   translate_group = parser.add_argument_group('translation options')
 
-  translate_group.add_argument('-bpl', '--bpl-file', metavar='FILE', default=None,
+  translate_group.add_argument('-bpl', '--bpl-file', metavar='FILE', default=None, action=FileAction,
     type=str, help='save (intermediate) Boogie code to FILE')
 
   translate_group.add_argument('--no-memory-splitting', action="store_true", default=False,

From 8120956e50eb1f1c5bc713482ae80cfdae7f1672 Mon Sep 17 00:00:00 2001
From: Shaobo <polarishehn@gmail.com>
Date: Mon, 16 Jul 2018 09:41:50 -0600
Subject: [PATCH 02/60] Bug fix

---
 share/smack/top.py | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/share/smack/top.py b/share/smack/top.py
index a181f9d15..570d46a3a 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -98,11 +98,10 @@ def validate_output_file(file):
   file_extension = os.path.splitext(file)[1][1:]
 
   try:
-    f = open(file, 'w')
-  except OSError:
+    with open(file, 'w') as f:
+      pass
+  except IOError:
     exit_with_error("file %s may not be writeable" % file)
-  finally:
-    f.close()
 
 def arguments():
   """Parse command-line arguments"""

From c5f579d92775bd1e19a59f4b9ade61890e69aa7c Mon Sep 17 00:00:00 2001
From: Shaobo <polarishehn@gmail.com>
Date: Mon, 16 Jul 2018 12:19:20 -0600
Subject: [PATCH 03/60] Use an alternative way to check the validity of output
 file path

The old way seems to cause certain issue for regtest
---
 share/smack/top.py | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/share/smack/top.py b/share/smack/top.py
index 570d46a3a..35cf72e4c 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -95,13 +95,16 @@ def validate_input_file(file):
   map(validate_input_file, files)
 
 def validate_output_file(file):
-  file_extension = os.path.splitext(file)[1][1:]
-
-  try:
-    with open(file, 'w') as f:
-      pass
-  except IOError:
+  dir_name = os.path.dirname(os.path.abspath(file))
+  if not os.path.isdir(dir_name):
+    exit_with_error("directory %s doesn't exist" % dirname)
+  if not os.access(dir_name, os.W_OK):
     exit_with_error("file %s may not be writeable" % file)
+  #try:
+  #  with open(file, 'w') as f:
+  #    pass
+  #except IOError:
+  #  exit_with_error("file %s may not be writeable" % file)
 
 def arguments():
   """Parse command-line arguments"""

From 1f2534b1a6e15708694047ffe34ce36f501ce619 Mon Sep 17 00:00:00 2001
From: zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 18 Oct 2018 15:08:26 +0200
Subject: [PATCH 04/60] Updated mono install procedure

Mono changed slightly their installation procedure. This is now
reflected in our scripts.
---
 .travis.yml  | 3 ++-
 bin/build.sh | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 01c29cbf3..fb2865022 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -42,7 +42,8 @@ before_install:
   - sudo add-apt-repository "deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.9 main"
   - wget -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
   - sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
-  - echo "deb http://download.mono-project.com/repo/ubuntu trusty main" | sudo tee /etc/apt/sources.list.d/mono-official.list
+  - sudo apt-get install -y apt-transport-https
+  - echo "deb https://download.mono-project.com/repo/ubuntu stable-trusty main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
   - sudo apt-get update
 
 install:
diff --git a/bin/build.sh b/bin/build.sh
index fc75a23c7..fda3d9480 100755
--- a/bin/build.sh
+++ b/bin/build.sh
@@ -271,7 +271,8 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
     ${WGET} -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
     # Adding MONO repository
     sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
-    echo "deb http://download.mono-project.com/repo/ubuntu trusty main" | sudo tee /etc/apt/sources.list.d/mono-official.list
+    sudo apt-get install -y apt-transport-https
+    echo "deb https://download.mono-project.com/repo/ubuntu stable-trusty main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
     sudo apt-get update
     sudo apt-get install -y ${DEPENDENCIES}
     sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_SHORT_VERSION} 30

From 4009480bee560ef6ebeade29595870e65682a2c3 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 18 Oct 2018 08:39:04 -0600
Subject: [PATCH 05/60] Switched to bento vagrant boxes

These boxes have better support than minimal.
They are also smaller.
---
 Vagrantfile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Vagrantfile b/Vagrantfile
index 3f304317e..ff6fe2834 100644
--- a/Vagrantfile
+++ b/Vagrantfile
@@ -10,7 +10,7 @@ Vagrant.configure(2) do |config|
   config.vm.synced_folder ".", "/home/vagrant/#{project_name}"
 
   config.vm.define :ubuntu do |ubuntu_config|
-    ubuntu_config.vm.box = "minimal/trusty64"
+    ubuntu_config.vm.box = "bento/ubuntu-14.04"
   end
 
   # This provision, 'fix-no-tty', gets rid of an error during build

From 16eb0408a0cc310a4adf09eb3adcefdd0db5eecf Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 18 Oct 2018 08:48:11 -0600
Subject: [PATCH 06/60] Updated default vagrant Ubuntu release to 16.04
 (xenial)

Note that Travis CI still does not support xenial. So switching
Travis to xenial will have to be done later on once they start
supporting it.
---
 Vagrantfile  |  2 +-
 bin/build.sh | 10 +++++++---
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/Vagrantfile b/Vagrantfile
index ff6fe2834..22d9228ea 100644
--- a/Vagrantfile
+++ b/Vagrantfile
@@ -10,7 +10,7 @@ Vagrant.configure(2) do |config|
   config.vm.synced_folder ".", "/home/vagrant/#{project_name}"
 
   config.vm.define :ubuntu do |ubuntu_config|
-    ubuntu_config.vm.box = "bento/ubuntu-14.04"
+    ubuntu_config.vm.box = "bento/ubuntu-16.04"
   end
 
   # This provision, 'fix-no-tty', gets rid of an error during build
diff --git a/bin/build.sh b/bin/build.sh
index fda3d9480..c01d8ddc8 100755
--- a/bin/build.sh
+++ b/bin/build.sh
@@ -186,11 +186,16 @@ linux-opensuse*)
   DEPENDENCIES+=" ncurses-devel zlib-devel"
   ;;
 
-linux-@(ubuntu|neon)-1[46]*)
+linux-@(ubuntu|neon)-14*)
   Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-14.04.zip"
   DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION} mono-complete libz-dev libedit-dev"
   ;;
 
+linux-@(ubuntu|neon)-16*)
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-16.04.zip"
+  DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION} mono-complete libz-dev libedit-dev"
+  ;;
+
 linux-ubuntu-12*)
   Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-14.04.zip"
   DEPENDENCIES+=" g++-4.8 autoconf automake bison flex libtool gettext gdb"
@@ -248,7 +253,6 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
 
   linux-@(ubuntu|neon)-1[46]*)
     RELEASE_VERSION=$(get-platform-trim "$(lsb_release -r)" | awk -F: '{print $2;}')
-    UBUNTU_CODENAME="trusty"
     case "$RELEASE_VERSION" in
     14*)
       UBUNTU_CODENAME="trusty"
@@ -272,7 +276,7 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
     # Adding MONO repository
     sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
     sudo apt-get install -y apt-transport-https
-    echo "deb https://download.mono-project.com/repo/ubuntu stable-trusty main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
+    echo "deb https://download.mono-project.com/repo/ubuntu stable-${UBUNTU_CODENAME} main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
     sudo apt-get update
     sudo apt-get install -y ${DEPENDENCIES}
     sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_SHORT_VERSION} 30

From 2253d7917e7be16a9d7d2696f16a6a8713de60d9 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sat, 20 Oct 2018 13:30:48 -0600
Subject: [PATCH 07/60] Updated Z3, Boogie, and Corral versions

---
 bin/build.sh | 8 ++++----
 bin/versions | 7 ++++---
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/bin/build.sh b/bin/build.sh
index c01d8ddc8..3ccb41f46 100755
--- a/bin/build.sh
+++ b/bin/build.sh
@@ -181,23 +181,23 @@ puts "Detected distribution: $distro"
 # Set platform-dependent flags
 case "$distro" in
 linux-opensuse*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-debian-8.10.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-debian-8.10.zip"
   DEPENDENCIES+=" llvm-clang llvm-devel gcc-c++ mono-complete make"
   DEPENDENCIES+=" ncurses-devel zlib-devel"
   ;;
 
 linux-@(ubuntu|neon)-14*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-14.04.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-14.04.zip"
   DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION} mono-complete libz-dev libedit-dev"
   ;;
 
 linux-@(ubuntu|neon)-16*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-16.04.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-16.04.zip"
   DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION} mono-complete libz-dev libedit-dev"
   ;;
 
 linux-ubuntu-12*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-14.04.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-14.04.zip"
   DEPENDENCIES+=" g++-4.8 autoconf automake bison flex libtool gettext gdb"
   DEPENDENCIES+=" libglib2.0-dev libfontconfig1-dev libfreetype6-dev libxrender-dev"
   DEPENDENCIES+=" libtiff-dev libjpeg-dev libgif-dev libpng-dev libcairo2-dev"
diff --git a/bin/versions b/bin/versions
index eb99b176f..8fa4712cd 100644
--- a/bin/versions
+++ b/bin/versions
@@ -1,7 +1,8 @@
 MONO_VERSION=5.0.0.100
-Z3_VERSION=4.6.0
-BOOGIE_COMMIT=c92bebd817
-CORRAL_COMMIT=179251cc9c
+Z3_SHORT_VERSION=4.8.1
+Z3_FULL_VERSION=4.8.1.016872a5e0f6
+BOOGIE_COMMIT=cd0609f660
+CORRAL_COMMIT=d7d389f22d
 SYMBOOGLIX_COMMIT=7210e5d09b
 LOCKPWN_COMMIT=73eddf97bd
 LLVM_SHORT_VERSION=3.9

From 3f844ef215a51b535c83a2a77291ab4e0aabb9b1 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sun, 21 Oct 2018 10:56:52 -0600
Subject: [PATCH 08/60] Fixed compiler warnings in models of string functions

---
 share/smack/include/string/string.h |  2 ++
 share/smack/lib/string.c            | 23 ++++++++++++-----------
 2 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/share/smack/include/string/string.h b/share/smack/include/string/string.h
index cefabd4e0..ca870343d 100644
--- a/share/smack/include/string/string.h
+++ b/share/smack/include/string/string.h
@@ -6,6 +6,8 @@
 
 #include <stddef.h>
 
+void *memcpy(void *str1, const void *str2, size_t n);
+void *memset(void *str, int c, size_t n);
 char *strcpy(char *dest, const char *src);
 size_t strlen(const char *str);
 char *strrchr(const char *src, int c);
diff --git a/share/smack/lib/string.c b/share/smack/lib/string.c
index 8b2438b28..4bf694e9a 100644
--- a/share/smack/lib/string.c
+++ b/share/smack/lib/string.c
@@ -3,10 +3,11 @@
 //
 #include <string.h>
 #include <stdlib.h>
+#include <smack.h>
 
 char *strcpy(char *dest, const char *src) {
   char *save = dest;
-  while (*dest++ = *src++);
+  while ((*dest++ = *src++));
   return save;
 }
 
@@ -55,7 +56,7 @@ char *strcat(char *dest, const char *src) {
 
   while (*dest)
     dest++;
-  while (*dest++ = *src++) ;
+  while ((*dest++ = *src++)) ;
 
   return retDest;
 }
@@ -77,7 +78,7 @@ char *strncat(char *dest, const char *src, size_t n) {
 char *strchr(const char *src, int c) {
   while (*src != 0) {
     if (*src == c) {
-      return src;
+      return (char *)src;
     }
     src++;
   }
@@ -90,7 +91,7 @@ char *strrchr(const char *src, int c) {
 
   while (*src != 0) {
     if (*src == c) {
-      result = src;
+      result = (char *)src;
     }
     src++;
   }
@@ -118,8 +119,8 @@ size_t strcspn(const char *s1, const char *s2) {
 }
 
 char *strpbrk(const char *s1, const char *s2) {
-  for (char *c1 = s1; *c1; c1++)
-    for (char *c2 = s2; *c2; c2++)
+  for (char *c1 = (char *)s1; *c1; c1++)
+    for (char *c2 = (char *)s2; *c2; c2++)
       if (*c1 == *c2)
         return c1;
   return 0;
@@ -133,7 +134,7 @@ char *strstr(const char *haystack, const char *needle) {
     const char *h, *n;
     for (h = haystack, n = needle; *h && *n && (*h == *n); h++, n++);
     if (*n == '\0')
-      return haystack;
+      return (char *)haystack;
   }
   return 0;
 }
@@ -168,13 +169,13 @@ char *strtok(char *str, const char *delim) {
 unsigned long int strtoul(const char *nptr, char **endptr, int base) {
   if (__VERIFIER_nondet_int()) {
     if (endptr != 0) {
-      *endptr = nptr;
+      *endptr = (char *)nptr;
     }
     return 0;
   } else {
     if (endptr != 0) {
       size_t size = strlen(nptr);
-      *endptr = nptr + size;
+      *endptr = (char *)nptr + size;
     }
     return __VERIFIER_nondet_ulong();
   }
@@ -183,13 +184,13 @@ unsigned long int strtoul(const char *nptr, char **endptr, int base) {
 double strtod(const char *nptr, char **endptr) {
   if (__VERIFIER_nondet_int()) {
     if (endptr != 0) {
-      *endptr = nptr;
+      *endptr = (char *)nptr;
     }
     return 0.0;
   } else {
     if (endptr != 0) {
       size_t size = strlen(nptr);
-      *endptr = nptr + size;
+      *endptr = (char *)nptr + size;
     }
     return __VERIFIER_nondet_long();
   }

From 0a3c98bc9687c09f765c210246d72c9bea1e214a Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sun, 21 Oct 2018 14:16:38 -0600
Subject: [PATCH 09/60] Refactored handling of standard C headers and
 implementations

Moved functions around to appropriate files. Got rid of subfolders
that were not needed.
---
 share/smack/frontend.py               |  6 +--
 share/smack/include/{math => }/math.h |  0
 share/smack/include/string/string.h   | 21 ---------
 share/smack/lib/smack.c               | 11 -----
 share/smack/lib/stdlib.c              | 64 +++++++++++++++++++++++++++
 share/smack/lib/string.c              | 45 -------------------
 6 files changed, 65 insertions(+), 82 deletions(-)
 rename share/smack/include/{math => }/math.h (100%)
 delete mode 100644 share/smack/include/string/string.h
 create mode 100644 share/smack/lib/stdlib.c

diff --git a/share/smack/frontend.py b/share/smack/frontend.py
index fac614d6e..0c3357132 100644
--- a/share/smack/frontend.py
+++ b/share/smack/frontend.py
@@ -61,10 +61,6 @@ def smack_header_path():
 def smack_headers(args):
   paths = []
   paths.append(smack_header_path())
-  if args.memory_safety or args.integer_overflow:
-    paths.append(os.path.join(smack_header_path(), 'string'))
-  if args.float:
-    paths.append(os.path.join(smack_header_path(), 'math'))
   return paths
 
 def smack_lib():
@@ -237,7 +233,7 @@ def rust_frontend(input_file, args):
 def default_build_libs(args):
   """Generate LLVM bitcodes for SMACK libraries."""
   bitcodes = []
-  libs = ['smack.c']
+  libs = ['smack.c', 'stdlib.c']
 
   if args.pthread:
     libs += ['pthread.c']
diff --git a/share/smack/include/math/math.h b/share/smack/include/math.h
similarity index 100%
rename from share/smack/include/math/math.h
rename to share/smack/include/math.h
diff --git a/share/smack/include/string/string.h b/share/smack/include/string/string.h
deleted file mode 100644
index ca870343d..000000000
--- a/share/smack/include/string/string.h
+++ /dev/null
@@ -1,21 +0,0 @@
-// This file is distributed under the MIT License. See LICENSE for details.
-//
-
-#ifndef STRING_H
-#define STRING_H
-
-#include <stddef.h>
-
-void *memcpy(void *str1, const void *str2, size_t n);
-void *memset(void *str, int c, size_t n);
-char *strcpy(char *dest, const char *src);
-size_t strlen(const char *str);
-char *strrchr(const char *src, int c);
-size_t strspn(const char *cs, const char *ct);
-unsigned long int strtoul(const char *nptr, char **endptr, int base);
-double strtod(const char *nptr, char **endptr);
-char *strerror(int errnum);
-char *getenv(const char *name);
-void *realloc (void *__ptr, size_t __size);
-
-#endif
diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c
index f2e8b54e0..3d289f8db 100644
--- a/share/smack/lib/smack.c
+++ b/share/smack/lib/smack.c
@@ -257,17 +257,6 @@ void* __VERIFIER_nondet_pointer(void) {
   return __VERIFIER_nondet();
 }
 
-void* calloc(size_t num, size_t size) {
-  void* ret;
-  if (__VERIFIER_nondet_int()) {
-    ret = 0;
-  } else {
-    ret = malloc(num * size);
-    memset(ret, 0, num * size);
-  }
-  return ret;
-}
-
 void __SMACK_dummy(int v) {
   __SMACK_code("assume true;");
 }
diff --git a/share/smack/lib/stdlib.c b/share/smack/lib/stdlib.c
new file mode 100644
index 000000000..f7948ca13
--- /dev/null
+++ b/share/smack/lib/stdlib.c
@@ -0,0 +1,64 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+#include <stdlib.h>
+#include <string.h>
+#include <smack.h>
+
+void* calloc(size_t num, size_t size) {
+  void* ret;
+  if (__VERIFIER_nondet_int()) {
+    ret = 0;
+  } else {
+    ret = malloc(num * size);
+    memset(ret, 0, num * size);
+  }
+  return ret;
+}
+
+void *realloc(void *ptr, size_t size) {
+  free(ptr);
+  return malloc(size);
+}
+
+unsigned long int strtoul(const char *nptr, char **endptr, int base) {
+  if (__VERIFIER_nondet_int()) {
+    if (endptr != 0) {
+      *endptr = (char *)nptr;
+    }
+    return 0;
+  } else {
+    if (endptr != 0) {
+      size_t size = strlen(nptr);
+      *endptr = (char *)nptr + size;
+    }
+    return __VERIFIER_nondet_ulong();
+  }
+}
+
+double strtod(const char *nptr, char **endptr) {
+  if (__VERIFIER_nondet_int()) {
+    if (endptr != 0) {
+      *endptr = (char *)nptr;
+    }
+    return 0.0;
+  } else {
+    if (endptr != 0) {
+      size_t size = strlen(nptr);
+      *endptr = (char *)nptr + size;
+    }
+    return __VERIFIER_nondet_long();
+  }
+}
+
+char *env_value_str = "xx";
+char *getenv(const char *name) {
+  if (__VERIFIER_nondet_int()) {
+    return 0;
+  } else {
+    env_value_str[0] = __VERIFIER_nondet_char();
+    env_value_str[1] = __VERIFIER_nondet_char();
+    return env_value_str;
+  }
+}
+
diff --git a/share/smack/lib/string.c b/share/smack/lib/string.c
index 4bf694e9a..a0cff849d 100644
--- a/share/smack/lib/string.c
+++ b/share/smack/lib/string.c
@@ -166,36 +166,6 @@ char *strtok(char *str, const char *delim) {
   return tok;
 }
 
-unsigned long int strtoul(const char *nptr, char **endptr, int base) {
-  if (__VERIFIER_nondet_int()) {
-    if (endptr != 0) {
-      *endptr = (char *)nptr;
-    }
-    return 0;
-  } else {
-    if (endptr != 0) {
-      size_t size = strlen(nptr);
-      *endptr = (char *)nptr + size;
-    }
-    return __VERIFIER_nondet_ulong();
-  }
-}
-
-double strtod(const char *nptr, char **endptr) {
-  if (__VERIFIER_nondet_int()) {
-    if (endptr != 0) {
-      *endptr = (char *)nptr;
-    }
-    return 0.0;
-  } else {
-    if (endptr != 0) {
-      size_t size = strlen(nptr);
-      *endptr = (char *)nptr + size;
-    }
-    return __VERIFIER_nondet_long();
-  }
-}
-
 char *error_str = "xx";
 char *strerror(int errnum) {
   error_str[0] = __VERIFIER_nondet_char();
@@ -203,18 +173,3 @@ char *strerror(int errnum) {
   return error_str;
 }
 
-char *env_value_str = "xx";
-char *getenv(const char *name) {
-  if (__VERIFIER_nondet_int()) {
-    return 0;
-  } else {
-    env_value_str[0] = __VERIFIER_nondet_char();
-    env_value_str[1] = __VERIFIER_nondet_char();
-    return env_value_str;
-  }
-}
-
-void *realloc (void *__ptr, size_t __size) {
-  free(__ptr);
-  return malloc(__size);
-}

From b135323a5af67c7daa29b4c232acd7281e23b77e Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sun, 21 Oct 2018 14:20:01 -0600
Subject: [PATCH 10/60] No need for null check on arguments of strstr

Passing null should lead to a memory safety error instead.
---
 share/smack/lib/string.c | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/share/smack/lib/string.c b/share/smack/lib/string.c
index a0cff849d..158f23bc5 100644
--- a/share/smack/lib/string.c
+++ b/share/smack/lib/string.c
@@ -127,9 +127,6 @@ char *strpbrk(const char *s1, const char *s2) {
 }
 
 char *strstr(const char *haystack, const char *needle) {
-  if (!haystack || !needle)
-    return 0;
-
   for (; *haystack; haystack++) {
     const char *h, *n;
     for (h = haystack, n = needle; *h && *n && (*h == *n); h++, n++);

From ced8cb0d6cdfc9d15a832aa07b4d3baee7f1497c Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Mon, 22 Oct 2018 03:46:29 -0600
Subject: [PATCH 11/60] Updated models for strto functions

The new models are simpler, and yet capture the same intent as
the previous ones. I also added the missing ones.
---
 share/smack/lib/stdlib.c | 54 ++++++++++++++++++++++++----------------
 1 file changed, 32 insertions(+), 22 deletions(-)

diff --git a/share/smack/lib/stdlib.c b/share/smack/lib/stdlib.c
index f7948ca13..134450a63 100644
--- a/share/smack/lib/stdlib.c
+++ b/share/smack/lib/stdlib.c
@@ -21,34 +21,44 @@ void *realloc(void *ptr, size_t size) {
   return malloc(size);
 }
 
+long int strtol(const char *nptr, char **endptr, int base) {
+  if (endptr != 0) {
+    size_t size = strlen(nptr);
+    unsigned nondet = __VERIFIER_nondet_unsigned_int();
+    __VERIFIER_assume(nondet <= size);
+    *endptr = (char *)nptr + nondet;
+  }
+  return __VERIFIER_nondet_long();
+}
+
 unsigned long int strtoul(const char *nptr, char **endptr, int base) {
-  if (__VERIFIER_nondet_int()) {
-    if (endptr != 0) {
-      *endptr = (char *)nptr;
-    }
-    return 0;
-  } else {
-    if (endptr != 0) {
-      size_t size = strlen(nptr);
-      *endptr = (char *)nptr + size;
-    }
-    return __VERIFIER_nondet_ulong();
+  if (endptr != 0) {
+    size_t size = strlen(nptr);
+    unsigned nondet = __VERIFIER_nondet_unsigned_int();
+    __VERIFIER_assume(nondet <= size);
+    *endptr = (char *)nptr + nondet;
   }
+  return __VERIFIER_nondet_unsigned_long();
+}
+
+unsigned long long int strtoull(const char *nptr, char **endptr, int base) {
+  if (endptr != 0) {
+    size_t size = strlen(nptr);
+    unsigned nondet = __VERIFIER_nondet_unsigned_int();
+    __VERIFIER_assume(nondet <= size);
+    *endptr = (char *)nptr + nondet;
+  }
+  return __VERIFIER_nondet_unsigned_long_long();
 }
 
 double strtod(const char *nptr, char **endptr) {
-  if (__VERIFIER_nondet_int()) {
-    if (endptr != 0) {
-      *endptr = (char *)nptr;
-    }
-    return 0.0;
-  } else {
-    if (endptr != 0) {
-      size_t size = strlen(nptr);
-      *endptr = (char *)nptr + size;
-    }
-    return __VERIFIER_nondet_long();
+  if (endptr != 0) {
+    size_t size = strlen(nptr);
+    unsigned nondet = __VERIFIER_nondet_unsigned_int();
+    __VERIFIER_assume(nondet <= size);
+    *endptr = (char *)nptr + nondet;
   }
+  return __VERIFIER_nondet_double();
 }
 
 char *env_value_str = "xx";

From c854fa8b000d22df431259745f94526d05167206 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Mon, 22 Oct 2018 04:10:48 -0600
Subject: [PATCH 12/60] Fixed handling of unnamed globals when generating debug
 info

Instead of an assertion requiring that globals are named,
we now simply skip generating debug info for unnamed globals.

Fixes #378
---
 lib/smack/SmackInstGenerator.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp
index 3e0484f82..ba672d087 100644
--- a/lib/smack/SmackInstGenerator.cpp
+++ b/lib/smack/SmackInstGenerator.cpp
@@ -477,8 +477,7 @@ void SmackInstGenerator::visitStoreInst(llvm::StoreInst& si) {
   if (SmackOptions::SourceLocSymbols) {
     if (const llvm::GlobalVariable* G = llvm::dyn_cast<const llvm::GlobalVariable>(P)) {
       if (const llvm::PointerType* t = llvm::dyn_cast<const llvm::PointerType>(G->getType())) {
-        if (!t->getElementType()->isPointerTy()) {
-          assert(G->hasName() && "Expected named global variable.");
+        if (!t->getElementType()->isPointerTy() && G->hasName()) {
           emit(recordProcedureCall(V, {Attr::attr("cexpr", G->getName().str())}));
         }
       }

From c57ced480c155c1ccbf8116c13d191f811fefde2 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Mon, 22 Oct 2018 20:07:30 +0000
Subject: [PATCH 13/60] Restored SMACK's SV-COMP witness file generation

This commit does the following,
1. Updated SMACK's JSON output generation according to Corral's C
trace format changes.
2. Updated JSON-to-witness-trace translation.
3. Simplified some logic in related scripts.
---
 share/smack/svcomp/toSVCOMPformat.py | 18 +++++++++++-----
 share/smack/svcomp/utils.py          |  2 +-
 share/smack/top.py                   | 32 ++++++++++++++--------------
 3 files changed, 30 insertions(+), 22 deletions(-)

diff --git a/share/smack/svcomp/toSVCOMPformat.py b/share/smack/svcomp/toSVCOMPformat.py
index 4f1bde6e4..6f5184375 100644
--- a/share/smack/svcomp/toSVCOMPformat.py
+++ b/share/smack/svcomp/toSVCOMPformat.py
@@ -133,6 +133,9 @@ def formatAssign(assignStmt):
     else:
       return ""
 
+def isSMACKInitFunc(funcName):
+  return funcName == '$initialize' or funcName == '__SMACK_static_init' or funcName == '__SMACK_init_func_memory_model'
+
 def smackJsonToXmlGraph(strJsonOutput, args, hasBug):
     """Converts output from SMACK (in the smackd json format) to a graphml
        format that conforms to the SVCOMP witness file format"""
@@ -157,23 +160,26 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug):
       for jsonTrace in jsonTraces:
         # Make sure it isn't a smack header file
         if not pat.match(jsonTrace["file"]):
+          desc = jsonTrace["description"]
           if formatAssign(jsonTrace["description"]):
           # Create new node and edge
             newNode = addGraphNode(tree)
             attribs = {"startline":str(jsonTrace["line"])}
-            attribs["assumption"] = formatAssign(str(jsonTrace["description"])) + ";"
+            attribs["assumption"] = formatAssign(desc) + ";"
             attribs["assumption.scope"] = callStack[-1]
             newEdge = addGraphEdge(tree, lastNode, newNode, attribs)
             prevLineNo = jsonTrace["line"]
             prevColNo = jsonTrace["column"]
             lastNode = newNode
             lastEdge = newEdge
-          if "CALL" in jsonTrace["description"]:
+          if "CALL" in desc:
             # Add function to call stack
             calledFunc = str(jsonTrace["description"][len("CALL "):]).strip()
             if calledFunc.startswith("devirtbounce"):
               print "Warning: calling function pointer dispatch procedure at line {0}".format(jsonTrace["line"])
               continue
+            if isSMACKInitFunc(calledFunc):
+              continue
             callStack.append(calledFunc)
             if (("__VERIFIER_error" in jsonTrace["description"][len("CALL"):]) or
                 ("__SMACK_overflow_false" in jsonTrace["description"][len("CALL"):]) or
@@ -185,15 +191,17 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug):
                 if vNode.attrib["id"] == newNode:
                   addKey(vNode, "violation", "true")
               attribs = {"startline":str(jsonTrace["line"])}
-              if not args.signed_integer_overflow:
+              if not args.integer_overflow:
                 attribs["enterFunction"] = callStack[-1]
               addGraphEdge(tree, lastNode, newNode, attribs)
               break
-          if "RETURN from" in jsonTrace["description"]:
-            returnedFunc = str(jsonTrace["description"][len("RETURN from "):]).strip()
+          if "RETURN from" in desc:
+            returnedFunc = str(desc[len("RETURN from "):]).strip()
             if returnedFunc.startswith("devirtbounce"):
               print "Warning: returning from function pointer dispatch procedure at line {0}".format(jsonTrace["line"])
               continue
+            if isSMACKInitFunc(returnedFunc):
+              continue
             if returnedFunc != callStack[-1]:
               raise RuntimeError('Procedure Call/Return dismatch at line {0}. Call stack head: {1}, returning from: {2}'.format(jsonTrace["line"], callStack[-1], returnedFunc))
             callStack.pop()
diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 26384ad9b..4e6625e4a 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -438,7 +438,7 @@ def verify_bpl_svcomp(args):
     sys.exit(smack.top.results(args)[result])
 
 def write_error_file(args, status, verifier_output):
-  return
+  #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
index eafa554ff..362a49a08 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -517,6 +517,8 @@ def error_trace(verifier_output, args):
 
 def smackdOutput(corralOutput):
   FILENAME = '[\w#$~%.\/-]+'
+  traceP = re.compile('(' + FILENAME + ')\((\d+),(\d+)\): Trace: Thread=(\d+)  (\((.*)\))?$')
+  errorP = re.compile('(' + FILENAME + ')\((\d+),(\d+)\): (error .*)$')
 
   passedMatch = re.search('Program has no bugs', corralOutput)
   if passedMatch:
@@ -533,32 +535,30 @@ def smackdOutput(corralOutput):
     threadid = 0
     desc = ''
     for traceLine in corralOutput.splitlines(True):
-      traceMatch = re.match('(' + FILENAME + ')\((\d+),(\d+)\): Trace: Thread=(\d+)  (\((.*)\))?$', traceLine)
-      traceAssumeMatch = re.match('(' + FILENAME + ')\((\d+),(\d+)\): Trace: Thread=(\d+)  (\((\s*\w+\s*=\s*\w+\s*)\))$', traceLine)
-      errorMatch = re.match('(' + FILENAME + ')\((\d+),(\d+)\): (error .*)$', traceLine)
+      traceMatch = traceP.match(traceLine)
       if traceMatch:
         filename = str(traceMatch.group(1))
         lineno = int(traceMatch.group(2))
         colno = int(traceMatch.group(3))
         threadid = int(traceMatch.group(4))
         desc = str(traceMatch.group(6))
-        assm = ''
-        if traceAssumeMatch:
-          assm = str(traceAssumeMatch.group(6))
-          #Remove bitvector indicator from trace assumption
-          assm = re.sub(r'=(\s*\d+)bv\d+', r'=\1', assm)
-        trace = { 'threadid': threadid,
+        for e in desc.split(','):
+          e = e.strip()
+          assm = re.sub(r'=(\s*\d+)bv\d+', r'=\1', e) if '=' in e else ''
+          trace = { 'threadid': threadid,
                   'file': filename,
                   'line': lineno,
                   'column': colno,
-                  'description': '' if desc == 'None' else desc,
+                  'description': e,
                   'assumption': assm }
-        traces.append(trace)
-      elif errorMatch:
-        filename = str(errorMatch.group(1))
-        lineno = int(errorMatch.group(2))
-        colno = int(errorMatch.group(3))
-        desc = str(errorMatch.group(4))
+          traces.append(trace)
+      else:
+        errorMatch = errorP.match(traceLine)
+        if errorMatch:
+          filename = str(errorMatch.group(1))
+          lineno = int(errorMatch.group(2))
+          colno = int(errorMatch.group(3))
+          desc = str(errorMatch.group(4))
 
     failsAt = { 'file': filename, 'line': lineno, 'column': colno, 'description': desc }
 

From 464e852b4cfad0b819e0cc5aa7c9f72c31cf2dfd Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Tue, 23 Oct 2018 06:22:27 -0600
Subject: [PATCH 14/60] Moved exit function from smack.c to stdlib.c

---
 share/smack/lib/smack.c  | 8 --------
 share/smack/lib/stdlib.c | 8 ++++++++
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c
index 3d289f8db..ad8eec7a7 100644
--- a/share/smack/lib/smack.c
+++ b/share/smack/lib/smack.c
@@ -55,14 +55,6 @@ void __SMACK_check_overflow(int flag) {
   __SMACK_dummy(flag); __SMACK_code("assert {:overflow} @ == $0;", flag);
 }
 
-void exit(int x) {
-#if MEMORY_SAFETY
-  __SMACK_code("assert $allocatedCounter == 0;");
-#endif
-  __SMACK_code("assume false;");
-  while(1);
-}
-
 char __VERIFIER_nondet_char(void) {
   char x = __SMACK_nondet_char();
   __VERIFIER_assume(x >= SCHAR_MIN && x <= SCHAR_MAX);
diff --git a/share/smack/lib/stdlib.c b/share/smack/lib/stdlib.c
index 134450a63..7f0eaf7d1 100644
--- a/share/smack/lib/stdlib.c
+++ b/share/smack/lib/stdlib.c
@@ -5,6 +5,14 @@
 #include <string.h>
 #include <smack.h>
 
+void exit(int x) {
+#if MEMORY_SAFETY
+  __SMACK_code("assert $allocatedCounter == 0;");
+#endif
+  __SMACK_code("assume false;");
+  while(1);
+}
+
 void* calloc(size_t num, size_t size) {
   void* ret;
   if (__VERIFIER_nondet_int()) {

From 20fcbdbe71a75c17f01b9c289c38fdbd2753c4de Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Tue, 23 Oct 2018 06:25:22 -0600
Subject: [PATCH 15/60] Turn on bit-vectors for an ECA SVCOMP benchmark

The benchmark needs bit-vector reasoning since it performs
division of negative numbers, in which case C standard does
not match SMTLIB integer arithmetic semantics.
---
 share/smack/svcomp/filters.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/share/smack/svcomp/filters.py b/share/smack/svcomp/filters.py
index 5546178ae..b36c452ce 100644
--- a/share/smack/svcomp/filters.py
+++ b/share/smack/svcomp/filters.py
@@ -50,7 +50,7 @@ def bv_filter(lines, raw_line_count, pruned_line_count):
   if ("bugBrokenOut" in lines or "returnsStructure" in lines or "__VERIFIER_nondet_double" in lines or
       "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines):
     return 0
-  elif '4294967294u' in lines:
+  elif ('4294967294u' in lines or '616783' in lines):
     return 1
 
   if raw_line_count > 1500:

From ada88847ebac735dbfeb1b4e0981fa29e54a8901 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Tue, 23 Oct 2018 14:55:33 -0600
Subject: [PATCH 16/60] Updated hacky SVCOMP loop reduction heuristics

---
 share/smack/svcomp/utils.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 4e6625e4a..842219958 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -119,6 +119,7 @@ def svcomp_process_file(args, name, ext):
       s = re.sub(r'100000', r'10', s)
       s = re.sub(r'15000', r'5', s)
       s = re.sub(r'i<=10000', r'i<=1', s)
+      s = re.sub(r'500000', r'50', s)
     elif length < 710 and 'dll_create_master' in s:
       args.no_memory_splitting = True
 

From 872bbb36cda120a00cd2cd62210afa6d5f181149 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Tue, 23 Oct 2018 14:59:39 -0600
Subject: [PATCH 17/60] Increased nested brackets depth for clang in SVCOMP

Some SVCOMP benchmarks have crazy nesting of brackets exceeding
256 levels deep, which couses for clang to stop with an error.
I am increasing the allowed depth with this commit.
---
 share/smack/svcomp/utils.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 842219958..9307adac9 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -50,6 +50,7 @@ def svcomp_frontend(input_file, args):
   name, ext = os.path.splitext(os.path.basename(args.input_files[0]))
   svcomp_process_file(args, name, ext)
 
+  args.clang_options += " -fbracket-depth=2048"
   args.clang_options += " -DSVCOMP"
   args.clang_options += " -DAVOID_NAME_CONFLICTS"
   args.clang_options += " -DCUSTOM_VERIFIER_ASSERT"

From 77f28c73758842b06764b7e1e088599a2522308a Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 25 Oct 2018 03:55:18 -0600
Subject: [PATCH 18/60] Updated loop bounds for several large SVCOMP benchmarks

---
 share/smack/svcomp/utils.py | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 9307adac9..d23cf0ece 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -222,6 +222,9 @@ def verify_bpl_svcomp(args):
   with open(args.bpl_file, "r") as f:
     bpl = f.read()
 
+  with open(args.input_files[0], "r") as f:
+    csource = f.read()
+
   is_crappy_driver_benchmark(args, bpl)
 
   if args.pthread:
@@ -294,6 +297,12 @@ def verify_bpl_svcomp(args):
   elif args.integer_overflow and ("jain" in bpl or "TerminatorRec02" in bpl or "NonTerminationSimple" in bpl):
     heurTrace += "Infinite loop in overflow benchmark. Setting loop unroll bar to INT_MAX.\n"
     loopUnrollBar = 2**31 - 1
+  elif args.integer_overflow and ("(x != 0)" in csource or "(z > 0)" in csource or "(max > 0)" in csource or "(k < N)" in csource):
+    heurTrace += "Large overflow benchmark. Setting loop unroll bar to INT_MAX.\n"
+    loopUnrollBar = 2**31 - 1
+  elif "i>>16" in csource:
+    heurTrace += "Large array reach benchmark. Setting loop unroll bar to INT_MAX.\n"
+    loopUnrollBar = 2**31 - 1
 
   if not "forall" in bpl:
     heurTrace += "No quantifiers detected. Setting z3 relevancy to 0.\n"

From bd255a3819798181cac13a972c9cc99fedf5fdf7 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 25 Oct 2018 10:25:07 -0600
Subject: [PATCH 19/60] Increased irreducible loop unroll count

I increased it to 12 since that is needed for new SVCOMP
sequentialized benchmarks.
---
 share/smack/svcomp/utils.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index d23cf0ece..fe4ded107 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -331,7 +331,7 @@ def verify_bpl_svcomp(args):
   command += ["/v:1"]
   command += ["/maxStaticLoopBound:%d" % staticLoopBound]
   command += ["/recursionBound:65536"]
-  command += ["/irreducibleLoopUnroll:2"]
+  command += ["/irreducibleLoopUnroll:12"]
   command += ["/trackAllVars"]
 
   verifier_output = smack.top.try_command(command, timeout=time_limit)

From ebbc0af585a78ee6bbb59b304945356b3e70a522 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 25 Oct 2018 13:36:13 -0600
Subject: [PATCH 20/60] Fixed a compiler warning in fenv

Using assume causes a warning to happen for SVCOMP benchmarks
since we turn off the definition of assume for SVCOMP.
---
 share/smack/lib/fenv.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/share/smack/lib/fenv.c b/share/smack/lib/fenv.c
index fd663fd04..859f4dd00 100644
--- a/share/smack/lib/fenv.c
+++ b/share/smack/lib/fenv.c
@@ -10,7 +10,7 @@ int fegetround(void) {
   const int CONST_FE_UPWARD = FE_UPWARD;
   const int CONST_FE_TOWARDZERO = FE_TOWARDZERO;
   int ret = __VERIFIER_nondet_int();
-  assume(ret < 0);
+  __VERIFIER_assume(ret < 0);
   __SMACK_code("if ($rmode == RNE) {@ := @;}", ret, CONST_FE_TONEAREST);
   __SMACK_code("if ($rmode == RTN) {@ := @;}", ret, CONST_FE_DOWNWARD);
   __SMACK_code("if ($rmode == RTP) {@ := @;}", ret, CONST_FE_UPWARD);

From 9a4c03c5729701ebb3dfa5aeb941d185f45c92e8 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 25 Oct 2018 15:03:53 -0600
Subject: [PATCH 21/60] Removed declaration of exit from SMACK header file

---
 share/smack/include/smack.h | 1 -
 1 file changed, 1 deletion(-)

diff --git a/share/smack/include/smack.h b/share/smack/include/smack.h
index 26958f3bc..60bf19eb4 100644
--- a/share/smack/include/smack.h
+++ b/share/smack/include/smack.h
@@ -54,7 +54,6 @@ void __VERIFIER_assume(int);
 void __VERIFIER_assert(int);
 #endif
 void __VERIFIER_error(void);
-void exit(int);
 
 #ifndef AVOID_NAME_CONFLICTS
 #define assert(EX) __VERIFIER_assert(EX)

From 80cc49a32d6e4203cfd442ed874cede94732f243 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Fri, 26 Oct 2018 01:38:47 -0600
Subject: [PATCH 22/60] Adjusting loop unroll for large SVCOMP overflow
 benchmark

---
 share/smack/svcomp/utils.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index fe4ded107..ddfe2c04e 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -297,7 +297,7 @@ def verify_bpl_svcomp(args):
   elif args.integer_overflow and ("jain" in bpl or "TerminatorRec02" in bpl or "NonTerminationSimple" in bpl):
     heurTrace += "Infinite loop in overflow benchmark. Setting loop unroll bar to INT_MAX.\n"
     loopUnrollBar = 2**31 - 1
-  elif args.integer_overflow and ("(x != 0)" in csource or "(z > 0)" in csource or "(max > 0)" in csource or "(k < N)" in csource):
+  elif args.integer_overflow and ("(x != 0)" in csource or "(z > 0)" in csource or "(max > 0)" in csource or "(k < N)" in csource or "partial_sum" in csource):
     heurTrace += "Large overflow benchmark. Setting loop unroll bar to INT_MAX.\n"
     loopUnrollBar = 2**31 - 1
   elif "i>>16" in csource:

From e52f1a84ba460339d1becc01aa4f0a6d3a056de6 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Fri, 26 Oct 2018 01:54:47 -0600
Subject: [PATCH 23/60] Adjusted heuristics for recognizing float benchmarks

---
 share/smack/svcomp/filters.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/share/smack/svcomp/filters.py b/share/smack/svcomp/filters.py
index b36c452ce..4d971390c 100644
--- a/share/smack/svcomp/filters.py
+++ b/share/smack/svcomp/filters.py
@@ -95,7 +95,8 @@ def float_filter(lines, raw_line_count, pruned_line_count):
   ddecl = 0
 
   if ("bugBrokenOut" in lines or "returnsStructure" in lines or "__VERIFIER_nondet_double" in lines or
-      "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines):
+      "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines or
+      "huge_floor" in lines or "huge_ceil" in lines or "tiny_sqrt" in lines or "fmax_float" in lines):
     return 1
 
   #heuristic #-1: don't do test on too large programs

From 99376b6f3fb32092096c92ab516cc7fbffadeaaf Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Fri, 26 Oct 2018 08:23:02 -0600
Subject: [PATCH 24/60] Fixed float filter for SVCOMP

---
 share/smack/svcomp/filters.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/share/smack/svcomp/filters.py b/share/smack/svcomp/filters.py
index 4d971390c..a018b0b1d 100644
--- a/share/smack/svcomp/filters.py
+++ b/share/smack/svcomp/filters.py
@@ -48,7 +48,8 @@ def svcomp_filter(f):
     
 def bv_filter(lines, raw_line_count, pruned_line_count):
   if ("bugBrokenOut" in lines or "returnsStructure" in lines or "__VERIFIER_nondet_double" in lines or
-      "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines):
+      "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines or
+      "huge_floor" in lines or "huge_ceil" in lines or "tiny_sqrt" in lines or "fmax_float" in lines):
     return 0
   elif ('4294967294u' in lines or '616783' in lines):
     return 1

From cd4abdb49d724ba98649a2182b727ee3d3dc7610 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Fri, 26 Oct 2018 09:27:58 -0600
Subject: [PATCH 25/60] Increasing BusyBox loop unroll bound for overflow

---
 share/smack/svcomp/utils.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index ddfe2c04e..d9e66fcbe 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -292,8 +292,8 @@ def verify_bpl_svcomp(args):
     heurTrace += "BusyBox memory safety benchmark detected. Setting loop unroll bar to 4.\n"
     loopUnrollBar = 4
   elif args.integer_overflow and "__main($i0" in bpl:
-    heurTrace += "BusyBox overflows benchmark detected. Setting loop unroll bar to 11.\n"
-    loopUnrollBar = 11
+    heurTrace += "BusyBox overflows benchmark detected. Setting loop unroll bar to 40.\n"
+    loopUnrollBar = 40
   elif args.integer_overflow and ("jain" in bpl or "TerminatorRec02" in bpl or "NonTerminationSimple" in bpl):
     heurTrace += "Infinite loop in overflow benchmark. Setting loop unroll bar to INT_MAX.\n"
     loopUnrollBar = 2**31 - 1

From 0dc5228c2f682901dc71b2d8f8ca499c8647967a Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Fri, 26 Oct 2018 10:18:01 -0600
Subject: [PATCH 26/60] Supressing warnings about unknown attributes in SVCOMP

---
 share/smack/svcomp/utils.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index d9e66fcbe..8f428601b 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -51,6 +51,7 @@ def svcomp_frontend(input_file, args):
   svcomp_process_file(args, name, ext)
 
   args.clang_options += " -fbracket-depth=2048"
+  args.clang_options += " -Wunknown-attributes"
   args.clang_options += " -DSVCOMP"
   args.clang_options += " -DAVOID_NAME_CONFLICTS"
   args.clang_options += " -DCUSTOM_VERIFIER_ASSERT"

From 21cc36a369056ed30addb04d614ed5a15a5be2a7 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Fri, 26 Oct 2018 11:33:11 -0600
Subject: [PATCH 27/60] Turn off di Corral flag for some SVCOMP benchmarks

It seems that it sometimes causes unsoundness, meaning bugs
to be missed.
---
 share/smack/svcomp/utils.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 8f428601b..dc259e9a8 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -51,7 +51,7 @@ def svcomp_frontend(input_file, args):
   svcomp_process_file(args, name, ext)
 
   args.clang_options += " -fbracket-depth=2048"
-  args.clang_options += " -Wunknown-attributes"
+  args.clang_options += " -Wno-unknown-attributes"
   args.clang_options += " -DSVCOMP"
   args.clang_options += " -DAVOID_NAME_CONFLICTS"
   args.clang_options += " -DCUSTOM_VERIFIER_ASSERT"
@@ -239,7 +239,8 @@ def verify_bpl_svcomp(args):
   else:
     corral_command += ["/k:1"]
     if not (args.memory_safety or args.bit_precise):
-      corral_command += ["/di"]
+      if not ("dll_create" in csource or "sll_create" in csource):
+        corral_command += ["/di"]
 
   # we are not modeling strcpy
   if args.pthread and "strcpy" in bpl:

From 91c26a45889cea4c814eafc55f90eed120f82f53 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sat, 27 Oct 2018 02:30:05 -0600
Subject: [PATCH 28/60] Added basic logging to overflow checking

---
 lib/smack/IntegerOverflowChecker.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/lib/smack/IntegerOverflowChecker.cpp b/lib/smack/IntegerOverflowChecker.cpp
index 284a58514..ae53c6d80 100644
--- a/lib/smack/IntegerOverflowChecker.cpp
+++ b/lib/smack/IntegerOverflowChecker.cpp
@@ -7,6 +7,7 @@
 // operations, and optionally allows for the checking of overflow.
 //
 
+#define DEBUG_TYPE "smack-overflow"
 #include "smack/IntegerOverflowChecker.h"
 #include "smack/Naming.h"
 #include "llvm/IR/Module.h"
@@ -144,6 +145,8 @@ bool IntegerOverflowChecker::runOnModule(Module& m) {
             int bits = std::stoi(len);
             Value* eo1 = extendBitWidth(ci->getArgOperand(0), bits, isSigned, &*I);
             Value* eo2 = extendBitWidth(ci->getArgOperand(1), bits, isSigned, &*I);
+            DEBUG(errs() << "Processing operator: " << op << "\n");
+            assert(INSTRUCTION_TABLE.count(op) != 0 && "Operator must be present in our instruction table.");
             BinaryOperator* ai = BinaryOperator::Create(INSTRUCTION_TABLE.at(op), eo1, eo2, "", &*I);
             if (auto pei = dyn_cast_or_null<ExtractValueInst>(prev)) {
               if (ci == dyn_cast<CallInst>(pei->getAggregateOperand())) {

From 7e6904caa22b67caea8d583e8c798adead9d4d30 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sat, 27 Oct 2018 09:58:43 -0600
Subject: [PATCH 29/60] Fixed a bug in integer overflow pass

It is remarkable that the original code actually worked most of
the time :).
---
 lib/smack/IntegerOverflowChecker.cpp | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/lib/smack/IntegerOverflowChecker.cpp b/lib/smack/IntegerOverflowChecker.cpp
index ae53c6d80..2551cf19d 100644
--- a/lib/smack/IntegerOverflowChecker.cpp
+++ b/lib/smack/IntegerOverflowChecker.cpp
@@ -122,8 +122,8 @@ bool IntegerOverflowChecker::runOnModule(Module& m) {
       if (auto ei = dyn_cast<ExtractValueInst>(&*I)) {
         if (auto ci = dyn_cast<CallInst>(ei->getAggregateOperand())) {
           Function* f = ci->getCalledFunction();
-          SmallVectorImpl<StringRef> *info = new SmallVector<StringRef, 3>;
-          if (f && f->hasName() && OVERFLOW_INTRINSICS.match(f->getName().str(), info)
+          SmallVector<StringRef, 4> info;
+          if (f && f->hasName() && OVERFLOW_INTRINSICS.match(f->getName(), &info)
               && ei->getIndices()[0] == 1) {
             /*
              * If ei is an ExtractValueInst whose value flows from an LLVM
@@ -138,16 +138,17 @@ bool IntegerOverflowChecker::runOnModule(Module& m) {
              * - Finally, an assumption about the value of the flag is created
              *   to block erroneous checking of paths after the overflow check.
              */
-            Instruction* prev = &*std::prev(I);
-            bool isSigned = info->begin()[1].str() == "s";
-            std::string op = info->begin()[2].str();
-            std::string len = info->begin()[3].str();
-            int bits = std::stoi(len);
+            DEBUG(errs() << "Processing intrinsic: " << f->getName().str() << "\n");
+            assert(info.size() == 4 && "Must capture three matched strings.");
+            bool isSigned = (info[1] == "s");
+            std::string op = info[2];
+            int bits = std::stoi(info[3]);
             Value* eo1 = extendBitWidth(ci->getArgOperand(0), bits, isSigned, &*I);
             Value* eo2 = extendBitWidth(ci->getArgOperand(1), bits, isSigned, &*I);
             DEBUG(errs() << "Processing operator: " << op << "\n");
             assert(INSTRUCTION_TABLE.count(op) != 0 && "Operator must be present in our instruction table.");
             BinaryOperator* ai = BinaryOperator::Create(INSTRUCTION_TABLE.at(op), eo1, eo2, "", &*I);
+            Instruction* prev = &*std::prev(I);
             if (auto pei = dyn_cast_or_null<ExtractValueInst>(prev)) {
               if (ci == dyn_cast<CallInst>(pei->getAggregateOperand())) {
                 Value* r = createResult(ai, bits, &*I);

From c5d045c648b6c5e9245ba46b7b7a49901ef36f42 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Mon, 29 Oct 2018 15:02:58 -0600
Subject: [PATCH 30/60] Crude hack that implements the new SVCOMP memcleanup
 property

This is an ugly ugly hack, but it seems to work. SVCOMP scripts
are getting to be pretty horrible, and we should rewrite them
at some point.
---
 share/smack/svcomp/utils.py | 25 +++++++++++++++++++------
 1 file changed, 19 insertions(+), 6 deletions(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index dc259e9a8..1938a77cf 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -25,7 +25,7 @@ def svcomp_frontend(input_file, args):
   svcomp_check_property(args)
 
   # fix: disable float filter for memory safety benchmarks
-  if not args.memory_safety:
+  if not (args.memory_safety or args.only_check_memcleanup):
     # test bv and executable benchmarks
     file_type, executable = filters.svcomp_filter(args.input_files[0])
     if file_type == 'bitvector':
@@ -64,19 +64,24 @@ def svcomp_frontend(input_file, args):
     args.clang_options += " -x c"
 
   bc = smack.frontend.clang_frontend(args.input_files[0], args)
-
   # run with no extra smack libraries
   libs = set()
 
   smack.top.link_bc_files([bc],libs,args)
+  if args.only_check_memcleanup:
+    args.memory_safety = False
 
 def svcomp_check_property(args):
+  args.only_check_memcleanup = False
   # Check if property is vanilla reachability, and return unknown otherwise
   if args.svcomp_property:
     with open(args.svcomp_property, "r") as f:
       prop = f.read()
     if "valid-deref" in prop:
       args.memory_safety = True
+    elif "valid-memcleanup" in prop:
+      args.memory_safety = True
+      args.only_check_memcleanup = True
     elif "overflow" in prop:
       args.integer_overflow = True
     elif not "__VERIFIER_error" in prop:
@@ -182,6 +187,11 @@ def verify_bpl_svcomp(args):
       args.bpl_file = smack.top.temporary_file(os.path.splitext(os.path.basename(args.bpl_file))[0], '.bpl', args)
       copyfile(args.bpl_with_all_props, args.bpl_file)
       smack.top.property_selection(args)
+  elif args.only_check_memcleanup:
+    heurTrace = "engage memcleanup checks.\n"
+    args.only_check_memleak = True
+    smack.top.property_selection(args)
+    args.only_check_memleak = False
 
   # invoke boogie for floats
   # I have to copy/paste part of verify_bpl
@@ -238,8 +248,8 @@ def verify_bpl_svcomp(args):
       corral_command += ["/cooperative"]
   else:
     corral_command += ["/k:1"]
-    if not (args.memory_safety or args.bit_precise):
-      if not ("dll_create" in csource or "sll_create" in csource):
+    if not (args.memory_safety or args.bit_precise or args.only_check_memcleanup):
+      if not ("dll_create" in csource or "sll_create" in csource or "changeMethaneLevel" in csource):
         corral_command += ["/di"]
 
   # we are not modeling strcpy
@@ -448,11 +458,14 @@ def verify_bpl_svcomp(args):
     verify_bpl_svcomp(args)
   else:
     write_error_file(args, result, verifier_output)
-    sys.exit(smack.top.results(args)[result])
+    if args.only_check_memcleanup and result == 'invalid-memtrack':
+      sys.exit('SMACK found an error: memory cleanup.')
+    else:
+      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':
+  if args.memory_safety or args.only_check_memcleanup or status == 'timeout' or status == 'unknown':
     return
   hasBug = (status != 'verified')
   #if not hasBug:

From 72e28267d0f94820a12d4097aee2376adc8d23cc Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Mon, 29 Oct 2018 15:21:44 -0600
Subject: [PATCH 31/60] Adjusted heuristics for recognizing float SVCOMP
 benchmarks

---
 share/smack/svcomp/filters.py | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/share/smack/svcomp/filters.py b/share/smack/svcomp/filters.py
index a018b0b1d..bba8548d3 100644
--- a/share/smack/svcomp/filters.py
+++ b/share/smack/svcomp/filters.py
@@ -49,7 +49,9 @@ def svcomp_filter(f):
 def bv_filter(lines, raw_line_count, pruned_line_count):
   if ("bugBrokenOut" in lines or "returnsStructure" in lines or "__VERIFIER_nondet_double" in lines or
       "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines or
-      "huge_floor" in lines or "huge_ceil" in lines or "tiny_sqrt" in lines or "fmax_float" in lines):
+      "huge_floor" in lines or "huge_ceil" in lines or "tiny_sqrt" in lines or "fmax_float" in lines or
+      "fabs_double" in lines or "round_double" in lines or "trunc_double" in lines or "zero_log" in lines or
+      "isinf_float" in lines or "trunc_float" in lines):
     return 0
   elif ('4294967294u' in lines or '616783' in lines):
     return 1
@@ -97,7 +99,9 @@ def float_filter(lines, raw_line_count, pruned_line_count):
 
   if ("bugBrokenOut" in lines or "returnsStructure" in lines or "__VERIFIER_nondet_double" in lines or
       "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines or
-      "huge_floor" in lines or "huge_ceil" in lines or "tiny_sqrt" in lines or "fmax_float" in lines):
+      "huge_floor" in lines or "huge_ceil" in lines or "tiny_sqrt" in lines or "fmax_float" in lines or
+      "fabs_double" in lines or "round_double" in lines or "trunc_double" in lines or "zero_log" in lines or
+      "isinf_float" in lines or "trunc_float" in lines):
     return 1
 
   #heuristic #-1: don't do test on too large programs

From 1b4167042fe02b2875d9761c2e2ca3a9a49fd709 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Mon, 29 Oct 2018 15:38:36 -0600
Subject: [PATCH 32/60] Updated semantics of __VERIFIER_error when memory
 safety is on

According to the SVCOMP rules, __VERIFIER_error aborts, which
means we have to check for memory leaks here.
---
 share/smack/lib/smack.c | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c
index ad8eec7a7..9df069a5d 100644
--- a/share/smack/lib/smack.c
+++ b/share/smack/lib/smack.c
@@ -46,6 +46,9 @@ void __VERIFIER_assert(int x) {
 void __VERIFIER_error(void) {
 #if !MEMORY_SAFETY && !SIGNED_INTEGER_OVERFLOW_CHECK
   __SMACK_code("assert false;");
+#elif MEMORY_SAFETY
+  __SMACK_code("assert {:valid_memtrack} $allocatedCounter == 0;");
+  __SMACK_code("assume false;");
 #else
   __SMACK_code("assume false;");
 #endif

From 298e838ff0e15803df67bd40c80eedd81dc0441b Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Tue, 30 Oct 2018 03:30:50 -0600
Subject: [PATCH 33/60] Fixed a bug in overflow checking

I introduced a bug when I moved retrieval of prev instruction
several statements down in the code. That in turn caused for a
wrong prev instruction to be captured since some of the function
calls I jumped over in fact update the iterator!
---
 lib/smack/IntegerOverflowChecker.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/smack/IntegerOverflowChecker.cpp b/lib/smack/IntegerOverflowChecker.cpp
index 2551cf19d..4f658ae24 100644
--- a/lib/smack/IntegerOverflowChecker.cpp
+++ b/lib/smack/IntegerOverflowChecker.cpp
@@ -143,12 +143,12 @@ bool IntegerOverflowChecker::runOnModule(Module& m) {
             bool isSigned = (info[1] == "s");
             std::string op = info[2];
             int bits = std::stoi(info[3]);
+            Instruction* prev = &*std::prev(I);
             Value* eo1 = extendBitWidth(ci->getArgOperand(0), bits, isSigned, &*I);
             Value* eo2 = extendBitWidth(ci->getArgOperand(1), bits, isSigned, &*I);
             DEBUG(errs() << "Processing operator: " << op << "\n");
             assert(INSTRUCTION_TABLE.count(op) != 0 && "Operator must be present in our instruction table.");
             BinaryOperator* ai = BinaryOperator::Create(INSTRUCTION_TABLE.at(op), eo1, eo2, "", &*I);
-            Instruction* prev = &*std::prev(I);
             if (auto pei = dyn_cast_or_null<ExtractValueInst>(prev)) {
               if (ci == dyn_cast<CallInst>(pei->getAggregateOperand())) {
                 Value* r = createResult(ai, bits, &*I);

From 9f192fd577c51aa7d2e73d983427df9140dafbec Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Wed, 31 Oct 2018 05:03:53 -0600
Subject: [PATCH 34/60] Dealing with stack-based memory safety SVCOMP
 benchmarks

---
 share/smack/svcomp/utils.py | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 1938a77cf..146a35900 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -138,6 +138,10 @@ def svcomp_process_file(args, name, ext):
     with open(args.input_files[0], 'w') as fo:
       fo.write(s)
 
+def force_timeout():
+  sys.stdout.flush()
+  time.sleep(1000)
+
 def is_crappy_driver_benchmark(args, bpl):
   if ("205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--rtl8150.ko-entry_point_true-unreach-call" in bpl or
       "32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful" in bpl or
@@ -152,12 +156,14 @@ def is_crappy_driver_benchmark(args, bpl):
       "linux-4.2-rc1.tar.xz-43_2a-drivers--net--ppp--ppp_generic.ko-entry_point_true-unreach-call" in bpl):
     if not args.quiet:
       print("Stumbled upon a crappy device driver benchmark\n")
-    while (True):
-      pass
+    force_timeout()
 
-def force_timeout():
-  sys.stdout.flush()
-  time.sleep(1000)
+def is_stack_benchmark(args, csource):
+  if ("getNumbers" in csource or "areNatural" in csource or "myPointerA" in csource or "if(i == 0) {" in csource or
+      "arr[194]" in csource or "if(1)" in csource or "alloca(10" in csource or "p[0] = 2;" in csource):
+    if not args.quiet:
+      print("Stumbled upon a stack-based memory safety benchmark\n")
+    sys.exit(smack.top.results(args)['unknown'])
 
 def verify_bpl_svcomp(args):
   """Verify the Boogie source file using SVCOMP-tuned heuristics."""
@@ -236,6 +242,9 @@ def verify_bpl_svcomp(args):
   with open(args.input_files[0], "r") as f:
     csource = f.read()
 
+  if args.memory_safety:
+    is_stack_benchmark(args, csource)
+
   is_crappy_driver_benchmark(args, bpl)
 
   if args.pthread:
@@ -436,8 +445,7 @@ def verify_bpl_svcomp(args):
             sys.exit(smack.top.results(args)[args.valid_deref_check_result])
         verify_bpl_svcomp(args)
       else:
-        # Sleep for 1000 seconds, so svcomp shows timeout instead of unknown
-        time.sleep(1000)
+        force_timeout()
   elif result == 'verified': #normal inlining
     heurTrace += "Normal inlining terminated and found no bugs.\n"
   else: #normal inlining

From ac20a9049cee646af799ffb7739923a97630cf4c Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Wed, 31 Oct 2018 05:21:44 -0600
Subject: [PATCH 35/60] Increased context switch bound for several more SVCOMP
 benchmarks

---
 share/smack/svcomp/utils.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 146a35900..b13ebbe6f 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -248,7 +248,7 @@ def verify_bpl_svcomp(args):
   is_crappy_driver_benchmark(args, bpl)
 
   if args.pthread:
-    if "fib_bench" in bpl or "27_Boop_simple_vf_false-unreach-call" in bpl:
+    if "fib_bench" in bpl or "27_Boop_simple_vf_false-unreach-call" in bpl or "k < 5;" in csource or "k < 10;" in csource or "k < 20;" in csource:
       heurTrace += "Increasing context switch bound for certain pthread benchmarks.\n"
       corral_command += ["/k:30"]
     else:

From 172e94a036872944593133db026d234c820e387b Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 1 Nov 2018 02:15:02 -0600
Subject: [PATCH 36/60] Not handling left shift overflow SVCOMP benchmarks yet

---
 share/smack/svcomp/utils.py | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index b13ebbe6f..68f8641ff 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -244,8 +244,12 @@ def verify_bpl_svcomp(args):
 
   if args.memory_safety:
     is_stack_benchmark(args, csource)
-
-  is_crappy_driver_benchmark(args, bpl)
+  elif args.integer_overflow and "mp_add(" in csource:
+    if not args.quiet:
+      print("Stumbled upon a left-shift-based overflow benchmark\n")
+    sys.exit(smack.top.results(args)['unknown'])
+  else:
+    is_crappy_driver_benchmark(args, bpl)
 
   if args.pthread:
     if "fib_bench" in bpl or "27_Boop_simple_vf_false-unreach-call" in bpl or "k < 5;" in csource or "k < 10;" in csource or "k < 20;" in csource:
@@ -318,7 +322,8 @@ def verify_bpl_svcomp(args):
   elif args.integer_overflow and ("jain" in bpl or "TerminatorRec02" in bpl or "NonTerminationSimple" in bpl):
     heurTrace += "Infinite loop in overflow benchmark. Setting loop unroll bar to INT_MAX.\n"
     loopUnrollBar = 2**31 - 1
-  elif args.integer_overflow and ("(x != 0)" in csource or "(z > 0)" in csource or "(max > 0)" in csource or "(k < N)" in csource or "partial_sum" in csource):
+  elif args.integer_overflow and ("(x != 0)" in csource or "(z > 0)" in csource or "(max > 0)" in csource or
+                                  "(k < N)" in csource or "partial_sum" in csource):
     heurTrace += "Large overflow benchmark. Setting loop unroll bar to INT_MAX.\n"
     loopUnrollBar = 2**31 - 1
   elif "i>>16" in csource:

From e55a2e78d1125ca86635c282e6f107b051c8db03 Mon Sep 17 00:00:00 2001
From: Mark Stanislaw Baranowski <mark.s.baranowski@gmail.com>
Date: Thu, 1 Nov 2018 14:37:54 -0700
Subject: [PATCH 37/60] Add checking for left-shift overflow for C programs.
 Fixes #382.

---
 include/smack/IntegerOverflowChecker.h |  4 ++--
 lib/smack/IntegerOverflowChecker.cpp   | 20 ++++++++++++++++++--
 share/smack/frontend.py                |  2 +-
 test/bits/left_shift_negative_fail.c   | 11 +++++++++++
 test/bits/left_shift_overflow.c        | 12 ++++++++++++
 test/bits/left_shift_overflow_fail.c   | 12 ++++++++++++
 test/bits/left_shift_unsigned.c        | 12 ++++++++++++
 test/bits/left_shift_unsigned_fail.c   | 12 ++++++++++++
 8 files changed, 80 insertions(+), 5 deletions(-)
 create mode 100644 test/bits/left_shift_negative_fail.c
 create mode 100644 test/bits/left_shift_overflow.c
 create mode 100644 test/bits/left_shift_overflow_fail.c
 create mode 100644 test/bits/left_shift_unsigned.c
 create mode 100644 test/bits/left_shift_unsigned_fail.c

diff --git a/include/smack/IntegerOverflowChecker.h b/include/smack/IntegerOverflowChecker.h
index 2fd095e25..6fe8dc3e8 100644
--- a/include/smack/IntegerOverflowChecker.h
+++ b/include/smack/IntegerOverflowChecker.h
@@ -24,8 +24,8 @@ class IntegerOverflowChecker: public llvm::ModulePass {
   llvm::Value* extendBitWidth(llvm::Value* v, int bits, bool isSigned, llvm::Instruction* i);
   llvm::BinaryOperator* createFlag(llvm::Value* v, int bits, bool isSigned, llvm::Instruction* i);
   llvm::Value* createResult(llvm::Value* v, int bits, llvm::Instruction* i);
-  void addCheck(llvm::Function* co, llvm::BinaryOperator* flag, llvm::Instruction* i);
-  void addBlockingAssume(llvm::Function* va, llvm::BinaryOperator* flag, llvm::Instruction* i);
+  void addCheck(llvm::Function* co, llvm::Value* flag, llvm::Instruction* i);
+  void addBlockingAssume(llvm::Function* va, llvm::Value* flag, llvm::Instruction* i);
 };
 }
 
diff --git a/lib/smack/IntegerOverflowChecker.cpp b/lib/smack/IntegerOverflowChecker.cpp
index 4f658ae24..e4b57bc58 100644
--- a/lib/smack/IntegerOverflowChecker.cpp
+++ b/lib/smack/IntegerOverflowChecker.cpp
@@ -94,7 +94,7 @@ Value* IntegerOverflowChecker::createResult(Value* v, int bits, Instruction* i)
  * This adds a call instruction to __SMACK_check_overflow to determine if an
  * overflow occured as indicated by flag.
  */
-void IntegerOverflowChecker::addCheck(Function* co, BinaryOperator* flag, Instruction* i) {
+void IntegerOverflowChecker::addCheck(Function* co, Value* flag, Instruction* i) {
   ArrayRef<Value*> args(CastInst::CreateIntegerCast(flag, co->arg_begin()->getType(), false, "", i));
   CallInst::Create(co, args, "", i);
 }
@@ -103,7 +103,7 @@ void IntegerOverflowChecker::addCheck(Function* co, BinaryOperator* flag, Instru
  * This inserts a call to assume with flag negated to prevent the verifier
  * from exploring paths past a __SMACK_check_overflow
  */
-void IntegerOverflowChecker::addBlockingAssume(Function* va, BinaryOperator* flag, Instruction* i) {
+void IntegerOverflowChecker::addBlockingAssume(Function* va, Value* flag, Instruction* i) {
   ArrayRef<Value*> args(CastInst::CreateIntegerCast(BinaryOperator::CreateNot(flag, "", i),
         va->arg_begin()->getType(), false, "", i));
   CallInst::Create(va, args, "", i);
@@ -119,6 +119,22 @@ bool IntegerOverflowChecker::runOnModule(Module& m) {
     if (Naming::isSmackName(F.getName()))
       continue;
     for (inst_iterator I = inst_begin(F), E = inst_end(F); I != E; ++I) {
+      // Add check for UBSan left shift
+      if (auto chkshft = dyn_cast<CallInst>(&*I)) {
+	Function* chkfn = chkshft->getCalledFunction();
+        if (chkfn!= nullptr &&
+            chkfn->hasName() &&
+            chkfn->getName().find("__ubsan_handle_shift_out_of_bounds") != std::string::npos &&
+            SmackOptions::IntegerOverflow) {
+          // If the call to __ubsan_handle_shift_out_of_bounds is reachable,
+          // then an overflow is possible.
+          ConstantInt* flag = ConstantInt::getTrue(chkshft->getFunction()->getContext());
+          addCheck(co, flag, &*I);
+          addBlockingAssume(va, flag, &*I);
+          I->replaceAllUsesWith(flag);
+          instToRemove.push_back(&*I);
+        }
+      }
       if (auto ei = dyn_cast<ExtractValueInst>(&*I)) {
         if (auto ci = dyn_cast<CallInst>(ei->getAggregateOperand())) {
           Function* f = ci->getCalledFunction();
diff --git a/share/smack/frontend.py b/share/smack/frontend.py
index 0c3357132..429907a04 100644
--- a/share/smack/frontend.py
+++ b/share/smack/frontend.py
@@ -72,7 +72,7 @@ def default_clang_compile_command(args, lib = False):
   cmd += args.clang_options.split()
   cmd += ['-DMEMORY_MODEL_' + args.mem_mod.upper().replace('-','_')]
   if args.memory_safety: cmd += ['-DMEMORY_SAFETY']
-  if args.integer_overflow: cmd += (['-ftrapv'] if not lib else ['-DSIGNED_INTEGER_OVERFLOW_CHECK'])
+  if args.integer_overflow: cmd += (['-ftrapv', '-fsanitize=shift'] if not lib else ['-DSIGNED_INTEGER_OVERFLOW_CHECK'])
   if args.float: cmd += ['-DFLOAT_ENABLED']
   if sys.stdout.isatty(): cmd += ['-fcolor-diagnostics']
   return cmd
diff --git a/test/bits/left_shift_negative_fail.c b/test/bits/left_shift_negative_fail.c
new file mode 100644
index 000000000..106963140
--- /dev/null
+++ b/test/bits/left_shift_negative_fail.c
@@ -0,0 +1,11 @@
+#include "smack.h"
+
+// @expect error
+// @flag --integer-overflow
+
+int main(void) {
+  int x = __VERIFIER_nondet_int();
+  int z = 0;
+  assume(x < 0);
+  return x << z;
+}
diff --git a/test/bits/left_shift_overflow.c b/test/bits/left_shift_overflow.c
new file mode 100644
index 000000000..62042b03b
--- /dev/null
+++ b/test/bits/left_shift_overflow.c
@@ -0,0 +1,12 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --integer-overflow
+
+int main(void) {
+  int x = __VERIFIER_nondet_int();
+  int z = __VERIFIER_nondet_int();
+  assume(x < 1024 && x >= 0);
+  assume(0 <= z && z <= 21);
+  return x << z;
+}
diff --git a/test/bits/left_shift_overflow_fail.c b/test/bits/left_shift_overflow_fail.c
new file mode 100644
index 000000000..656780a66
--- /dev/null
+++ b/test/bits/left_shift_overflow_fail.c
@@ -0,0 +1,12 @@
+#include "smack.h"
+
+// @expect error
+// @flag --integer-overflow
+
+int main(void) {
+  int x = __VERIFIER_nondet_int();
+  int z = __VERIFIER_nondet_int();
+  assume(x >= 1024);
+  assume(0 <= z && z <= 21);
+  return x << z;
+}
diff --git a/test/bits/left_shift_unsigned.c b/test/bits/left_shift_unsigned.c
new file mode 100644
index 000000000..e3edc1a17
--- /dev/null
+++ b/test/bits/left_shift_unsigned.c
@@ -0,0 +1,12 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --integer-overflow
+
+int main(void) {
+  unsigned int x = __VERIFIER_nondet_unsigned_int();
+  unsigned int z = __VERIFIER_nondet_unsigned_int();
+
+  assume(z < sizeof(x)*8);
+  return x << z;
+}
diff --git a/test/bits/left_shift_unsigned_fail.c b/test/bits/left_shift_unsigned_fail.c
new file mode 100644
index 000000000..ec7316e04
--- /dev/null
+++ b/test/bits/left_shift_unsigned_fail.c
@@ -0,0 +1,12 @@
+#include "smack.h"
+
+// @expect error
+// @flag --integer-overflow
+
+int main(void) {
+  unsigned int x = __VERIFIER_nondet_unsigned_int();
+  unsigned int z = __VERIFIER_nondet_unsigned_int();
+
+  assume(z >= sizeof(x)*8);
+  return x << z;
+}

From f9dcc92f3f42b533465f2c6b89bb95ffd46f8453 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Fri, 2 Nov 2018 07:07:58 -0600
Subject: [PATCH 38/60] Minor fixes to integer overflow checking

---
 lib/smack/IntegerOverflowChecker.cpp | 32 ++++++++++++++--------------
 share/smack/svcomp/utils.py          |  4 ----
 2 files changed, 16 insertions(+), 20 deletions(-)

diff --git a/lib/smack/IntegerOverflowChecker.cpp b/lib/smack/IntegerOverflowChecker.cpp
index e4b57bc58..cd442c9ad 100644
--- a/lib/smack/IntegerOverflowChecker.cpp
+++ b/lib/smack/IntegerOverflowChecker.cpp
@@ -119,28 +119,28 @@ bool IntegerOverflowChecker::runOnModule(Module& m) {
     if (Naming::isSmackName(F.getName()))
       continue;
     for (inst_iterator I = inst_begin(F), E = inst_end(F); I != E; ++I) {
-      // Add check for UBSan left shift
-      if (auto chkshft = dyn_cast<CallInst>(&*I)) {
-	Function* chkfn = chkshft->getCalledFunction();
-        if (chkfn!= nullptr &&
-            chkfn->hasName() &&
-            chkfn->getName().find("__ubsan_handle_shift_out_of_bounds") != std::string::npos &&
-            SmackOptions::IntegerOverflow) {
-          // If the call to __ubsan_handle_shift_out_of_bounds is reachable,
-          // then an overflow is possible.
-          ConstantInt* flag = ConstantInt::getTrue(chkshft->getFunction()->getContext());
-          addCheck(co, flag, &*I);
-          addBlockingAssume(va, flag, &*I);
-          I->replaceAllUsesWith(flag);
-          instToRemove.push_back(&*I);
+      // Add check for UBSan left shift when needed
+      if (SmackOptions::IntegerOverflow) {
+        if (auto chkshft = dyn_cast<CallInst>(&*I)) {
+	  Function* chkfn = chkshft->getCalledFunction();
+          if (chkfn && chkfn->hasName() &&
+              chkfn->getName().find("__ubsan_handle_shift_out_of_bounds") != std::string::npos) {
+            // If the call to __ubsan_handle_shift_out_of_bounds is reachable,
+            // then an overflow is possible.
+            ConstantInt* flag = ConstantInt::getTrue(chkshft->getFunction()->getContext());
+            addCheck(co, flag, &*I);
+            addBlockingAssume(va, flag, &*I);
+            I->replaceAllUsesWith(flag);
+            instToRemove.push_back(&*I);
+          }
         }
       }
       if (auto ei = dyn_cast<ExtractValueInst>(&*I)) {
         if (auto ci = dyn_cast<CallInst>(ei->getAggregateOperand())) {
           Function* f = ci->getCalledFunction();
           SmallVector<StringRef, 4> info;
-          if (f && f->hasName() && OVERFLOW_INTRINSICS.match(f->getName(), &info)
-              && ei->getIndices()[0] == 1) {
+          if (f && f->hasName() && OVERFLOW_INTRINSICS.match(f->getName(), &info) &&
+              ei->getIndices()[0] == 1) {
             /*
              * If ei is an ExtractValueInst whose value flows from an LLVM
              * checked value intrinsic f, then we do the following:
diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 68f8641ff..9318143ac 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -244,10 +244,6 @@ def verify_bpl_svcomp(args):
 
   if args.memory_safety:
     is_stack_benchmark(args, csource)
-  elif args.integer_overflow and "mp_add(" in csource:
-    if not args.quiet:
-      print("Stumbled upon a left-shift-based overflow benchmark\n")
-    sys.exit(smack.top.results(args)['unknown'])
   else:
     is_crappy_driver_benchmark(args, bpl)
 

From 3b47a40526a9a4ffc52190001a0e9a4065da7f23 Mon Sep 17 00:00:00 2001
From: Jack J Garzella <jjgarzella@gmail.com>
Date: Tue, 30 Oct 2018 12:54:21 -0600
Subject: [PATCH 39/60] Fix D support by adding custom compile_to_bc

The D compiler is not flag-compatible with clang
---
 share/smack/frontend.py | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/share/smack/frontend.py b/share/smack/frontend.py
index 429907a04..c959467d2 100644
--- a/share/smack/frontend.py
+++ b/share/smack/frontend.py
@@ -83,6 +83,12 @@ def compile_to_bc(input_file, compile_command, args):
   try_command(compile_command + ['-o', bc, input_file], console=True)
   return bc
 
+def d_compile_to_bc(input_file, compile_command, args):
+  """Compile a D source file to LLVM IR."""
+  bc = temporary_file(os.path.splitext(os.path.basename(input_file))[0], '.bc', args)
+  try_command(compile_command + ['-of=' + bc, input_file], console=True)
+  return bc
+
 def fortran_compile_to_bc(input_file, compile_command, args):
   """Compile a FORTRAN source file to LLVM IR."""
 
@@ -148,7 +154,7 @@ def d_frontend(input_file, args):
   compile_command = ['ldc2', '-output-ll']
   compile_command += map(lambda path: '-I=' + path, smack_headers(args))
   args.entry_points += ['_Dmain']
-  return compile_to_bc(input_file,compile_command,args)
+  return d_compile_to_bc(input_file,compile_command,args)
 
 def fortran_frontend(input_file, args):
   """Generate Boogie code from Fortran language source(s)."""

From 94fdde6e0568bbad169746377c8425c293a2472f Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Fri, 2 Nov 2018 10:11:46 -0600
Subject: [PATCH 40/60] Turn on bitvectors for BusyBox overflows

---
 share/smack/svcomp/filters.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/share/smack/svcomp/filters.py b/share/smack/svcomp/filters.py
index bba8548d3..34ee0fe07 100644
--- a/share/smack/svcomp/filters.py
+++ b/share/smack/svcomp/filters.py
@@ -53,7 +53,7 @@ def bv_filter(lines, raw_line_count, pruned_line_count):
       "fabs_double" in lines or "round_double" in lines or "trunc_double" in lines or "zero_log" in lines or
       "isinf_float" in lines or "trunc_float" in lines):
     return 0
-  elif ('4294967294u' in lines or '616783' in lines):
+  elif ('4294967294u' in lines or '616783' in lines or '__main(argc' in lines):
     return 1
 
   if raw_line_count > 1500:

From 63fcba384e64e811bebd039ad950c5f7dcc8b52e Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sun, 4 Nov 2018 00:42:33 -0600
Subject: [PATCH 41/60] Turn on bit-vectors for ddv memory safety benchmarks

---
 share/smack/svcomp/utils.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 9318143ac..bcdbb85e3 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -43,7 +43,7 @@ def svcomp_frontend(input_file, args):
   else:
     with open(input_file, "r") as sf:
       sc = sf.read()
-    if 'unsigned char b:2' in sc or "4294967294u" in sc:
+    if 'unsigned char b:2' in sc or "4294967294u" in sc or "_ddv_module_init" in sc:
       args.bit_precise = True
       #args.bit_precise_pointers = True
 

From 9dba4bdeb6832b2b62b9a2cfb47837c3ea0b6fa3 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Mon, 5 Nov 2018 04:13:15 -0700
Subject: [PATCH 42/60] Fixed a bug in galloc generation

The code that generates galloc invocation statements did not take
care of the case when bit-precise-pointers option is turned on.
This is now fixed.
---
 lib/smack/SmackRep.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp
index d0913e2af..d9d69ad48 100644
--- a/lib/smack/SmackRep.cpp
+++ b/lib/smack/SmackRep.cpp
@@ -1080,7 +1080,7 @@ std::string SmackRep::getPrelude() {
     s << "// Global allocations" << "\n";
     std::list<const Stmt*> stmts;
     for (auto E : globalAllocations)
-      stmts.push_back(Stmt::call("$galloc", {expr(E.first), Expr::lit(E.second)}));
+      stmts.push_back(Stmt::call("$galloc", {expr(E.first), pointerLit(E.second)}));
     s << Decl::procedure("$global_allocations", {}, {}, {}, {Block::block("",stmts)}) << "\n";
     s << "\n";
   }

From ceff80e2f86a6615741f885ad68c41f2be0d369d Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Mon, 5 Nov 2018 04:16:25 -0700
Subject: [PATCH 43/60] Enabling bit-vectors for SVCOMP busybox benchmarks with
 mem safety

---
 share/smack/svcomp/utils.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index bcdbb85e3..8cb77a231 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -43,7 +43,7 @@ def svcomp_frontend(input_file, args):
   else:
     with open(input_file, "r") as sf:
       sc = sf.read()
-    if 'unsigned char b:2' in sc or "4294967294u" in sc or "_ddv_module_init" in sc:
+    if 'unsigned char b:2' in sc or "4294967294u" in sc or "_ddv_module_init" in sc or "bb_process_escape_sequence" in sc:
       args.bit_precise = True
       #args.bit_precise_pointers = True
 

From 267682eb60ca2913f6ec2fd66efa53465e1b05d8 Mon Sep 17 00:00:00 2001
From: "Mark S. Baranowski" <mark.s.baranowski@gmail.com>
Date: Tue, 6 Nov 2018 16:35:41 -0700
Subject: [PATCH 44/60] Fix rust entry point

---
 include/smack/Naming.h           |  5 +++++
 lib/smack/Naming.cpp             |  5 +++++
 lib/smack/SmackInstGenerator.cpp | 15 ++++++++++++++-
 3 files changed, 24 insertions(+), 1 deletion(-)

diff --git a/include/smack/Naming.h b/include/smack/Naming.h
index 17c1d4fbc..65f1ccf01 100644
--- a/include/smack/Naming.h
+++ b/include/smack/Naming.h
@@ -91,6 +91,11 @@ class Naming {
   static const std::string MEMORY_SAFETY_FUNCTION;
   static const std::string MEMORY_LEAK_FUNCTION;
 
+  static const std::string RUST_ENTRY;
+  static const std::string RUST_PANIC1;
+  static const std::string RUST_PANIC2;
+  static const std::string RUST_PANIC_ANNOTATION;
+
   static const std::map<unsigned,std::string> INSTRUCTION_TABLE;
   static const std::map<unsigned,std::string> CMPINST_TABLE;
   static const std::map<unsigned,std::string> ATOMICRMWINST_TABLE;
diff --git a/lib/smack/Naming.cpp b/lib/smack/Naming.cpp
index 645510fc0..657b49963 100644
--- a/lib/smack/Naming.cpp
+++ b/lib/smack/Naming.cpp
@@ -61,6 +61,11 @@ const std::string Naming::MEM_OP = "$mop";
 const std::string Naming::REC_MEM_OP = "boogie_si_record_mop";
 const std::string Naming::MEM_OP_VAL = "$MOP";
 
+const std::string Naming::RUST_ENTRY = "_ZN3std2rt10lang_start";
+const std::string Naming::RUST_PANIC1 = "_ZN4core9panicking5panic";
+const std::string Naming::RUST_PANIC2 = "_ZN3std9panicking11begin_panic";
+const std::string Naming::RUST_PANIC_ANNOTATION = "rust_panic";
+
 const std::string Naming::BLOCK_LBL = "$bb";
 const std::string Naming::RET_VAR = "$r";
 const std::string Naming::EXN_VAR = "$exn";
diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp
index ba672d087..a7049425f 100644
--- a/lib/smack/SmackInstGenerator.cpp
+++ b/lib/smack/SmackInstGenerator.cpp
@@ -599,7 +599,20 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) {
     // Semantically, this function simply returns the value v.
     Value* val = ci.getArgOperand(0);
     emit(Stmt::assign(rep->expr(&ci), rep->expr(val)));
-    
+
+    // Set the entry point for Rust programs
+  } else if (name.find(Naming::RUST_ENTRY) != std::string::npos) {
+    auto castExpr = ci.getArgOperand(0);
+    if (auto CE = dyn_cast<const Constant>(castExpr)) {
+      auto mainFunc = CE->getOperand(0);
+      emit(Stmt::call(mainFunc->getName(), {},{}));
+    }
+
+    // Convert Rust's panic functions into assertion violations
+  } else if (name.find(Naming::RUST_PANIC1) != std::string::npos
+             || name.find(Naming::RUST_PANIC2) != std::string::npos) {
+    emit(Stmt::assert_(Expr::lit(false), {Attr::attr(Naming::RUST_PANIC_ANNOTATION)}));
+
   } else if (name.find(Naming::VALUE_PROC) != std::string::npos) {
     emit(rep->valueAnnotation(ci));
 

From 6eb2bcf154d009759eea7ba3f17fceb35806e965 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 8 Nov 2018 12:16:21 -0700
Subject: [PATCH 45/60] Removing return and argument values from SVCOMP
 witnesses

Those contain `:` in Corral error traces.
---
 share/smack/svcomp/toSVCOMPformat.py | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/share/smack/svcomp/toSVCOMPformat.py b/share/smack/svcomp/toSVCOMPformat.py
index 6f5184375..8cc94e5ba 100644
--- a/share/smack/svcomp/toSVCOMPformat.py
+++ b/share/smack/svcomp/toSVCOMPformat.py
@@ -161,11 +161,13 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug):
         # Make sure it isn't a smack header file
         if not pat.match(jsonTrace["file"]):
           desc = jsonTrace["description"]
-          if formatAssign(jsonTrace["description"]):
+          formattedAssign = formatAssign(desc)
+          # Make sure it is not return value
+          if formattedAssign and not ":" in formattedAssign:
           # Create new node and edge
             newNode = addGraphNode(tree)
             attribs = {"startline":str(jsonTrace["line"])}
-            attribs["assumption"] = formatAssign(desc) + ";"
+            attribs["assumption"] = formattedAssign + ";"
             attribs["assumption.scope"] = callStack[-1]
             newEdge = addGraphEdge(tree, lastNode, newNode, attribs)
             prevLineNo = jsonTrace["line"]

From f118fca5b9e2b7ddfd8d3972498375370feb13a1 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 8 Nov 2018 12:31:15 -0700
Subject: [PATCH 46/60] Enabling witnesses for memory safety

---
 share/smack/svcomp/utils.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 8cb77a231..5b5ec86bd 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -474,7 +474,7 @@ def verify_bpl_svcomp(args):
 
 def write_error_file(args, status, verifier_output):
   #return
-  if args.memory_safety or args.only_check_memcleanup or status == 'timeout' or status == 'unknown':
+  if status == 'timeout' or status == 'unknown':
     return
   hasBug = (status != 'verified')
   #if not hasBug:

From acae4e1032816b17014449cdbc74cefc0e820f86 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sat, 10 Nov 2018 15:10:58 -0700
Subject: [PATCH 47/60] Minor fix to comments in Rust additions

---
 lib/smack/SmackInstGenerator.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp
index a7049425f..9011ad9db 100644
--- a/lib/smack/SmackInstGenerator.cpp
+++ b/lib/smack/SmackInstGenerator.cpp
@@ -600,17 +600,17 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) {
     Value* val = ci.getArgOperand(0);
     emit(Stmt::assign(rep->expr(&ci), rep->expr(val)));
 
-    // Set the entry point for Rust programs
   } else if (name.find(Naming::RUST_ENTRY) != std::string::npos) {
+    // Set the entry point for Rust programs
     auto castExpr = ci.getArgOperand(0);
     if (auto CE = dyn_cast<const Constant>(castExpr)) {
       auto mainFunc = CE->getOperand(0);
       emit(Stmt::call(mainFunc->getName(), {},{}));
     }
 
-    // Convert Rust's panic functions into assertion violations
   } else if (name.find(Naming::RUST_PANIC1) != std::string::npos
              || name.find(Naming::RUST_PANIC2) != std::string::npos) {
+    // Convert Rust's panic functions into assertion violations
     emit(Stmt::assert_(Expr::lit(false), {Attr::attr(Naming::RUST_PANIC_ANNOTATION)}));
 
   } else if (name.find(Naming::VALUE_PROC) != std::string::npos) {

From 4f871663365f1a717ab23fef43f38d5d4d3545d1 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Wed, 14 Nov 2018 03:53:04 -0700
Subject: [PATCH 48/60] Fixed and improved SVCOMP witness generation

Mainly I added support for generating a subset of possible
memory safety witnesses.
---
 share/smack/svcomp/toSVCOMPformat.py | 55 +++++++++++++++++++---------
 share/smack/svcomp/utils.py          |  2 +-
 2 files changed, 39 insertions(+), 18 deletions(-)

diff --git a/share/smack/svcomp/toSVCOMPformat.py b/share/smack/svcomp/toSVCOMPformat.py
index 8cc94e5ba..f03a5b4af 100644
--- a/share/smack/svcomp/toSVCOMPformat.py
+++ b/share/smack/svcomp/toSVCOMPformat.py
@@ -10,6 +10,7 @@
 import pprint
 import os
 import hashlib
+import datetime
 
 nextNum = 0
 
@@ -36,8 +37,8 @@ def addKeyDefs(root):
     keys.append(["specification", "string",  "graph", "specification", False])
     keys.append(["programfile", "string",  "graph", "programfile", False])
     keys.append(["programhash", "string",  "graph", "programhash", False])
-    keys.append(["MemoryModel", "string",  "graph", "memorymodel", False])
     keys.append(["architecture", "string",  "graph", "architecture", False])
+    keys.append(["creationtime", "string",  "graph", "creationtime", False])
     keys.append(["tokenSet",           "string",  "edge",  "tokens",         False])
     keys.append(["originTokenSet",     "string",  "edge",  "origintokens",   False])
     keys.append(["negativeCase",       "string",  "edge",  "negated",        True, "false"])
@@ -117,10 +118,10 @@ def buildEmptyXmlGraph(args, hasBug):
     programfile = os.path.abspath(args.orig_files[0])
     addKey(graph, "programfile", programfile)
     with open(programfile, 'r') as pgf:
-      addKey(graph, "programhash", hashlib.sha1(pgf.read()).hexdigest())
-    addKey(graph, "memorymodel", "precise")
+      addKey(graph, "programhash", hashlib.sha256(pgf.read()).hexdigest())
     addKey(graph, "architecture",
             re.search(r'-m(32|64)', args.clang_options).group(1) + 'bit')
+    addKey(graph, "creationtime", datetime.datetime.now().replace(microsecond=0).isoformat())
     return tree
 
 def formatAssign(assignStmt):
@@ -136,7 +137,7 @@ def formatAssign(assignStmt):
 def isSMACKInitFunc(funcName):
   return funcName == '$initialize' or funcName == '__SMACK_static_init' or funcName == '__SMACK_init_func_memory_model'
 
-def smackJsonToXmlGraph(strJsonOutput, args, hasBug):
+def smackJsonToXmlGraph(strJsonOutput, args, hasBug, status):
     """Converts output from SMACK (in the smackd json format) to a graphml
        format that conforms to the SVCOMP witness file format"""
     # Build tree & start node
@@ -183,20 +184,40 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug):
             if isSMACKInitFunc(calledFunc):
               continue
             callStack.append(calledFunc)
-            if (("__VERIFIER_error" in jsonTrace["description"][len("CALL"):]) or
-                ("__SMACK_overflow_false" in jsonTrace["description"][len("CALL"):]) or
-                 ("__SMACK_check_overflow" in jsonTrace["description"][len("CALL"):])):
-              newNode = addGraphNode(tree)
-              # addGraphNode returns a string, so we had to search the graph to get the node that we want
-              vNodes =tree.find("graph").findall("node")
-              for vNode in vNodes:
-                if vNode.attrib["id"] == newNode:
-                  addKey(vNode, "violation", "true")
-              attribs = {"startline":str(jsonTrace["line"])}
-              if not args.integer_overflow:
+            if args.only_check_memcleanup or status == 'invalid-memtrack':
+              if "__SMACK_check_memory_leak" in jsonTrace["description"][len("CALL"):]:
+                newNode = addGraphNode(tree)
+                # addGraphNode returns a string, so we had to search the graph to get the node that we want
+                vNodes =tree.find("graph").findall("node")
+                for vNode in vNodes:
+                  if vNode.attrib["id"] == newNode:
+                    addKey(vNode, "violation", "true")
+                attribs = {"startline":str(jsonTrace["line"])}
+                addGraphEdge(tree, lastNode, newNode, attribs)
+                break
+            elif args.integer_overflow:
+              if "__SMACK_check_overflow" in jsonTrace["description"][len("CALL"):]:
+                newNode = addGraphNode(tree)
+                # addGraphNode returns a string, so we had to search the graph to get the node that we want
+                vNodes =tree.find("graph").findall("node")
+                for vNode in vNodes:
+                  if vNode.attrib["id"] == newNode:
+                    addKey(vNode, "violation", "true")
+                attribs = {"startline":str(jsonTrace["line"])}
+                addGraphEdge(tree, lastNode, newNode, attribs)
+                break
+            else:
+              if "__VERIFIER_error" in jsonTrace["description"][len("CALL"):]:
+                newNode = addGraphNode(tree)
+                # addGraphNode returns a string, so we had to search the graph to get the node that we want
+                vNodes =tree.find("graph").findall("node")
+                for vNode in vNodes:
+                  if vNode.attrib["id"] == newNode:
+                    addKey(vNode, "violation", "true")
+                attribs = {"startline":str(jsonTrace["line"])}
                 attribs["enterFunction"] = callStack[-1]
-              addGraphEdge(tree, lastNode, newNode, attribs)
-              break
+                addGraphEdge(tree, lastNode, newNode, attribs)
+                break
           if "RETURN from" in desc:
             returnedFunc = str(desc[len("RETURN from "):]).strip()
             if returnedFunc.startswith("devirtbounce"):
diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 5b5ec86bd..eeaeebde5 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -482,7 +482,7 @@ def write_error_file(args, status, verifier_output):
   if args.error_file:
     error = None
     if args.language == 'svcomp':
-      error = smackJsonToXmlGraph(smack.top.smackdOutput(verifier_output), args, hasBug)
+      error = smackJsonToXmlGraph(smack.top.smackdOutput(verifier_output), args, hasBug, status)
     elif hasBug:
       error = smack.top.error_trace(verifier_output, args)
     if error is not None:

From 47bc23111db6151c0780cfa0584162b295ede34d Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Tue, 20 Nov 2018 06:34:15 -0700
Subject: [PATCH 49/60] Added more buggy SVCOMP driver benchmarks to our list

---
 share/smack/svcomp/utils.py | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index eeaeebde5..a388c2ea7 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -142,7 +142,7 @@ def force_timeout():
   sys.stdout.flush()
   time.sleep(1000)
 
-def is_crappy_driver_benchmark(args, bpl):
+def is_buggy_driver_benchmark(args, bpl):
   if ("205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--rtl8150.ko-entry_point_true-unreach-call" in bpl or
       "32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful" in bpl or
       "32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--media--dvb-core--dvb-core.ko-ldv_main5_sequence_infinite_withcheck_stateful" in bpl or
@@ -153,6 +153,10 @@ def is_crappy_driver_benchmark(args, bpl):
       "linux-4.2-rc1.tar.xz-32_7a-drivers--net--usb--r8152.ko-entry_point_true-unreach-call" in bpl or
       "linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-ethernet-smsc-smsc911x_true-unreach-call" in bpl or
       "linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call" in bpl or
+      "linux-4.2-rc1.tar.xz-32_7a-drivers--usb--gadget--libcomposite.ko-entry_point_true-unreach-call" in bpl or
+      "linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-platform-marvell-ccic-cafe_ccic_true-unreach-call" in bpl or
+      "linux-4.0-rc1---drivers--media--usb--uvc--uvcvideo.ko_false-unreach-call" in bpl or
+      "linux-4.0-rc1---drivers--char--ipmi--ipmi_msghandler.ko_true-unreach-call" in bpl or
       "linux-4.2-rc1.tar.xz-43_2a-drivers--net--ppp--ppp_generic.ko-entry_point_true-unreach-call" in bpl):
     if not args.quiet:
       print("Stumbled upon a crappy device driver benchmark\n")
@@ -245,7 +249,7 @@ def verify_bpl_svcomp(args):
   if args.memory_safety:
     is_stack_benchmark(args, csource)
   else:
-    is_crappy_driver_benchmark(args, bpl)
+    is_buggy_driver_benchmark(args, bpl)
 
   if args.pthread:
     if "fib_bench" in bpl or "27_Boop_simple_vf_false-unreach-call" in bpl or "k < 5;" in csource or "k < 10;" in csource or "k < 20;" in csource:

From f97c2c0c1cef03ddb82adae481228ab58d086ef8 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Tue, 20 Nov 2018 06:39:44 -0700
Subject: [PATCH 50/60] Minor SVCOMP logging fix

---
 share/smack/svcomp/utils.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index a388c2ea7..5e45e7cff 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -159,7 +159,7 @@ def is_buggy_driver_benchmark(args, bpl):
       "linux-4.0-rc1---drivers--char--ipmi--ipmi_msghandler.ko_true-unreach-call" in bpl or
       "linux-4.2-rc1.tar.xz-43_2a-drivers--net--ppp--ppp_generic.ko-entry_point_true-unreach-call" in bpl):
     if not args.quiet:
-      print("Stumbled upon a crappy device driver benchmark\n")
+      print("Stumbled upon a buggy device driver benchmark\n")
     force_timeout()
 
 def is_stack_benchmark(args, csource):

From f3281a5af0dc4c4ef774ece31606d5f803434b6a Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Wed, 21 Nov 2018 05:04:22 -0700
Subject: [PATCH 51/60] Adjusting filter for float SVCOMP benchmarks

---
 share/smack/svcomp/filters.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/share/smack/svcomp/filters.py b/share/smack/svcomp/filters.py
index 34ee0fe07..1a0c8a47e 100644
--- a/share/smack/svcomp/filters.py
+++ b/share/smack/svcomp/filters.py
@@ -51,7 +51,7 @@ def bv_filter(lines, raw_line_count, pruned_line_count):
       "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines or
       "huge_floor" in lines or "huge_ceil" in lines or "tiny_sqrt" in lines or "fmax_float" in lines or
       "fabs_double" in lines or "round_double" in lines or "trunc_double" in lines or "zero_log" in lines or
-      "isinf_float" in lines or "trunc_float" in lines):
+      "isinf_float" in lines or "trunc_float" in lines or "exponent_less_127" in lines):
     return 0
   elif ('4294967294u' in lines or '616783' in lines or '__main(argc' in lines):
     return 1
@@ -101,7 +101,7 @@ def float_filter(lines, raw_line_count, pruned_line_count):
       "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines or
       "huge_floor" in lines or "huge_ceil" in lines or "tiny_sqrt" in lines or "fmax_float" in lines or
       "fabs_double" in lines or "round_double" in lines or "trunc_double" in lines or "zero_log" in lines or
-      "isinf_float" in lines or "trunc_float" in lines):
+      "isinf_float" in lines or "trunc_float" in lines or "exponent_less_127" in lines):
     return 1
 
   #heuristic #-1: don't do test on too large programs

From 5a54afbf2d853a3b159397ba4aad63ee77f14db1 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 22 Nov 2018 06:45:24 -0700
Subject: [PATCH 52/60] Fixed witness generation for memory leak property

---
 share/smack/svcomp/toSVCOMPformat.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/share/smack/svcomp/toSVCOMPformat.py b/share/smack/svcomp/toSVCOMPformat.py
index f03a5b4af..02469c5fa 100644
--- a/share/smack/svcomp/toSVCOMPformat.py
+++ b/share/smack/svcomp/toSVCOMPformat.py
@@ -185,7 +185,9 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug, status):
               continue
             callStack.append(calledFunc)
             if args.only_check_memcleanup or status == 'invalid-memtrack':
-              if "__SMACK_check_memory_leak" in jsonTrace["description"][len("CALL"):]:
+              if "__SMACK_check_memory_leak" in jsonTrace["description"][len("CALL"):] or
+                 "__VERIFIER_error" in jsonTrace["description"][len("CALL"):] or
+                 "exit" in jsonTrace["description"][len("CALL"):]:
                 newNode = addGraphNode(tree)
                 # addGraphNode returns a string, so we had to search the graph to get the node that we want
                 vNodes =tree.find("graph").findall("node")

From 8f53d4c3eb4ce2b1d0b72fc46347ce2843b25885 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 22 Nov 2018 07:07:02 -0700
Subject: [PATCH 53/60] Minor fix to Python syntax

---
 share/smack/svcomp/toSVCOMPformat.py | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/share/smack/svcomp/toSVCOMPformat.py b/share/smack/svcomp/toSVCOMPformat.py
index 02469c5fa..9db836eaf 100644
--- a/share/smack/svcomp/toSVCOMPformat.py
+++ b/share/smack/svcomp/toSVCOMPformat.py
@@ -185,9 +185,9 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug, status):
               continue
             callStack.append(calledFunc)
             if args.only_check_memcleanup or status == 'invalid-memtrack':
-              if "__SMACK_check_memory_leak" in jsonTrace["description"][len("CALL"):] or
-                 "__VERIFIER_error" in jsonTrace["description"][len("CALL"):] or
-                 "exit" in jsonTrace["description"][len("CALL"):]:
+              if ("__SMACK_check_memory_leak" in jsonTrace["description"][len("CALL"):] or
+                  "__VERIFIER_error" in jsonTrace["description"][len("CALL"):] or
+                  "exit" in jsonTrace["description"][len("CALL"):]):
                 newNode = addGraphNode(tree)
                 # addGraphNode returns a string, so we had to search the graph to get the node that we want
                 vNodes =tree.find("graph").findall("node")

From b766449b5e6b6af3497d63cf86208a52b8fbf27a Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 22 Nov 2018 09:15:47 -0700
Subject: [PATCH 54/60] Adding abort function to witness generation for memory
 leak

---
 share/smack/svcomp/toSVCOMPformat.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/share/smack/svcomp/toSVCOMPformat.py b/share/smack/svcomp/toSVCOMPformat.py
index 9db836eaf..de826069c 100644
--- a/share/smack/svcomp/toSVCOMPformat.py
+++ b/share/smack/svcomp/toSVCOMPformat.py
@@ -187,6 +187,7 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug, status):
             if args.only_check_memcleanup or status == 'invalid-memtrack':
               if ("__SMACK_check_memory_leak" in jsonTrace["description"][len("CALL"):] or
                   "__VERIFIER_error" in jsonTrace["description"][len("CALL"):] or
+                  "abort" in jsonTrace["description"][len("CALL"):] or
                   "exit" in jsonTrace["description"][len("CALL"):]):
                 newNode = addGraphNode(tree)
                 # addGraphNode returns a string, so we had to search the graph to get the node that we want

From e617d1eab00cffac86d7a5ef9e3da73e43cb33cf Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Thu, 22 Nov 2018 22:56:21 +0000
Subject: [PATCH 55/60] Generate precise violation node for witnesses

---
 share/smack/svcomp/toSVCOMPformat.py | 57 ++++++++--------------------
 share/smack/top.py                   |  2 +-
 2 files changed, 16 insertions(+), 43 deletions(-)

diff --git a/share/smack/svcomp/toSVCOMPformat.py b/share/smack/svcomp/toSVCOMPformat.py
index de826069c..db3166c11 100644
--- a/share/smack/svcomp/toSVCOMPformat.py
+++ b/share/smack/svcomp/toSVCOMPformat.py
@@ -156,10 +156,20 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug, status):
       pat = re.compile(".*smack\.[c|h]$")
       prevLineNo = -1
       prevColNo = -1
-      callStack = ['main']
+      callStack = [('main', '0')]
       # Loop through each trace
       for jsonTrace in jsonTraces:
         # Make sure it isn't a smack header file
+        if "ASSERTION FAILS" in jsonTrace["description"]:
+          newNode = addGraphNode(tree)
+          # addGraphNode returns a string, so we had to search the graph to get the node that we want
+          vNodes =tree.find("graph").findall("node")
+          for vNode in vNodes:
+            if vNode.attrib["id"] == newNode:
+              addKey(vNode, "violation", "true")
+          attribs = {"startline":str(callStack[-1][1])}
+          addGraphEdge(tree, lastNode, newNode, attribs)
+          break
         if not pat.match(jsonTrace["file"]):
           desc = jsonTrace["description"]
           formattedAssign = formatAssign(desc)
@@ -169,7 +179,7 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug, status):
             newNode = addGraphNode(tree)
             attribs = {"startline":str(jsonTrace["line"])}
             attribs["assumption"] = formattedAssign + ";"
-            attribs["assumption.scope"] = callStack[-1]
+            attribs["assumption.scope"] = callStack[-1][0]
             newEdge = addGraphEdge(tree, lastNode, newNode, attribs)
             prevLineNo = jsonTrace["line"]
             prevColNo = jsonTrace["column"]
@@ -183,44 +193,7 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug, status):
               continue
             if isSMACKInitFunc(calledFunc):
               continue
-            callStack.append(calledFunc)
-            if args.only_check_memcleanup or status == 'invalid-memtrack':
-              if ("__SMACK_check_memory_leak" in jsonTrace["description"][len("CALL"):] or
-                  "__VERIFIER_error" in jsonTrace["description"][len("CALL"):] or
-                  "abort" in jsonTrace["description"][len("CALL"):] or
-                  "exit" in jsonTrace["description"][len("CALL"):]):
-                newNode = addGraphNode(tree)
-                # addGraphNode returns a string, so we had to search the graph to get the node that we want
-                vNodes =tree.find("graph").findall("node")
-                for vNode in vNodes:
-                  if vNode.attrib["id"] == newNode:
-                    addKey(vNode, "violation", "true")
-                attribs = {"startline":str(jsonTrace["line"])}
-                addGraphEdge(tree, lastNode, newNode, attribs)
-                break
-            elif args.integer_overflow:
-              if "__SMACK_check_overflow" in jsonTrace["description"][len("CALL"):]:
-                newNode = addGraphNode(tree)
-                # addGraphNode returns a string, so we had to search the graph to get the node that we want
-                vNodes =tree.find("graph").findall("node")
-                for vNode in vNodes:
-                  if vNode.attrib["id"] == newNode:
-                    addKey(vNode, "violation", "true")
-                attribs = {"startline":str(jsonTrace["line"])}
-                addGraphEdge(tree, lastNode, newNode, attribs)
-                break
-            else:
-              if "__VERIFIER_error" in jsonTrace["description"][len("CALL"):]:
-                newNode = addGraphNode(tree)
-                # addGraphNode returns a string, so we had to search the graph to get the node that we want
-                vNodes =tree.find("graph").findall("node")
-                for vNode in vNodes:
-                  if vNode.attrib["id"] == newNode:
-                    addKey(vNode, "violation", "true")
-                attribs = {"startline":str(jsonTrace["line"])}
-                attribs["enterFunction"] = callStack[-1]
-                addGraphEdge(tree, lastNode, newNode, attribs)
-                break
+            callStack.append((calledFunc, jsonTrace["line"]))
           if "RETURN from" in desc:
             returnedFunc = str(desc[len("RETURN from "):]).strip()
             if returnedFunc.startswith("devirtbounce"):
@@ -228,8 +201,8 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug, status):
               continue
             if isSMACKInitFunc(returnedFunc):
               continue
-            if returnedFunc != callStack[-1]:
-              raise RuntimeError('Procedure Call/Return dismatch at line {0}. Call stack head: {1}, returning from: {2}'.format(jsonTrace["line"], callStack[-1], returnedFunc))
+            if returnedFunc != callStack[-1][0]:
+              raise RuntimeError('Procedure Call/Return dismatch at line {0}. Call stack head: {1}, returning from: {2}'.format(jsonTrace["line"], callStack[-1][0], returnedFunc))
             callStack.pop()
     print
     print
diff --git a/share/smack/top.py b/share/smack/top.py
index 65158d27b..18d415fc5 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -544,7 +544,7 @@ def error_trace(verifier_output, args):
 
 def smackdOutput(corralOutput):
   FILENAME = '[\w#$~%.\/-]+'
-  traceP = re.compile('(' + FILENAME + ')\((\d+),(\d+)\): Trace: Thread=(\d+)  (\((.*)\))?$')
+  traceP = re.compile('(' + FILENAME + ')\((\d+),(\d+)\): Trace: Thread=(\d+)  (\((.*)[\);])?$')
   errorP = re.compile('(' + FILENAME + ')\((\d+),(\d+)\): (error .*)$')
 
   passedMatch = re.search('Program has no bugs', corralOutput)

From 2ca49f1f2316f1844429ca7438cb217661b1b247 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Fri, 23 Nov 2018 06:53:19 -0700
Subject: [PATCH 56/60] Exclude SVCOMP float benchmarks with trigonometric
 functions

Those are not specified by the standard anyways.
---
 share/smack/svcomp/utils.py | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 5e45e7cff..882a57ec2 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -249,6 +249,10 @@ def verify_bpl_svcomp(args):
   if args.memory_safety:
     is_stack_benchmark(args, csource)
   else:
+    if "angleInRadian" in csource:
+      if not args.quiet:
+        print("Stumbled upon trigonometric function is float benchmark\n")
+      sys.exit(smack.top.results(args)['unknown'])
     is_buggy_driver_benchmark(args, bpl)
 
   if args.pthread:

From 172503a5f9fbabc263eea0282af51a8280c769a0 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Fri, 23 Nov 2018 06:56:14 -0700
Subject: [PATCH 57/60] Run Corral on SVCOMP floating-point category

Corral produces better results than Boogie.
---
 share/smack/svcomp/utils.py | 24 ------------------------
 1 file changed, 24 deletions(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 882a57ec2..c02557665 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -35,7 +35,6 @@ def svcomp_frontend(input_file, args):
       #sys.exit(smack.top.results(args)['unknown'])
       args.float = True
       args.bit_precise = True
-      args.bit_precise_pointers = True
       #args.verifier = 'boogie'
       args.time_limit = 1000
       args.unroll = 100
@@ -203,29 +202,6 @@ def verify_bpl_svcomp(args):
     smack.top.property_selection(args)
     args.only_check_memleak = False
 
-  # invoke boogie for floats
-  # I have to copy/paste part of verify_bpl
-  if args.float:
-    args.verifier = 'boogie'
-    boogie_command = ["boogie"]
-    boogie_command += [args.bpl_file]
-    boogie_command += ["/nologo", "/noinfer", "/doModSetAnalysis"]
-    boogie_command += ["/timeLimit:%s" % args.time_limit]
-    boogie_command += ["/errorLimit:%s" % args.max_violations]
-    boogie_command += ["/loopUnroll:%d" % args.unroll]
-    if args.bit_precise:
-      x = "bopt:" if args.verifier != 'boogie' else ""
-      boogie_command += ["/%sproverOpt:OPTIMIZE_FOR_BV=true" % x]
-      boogie_command += ["/%sboolControlVC" % x]
-
-    if args.verifier_options:
-      boogie_command += args.verifier_options.split()
-
-    boogie_output = smack.top.try_command(boogie_command, timeout=args.time_limit)
-    boogie_result = smack.top.verification_result(boogie_output)
-    write_error_file(args, boogie_result, boogie_output)
-    sys.exit(smack.top.results(args)[boogie_result])
-
   # If pthreads found, perform lock set analysis
   if args.pthread:
     lockpwn_command = ["lockpwn"]

From 0da7c624b860612b195c8648259a651ee6da0282 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sun, 25 Nov 2018 00:44:19 -0700
Subject: [PATCH 58/60] Turn on bit precise pointers for a float SVCOMP
 benchmark

The benchmark does low-level operations to obtain sign.
---
 share/smack/svcomp/utils.py | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index c02557665..e86125562 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -32,17 +32,17 @@ def svcomp_frontend(input_file, args):
       args.bit_precise = True
       args.bit_precise_pointers = True
     if file_type == 'float' and not args.integer_overflow:
-      #sys.exit(smack.top.results(args)['unknown'])
       args.float = True
       args.bit_precise = True
-      #args.verifier = 'boogie'
-      args.time_limit = 1000
-      args.unroll = 100
+      with open(input_file, "r") as sf:
+        sc = sf.read()
+      if 'copysign(1' in sc:
+        args.bit_precise_pointers = True
     args.execute = executable
   else:
     with open(input_file, "r") as sf:
       sc = sf.read()
-    if 'unsigned char b:2' in sc or "4294967294u" in sc or "_ddv_module_init" in sc or "bb_process_escape_sequence" in sc:
+    if "unsigned char b:2" in sc or "4294967294u" in sc or "_ddv_module_init" in sc or "bb_process_escape_sequence" in sc:
       args.bit_precise = True
       #args.bit_precise_pointers = True
 

From 65a21789cfc0861d1f3baa87be1570321923d4ed Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Tue, 27 Nov 2018 03:51:38 -0700
Subject: [PATCH 59/60] Updated loop unroll for large concurrency benchmarks

---
 share/smack/svcomp/utils.py | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index e86125562..c60a6fe45 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -309,6 +309,9 @@ def verify_bpl_svcomp(args):
   elif "i>>16" in csource:
     heurTrace += "Large array reach benchmark. Setting loop unroll bar to INT_MAX.\n"
     loopUnrollBar = 2**31 - 1
+  elif "whoop_poll_table" in csource:
+    heurTrace += "Large concurrency benchmark. Setting loop unroll bar to INT_MAX.\n"
+    loopUnrollBar = 2**31 - 1
 
   if not "forall" in bpl:
     heurTrace += "No quantifiers detected. Setting z3 relevancy to 0.\n"

From eb9811adabcaca203bb3212903b1e79257d382ee Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Tue, 27 Nov 2018 03:56:25 -0700
Subject: [PATCH 60/60] Bumped version number to 1.9.2

---
 Doxyfile                                                        | 2 +-
 share/smack/reach.py                                            | 2 +-
 share/smack/top.py                                              | 2 +-
 .../src/benchexec/benchexec/tools/smack_benchexec_driver.py     | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Doxyfile b/Doxyfile
index ee3c75f72..78f93ec58 100644
--- a/Doxyfile
+++ b/Doxyfile
@@ -5,7 +5,7 @@
 #---------------------------------------------------------------------------
 DOXYFILE_ENCODING      = UTF-8
 PROJECT_NAME           = smack
-PROJECT_NUMBER         = 1.9.1
+PROJECT_NUMBER         = 1.9.2
 PROJECT_BRIEF          = "A bounded software verifier."
 PROJECT_LOGO           =
 OUTPUT_DIRECTORY       = docs
diff --git a/share/smack/reach.py b/share/smack/reach.py
index 53528e443..c2b25b104 100755
--- a/share/smack/reach.py
+++ b/share/smack/reach.py
@@ -11,7 +11,7 @@
 from smackgen import *
 from smackverify import *
 
-VERSION = '1.9.1'
+VERSION = '1.9.2'
 
 def reachParser():
     parser = argparse.ArgumentParser(add_help=False, parents=[verifyParser()])
diff --git a/share/smack/top.py b/share/smack/top.py
index 18d415fc5..194a4b8fa 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -15,7 +15,7 @@
 from prelude import append_prelude
 from frontend import link_bc_files, frontends, languages, extra_libs 
 
-VERSION = '1.9.1'
+VERSION = '1.9.2'
 
 def results(args):
   """A dictionary of the result output messages."""
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 84e6b9c26..2c50a0b93 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.9.1'
+        return '1.9.2'
 
     def name(self):
         """