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

Class ModelConfiguration

java.lang.Object
dev.civl.mc.model.IF.ModelConfiguration
public final class ModelConfiguration extends Object
This file contains the constants used by the model builder/translator, which reflects the translation strategy of CIVL. For example, for every scope, the heap variable is added as the variable with index 0.

  • Field Details

    • STATIC_CONSTANT_SCOPE

      public static final int STATIC_CONSTANT_SCOPE
      See Also:

    • STATIC_ROOT_SCOPE

      public static final int STATIC_ROOT_SCOPE
      See Also:

    • DYNAMIC_CONSTANT_SCOPE

      public static final int DYNAMIC_CONSTANT_SCOPE
      See Also:

    • DYNAMIC_NULL_SCOPE

      public static final int DYNAMIC_NULL_SCOPE
      See Also:

    • DYNAMIC_UNDEFINED_SCOPE

      public static final int DYNAMIC_UNDEFINED_SCOPE
      See Also:

    • NULL_POINTER_DYSCOPE

      public static final int NULL_POINTER_DYSCOPE
      See Also:

    • NULL_POINTER_VID

      public static final int NULL_POINTER_VID
      See Also:

    • UNDEFINED_PROC_ID

      public static final int UNDEFINED_PROC_ID
      See Also:

    • FILESYSTEM

      public static final String FILESYSTEM
      See Also:

    • GENERAL_ROOT

      public static final String GENERAL_ROOT
      See Also:

    • SYMBOL_PREFIXES

      public static final String[] SYMBOL_PREFIXES
      The array of prefixes for symbolic constants.

    • INPUT_PREIFX_INDEX

      public static final int INPUT_PREIFX_INDEX
      The prefix of symbolic constants representing input variables.
      See Also:

    • HAVOC_PREFIX_INDEX

      public static final int HAVOC_PREFIX_INDEX
      The prefix of symbolic constants created by havoc.
      See Also:

    • HEAP_OBJECT_PREFIX_INDEX

      public static final int HEAP_OBJECT_PREFIX_INDEX
      The prefix of symbolic constants representing heap objects.
      See Also:

    • INVALID

      public static final String INVALID
      Constant for the name of invalid heap objects.
      See Also:

    • RESERVE_NAMES

      public static Set<String> RESERVE_NAMES
      the set of reserved names for symbolic constants

    • SIZEOF_VARS

      public static Set<dev.civl.sarl.IF.expr.SymbolicConstant> SIZEOF_VARS

    • DECOMP_ALL

      public static final int DECOMP_ALL
      ALL, corresponds to the enumerator ALL of the enumeration type $domain_decomposition.
      See Also:

    • DECOMP_RANDOM

      public static final int DECOMP_RANDOM
      RANDOM, corresponds to the enumerator ALL of the enumeration type $domain_decomposition.
      See Also:

    • DECOMP_ROUND_ROBIN

      public static final int DECOMP_ROUND_ROBIN
      ROUND_ROBIN, corresponds to the enumerator ALL of the enumeration type $domain_decomposition.
      See Also:

    • ATOMIC_LOCK_VARIABLE_INDEX

      public static final String ATOMIC_LOCK_VARIABLE_INDEX
      The name of the atomic lock variable of the system scope.
      See Also:

    • TIME_COUNT_VARIABLE

      public static final String TIME_COUNT_VARIABLE
      The name of the time count variable, which is incremented by the system function $next_time_count() of civlc.cvh.
      See Also:

    • BROKEN_TIME_VARIABLE

      public static final String BROKEN_TIME_VARIABLE
      The variable to store broken time information for the time library. This variable is needed because some functions of time.h returns a pointer to it.
      See Also:

    • HEAP_VAR

      public static final String HEAP_VAR
      The name of the heap variable of each scope.
      See Also:

    • HEAP_VARIABLE_INDEX

      public static final int HEAP_VARIABLE_INDEX
      The index of the heap variable in the scope.
      See Also:

    • FILE_SYSTEM_TYPE

      public static final String FILE_SYSTEM_TYPE
      The name of the file system variable, created when stdio transformation is performed.
      See Also:

    • RANGE_TYPE

      public static final String RANGE_TYPE
      The name of the $range type.
      See Also:

    • PTHREAD_THREAD_TYPE

      public static final String PTHREAD_THREAD_TYPE
      The name of the "pthread_t" type defined in pthread library
      See Also:

    • PTHREAD_GPOOL

      public static final String PTHREAD_GPOOL
      The name of _pthread_gpool_t type, which is the object type of the handle $pthread_gpool, and is used by pthread.cvl.
      See Also:

    • PTHREAD_POOL

      public static final String PTHREAD_POOL
      The name of _pthread_poo_t type, which is the object type of the handle $pthread_pool, and is used by pthread.cvl.
      See Also:

    • BARRIER_TYPE

      public static final String BARRIER_TYPE
      The name of __barrier__ type, which is the object type of the handle $barrier.
      See Also:

    • BUNDLE_TYPE

      public static final String BUNDLE_TYPE
      the name of $bundle type
      See Also:

    • DYNAMIC_TYPE

      public static final String DYNAMIC_TYPE
      the name of $dynamic type
      See Also:

    • HEAP_TYPE

      public static final String HEAP_TYPE
      the name of the heap type
      See Also:

    • MESSAGE_TYPE

      public static final String MESSAGE_TYPE
      the name of message type
      See Also:

    • PROC_TYPE

      public static final String PROC_TYPE
      the name of process reference type
      See Also:

    • SCOPE_TYPE

      public static final String SCOPE_TYPE
      See Also:

    • QUEUE_TYPE

      public static final String QUEUE_TYPE
      the name of queue type
      See Also:

    • COMM_TYPE

      public static final String COMM_TYPE
      The name of $comm type, which is the object type of the handle $comm.
      See Also:

    • GBARRIER_TYPE

      public static final String GBARRIER_TYPE
      The name of __gbarrier__ type, which is the object type of the handle $gbarrier.
      See Also:

    • GCOMM_TYPE

      public static final String GCOMM_TYPE
      The name of __gcomm__ type, which is the object type of the handle $gcomm.
      See Also:

    • INT_ITER_TYPE

      public static final String INT_ITER_TYPE
      The name of __int_iter__ type, which is the object type of the handle $int_iter.
      See Also:

    • REAL_FILE_TYPE

      public static final String REAL_FILE_TYPE
      The file type $file.
      See Also:

    • FILE_STREAM_TYPE

      public static final String FILE_STREAM_TYPE
      The file reference type FILE.
      See Also:

    • TM_TYPE

      public static final String TM_TYPE
      The tm type, used by time.h.
      See Also:

    • FLOAT_COMPLEX_TYPE

      public static final String FLOAT_COMPLEX_TYPE
      The CIVL-C struct type corresponding to C's float _Complex.
      See Also:

    • DOUBLE_COMPLEX_TYPE

      public static final String DOUBLE_COMPLEX_TYPE
      The CIVL-C struct type corresponding to C's double _Complex.
      See Also:

    • LDOUBLE_COMPLEX_TYPE

      public static final String LDOUBLE_COMPLEX_TYPE
      The CIVL-C struct type corresponding to C's long double _Complex.
      See Also:

    • TIME_LIB

      public static final String TIME_LIB
      The name of the time.h library.
      See Also:

    • NEXT_TIME_COUNT

      public static final String NEXT_TIME_COUNT
      the function to get the unique counter of time
      See Also:

    • DYNAMIC_TYPE_NAME

      public static final String DYNAMIC_TYPE_NAME
      name of the symbolic type for mapping user-defined types to integers
      See Also:

    • ANONYMOUS_VARIABLE_PREFIX

      public static final String ANONYMOUS_VARIABLE_PREFIX
      prefix for anonymous variables
      See Also:

    • COMM_WORLD

      public static final String COMM_WORLD
      The name of the identifier of the MPI_Comm variable in the final CIVL program.
      See Also:

    • GCOMM_WORLD

      public static final String GCOMM_WORLD
      The name of the identifier of the CMPI_Gcomm variable in the final CIVL program.
      See Also:

    • GCOMMS

      public static final String GCOMMS
      The name of the identifier of the CMPI_Gcomm sequence variable in the final CIVL-MPI program
      See Also:

    • MPI_SYS_STATUS

      public static final String MPI_SYS_STATUS
      The name of the variable representing the status of an MPI process, which is modified by MPI_Init() and MPI_Finalized().
      See Also:

    • NPROCS

      public static final String NPROCS
      The name of the input variable denoting the number of MPI processes in the final CIVL-C program.
      See Also:

    • NPROCS_UPPER_BOUND

      public static final String NPROCS_UPPER_BOUND
      The name of the input variable denoting the upper bound of the number of MPI processes in the final CIVL-C program.
      See Also:

    • NPROCS_LOWER_BOUND

      public static final String NPROCS_LOWER_BOUND
      The name of the input variable denoting the lower bound of the number of MPI processes in the final CIVL-C program.
      See Also:

    • ContractResultName

      public static final String ContractResultName
      The "\result" constant used in ACSL contracts which stands for the returned value.
      See Also:

    • ContractMPICommRankName

      public static final String ContractMPICommRankName
      The extended "\mpi_comm_rank" constant used in CIVL-ACSL contracts which stands for the rank in a specific communicator of an MPI process.
      See Also:

    • ContractMPICommSizeName

      public static final String ContractMPICommSizeName
      The extended "\mpi_comm_size" constant used in CIVL-ACSL contracts which stands for the number of MPI processes in a specific communicator.
      See Also:

  • Constructor Details

    • ModelConfiguration

      public ModelConfiguration()

  • Method Details

    • addReservedName

      public static void addReservedName(String name)
      add new name to the reserved name set
      Parameters:
      name - name to be added to the reserved name set

    • addSizeofSymbol

      public static void addSizeofSymbol(dev.civl.sarl.IF.expr.SymbolicConstant symbol)

    • getAbstractFunctionName

      public static dev.civl.sarl.IF.object.StringObject getAbstractFunctionName(dev.civl.sarl.IF.SymbolicUniverse universe, String identifier)

      Returns a StringObject which is the name of the value an abstract function. The value of an abstract function is a function type symbolic constant.

      The returned name follows CIVL's naming convention for abstract function values and is uniquely associated with the given identifier.

      Note that for function type symbolic constants that are not values of abstract functions, their names should be what getFunctionConstantName(SymbolicUniverse, String) decides to be.

      Parameters:
      universe - a reference to the SymbolicUniverse
      identifier - an identifier that belongs to an abstract function
      Returns:
      a StringObject which is the name of an abstract function

    • getFunctionConstantName

      public static dev.civl.sarl.IF.object.StringObject getFunctionConstantName(dev.civl.sarl.IF.SymbolicUniverse universe, String identifier)

      Returns a StringObject which is the name of a function type symbolic constant. This symbolic constant is not the value of an abstract function.

      The returned name follows CIVL's naming convention for function type symbolic constants that are not values of abstract functions and is uniquely associated with the given identifier.

      Parameters:
      universe - a reference to the SymbolicUniverse
      identifier - an identifier that belongs to a symbolic constant
      Returns:
      a StringObject which is the name of a symbolic constant

    • getInvalidName

      public static dev.civl.sarl.IF.object.StringObject getInvalidName(dev.civl.sarl.IF.SymbolicUniverse universe)
      Parameters:
      universe - a reference to the SymbolicUniverse
      Returns:
      the StringObject which is the name of the symbolic constant representing invalid heap object values.

    • getSizeofPrimitiveTypeName

      public static dev.civl.sarl.IF.object.StringObject getSizeofPrimitiveTypeName(dev.civl.sarl.IF.SymbolicUniverse universe, CIVLPrimitiveType.PrimitiveTypeKind kind)

      Returns the name of the unique symbolic constant which represents the value of the size of a specific CIVLPrimitiveType.

      Parameters:
      universe - a reference to the SymbolicUniverse
      kind - the kind of the given CIVLPrimitiveType
      Returns:
      the name of the unique symbolic constant which represents the value of the size of a specific CIVLPrimitiveType

    • getSizeofNonPrimitiveTypeFunctionName

      public static dev.civl.sarl.IF.object.StringObject getSizeofNonPrimitiveTypeFunctionName(dev.civl.sarl.IF.SymbolicUniverse universe)

      Returns the name of the unique function type symbolic constant which maps non-primitive types to their size values.

      Parameters:
      universe - a reference to the SymbolicUniverse
      Returns:
      the name of the unique function type symbolic constant which maps non-primitive types to their size values.