From 704efe9b74b9e3ee0bf2eafb54259094fed0c9d6 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sun, 16 Aug 2020 21:18:34 -0600
Subject: [PATCH 01/20] Updated Boogie to its latest release

---
 bin/versions | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bin/versions b/bin/versions
index 6be059a2c..a796e543a 100644
--- a/bin/versions
+++ b/bin/versions
@@ -1,7 +1,7 @@
 Z3_VERSION=4.8.8
 CVC4_VERSION=1.7
 YICES2_VERSION=2.6.2
-BOOGIE_VERSION=2.6.15
+BOOGIE_VERSION=2.7.15
 CORRAL_VERSION=1.0.12
 SYMBOOGLIX_COMMIT=ccb2e7f2b3
 LOCKPWN_COMMIT=12ba58f1ec

From 04c527b44a1247820f12977569c360b5ec60c310 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Tue, 18 Aug 2020 16:42:32 -0600
Subject: [PATCH 02/20] Turned off clang-format for a comment in
 test/c/basic/transform-out.c

This commit allows clang-format to still check that file.
---
 .travis.yml                  | 2 +-
 test/c/basic/transform-out.c | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/.travis.yml b/.travis.yml
index 3791b47ce..ccf50b7c9 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -73,6 +73,6 @@ before_script:
   - llvm-config --version
 
 script:
-  - ./format/run-clang-format.py -e test/c/basic/transform-out.c -r lib/smack include/smack share/smack/include share/smack/lib test examples
+  - ./format/run-clang-format.py -r lib/smack include/smack share/smack/include share/smack/lib test examples
   - flake8 test/regtest.py share/smack/ --extend-exclude share/smack/svcomp/,share/smack/reach.py
   - INSTALL_RUST=1 ./bin/build.sh
diff --git a/test/c/basic/transform-out.c b/test/c/basic/transform-out.c
index d56756fc9..dad17ff34 100644
--- a/test/c/basic/transform-out.c
+++ b/test/c/basic/transform-out.c
@@ -3,7 +3,9 @@
 #include <stdlib.h>
 
 // @expect verified
+// clang-format off
 // @flag --transform-out "sed -e 's/[[:digit:]]* verified, [[:digit:]]* error/1 verified, 0 errors/' -e 's/can fail/no bugs/'"
+// clang-format on
 
 int main(void) {
   assert(0);

From 4eab7bf4942767b4c982cce9a56e859d07473e38 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Wed, 19 Aug 2020 21:15:49 -0600
Subject: [PATCH 03/20] Added format checking llvm2bpl.cpp into CI

---
 .travis.yml                 |  2 +-
 tools/llvm2bpl/llvm2bpl.cpp | 14 +++++++-------
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index ccf50b7c9..0ffdfd721 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -73,6 +73,6 @@ before_script:
   - llvm-config --version
 
 script:
-  - ./format/run-clang-format.py -r lib/smack include/smack share/smack/include share/smack/lib test examples
+  - ./format/run-clang-format.py -r lib/smack include/smack tools share/smack/include share/smack/lib test examples
   - flake8 test/regtest.py share/smack/ --extend-exclude share/smack/svcomp/,share/smack/reach.py
   - INSTALL_RUST=1 ./bin/build.sh
diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp
index 0a71fdf65..136b1c0a9 100644
--- a/tools/llvm2bpl/llvm2bpl.cpp
+++ b/tools/llvm2bpl/llvm2bpl.cpp
@@ -24,10 +24,6 @@
 #include "llvm/Support/raw_ostream.h"
 #include "llvm/Target/TargetMachine.h"
 
-#include "utils/Devirt.h"
-#include "utils/MergeGEP.h"
-#include "utils/SimplifyExtractValue.h"
-#include "utils/SimplifyInsertValue.h"
 #include "smack/AddTiming.h"
 #include "smack/BplFilePrinter.h"
 #include "smack/CodifyStaticInits.h"
@@ -42,6 +38,10 @@
 #include "smack/SmackOptions.h"
 #include "smack/SplitAggregateValue.h"
 #include "smack/VerifierCodeMetadata.h"
+#include "utils/Devirt.h"
+#include "utils/MergeGEP.h"
+#include "utils/SimplifyExtractValue.h"
+#include "utils/SimplifyInsertValue.h"
 
 static llvm::cl::opt<std::string>
     InputFilename(llvm::cl::Positional,
@@ -108,9 +108,9 @@ static TargetMachine *GetTargetMachine(Triple TheTriple, StringRef CPUStr,
       Reloc::Static,   /* was getRelocModel(),*/
       None,            /* Use default CodeModel */
       CodeGenOpt::None /*GetCodeGenOptLevel())*/
-      );
-}
+  );
 }
+} // namespace
 
 int main(int argc, char **argv) {
   llvm::llvm_shutdown_obj shutdown; // calls llvm_shutdown() on exit
@@ -152,7 +152,7 @@ int main(int argc, char **argv) {
   pass_manager.add(llvm::createLowerSwitchPass());
   // pass_manager.add(llvm::createCFGSimplificationPass());
   // Shaobo: sea-dsa is inconsistent with the pass below.
-  //pass_manager.add(llvm::createInternalizePass());
+  // pass_manager.add(llvm::createInternalizePass());
   pass_manager.add(llvm::createPromoteMemoryToRegisterPass());
 
   if (StaticUnroll) {

From 47e12357839003c30c96230fd485d90dfbfdeb9c Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Wed, 19 Aug 2020 22:53:39 -0600
Subject: [PATCH 04/20] Fixed SV-COMP scripts

---
 share/smack/svcomp/utils.py | 120 ++++++++++++++++++++----------------
 share/smack/top.py          |   2 +-
 2 files changed, 67 insertions(+), 55 deletions(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index c520e6bca..7f1336e9e 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -25,13 +25,13 @@ def svcomp_frontend(input_file, args):
   svcomp_check_property(args)
 
   # fix: disable float filter for memory safety benchmarks
-  if not (args.memory_safety or args.only_check_memcleanup):
+  if not ('memory-safety' in args.check or 'memleak' in args.check):
     # test bv and executable benchmarks
     file_type, executable = filters.svcomp_filter(args.input_files[0])
     if file_type == 'bitvector':
       args.integer_encoding = 'bit-vector'
       args.pointer_encoding = 'bit-vector'
-    if file_type == 'float' and not args.integer_overflow:
+    if file_type == 'float' and not 'integer-overflow' in args.check:
       args.float = True
       args.integer_encoding = 'bit-vector'
       with open(input_file, "r") as sf:
@@ -66,24 +66,21 @@ def svcomp_frontend(input_file, args):
   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
+      args.check = ['memory-safety']
     elif "valid-memcleanup" in prop:
-      args.memory_safety = True
-      args.only_check_memcleanup = True
+      args.check = ['memleak']
     elif "overflow" in prop:
-      args.integer_overflow = True
+      args.check = ['integer-overflow']
     elif not "reach_error" in prop:
-      sys.exit(smack.top.results(args)['unknown'])
+      print(smack.top.results(args)['unknown'][0])
+      sys.exit(smack.top.results(args)['unknown'][1])
 
 def svcomp_process_file(args, name, ext):
   args.orig_files = list(args.input_files)
@@ -98,14 +95,14 @@ def svcomp_process_file(args, name, ext):
     s = re.sub(r'static\s+char\s+dir\[42\];\s+for\(int\s+i=0;\s+i<42;\s+\+\+i\)\s+dir\[i\]\s+=\s+__VERIFIER_nondet_char\(\);\s+dir\[41\]\s+=\s+\'\\0\';', r'static char dir[3];\n  dir[0] = __VERIFIER_nondet_char();\n  dir[1] = __VERIFIER_nondet_char();\n  dir[2] = 0;', s)
     s = re.sub(r'__VERIFIER_assume\(i < 16\);', r'__VERIFIER_assume(i >= 0 && i < 16);', s)
 
-    if args.memory_safety and not 'argv=malloc' in s:
+    if 'memory-safety' in args.check and not 'argv=malloc' in s:
       s = re.sub(r'typedef long unsigned int size_t', r'typedef unsigned int size_t', s)
-    elif args.memory_safety and re.search(r'getopt32\([^,)]+,[^,)]+,[^.)]+\);', s):
+    elif 'memory-safety' in args.check and re.search(r'getopt32\([^,)]+,[^,)]+,[^.)]+\);', s):
       if not args.quiet:
         print("Stumbled upon a benchmark that requires precise handling of vararg\n")
       while (True):
         pass
-    elif args.memory_safety and ('count is too big' in s or 'pdRfilsLHarPv' in s or 'rnugG' in s):
+    elif 'memory-safety' in args.check and ('count is too big' in s or 'pdRfilsLHarPv' in s or 'rnugG' in s):
       if not args.quiet:
         print("Stumbled upon a benchmark that contains undefined behavior\n")
       while (True):
@@ -113,7 +110,7 @@ def svcomp_process_file(args, name, ext):
 
     if 'argv=malloc' in s:
 #      args.integer_encoding = 'bit-vector'
-      if args.integer_overflow and ('unsigned int d = (unsigned int)((signed int)(unsigned char)((signed int)*q | (signed int)(char)32) - 48);' in s or 'bb_ascii_isalnum' in s or 'ptm=localtime' in s or '0123456789.' in s):
+      if 'integer-overflow' in args.check and ('unsigned int d = (unsigned int)((signed int)(unsigned char)((signed int)*q | (signed int)(char)32) - 48);' in s or 'bb_ascii_isalnum' in s or 'ptm=localtime' in s or '0123456789.' in s):
         args.integer_encoding = 'bit-vector'
         args.pointer_encoding = 'bit-vector'
 
@@ -167,7 +164,8 @@ def is_stack_benchmark(args, csource):
       "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'])
+    print(smack.top.results(args)['unknown'][0])
+    sys.exit(smack.top.results(args)['unknown'][1])
 
 def inject_assert_false(args):
     with open(args.bpl_file, 'r') as bf:
@@ -180,38 +178,42 @@ def verify_bpl_svcomp(args):
   """Verify the Boogie source file using SVCOMP-tuned heuristics."""
   heurTrace = "\n\nHeuristics Info:\n"
 
-  if not args.memory_safety and not args.only_check_memcleanup and not args.integer_overflow:
+  if not 'memory-safety' in args.check and not 'memleak' in args.check and not 'integer-overflow' in args.check:
     inject_assert_false(args)
 
-  if args.memory_safety:
-    if not (args.only_check_valid_deref or args.only_check_valid_free or args.only_check_memleak):
+  if 'memory-safety' in args.check:
+    if len(args.check) == 1:
       heurTrace = "engage valid deference checks.\n"
-      args.only_check_valid_deref = True
+      args.check.pop()
+      args.check.append('valid-deref')
       args.prop_to_check = 'valid-deref'
       args.bpl_with_all_props = smack.top.temporary_file(os.path.splitext(os.path.basename(args.bpl_file))[0], '.bpl', args)
       copyfile(args.bpl_file, args.bpl_with_all_props)
-      smack.top.property_selection(args)
-    elif args.only_check_valid_deref:
+      smack.top.memsafety_subproperty_selection(args)
+      args.check.append('memory-safety')
+    elif 'valid-deref' in args.check:
       heurTrace = "engage valid free checks.\n"
-      args.only_check_valid_free = True
+      args.check.pop()
+      args.check.pop()
       args.prop_to_check = 'valid-free'
-      args.only_check_valid_deref = False
+      args.check.append('valid-free')
       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_valid_free:
+      smack.top.memsafety_subproperty_selection(args)
+      args.check.append('memory-safety')
+    elif 'valid-free' in args.check:
       heurTrace = "engage memleak checks.\n"
-      args.only_check_memleak = True
+      args.check.pop()
+      args.check.pop()
       args.prop_to_check = 'memleak'
-      args.only_check_valid_free = False
+      args.check.append('memleak')
       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:
+      smack.top.memsafety_subproperty_selection(args)
+      args.check.append('memory-safety')
+  elif 'memleak' in args.check:
     heurTrace = "engage memcleanup checks.\n"
-    args.only_check_memleak = True
-    smack.top.property_selection(args)
-    args.only_check_memleak = False
+    smack.top.memsafety_subproperty_selection(args)
 
   # If pthreads found, perform lock set analysis
   if args.pthread:
@@ -234,17 +236,19 @@ def verify_bpl_svcomp(args):
   with open(args.input_files[0], "r") as f:
     csource = f.read()
 
-  if args.memory_safety:
+  if 'memory-safety' in args.check:
     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'])
+      print(smack.top.results(args)['unknown'][0])
+      sys.exit(smack.top.results(args)['unknown'][1])
     elif "copysign(1" in csource:
       if not args.quiet:
         print("Stumbled upon tricky float benchmark\n")
-      sys.exit(smack.top.results(args)['unknown'])
+      print(smack.top.results(args)['unknown'][0])
+      sys.exit(smack.top.results(args)['unknown'][1])
     is_buggy_driver_benchmark(args, bpl)
 
   if args.pthread:
@@ -257,7 +261,7 @@ def verify_bpl_svcomp(args):
       corral_command += ["/cooperative"]
   else:
     corral_command += ["/k:1"]
-    if not (args.memory_safety or args.integer_encoding == 'bit-vector' or args.only_check_memcleanup):
+    if not ('memory-safety' in args.check or args.integer_encoding == 'bit-vector' or 'memleak' in args.check):
       if not ("dll_create" in csource or "sll_create" in csource or "changeMethaneLevel" in csource):
         corral_command += ["/di"]
 
@@ -266,7 +270,8 @@ def verify_bpl_svcomp(args):
     heurTrace += "We are not modeling strcpy - aborting\n"
     if not args.quiet:
       print((heurTrace + "\n"))
-    sys.exit(smack.top.results(args)['unknown'])
+    print(smack.top.results(args)['unknown'][0])
+    sys.exit(smack.top.results(args)['unknown'][1])
 
   # Setting good loop unroll bound based on benchmark class
   loopUnrollBar = 8
@@ -309,16 +314,16 @@ def verify_bpl_svcomp(args):
   elif "printf_false-unreach-call" in bpl or "echo_true-no-overflow" in bpl:
     heurTrace += "BusyBox benchmark detected. Setting loop unroll bar to 11.\n"
     loopUnrollBar = 11
-  elif args.memory_safety and "__main($i0" in bpl:
+  elif 'memory-safety' in args.check and "__main($i0" in bpl:
     heurTrace += "BusyBox memory safety benchmark detected. Setting loop unroll bar to 4.\n"
     loopUnrollBar = 4
-  elif args.integer_overflow and "__main($i0" in bpl:
+  elif 'integer-overflow' in args.check and "__main($i0" in bpl:
     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):
+  elif 'integer-overflow' in args.check 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
+  elif 'integer-overflow' in args.check 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
@@ -333,7 +338,7 @@ def verify_bpl_svcomp(args):
     heurTrace += "No quantifiers detected. Setting z3 relevancy to 0.\n"
     corral_command += ["/bopt:proverOpt:O:smt.relevancy=0"]
 
-  if args.memory_safety:
+  if 'memory-safety' in args.check:
     if args.prop_to_check == 'valid-deref':
       if "memleaks_test12_false-valid-free" in bpl:
         time_limit = 10
@@ -363,7 +368,7 @@ def verify_bpl_svcomp(args):
     if not args.quiet:
       error = smack.top.error_trace(verifier_output, args)
       print(error)
-    if args.memory_safety:
+    if 'memory-safety' in args.check:
       heurTrace += (args.prop_to_check + "has errors\n")
       if args.prop_to_check == 'valid-free':
         if args.valid_deref_check_result != 'verified':
@@ -399,16 +404,18 @@ def verify_bpl_svcomp(args):
           heurTrace += "Oops, execution result says {0}.\n".format(execution_result)
           if not args.quiet:
             print((heurTrace + "\n"))
-          sys.exit(smack.top.results(args)['unknown'])
+          print(smack.top.results(args)['unknown'][0])
+          sys.exit(smack.top.results(args)['unknown'][1])
       random_test_result = random_test(args, result)
       if random_test_result == 'false' or random_test_result == 'unknown':
         heurTrace += "Oops, random testing says {0}.\n".format(random_test_result)
         if not args.quiet:
           print((heurTrace + "\n"))
-        sys.exit(smack.top.results(args)['unknown'])
+        print(smack.top.results(args)['unknown'][0])
+        sys.exit(smack.top.results(args)['unknown'][1])
       if not args.quiet:
         print((heurTrace + "\n"))
-      if args.memory_safety:
+      if 'memory-safety' in args.check:
         heurTrace += (args.prop_to_check + "is verified\n")
         if args.prop_to_check == 'valid-deref':
           args.valid_deref_check_result = 'verified'
@@ -418,11 +425,13 @@ def verify_bpl_svcomp(args):
           if args.valid_deref_check_result == 'timeout':
             force_timeout()
           else:
-            sys.exit(smack.top.results(args)[args.valid_deref_check_result])
+            print(smack.top.results(args)[args.valid_deref_check_result][0])
+            sys.exit(smack.top.results(args)[args.valid_deref_check_result][1])
         verify_bpl_svcomp(args)
       else:
         write_error_file(args, 'verified', verifier_output)
-        sys.exit(smack.top.results(args)['verified'])
+        print(smack.top.results(args)['verified'][0])
+        sys.exit(smack.top.results(args)['verified'][1])
     else:
       heurTrace += "Only unrolled " + str(unrollMax) + " times.\n"
       heurTrace += "Insufficient unrolls to consider 'verified'.  "
@@ -430,7 +439,7 @@ def verify_bpl_svcomp(args):
       if not args.quiet:
         print((heurTrace + "\n"))
         sys.stdout.flush()
-      if args.memory_safety:
+      if 'memory-safety' in args.check:
         heurTrace += (args.prop_to_check + " times out\n")
         if args.prop_to_check == 'valid-deref':
           args.valid_deref_check_result = 'timeout'
@@ -441,7 +450,8 @@ def verify_bpl_svcomp(args):
           if args.valid_deref_check_result == 'timeout':
             force_timeout()
           else:
-            sys.exit(smack.top.results(args)[args.valid_deref_check_result])
+            print(smack.top.results(args)[args.valid_deref_check_result][0])
+            sys.exit(smack.top.results(args)[args.valid_deref_check_result][1])
         verify_bpl_svcomp(args)
       else:
         force_timeout()
@@ -451,7 +461,7 @@ def verify_bpl_svcomp(args):
     heurTrace += "Normal inlining returned 'unknown'.  See errors above.\n"
   if not args.quiet:
     print((heurTrace + "\n"))
-  if args.memory_safety and result == 'verified':
+  if 'memory-safety' in args.check and result == 'verified':
     heurTrace += (args.prop_to_check + " is verified\n")
     if args.prop_to_check == 'valid-deref':
       args.valid_deref_check_result = 'verified'
@@ -461,14 +471,16 @@ def verify_bpl_svcomp(args):
       if args.valid_deref_check_result == 'timeout':
         force_timeout()
       else:
-        sys.exit(smack.top.results(args)[args.valid_deref_check_result])
+        print(smack.top.results(args)[args.valid_deref_check_result][0])
+        sys.exit(smack.top.results(args)[args.valid_deref_check_result][1])
     verify_bpl_svcomp(args)
   else:
     write_error_file(args, result, verifier_output)
-    if args.only_check_memcleanup and result == 'invalid-memtrack':
+    if 'memleak' in args.check and result == 'invalid-memtrack':
       sys.exit('SMACK found an error: memory cleanup.')
     else:
-      sys.exit(smack.top.results(args)[result])
+      print(smack.top.results(args)[result][0])
+      sys.exit(smack.top.results(args)[result][1])
 
 def write_error_file(args, status, verifier_output):
   #return
diff --git a/share/smack/top.py b/share/smack/top.py
index 49ddef237..d46664510 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -600,7 +600,7 @@ def annotate_bpl(args):
 
 
 def memsafety_subproperty_selection(args):
-    selected_props = {}
+    selected_props = set()
     if 'memory-safety' in args.check:
         return
     if 'valid-deref' in args.check:

From 1b956e12e776773e91284ca4b1c198f484346896 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Thu, 20 Aug 2020 11:56:23 -0600
Subject: [PATCH 05/20] Enabled string functions for certain SV-COMP properties

---
 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 7f1336e9e..2272df8e0 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -46,6 +46,9 @@ def svcomp_frontend(input_file, args):
       args.integer_encoding = 'bit-vector'
       #args.pointer_encoding = 'bit-vector'
 
+  if 'memory-safety' in args.check or 'memleak' in args.check or 'integer-overflow' in args.check:
+      args.strings = True
+
   name, ext = os.path.splitext(os.path.basename(args.input_files[0]))
   svcomp_process_file(args, name, ext)
 

From 836ab564583bd51b8cb8d4324c6b28c28bf0a134 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Mon, 17 Aug 2020 19:25:51 -0600
Subject: [PATCH 06/20] Upgrade SMACK to LLVM 10

---
 .gitmodules                         |  1 -
 bin/versions                        |  4 +-
 include/smack/Regions.h             |  1 +
 include/smack/SimplifyLibCalls.h    |  6 +--
 include/smack/SplitAggregateValue.h |  6 +--
 include/utils/InitializePasses.h    | 13 +++++
 lib/smack/AddTiming.cpp             |  6 ++-
 lib/smack/Debug.cpp                 |  5 +-
 lib/smack/ExtractContracts.cpp      |  6 ++-
 lib/smack/SimplifyLibCalls.cpp      |  7 +--
 lib/smack/SplitAggregateValue.cpp   | 82 +++++++++++++++--------------
 lib/utils/Devirt.cpp                | 18 ++++---
 sea-dsa                             |  2 +-
 tools/llvm2bpl/llvm2bpl.cpp         |  2 +
 14 files changed, 93 insertions(+), 66 deletions(-)
 create mode 100644 include/utils/InitializePasses.h

diff --git a/.gitmodules b/.gitmodules
index fe7950bd7..32ba47b83 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,4 +1,3 @@
 [submodule "sea-dsa"]
   path = sea-dsa
   url = https://github.com/seahorn/sea-dsa.git
-  branch = llvm-8.0
diff --git a/bin/versions b/bin/versions
index a796e543a..fc5b9a60b 100644
--- a/bin/versions
+++ b/bin/versions
@@ -5,6 +5,6 @@ BOOGIE_VERSION=2.7.15
 CORRAL_VERSION=1.0.12
 SYMBOOGLIX_COMMIT=ccb2e7f2b3
 LOCKPWN_COMMIT=12ba58f1ec
-LLVM_SHORT_VERSION=9
-LLVM_FULL_VERSION=9.0.1
+LLVM_SHORT_VERSION=10
+LLVM_FULL_VERSION=10.0.1
 RUST_VERSION=2020-05-21
diff --git a/include/smack/Regions.h b/include/smack/Regions.h
index d2c1ad0ea..8e783050e 100644
--- a/include/smack/Regions.h
+++ b/include/smack/Regions.h
@@ -6,6 +6,7 @@
 
 #include "seadsa/Graph.hh"
 #include "llvm/IR/InstVisitor.h"
+#include "llvm/Pass.h"
 
 using namespace llvm;
 
diff --git a/include/smack/SimplifyLibCalls.h b/include/smack/SimplifyLibCalls.h
index 227f7eed3..139d3b242 100644
--- a/include/smack/SimplifyLibCalls.h
+++ b/include/smack/SimplifyLibCalls.h
@@ -12,7 +12,7 @@ namespace smack {
 
 using namespace llvm;
 
-class SimplifyLibCalls : public ModulePass,
+class SimplifyLibCalls : public FunctionPass,
                          public InstVisitor<SimplifyLibCalls> {
 private:
   bool modified;
@@ -20,9 +20,9 @@ class SimplifyLibCalls : public ModulePass,
 
 public:
   static char ID;
-  SimplifyLibCalls() : ModulePass(ID) {}
+  SimplifyLibCalls() : FunctionPass(ID) {}
   virtual void getAnalysisUsage(AnalysisUsage &AU) const;
-  virtual bool runOnModule(Module &M);
+  virtual bool runOnFunction(Function &F);
   void visitCallInst(CallInst &);
 };
 } // namespace smack
diff --git a/include/smack/SplitAggregateValue.h b/include/smack/SplitAggregateValue.h
index 98a06362a..b09b1642a 100644
--- a/include/smack/SplitAggregateValue.h
+++ b/include/smack/SplitAggregateValue.h
@@ -14,13 +14,13 @@
 
 namespace smack {
 
-class SplitAggregateValue : public llvm::BasicBlockPass {
+class SplitAggregateValue : public llvm::FunctionPass {
 public:
   typedef std::vector<std::pair<llvm::Value *, unsigned>> IndexT;
   typedef std::pair<IndexT, llvm::Constant *> InfoT;
   static char ID;
-  SplitAggregateValue() : llvm::BasicBlockPass(ID) {}
-  virtual bool runOnBasicBlock(llvm::BasicBlock &BB);
+  SplitAggregateValue() : llvm::FunctionPass(ID) {}
+  virtual bool runOnFunction(llvm::Function &F);
 
 private:
   llvm::Value *splitAggregateLoad(llvm::LoadInst *li, std::vector<InfoT> &info,
diff --git a/include/utils/InitializePasses.h b/include/utils/InitializePasses.h
new file mode 100644
index 000000000..faf799910
--- /dev/null
+++ b/include/utils/InitializePasses.h
@@ -0,0 +1,13 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+#ifndef UTILS_INITIALIZEPASSES_H
+#define UTILS_INITIALIZEPASSES_H
+
+#include "llvm/InitializePasses.h"
+
+namespace llvm {
+void initializeDevirtualizePass(PassRegistry &Registry);
+} // end namespace llvm
+
+#endif // UTILS_INITIALIZEPASSES_H
diff --git a/lib/smack/AddTiming.cpp b/lib/smack/AddTiming.cpp
index ad1eb2a40..7cc074857 100644
--- a/lib/smack/AddTiming.cpp
+++ b/lib/smack/AddTiming.cpp
@@ -28,6 +28,7 @@
 #include "llvm/IR/IntrinsicInst.h"
 #include "llvm/IR/Value.h"
 #include "llvm/Pass.h"
+#include "llvm/Support/Alignment.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
 
@@ -186,7 +187,8 @@ unsigned AddTiming::getInstructionCost(const Instruction *I) const {
     Type *ValTy = SI->getValueOperand()->getType();
     assert(!ValTy->isStructTy() &&
            "Timing annotations do not currently work for struct sized stores");
-    return TTI->getMemoryOpCost(I->getOpcode(), ValTy, SI->getAlignment(),
+    return TTI->getMemoryOpCost(I->getOpcode(), ValTy,
+                                MaybeAlign(SI->getAlignment()),
                                 SI->getPointerAddressSpace());
   }
   case Instruction::Load: {
@@ -194,7 +196,7 @@ unsigned AddTiming::getInstructionCost(const Instruction *I) const {
     assert(!I->getType()->isStructTy() &&
            "Timing annotations do not currently work for struct sized loads");
     return TTI->getMemoryOpCost(I->getOpcode(), I->getType(),
-                                LI->getAlignment(),
+                                MaybeAlign(LI->getAlignment()),
                                 LI->getPointerAddressSpace());
   }
   case Instruction::ZExt:
diff --git a/lib/smack/Debug.cpp b/lib/smack/Debug.cpp
index 1d12f49bd..4a3c3d06d 100644
--- a/lib/smack/Debug.cpp
+++ b/lib/smack/Debug.cpp
@@ -42,7 +42,8 @@ void setCurrentDebugTypes(const char **Types, unsigned Count) {
 
 static ::llvm::cl::opt<bool, true> Debug("debug",
                                          cl::desc("Enable debug output"),
-                                         cl::Hidden, cl::location(DebugFlag));
+                                         cl::Hidden,
+                                         cl::location(smack::DebugFlag));
 
 namespace {
 
@@ -50,7 +51,7 @@ struct DebugOnlyOpt {
   void operator=(const std::string &Val) const {
     if (Val.empty())
       return;
-    DebugFlag = true;
+    smack::DebugFlag = true;
     SmallVector<StringRef, 8> dbgTypes;
     StringRef(Val).split(dbgTypes, ',', -1, false);
     for (auto dbgType : dbgTypes)
diff --git a/lib/smack/ExtractContracts.cpp b/lib/smack/ExtractContracts.cpp
index f0cc0b00c..4d8b81b63 100644
--- a/lib/smack/ExtractContracts.cpp
+++ b/lib/smack/ExtractContracts.cpp
@@ -229,7 +229,8 @@ bool ExtractContracts::runOnModule(Module &M) {
     }
 
     if (!contractBlocks.empty()) {
-      auto *newF = CodeExtractor(contractBlocks).extractCodeRegion();
+      auto *newF = CodeExtractor(contractBlocks)
+                       .extractCodeRegion(CodeExtractorAnalysisCache(*F));
 
       std::vector<CallInst *> Is;
       for (auto V : newF->users())
@@ -258,7 +259,8 @@ bool ExtractContracts::runOnModule(Module &M) {
 
     for (auto const &entry : invariantBlocks) {
       auto BBs = entry.second;
-      auto *newF = CodeExtractor(BBs).extractCodeRegion();
+      auto *newF =
+          CodeExtractor(BBs).extractCodeRegion(CodeExtractorAnalysisCache(*F));
 
       std::vector<CallInst *> Is;
       for (auto V : newF->users())
diff --git a/lib/smack/SimplifyLibCalls.cpp b/lib/smack/SimplifyLibCalls.cpp
index 605f161f6..8400fc13e 100644
--- a/lib/smack/SimplifyLibCalls.cpp
+++ b/lib/smack/SimplifyLibCalls.cpp
@@ -28,15 +28,16 @@ void SimplifyLibCalls::getAnalysisUsage(AnalysisUsage &AU) const {
   AU.addRequired<TargetLibraryInfoWrapperPass>();
 }
 
-bool SimplifyLibCalls::runOnModule(Module &M) {
+bool SimplifyLibCalls::runOnFunction(Function &F) {
   modified = false;
   simplifier = new LibCallSimplifier(
-      M.getDataLayout(), &getAnalysis<TargetLibraryInfoWrapperPass>().getTLI(),
+      F.getParent()->getDataLayout(),
+      &getAnalysis<TargetLibraryInfoWrapperPass>().getTLI(F),
       getAnalysis<OptimizationRemarkEmitterWrapperPass>().getORE(),
       &getAnalysis<BlockFrequencyInfoWrapperPass>().getBFI(),
       &getAnalysis<ProfileSummaryInfoWrapperPass>().getPSI());
   if (simplifier)
-    visit(M);
+    visit(F);
   return modified;
 }
 
diff --git a/lib/smack/SplitAggregateValue.cpp b/lib/smack/SplitAggregateValue.cpp
index bd9243901..0c27514f9 100644
--- a/lib/smack/SplitAggregateValue.cpp
+++ b/lib/smack/SplitAggregateValue.cpp
@@ -22,50 +22,52 @@ std::vector<unsigned> getSeconds(SplitAggregateValue::IndexT lst) {
   return ret;
 }
 
-bool SplitAggregateValue::runOnBasicBlock(BasicBlock &BB) {
-  std::vector<Instruction *> toRemove;
-  LLVMContext &C = BB.getContext();
-  for (Instruction &I : BB) {
-    IndexT idx;
-    std::vector<InfoT> info;
-    if (LoadInst *li = dyn_cast<LoadInst>(&I)) {
-      if (li->getType()->isAggregateType()) {
-        visitAggregateValue(nullptr, li->getType(), idx, info, C);
-        IRBuilder<> irb(li);
-        li->replaceAllUsesWith(splitAggregateLoad(li, info, irb));
-        toRemove.push_back(li);
-      }
-    } else if (StoreInst *si = dyn_cast<StoreInst>(&I)) {
-      Value *V = si->getValueOperand();
-      if (V->getType()->isAggregateType()) {
-        visitAggregateValue(dyn_cast_or_null<Constant>(V), V->getType(), idx,
-                            info, C);
-        IRBuilder<> irb(si);
-        splitAggregateStore(si, info, irb);
-        toRemove.push_back(si);
-      }
-    } else if (ReturnInst *ri = dyn_cast<ReturnInst>(&I)) {
-      Value *V = ri->getReturnValue();
-      if (isConstantAggregate(V)) {
-        visitAggregateValue(cast<Constant>(V), V->getType(), idx, info, C);
-        splitConstantReturn(ri, info);
-      }
-    } else if (CallInst *ci = dyn_cast<CallInst>(&I)) {
-      for (unsigned i = 0; i < ci->getNumArgOperands(); ++i) {
-        Value *arg = ci->getArgOperand(i);
-        if (isConstantAggregate(arg)) {
-          info.clear();
-          idx.clear();
-          visitAggregateValue(cast<Constant>(arg), arg->getType(), idx, info,
-                              C);
-          splitConstantArg(ci, i, info);
+bool SplitAggregateValue::runOnFunction(Function &F) {
+  for (auto &BB : F) {
+    std::vector<Instruction *> toRemove;
+    LLVMContext &C = BB.getContext();
+    for (Instruction &I : BB) {
+      IndexT idx;
+      std::vector<InfoT> info;
+      if (LoadInst *li = dyn_cast<LoadInst>(&I)) {
+        if (li->getType()->isAggregateType()) {
+          visitAggregateValue(nullptr, li->getType(), idx, info, C);
+          IRBuilder<> irb(li);
+          li->replaceAllUsesWith(splitAggregateLoad(li, info, irb));
+          toRemove.push_back(li);
+        }
+      } else if (StoreInst *si = dyn_cast<StoreInst>(&I)) {
+        Value *V = si->getValueOperand();
+        if (V->getType()->isAggregateType()) {
+          visitAggregateValue(dyn_cast_or_null<Constant>(V), V->getType(), idx,
+                              info, C);
+          IRBuilder<> irb(si);
+          splitAggregateStore(si, info, irb);
+          toRemove.push_back(si);
+        }
+      } else if (ReturnInst *ri = dyn_cast<ReturnInst>(&I)) {
+        Value *V = ri->getReturnValue();
+        if (isConstantAggregate(V)) {
+          visitAggregateValue(cast<Constant>(V), V->getType(), idx, info, C);
+          splitConstantReturn(ri, info);
+        }
+      } else if (CallInst *ci = dyn_cast<CallInst>(&I)) {
+        for (unsigned i = 0; i < ci->getNumArgOperands(); ++i) {
+          Value *arg = ci->getArgOperand(i);
+          if (isConstantAggregate(arg)) {
+            info.clear();
+            idx.clear();
+            visitAggregateValue(cast<Constant>(arg), arg->getType(), idx, info,
+                                C);
+            splitConstantArg(ci, i, info);
+          }
         }
       }
     }
-  }
 
-  for (auto &i : toRemove)
-    i->eraseFromParent();
+    for (auto &i : toRemove)
+      i->eraseFromParent();
+  }
   return true;
 }
 
diff --git a/lib/utils/Devirt.cpp b/lib/utils/Devirt.cpp
index 5722830db..a1e9fad27 100644
--- a/lib/utils/Devirt.cpp
+++ b/lib/utils/Devirt.cpp
@@ -12,6 +12,8 @@
 #include "utils/Devirt.h"
 
 #include "smack/Debug.h"
+#include "seadsa/InitializePasses.hh"
+#include "utils/InitializePasses.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/ADT/Statistic.h"
 
@@ -21,17 +23,10 @@
 
 using namespace llvm;
 
-// Pass ID variable
-char Devirtualize::ID = 0;
-
 // Pass statistics
 STATISTIC(FuncAdded, "Number of bounce functions added");
 STATISTIC(CSConvert, "Number of call sites converted");
 
-// Pass registration
-RegisterPass<Devirtualize>
-Z ("devirt", "Devirtualize indirect function calls");
-
 const bool SKIP_INCOMPLETE_NODES = false;
 
 //
@@ -519,3 +514,12 @@ Devirtualize::runOnModule (Module & M) {
   //
   return true;
 }
+
+// Pass ID variable
+char Devirtualize::ID = 0;
+
+using namespace seadsa;
+// Pass registration
+INITIALIZE_PASS_BEGIN(Devirtualize, "devirt", "Devirtualize indirect function calls", false, false)
+INITIALIZE_PASS_DEPENDENCY(CompleteCallGraph)
+INITIALIZE_PASS_END(Devirtualize, "devirt", "Devirtualize indirect function calls", false, false)
diff --git a/sea-dsa b/sea-dsa
index 39ddfbfcb..584fd4d69 160000
--- a/sea-dsa
+++ b/sea-dsa
@@ -1 +1 @@
-Subproject commit 39ddfbfcbc58287bca76bc7ff2539f7e97635eac
+Subproject commit 584fd4d69f4e28b5639f9ff33fcd11e9b0a1dfc5
diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp
index 136b1c0a9..aed597d4c 100644
--- a/tools/llvm2bpl/llvm2bpl.cpp
+++ b/tools/llvm2bpl/llvm2bpl.cpp
@@ -42,6 +42,7 @@
 #include "utils/MergeGEP.h"
 #include "utils/SimplifyExtractValue.h"
 #include "utils/SimplifyInsertValue.h"
+#include "utils/InitializePasses.h"
 
 static llvm::cl::opt<std::string>
     InputFilename(llvm::cl::Positional,
@@ -146,6 +147,7 @@ int main(int argc, char **argv) {
   llvm::initializeAnalysis(Registry);
 
   llvm::initializeCodifyStaticInitsPass(Registry);
+  llvm::initializeDevirtualizePass(Registry);
 
   llvm::legacy::PassManager pass_manager;
 

From 90511e5db58657e5ddcab9c24072bcc1f17e2ced Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Mon, 17 Aug 2020 19:35:34 -0600
Subject: [PATCH 07/20] Satisfy clang-format

---
 lib/smack/Prelude.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/smack/Prelude.cpp b/lib/smack/Prelude.cpp
index bcb867aed..2e270b3f5 100644
--- a/lib/smack/Prelude.cpp
+++ b/lib/smack/Prelude.cpp
@@ -980,7 +980,7 @@ void IntOpGen::generateMemOps(std::stringstream &s) const {
       } else {
         auto loadBody = prelude.mapSelExpr(0);
         auto storeBody = prelude.mapUpdExpr(0, Expr::bvExtract(valExpr, 8, 0));
-        for (unsigned i = 1; i<size>> 3; ++i) {
+        for (unsigned i = 1; i<size> > 3; ++i) {
           unsigned lowerIdx = i << 3;
           unsigned upperIdx = lowerIdx + 8;
           loadBody = Expr::bvConcat(prelude.mapSelExpr(i), loadBody);

From 1993d96a17a1eaeaf03b44bfc0653e479af36726 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Mon, 17 Aug 2020 21:39:19 -0600
Subject: [PATCH 08/20] Satisfy clang-format without compilation error

---
 lib/smack/Prelude.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/smack/Prelude.cpp b/lib/smack/Prelude.cpp
index 2e270b3f5..eca7a295f 100644
--- a/lib/smack/Prelude.cpp
+++ b/lib/smack/Prelude.cpp
@@ -980,7 +980,7 @@ void IntOpGen::generateMemOps(std::stringstream &s) const {
       } else {
         auto loadBody = prelude.mapSelExpr(0);
         auto storeBody = prelude.mapUpdExpr(0, Expr::bvExtract(valExpr, 8, 0));
-        for (unsigned i = 1; i<size> > 3; ++i) {
+        for (unsigned i = 1; i < (size >> 3); ++i) {
           unsigned lowerIdx = i << 3;
           unsigned upperIdx = lowerIdx + 8;
           loadBody = Expr::bvConcat(prelude.mapSelExpr(i), loadBody);

From 7aa4a3eb0fc2fea59ed6e716a118ce59dea1fd0a Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Tue, 18 Aug 2020 12:52:27 -0600
Subject: [PATCH 09/20] Added support for FNeg operation

---
 include/smack/SmackInstGenerator.h |  1 +
 include/smack/SmackRep.h           |  4 ++++
 lib/smack/Naming.cpp               |  1 +
 lib/smack/Prelude.cpp              |  3 ++-
 lib/smack/SmackInstGenerator.cpp   | 14 ++++++++++++++
 lib/smack/SmackRep.cpp             | 13 +++++++++++++
 6 files changed, 35 insertions(+), 1 deletion(-)

diff --git a/include/smack/SmackInstGenerator.h b/include/smack/SmackInstGenerator.h
index e65db1f5e..f5c137830 100644
--- a/include/smack/SmackInstGenerator.h
+++ b/include/smack/SmackInstGenerator.h
@@ -68,6 +68,7 @@ class SmackInstGenerator : public llvm::InstVisitor<SmackInstGenerator> {
   void visitUnreachableInst(llvm::UnreachableInst &i);
 
   void visitBinaryOperator(llvm::BinaryOperator &I);
+  void visitUnaryOperator(llvm::UnaryOperator &I);
 
   void visitExtractElementInst(llvm::ExtractElementInst &I);
   void visitInsertElementInst(llvm::InsertElementInst &I);
diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h
index 875a6ad90..53043330f 100644
--- a/include/smack/SmackRep.h
+++ b/include/smack/SmackRep.h
@@ -85,6 +85,7 @@ class SmackRep {
   bool isFpArithOp(unsigned opcode);
   const Expr *bop(unsigned opcode, const llvm::Value *lhs,
                   const llvm::Value *rhs, const llvm::Type *t);
+  const Expr *uop(const llvm::Value *op);
   const Expr *cmp(unsigned predicate, const llvm::Value *lhs,
                   const llvm::Value *rhs, bool isUnsigned);
   const Expr *select(const llvm::Value *condVal, const llvm::Value *trueVal,
@@ -147,6 +148,9 @@ class SmackRep {
   const Expr *bop(const llvm::BinaryOperator *BO);
   const Expr *bop(const llvm::ConstantExpr *CE);
 
+  const Expr *uop(const llvm::UnaryOperator *UO);
+  const Expr *uop(const llvm::ConstantExpr *CE);
+
   const Expr *cmp(const llvm::CmpInst *I);
   const Expr *cmp(const llvm::ConstantExpr *CE);
 
diff --git a/lib/smack/Naming.cpp b/lib/smack/Naming.cpp
index 18d437e23..f4dd71358 100644
--- a/lib/smack/Naming.cpp
+++ b/lib/smack/Naming.cpp
@@ -121,6 +121,7 @@ const std::map<unsigned, std::string> Naming::INSTRUCTION_TABLE{
     {Instruction::FMul, "$fmul"},
     {Instruction::FDiv, "$fdiv"},
     {Instruction::FRem, "$frem"},
+    {Instruction::FNeg, "$fneg"},
     {Instruction::ShuffleVector, "$shufflevector"},
     {Instruction::InsertElement, "$insertelement"},
     {Instruction::ExtractElement, "$extractelement"}};
diff --git a/lib/smack/Prelude.cpp b/lib/smack/Prelude.cpp
index eca7a295f..b72839886 100644
--- a/lib/smack/Prelude.cpp
+++ b/lib/smack/Prelude.cpp
@@ -1333,6 +1333,7 @@ const Attr *FpOp::fpAttrFunc(std::string opName) {
       {"fdiv", "fp.div"},
       {"frem", "fp.rem"},
       {"fma", "fp.fma"},
+      {"fneg", "fp.neg"},
       {"isnormal", "fp.isNormal"},
       {"issubnormal", "fp.isSubnormal"},
       {"iszero", "fp.isZero"},
@@ -1388,7 +1389,7 @@ void FpOpGen::generateArithOps(std::stringstream &s) const {
       {"abs", 1, false}, {"round", 1, true}, {"sqrt", 1, true},
       {"fadd", 2, true}, {"fsub", 2, true},  {"fmul", 2, true},
       {"fdiv", 2, true}, {"frem", 2, false}, {"min", 2, false},
-      {"max", 2, false}, {"fma", 3, true}};
+      {"max", 2, false}, {"fma", 3, true},   {"fneg", 1, false}};
 
   for (auto &f : fpArithOps) {
     if (SmackOptions::FloatEnabled)
diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp
index f8ca4c702..70b93fe9a 100644
--- a/lib/smack/SmackInstGenerator.cpp
+++ b/lib/smack/SmackInstGenerator.cpp
@@ -372,6 +372,20 @@ void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator &I) {
   emit(Stmt::assign(rep->expr(&I), E));
 }
 
+/******************************************************************************/
+/*                   UNARY                    OPERATIONS                     */
+/******************************************************************************/
+
+void SmackInstGenerator::visitUnaryOperator(llvm::UnaryOperator &I) {
+  assert(I.getOpcode() == Instruction::FNeg && !isa<VectorType>(I.getType()) &&
+         "Unsupported unary operation!");
+  processInstruction(I);
+  SmackWarnings::warnIfUnsound(std::string("floating-point arithmetic ") +
+                                   I.getOpcodeName(),
+                               SmackOptions::FloatEnabled, currBlock, &I);
+  emit(Stmt::assign(rep->expr(&I), rep->uop(&I)));
+}
+
 /******************************************************************************/
 /*                   VECTOR                    OPERATIONS                     */
 /******************************************************************************/
diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp
index 40dfe0bef..61ec40dbd 100644
--- a/lib/smack/SmackRep.cpp
+++ b/lib/smack/SmackRep.cpp
@@ -924,6 +924,19 @@ const Expr *SmackRep::bop(unsigned opcode, const llvm::Value *lhs,
   return Expr::fn(opName(fn, {t}), expr(lhs), expr(rhs));
 }
 
+const Expr *SmackRep::uop(const llvm::ConstantExpr *CE) {
+  return uop(CE->getOperand(0));
+}
+
+const Expr *SmackRep::uop(const llvm::UnaryOperator *UO) {
+  return uop(UO->getOperand(0));
+}
+
+const Expr *SmackRep::uop(const llvm::Value *op) {
+  std::string fn = Naming::INSTRUCTION_TABLE.at(Instruction::FNeg);
+  return Expr::fn(opName(fn, {op->getType()}), expr(op));
+}
+
 const Expr *SmackRep::cmp(const llvm::CmpInst *I) {
   return cmp(I->getPredicate(), I->getOperand(0), I->getOperand(1),
              I->isUnsigned());

From 1fa5dd24267811d9708e22cd867672794dc2a9f3 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Tue, 18 Aug 2020 17:47:15 -0600
Subject: [PATCH 10/20] Replaced stripPointerCasts with
 stripPointerCastsAndAliases

---
 lib/smack/SmackInstGenerator.cpp | 8 ++++----
 lib/smack/SmackRep.cpp           | 4 ++--
 lib/utils/Devirt.cpp             | 4 ++--
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp
index 70b93fe9a..e3d147a55 100644
--- a/lib/smack/SmackInstGenerator.cpp
+++ b/lib/smack/SmackInstGenerator.cpp
@@ -200,7 +200,7 @@ void SmackInstGenerator::generatePhiAssigns(llvm::Instruction &ti) {
 
       llvm::PHINode *phi = llvm::cast<llvm::PHINode>(s);
       if (llvm::Value *v = phi->getIncomingValueForBlock(block)) {
-        v = v->stripPointerCasts();
+        v = v->stripPointerCastsAndAliases();
         lhs.push_back(rep->expr(phi));
         rhs.push_back(rep->expr(v));
       }
@@ -519,7 +519,7 @@ void SmackInstGenerator::visitLoadInst(llvm::LoadInst &li) {
 void SmackInstGenerator::visitStoreInst(llvm::StoreInst &si) {
   processInstruction(si);
   const llvm::Value *P = si.getPointerOperand();
-  const llvm::Value *V = si.getValueOperand()->stripPointerCasts();
+  const llvm::Value *V = si.getValueOperand()->stripPointerCastsAndAliases();
   assert(!V->getType()->isAggregateType() && "Unexpected store value.");
 
   if (isa<VectorType>(V->getType())) {
@@ -649,7 +649,7 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) {
   Function *f = ci.getCalledFunction();
   if (!f) {
     assert(ci.getCalledValue() && "Called value is null");
-    f = cast<Function>(ci.getCalledValue()->stripPointerCasts());
+    f = cast<Function>(ci.getCalledValue()->stripPointerCastsAndAliases());
   }
 
   std::string name = f->hasName() ? f->getName() : "";
@@ -848,7 +848,7 @@ void SmackInstGenerator::visitDbgValueInst(llvm::DbgValueInst &dvi) {
       auto currInst = std::prev(nextInst);
       if (currInst != dvi.getParent()->begin()) {
         const Instruction &pi = *std::prev(currInst);
-        V = V->stripPointerCasts();
+        V = V->stripPointerCastsAndAliases();
         if (!llvm::isa<const PHINode>(&pi) &&
             V == llvm::dyn_cast<const Value>(&pi))
           emit(recordProcedureCall(
diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp
index 61ec40dbd..e78b5513b 100644
--- a/lib/smack/SmackRep.cpp
+++ b/lib/smack/SmackRep.cpp
@@ -355,7 +355,7 @@ const Stmt *SmackRep::valueAnnotation(const CallInst &CI) {
 
   assert(CI.getNumArgOperands() > 0 && "Expected at least one argument.");
   assert(CI.getNumArgOperands() <= 2 && "Expected at most two arguments.");
-  const Value *V = CI.getArgOperand(0)->stripPointerCasts();
+  const Value *V = CI.getArgOperand(0)->stripPointerCastsAndAliases();
 
   if (CI.getNumArgOperands() == 1) {
     name = indexedName(Naming::VALUE_PROC, {type(V->getType())});
@@ -788,7 +788,7 @@ const Expr *SmackRep::expr(const llvm::Value *v, bool isConstIntUnsigned) {
   using namespace llvm;
 
   if (isa<const Constant>(v)) {
-    v = v->stripPointerCasts();
+    v = v->stripPointerCastsAndAliases();
   }
 
   if (isa<GlobalValue>(v)) {
diff --git a/lib/utils/Devirt.cpp b/lib/utils/Devirt.cpp
index a1e9fad27..ecb281a10 100644
--- a/lib/utils/Devirt.cpp
+++ b/lib/utils/Devirt.cpp
@@ -168,7 +168,7 @@ Devirtualize::findInCache (const CallSite & CS,
     // Check the type of the function pointer and the argumentsa
     PointerType* PT = dyn_cast<PointerType>(bounceFunc->arg_begin()->getType());
     assert(PT);
-    if (CS.getCalledValue()->stripPointerCasts()->getType() != PT)
+    if (CS.getCalledValue()->stripPointerCastsAndAliases()->getType() != PT)
       continue;
 
     FunctionType* FT = dyn_cast<FunctionType>(PT->getElementType());
@@ -456,7 +456,7 @@ Devirtualize::processCallSite (CallSite &CS) {
   // First, determine if this is a direct call.  If so, then just ignore it.
   //
   Value * CalledValue = CS.getCalledValue();
-  if (isa<Function>(CalledValue->stripPointerCasts()))
+  if (isa<Function>(CalledValue->stripPointerCastsAndAliases()))
     return;
 
   //

From 2b31cfa6c16b05bfa97917e9c9550d801c4d3624 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Tue, 18 Aug 2020 19:19:57 -0600
Subject: [PATCH 11/20] Added sea-dsa's `RemovePtrToInt` pass

Fixes #602
---
 sea-dsa                     | 2 +-
 tools/llvm2bpl/llvm2bpl.cpp | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/sea-dsa b/sea-dsa
index 584fd4d69..6034037da 160000
--- a/sea-dsa
+++ b/sea-dsa
@@ -1 +1 @@
-Subproject commit 584fd4d69f4e28b5639f9ff33fcd11e9b0a1dfc5
+Subproject commit 6034037da3a984fd1de4c03a45ea11441f74cc16
diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp
index aed597d4c..9035b561e 100644
--- a/tools/llvm2bpl/llvm2bpl.cpp
+++ b/tools/llvm2bpl/llvm2bpl.cpp
@@ -43,6 +43,8 @@
 #include "utils/SimplifyExtractValue.h"
 #include "utils/SimplifyInsertValue.h"
 #include "utils/InitializePasses.h"
+#include "seadsa/InitializePasses.hh"
+#include "seadsa/support/RemovePtrToInt.hh"
 
 static llvm::cl::opt<std::string>
     InputFilename(llvm::cl::Positional,
@@ -148,9 +150,11 @@ int main(int argc, char **argv) {
 
   llvm::initializeCodifyStaticInitsPass(Registry);
   llvm::initializeDevirtualizePass(Registry);
+  llvm::initializeRemovePtrToIntPass(Registry);
 
   llvm::legacy::PassManager pass_manager;
 
+  pass_manager.add(seadsa::createRemovePtrToIntPass());
   pass_manager.add(llvm::createLowerSwitchPass());
   // pass_manager.add(llvm::createCFGSimplificationPass());
   // Shaobo: sea-dsa is inconsistent with the pass below.

From d09ab83a6b94f7bdeb05fc8f037e1007722a3006 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Wed, 19 Aug 2020 10:22:37 -0600
Subject: [PATCH 12/20] Upgraded sea-dsa

---
 sea-dsa | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sea-dsa b/sea-dsa
index 6034037da..f7658f8fe 160000
--- a/sea-dsa
+++ b/sea-dsa
@@ -1 +1 @@
-Subproject commit 6034037da3a984fd1de4c03a45ea11441f74cc16
+Subproject commit f7658f8feb6ec6c664730053e3a2636b8df6ff9a

From 5c76344806b18ca2ab8f4a8ee4d664b3a199c7c1 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Wed, 19 Aug 2020 23:01:53 -0600
Subject: [PATCH 13/20] Upgraded sea-dsa

---
 sea-dsa | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sea-dsa b/sea-dsa
index f7658f8fe..2483d56f6 160000
--- a/sea-dsa
+++ b/sea-dsa
@@ -1 +1 @@
-Subproject commit f7658f8feb6ec6c664730053e3a2636b8df6ff9a
+Subproject commit 2483d56f68ad08336624568c0d8ae2ddf9820725

From 88416311da3d9039c6519e491a4c184054d5ddd7 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Thu, 20 Aug 2020 12:16:36 -0600
Subject: [PATCH 14/20] Clang-format llvm2bpl.cpp

---
 tools/llvm2bpl/llvm2bpl.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp
index 9035b561e..61427c5c9 100644
--- a/tools/llvm2bpl/llvm2bpl.cpp
+++ b/tools/llvm2bpl/llvm2bpl.cpp
@@ -24,6 +24,8 @@
 #include "llvm/Support/raw_ostream.h"
 #include "llvm/Target/TargetMachine.h"
 
+#include "seadsa/InitializePasses.hh"
+#include "seadsa/support/RemovePtrToInt.hh"
 #include "smack/AddTiming.h"
 #include "smack/BplFilePrinter.h"
 #include "smack/CodifyStaticInits.h"
@@ -39,12 +41,10 @@
 #include "smack/SplitAggregateValue.h"
 #include "smack/VerifierCodeMetadata.h"
 #include "utils/Devirt.h"
+#include "utils/InitializePasses.h"
 #include "utils/MergeGEP.h"
 #include "utils/SimplifyExtractValue.h"
 #include "utils/SimplifyInsertValue.h"
-#include "utils/InitializePasses.h"
-#include "seadsa/InitializePasses.hh"
-#include "seadsa/support/RemovePtrToInt.hh"
 
 static llvm::cl::opt<std::string>
     InputFilename(llvm::cl::Positional,

From 6186e27f73e008f5e0a929f4899d0b159a30edf4 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Thu, 20 Aug 2020 23:33:47 -0600
Subject: [PATCH 15/20] Updated documentations to LLVM 10

---
 docs/installation.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/docs/installation.md b/docs/installation.md
index 7a7745d00..183e158dd 100644
--- a/docs/installation.md
+++ b/docs/installation.md
@@ -80,8 +80,8 @@ to Docker's official documentation.
 
 SMACK depends on the following projects:
 
-* [LLVM][] version [9.0.1][LLVM-9.0.1]
-* [Clang][] version [9.0.1][Clang-9.0.1]
+* [LLVM][] version [10.0.1][LLVM-10.0.1]
+* [Clang][] version [10.0.1][Clang-10.0.1]
 * [Boost][] version 1.55 or greater
 * [Python][] version 3.6.8 or greater
 * [Ninja][] version 1.5.1 or greater
@@ -210,9 +210,9 @@ shell in the `test` directory by executing
 [CMake]: http://www.cmake.org
 [Python]: http://www.python.org
 [LLVM]: http://llvm.org
-[LLVM-9.0.1]: http://llvm.org/releases/download.html#9.0.1
+[LLVM-10.0.1]: http://llvm.org/releases/download.html#10.0.1
 [Clang]: http://clang.llvm.org
-[Clang-9.0.1]: http://llvm.org/releases/download.html#9.0.1
+[Clang-10.0.1]: http://llvm.org/releases/download.html#10.0.1
 [Boogie]: https://github.com/boogie-org/boogie
 [Corral]: https://github.com/boogie-org/corral
 [Z3]: https://github.com/Z3Prover/z3/

From f02bfb54f5df8ab69e6ed296fa499a38ceb3236c Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Tue, 25 Aug 2020 12:19:51 -0600
Subject: [PATCH 16/20] Upgrade sea-dsa

---
 sea-dsa | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sea-dsa b/sea-dsa
index 2483d56f6..77fa9ef09 160000
--- a/sea-dsa
+++ b/sea-dsa
@@ -1 +1 @@
-Subproject commit 2483d56f68ad08336624568c0d8ae2ddf9820725
+Subproject commit 77fa9ef0935aee4085a5ecdf52f67fcf2f87513b

From 8d9f8c723ff81ecb8678a68f05d2b7fcd8be9539 Mon Sep 17 00:00:00 2001
From: "Mark S. Baranowski" <mark.s.baranowski@gmail.com>
Date: Wed, 26 Aug 2020 13:57:34 -0600
Subject: [PATCH 17/20] Upgrade rustc version

---
 bin/versions | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bin/versions b/bin/versions
index fc5b9a60b..2ad20a6f3 100644
--- a/bin/versions
+++ b/bin/versions
@@ -7,4 +7,4 @@ SYMBOOGLIX_COMMIT=ccb2e7f2b3
 LOCKPWN_COMMIT=12ba58f1ec
 LLVM_SHORT_VERSION=10
 LLVM_FULL_VERSION=10.0.1
-RUST_VERSION=2020-05-21
+RUST_VERSION=2020-08-23

From eb3dee34316501a57b92589a0fb26db2ae22d46f Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sun, 30 Aug 2020 21:16:48 -0600
Subject: [PATCH 18/20] Updated CVC4 version to 1.8

---
 bin/versions | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bin/versions b/bin/versions
index 2ad20a6f3..c71e9e983 100644
--- a/bin/versions
+++ b/bin/versions
@@ -1,5 +1,5 @@
 Z3_VERSION=4.8.8
-CVC4_VERSION=1.7
+CVC4_VERSION=1.8
 YICES2_VERSION=2.6.2
 BOOGIE_VERSION=2.7.15
 CORRAL_VERSION=1.0.12

From ba28e597000c4c667f82f35662b79b325a6f1877 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 3 Sep 2020 09:45:41 -0600
Subject: [PATCH 19/20] Fixing discrepancy between bit-vector flag in llvm2bpl
 and Python script

Fixes #611
---
 lib/smack/SmackWarnings.cpp | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/lib/smack/SmackWarnings.cpp b/lib/smack/SmackWarnings.cpp
index 8746c10e3..b7bc2b1cd 100644
--- a/lib/smack/SmackWarnings.cpp
+++ b/lib/smack/SmackWarnings.cpp
@@ -38,8 +38,12 @@ SmackWarnings::getUnsetFlags(RequiredFlagsT requiredFlags) {
 
 std::string SmackWarnings::getFlagStr(UnsetFlagsT flags) {
   std::string ret = "";
-  for (auto f : flags)
-    ret += ("--" + f->ArgStr.str() + " ");
+  for (auto f : flags) {
+    if (f->ArgStr.str() == "bit-precise")
+      ret += ("--integer-encoding=bit-vector ");
+    else
+      ret += ("--" + f->ArgStr.str() + " ");
+  }
   return ret;
 }
 

From 4666d43134a5949cd2230cf0327b99bdf95e4f51 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sat, 5 Sep 2020 17:28:55 -0600
Subject: [PATCH 20/20] Bumped version number to 2.6.0

---
 Doxyfile             | 2 +-
 share/smack/reach.py | 2 +-
 share/smack/top.py   | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Doxyfile b/Doxyfile
index a23d248f2..9bc8b160c 100644
--- a/Doxyfile
+++ b/Doxyfile
@@ -5,7 +5,7 @@
 #---------------------------------------------------------------------------
 DOXYFILE_ENCODING      = UTF-8
 PROJECT_NAME           = smack
-PROJECT_NUMBER         = 2.5.0
+PROJECT_NUMBER         = 2.6.0
 PROJECT_BRIEF          = "A bounded software verifier."
 PROJECT_LOGO           =
 OUTPUT_DIRECTORY       = docs
diff --git a/share/smack/reach.py b/share/smack/reach.py
index 3aef8c852..b06b7462a 100755
--- a/share/smack/reach.py
+++ b/share/smack/reach.py
@@ -11,7 +11,7 @@
 from smackgen import *
 from smackverify import *
 
-VERSION = '2.5.0'
+VERSION = '2.6.0'
 
 
 def reachParser():
diff --git a/share/smack/top.py b/share/smack/top.py
index d46664510..06343c8be 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -13,7 +13,7 @@
 from .replay import replay_error_trace
 from .frontend import link_bc_files, frontends, languages, extra_libs
 
-VERSION = '2.5.0'
+VERSION = '2.6.0'
 
 
 def results(args):