kframework / c-semantics

Semantics of C in K
Other
302 stars 39 forks source link

C++: static cast fails to invoke `#convertStatic` #263

Closed h0nzZik closed 7 years ago

h0nzZik commented 7 years ago

I have some partial/experimental implementation of C++ enumerators, and for debugging purpuses I wanted to static_cast them to integers and back. Static cast, as described in 5.2.9:4-5 and implemented in cpp14/language/translation/expr/cast.k, first tries to direct-initialize a new temporary variable, and if that fails, it performs some conversion from 5.2.9:6-12 (implemented by #convertStatic). However I encountered some problems while casting integers to enums.

Ints are not implicitly convertible to enums, so they should be converted by #convertStatic. First problem is that some rules in cpp14/language/common/conversion.k allow implicit conversion of ints to enums. That is easy to fix.

But after fixing that (and implemeting some productions like min, max etc) I was not able to make figureInit() rewrite to ill-formed (or cannot-convert) in compile time (while running static semantics). For the cast in this piece of code

enum E{};
int main() {
    int a = 4;
    (E)a;
}

the translation semantics yields

`ExpressionStmt`(lecpp(`ExprLoc`(`CabsLoc`(...),
`_:=__CPP-SYNTAX`(
    lecpp(
        temp(...),
        hasTrace(...),
        tcpp(...,..,unscopedEnum(...))
    ),
    `ConvertType`(
        tcpp(...,...,unscopedEnum(...)),
        `ExprLoc`(`CabsLoc`(...),`ExprLoc`(`CabsLoc`(...),
            `Name`(`NoNNS`(.KList),`Identifier`(#token("\"a\"","String")))
        ))
    )
)),hasTrace(...),tcpp(...,...,unscopedEnum(...))))

which then evaluates to cannot-convert during runtime. I was trying to check the ill-formedness in assignment.k, but without much success, because the convertType(_,_) gets rewritten to ConvertType(,), which does not get rewritten anymore if the second parameter is a variable.

When trying to convert constant (e.g. (E)5), then convertType correctly rewrites to cannot-convert. @dwightguth any idea?

dwightguth commented 7 years ago

so, first of all, you are correct that we should probably add notBool isCPPEnumType(T) to the side condition of the rules in conversion.k. They exist in that form because they need to be able to handle char16_t, char32_t, and wchar_t, which are integer types but neither signed nor unsigned types. It was written without thinking that far ahead about enumerations at the time.

I believe what you want to try to do is to add a side condition to the rule that creates ConvertType nodes in the tree which asserts that the types involved make the conversion possible in some fashion.

dwightguth commented 7 years ago

I am working on a fix for this issue and should have it out soon. I would wait and come back to this once that's done.

h0nzZik commented 7 years ago

I have already created something for both parts. Do you think it would not be sufficient, or it is too ad-hoc?

dwightguth commented 7 years ago

Yes, this is too ad-hoc. I will have something out in the near future that should work without breaking the structure that I already began laying out

h0nzZik commented 7 years ago

This was probably fixed in 6cd2af9e88f11039da28a2b7a54bdf5474d0b261. Can we close it?