k-induction bugs Investigation

[ChenfengWei0]

• example1

  int main()
  {
  int status = 0;
  // status = *
  while(__VERIFIER_nondet_int()) // __verifier_nondet_int$1 = *
  {
  if(!status) // status = *
  {
    status = 1;
  }
  else if(status == 1)
  {
    status = 2;
  }
  } // status = 1 U 2
  
  while(1)
  __ESBMC_assert(status != 2, "");
  
  return 0;
  }

• expected result: VERIFICATION FAILED
• --k-induction:
  • VERIFICATION SUCCESSFUL
  • Solution found by the inductive step (k = 2)
• --k-induction-parallel
  • VERIFICATION FAILED
  • forward condition process crashed.
  • Bug found by the base case (k = 3)
• --unwind 3
  • VERIFICATION FAILED
  • unwinding assertion loop
• --unwind 3 --no-unwinding-assertions
  • VERIFICATION FAILED
  • (_Bool)(status != 2)

[ChenfengWei0]

example2

int main()
{
  int status = 0;
  // status = *
  while (rand() % 2) // __verifier_nondet_int$1 = *
  {
    if (!status) // status = *
    {
      status = 1;
    }
    else if (status == 1)
    {
      status = 2;
    }
  } // status = 1 U 2

  while (1)
    __ESBMC_assert(status != 1, ""); // changed

  return 0;
}

• k-induction: VERIFICATION FAILED. k-step = 2

[ChenfengWei0]

diff

main (c:@F@main):
        // 28 file 2.c line 435 function main
        signed int status;
        // 29 file 2.c line 435 function main
        status=0;
        // 30 file 2.c line 437 function main
        status=NONDET(signed int);
        // 31 file 2.c line 437 function main
     1: signed int return_value$___VERIFIER_nondet_int$1;
        // 32 file 2.c line 437 function main
        return_value$___VERIFIER_nondet_int$1=NONDET(signed int);
        // 33 no location
        IF !(_Bool)return_value$___VERIFIER_nondet_int$1 THEN GOTO 4

main (c:@F@main):
        // 28 file 2.c line 435 function main
        signed int status;
        // 29 file 2.c line 435 function main
        status=0;
        // 30 file 2.c line 437 function main
        status=NONDET(signed int);
        // 31 file 2.c line 437 function main
     1: signed int return_value$_rand$1;
        // 32 file 2.c line 437 function main
        FUNCTION_CALL:  return_value$_rand$1=rand()
        // 33 no location
        IF !((_Bool)(return_value$_rand$1 % 2)) THEN GOTO 4

[ChenfengWei0]

No function body for rand()

[ChenfengWei0]

#define __VERIFIER_assert(cond)                                                \
  do                                                                           \
  {                                                                            \
    if(!(cond))                                                                \
    {                                                                          \
      __ESBMC_assert(0, "");                                                   \
      abort();                                                                 \
    }                                                                          \
  } while(0)

#include <stdlib.h>
#include <math.h>
extern int __VERIFIER_nondet_int(void);
extern void abort(void);
#include <assert.h>
void reach_error()
{
  assert(0);
}

int main()
{
  int status = 0;

  while(nondet_int())
  {
    if(!status)
    {
      status = 1;
    }
    else if(status == 1)
    {
      status = 2;
    }
    else if(status >= 2)
    {
      status = 3;
    }
  }
  __VERIFIER_assert(status != 3);
  return 0;
}

• --k-induction
  • VERIFICATION SUCCESSFUL
• --k-induction --k-step 4
  • VERIFICATION FAILED
• --unwind 3
  • VERIFICATION FAILED
  • unwinding assertion loop
• --unwind 3 --no-unwinding-assertions
  • VERIFICATION SUCCESSFUL
• --unwind 4
  • VERIFICATION FAILED
  • status != 3

[ChenfengWei0]

with/ without --k-step

Checking base case, k = 1
[PROGRESS] Starting Bounded Model Checking
Not unwinding
Symex completed in: 0.004s (25 assignments)
Slicing time: 0.000s (removed 21 assignments)
Generated 1 VCC(s), 0 remaining after simplification (4 assignments)
BMC program time: 0.004s
No bug has been found in the base case
[PROGRESS] Checking forward condition, k = 1
[PROGRESS] Starting Bounded Model Checking
Not unwinding
Symex completed in: 0.004s (25 assignments)
Slicing time: 0.000s (removed 21 assignments)
Generated 1 VCC(s), 1 remaining after simplification (4 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.001s
The forward condition is unable to prove the property
Checking base case, k = 2
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 11  iteration  1   file 2.c line 479 function main
Not unwinding
Symex completed in: 0.004s (30 assignments)
Slicing time: 0.000s (removed 22 assignments)
Generated 1 VCC(s), 1 remaining after simplification (8 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.001s
BMC program time: 0.006s
No bug has been found in the base case
[PROGRESS] Checking forward condition, k = 2
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 11  iteration  1   file 2.c line 479 function main
Not unwinding
Symex completed in: 0.004s (29 assignments)
Slicing time: 0.000s (removed 23 assignments)
Generated 1 VCC(s), 1 remaining after simplification (6 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.001s
The forward condition is unable to prove the property
[PROGRESS] Checking inductive step, k = 2
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 11  iteration  1   file 2.c line 479 function main
Not unwinding
Symex completed in: 0.005s (50 assignments)
Slicing time: 0.001s (removed 25 assignments)
Generated 0 VCC(s), 0 remaining after simplification (25 assignments)
BMC program time: 0.006s

VERIFICATION SUCCESSFUL

Checking base case, k = 1
[PROGRESS] Starting Bounded Model Checking
Not unwinding
Symex completed in: 0.004s (25 assignments)
Slicing time: 0.000s (removed 21 assignments)
Generated 1 VCC(s), 0 remaining after simplification (4 assignments)
BMC program time: 0.004s
No bug has been found in the base case
[PROGRESS] Checking forward condition, k = 1
[PROGRESS] Starting Bounded Model Checking
Not unwinding
Symex completed in: 0.004s (25 assignments)
Slicing time: 0.000s (removed 21 assignments)
Generated 1 VCC(s), 1 remaining after simplification (4 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.001s
The forward condition is unable to prove the property
Checking base case, k = 4
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 11  iteration  1   file 2.c line 479 function main
Unwinding loop 11  iteration  2   file 2.c line 479 function main
Unwinding loop 11  iteration  3   file 2.c line 479 function main
Not unwinding
Symex completed in: 0.006s (38 assignments)
Slicing time: 0.000s (removed 24 assignments)
Generated 1 VCC(s), 1 remaining after simplification (14 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.001s
[PROGRESS] Building error trace

[ChenfengWei0]

okay, the bug is that the k will not grow when there is

• a loop with guard condition a nondet_int
• two loop at least the base case will only go up to k=2

[ChenfengWei0]

E.g.

int main()
{
  int x =10;
  while(x--)
  {
    assert(x);
  }
}

result

Checking base case, k = 9
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 501 function main
Unwinding loop 2  iteration  2   file 2.c line 501 function main
Unwinding loop 2  iteration  3   file 2.c line 501 function main
Unwinding loop 2  iteration  4   file 2.c line 501 function main
Unwinding loop 2  iteration  5   file 2.c line 501 function main
Unwinding loop 2  iteration  6   file 2.c line 501 function main
Unwinding loop 2  iteration  7   file 2.c line 501 function main
Unwinding loop 2  iteration  8   file 2.c line 501 function main
Not unwinding
Symex completed in: 0.002s (30 assignments)
Slicing time: 0.000s (removed 28 assignments)
Generated 9 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.002s
No bug has been found in the base case
[PROGRESS] Checking forward condition, k = 9
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 501 function main
Unwinding loop 2  iteration  2   file 2.c line 501 function main
Unwinding loop 2  iteration  3   file 2.c line 501 function main
Unwinding loop 2  iteration  4   file 2.c line 501 function main
Unwinding loop 2  iteration  5   file 2.c line 501 function main
Unwinding loop 2  iteration  6   file 2.c line 501 function main
Unwinding loop 2  iteration  7   file 2.c line 501 function main
Unwinding loop 2  iteration  8   file 2.c line 501 function main
Not unwinding
Symex completed in: 0.002s (30 assignments)
Slicing time: 0.000s (removed 28 assignments)
Generated 1 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
The forward condition is unable to prove the property
[PROGRESS] Checking inductive step, k = 9
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 501 function main
Unwinding loop 2  iteration  2   file 2.c line 501 function main
Unwinding loop 2  iteration  3   file 2.c line 501 function main
Unwinding loop 2  iteration  4   file 2.c line 501 function main
Unwinding loop 2  iteration  5   file 2.c line 501 function main
Unwinding loop 2  iteration  6   file 2.c line 501 function main
Unwinding loop 2  iteration  7   file 2.c line 501 function main
Unwinding loop 2  iteration  8   file 2.c line 501 function main
Not unwinding
Symex completed in: 0.004s (64 assignments)
Slicing time: 0.001s (removed 26 assignments)
Generated 1 VCC(s), 1 remaining after simplification (38 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.001s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
The inductive step is unable to prove the property
Checking base case, k = 10
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 501 function main
Unwinding loop 2  iteration  2   file 2.c line 501 function main
Unwinding loop 2  iteration  3   file 2.c line 501 function main
Unwinding loop 2  iteration  4   file 2.c line 501 function main
Unwinding loop 2  iteration  5   file 2.c line 501 function main
Unwinding loop 2  iteration  6   file 2.c line 501 function main
Unwinding loop 2  iteration  7   file 2.c line 501 function main
Unwinding loop 2  iteration  8   file 2.c line 501 function main
Unwinding loop 2  iteration  9   file 2.c line 501 function main
Not unwinding
Symex completed in: 0.002s (33 assignments)
Slicing time: 0.000s (removed 30 assignments)
Generated 10 VCC(s), 1 remaining after simplification (3 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
[PROGRESS] Building error trace

[ChenfengWei0]

Interesting result from --k-induction-parallel

#include <assert.h>

int main()
{
  int status = 0;

  int cnt = 4;
  while (cnt--)
  {
    if (!status)
    {
      status = 1;
    }
    else if (status == 1)
    {
      status = 2;
    }
    else if (status == 2)
    {
      status = 3;
    }
    else if (status >= 3)
    {
      status = 4;
    }
  }

  do
  {
    if (!(status != 4))
    {
      assert(0);
    }
  } while (0);
}

• in most cases

  
  Checking base case, k = 1

[PROGRESS] Starting Bounded Model Checking GOTO program processing time: 0.023s Checking inductive step, k = 2 [PROGRESS] Starting Bounded Model Checking Not unwinding Symex completed in: 0.005s (25 assignments) Slicing time: 0.000s (removed 23 assignments) Generated 0 VCC(s), 0 remaining after simplification (2 assignments) BMC program time: 0.005s No bug has been found in the base case Checking base case, k = 2

[PROGRESS] Starting Bounded Model Checking Unwinding loop 11 iteration 1 file 2.c line 475 function main Unwinding loop 11 iteration 1 file 2.c line 475 function main Not unwinding Symex completed in: 0.005s (28 assignments) Slicing time: 0.000s (removed 26 assignments) Generated 0 VCC(s), 0 remaining after simplification (2 assignments) BMC program time: 0.005s No bug has been found in the base case Checking base case, k = 3

[PROGRESS] Starting Bounded Model Checking Not unwinding Symex completed in: 0.010s (64 assignments) Slicing time: 0.000s (removed 31 assignments) Generated 0 VCC(s), 0 remaining after simplification (33 assignments) BMC program time: 0.010s

VERIFICATION SUCCESSFUL INDUCTIVE STEP PROCESS FINISHED. Unwinding loop 11 iteration 1 file 2.c line 475 function main Unwinding loop 11 iteration 2 file 2.c line 475 function main Not unwinding Symex completed in: 0.006s (31 assignments) Slicing time: 0.000s (removed 29 assignments) Generated 0 VCC(s), 0 remaining after simplification (2 assignments) BMC program time: 0.006s No bug has been found in the base case BASE CASE PROCESS FINISHED.

forward condition process crashed.

Solution found by the inductive step (k = 2) VERIFICATION SUCCESSFUL

- and very few times we can have the correct result
```sh
➜  bin ./esbmc 2.c --color --k-induction-parallel
ESBMC version 7.2.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc

[PROGRESS] Parsing
[PROGRESS] Parsing
[PROGRESS] Parsing
[PROGRESS] Converting
[PROGRESS] Converting
[PROGRESS] Converting
^[[A^[[A[PROGRESS] Generating GOTO Program

[PROGRESS] Generating GOTO Program
[PROGRESS] Generating GOTO Program
GOTO program creation time: 0.424s
GOTO program processing time: 0.019s
Checking base case, k = 1

[PROGRESS] Starting Bounded Model Checking
Not unwinding
Symex completed in: 0.004s (25 assignments)
Slicing time: 0.000s (removed 23 assignments)
Generated 0 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.004s
No bug has been found in the base case
Checking base case, k = 2

[PROGRESS] Starting Bounded Model Checking
Unwinding loop 11  iteration  1   file 2.c line 475 function main
Not unwinding
Symex completed in: 0.004s (28 assignments)
Slicing time: 0.000s (removed 26 assignments)
Generated 0 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.004s
No bug has been found in the base case
Checking base case, k = 3

[PROGRESS] Starting Bounded Model Checking
Unwinding loop 11  iteration  1   file 2.c line 475 function main
Unwinding loop 11  iteration  2   file 2.c line 475 function main
Not unwinding
Symex completed in: 0.004s (31 assignments)
Slicing time: 0.000s (removed 29 assignments)
Generated 0 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.004s
No bug has been found in the base case
Checking base case, k = 4

[PROGRESS] Starting Bounded Model Checking
Unwinding loop 11  iteration  1   file 2.c line 475 function main
Unwinding loop 11  iteration  2   file 2.c line 475 function main
Unwinding loop 11  iteration  3   file 2.c line 475 function main
Not unwinding
Symex completed in: 0.005s (34 assignments)
Slicing time: 0.001s (removed 32 assignments)
Generated 0 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.006s
No bug has been found in the base case
Checking base case, k = 5

[PROGRESS] Starting Bounded Model Checking
Unwinding loop 11  iteration  1   file 2.c line 475 function main
Unwinding loop 11  iteration  2   file 2.c line 475 function main
Unwinding loop 11  iteration  3   file 2.c line 475 function main
Unwinding loop 11  iteration  4   file 2.c line 475 function main
Symex completed in: 0.005s (36 assignments)
Slicing time: 0.000s (removed 34 assignments)
Generated 1 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.001s
[PROGRESS] Building error trace

[Counterexample]

State 1 file 2.c line 495 function main thread 0
----------------------------------------------------
Violated property:
  file 2.c line 495 function main
  assertion
  status != 4

VERIFICATION FAILED
BASE CASE PROCESS FINISHED.

Bug found by the base case (k = 5)
VERIFICATION FAILED

[ChenfengWei0]

By setting no-unwinding-assertions and partial-loops false (was true) in inductive step, we now have the correct result

k_step_inc1
1
Checking base case, k = 1
[PROGRESS] Starting Bounded Model Checking
Not unwinding
Symex completed in: 0.001s (16 assignments)
Slicing time: 0.000s (removed 14 assignments)
Generated 0 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.001s
No bug has been found in the base case
[PROGRESS] Checking forward condition, k = 1
[PROGRESS] Starting Bounded Model Checking
Not unwinding
Symex completed in: 0.001s (16 assignments)
Slicing time: 0.000s (removed 14 assignments)
Generated 1 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
The forward condition is unable to prove the property
k_step_inc1
2
Checking base case, k = 2
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.002s (19 assignments)
Slicing time: 0.000s (removed 17 assignments)
Generated 0 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.002s
No bug has been found in the base case
[PROGRESS] Checking forward condition, k = 2
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.001s (19 assignments)
Slicing time: 0.000s (removed 17 assignments)
Generated 1 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
The forward condition is unable to prove the property
[PROGRESS] Checking inductive step, k = 2
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.004s (57 assignments)
Slicing time: 0.001s (removed 33 assignments)
Generated 1 VCC(s), 1 remaining after simplification (24 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.001s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.001s
The inductive step is unable to prove the property
k_step_inc1
3
Checking base case, k = 3
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.002s (22 assignments)
Slicing time: 0.000s (removed 20 assignments)
Generated 0 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.002s
No bug has been found in the base case
[PROGRESS] Checking forward condition, k = 3
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.002s (22 assignments)
Slicing time: 0.000s (removed 20 assignments)
Generated 1 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
The forward condition is unable to prove the property
[PROGRESS] Checking inductive step, k = 3
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.005s (78 assignments)
Slicing time: 0.001s (removed 39 assignments)
Generated 1 VCC(s), 1 remaining after simplification (39 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.001s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.001s
The inductive step is unable to prove the property
k_step_inc1
4
Checking base case, k = 4
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Unwinding loop 2  iteration  3   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.002s (25 assignments)
Slicing time: 0.000s (removed 23 assignments)
Generated 0 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.002s
No bug has been found in the base case
[PROGRESS] Checking forward condition, k = 4
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Unwinding loop 2  iteration  3   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.002s (25 assignments)
Slicing time: 0.000s (removed 23 assignments)
Generated 1 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.001s
The forward condition is unable to prove the property
[PROGRESS] Checking inductive step, k = 4
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Unwinding loop 2  iteration  3   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.007s (99 assignments)
Slicing time: 0.000s (removed 45 assignments)
Generated 1 VCC(s), 1 remaining after simplification (54 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.001s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.001s
The inductive step is unable to prove the property
k_step_inc1
5
Checking base case, k = 5
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Unwinding loop 2  iteration  3   file 2.c line 472 function main
Unwinding loop 2  iteration  4   file 2.c line 472 function main
Symex completed in: 0.002s (27 assignments)
Slicing time: 0.000s (removed 25 assignments)
Generated 1 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
[PROGRESS] Building error trace

[Counterexample]

State 1 file 2.c line 496 function main thread 0
----------------------------------------------------
Violated property:
  file 2.c line 496 function main
  assertion 0
  0

VERIFICATION FAILED

Bug found (k = 5)

[ChenfengWei0]

#include <assert.h>

int main()
{
  int status = 0;

  int cnt = 4;
  while (cnt--)
  {
    if (!status)
    {
      status = 1;
    }
    else if (status == 1)
    {
      status = 2;
    }
    else if (status == 2)
    {
      status = 3;
    }
    else if (status >= 3)
    {
      status = 4;
    }
  }

  assert(status==4);  // added
  // assert(status!=0);  // or

  do
  {
    if (!(status != 4))
    {
      assert(0);
    }
  } while (0);
}

ESBMC version 7.2.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
[PROGRESS] Parsing
[PROGRESS] Converting
[PROGRESS] Generating GOTO Program
GOTO program creation time: 0.235s
GOTO program processing time: 0.000s
Checking base case, k = 1
[PROGRESS] Starting Bounded Model Checking
Not unwinding
Symex completed in: 0.000s (16 assignments)
Slicing time: 0.000s (removed 14 assignments)
Generated 0 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.000s
No bug has been found in the base case
[PROGRESS] Checking forward condition, k = 1
[PROGRESS] Starting Bounded Model Checking
Not unwinding
Symex completed in: 0.000s (16 assignments)
Slicing time: 0.001s (removed 14 assignments)
Generated 1 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.001s
The forward condition is unable to prove the property
Checking base case, k = 2
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.001s (19 assignments)
Slicing time: 0.000s (removed 17 assignments)
Generated 0 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.001s
No bug has been found in the base case
[PROGRESS] Checking forward condition, k = 2
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.001s (19 assignments)
Slicing time: 0.000s (removed 17 assignments)
Generated 1 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.001s
The forward condition is unable to prove the property
[PROGRESS] Checking inductive step, k = 2
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.004s (57 assignments)
Slicing time: 0.000s (removed 22 assignments)
Generated 1 VCC(s), 1 remaining after simplification (35 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.001s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.010s
The inductive step is unable to prove the property
Checking base case, k = 3
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.002s (22 assignments)
Slicing time: 0.000s (removed 20 assignments)
Generated 0 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.002s
No bug has been found in the base case
[PROGRESS] Checking forward condition, k = 3
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.002s (22 assignments)
Slicing time: 0.000s (removed 20 assignments)
Generated 1 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
The forward condition is unable to prove the property
[PROGRESS] Checking inductive step, k = 3
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.004s (78 assignments)
Slicing time: 0.001s (removed 28 assignments)
Generated 1 VCC(s), 1 remaining after simplification (50 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.001s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.012s
The inductive step is unable to prove the property
Checking base case, k = 4
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Unwinding loop 2  iteration  3   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.002s (25 assignments)
Slicing time: 0.000s (removed 23 assignments)
Generated 0 VCC(s), 0 remaining after simplification (2 assignments)
BMC program time: 0.002s
No bug has been found in the base case
[PROGRESS] Checking forward condition, k = 4
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Unwinding loop 2  iteration  3   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.002s (25 assignments)
Slicing time: 0.000s (removed 23 assignments)
Generated 1 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
The forward condition is unable to prove the property
[PROGRESS] Checking inductive step, k = 4
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Unwinding loop 2  iteration  3   file 2.c line 472 function main
Not unwinding
Symex completed in: 0.007s (99 assignments)
Slicing time: 0.000s (removed 34 assignments)
Generated 1 VCC(s), 1 remaining after simplification (65 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.001s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.016s
The inductive step is unable to prove the property
Checking base case, k = 5
[PROGRESS] Starting Bounded Model Checking
Unwinding loop 2  iteration  1   file 2.c line 472 function main
Unwinding loop 2  iteration  2   file 2.c line 472 function main
Unwinding loop 2  iteration  3   file 2.c line 472 function main
Unwinding loop 2  iteration  4   file 2.c line 472 function main
Symex completed in: 0.003s (27 assignments)
Slicing time: 0.000s (removed 25 assignments)
Generated 2 VCC(s), 1 remaining after simplification (2 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
[PROGRESS] Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
[PROGRESS] Building error trace

[Counterexample]

State 1 file 2.c line 498 function main thread 0
----------------------------------------------------
Violated property:
  file 2.c line 498 function main
  assertion 0
  0

VERIFICATION FAILED

[ChenfengWei0]

If we use the --base-case option only, we can get the correct result

[ChenfengWei0]

#include <assert.h>

int main()
{
  int status = 0;

  int cnt = 4;
  while (cnt--)
  {
    if (!status)
    {
      status = 1;
    }
    else if (status == 1)
    {
      status = 2;
    }
    else if (status == 2)
    {
      status = 3;
    }
    else if (status >= 3)
    {
      status = 4;
    }
  }

  __ESBMC_assume(status);
  assert(status);
  do
  {
    if (!(status != 4))
    {
      assert(0);
    }
  } while (0);
}

wrong result

[ChenfengWei0]

simplest example

#include <assert.h>

int main()
{
  int cnt = 2;
  while (cnt--)
  {
  }

  // if we add this assert here we get the correct result
  // otherwise wrong result
  // assert(cnt==-1);
  // not working if add  
  // assert(1==1);

  do
  {
    assert(0);

  } while (0);
}

[ChenfengWei0]

#define __VERIFIER_assert(cond)                                                \
  do                                                                           \
  {                                                                            \
    if(!(cond))                                                                \
    {                                                                          \
      __ESBMC_assert(0, "");                                                   \
      abort();                                                                 \
    }                                                                          \
  } while(0)

#include <stdlib.h>
extern int __VERIFIER_nondet_int(void);
extern void abort(void);
#include <assert.h>
void reach_error()
{
  assert(0);
}

int main()
{
  int status = 0;

  while(__VERIFIER_nondet_int())
  {
    if(!status)
    {
      status = 1;
    }
    else if(status == 1)
    {
      status = 2;
    }
    else if(status >= 2)
    {
      status = 3;
    }
  }
  assert(status>=0); // after add this we have correct result
  __VERIFIER_assert(status != 3);
  return 0;
}

[ChenfengWei0]

--k-induction perform endlessly in this case

#define __VERIFIER_assert(cond)                                                \
  do                                                                           \
  {                                                                            \
    if(!(cond))                                                                \
    {                                                                          \
      __ESBMC_assert(0, "");                                                   \
      abort();                                                                 \
    }                                                                          \
  } while(0)

#include <stdlib.h>
extern int __VERIFIER_nondet_int(void);
extern void abort(void);
#include <assert.h>
void reach_error()
{
  assert(0);
}

int main()
{
  int status = 0;
  int x = __VERIFIER_nondet_int();
  while(x)
  {
    if(!status)
    {
      status = 1;
    }
    else if(status == 1)
    {
      status = 2;
    }
    else if(status >= 2)
    {
      status = 3;
    }
  }
  assert(x>=0); // after add this we have correct result
  __VERIFIER_assert(status != 3);
  return 0;
}

[ChenfengWei0]

If we use output-goto and binary to re-read the program and use k-induction to verify, we can now have the correct result.

[ChenfengWei0]

If we use output-goto and binary to re-read the program and use k-induction to verify, we can now have the correct result.

The guess is that sth is set wrongly but was dropped during the goto re-read process.

[ChenfengWei0]

Something wrong in goto_k_induction(goto_functions);

• compute_loop

[ChenfengWei0]

    if(
      cmdline.isset("inductive-step") || cmdline.isset("k-induction") ||
      cmdline.isset("k-induction-parallel"))
    {
      // remove skips before doing k-induction
      remove_skip(goto_functions);

      goto_k_induction(goto_functions);
    }

this will partially fix the issues.

[ChenfengWei0]

main (c:@F@main):
        // 33 file 2.c line 497 column 3 function main
        signed int cnt;
        // 34 file 2.c line 497 column 3 function main
        cnt=12;
        // 35 file 2.c line 498 column 3 function main
     1: signed int tmp$1;
        // 36 file 2.c line 498 column 10 function main
        tmp$1=cnt;
        // 37 file 2.c line 498 column 10 function main
        cnt=cnt - 1;
        // 38 file 2.c line 498 column 3 function main
        IF !(_Bool)tmp$1 THEN GOTO 2
        // 39 file 2.c line 498 column 3 function main
        SKIP
        // 40 file 2.c line 498 column 3 function main
        SKIP
        // 41 file 2.c line 499 column 3 function main
        SKIP
        // 42 file 2.c line 498 column 3 function main
        GOTO 1
        // 43 file 2.c line 498 column 3 function main
     2: SKIP
        // 44 file 2.c line 504 column 5 function main
     3: 4;

        // 45 file 2.c line 504 column 5 function main
        ASSERT 0 // assertion 0
        // 46 no location
        IF 0 THEN GOTO 3
        // 47 file 2.c line 502 column 3 function main
        SKIP
        // 48 file 2.c line 507 column 1 function main
        dead tmp$1;
        // 49 file 2.c line 507 column 1 function main
        dead cnt;
        // 50 file 2.c line 507 column 1 function main
        RETURN: NONDET(signed int)
        // 51 file 2.c line 507 column 1 function main
        END_FUNCTION // main

---

main (c:@F@main):
        // 28 file 2.c line 497 column 3 function main
        signed int cnt;
        // 29 file 2.c line 497 column 3 function main
        cnt=12;
        // 30 file 2.c line 498 column 3 function main
        cnt=NONDET(signed int);
        // 31 file 2.c line 498 column 3 function main
     1: signed int tmp$1;
        // 32 file 2.c line 498 column 10 function main
        tmp$1=cnt;
        // 33 file 2.c line 498 column 10 function main
        cnt=cnt - 1;
        // 34 file 2.c line 498 column 3 function main
        IF !(_Bool)tmp$1 THEN GOTO 2
        // 35 file 2.c line 498 column 3 function main
        GOTO 1
        // 36 file 2.c line 504 column 5 function main
     2: 4;

        // 37 file 2.c line 504 column 5 function main
        ASSERT 0 // assertion 0
        // 38 file 2.c line 507 column 1 function main
        dead tmp$1;
        // 39 file 2.c line 507 column 1 function main
        dead cnt;
        // 40 file 2.c line 507 column 1 function main
        RETURN: NONDET(signed int)
        // 41 file 2.c line 507 column 1 function main
        END_FUNCTION // main

[ChenfengWei0]

main (c:@F@main):
        // 27 file 2.c line 578 column 3 function main
        signed int status;
        // 28 file 2.c line 578 column 3 function main
        status=0;
        // 29 file 2.c line 580 column 3 function main
        status=NONDET(signed int);
        // 30 file 2.c line 580 column 3 function main
     1: signed int return_value$_nondet_int$1;
        // 31 file 2.c line 580 column 10 function main
        return_value$_nondet_int$1=NONDET(signed int);
        // 32 file 2.c line 580 column 3 function main
        IF !(_Bool)return_value$_nondet_int$1 THEN GOTO 4
        // 33 file 2.c line 582 column 5 function main
        IF !(!(_Bool)status) THEN GOTO 2
        // 34 file 2.c line 584 column 7 function main
        status=1;
        // 35 file 2.c line 584 column 7 function main
        GOTO 3
        // 36 file 2.c line 582 column 5 function main
     2: IF !(status == 1) THEN GOTO 3
        // 37 file 2.c line 588 column 7 function main
        status=2;
        // 38 file 2.c line 580 column 3 function main
     3: GOTO 1
        // 39 file 2.c line 592 column 3 function main
     4: ASSERT status != -1
        // 40 file 2.c line 594 column 3 function main
     5: signed int return_value$_nondet_int$2;
        // 41 file 2.c line 594 column 10 function main
        return_value$_nondet_int$2=NONDET(signed int);
        // 42 file 2.c line 594 column 3 function main
        IF !(_Bool)return_value$_nondet_int$2 THEN GOTO 6
        // 43 file 2.c line 595 column 5 function main
        ASSERT (_Bool)(status != 2)
        // 44 file 2.c line 594 column 3 function main
        GOTO 5
        // 45 file 2.c line 597 column 3 function main
     6: RETURN: 0
        // 46 file 2.c line 598 column 1 function main
        END_FUNCTION // main

[ChenfengWei0]

add an assert to terminate k-induction?