Labels need to be renamed

[pattersonz]

When a label exists in a configuration, the configuration duplicates the label with the same name twice. If both labels exist in the same scope, this causes an error. For example:

char
foo()
{
  int x;
  goto label;
 label:
  x +=
    #ifdef A
    2
    #else
    3
    #endif
    ;
}

transforms into:

#include <stdbool.h>

extern void __static_type_error(char *msg);
extern void __static_renaming(char *renaming, char *original);
extern void __static_condition_renaming(char *expression, char *renaming);

void __static_initializer_default();

extern const bool __static_condition_default_3;
extern const bool __static_condition_default_2;
void __static_initializer_default() {
__static_renaming("__foo_0", "foo");
__static_renaming("__x_1", "x");

__static_condition_renaming("__static_condition_default_2", "(declare-fun |(defined A)| () Bool)(assert \
|(defined A)|)");
__static_condition_renaming("__static_condition_default_3", "(declare-fun |(defined A)| () Bool)(assert \
(not |(defined A)|))");

};

static char __foo_0 () {
{
int  __x_1;
goto label ;


{
if (__static_condition_default_2) {
label :  __x_1  += 2 ;

}

if (__static_condition_default_3) {
label :  __x_1  += 3 ;

}

}}


}

which will throw this error:
gotoTest.desugared.c: In function ‘__foo_0’:
gotoTest.desugared.c:33:1: error: duplicate label ‘label’
label : __x_1 += 3 ;
^~~~~
gotoTest.desugared.c:28:1: note: previous definition of ‘label’ was here
label : __x_1 += 2 ;
^~~~~

[paulgazz]

Solving this requires a few things in order to still desugar in a single pass:

• The existing symbol table can be used to store labels by putting them in a different namespace (the label namespace is separate from both tags and regular symbols).
• A goto may appear before the label itself. Since the label itself may be duplicated during desugaring, there is no way in a single pass to know the renamings ahead of time. What can be done to maintain a single pass is to create a level of indirection: create a fresh label, then when all labels have been collected and renamed by the end of the function, create a special code section that dispatches the goto label to the correct label renaming based on static conditionals.

Without allowing multiple passes or rearchitecting the output data structure, this is what the single-pass approach might look like

   goto label;
//...
label:  // ...
//...
label:  // in another configuration

will become

  goto __label_1;
// ...
__label_2:  // ...
__label_3:  // ...
// indirection generated automatically
__label_1:
if (__static_condition_4) {
  goto __label_2;
}
if (__static_condition_5) {
  goto __label_3;
}