Special functions, DNR functions

jordr commented 4 years ago

How?

$ klee -libc=uclibc -simplify-sym-indices -search=nurs:covnew -split-search -skip-functions-not=yyparse,bc_copy_num,parse_args,yy_get_next_buffer,yyrestart,klee_init_env,malloc  -w=2d4099,e6e1ab,8b29fc --inline=memcpy,memcmp --posix-runtime bc.bc --sym-args 0 8 16 --sym-files 1 64 --sym-stdin 64 --sym-stdout
[dc58bf] KLEE: ■ ■ ■ ■ ■  malloc
[dc58bf] KLEE: ■ ■ ■ ■ ■  malloc
[dc58bf] KLEE: ■ ■ ■ ■ ■  malloc
[dc58bf] KLEE: ■ ■ ■ ■ ■  malloc
[dc58bf] KLEE: ■ ■ ■ ■ ■  malloc
[dc58bf] KLEE: ■ ■ ■ ■ ■  malloc
[6e6b35] KLEE: ■ ■ ■ ■ ■ ■  yy_fatal_error (skipped)
    #000004408 in yy_get_next_buffer () at /home/ubuntu/code/chopper-experiments/bc/bc-1.06/build/bc/lex.yy.c:1630
    #100003626 in yylex () at /home/ubuntu/code/chopper-experiments/bc/bc-1.06/build/bc/lex.yy.c:1433
    #200001167 in yyparse () at /usr/gnu/share/bison.simple:431
    #300000879 in __user_main (argc=11, argv=94402471993424) at /home/ubuntu/code/chopper-experiments/bc/bc-1.06/build/bc/../../bc/main.c:259
    #400067586 in __uClibc_main (main=94402456888144, argc=11, argv=94402471993424, app_init=0, app_fini=0, rtld_fini=0, stack_end=0) at /home/ubuntu/code/klee-uclibc/libc/misc/internals/__uClibc_main.c:401
    #500073696 in main (=11, =94402471993424)
[d6c361] KLEE: ERROR: /home/ubuntu/code/chopper-experiments/bc/bc-1.06/build/bc/lex.yy.c:1630: reached "unreachable" instruction

This can be manually fixed by adding yy_fatal_error to the list of kept functions

Why?

The function yy_fatal_error looks like:

; Function Attrs: noreturn nounwind uwtable
define internal fastcc void @yy_fatal_error(i8* %msg) #4 {
entry:
  %0 = load %struct._IO_FILE** bitcast (%struct.__STDIO_FILE_STRUCT.188** @stderr to %struct._IO_FILE**), align 8, !dbg !4730, !tbaa !3482
  %call = tail call i32 (%struct._IO_FILE*, i8*, ...)* bitcast (i32 (%struct.__STDIO_FILE_STRUCT.232*, i8*, ...)* @fprintf to i32 (%struct._IO_FILE*, i8*, ...)*)(%struct._IO_FILE* %0, i8* getelementptr inbounds ([4 x i8]* @.str1197, i64 0, i64 0), i8* %m
  tail call void @exit(i32 2) #19, !dbg !4731
  unreachable, !dbg !4731
}

It is called from here:

define internal fastcc i32 @yy_get_next_buffer() #0 {
entry:
  %0 = load %struct.yy_buffer_state** @yy_current_buffer, align 8, !dbg !4671, !tbaa !3482
  %yy_ch_buf = getelementptr inbounds %struct.yy_buffer_state* %0, i64 0, i32 1, !dbg !4671
  %1 = load i8** %yy_ch_buf, align 8, !dbg !4671, !tbaa !4384
  %2 = load i8** @yytext, align 8, !dbg !4672, !tbaa !3482
  %3 = load i8** @yy_c_buf_p, align 8, !dbg !4673, !tbaa !3482
  %4 = load i32* @yy_n_chars, align 4, !dbg !4673, !tbaa !3468
  %add = add nsw i32 %4, 1, !dbg !4673
  %idxprom = sext i32 %add to i64, !dbg !4673
  %arrayidx = getelementptr inbounds i8* %1, i64 %idxprom, !dbg !4673
  %cmp = icmp ugt i8* %3, %arrayidx, !dbg !4673
  br i1 %cmp, label %if.then, label %if.end, !dbg !4673

if.then:                                          ; preds = %entry
  tail call fastcc void @yy_fatal_error(i8* getelementptr inbounds ([56 x i8]* @.str1298, i64 0, i64 0)), !dbg !4675
  unreachable

The issue seems to be that KLEE does not tolerate an unreachable with no !dbg argument.

Proposed fix

Scan all functions to detect those that must end with an unreachable instruction. Detect them as "exception" functions and keep them?

jordr commented 4 years ago

This seems to work well:

Keeper.cpp@generateSkippedTargets

    for(klee::SpecialFunctionHandler::const_iterator sf = klee::SpecialFunctionHandler::begin(), se = klee::SpecialFunctionHandler::end(); sf != se; ++sf) {
      if(strcmp(funClass.key.c_str(), sf->name) == 0) {
        klee::klee_warning("Special function scanned: '%s', doesNotReturn=%d, hasReturnValue=%d", sf->name, sf->doesNotReturn, sf->hasReturnValue);
      }
    }

$ chopit.py -f=insertion_sort,insert_ordered,test,__user_main,main,malloc,bubble_sort --inline=memcpy sort.b
[4814d3] KLEE: WARNING: Special function scanned: 'free', doesNotReturn=0, hasReturnValue=0
[4814d3] KLEE: WARNING: Special function scanned: '__assert_fail', doesNotReturn=1, hasReturnValue=0
[4814d3] KLEE: WARNING: Special function scanned: 'exit', doesNotReturn=1, hasReturnValue=0
[4814d3] KLEE: WARNING: Special function scanned: 'klee_make_symbolic', doesNotReturn=0, hasReturnValue=0
[4814d3] KLEE: WARNING: Special function scanned: 'abort', doesNotReturn=1, hasReturnValue=0
[4814d3] KLEE: WARNING: Special function scanned: 'malloc', doesNotReturn=0, hasReturnValue=1

In bc:

Name	DoesNotReturn	HasReturnValue
klee_prefer_cex	0	0
klee_check_memory_access	0	0
klee_get_valuel	0	1
malloc	0	1
klee_assume	0	0
klee_report_error	1	0
klee_warning	0	0
free	0	0
realloc	0	1
klee_warning_once	0	0
klee_posix_prefer_cex	0	0
klee_mark_global	0	0
klee_is_symbolic	0	1
klee_make_symbolic	0	0
abort	1	0
__assert_fail	1	0
exit	1	0
klee_get_errno	0	1

This should probably be used to preserve functions that do not return (and we should preserve klee functions too?). However, this does not solve the problem of custom DNR functions such as yy_fatal_error.

List of all recognized DNR functions:

  addDNR("__assert_rtn", handleAssertFail),
  addDNR("__assert_fail", handleAssertFail),
  addDNR("_assert", handleAssert),
  addDNR("abort", handleAbort),
  addDNR("_exit", handleExit),
  { "exit", &SpecialFunctionHandler::handleExit, true, false, true },
  addDNR("klee_abort", handleAbort),
  addDNR("klee_silent_exit", handleSilentExit),  
  addDNR("klee_report_error", handleReportError),

jordr commented 4 years ago

Special functions are fixed, but we need to do some additional work to detect DNR functions from the LLVM bytecode + some analysis because we may want to keep may-DNR functions

jordr / chopper