Uninitialized Function Pointer Results In Safe

[kbittick]

Hello,

I'm messing around with IKOS a bit and had an interesting result with this test case:

void unsafe() {
    char buffer[10];
    buffer[10] = 0;
}

void safe() {
}

int main() {
    void(*func_ptr)();
    func_ptr();
    return 0;
}

It invokes an uninitialized function pointer, which is unsafe because (of course) it's usually going to jump to unmapped or non executable memory and crash, but also because it could in principle invoke unsafe().

./install/bin/ikos my_test_cases/test10.c
[*] Compiling my_test_cases/test10.c
my_test_cases/test10.c:3:5: warning: array index 10 is past the end of the array (which contains 10 elements) [-Warray-bounds]
    buffer[10] = 0;
    ^      ~~
my_test_cases/test10.c:2:5: note: array 'buffer' declared here
    char buffer[10];
    ^
my_test_cases/test10.c:11:5: warning: variable 'func_ptr' is uninitialized when used here [-Wuninitialized]
    func_ptr();
    ^~~~~~~~
my_test_cases/test10.c:10:22: note: initialize the variable 'func_ptr' to silence this warning
    void(*func_ptr)();
                     ^
                      = 0
2 warnings generated.
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'

# Time stats:
clang        : 0.041 sec
ikos-analyzer: 0.005 sec
ikos-pp      : 0.003 sec

# Summary:
Total number of checks                : 0
Total number of unreachable checks    : 0
Total number of safe checks           : 0
Total number of definite unsafe checks: 0
Total number of warnings              : 0

The program is SAFE

# Results
No entries.

There are some warnings from Clang, but none from IKOS. I also noticed it didn't actually run any checks. I'm not sure if this has something to do with uninitialized values not being modeled the way I'd expect, or maybe how IKOS handles control flow and indirection, or maybe this is just violating other IKOS assumptions.

[arthaud]

Hi @kbittick, Most likely, this is so obvious that clang/llvm optimized the error away. Could you try running ikos with the --display-llvm option?

[kbittick]

Definitely looks along those lines, relevant snippet with --display-llvm is empty

; Function Attrs: noinline nounwind uwtable
define dso_local i32 @main() #0 !dbg !21 {
  unreachable, !dbg !25
}

Is this a pre-pass by IKOS? I tried to recreate with the options from IKOS's clang invocation:

/usr/lib/llvm-9/bin/clang -S -emit-llvm -Wall -U_FORTIFY_SOURCE -D_FORTIFY_SOURCE=0 -O0 -Xclang -disable-O0-optnone my_test_cases/test10.c

Which got more what I'd expect:

; Function Attrs: noinline nounwind uwtable
define dso_local i32 @main() #0 {
  %1 = alloca i32, align 4
  %2 = alloca void (...)*, align 8
  store i32 0, i32* %1, align 4
  %3 = load void (...)*, void (...)** %2, align 8
  call void (...) %3()
  ret i32 0
}

Thanks much

[arthaud]

Yes, that's ikos-pp, which does some very basic optimization, such as -mem2reg which hoists those alloca into llvm registers.

[kbittick]

Okay yeah, looks like -mem2reg converts it to just a function call on undef:

; Function Attrs: noinline nounwind uwtable
define dso_local i32 @main() #0 {
  call void (...) undef()
  ret i32 0
}

And then -remove-unreachable-blocks kills the call and return.

Looks like this -remove-unreachable-blocks delegates to an llvm function llvm::removeUnreachableBlocks. I'm guessing removing the call undef is within the bounds of undefined behavior, so it's safe for LLVM to do. It does seem to change the semantics of the code though, from the perspective of checking safety properties.

Thanks much.

[ivanperez-keera]

I'm following up on this.

Seeing Maxime's comment (" Most likely, this is so obvious that clang/llvm optimized the error away."), and the follow-up discussion, I wonder if anything needs to be done.

@kbittick please let me know. Thanks!

[kbittick]

I think it's probably fine as is since Clang is warning about the undefined behavior anyway, as long as there aren't cases where the compiler or the optimizer are changing semantics without a warning.

[ivanperez-keera]

Sounds good. In that case, I think we can close the issue, and if you find a case where both of them do that you can re-open it.