ikos crashes during preprocessing

[yiyuaner]

I was running ikos using a bitcode file compiled from clang-9.

The command is:

ikos -a=boa redis-cli.bc 2>&1 | tee log

The stack trace is:

#0  0x000055bb668ab98d in ikos::frontend::import::FunctionImporter::translate_phi_l
ate(ikos::frontend::import::BasicBlockTranslation*, llvm::PHINode*) ()
#1  0x000055bb668ac136 in ikos::frontend::import::FunctionImporter::translate_phi_n
odes(ikos::frontend::import::BasicBlockTranslation*, llvm::BasicBlock*) ()
#2  0x000055bb668b27b1 in ikos::frontend::import::FunctionImporter::translate_phi_n
odes() ()
#3  0x000055bb668b4d55 in ikos::frontend::import::FunctionImporter::translate_contr
ol_flow_graph() ()
#4  0x000055bb668b4d75 in ikos::frontend::import::FunctionImporter::translate_body(
) ()
#5  0x000055bb668a21a1 in ikos::frontend::import::BundleImporter::translate_functio
n_body(llvm::Function*) ()
#6  0x000055bb66892cdb in ikos::frontend::import::Importer::import(llvm::Module&, i
kos::ar::Flags<ikos::frontend::import::Importer::ImportOption>) ()
#7  0x000055bb665b95d1 in main ()

The bitcode file is attached for your reference. redis-cli.zip

[ivanperez-keera]

Thanks for filing this and for your patience.

I'm able to reproduce this bug with the latest version of ikos.

I'm tracing this down.

This is a segfault. The problem is in line 1455 in:

https://github.com/NASA-SW-VnV/ikos/blob/8608a78adfb7c6c5421b9eec4d5bc6929f5bd647/frontend/llvm/src/import/function.cpp#L1447-L1455

More specifically, ar_value->type() is the call that segfaults.

The pointer is not null. ar_value has the value 0x71 which seems a pointer to a very low memory location if I'm interpreting this right.

Looking at how ar_value is defined in line 1452 (that's the path taken in this case) takes me to:

https://github.com/NASA-SW-VnV/ikos/blob/8608a78adfb7c6c5421b9eec4d5bc6929f5bd647/frontend/llvm/src/import/function.cpp#L1705-L1712

var at the return point is indeed 0x71. Perhaps this is a problem with either the implementation of the symbols table or the values being put in it? I'd appreciate a second pair of eyes here.

[yiyuaner]

@ivanperez-keera The problem is that llvm_value is never translated, i.e., this->_variables.find(llvm_value) == this->_variables.end() in the following code fragment:

https://github.com/NASA-SW-VnV/ikos/blob/8608a78adfb7c6c5421b9eec4d5bc6929f5bd647/frontend/llvm/src/import/function.cpp#L1447-L1455

Notable, the assertion in the function translate_value is not compiled into the binary of ikos-analyzer (even in cmake Debug build), hence we have missed the assertion error:

https://github.com/NASA-SW-VnV/ikos/blob/8608a78adfb7c6c5421b9eec4d5bc6929f5bd647/frontend/llvm/src/import/function.cpp#L1705-L1707

We can try dumping out llvm_value:

(gdb) p llvm_value->dump()
  %24 = zext i1 undef to i8, !dbg !8997

However, in my debugging, the function FunctionImporter::translate_cast is never called on the llvm_value. Why is that? Isn't IKOS translate each instruction one by one?

[yiyuaner]

Also, not sure if this has something to do with the llvm version. When I raised the issue, the bitcode is compiled by clang-9, but the latest ikos uses llvm 14.

[ivanperez-keera]

I don't think it's due to the version of LLVM. I was able to reproduce this with the latest version, which uses LLVM 14.