Project

General

Profile

Actions
Copy link

Bug #328

open

Short logic when calling functions in conditions should be implemented correctly

Added by Pavel Shved over 13 years ago. Updated over 9 years ago.

Status:
Open
Priority:
Low
Assignee:
-
Category:
CIL
Target version:
-
Start date:
08/03/2010
Due date:
% Done:

0%

Estimated time:
Detected in build:
pre-ldv
Platform:
Published in build:

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).

Actions
Copy link
 #1

Updated by Evgeny Novikov about 13 years ago

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:
...

Actions
Copy link
 #2

Updated by Pavel Shved about 13 years ago

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.

Actions
Copy link
 #3

Updated by Pavel Shved over 12 years ago

  • Project changed from Linux Driver Verification to BLAST
  • Category deleted (BLAST)
Actions
Copy link
 #4

Updated by Vadim Mutilin over 9 years ago

  • Category set to CIL
  • Assignee deleted (Pavel Shved)
Actions
Copy link
 #5

Updated by Mikhail Mandrykin over 9 years ago

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) {
...
    }
  }

Actions
Copy link

Also available in: Atom PDF