Softening "function unreachable" asserts

[jordr]

Running vanilla Chopper on the is_lower benchmark from KLEE:

/*
 * First KLEE tutorial: testing a small function
 */

#include <klee/klee.h>

int my_islower(int x) {
  if (x >= 'a' && x <= 'z')
    return 1;
  else return 0;
}

int main() {
  char c;
  klee_make_symbolic(&c, sizeof(c), "input");
  return my_islower(c);

Skipping main is the easiest way to trigger the assert:

$ kleegacy -libc=klee -search=dfs -skip-functions=main islower.bc
KLEE: output directory is "/home/ubuntu/code/chopper/examples/islower/klee-out-9"
Using STP solver backend
KLEE: Runnining pointer analysis...
KLEE: Runnining reachability analysis...
function '__wrap_main' is not found
KLEE: Runnining mod-ref analysis...
function '__wrap_main' is not found (or unreachable)
kleegacy: /home/ubuntu/code/chopper/lib/Analysis/ModRefAnalysis.cpp:61: void ModRefAnalysis::run(): Assertion `false' failed.
0  kleegacy        0x0000561c70fc2992 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  kleegacy        0x0000561c70fc228c
2  libpthread.so.0 0x00007f3af3c52890
3  libc.so.6       0x00007f3af2b20e97 gsignal + 199
4  libc.so.6       0x00007f3af2b22801 abort + 321
5  libc.so.6       0x00007f3af2b1239a
6  libc.so.6       0x00007f3af2b12412
7  kleegacy        0x0000561c70675874 ModRefAnalysis::run() + 434
8  kleegacy        0x0000561c705d8b2c klee::KModule::prepare(klee::Interpreter::ModuleOptions const&, std::vector<klee::Interpreter::SkippedFunctionOption, std::allocator<klee::Interpreter::SkippedFunctionOption> > const&, klee::InterpreterHandler*, ReachabilityAnalysis*, Inliner*, AAPass*, ModRefAnalysis*, Cloner*, SliceGenerator*) + 3550
9  kleegacy        0x0000561c70520640 klee::Executor::setModule(llvm::Module*, klee::Interpreter::ModuleOptions const&) + 1656
10 kleegacy        0x0000561c70503b35 main + 4654
11 libc.so.6       0x00007f3af2b03b97 __libc_start_main + 231
12 kleegacy        0x0000561c704fd71a _start + 42
[1]    5458 abort (core dumped)  kleegacy -libc=klee -search=dfs -skip-functions=main islower.bc

It does not seem to me like it is a critical error, and so I wrote this patch in order to recover and continue with the analysis:

diff --git a/lib/Analysis/ModRefAnalysis.cpp b/lib/Analysis/ModRefAnalysis.cpp
index fc154c5a..b15c6ce2 100644
--- a/lib/Analysis/ModRefAnalysis.cpp
+++ b/lib/Analysis/ModRefAnalysis.cpp
@@ -54,15 +55,23 @@ void ModRefAnalysis::run() {
         assert(false);
     }
 
+    vector<vector<string>::iterator> todel;
     for (vector<string>::iterator i = targets.begin(); i != targets.end(); i++) {
         string name = *i;
         Function *f = module->getFunction(name);
         if (!f) {
             errs() << "function '" << name << "' is not found (or unreachable)\n";
-            assert(false);
+            todel.push_back(i);
+            continue; // JOR: TODO: ensure safety
         }
         targetFunctions.push_back(f);
     }
+    for (vector<vector<string>::iterator>::iterator d = todel.begin(); d != todel.end(); d++) {
+        targets.erase(*d); // JOR: not sure this helps
+    }

and do the same in ReachabilityAnalysis.

On larger benchmarks like bc, a lot of functions may be found unreachable when trying to skip (almost) everything:

[791b55] KLEE: Runnining mod-ref analysis...
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yywrap' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'bc_out_long' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'usage' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_delete_buffer' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'bc_str2num' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function '__sigdelset' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_switch_to_buffer' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_flush_buffer' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'new_yy_file' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'find_id' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_scan_buffer' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'get_var' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'long_val' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'copy_array' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'pn' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'assign' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'pv' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_scan_string' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'num2str' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_scan_bytes' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'bc_is_near_zero' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_load_buffer_state' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_init_buffer' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'bc_raisemod' is not found (or unreachable)

Q: Is this a safe way to proceed with this issue? Is it correct to assume that this assertion is not critical?