code is executed after abort condition

[MohamedGhardallou]

Hello,

Describe the bug

please consider the following program :

@[CFunction (binding = "log_int($1)", header = "env.h")]
extern function log_int(i : int32) 

const MSEC_PER_SYSTICK: nat32 = 1

activity waitMsec (msec: nat32)
  var i: nat32 = msec / MSEC_PER_SYSTICK
  repeat
      await true
      i = i - 1
  until i == 0 end
end

activity verify_basic(new_time: nat32)() 

  var time_changed : bool = false
  var time : nat32 = new_time
  var state : nat32 = 0

  log_int(0)

  cobegin weak

    //time change detection branch
    //in this case time will never change 
    repeat
      time_changed = false
      await (new_time != time)
      time_changed = true
      time = new_time
      await true
    end
  with
    repeat
      if state == 0 then
        //print 10000 , wait for one second and jump to state 2
        log_int(10000)
        run waitMsec(1000)
        state = 2

      elseif state == 2 then
        log_int(10002)
        when time_changed abort
          //infinite loop
          repeat 
            run waitMsec(100000)
          end
        end
        log_int(2) // this should never be executed
        state = 0
        await true
      end
      await true
    end
  end
end

activity read_time()(new_time: nat32)
  await true
  new_time = 4000
end

activity verify()()

  var time :nat32 = 0
  run read_time()(time)

  cobegin weak
    repeat
      run waitMsec(1000)
      run read_time()(time)
    end
  with
    run verify_basic(time)()
  end

end

@[EntryPoint]
activity main(stop_btn: bool)( )

  repeat
    when stop_btn abort
      run verify()()
    end
  end

end

env.h

static void log_int(int i)
{
    printf("log_int %d\n" , i);
}

Expected behaviour

If you execute this program for 2 second (2000 cycles) you should see the following output on the screen : log_int 0 log_int 10000 log_int 10002

After 2 seconds verify_basic activity is in state 2 (infinite loop). if we set stop_btn to true and we do one step log_int(2) is executed. This is a bug.

[FriedrichGretz]

I confirm there is an output from an activity that should have been aborted in the tick where stop_btn is true. I'll have to investigate further why is this the case.

[FriedrichGretz]

The minimal repro for this bug is

activity B ()
    var x: int32 = 18
    cobegin
        cobegin
            await true
            x = -42
        with
            await true
        end
    with
        await true
    end
end

@[EntryPoint]
activity A ()
    when true reset
        run B()
    end
end

Here x should never become -42 but it does (and stays so forever after the first tick). The reason is that we do initialise the main program counter of an activity but we leave all others unchanged and rely on control flow starting for the first statement to take care of the rest. This leaves the further nested ones in their old state from the previous invocation. None of our code generation tests seems to catch it.

Fix is on the way.

[MohamedGhardallou]

Hello @FriedrichGretz The fix is working thanks .

but I see that some counters are assigned twice . it should be optimized by the compiler but just in case you missed that .

Thanks

[FriedrichGretz]

Yes, everything is zero-ed out and then the main program counter is set. Indeed this is a bit wasteful but I guess the C compiler will optimise it away.

[mschlund]

Is the version bumped after the fixes? For me "blechc --version" still shows "Blech Compiler 0.7.0+0"

[schorg]

@mschlund now you can use the latest release v0.7.2 you will see Blech Compiler 0.7.2+0 Copyright (C) 2019-2022 see blech-lang.org