Skip to content

C Frontend doesn't handle extern declarations in nested scope correctly #1867

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
hannes-steffenhagen-diffblue opened this issue Feb 20, 2018 · 3 comments

Comments

@hannes-steffenhagen-diffblue
Copy link
Contributor

Given a C program like this

#include <stdio.h>

int some_global = 10;

void shadow()
{
  int some_global = 5;
  printf("local: %d\n", some_global);
  {
    extern int some_global;
    ++some_global;
    printf("global: %d\n", some_global);
  }
  printf("local: %d\n", some_global);
  {
    extern int some_global;
    ++some_global;
    printf("global: %d\n", some_global);
  }
}

int main(void)
{
  shadow();
}

The correct output is

local: 5
global: 11
local: 5
global: 12

i.e. the local variable declaration should shadow the global variable, and the extern declaration should shadow the local variable with the global variable.

But the goto function generated for shadow is

shadow /* shadow */
        // 3 file main.c line 7 function shadow
        signed int shadow$$1$$some_global;
        // 4 file main.c line 7 function shadow
        shadow$$1$$some_global = 5;
        // 5 file main.c line 8 function shadow
        printf("local: %d\n", shadow$$1$$some_global);
        // 6 no location
        SKIP
        // 7 file main.c line 11 function shadow
        shadow$$1$$some_global = shadow$$1$$some_global + 1;
        // 8 file main.c line 12 function shadow
        printf("global: %d\n", shadow$$1$$some_global);
        // 9 file main.c line 14 function shadow
        printf("local: %d\n", shadow$$1$$some_global);
        // 10 no location
        SKIP
        // 11 file main.c line 17 function shadow
        shadow$$1$$some_global = shadow$$1$$some_global + 1;
        // 12 file main.c line 18 function shadow
        printf("global: %d\n", shadow$$1$$some_global);
        // 13 file main.c line 20 function shadow
        dead shadow$$1$$some_global;
        // 14 file main.c line 20 function shadow
        END_FUNCTION

In this case, the extern declaration seemingly gets ignored and the assignments that should've been made to the global variable are made to the local variable instead.

@martin-cs
Copy link
Collaborator

May I ask what basis you use for determining what the right behaviour is? It's not that I doubt it, I'm just wondering why it's that. From my copy of ISO 9899:1999 I've found:

6.2.1.2. For each different entity that an identifier designates, the identifier is visible (i.e., can be used) only within a region of program text called its scope. Different entities designated by the same identifier either have different scopes, or are in different name spaces. There are four kinds of scopes: function, file, block, and function prototype. (A function prototype is a declaration of a function that declares the types of its parameters.)

[Only file and block level matter for us.]

6.2.1.4 Every other identifier has scope determined by the placement of its declaration (in a declarator or type specifier). If the declarator or type specifier that declares the identifier appears outside of any block or list of parameters, the identifier has file scope, which terminates at the end of the translation unit. If the declarator or type specifier that declares the identifier appears inside a block or within the list of parameter declarations in a function definition, the identifier has block scope, which terminates at the end of the associated block. If the declarator or type specifier that declares the identifier appears
within the list of parameter declarations in a function prototype (not part of a function definition), the identifier has function prototype scope, which terminates at the end of the function declarator. If an identifier designates two different entities in the same name space, the scopes might overlap. If so, the scope of one entity (the inner scope) will be a strict subset of the scope of the other entity (the outer scope). Within the inner scope, the identifier designates the entity declared in the inner scope; the entity declared in the outer scope is hidden (and not visible) within the inner scope.

[So I make that four identifiers called "some_global", one with file scope, three with respectively nested block scope.]

6.2.2.1 An identifier declared in different scopes or in the same scope more than once can be made to refer to the same object or function by a process called linkage. There are three kinds of linkage: external, internal, and none.

6.2.2.2 In the set of translation units and libraries that constitutes an entire program, each declaration of a particular identifier with external linkage denotes the same object or function. Within one translation unit, each declaration of an identifier with internal linkage denotes the same object or function. Each declaration of an identifier with no linkage denotes a unique entity.

[Right, so whether the identifiers point to the same thing or not is a question of linkage.]

6.2.2.4 For an identifier declared with the storage-class specifier extern in a scope in which a prior declaration of that identifier is visible, (As specified in 6.2.1, the later declaration might hide the prior declaration.) if the prior declaration specifies internal or external linkage, the linkage of the identifier at the later declaration is the same as the linkage specified at the prior declaration. If no prior declaration is visible, or if the prior declaration specifies no linkage, then the identifier has external linkage.

[ This seems to be one of the key clauses. The two deeply nested declarations with extern specifiers should have the same linkage as the previous (still block layer) declaration, or external if it doesn't have one. ]

6.2.2.5 If the declaration of an identifier for a function has no storage-class specifier, its linkage is determined exactly as if it were declared with the storage-class specifier extern. If the declaration of an identifier for an object has file scope and no storage-class specifier, its linkage is external.

[ The first definition of some_global has external linkage. ]

6.2.2.6 The following identifiers have no linkage: an identifier declared to be anything other than an object or a function; an identifier declared to be a function parameter; a block scope identifier for an object declared without the storage-class specifier extern.

[The inner one has no linkage.]

6.2.2.7 If, within a translation unit, the same identifier appears with both internal and external linkage, the behavior is undefined.

[Fascinating...]

--

So as I see it, there are four identifiers called some_global. The outer-most "global" one and the two extern ones all have external linkage and thus refer to the same object. The "local" one has no linkage and is thus a unique object.

TL;DR : I agree with the suggested reference output.

I also agree with the analysis of the problem and, yes, I think the bug is in the handling, or non-handling of extern on the local variable declarations.

@tautschnig
Copy link
Collaborator

Thanks a lot for the detailed analysis! I think I've got a fix, I'll post the PR in the morning.

@hannes-steffenhagen-diffblue
Copy link
Contributor Author

@martin-cs @tautschnig Thanks for looking into this so quickly!

tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 21, 2018
Previously, extern declarations would only be recorded in the global scope.
While they do belong to the global scope, they still need to take precedence in
name lookups in the local/current scope as well.

Also removing an unnecessary iostream include.

Fixes: diffblue#1867
tautschnig added a commit to tautschnig/cbmc that referenced this issue Apr 27, 2018
Previously, extern declarations would only be recorded in the global scope.
While they do belong to the global scope, they still need to take precedence in
name lookups in the local/current scope as well.

Also removing an unnecessary iostream include.

Fixes: diffblue#1867
tautschnig added a commit to tautschnig/cbmc that referenced this issue May 21, 2018
Previously, extern declarations would only be recorded in the global scope.
While they do belong to the global scope, they still need to take precedence in
name lookups in the local/current scope as well.

Also removing an unnecessary iostream include.

Fixes: diffblue#1867
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants