Bug #328
open
Short logic when calling functions in conditions should be implemented correctly
Added by Pavel Shved almost 14 years ago.
Updated over 9 years ago.
Detected in build:
pre-ldv
Description
Given the code snippet
if (f() || g()) {...}
CIL transforms it into the following code:
tmp1 = f();
tmp2 = g();
if (tmp1 || tmp2) {...}
That is obviously not correct (and one mutex_lock driver even fails because of it); programmers do rely on short logic. Note that in other cases short logic is correctly processed with CIL, it's just for function calls (which are transformed into assignments of temporary variables) where it happens.
Letting the program through Aspectator solves it (LLVM has more correct short logic transformation).
As I understand it isn't made by LLVM. This is done during function bodies gimplification. But because of some reasons we plan to use more low-level representation like source code itself. So we either should fix CIL (put some conditions and labels) or make some hacks inside ldv gcc pretty printer.
To remember the one way how to do this, here is the code produced by LLVM:
...
blast_must_tmp__6 = f();
if ((blast_must_tmp__6 != 0u)) {
goto llvm_cbe_bb1;
} else {
goto llvm_cbe_bb;
}
llvm_cbe_bb:
blast_must_tmp__7 = g();
if ((blast_must_tmp__7 != 0u)) {
goto llvm_cbe_bb1;
} else {
goto llvm_cbe_bb2;
}
llvm_cbe_bb1:
*(&llvm_cbe_tmp__5) = 0u;
goto llvm_cbe_bb3;
llvm_cbe_bb2:
*(&llvm_cbe_tmp__5) = 1u;
goto llvm_cbe_bb3;
llvm_cbe_bb3:
...
Fix at aspectator level, I guess, is fairly useless unless all rule models are instrumented through aspectator. Because, if some models are without aspects, then CIL won't work correctly with the rest of them.
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)
- Category set to CIL
- Assignee deleted (
Pavel Shved)
As of October 2014, the bug doesn't show up in current development branch of CIL 1.7.3 (bc1cb8e676e71c0adabe04da5d760d2c85f24268):
if (f() || g()) { ...
is transformed into
tmp = f();
if (tmp) {
...
} else {
tmp___0 = g();
if (tmp___0) {
...
}
}
Also available in: Atom
PDF