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:

ikos/frontend/llvm/src/import/function.cpp

Lines 1447 to 1455 in 8608a78

	if (llvm::isa< llvm::Constant >(llvm_value) &&
	!llvm::isa< llvm::GlobalValue >(llvm_value)) {
	ar_value =
	this->translate_value(bb_translation, llvm_value, result->type());
	} else {
	ar_value = this->translate_value(bb_translation, llvm_value, nullptr);
	}
	if (ar_value->type() == result->type()) {

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:

ikos/frontend/llvm/src/import/function.cpp

Lines 1705 to 1712 in 8608a78

	auto it = this->_variables.find(value);
	ikos_assert_msg(it != this->_variables.end(),
	"value hasn't been translated yet");
	ar::Variable* var = it->second;
	if (type == nullptr || var->type() == type) {
	return var;

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:

ikos/frontend/llvm/src/import/function.cpp

Lines 1447 to 1455 in 8608a78

	if (llvm::isa< llvm::Constant >(llvm_value) &&
	!llvm::isa< llvm::GlobalValue >(llvm_value)) {
	ar_value =
	this->translate_value(bb_translation, llvm_value, result->type());
	} else {
	ar_value = this->translate_value(bb_translation, llvm_value, nullptr);
	}
	if (ar_value->type() == result->type()) {

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:

ikos/frontend/llvm/src/import/function.cpp

Lines 1705 to 1707 in 8608a78

	auto it = this->_variables.find(value);
	ikos_assert_msg(it != this->_variables.end(),
	"value hasn't been translated yet");

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.