0001768: Crah with the option -ulevel - Frama-C Bug Tracking System

(0005065)
yakobowski (manager)
2014-05-01 00:06

Multiple slicing pragma inside a single function are currently not supported. Unfortunately, this property is not properly checked, and analysing a code that does not honor it leads to the crash you observe. In your example, your unique slice pragma is duplicated when the loop is unrolled.

If you have compiled Frama-C from source, you can remove the assertion at src/logic/logic_interp.ml:796. I'm reasonably sure that for simple cases, including yours, it is not needed.

(0005066)
nguenaomer (reporter)
2014-05-01 00:19

Thank you for this helful reply !
However, I will not change the source of frama-c.
I still wonder why the -ulevel option keeps loop in the program after the unfoldings.

Thanks

$frama-c fsm.c -ulevel 10 -print
[kernel] preprocessing with "gcc -C -E -I. fsm.c"
/* Generated by Frama-C */
int choix;
int state = 1;
int cumul = 0;
int step = 0;
/*@ ensures (\result ≡ 0 ∨ \result ≡ 1) ∨ \result ≡ 2; */
extern int choisir();

void lecture(void)
{
  choix = choisir();
  return;
}

void fsm_transition(void)
{
  switch (state) {
    case 1: ;
    if (choix == 2) {
      cumul += 2;
      state = 2;
    }
    else cumul ++;
    break;
    case 2: ;
    if (step == 50)
      if (choix == 1) state = 3; else cumul ++;
    else cumul ++;
    break;
    case 3: ;
    if (choix == 0)
      if (cumul == 10) state = 1;
    default: ;
    break;
  }
  return;
}

int main(void)
{
  int __retres;
  if (! (step >= 0)) goto unrolling_2_loop;
  lecture();
  fsm_transition();
  if (state == 3) {
    /*@ slice pragma ctrl; */ ;
    goto unrolling_2_loop;
  }
  step ++;
  unrolling_12_loop: /* internal */ ;
  if (! (step >= 0)) goto unrolling_2_loop;
  lecture();
  fsm_transition();
  if (state == 3) {
    /*@ slice pragma ctrl; */ ;
    goto unrolling_2_loop;
  }
  step ++;
  unrolling_11_loop: /* internal */ ;
  if (! (step >= 0)) goto unrolling_2_loop;
  lecture();
  fsm_transition();
  if (state == 3) {
    /*@ slice pragma ctrl; */ ;
    goto unrolling_2_loop;
  }
  step ++;
  unrolling_10_loop: /* internal */ ;
  if (! (step >= 0)) goto unrolling_2_loop;
  lecture();
  fsm_transition();
  if (state == 3) {
    /*@ slice pragma ctrl; */ ;
    goto unrolling_2_loop;
  }
  step ++;
  unrolling_9_loop: /* internal */ ;
  if (! (step >= 0)) goto unrolling_2_loop;
  lecture();
  fsm_transition();
  if (state == 3) {
    /*@ slice pragma ctrl; */ ;
    goto unrolling_2_loop;
  }
  step ++;
  unrolling_8_loop: /* internal */ ;
  if (! (step >= 0)) goto unrolling_2_loop;
  lecture();
  fsm_transition();
  if (state == 3) {
    /*@ slice pragma ctrl; */ ;
    goto unrolling_2_loop;
  }
  step ++;
  unrolling_7_loop: /* internal */ ;
  if (! (step >= 0)) goto unrolling_2_loop;
  lecture();
  fsm_transition();
  if (state == 3) {
    /*@ slice pragma ctrl; */ ;
    goto unrolling_2_loop;
  }
  step ++;
  unrolling_6_loop: /* internal */ ;
  if (! (step >= 0)) goto unrolling_2_loop;
  lecture();
  fsm_transition();
  if (state == 3) {
    /*@ slice pragma ctrl; */ ;
    goto unrolling_2_loop;
  }
  step ++;
  unrolling_5_loop: /* internal */ ;
  if (! (step >= 0)) goto unrolling_2_loop;
  lecture();
  fsm_transition();
  if (state == 3) {
    /*@ slice pragma ctrl; */ ;
    goto unrolling_2_loop;
  }
  step ++;
  unrolling_4_loop: /* internal */ ;
  if (! (step >= 0)) goto unrolling_2_loop;
  lecture();
  fsm_transition();
  if (state == 3) {
    /*@ slice pragma ctrl; */ ;
    goto unrolling_2_loop;
  }
  step ++;
  unrolling_3_loop: /* internal */ ;
  while (step >= 0) {
    lecture();
    fsm_transition();
    if (state == 3) {
      /*@ slice pragma ctrl; */ ;
      break;
    }
    step ++;
  }
  unrolling_2_loop: /* internal */ ;
  __retres = 0;
  return __retres;
}

(0005093)
patrick (developer)
2014-05-14 17:22

Fixed in removing assertion at src/logic/logic_interp.ml:796.

(0005101)
yakobowski (manager)
2014-05-16 11:11

0001768:0005066 : the subpart of Frama-C that performs loop unrolling does not try to "understand" loops. It just copies the body N times. As it cannot guarantee that the loop is fully unrolled, the body is kept in case it gets executed.

If the loop is fully unrolled and you want to remove its body (after Value has ran), you can use the Sparecode plugin. It is seems similar to Slicing, but remove all dead code. Furthermore, it will also remove quite a few other things, like useless conditional tests that stem from the loop condition.

Issue History
Date Modified	Username	Field	Change
2014-04-30 22:33	nguenaomer	New Issue
2014-05-01 00:06	yakobowski	Note Added: 0005065
2014-05-01 00:19	nguenaomer	Note Added: 0005066
2014-05-14 17:22	patrick	Note Added: 0005093
2014-05-14 17:24	signoles	Assigned To	=> patrick
2014-05-14 17:24	signoles	Status	new => assigned
2014-05-14 17:26	patrick	Status	assigned => resolved
2014-05-14 17:26	patrick	Resolution	open => fixed
2014-05-16 11:11	yakobowski	Note Added: 0005101
2014-08-06 16:09	patrick	Relationship added	has duplicate 0001906
2015-03-17 22:17	signoles	Fixed in Version	=> Frama-C Sodium
2015-03-17 22:18	signoles	Status	resolved => closed

Notes
(0005065) yakobowski (manager) 2014-05-01 00:06	Multiple slicing pragma inside a single function are currently not supported. Unfortunately, this property is not properly checked, and analysing a code that does not honor it leads to the crash you observe. In your example, your unique slice pragma is duplicated when the loop is unrolled. If you have compiled Frama-C from source, you can remove the assertion at src/logic/logic_interp.ml:796. I'm reasonably sure that for simple cases, including yours, it is not needed.

(0005066) nguenaomer (reporter) 2014-05-01 00:19	Thank you for this helful reply ! However, I will not change the source of frama-c. I still wonder why the -ulevel option keeps loop in the program after the unfoldings. Thanks $frama-c fsm.c -ulevel 10 -print [kernel] preprocessing with "gcc -C -E -I. fsm.c" /* Generated by Frama-C / int choix; int state = 1; int cumul = 0; int step = 0; /@ ensures (\result ≡ 0 ∨ \result ≡ 1) ∨ \result ≡ 2; / extern int choisir(); void lecture(void) { choix = choisir(); return; } void fsm_transition(void) { switch (state) { case 1: ; if (choix == 2) { cumul += 2; state = 2; } else cumul ++; break; case 2: ; if (step == 50) if (choix == 1) state = 3; else cumul ++; else cumul ++; break; case 3: ; if (choix == 0) if (cumul == 10) state = 1; default: ; break; } return; } int main(void) { int __retres; if (! (step >= 0)) goto unrolling_2_loop; lecture(); fsm_transition(); if (state == 3) { /@ slice pragma ctrl; / ; goto unrolling_2_loop; } step ++; unrolling_12_loop: / internal / ; if (! (step >= 0)) goto unrolling_2_loop; lecture(); fsm_transition(); if (state == 3) { /@ slice pragma ctrl; / ; goto unrolling_2_loop; } step ++; unrolling_11_loop: / internal / ; if (! (step >= 0)) goto unrolling_2_loop; lecture(); fsm_transition(); if (state == 3) { /@ slice pragma ctrl; / ; goto unrolling_2_loop; } step ++; unrolling_10_loop: / internal / ; if (! (step >= 0)) goto unrolling_2_loop; lecture(); fsm_transition(); if (state == 3) { /@ slice pragma ctrl; / ; goto unrolling_2_loop; } step ++; unrolling_9_loop: / internal / ; if (! (step >= 0)) goto unrolling_2_loop; lecture(); fsm_transition(); if (state == 3) { /@ slice pragma ctrl; / ; goto unrolling_2_loop; } step ++; unrolling_8_loop: / internal / ; if (! (step >= 0)) goto unrolling_2_loop; lecture(); fsm_transition(); if (state == 3) { /@ slice pragma ctrl; / ; goto unrolling_2_loop; } step ++; unrolling_7_loop: / internal / ; if (! (step >= 0)) goto unrolling_2_loop; lecture(); fsm_transition(); if (state == 3) { /@ slice pragma ctrl; / ; goto unrolling_2_loop; } step ++; unrolling_6_loop: / internal / ; if (! (step >= 0)) goto unrolling_2_loop; lecture(); fsm_transition(); if (state == 3) { /@ slice pragma ctrl; / ; goto unrolling_2_loop; } step ++; unrolling_5_loop: / internal / ; if (! (step >= 0)) goto unrolling_2_loop; lecture(); fsm_transition(); if (state == 3) { /@ slice pragma ctrl; / ; goto unrolling_2_loop; } step ++; unrolling_4_loop: / internal / ; if (! (step >= 0)) goto unrolling_2_loop; lecture(); fsm_transition(); if (state == 3) { /@ slice pragma ctrl; / ; goto unrolling_2_loop; } step ++; unrolling_3_loop: / internal / ; while (step >= 0) { lecture(); fsm_transition(); if (state == 3) { /@ slice pragma ctrl; / ; break; } step ++; } unrolling_2_loop: / internal */ ; __retres = 0; return __retres; }

(0005093) patrick (developer) 2014-05-14 17:22	Fixed in removing assertion at src/logic/logic_interp.ml:796.

(0005101) yakobowski (manager) 2014-05-16 11:11	0001768:0005066 : the subpart of Frama-C that performs loop unrolling does not try to "understand" loops. It just copies the body N times. As it cannot guarantee that the loop is fully unrolled, the body is kept in case it gets executed. If the loop is fully unrolled and you want to remove its body (after Value has ran), you can use the Sparecode plugin. It is seems similar to Slicing, but remove all dead code. Furthermore, it will also remove quite a few other things, like useless conditional tests that stem from the loop condition.