Variables sometimes fail to update in counterexamples

[noloerino]

The counterexample produced for the below code should not be a reachable state, since the step variable is incremented on every cycle in the next block. However, the counterexample has the value of step at 1 on consecutive cycles despite this.

Code

module main {

    var x : integer;
    var step : integer;

    init {
        x = 0;
        step = 0;
    }

    next {
        x' = 1;
        step' = step + 1;
        assert ((step == 1) ==> (x == 0)); // should fail
    }

    // invariant x_zero : (step == 1) ==> (x == 0);

    control {
        vobj = bmc_noLTL(3);
        check;
        print_results;
        vobj.print_cex();
    }
}

Output

$ uclid no_update.ucl
Successfully instantiated 1 module(s).
2 assertions passed.
1 assertions failed.
0 assertions indeterminate.
  PASSED -> vobj [Step #1] assertion @ no_update.ucl, line 14
  PASSED -> vobj [Step #3] assertion @ no_update.ucl, line 14
  FAILED -> vobj [Step #2] assertion @ no_update.ucl, line 14
CEX for vobj [Step #2] assertion @ no_update.ucl, line 14
=================================
Step #0
  step : 0
  x : 0
=================================
=================================
Step #1
  step : 1
  x : 1
=================================
=================================
Step #2
  step : 1
  x : 1
=================================
Finished execution for module: main.

[polgreen]

hmm. Can you make this produce an unsound verification result (i.e., a case where verification fails when actually it should pass)? If not, I think this might just be a problem parsing the counterexample back but I'll take a look.

[noloerino]

I had an example where I think the result was unsound, but the counterexample produced was like this one where the step counter should have been incremented. I'll see if I can minimize it and double check to make sure that the model was supposed to be sound.

…

On Fri, Mar 4, 2022 at 3:05 AM E Polgreen ***@***.***> wrote: hmm. Can you make this produce an unsound verification result (i.e., a case where verification fails when actually it should pass)? If not, I think this might just be a problem parsing the counterexample back but I'll take a look. — Reply to this email directly, view it on GitHub <#160 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFFY4GQSQF7SHAFX2PAKQP3U6HVAZANCNFSM5P4EZ6AA> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[noloerino]

Here's an example. The invariant done should express the same logic as the assert statement in the next block, but the invariant passes while the assertion fails.

module fsm {
    type op_t = enum { SET_T, SET_F };

    input imem : [bv3]op_t;
    var pc : bv3;
    var reg : boolean;
    
    init {
        pc = 0bv3;
    }

    next {
        case
            (imem[pc] == SET_T) : { reg' = true; }
            (imem[pc] == SET_F) : { reg' = false; }
        esac
        pc' = pc + 1bv3;
    }
}

module main {
    type * = fsm.*;

    var imem : [bv3]op_t;
    var step : integer;
    
    instance fsm_0 : fsm (imem : (imem));

    init {
        assume (imem[0bv3] == SET_T);
        assume (imem[1bv3] == SET_F);
        step = 0;
    }

    next {
        next (fsm_0);
        step' = step + 1;
        case
            (step == 1): {
                assert (fsm_0.reg == true);
            }
        esac
    }
        
    invariant done : (step == 1) ==> fsm_0.reg == true;

    control {
        vobj = bmc_noLTL(4);
        check;
        print_results;
        vobj.print_cex(step, imem, fsm_0.pc, fsm_0.reg);
    }
}

Output:

Successfully instantiated 2 module(s).
8 assertions passed.
1 assertions failed.
0 assertions indeterminate.
  PASSED -> vobj [Step #0] property done @ no_update_unsound.ucl, line 45
  PASSED -> vobj [Step #1] assertion @ no_update_unsound.ucl, line 40
  PASSED -> vobj [Step #1] property done @ no_update_unsound.ucl, line 45
  PASSED -> vobj [Step #2] property done @ no_update_unsound.ucl, line 45
  PASSED -> vobj [Step #3] assertion @ no_update_unsound.ucl, line 40
  PASSED -> vobj [Step #3] property done @ no_update_unsound.ucl, line 45
  PASSED -> vobj [Step #4] assertion @ no_update_unsound.ucl, line 40
  PASSED -> vobj [Step #4] property done @ no_update_unsound.ucl, line 45
  FAILED -> vobj [Step #2] assertion @ no_update_unsound.ucl, line 40
CEX for vobj [Step #2] assertion @ no_update_unsound.ucl, line 40
=================================
Step #0
  step : 0
  imem : 
	1 : SET_F
	- : SET_T
  fsm_0.pc : 0
  fsm_0.reg : false
=================================
=================================
Step #1
  step : 1
  imem : 
	1 : SET_F
	- : SET_T
  fsm_0.pc : 1
  fsm_0.reg : true
=================================
=================================
Step #2
  step : 1
  imem : 
	1 : SET_F
	- : SET_T
  fsm_0.pc : 2
  fsm_0.reg : false
=================================
Finished execution for module: main.

As you can see in the provided counterexample, step's value fails to update while the values within the fsm_0 instance do update. It's possible this is related in some way to #156, since verification seems to pass when the transition logic + state for the fsm module is inlined into main instead.