Nullptr deref test

.github/workflows/Test-Suite.yml

@@ -16,7 +16,7 @@ jobs:
   # This workflow contains a single job called "build"
   linux_build:
     # The type of runner that the job will run on
-    runs-on: ubuntu-20.04
+    runs-on: ubuntu-24.04
 
     # Steps represent a sequence of tasks that will be executed as part of the job
     steps:
@@ -26,9 +26,11 @@ jobs:
       - name: env-setup
         run: |
             sudo apt-get update
-            sudo apt-get install unzip tar
-            wget https://github.com/llvm/llvm-project/releases/download/llvmorg-16.0.0/clang+llvm-16.0.0-x86_64-linux-gnu-ubuntu-18.04.tar.xz
-            mkdir -p "/opt/llvm" && tar -xf clang+llvm-16.0.0-x86_64-linux-gnu-ubuntu-18.04.tar.xz -C "/opt/llvm" --strip-components 1
+            sudo add-apt-repository -y ppa:ubuntu-toolchain-r/test
+            sudo apt-get update
+            sudo apt-get install cmake gcc g++ nodejs doxygen graphviz lcov libncurses5-dev libtinfo6 libzstd-dev unzip tar
+            wget https://github.com/SVF-tools/SVF/releases/download/SVF-3.0/llvm-16.0.0-ubuntu24-rtti-x86-64.tar.gz
+            mkdir -p "/opt/llvm" && tar -xf llvm-16.0.0-ubuntu24-rtti-x86-64.tar.gz -C "/opt/llvm" --strip-components 1
             echo "/opt/llvm/bin" >> $GITHUB_PATH
 
       - name: stash-changes

CMakeLists.txt

@@ -269,7 +269,7 @@ endforeach()
 # Run with: (ctest -R diff-perf-cruxbc-small -VV)
 set(diff_tests_cruxbc_small
   dc bc libbz2.so bunzip2 htop)
-set(cmdw "wpa -vfspta -dump-vfg -dump-json=ir.json")
+set(cmdw "wpa -vfspta -dump-vfg")
 string(REPLACE " " ";" commandtempw ${cmdw})
 set(commandw ${commandtempw})
 foreach(file ${diff_tests_cruxbc_small})
@@ -289,7 +289,7 @@ endforeach()
 # Crux bc Big: Filesystem & Performance regression testing
 # Run with (ctest -R diff-perf-cruxbc-big -VV)
 set(diff_tests_cruxbc_big libcurl.so bash)
-set(cmdw "wpa -ander -dump-json=ir.json")
+set(cmdw "wpa -ander")
 string(REPLACE " " ";" commandtempw ${cmdw})
 set(commandw ${commandtempw})
 foreach(file ${diff_tests_cruxbc_big})
@@ -326,19 +326,37 @@ foreach(filename ${ae_overflow_files})
           COMMAND ae -overflow -field-limit=1024 ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
           WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
   )
+  add_test(
+          NAME ae_recursion_tests/${filename}-widen-narrow
+          COMMAND ae -overflow -handle-recur=widen-narrow -field-limit=1024 ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
+          WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
+  )
 endforeach()
 
-# loops over ae_nullptr_files and run "ae $bc_file"
-file(GLOB ae_nullptr_files RELATIVE ${CMAKE_CURRENT_SOURCE_DIR} "${CMAKE_CURRENT_SOURCE_DIR}/test_cases_bc/ae_nullptr_deref_tests/*.bc")
+# loops over ae_nullptr_deref_files and run "ae -null-ptr-deref $bc_file"
+file(GLOB ae_nullptr_deref_files RELATIVE ${CMAKE_CURRENT_SOURCE_DIR} "${CMAKE_CURRENT_SOURCE_DIR}/test_cases_bc/ae_nullptr_deref_tests/*.bc")
 
-foreach(filename ${ae_nullptr_files})
+foreach(filename ${ae_nullptr_deref_files})
   add_test(
-          NAME ae_nullptr/${filename}
-          COMMAND ae -nullptr ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
+          NAME ae_nullptr_deref_tests/${filename}
+          COMMAND ae -null-ptr-deref ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
           WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
   )
+
 endforeach()
 
+# loops over ae_recursion_files and run "ae -overflow $bc_file" under 3 recursion modes
+file(GLOB ae_recursion_files RELATIVE ${CMAKE_CURRENT_SOURCE_DIR} "${CMAKE_CURRENT_SOURCE_DIR}/test_cases_bc/ae_recursion_tests/*.bc")
+
+foreach(filename ${ae_recursion_files})
+  add_test(
+          NAME ae_recursion_tests/${filename}-widen-narrow
+          COMMAND ae -overflow -handle-recur=widen-narrow -field-limit=1024 -widen-delay=10 ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
+          WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
+  )
+endforeach()
+
+
 ## symbolic abstraction tests  (ctest -R symabs -VV)
 set(cmd "ae  -symabs")
 string(REPLACE " " ";" commandtemp ${cmd})

diff_tests/difftest.py

@@ -67,6 +67,8 @@ def comparer_andersen(stats1: Stats, stats2: Stats):
     delta = abs(d1 - d2) / d1
     exceptions = [
         ('basic_cpp_tests/queue-1.cpp.bc', 0.01), # 0.00604714303344439
+        ('basic_cpp_tests/deque-3.cpp.bc', 0.01), # 0.0010105589240854218
+        ('basic_cpp_tests/deque-4.cpp.bc', 0.01), # 0.0010217113665389242
         ('basic_cpp_tests/stack-1.cpp.bc', 0.01), # 0.0022123893805308967
         ('basic_cpp_tests/vector-1.cpp.bc', 0.15), # 0.1426766811269205
         ('basic_cpp_tests/vector-3.cpp.bc', 0.17), # 0.15063392744891338