Refactor type compatibility + minor fixes.

kframework · Mar 22, 2016 · 48ed5c0 · 48ed5c0
1 parent 805113d
commit 48ed5c0
Show file tree

Hide file tree

Showing 22 changed files with 138 additions and 201 deletions.
diff --git a/semantics/language/common/alignment.k b/semantics/language/common/alignment.k
@@ -48,14 +48,6 @@ module C-ALIGNMENT
      rule byteAlignofType(t(Qs::Quals, Mods::Set, enumType(_)))
           => byteAlignofType(t(Qs, Mods, cfg:enumAlias))
 
-     syntax Int ::= byteAlignofList(List) [function]
-     syntax Int ::= "byteAlignofList'" "(" Int "," List ")" [function]
-
-     rule byteAlignofList(L:List) => byteAlignofList'(0, L)
-     rule byteAlignofList'(Sz:Int, ListItem(T:Type) LL:List)
-          => byteAlignofList'((Sz +Int byteAlignofType(T)), LL)
-     rule byteAlignofList'(Sz:Int, .List) => Sz
-
      syntax Int ::= "maxByteAlignofList'" "(" Int "," List ")" [function]
      rule maxByteAlignofList(L:List) => maxByteAlignofList'(1, L)
      rule maxByteAlignofList'(Sz:Int, ListItem(T:Type) LL:List)

diff --git a/semantics/language/common/binding.k b/semantics/language/common/binding.k
@@ -41,6 +41,12 @@ module C-BINDING
                (ListItem(V:RValue) => .List) _)
           requires notBool isVoidType(T)
           [structural]
+     rule bind(ListItem(typedDeclaration(T:VoidType, _)),
+               ListItem(T':VoidType), .List) => .K
+          [structural]
+     rule bind(ListItem(typedDeclaration(T:VoidType, _)),
+               ListItem(typedDeclaration(T':VoidType, _)), .List) => .K
+          [structural]
      // No prototype -- but the args must still have ids/types in the def.
      rule (.K => bindParam(X, T, argPromote(V)))
           ~> bind(
@@ -70,20 +76,14 @@ module C-BINDING
           ~> bind(.List, _, ListItem(_) _)
      rule (.K => UNDEF("CB4", "Function defined with no parameters "
                +String "called with arguments.", "6.5.2.2:6, J.2:1 item 38"))
-          ~> bind(ListItem(typedDeclaration(T::Type, _)), _, ListItem(_) _)
-          requires isVoidType(T)
+          ~> bind(ListItem(typedDeclaration(T:VoidType, _)), _, ListItem(_) _)
      // Variadic.
      rule bind(ListItem(variadic), ListItem(variadic), Vs:List)
           => bindVariadics(Vs, 0)
           [structural]
      // No params.
-     rule bind(ListItem(typedDeclaration(T::Type, _)),
-               ListItem(typedDeclaration(T'::Type, _)), .List) => .K
-          requires isVoidType(T) andBool isVoidType(T')
-          [structural]
-     rule bind(ListItem(typedDeclaration(T::Type, _)),
+     rule bind(ListItem(typedDeclaration(T:VoidType, _)),
                .List, .List) => .K
-          requires isVoidType(T)
           [structural]
      // Builtins -- they don't have named parameters.
      rule <k> (.K => bindParam(unnamed(N, Tu), T, V))
@@ -97,9 +97,8 @@ module C-BINDING
           <next-unnamed> N:Int => N +Int 1 </next-unnamed>
           requires T =/=K variadic
           [structural]
-     rule bind(ListItem(T:Type),
-               ListItem(T':Type), .List) => .K
-          requires isVoidType(T) andBool isVoidType(T')
+     rule bind(ListItem(T:VoidType),
+               ListItem(T':VoidType), .List) => .K
           [structural]
      rule bind(.List, .List, .List) => .K
           [structural]
@@ -137,7 +136,7 @@ module C-BINDING
           [function]
 
      rule #arePromotedTypesCompat(_, T::UType, T'::UType) => true
-          requires areCompatible(type(argPromoteType(T)), type(argPromoteType(T')))
+          requires type(argPromoteType(T)) ==Type type(argPromoteType(T'))
 
      rule #arePromotedTypesCompat(V:Int, T::UType, T':SignedIntegerUType) => true
           requires (argPromoteType(T)
@@ -189,9 +188,9 @@ module C-BINDING
      syntax Bool ::= isArgPromoted(K) [function]
      rule isArgPromoted(variadic) => true
      rule isArgPromoted(typedDeclaration(T::Type, _))
-          => areCompatible(utype(T), argPromoteType(utype(T)))
+          => utype(T) ==Type argPromoteType(utype(T))
      rule isArgPromoted(T:Type)
-          => areCompatible(utype(T), argPromoteType(utype(T)))
+          => utype(T) ==Type argPromoteType(utype(T))
 
 endmodule
 
diff --git a/semantics/language/common/bitsize.k b/semantics/language/common/bitsize.k
@@ -66,14 +66,6 @@ module C-BITSIZE
      rule numBytes(ut(Mods::Set, enumType(_))) => numBytes(ut(Mods, cfg:enumAlias))
      rule numBytes(_) => 0 [owise]
 
-     syntax Int ::= byteSizeofList(List) [function]
-     syntax Int ::= "byteSizeofList'" "(" Int "," List ")" [function]
-
-     rule byteSizeofList(L:List) => byteSizeofList'(0, L)
-     rule byteSizeofList'(Sz:Int, ListItem(T:Type) LL:List)
-          => byteSizeofList'((Sz +Int byteSizeofType(utype(T))), LL)
-     rule byteSizeofList'(Sz:Int, .List) => Sz
-
      syntax Int ::= "maxByteSizeofList'" "(" Int "," List ")" [function]
      rule maxByteSizeofList(L:List) => maxByteSizeofList'(0, L)
      rule maxByteSizeofList'(Sz:Int, ListItem(T:Type) LL:List)

diff --git a/semantics/language/common/expr/additive.k b/semantics/language/common/expr/additive.k
@@ -196,7 +196,7 @@ module C-COMMON-EXPR-ADDITIVE
           requires base(L1) ==K base(L2)
                andBool notBool isFunctionType(T) andBool notBool isFunctionType(T')
                andBool isCompleteType(T) andBool isCompleteType(T')
-               andBool areCompatible(stripQualifiers(T), stripQualifiers(T'))
+               andBool stripQualifiers(T) ==Type stripQualifiers(T')
           [structural]
 
      // uintptr_t
@@ -213,10 +213,8 @@ module C-COMMON-EXPR-ADDITIVE
                andBool (isFunctionType(innerType(utype(L))) orBool isFunctionType(innerType(utype(R)))
                     orBool notBool isCompleteType(innerType(utype(L)))
                     orBool notBool isCompleteType(innerType(utype(R)))
-                    orBool notBool
-                    areCompatible(
-                         stripQualifiers(innerType(utype(L))),
-                         stripQualifiers(innerType(utype(R)))))
+                    orBool stripQualifiers(innerType(utype(L)))
+                         =/=Type stripQualifiers(innerType(utype(R))))
 
      rule (.K => UNDEF("CEA5", "Computing pointer difference between two different objects.",
           "6.5.6:9, J.2:1 item 48"))

diff --git a/semantics/language/common/expr/bitwise.k b/semantics/language/common/expr/bitwise.k
@@ -71,7 +71,7 @@ module C-COMMON-EXPR-BITWISE
      rule (.K => UNDEF("CEB4",
                "The left operand in a bitwise left-shift is negative.",
                "6.5.7:4, J.2:1 item 52"))
-          ~> tv(E1:Int, T1::UType) << R:RValue
+          ~> tv(E1:Int, T1:SignedIntegerUType) << R:RValue
           requires isPromoted(T1) andBool isPromoted(utype(R))
                andBool E1 <Int 0
           [structural]
@@ -90,7 +90,7 @@ module C-COMMON-EXPR-BITWISE
           requires isPromoted(T1) andBool isPromoted(T2)
                andBool E2 >=Int 0
                andBool E2 <Int bitSizeofType(T1)
-               andBool (E1 >=Int 0 orBool notBool isSignedIntegerType(T1))
+               andBool E1 >=Int 0
           [structural]
      rule (.K => CV("CEB5",
                "Both bitwise shift operands must have integer type.",
@@ -116,9 +116,9 @@ module C-COMMON-EXPR-BITWISE
      rule (.K => IMPL("CEB8",
                "The left operand in a bitwise right-shift is negative.",
                "6.5.7:5, J.3.5:1 item 5"))
-          ~> tv(E1:Int, T1::UType) >> R:RValue
+          ~> tv(E1:Int, T1:SignedIntegerUType) >> R:RValue
           requires isPromoted(T1) andBool isPromoted(utype(R))
-               andBool E1 <Int 0 andBool isSignedIntegerType(T1)
+               andBool E1 <Int 0
           [structural]
 
      /*@ \fromStandard{\source[n1570]{\para{6.5.10}{3--4}}}{

diff --git a/semantics/language/common/type-builder.k b/semantics/language/common/type-builder.k
@@ -1,7 +1,7 @@
 module C-TYPE-BUILDER-SYNTAX
      imports C-TYPING-SYNTAX
 
-     syntax FlexType ::= Type | SimpleType
+     syntax FlexType ::= Type | SimpleType | Variadic
 
      syntax Type ::= fun(FlexType) [function, klabel(fun1)]
                    | fun(FlexType, FlexType) [function, klabel(fun2)]
@@ -75,6 +75,7 @@ module C-TYPE-BUILDER
 
      syntax Type ::= expand(FlexType) [function]
      rule expand(T:Type) => T
+     rule expand(T:Variadic) => T
      rule expand(T:SimpleType) => type(T)
 
      syntax UType ::= expandut(FlexType) [function]

diff --git a/semantics/language/common/typing.k b/semantics/language/common/typing.k
@@ -59,9 +59,10 @@ module C-TYPING-SYNTAX
      syntax Bool ::= Quals "<=Quals" Quals [function]
 
      // Basic types
-     syntax SimpleSignedBitfieldType ::= bitfieldType(SimpleSignedIntType, Int)
-     syntax SimpleUnsignedBitfieldType ::= bitfieldType(SimpleUnsignedIntType, Int)
-                                         | bitfieldType(SimpleBoolType, Int)
+     syntax SimpleBitfieldType ::= SimpleSignedBitfieldType | SimpleUnsignedBitfieldType
+                                 | bitfieldType(BitfieldFieldType, Int)
+     syntax SimpleSignedBitfieldType ::= bitfieldType(SignedBitfieldFieldType, Int)
+     syntax SimpleUnsignedBitfieldType ::= bitfieldType(UnsignedBitfieldFieldType, Int)
 
      syntax SimpleCharType ::= "char" [function]
      syntax SimpleSignedType ::= "short-int" | SimpleSignedIntType
@@ -82,11 +83,11 @@ module C-TYPING-SYNTAX
      syntax SimpleBoolType ::= "bool"
      syntax SimpleVoidType ::= "void"
      syntax SimpleNoType ::= "no-type"
-     syntax BitfieldFieldType ::= SimpleSignedIntType
-                                | SimpleUnsignedIntType
-                                | SimpleBoolType
+     syntax BitfieldFieldType ::= SignedBitfieldFieldType | UnsignedBitfieldFieldType
+     syntax SignedBitfieldFieldType ::= SimpleSignedIntType
+     syntax UnsignedBitfieldFieldType ::= SimpleUnsignedIntType | SimpleBoolType
      syntax SimpleIntegerType ::= SimpleSignedType | SimpleUnsignedType
-                                | bitfieldType(BitfieldFieldType, Int)
+                                | SimpleBitfieldType
                                 | BitfieldFieldType
 
      syntax SimpleBasicType ::= SimpleNoType | SimpleVoidType | SimpleCharType
@@ -145,7 +146,8 @@ module C-TYPING-SYNTAX
      syntax SimpleUType ::= SimpleTypedefType
 
      syntax SimpleTypedefType ::= typedefType(CId, Type)
-     syntax Type ::= "variadic"
+     syntax Variadic ::= "variadic"
+     syntax DType ::= Variadic
 
      syntax Type ::= BasicType | PointerType | AggregateOrUnionType
                    | StructOrUnionType | ArrayOrFunctionType
@@ -165,16 +167,19 @@ module C-TYPING-SYNTAX
      syntax UnsignedIntegerType ::= UCharType | BoolType | UnsignedBitfieldType
      syntax CharType ::= UCharType | SCharType
      syntax BitfieldType ::= UnsignedBitfieldType | SignedBitfieldType
+                           | t(Quals, Set, SimpleBitfieldType)
      syntax ArrayType ::= FixedLengthArrayType | IncompleteArrayType
                         | VariableLengthArrayType
      syntax PointerOrArrayType ::= PointerType | ArrayType
 
      syntax ArrayOrFunctionUType ::= FunctionUType
                                    | FixedLengthArrayUType | IncompleteArrayUType
                                    | VariableLengthArrayUType
-     syntax IntegerUType ::= UnsignedIntegerUType | SignedIntegerUType
+     syntax IntegerUType ::= UnsignedIntegerUType | SignedIntegerUType | BitfieldUType
      syntax SignedIntegerUType ::= SCharUType | SignedBitfieldUType
      syntax UnsignedIntegerUType ::= UCharUType | BoolUType | UnsignedBitfieldUType
+     syntax BitfieldUType ::= SignedBitfieldUType | UnsignedBitfieldUType
+                            | ut(Set, SimpleBitfieldType)
 
      syntax UnsignedIntegerType ::= t(Quals, Set, SimpleUnsignedType)
      syntax SignedIntegerType ::= t(Quals, Set, SimpleSignedType)
@@ -308,6 +313,7 @@ module C-TYPING-SYNTAX
      // Turns old-style param list into the empty list so that arguments will
      // be promoted on call.
      syntax Type ::= toPrototype(Type) [function]
+
 endmodule
 
 module C-TYPING