Does New Scope Rule Apply to Labels?

jiong · 2011-02-05 03:46:57

Hi, is the new scope rule in Spin6 supposed to work for labels too? Please take a look at the example below:

inline test_inline(a)
{
  test_inline1(a);
  assert(a == 1);
  goto Return;
Return:
  a = 1;
}

inline test_inline1(a)
{
  goto Return;
Return:
  a = 2;
}

active proctype test()
{
  int a = 0;
  test_inline(a);
}

If I understand correctly, the "goto Return" should jump to the "Return" in the same scope (inside inline function). If that is true, the assert(a==1) should fail. But in real case, it is not executed at all. The second "goto" jumps to the first "Return". Is that expected?

Last edited by jiong (2011-02-05 03:49:26)

spinroot · 2011-02-05 05:37:38

that's a bug -- thank you for that example.
it will be fixed in the next release of spin.
the scope rules do not extend to labels, so the correct behavior from spin in this case would be to declared an "Error: label Return redeclared"
with the bug, it does not give the error, but effectively only recognizes one of the labels.
this will be the last one seen by the parser (so that in this case depends subtly on the order in which the inlines are expanded)

jiong · 2011-02-06 02:53:51

Thanks spinroot for the reply. I hope the scoped labels can also be supported in the future as it is much easier to extract C function calls with inline expansion. To extract functions as inline is so far the only way I found feasible to support concurrent function calls. But there might be duplicate labels when there are multiple calling points for an inline function in a process, like the example below:

inline function1()
{
  // some code here
  goto Return_function1;
  // some code here
Return_function1: skip;
}

proctype test()
{
  // two calls to function1
  function1();
  function1();
}

Of course, I can work around the issue the gotos:

proctype test()
{
  int ret;
  ret = 0;
  goto function1_wrap;
L0:
  ret = 1;
  goto function1_wrap;
L1:

function1_wrap:
  function1();
  if
  ::ret == 0 -> goto L0;
  ::ret == 1 -> goto L1;
  ::else -> assert(false);
  fi;
}

But the scoped label approach is obviously more elegant. What do you think?

spinroot · 2011-02-06 20:21:10

you're quite right

jiong · 2011-02-11 09:14:34

Hi Gerard, do you have plan to enable the scoped labels in the near future?

spinroot · 2011-02-11 17:36:23

it's on the list of things to consider, but there's no definite plan yet.
i'll definitely look into it though -- to see how much would be involved in makeing that change. it's probably not too hard to do, and i agree that it would be quite useful

spinroot · 2011-02-11 21:37:29

it will be fixed in the next Spin release (6.0.2)
it turned out not to be very hard to do
if a goto jumps to a label spin now first tries to find the destination label within the same inline (if the goto appears in an inline), and only if it's not there it will match on another destination label anywhere else within the same proctype
this gives the right default behavior, without losing existing functionality
and it solves the problem you had with labels with the same name appearing in different inlines

jiong · 2011-02-12 02:28:48

Yes, thanks man!

Spinroot

#1 2011-02-05 03:46:57

Does New Scope Rule Apply to Labels?

#2 2011-02-05 05:37:38

Re: Does New Scope Rule Apply to Labels?

#3 2011-02-06 02:53:51

Re: Does New Scope Rule Apply to Labels?

#4 2011-02-06 20:21:10

Re: Does New Scope Rule Apply to Labels?

#5 2011-02-11 09:14:34

Re: Does New Scope Rule Apply to Labels?

#6 2011-02-11 17:36:23

Re: Does New Scope Rule Apply to Labels?

#7 2011-02-11 21:37:29

Re: Does New Scope Rule Apply to Labels?

#8 2011-02-12 02:28:48

Re: Does New Scope Rule Apply to Labels?

Board footer