GenMC crash with -check-liveness and -disable-spin-assume

[db7]

Here is a small example that crashes GenMC

#include <stdbool.h>

void __VERIFIER_spin_start(void);
void __VERIFIER_spin_end(bool);

#define await_while(cond)                                      \
	for (int tmp = 0; __VERIFIER_spin_start(), tmp = cond, \
			__VERIFIER_spin_end(!tmp), tmp;)

int *ptr;
int main()
{
	await_while(!__atomic_load_n(&ptr, __ATOMIC_RELAXED));
	return 0;
}

It uses an await_while macro as discussed in #16, but cases GenMC to give this error message:

user@d0d1f66d6eaf:~$ genmc -check-liveness -disable-spin-assume test.c
genmc: /usr/lib/llvm-8/include/llvm/Support/Casting.h:255: typename cast_retty<X, Y *>::ret_type llvm::cast(Y *) [X = llvm::IntegerType, Y = const llvm::Type]: Assertion `isa<X>(Val) && "cast<Ty>() argument of incompatible type!"' failed.
Aborted (core dumped)
user@d0d1f66d6eaf:~$ 

I know that for this small example the automatic spin-assume transformation works, but in original example where we started it does not. Is there something wrong with the use of __VERIFIER_spin_* or is there a bug in GenMC?

[michaliskok]

Try using -disable-load-annotation.

The problem is that GenMC generally tries to optimize the usage of assume-like functions (e.g., __VERIFIER_spin_end()) by not considering values that will make them fail, but the current version does not like assume()s on pointer types. This is probably going to be fixed in v0.7 (as part of a different rewrite), but until then you can use the above switch to disable the optimization.

Thanks for all the bug reports; they are very helpful.

(BTW, have you modified the error reporting in the tool? I expect internal assertions to fire in such cases.)

[db7]

Excellent! It works with -disable-load-annotation. Thank you.

The error report is from an unmodified version of GenMC 0.6 compiled with LLVM 8.