Module dev.civl.mc
Package dev.civl.mc.model.IF

Interface CIVLTypeFactory

public interface CIVLTypeFactory
The CIVL type factory provides the CIVL primitive types, like $bool, int, float, $scope , etc. It also constructs the heap type and bundle type, which are model-sensitive, and could be different from model to model.

  • Method Details

    • booleanType

      CIVLPrimitiveType booleanType()
      Get the boolean primitive type.
      Returns:
      The boolean primitive type.

    • bundleSymbolicType

      dev.civl.sarl.IF.type.SymbolicUnionType bundleSymbolicType()
      Returns the symbolic type of the bundle type.
      Returns:
      the symbolic type of the bundle type.

    • bundleType

      CIVLBundleType bundleType()
      Gets the CIVL bundle type, which is unique for a given CIVL model. A bundle type is a union type of all types referenced by a given CIVL model. A bundle type needs to be completed at the end of the construction of the model.
      Returns:
      the CIVL bundle type of the model

    • charType

      CIVLPrimitiveType charType()
      Get the char primitive type.
      Returns:
      The char primitive type.

    • completeArrayType

      CIVLCompleteArrayType completeArrayType(CIVLType elementType, Expression extent)
      Returns a new complete array type with specified extent (length expression) and element type.
      Parameters:
      elementType - the type of each element in the array
      extent - the expression of integer type specifying the length of the array
      Returns:
      the complete array type, as specified

    • completeDomainType

      CIVLCompleteDomainType completeDomainType(CIVLType rangeType, int dim)
      Creates a complete regular domain type, which is has the given dimension and is composed by the given range type.
      Parameters:
      rangeType - the range type
      dim - the dimension of the domain type
      Returns:
      the complete regular domain type.

    • domainType

      CIVLDomainType domainType(CIVLType rangeType)
      This returns the universal domain type ($domain). It includes all the complete domain types ($domain(n)).
      Parameters:
      rangeType -
      Returns:
      the universal domain type

    • dynamicType

      CIVLPrimitiveType dynamicType()
      Get the dynamic type.
      Returns:
      The dynamic type.

    • enumType

      CIVLEnumType enumType(String name, Map<String,BigInteger> valueMap)
      Creates a new instance of enumeration type with the specified name.
      Parameters:
      name - The name of the enumeration type to be created.
      valueMap - The map of enumerator names and their values.
      Returns:
      The new enumeration type.

    • functionType

      CIVLFunctionType functionType(CIVLType returnType, CIVLType[] paraTypes)
      Creates a new instance of function type, which contains a return type and a list of parameter types.
      Parameters:
      returnType - The return type of the function type.
      paraTypes - The parameter types of the function type.
      Returns:
      the new function type

    • heapType

      CIVLHeapType heapType(String name)
      Returns a new, incomplete heap type. The heap type must be completed later by specifying a sequence of malloc statements in method completeHeapType(dev.civl.mc.model.IF.type.CIVLHeapType, java.util.Collection<dev.civl.mc.model.IF.statement.MallocStatement>).
      Parameters:
      name - a name to give to the new heap type
      Returns:
      a new incomplete heap type

    • incompleteArrayType

      CIVLArrayType incompleteArrayType(CIVLType elementType)
      Get a new incomplete array type.
      Parameters:
      elementType - The type of each element in the array.
      Returns:
      A new array type with the given base type.

    • integerType

      CIVLPrimitiveType integerType()
      Get the integer primitive type.
      Returns:
      The integer primitive type.

    • heapType

      CIVLHeapType heapType()
      Returns the CIVL heap type, which is unique for a given CIVL model. A heap type is a struct type of all types appearing in a malloc statement, plus all handled object types used by the model. A heap type needs to be completed at the end of the construction of the model.
      Returns:
      the CIVL heap type

    • heapSymbolicType

      dev.civl.sarl.IF.type.SymbolicType heapSymbolicType()
      Returns the symbolic heap type
      Returns:
      the symbolic heap type

    • pointerType

      CIVLPointerType pointerType(CIVLType baseType)
      Get a new pointer type.
      Parameters:
      baseType - The type pointed to by the pointer.
      Returns:
      A new pointer type with the given base type.

    • processType

      CIVLPrimitiveType processType()
      Get the process type.
      Returns:
      The process type.

    • rangeType

      CIVLType rangeType()
      Returns the range type of the system.
      Returns:
      the range type of the system.

    • realType

      CIVLPrimitiveType realType()
      Get the real primitive type.
      Returns:
      The real primitive type.

    • scopeType

      CIVLScopeType scopeType()
      Get the scope primitive type.
      Returns:
      The scope primitive type.

    • structField

      StructOrUnionField structField(Identifier name, CIVLType type, int index, boolean isAnonymous, CIVLStructOrUnionType enclosingType)
      Returns a new struct field, used to complete a struct type.
      Parameters:
      name - Identifier for the name of this struct member.
      type - The type of this struct member.
      index - Index of the field in its enclosing struct/union
      isAnonymous - Whether this field is an anonymous member
      enclosingType - The struct/union type directly containing this field.
      Returns:
      A struct field with the given name and type.

    • structOrUnionType

      CIVLStructOrUnionType structOrUnionType(Identifier name, boolean isStruct)
      Returns new incomplete struct or union type with given name. Type can be completed later using one of the "complete" methods in CIVLStructOrUnionType. The struct or union returned is a new instance of struct or union type that will never be equal to another struct or union type, regardless of identifier or fields.
      Parameters:
      name - identifier, usually the "tag" for this struct or union type
      isStruct - is the new type a struct type? If false, then the new type will be a union type
      Returns:
      a new incomplete struct or union type with given name

    • systemType

      CIVLType systemType(String name)
      Obtains the CIVL type by the given name. This returns the type that has been added by addSystemType(String, CIVLType), and returns null if no such type.
      Parameters:
      name - The name (key) of the type.
      Returns:
      the CIVL type of the given name

    • voidType

      CIVLPrimitiveType voidType()
      Returns the void type. Used in places where a type is required syntactically but there is no type, such as function which does not return a value.
      Returns:
      The CIVL void type

    • civlMemType

      CIVLMemType civlMemType()
      Returns the CIVLMemType. A mem type is the type of all expressions representing a set of pointers.
      Returns:
      the mem type, which is the type of all expressions representing a set of pointers

    • civlSetType

      CIVLSetType civlSetType(CIVLType elementType)
      Returns the CIVLSetType. A set type is the type of expressions that representing a set of objects of a non-set type.
      Parameters:
      elementType - the element type of the creating set type, note that the CIVLType.TypeKind of the element type cannot be CIVLType.TypeKind.SET
      Returns:
      the set type

    • dynamicSymbolicType

      dev.civl.sarl.IF.type.SymbolicTupleType dynamicSymbolicType()
      Returns the symbolic type used to represent values of type CIVLDynamicType
      Returns:
      the symbolic type used to represent values of type CIVLDynamicType

    • dynamicMemType

      dev.civl.sarl.IF.type.SymbolicType dynamicMemType()
      Returns:
      the symbolic type used to represent values of expressions of CIVLMemType

    • functionPointerSymbolicType

      dev.civl.sarl.IF.type.SymbolicTupleType functionPointerSymbolicType()
      Gets the symbolic function pointer type.
      Returns:
      the symbolic function pointer type.

    • pointerSymbolicType

      dev.civl.sarl.IF.type.SymbolicTupleType pointerSymbolicType()
      Returns the symbolic type used to represent pointers.
      Returns:
      he symbolic type used to represent pointers

    • processSymbolicType

      dev.civl.sarl.IF.type.SymbolicTupleType processSymbolicType()
      Returns the symbolic type used to represent process reference values
      Returns:
      the symbolic type used to represent process reference values

    • scopeSymbolicType

      dev.civl.sarl.IF.type.SymbolicType scopeSymbolicType()
      Returns the symbolic type used to represent scope values
      Returns:
      the symbolic type used to represent scope values

    • voidSymbolicType

      dev.civl.sarl.IF.type.SymbolicType voidSymbolicType()

    • addHeapFieldObjectType

      void addHeapFieldObjectType(CIVLType type, int id)
      Add the given type as the object type of one of the heap field. This will add one more element to the heap type.
      Parameters:
      type -
      id -

    • addSystemType

      void addSystemType(String name, CIVLType type)
      Added a type in map of system type, which is the map of types of system libraries, e.g., $gcomm/$comm for comm, $file for stdio, $gbarrier/$barrier for concurrency, etc. Each type that will be used by the system library components (e.g., library executor, etc) should be added explicitly by calling this method.
      Parameters:
      name - The name of the type.
      type - The type to be added as a system type

    • completeBundleType

      void completeBundleType(CIVLBundleType bundleType, List<CIVLType> eleTypes, Collection<dev.civl.sarl.IF.type.SymbolicType> types)
      Completes the bundle type by specifying the list of all dynamic types which can occur as bundle elements. If the collections yields a sequence of types t_i, then the bundle symbolic type is union_i(array(t_i)).
      Parameters:
      bundleType - an incomplete bundle type
      eleTypes - the list of types that could be the element of the bundle type
      types - the set of all dynamic types which occur as bundle elements

    • completeHeapType

      void completeHeapType(CIVLHeapType heapType, Collection<MallocStatement> mallocs)
      Completes the heap type.
      Parameters:
      heapType - an incomplete heap type
      mallocs - sequence of malloc statements that can access heaps of that type

    • getHeapFieldId

      int getHeapFieldId(CIVLType type)
      Returns the type of the heap field of the given index. A CIVL model has its unique heap type, which has type of tuples of arrays of arrays of type, determined by malloc statements and handle types appear in the source program. For examples, given the following program, 
       int main(){
   int* p = malloc(sizeof(int)*4);
   $gcomm gcomm = $gcomm_create(...);
   ...
 }
      the heap type of the model of this program will be (int[][], __gcomm__[][]).
      Parameters:
      type - the type which is a field of the heap type
      Returns:
      the ID of the type in the heap

    • initBundleType

      CIVLBundleType initBundleType()
      Initializes the bundle type of the model and return the result.
      Returns:
      The new initial bundle type.

    • sizeofDynamicType

      dev.civl.sarl.IF.expr.NumericExpression sizeofDynamicType(dev.civl.sarl.IF.type.SymbolicType dynamicType)
      Return the size of a dynamic type. Note that the given type must not contain any incomplete array type.
      Parameters:
      universe - a reference to the SymbolicUniverse
      the - a symbolic type
      Returns:
      the size of a dynamic type

    • expressionOfType

      dev.civl.sarl.IF.expr.SymbolicExpression expressionOfType(CIVLType civlType, dev.civl.sarl.IF.type.SymbolicType type)
      Given a symbolic type, returns a canonical symbolic expression which somehow wraps that type so it can be used as a value. Nothing should be assumed about the symbolic expression. To extract the type from such an expression, use method getType(dev.civl.sarl.IF.expr.SymbolicExpression).
      Parameters:
      civlType - the CIVL type that the symbolic type corresponds to.
      type - a symbolic type
      Returns:
      a canonical symbolic expression wrapping that type

    • getType

      dev.civl.sarl.IF.type.SymbolicType getType(dev.civl.sarl.IF.expr.SymbolicExpression expr)
      Given a symbolic expression returned by the method expressionOfType(dev.civl.mc.model.IF.type.CIVLType, dev.civl.sarl.IF.type.SymbolicType), this extracts the type that was used to create that expression. If the given expression is not an expression that was created by expressionOfType(dev.civl.mc.model.IF.type.CIVLType, dev.civl.sarl.IF.type.SymbolicType), the behavior is undefined.
      Parameters:
      expr - a symbolic expression returned by method expressionOfType(dev.civl.mc.model.IF.type.CIVLType, dev.civl.sarl.IF.type.SymbolicType)
      Returns:
      the symbolic type used to create that expression

    • getStaticTypeOfDynamicType

      CIVLType getStaticTypeOfDynamicType(dev.civl.sarl.IF.expr.SymbolicExpression typeId)
      Given a symbolic expression returned by the method expressionOfType(dev.civl.mc.model.IF.type.CIVLType, dev.civl.sarl.IF.type.SymbolicType), this returns the CIVLType which is associated to the dynamic type that was used to create the given expression. If the given expression is not an expression that was created by expressionOfType(dev.civl.mc.model.IF.type.CIVLType, dev.civl.sarl.IF.type.SymbolicType), the behavior is undefined.
      Parameters:
      expr - a symbolic expression returned by method expressionOfType(dev.civl.mc.model.IF.type.CIVLType, dev.civl.sarl.IF.type.SymbolicType)
      Returns:
      the corresponding CIVL type of the given dynamic type which was used to create the given expression

    • sizeofNonPrimitiveTypesFact

      dev.civl.sarl.IF.expr.BooleanExpression sizeofNonPrimitiveTypesFact()
      Returns:
      a boolean expression which is the fact about the size-of any non-primitive type, i.e. the size-of any non-primitive type is positive.