about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorNguyễn Gia Phong <cnx@loang.net>2023-07-31 16:46:13 +0900
committerNguyễn Gia Phong <cnx@loang.net>2024-03-05 17:26:57 +0900
commitbb2337248e770863b8e488c8f02adf90369a624f (patch)
treed83f663cd84d9845d673c1be39b060ff84c06cec
parentd37a4bca5dd23feabf0e4554a997a4b505b47f05 (diff)
downloadklee-bb2337248e770863b8e488c8f02adf90369a624f.tar.gz
Fallback on UB
This is not benefitting off UBSan, but there are too many moving parts
now that a common denominator is needed for me to mentally keep
track of things.

(Yes, it's embarrassing that I commit less often working
on software engineering research software, now I'm paying the price.)-;
-rw-r--r--lib/Core/Executor.cpp4
-rw-r--r--shell.nix4
2 files changed, 6 insertions, 2 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 6be77eb1..e0ab9f84 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -4135,6 +4135,10 @@ void Executor::terminateStateOnError(ExecutionState &state,
     interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix);
   }
 
+  metaEnvVars[state.patchNo] = state.metaEnvVar;
+  getConstraintLog(state, state.formula, Interpreter::SMTLIB2);
+  if (exitStates[state.patchNo].insert(&state).second)
+    searchDifferentiators(&state);
   terminateState(state, terminationType);
 
   if (shouldExitOn(terminationType))
diff --git a/shell.nix b/shell.nix
index 570f39bd..8e14a489 100644
--- a/shell.nix
+++ b/shell.nix
@@ -1,10 +1,10 @@
 with import <nixpkgs> {};
 let symbdiff = callPackage ./tools/symbdiff { };
 in mkShell {
-  packages = [ clang symbdiff ];
+  packages = [ llvmPackages_12.clang symbdiff ];
   shellHook = ''
     # clang -emit-llvm -c -DKLEE_RUNTIME metaprogram.c for bitcode
     # clang -o metaprogram{,.c} for binary
-    alias clang='clang -g -O0 -Xclang -disable-O0-optnone'
+    alias clang='clang -g -O0 -Xclang -disable-O0-optnone -fsanitize=undefined -fno-sanitize=local-bounds,function,vptr'
  '';
 }