Fixes #264. (#265)

examples/error-codes/Error_Codes.csv

@@ -124,7 +124,7 @@ USP-STDLIB3,Called the atexit function after normal program termination has begu
 USP-STDLIB6,Called the at_quick_exit function after normal program termination has begun.,"7.22.4.3:2, J.1:1 item 45",Unspecified Behavior,
 CV-CCV9,Conversion from pointer to floating point type or from floating point type to pointer.,6.5.4:4,Constraint Violation,
 CV-CCV10,Conversion to or from non-scalar type.,6.5.4:2,Constraint Violation,
-CV-CDT3,Field has incomplete type.,"6.7.2.1:3",Constraint Violation,
+CV-CDT3,Field has incomplete type or contains a flexible array member.,"6.7.2.1:3",Constraint Violation,
 CV-CDT4,Field has incomplete type.,"6.7.2.1:3",Constraint Violation,
 CV-CEA7,Computing pointer addition of a pointer not to a complete object type.,6.5.6:2,Constraint Violation,
 CV-CEA8,Computing pointer minus integer of a pointer not to a complete object type.,6.5.6:3,Constraint Violation,
@@ -178,8 +178,9 @@ CV-FD2,Invalid return type in function definition.,6.7.6.3:1,Constraint Violatio
 CV-FD3,Incomplete parameter type in function definition.,6.7.6.3:4,Constraint Violation,
 CV-SSA1,Non-constant expression in static assertion.,6.7.10:2,Constraint Violation,
 CV-SSA2,Static assertion failed: ,6.7.10:2,Constraint Violation,
-CV-CTI3,The width of a bit field shall be an integer constant expression.,6.7.2.1:4,Constraint Violation,
 CV-CTI2,Arrays must have positive length.,6.7.6.2:1,Constraint Violation,
+CV-CTI3,The width of a bit field shall be an integer constant expression.,6.7.2.1:4,Constraint Violation,
+CV-CTI5,Structs containing a flexible array member must not be array elements.,6.7.2.1:2,Constraint Violation,
 IMPL-CCV2,Conversion to signed integer outside the range that can be represented.,"6.3.1.3:3, J.3.5:1 item 4",Implementation Defined Behavior,
 IMPL-CEB8,The left operand in a bitwise right-shift is negative.,"6.5.7:5, J.3.5:1 item 5",Implementation Defined Behavior,
 IMPL-CTI4,"Bit-field with type other than signed int, unsigned int, or _Bool.","6.7.2.1:5, J.3.9:1 item 2",Implementation Defined Behavior,

examples/error-codes/violates-constraint/fatal/CV-CTI5-bad-static.c

@@ -0,0 +1,12 @@
+// Copyright (c) 2015 Runtime Verification, Inc. (RV-Match team). All Rights Reserved.
+
+struct s {
+      int s;
+      int flex[];
+};
+
+struct s arr[5];
+
+int main(void){
+
+}

examples/error-codes/violates-constraint/fatal/CV-CTI5-bad-static.output

@@ -0,0 +1,3 @@
+CV-CTI5-bad-static.c:8:1: error: Structs containing a flexible array member must not be array elements.
+  Constraint violation (CV-CTI5). See C11 sec. 6.7.2.1:2
+Translation failed (config dumped). Run kcc -d CV-CTI5-bad-static.c to see commands run.

examples/error-codes/violates-constraint/nonfatal/CV-CDT3-bad-static.output

@@ -1,2 +1,2 @@
-CV-CDT3-bad-static.c:1:1: error: Field x has incomplete type.
-  Constraint violation (CV-CDT3). See C11 sec. 6.7.2.1:3
+CV-CDT3-bad-static.c:1:1: error: Field x has incomplete type or contains a flexible array member.
+  Constraint violation (CV-CDT3). See C11 sec. 6.7.2.1:2

examples/error-codes/violates-constraint/nonfatal/CV-CDT4-bad-static.output

@@ -1,2 +1,2 @@
 CV-CDT4-bad-static.c:1:1: error: Field y has incomplete type.
-  Constraint violation (CV-CDT4). See C11 sec. 6.7.2.1:3
+  Constraint violation (CV-CDT4). See C11 sec. 6.7.2.1:2

semantics/c11/language/common/memory/writing.k

@@ -372,7 +372,7 @@ module C-MEMORY-WRITING
      // Upgrade the effective type for a malloced region to an array.
      rule <k> setEffectiveType(loc(Base::SymBase, _), T'::Type) => .K ...</k>
           <mem>... Base |-> object(T::Type => type(arrayType(T', Len /Int byteSizeofType(T'))), Len::Int, _) ...</mem>
-          requires isNoType(T) andBool notBool isNoType(T') andBool notBool isFlexibleStruct(T')
+          requires isNoType(T) andBool notBool isNoType(T') andBool notBool isFlexibleType(T')
           [structural]
      rule <k> setEffectiveType(loc(Base::SymBase, _), T'::Type) => .K ...</k>
           <mem>... Base |-> object(T::Type, _, _) ...</mem>
@@ -382,7 +382,7 @@ module C-MEMORY-WRITING
      // malloced region.
      rule <k> setEffectiveType(loc(Base::SymBase, _), T'::Type) => .K ...</k>
           <mem>... Base |-> object(T::Type => lockFlexibleStruct(T', Len -Int byteSizeofType(T')), Len::Int, _) ...</mem>
-          requires isNoType(T) andBool isFlexibleStruct(T')
+          requires isNoType(T) andBool isFlexibleType(T')
           [structural]
      rule <k> setEffectiveType(Loc::SymLoc, _) => .K ...</k>
           <mem> Mem:Map </mem>

semantics/c11/language/common/typing.k

@@ -353,8 +353,9 @@ module C-TYPING-SYNTAX
      syntax Type ::= unlock(Int, Type) [function]
      syntax Type ::= unlockAll(Type) [function]
 
-     // True iff the type is a struct with a flexible array member.
-     syntax Bool ::= isFlexibleStruct(Type) [function]
+     // A flexible type is a struct with a flexible array member or a union
+     // with a member that has a flexible type.
+     syntax Bool ::= isFlexibleType(Type) [function]
 
      // Locks the type of the flexible array member to a fixed array.
      syntax Type ::= lockFlexibleStruct(Type, Int) [function]

semantics/c11/language/common/typing/common.k

@@ -17,6 +17,7 @@ module C-TYPING-COMMON
      imports FLOAT
 
      rule type(T:Type) => T
+     rule type(typedDeclaration(T::Type, _)) => T
      rule type(T:SimpleType) => t(noQuals, .Set, T)
      rule type(T:SimpleArrayUType) => t(noQuals, .Set, qualSimple(T))
      rule type(ut(Mods::Set, T::SimpleUType)) => t(noQuals, Mods, qualSimple(T))

semantics/c11/language/common/typing/predicates.k

@@ -101,12 +101,20 @@ module C-TYPING-PREDICATES
      rule isTruthValue(tv(V::CValue, ut(_, T::SimpleUType)))
           => T ==K int andBool (V ==K 0 orBool V ==K 1)
 
-     rule isFlexibleStruct(T:StructType) => isFlexibleStruct'(getFieldInfo(T))
-     rule isFlexibleStruct(_) => false [owise]
+     rule isFlexibleType(T:StructType) => isFlexibleStruct(getFieldInfo(T))
+     rule isFlexibleType(T:UnionType) => isFlexibleUnion(getFieldInfo(T))
+     rule isFlexibleType(_) => false [owise]
 
-     syntax Bool ::= "isFlexibleStruct'" "(" FieldInfo ")" [function]
-     rule isFlexibleStruct'(fieldInfo(_:List ListItem(typedDeclaration(T::Type, _)), _, _, _, _)) => true
+     syntax Bool ::= isFlexibleStruct(FieldInfo) [function]
+     rule isFlexibleStruct(fieldInfo(_:List ListItem(typedDeclaration(T::Type, _)), _, _, _, _)) => true
           requires isFlexibleArrayType(T)
-     rule isFlexibleStruct'(_) => false [owise]
+     rule isFlexibleStruct(_) => false [owise]
+
+     syntax Bool ::= isFlexibleUnion(FieldInfo) [function]
+     rule isFlexibleUnion(fieldInfo(_:List ListItem(typedDeclaration(T::Type, _)), _, _, _, _)) => true
+          requires isFlexibleType(T)
+     rule isFlexibleUnion(fieldInfo(_:List (ListItem(typedDeclaration(T::Type, _)) => .List), _, _, _, _))
+          requires notBool isFlexibleType(T)
+     rule isFlexibleUnion(_) => false [owise]
 
 endmodule

semantics/c11/language/translation/decl/tagged.k

@@ -46,7 +46,7 @@ module C-DECL-TAGGED
           ~> StructDef(_, krlist(L:List), _)
           requires notBool hasNamedField(L)
           [structural]
-     rule (.K => CV("CDT3", "Field " +String firstIncomplete(L) +String " has incomplete type.", "6.7.2.1:3"))
+     rule (.K => CV("CDT3", "Field " +String firstIncompleteOrFlexible(L) +String " has incomplete type or contains a flexible array member.", "6.7.2.1:2"))
           ~> StructDef(_, krlist(L:List), _)
           requires notBool structFieldsComplete(L)
           [structural]
@@ -58,7 +58,7 @@ module C-DECL-TAGGED
           ~> UnionDef(_, krlist(L:List), _)
           requires notBool hasNamedField(L)
           [structural]
-     rule (.K => CV("CDT4", "Field " +String firstIncomplete(L) +String " has incomplete type.", "6.7.2.1:3"))
+     rule (.K => CV("CDT4", "Field " +String firstIncomplete(L) +String " has incomplete type.", "6.7.2.1:2"))
           ~> UnionDef(_, krlist(L:List), _)
           requires notBool allComplete(L)
           [structural]
@@ -200,13 +200,18 @@ module C-DECL-TAGGED
 
      syntax Bool ::= structFieldsComplete(List) [function]
      rule structFieldsComplete(L::List ListItem(typedDeclaration(T::Type, _)))
-          => allComplete(L) andBool (isCompleteType(T) orBool isIncompleteArrayType(T))
+          => allComplete(L) andBool allRigid(L)
+               andBool ((isCompleteType(T) andBool isRigidType(T)) orBool isIncompleteArrayType(T))
      rule structFieldsComplete(.List) => true
 
      syntax Bool ::= allComplete(List) [function]
-     rule allComplete(ListItem(typedDeclaration(T::Type, _)) L::List)
-          => isCompleteType(T) andBool allComplete(L)
-     rule allComplete(.List) => true
+     rule allComplete(L::List) => all(mapList(L, #klabel(`type`)), #klabel(`isCompleteType`))
+
+     syntax Bool ::= allRigid(List) [function]
+     rule allRigid(L::List) => all(mapList(L, #klabel(`type`)), #klabel(`isRigidType`))
+
+     syntax Bool ::= isRigidType(Type) [function]
+     rule isRigidType(T::Type) => notBool isFlexibleType(T)
 
      syntax String ::= firstIncomplete(List) [function]
      rule firstIncomplete(ListItem(typedDeclaration(T::Type, X::CId)) _) => idToString(X)
@@ -215,6 +220,13 @@ module C-DECL-TAGGED
           requires isCompleteType(T)
      rule firstIncomplete(.List) => ""
 
+     syntax String ::= firstIncompleteOrFlexible(List) [function]
+     rule firstIncompleteOrFlexible(ListItem(typedDeclaration(T::Type, X::CId)) _) => idToString(X)
+          requires notBool isCompleteType(T) orBool isFlexibleType(T)
+     rule firstIncompleteOrFlexible((ListItem(typedDeclaration(T::Type, X::CId)) => .List) _)
+          requires isCompleteType(T) andBool notBool isFlexibleType(T)
+     rule firstIncompleteOrFlexible(.List) => ""
+
      rule makeUnionFieldInfo(Pack::Bool, Fs::List)
           => makeUnionFieldInfo'(Pack, Fs, .Map, .Map, .List)
 

semantics/c11/language/translation/typing/interpretation.k

@@ -50,25 +50,31 @@ module C-TYPING-INTERPRETATION
      context ArrayType(_, (HOLE:KItem => reval(HOLE)), _) [ndheat, result(RValue)]
      rule ArrayType(T:Type, tv(N:Int, T'::UType), Spec:K)
           => pushTypeDown(T, makeArrayType(tv(N, T'), Spec))
-          requires N >Int 0
+          requires N >Int 0 andBool notBool isFlexibleType(T)
           [structural]
      rule ArrayType(T:Type, UnspecifiedSizeExpression(), Spec:K)
           => pushTypeDown(T, makeArrayType(UnspecifiedSizeExpression(), Spec))
+          requires notBool isFlexibleType(T)
           [structural]
      rule ArrayType(T:Type, N:RValue, Spec:K)
           => pushTypeDown(T, makeArrayType(N, Spec))
-          requires isHold(N) // VLAs
+          requires isHold(N) andBool notBool isFlexibleType(T) // VLAs
           [structural]
      rule ArrayType(T:Type, emptyValue, _)
           => pushTypeDown(T, makeIncompleteArrayType)
+          requires notBool isFlexibleType(T)
           [structural]
      rule (.K => UNDEF("CTI1", "Arrays must have integer length.", "6.6:6, J.2:1 item 55"))
           ~> ArrayType(_, tv(_:Float, _), _)
           [structural]
      rule (.K => CV("CTI2", "Arrays must have positive length.", "6.7.6.2:1"))
-          ~> ArrayType(_:Type, tv(Len:Int, _), _)
+          ~> ArrayType(T:Type, tv(Len:Int, _), _)
           requires Len <=Int 0
           [structural]
+     rule (.K => CV("CTI5", "Structs containing a flexible array member must not be array elements.", "6.7.2.1:2"))
+          ~> ArrayType(T:Type, _, _)
+          requires isFlexibleType(T)
+          [structural]
 
      rule PointerType(Specifier(list(Mods:List)), T:Type)
           => pushTypeDown(T, makePointerType(listToSet(Mods)))

tests/unit-fail-compilation/flexible-array.c

@@ -0,0 +1,20 @@
+#include <stdlib.h>
+
+struct fam {
+      int a;
+      int fam[];
+};
+
+struct container {
+      int b;
+      struct fam f;  // <-------------- flagged by gcc as compiler extension
+};
+
+int main(void) {
+      struct container * c = malloc(100 * sizeof(int));
+      c->b = 1;
+      c->f.a = 2;
+      c->f.fam[5] = 3;
+      return c->f.fam[5];
+}
+

tests/unit-fail-compilation/flexible-array.ref

@@ -0,0 +1,3 @@
+flexible-array.c:8:1: error: Field f has incomplete type or contains a flexible array member.
+  Constraint violation (CV-CDT3). See C11 sec. 6.7.2.1:2
+Translation failed (config dumped). Run kcc -d flexible-array.c to see commands run.