Module dev.civl.abc
Package dev.civl.abc.ast.type.IF

Interface TypeFactory

public interface TypeFactory

A factory for producing C types, which are represented as instances of Type. C types are complicated. First, types have state which may change during compile-time processing of the translation unit. For example, at any point in the translation unit, an object type is either complete or incomplete, and this may change. Example: 

 typedef struct Node {
   struct Node *next;
 } list;
Immediately after the struct Node the structure type exists, but is incomplete. It becomes complete immediately after the }.

A Type may be associated to an Entity (more precisely, to any Entity other than a Label). The type associated to an Entity may change as declarations of that Entity are processed.

Types are immutable, with the following exception: a tagged type (instance of StructureOrUnionType or EnumerationType) may start off as incomplete and later be completed. Hence any other types that have a reference to that tagged type will also reflect the change. On the other hand, an array declared with an incomplete type, such as int a[] and later declared with a complete type such as int a[5] does not result in a modifcation to the ArrayType object. Instead, the type associated to the Variable named a is changed from the incomplete type int[] to the complete type int[5].

There are two kinds of types: function and object types. These are represented by two interfaces, FunctionType and ObjectType, each of which extends Type.

Detailed information on specified types:

ArrayType: this is an object type specified by an element type and the extent. The element type must be a complete object type. For the extent, there are 4 possibilities:

  1. the extent is not specified (i.e., is null): then the array type is an incomplete type. It becomes complete when the extent is specified in a later declaration.
  2. the extent is *: this is a VLA type of unspecified size. It is nevertheless a complete type. This can only be used in declarations or type names in function prototype scope (i.e., in a function declaration that is not part of a function definition).
  3. the extent is an integer constant expression and the element type has known constant size: then the array type is not a VLA type. It is complete.
  4. otherwise, the extent is an expression which is not a constant expression or the element type does not have known constant size. This is a VLA type. It is complete. If it occurs in function prototype scope, it is replaced by * (i.e., the expression is not used).

Some vocabulary:

  • An object type has known constant size iff it is not incomplete and not a VLA (Variable Length Array) type.
  • A variably modified (VM) type is a declarator type which in the nested sequence of declarators has a VLA type, or any type derived from a VM type. I.e.: a VLA is a VM; a pointer to a VM is a VM; a function returning a VM is a VM; an array with a VM element type is a VM.

Some restrictions:

  • An identifier declared with a VM type must be an object, be an ordinary identifier, have no linkage, and have either block or function prototype scope.
  • An object declared with static or thread storage duration shall not have a VLA type (but may have a VM type).
  • Pointer types are always complete object types (even if the referenced type is not).

A structure or union type exists (come into scope) as soon as the tag name first appears, but is incomplete until the } is reached, then it is complete. The last member may be an incomplete array type. Members must have object types and cannot have VM types.

Enumeration types: complete once } is reached.

Atomic types: the base type cannot be array, function, atomic, or qualified.

void: is an incomplete object type that can never be completed.

Function Types: a function type is specified by the return type and types of the parameters. In function definitions: the parameter types (after adjustment) cannot be incomplete. Hence once you get to the definition, all parameter types must be complete (or an exception will be thrown). The adjustments: a parameter of type qualified array of T is changed to qualified pointer to T; qualified function returning T changed to qualified pointer to function returning T.

Qualifiers:

  • A type can come with qualifiers: const, restrict, volatile, _Atomic.
  • If the specification of an array type includes any type qualifiers, the element type is so-qualified, not the array type. If the specification of a function type includes any type qualifiers, the behavior is undefined. [Both can happen through typedefs.] Moreover, restrict can only be used with pointer types whose referenced type is an object type. _Atomic can not be used with an array or function type.
  • If the _Atomic qualifier occurs (possibly with other qualifiers), the result is the so-qualified Atomic type.

See C11 Sec. 5.2.4.2.1 for the minimum values of the bounds for each standard integer type.

  • Field Details

  • Method Details

    • basicType

      StandardBasicType basicType(StandardBasicType.BasicTypeKind kind)
      Returns an instance of BasicType representing the type of the given basic type kind and qualified as specified. It is unspecified whether this method will return a new instance each time it is invoked, or will use something like a flyweight pattern to share instances. This choice should be invisible to the user, since the basic types are immutable.
      Parameters:
      kind - one of the basic type kinds
      Returns:
      an instance of BasicType corresponding to the given parameters

    • signedIntegerType

      StandardSignedIntegerType signedIntegerType(StandardSignedIntegerType.SignedIntKind kind)
      Returns the standard signed integer type of the given kind. While these types are all basic types and can therefore be obtained by method basicType, this method is sometimes more convenient. There are 5 standard signed integer types.
      Parameters:
      kind - the signed integer type kind; note that the names of the elements of this enumerated type are exactly the same as the names of the corresponding types in BasicTypeKind
      Returns:
      the signed integer type of that kind

    • unsignedIntegerType

      StandardUnsignedIntegerType unsignedIntegerType(StandardUnsignedIntegerType.UnsignedIntKind kind)
      Returns the standard unsigned integer type of the given kind. While these types are all basic types and can therefore be obtained by method basicType, this method is sometimes more convenient. There are 6 standard unsigned integer types (those corresponding to the standard signed integer types, and _Bool).
      Parameters:
      kind - the unsigned integer type kind; note that the names of the elements of this enumerated type are exactly the same as the names of the corresponding types in BasicTypeKind
      Returns:
      the unsigned integer type of that kind

    • pointerType

      PointerType pointerType(Type referencedType)
      Returns an instance of PointerType with the given referenced type. It is unspecified whether this returns a new instance each time it is called or can return previously returned instances.
      Parameters:
      referencedType - the base type of the pointer type
      Returns:
      a pointer type as specified

    • atomicType

      AtomicType atomicType(UnqualifiedObjectType baseType)
      The atomic type associated to a base type. This type may be denoted _Atomic(baseType) or by using the type qualifier _Atomic in a declaration. The base type cannot be an array type, a function type, an atomic type, or a qualified type. However, the resulting AtomicType can be qualified.
      Parameters:
      baseType - the base type
      Returns:
      the atomic type

    • incompleteArrayType

      ArrayType incompleteArrayType(ObjectType elementType)
      Returns an incomplete array type (i.e., the extent is not specified). Note: according to the C standard, qualifiers applied to an array type are actually applied to the element type.
      Parameters:
      elementType - a complete object type
      Returns:
      an incomplete array type with given element type

    • arrayType

      ArrayType arrayType(ObjectType elementType, IntegerValue constantExtent)
      Returns a complete array type in which the size expression has been evaluated to a known constant value.
      Parameters:
      elementType - the type of the elements of the array
      constantExtent - the constant array length
      Returns:
      the complete array type with constant extent

    • unspecifiedVariableLengthArrayType

      ArrayType unspecifiedVariableLengthArrayType(ObjectType elementType)
      Returns a complete array type of "unspecified variable length". This is declared using a "*" for the size expression. This can only be used in function prototype scope.
      Parameters:
      elementType -
      Returns:
      complete array type of unspecified variable length

    • variableLengthArrayType

      ArrayType variableLengthArrayType(ObjectType elementType, ExpressionNode variableSize)
      Returns a complete array type in which the size expression cannot be evaluated to a known constant value.
      Parameters:
      elementType - the type of the elements of the array
      variableSize - the expression which defines the extent (length) of the array
      Returns:
      a complete array type as specified

    • structureOrUnionType

      StructureOrUnionType structureOrUnionType(Object key, boolean isStruct, String tag)
      Returns a new incomplete structure or union type with the given tag. The type can be completed using methods in the resulting StructureOrUnionType object.
      Parameters:
      key - a key to use to determine if two StructureOrUnionType instances with same tag and "isStruct" values are to be considered equal.
      isStruct - is this a structure type (as opposed to union)?
      tag - the tag for the structure or union, as in "struct TAG ..."; may be null for an anonymous structure or union
      Returns:
      a new, incomplete StructureOrUnion type

    • newField

      Field newField(FieldDeclarationNode declaration, ObjectType type, Value bitWidth)
      Creates a new field entity. These correspond to the field declarations in a complete structure or union definition.
      Parameters:
      declaration - the field declaration
      type - the type of the field
      bitWidth - the optional bit width parameter
      Returns:
      the new field

    • enumerationType

      EnumerationType enumerationType(Object key, String tag)
      Returns an enumeration type with the given tag and key. The type can be completed using methods in the resulting EnumerationType object.
      Parameters:
      key - an object used to uniquely identify the enumeration type; it is used in the equals method
      tag - the tag for the enumeration type, as in "enum TAG ..."; may be null for an anonymous enumeration type
      Returns:
      a new, incomplete enumeration type

    • newEnumerator

      Enumerator newEnumerator(EnumeratorDeclarationNode declaration, EnumerationType enumeration, Value value)
      Creates a new enumerator entity. These correspond to the enumerators in the enumerator list of a complete enumeration definition.
      Parameters:
      declaration - the declaration of the enumerator in the enuemrator list
      enumeration - the enumeration of which this enumerator is a part
      value - the constant integer value associated to the enumerator
      Returns:
      the new enumerator entity

    • qualifiedType

      QualifiedObjectType qualifiedType(UnqualifiedObjectType baseType, boolean constQualified, boolean volatileQualified, boolean restrictQualified, boolean inputQualified, boolean outputQualified)
      Returns a qualified type based on the given unqualified type. At least one of the 3 qualifiers must be true.
      Parameters:
      baseType - an unqualified object type
      constQualified - should the resulting type be "const" qualified?
      volatileQualified - should the resulting type be "volatile" qualified?
      restrictQualified - should the resulting type be "restrict" qualified?
      inputQualified - should the result type be "_input" qualified?
      outputQualified - should the resulting type be "_output" qualified?
      Returns:
      qualified version of given unqualified type

    • qualify

      ObjectType qualify(ObjectType startType, boolean constQualified, boolean volatileQualified, boolean restrictQualified, boolean inputQualified, boolean outputQualified)
      A more general algorithm for qualifying a type: for each true-valued parameter, the corresponding qualifier is "added" to the resulting type, i.e., if the type is already so-qualified, it is not changed, otherwise, the result will be so qualified. The given type (startType) may or may not already be a QualifiedObjectType. The 3 boolean parameters may or may not be all false. The result may or may not be a QualifiedObjectType.
      Parameters:
      startType - an object type
      constQualified - should the resulting type be "const" qualified?
      volatileQualified - should the resulting type be "volatile" qualified?
      restrictQualified - should the resulting type be "restrict" qualified?
      inputQualified - should the result type be "_input" qualified?
      outputQualified - should the resulting type be "_output" qualified?
      Returns:
      the correct object type properly qualified, possibly the original type as given.

    • compositeType

      Type compositeType(Type type1, Type type2)

      Given two compatible types, returns the "composite type" obtained by combining features of both types. If the two types are not compatible, the behavior is undefined. Hence, you should always check compatibility before invoking this method (i.e., check that type1.compatibleWith(type2) is true).

      Implementation: there are special rules for array and function types described in C11 Sec. 6.2.7(3). For all other types, the types have to be basically equivalent, so we just return type1.

      Parameters:
      type1 - a type
      type2 - a type which is compatible with type1
      Returns:
      the composite type

    • compositeArrayTypeInDeclarationForCIVLC

      Type compositeArrayTypeInDeclarationForCIVLC(Type varType, Type compositeType)

      Given a variable v declaration with an initializer, the declared type t1 of v and the composite type t2 , which strictly conforms C11 standard, for t1 and the type of the initializer , returns the composite type, which conforms CIVL-C extention, for t1 and t2.

      The composite type conforming CIVL-C follows one rule: if a sub-type t in t1 is an array type with variable length, the corresponding sub-type in the composite type has the same type as t

      Parameters:
      varType - the declared type of
      compositeType - the composite type for the declared type and the initializer type conforming C11 standard
      Returns:
      the composite type conforming CIVL-C extention

    • functionType

      FunctionType functionType(ObjectType returnType)
      Returns the function type with the given return type but with no information on the parameters. The return type cannot be an array type or a function type.
      Parameters:
      returnType - the return type of the function
      Returns:
      the function type

    • functionType

      FunctionType functionType(ObjectType returnType, boolean fromIdentifierList, Iterable<ObjectType> parameterTypes, boolean hasVariableArgs)
      Returns the function type with the given return type and parameter type list. The return type cannot be an array type or a function type.
      Parameters:
      returnType - the type returned by calls to the function
      fromIdentifierList - was this type generated from a function definition using an identifier list (as opposed to a parameter type list)?
      parameterTypes - the type of each parameter
      hasVariableArgs - is the "..." used in the declaration?
      Returns:
      a function type as specified in which the types of the parameters is known

    • getNumTypes

      int getNumTypes()
      Returns the number of distinct types controlled by this type factory.
      Returns:
      the number of types conrolloed by this type factory

    • getType

      Type getType(int id)
      Returns the id-th type conrolled by this type factory.
      Parameters:
      id - an int in the range [0,numTypes-1]
      Returns:
      the id-th type

    • getTypes

      Iterable<Type> getTypes()
      Returns the set of types controlled by this type factory as an Iterable object. The iterator will return the types in order of increasing ID.
      Returns:
      sequence of types controlled by this type factory

    • printTypes

      void printTypes(PrintStream out)
      Prints a human-readable description of all the types controlled by this type factory.
      Parameters:
      out - a print stream to which the output should be sent

    • integerPromotion

      IntegerType integerPromotion(IntegerType type)
      C11 6.3.1.1:

      The following may be used in an expression wherever an int or unsigned int may be used:

      • An object or expression with an integer type (other than int or unsigned int) whose integer conversion rank is less than or equal to the rank of int and unsigned int.
      • A bit-field of type _Bool, int, signed int, or unsigned int.

      If an int can represent all values of the original type (as restricted by the width, for a bit-field), the value is converted to an int; otherwise, it is converted to an unsigned int. These are called the integer promotions. All other types are unchanged by the integer promotions.

      The integer promotions preserve value including sign. As discussed earlier, whether a "plain" char is treated as signed is implementation-defined.

      Parameters:
      type -
      Returns:
      the integer promotion

    • rangeChoice

      IntegerType rangeChoice(BigInteger value, IntegerType type1, IntegerType type2)
      Returns a integer type object T with the following semantics: if the value falls within the range of type1, T represents type1, else T represents type2. These expressions can be nested to form a sequence of tests. If it can be determined that value lies (resp., does not lie) in the range of type1 for all conforming C implementations, then this method may just return type1 (resp., type2).
      Parameters:
      value - an integer
      type1 - an integer type
      type2 - an integer type
      Returns:
      an integer type with the semantics described above

    • rangeChoice

      IntegerType rangeChoice(BigInteger value, IntegerType[] typeList)
      Returns an IntegerType T with the following semantics: if the value falls within the range of typeList[0] then typeList[0], else if the value falls within the range of typeList[1] then typeList[1], else if ...., else if the value falls within the range of typeList[n-1] then typeList[n-1], else null. Here, n=typeList.length.
      Parameters:
      value - an integer
      typeList - a sequence of integer types; it could have length 0, but this would not be very useful (result is equivalent to null).
      Returns:
      an IntegerType with the semantics defined above.

    • size_t

      UnsignedIntegerType size_t()
      Returns the type size_t. The C Standard specified that every C implementation must define an unsigned integer type called size_t. It is the return type of the sizeof operator. It may or may not be one of the standard unsigned integer types. Repeated calls to this method will always return the same type.
      Returns:
      the unsigned integer type size_t.

    • ptrdiff_t

      SignedIntegerType ptrdiff_t()
      Returns the type ptrdiff_t,
      which is the signed integer type of the result of subtracting two pointers;
      (C11, Sec.7.19).
      Returns:
      the signed integer type ptrdiff_t

    • wchar_t

      IntegerType wchar_t()
      Returns the type wchar_t:
      an integer type whose range of values can represent distinct codes for all members of the largest extended character set specified among the supported locales; the null character shall have the code value zero. Each member of the basic character set shall have a code value equal to its value when used as the lone character in an integer character constant if an implementation does not define _ _STDC_MB_MIGHT_NEQ_WC_ _.
      (C11, Sec. 7.19).
      Returns:
      the integer type wchar_t

    • char16_t

      UnsignedIntegerType char16_t()
      Returns the type char16_t, "...an unsigned integer type used for 16-bit characters and is the same type as uint_least16_t (described in 7.20.1.2)", defined in Sec. 7.28, uchar.h.
      Returns:
      the integer type char16_t

    • char32_t

      UnsignedIntegerType char32_t()
      Returns the type char32_t, "...an unsigned integer type used for 32-bit characters and is the same type as uint_least32_t (also described in 7.20.1.2)."
      Returns:
      the intger type char32_t

    • voidType

      ObjectType voidType()
      Returns an instance of ObjectType representing the "void" type. This is an incomplete object type which can never be completed. It is unspecified whether this method always returns a new instance or the same instance. The choice is invisible, since the type returned is immutable.
      Returns:
      an instance of the void type

    • floatingType

      FloatingType floatingType(FloatingType.FloatKind kind, boolean isReal)
      Returns the floating point type (real or complex) as specified. As these types are all standard basic types, they can also be obtained by method basicType, but this method is provided because it is more convenient in certain contexts.
      Parameters:
      kind - the kind of floating type: LONG_DOUBLE, DOUBLE, or FLOAT (whether real or complex)
      isReal - is this a real type (not complex)?
      Returns:
      one of the basic types LONG_DOUBLE, DOUBLE, FLOAT, LONG_DOUBLE_COMPLEX, DOUBLE_COMPLEX, or FLOAT_COMPLEX, as specified

    • processType

      ObjectType processType()
      Returns the process type.

    • heapType

      ObjectType heapType()
      Returns the heap type.

    • memType

      MemType memType(PointerType elementType)
      Creates the MemType
      Parameters:
      the - element tyoe of this mem type
      Returns:
      the mem type

    • theSetType

      SetType theSetType(ObjectType elementType)
      Creates a SetType with the given element type.
      Parameters:
      elementType - the element type of the returned set type
      Returns:
      a SetType

    • scopeType

      ObjectType scopeType()
      Returns the scope type

    • rangeType

      ObjectType rangeType()
      Returns the CIVL-C range type, denoted $range, which represents a sequence of integers.
      Returns:
      the range type

    • domainType

      DomainType domainType()
      Returns the universal domain type $domain. The domain type consists of all finite tuples of integers.

    • domainType

      DomainType domainType(int dimension)
      Returns the domain type with specified dimension, $domain(n) . This is a sub-type of $domain, which is the union over all positive integers n $domain(n).
      Parameters:
      dimension - the dimension of the domain type, i.e., the arity of the tuples in the domain
      Returns:
      the domain type of the given dimension

    • usualArithmeticConversion

      ArithmeticType usualArithmeticConversion(ArithmeticType type1, ArithmeticType type2)
      Computes the type resulting from the "usual arithmetic conversion". From C11 Sec. 6.3.1.8:
      Many operators that expect operands of arithmetic type cause conversions and yield result types in a similar way. The purpose is to determine a common real type for the operands and result. For the specified operands, each operand is converted, without change of type domain, to a type whose corresponding real type is the common real type. Unless explicitly stated otherwise, the common real type is also the corresponding real type of the result, whose type domain is the type domain of the operands if they are the same, and complex otherwise. This pattern is called the usual arithmetic conversions:
      • First, if the corresponding real type of either operand is long double, the other operand is converted, without change of type domain, to a type whose corresponding real type is long double.
      • Otherwise, if the corresponding real type of either operand is double, the other operand is converted, without change of type domain, to a type whose corresponding real type is double.
      • Otherwise, if the corresponding real type of either operand is float, the other operand is converted, without change of type domain, to a type whose corresponding real type is float.
      • Otherwise, the integer promotions are performed on both operands. Then the following rules are applied to the promoted operands:
        • If both operands have the same type, then no further conversion is needed.
        • Otherwise, if both operands have signed integer types or both have unsigned integer types, the operand with the type of lesser integer conversion rank is converted to the type of the operand with greater rank.
        • Otherwise, if the operand that has unsigned integer type has rank greater or equal to the rank of the type of the other operand, then the operand with signed integer type is converted to the type of the operand with unsigned integer type.
        • Otherwise, if the type of the operand with signed integer type can represent all of the values of the type of the operand with unsigned integer type, then the operand with unsigned integer type is converted to the type of the operand with signed integer type.
        • Otherwise, both operands are converted to the unsigned integer type corresponding to the type of the operand with signed integer type.
      Parameters:
      type1 - an arithmetic type
      type2 - an arithmetic type
      Returns:
      the type of the result of the "usual arithmetic conversion" applied to the two types

    • qualify

      ObjectType qualify(ObjectType startType, boolean atomic, boolean constQualified, boolean volatileQualified, boolean restrictQualified, boolean inputQualified, boolean outputQualified)
      Adds qualifiers and atomic designation as needed to the given type.
      Parameters:
      startType - any object type (qualified or unqualified, atomic or non-atomic)
      atomic - add atomic qualification to type if not already present?
      constQualified - and const qualification to type if not already present?
      volatileQualified - add volatile qualification to type if not already present?
      restrictQualified - add restrict qualification to type if not already present?
      Returns:
      type with given qualifications added (none are removed)

    • lambdaType

      ObjectType lambdaType(Type freeVariableType, Type lambdaFunctionType)
      Returns a LambdaType which consists of the type of the free variable of the lambda term. (void if the free variable is absent); and the type of the lambda function (the lambda function is an expression).
      Parameters:
      freeVariableType - The type of the free variable of the lambda term.
      lambdaFunctionType - The type of the lambda function expression.
      Returns:

    • isArrayOfCharType

      boolean isArrayOfCharType(Type type)
      Is the given type an array-of-char type?
      Parameters:
      type -
      Returns:

    • isVoidType

      boolean isVoidType(Type type)
      Is the given type a void type?
      Parameters:
      type -
      Returns:

    • isBundleType

      boolean isBundleType(Type type)
      Is the given type a CIVL-C bundle type?
      Parameters:
      type -
      Returns:

    • isPointerType

      boolean isPointerType(Type type)
      Is the given type a (qualified or unqualified) pointer type?
      Parameters:
      type -
      Returns: