kframework / c-semantics

Semantics of C in K
Other
305 stars 40 forks source link

Union bug #612

Closed h0nzZik closed 4 years ago

h0nzZik commented 4 years ago

The following code

union UN_1{
    int j;
};

// it work if it is a struct
union UN_ {
    // the order of members does not matter
    int d1;
        // it works if this (UN_1) is struct
    union UN_1 d2;

    // this fixes the problem
    //int j; 
};

// making it local variable does not help
union UN_ un_data;

int main(void){
    un_data.d2.j = 20;
    return 0;
}

when executed, results in the error:

Type of lvalue (int) not compatible with the effective type of the object being accessed (union UN_):
      > in main at union.c:17:2

    Undefined behavior (UB-EIO10):
        see C11 section 6.5:7 http://rvdoc.org/C11/6.5
        see C11 section J.2:1 item 37 http://rvdoc.org/C11/J.2
        see CERT-C section EXP39-C http://rvdoc.org/CERT-C/EXP39-C
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

. However, if the outer union contains j (with the same name as in the inner union), the problem disappears. The difference is that in the second case, the lvalue that is used to access the object, has in its loc3 component an information that j is the active variant of d2.

I suspect the bug is somewhere near https://github.com/kframework/c-semantics/blob/master/semantics/c/language/common/typing/effective.k#L196-L212. This code is called in the translation semantics when processing the assignment to the (nested) member, from createLv through updateLastAccessVariant to setVariantToOffset, which is called somewhat like

  setVariantAtOffset(
          t(quals(`.Set`(.KList)),`_Set_`(`SetItem`(activeVariant(`Identifier`(#token("\"d2\"","String    ")))),`SetItem`(fieldInfo(`_List_`(`ListItem`(typedDeclaration(t(quals(`.Set`(.KList)),`.Set`(.KList    ),`int_C-TYPING-SYNTAX`(.KList)),`Identifier`(#token("\"d1\"","String")))),`ListItem`(typedDeclarati    on(t(quals(`.Set`(.KList)),`.Set`(.KList),unionType(tag(`Identifier`(#token("\"UN_1\"","String")),#t    oken("\"/home/jtusil/denso-test/union.cd8311d83-5f9a-11ea-8308-e7dc7a92c17d\"","String"),`global_C-T    YPING-SYNTAX`(.KList)))),`Identifier`(#token("\"d2\"","String"))))),#token("32","Int"),`_Map_`(`_|->    _`(`Identifier`(#token("\"d1\"","String")),t(quals(`.Set`(.KList)),`.Set`(.KList),`int_C-TYPING-SYNT    AX`(.KList))),`_|->_`(`Identifier`(#token("\"d2\"","String")),t(quals(`.Set`(.KList)),`SetItem`(fiel    dInfo(`ListItem`(typedDeclaration(t(quals(`.Set`(.KList)),`.Set`(.KList),`int_C-TYPING-SYNTAX`(.KLis    t)),`Identifier`(#token("\"j\"","String")))),#token("32","Int"),`_|->_`(`Identifier`(#token("\"j\"",    "String")),t(quals(`.Set`(.KList)),`.Set`(.KList),`int_C-TYPING-SYNTAX`(.KList))),`_|->_`(`Identifie    r`(#token("\"j\"","String")),#token("0","Int")),`.Set`(.KList))),unionType(tag(`Identifier`(#token("    \"UN_1\"","String")),#token("\"/home/jtusil/denso-test/union.cd8311d83-5f9a-11ea-8308-e7dc7a92c17d\"    ","String"),`global_C-TYPING-SYNTAX`(.KList)))))),`_Map_`(`_|->_`(`Identifier`(#token("\"d1\"","Stri    ng")),#token("0","Int")),`_|->_`(`Identifier`(#token("\"d2\"","String")),#token("0","Int"))),`.Set`(    .KList)))),unionType(tag(`Identifier`(#token("\"UN_\"","String")),#token("\"/home/jtusil/denso-test/    union.cd8311d83-5f9a-11ea-8308-e7dc7a92c17d\"","String"),`global_C-TYPING-SYNTAX`(.KList))))
          `Identifier`(#token("\"j\"","String")),
          0
  )

i.e. with the outer union as the type and j as the member identifier. Rules for setVariantAtOffset contain a side condition that checks whether j is a member of UN_ - which is suspicious, and probably causes the 'normal' behavior when UN_ contains j as a member.

h0nzZik commented 4 years ago

Fixed by https://github.com/kframework/c-semantics/commit/20371b58de9667f4c06e628a0160b56d1d41014b.