Module dev.civl.mc
Package dev.civl.mc.state.IF

Interface StateFactory

public interface StateFactory
The state factory is used to create all state objects.

  • Method Summary

    Modifier and Type
    Method
    Description
    State
    addProcess(State state, CIVLFunction function, int functionParentDyscope, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments, int callerPid, boolean isSelfDestructable)
    Adds a new process.
    State
    addProcess(State state, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments, int callerPid, boolean isSelfDestructable)
    Adds a new process.
    State
    addReadWriteRecords(State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression memValue, boolean isRead)
    Records a collection of pointers to changed memory locations.
    State
    addToPathcondition(State state, int pid, dev.civl.sarl.IF.expr.BooleanExpression clause)
    Add a boolean value clause to the path condition of the given state.
    State
    canonic(State state, boolean collectProcesses, boolean collectScopes, boolean collectHeaps, boolean collectSymbolicConstants, boolean simplify, Set<CIVLHeapException.HeapErrorKind> toBeIgnored)
    Return the "canonical" version of the given state.
    State
    collectHeaps(State state, Set<CIVLHeapException.HeapErrorKind> toBeIgnored)
    Performs a garbage collection and canonicalization of heaps.
    State
    collectProcesses(State state)
    Performs a garbage collection and canonicalization of the process states.
    State
    collectScopes(State state, Set<CIVLHeapException.HeapErrorKind> toBeIgnored)
    Performs a garbage collection and canonicalization of dynamic scopes.
    State
    deallocate(State state, dev.civl.sarl.IF.expr.SymbolicExpression heapObjectPointer, dev.civl.sarl.IF.expr.SymbolicExpression scopeOfPointer, int mallocId, int index)
    Deallocates a heap object from the heap of a given dyscope.
    State
    emptyState(int nprocs)
    Creates an empty state which contains no dyscopes but an array of process states with length 'nprocs'.
    State
    enterAtomic(State state, int pid)
    Process pid enters a new atomic section.
    State
    getAtomicLock(State state, int pid)
    Declares that the process with the given PID now owns the atomic lock.
    int
    getDyscopeId(dev.civl.sarl.IF.expr.SymbolicExpression scopeValue)
    Converts a value of scope type to a dynamic scope ID.
    Pair<State,dev.civl.sarl.IF.expr.SymbolicConstant>
    getFreshSymbol(State state, int index, dev.civl.sarl.IF.type.SymbolicType type)
    Creates a fresh symbolic constant of the given type at the given state.
    long
    getNumStateInstances()
    Returns the number of objects of type State that have been instantiated since this JVM started.
    State
    initialState(Model model)
    Returns the canonic, initial state for a CIVL Model.
    Map<Variable,dev.civl.sarl.IF.expr.SymbolicExpression>
    inputVariableValueMap(State state)
    Returns the map of input variable and their value at the given state; empty map if there are no input variables.
    boolean
    isDescendantOf(State state, int ancestor, int descendant)
    Checks if one dyscope is strictly the descendant of the other (not equal to).
    boolean
    isScopeIdDefined(int sid)
     
    State
    leaveAtomic(State state, int pid)
    Process pid leaves an atomic section.
    Precondition: in the given state, the process pid holds the atomic lock and its atomic count is greater than zero.
    The atomic count is decremented by 1 after this method;
    if the resultant atomic count is 0, then the atomic lock is released as well.
    boolean
    lockedByAtomic(State state)
    Checks if any process at the state is holding the atomic lock, i.e, the process is executing some atomic blocks.
    int
    lowestCommonAncestor(State state, int one, int another)
    Computes the lowest common ancestor of two given dyscopes.
    Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression>
    malloc(State state, int pid, int dyscopeID, int mallocID, dev.civl.sarl.IF.type.SymbolicType elementType, dev.civl.sarl.IF.expr.NumericExpression elementCount)
    Allocates an object for the given malloc ID in the heap of the given dyscope.
    Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression>
    malloc(State state, int dyscopeID, int mallocID, dev.civl.sarl.IF.expr.SymbolicExpression heapObject)
    Allocates an object, of the given value, for the given malloc ID in the heap of the given dyscope.
    MemoryUnitFactory
    memUnitFactory()
    returns the memory unit factory associated with this state factory, which contains utility functions for
    dev.civl.sarl.IF.expr.SymbolicExpression
    nullScopeValue()
     
    DynamicMemoryLocationSet
    peekReadWriteSet(State state, int pid, boolean isRead)
     
    State
    popAssumption(State state, int pid)
     
    State
    popCallStack(State state, int pid)
    Pops an entry off the call stack for a process.
    State
    popReadWriteSet(State state, int pid, boolean isRead)
     
    int
    processInAtomic(State state)
    Returns the PID of the process that holds the atomic lock at a certain state
    dev.civl.sarl.IF.expr.SymbolicExpression
    processValue(int pid)
     
    State
    pushAssumption(State state, int pid, dev.civl.sarl.IF.expr.BooleanExpression assumption)
     
    State
    pushCallStack(State state, int pid, CIVLFunction function, int functionParentDyscope, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)
    Pushes a new entry onto the call stack for a process.
    State
    pushCallStack(State state, int pid, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)
    Pushes a new entry onto the call stack for a process.
    State
    pushContract(State state, int pid, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)
    Pushes a new frame onto the call stack where static scope of the frame is the contract scope of a function.
    State
    pushEmptyReadWrite(State state, int pid, boolean isRead)
     
    State
    releaseAtomicLock(State state)
    Releases the atomic lock, by updating the atomic lock variable with the undefined process value.
    State
    removeProcess(State state, int pid)
    Removes a process from the state.
    dev.civl.sarl.IF.expr.SymbolicExpression
    scopeValue(int sid)
    Converts an integer dynamic scope id into a symbolic expression
    void
    setConfiguration(CIVLConfiguration config)
     
    State
    setLocation(State state, int pid, Location location)
    Sets the location of a process.
    State
    setLocation(State state, int pid, Location location, boolean accessChanged)
    Sets the location of a process.
    State
    setProcessState(State state, ProcessState processState)
    Updates the state by replacing the process state with the given one where the PID of the old process state is the same as the given process state.
    void
    setSymbolicUtility(SymbolicUtility symbolicUtility)
     
    State
    setVariable(State state, int vid, int scopeId, dev.civl.sarl.IF.expr.SymbolicExpression value)
    Updates the value assigned to a variable in the state.
    State
    setVariable(State state, Variable variable, int pid, dev.civl.sarl.IF.expr.SymbolicExpression value)
    Updates the value assigned to a variable in the state.
    State
    simplify(State state)
    Simplifies all variable values in the state, using the path condition as the simplification context.
    State
    simplify(State state, int pid)
     
    State
    simplify(State state, int pid, Set<dev.civl.sarl.IF.expr.SymbolicConstant> aggressiveSet)
     
    State
    simplify(State state, Set<dev.civl.sarl.IF.expr.SymbolicConstant> aggressiveSet)
     
    dev.civl.sarl.IF.SymbolicUniverse
    symbolicUniverse()
    Returns the symbolic universe used by this factory to manipulate symbolic expressions.
    State
    terminateProcess(State state, int pid)
    Sets the process state for the designated process to be the process state with the empty stack.
    dev.civl.sarl.IF.expr.SymbolicExpression
    undefinedScopeValue()
     
    Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression>
    valueSetHavoc(State state, dev.civl.sarl.IF.expr.SymbolicExpression value, dev.civl.sarl.IF.expr.SymbolicExpression valueSetTemplate)
    Performs a value-set havoc operation that replaces parts of a value specified by a value set template with fresh symbolic constants using the havoc prefix (Y).

  • Method Details

    • symbolicUniverse

      dev.civl.sarl.IF.SymbolicUniverse symbolicUniverse()
      Returns the symbolic universe used by this factory to manipulate symbolic expressions.
      Returns:
      the symbolic universe

    • canonic

      State canonic(State state, boolean collectProcesses, boolean collectScopes, boolean collectHeaps, boolean collectSymbolicConstants, boolean simplify, Set<CIVLHeapException.HeapErrorKind> toBeIgnored) throws CIVLHeapException
      Return the "canonical" version of the given state. The state returned will satisfy all of the following:
      • it will be observationally equivalent to the given state, i.e., there is no way a CIVL-C program can distinguish between the two states
      • there will be no gaps in the dynamic scope IDs and no null dynamic scopes
      • there will be no gaps in the PIDs and no null process states
      • every dynamic scope will be reachable (starting from the frame of the call stack of one of the processes and following parent edges in the dyscope tree)
      • the state returned will be the unique representative of its equivalence class, i.e., if this method is invoked with two equivalent states, it will return the same object
      Note that the state returned may in fact be the same as the one given. Note that this does everything that methods
      invalid reference 
      #collectScopes(State)
      and collectProcesses(dev.civl.mc.state.IF.State) do. So there is no need to call those methods if you are already calling this method. This method may go further in simplifying the state. This is up to the particular implementation.
      Parameters:
      state - any non-null CIVL state
      collectProcesses - shall processes be collected?
      collectScopes - shall scopes be collected?
      collectHeaps - shall heaps be collected?
      Returns:
      the canonical version of the given state
      Throws:
      CIVLHeapException

    • initialState

      State initialState(Model model) throws CIVLHeapException
      Returns the canonic, initial state for a CIVL Model.
      Returns:
      the initial state
      Throws:
      CIVLHeapException

    • setVariable

      State setVariable(State state, Variable variable, int pid, dev.civl.sarl.IF.expr.SymbolicExpression value)
      Updates the value assigned to a variable in the state. Specifically, returns a state which is equivalent to the given one, except that the value assigned to the specified variable is replaced by the given value.
      Parameters:
      state - The old state
      variable - The variable to update
      pid - The PID of the process containing the variable
      value - The new value to be assigned to the variable
      Returns:
      A new state that is the old state modified by updating the value of the variable

    • setVariable

      State setVariable(State state, int vid, int scopeId, dev.civl.sarl.IF.expr.SymbolicExpression value)

      Updates the value assigned to a variable in the state. Specifically, returns a state which is equivalent to the given one, except that the value assigned to the specified variable is replaced by the given value.

      In this version of the method, the variable is specified by its dynamic scope ID and variable ID.

      Parameters:
      state - The old state
      vid - variable ID number
      value - The new value to assign to the variable
      scopeID - The ID of the dynamic scope containing the variable. This version of the method is useful when setting the target of a pointer. For a variable in the current lexical scope, use the version of the method without this argument
      Returns:
      A new state that is the old state modified by updating the value of the variable
      See Also:

    • addProcess

      State addProcess(State state, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments, int callerPid, boolean isSelfDestructable)

      Adds a new process. The new process is created and one entry is pushed onto its call stack. That entry will have a dynamic scope whose parent is determined by the calling process (the process that is executing the spawn command to create this new process) and the given function. The parent dynamic scope is computed by starting with the current dynamic scope of the caller, and working up the parent chain, stopping at the first dynamic scope whose static scope matches the containing scope of the function. If no such dynamic scope is found in the chain, an IllegalArgumentException is thrown. Hence the calling process must have a non-empty call stack.

      The PID of the new process will be State.numProcs(), where state is the pre-state (the given state), not the new state.

      Parameters:
      state - The old state.
      function - The function in which the new process starts.
      arguments - The arguments to this function call.
      callerPid - the PID of the process that is creating the new process
      isSelfDestructable - If the process is self-destructable. See ProcessState.isSelfDestructable()
      Returns:
      A new state that is the old state modified by adding a process whose location is the start location of the function and with a new dynamic scope corresponding to the outermost lexical scope of the function.

    • addToPathcondition

      State addToPathcondition(State state, int pid, dev.civl.sarl.IF.expr.BooleanExpression clause)

      Add a boolean value clause to the path condition of the given state. The new path condition is the conjunction of the old path condition of the given state and the given clause. Returns a new state which is same as the given one but owns the new path condition.

      Based on the semantics of symbolic execution, this is the one of the only two ways to update a path condition (1. conjunction with a new clause; 2. simplification).

      Parameters:
      state - The state before the path condition being updated.
      pid - The PID of the calling process.
      clause - The boolean value symbolic expression which will be added to the path condition.
      Returns:
      A new state which is same as the given one but owns the new path condition.

    • addProcess

      State addProcess(State state, CIVLFunction function, int functionParentDyscope, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments, int callerPid, boolean isSelfDestructable)

      Adds a new process. The new process is created and one entry is pushed onto its call stack. That entry will have a dynamic scope whose parent is determined by the calling process (the process that is executing the spawn command to create this new process) and the given function. The parent dynamic scope is computed by starting with the current dynamic scope of the caller, and working up the parent chain, stopping at the first dynamic scope whose static scope matches the containing scope of the function. If no such dynamic scope is found in the chain, an IllegalArgumentException is thrown. Hence the calling process must have a non-empty call stack.

      The PID of the new process will be State.numProcs(), where state is the pre-state (the given state), not the new state.

      Parameters:
      state - The old state.
      function - The function in which the new process starts.
      functionParentDyscope - The dyscope ID of the parent of the new function
      arguments - The arguments to this function call.
      callerPid - the PID of the process that is creating the new process
      isSelfDestructable - If the process is self-destructable. See ProcessState.isSelfDestructable()
      Returns:
      A new state that is the old state modified by adding a process whose location is the start location of the function and with a new dynamic scope corresponding to the outermost lexical scope of the function.

    • terminateProcess

      State terminateProcess(State state, int pid)
      Sets the process state for the designated process to be the process state with the empty stack.
      Parameters:
      state - the old state
      pid - the PID of the process to terminate
      Returns:
      state that is identical to old except that the process state for process PID has been set to the process state with the empty stack

    • removeProcess

      State removeProcess(State state, int pid)
      Removes a process from the state. The process state associated to that process is set to null. No other part of the state is affected. To really get rid of the process state you need to call collectProcesses(dev.civl.mc.state.IF.State).
      Parameters:
      state - The old state
      pid - The PID
      Returns:
      A new state that is the same as the old state with the process state set to null

    • setLocation

      State setLocation(State state, int pid, Location location)
      Sets the location of a process. This changes the top stack frame for the process so that it points to the new location. The given process must have a non-empty stack (although the location component of that frame is not used, so it is OK if it is null). There is no change of the access of variables from the current location to the target location. This may involve adding and removing scopes, if the scope of the new location differs from the original scope.
      Parameters:
      state - The old state.
      pid - The PID of the process making the move.
      location - The target location.
      Returns:
      A new state that is the same as the old state with the given process at a new location, and scopes added and removed as necessary

    • setLocation

      State setLocation(State state, int pid, Location location, boolean accessChanged)
      Sets the location of a process. This changes the top stack frame for the process so that it points to the new location. The given process must have a non-empty stack (although the location component of that frame is not used, so it is OK if it is null). This may involve adding and removing scopes, if the scope of the new location differs from the original scope.
      Parameters:
      state - The old state.
      pid - The PID of the process making the move.
      location - The target location.
      accessChanged - True iff there is change of variable accessing (write or read-only) from the current location to the target location
      Returns:
      A new state that is the same as the old state with the given process at a new location, and scopes added and removed as necessary

    • pushCallStack

      State pushCallStack(State state, int pid, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)
      Pushes a new entry onto the call stack for a process. Used when a process calls a function. The process should already exist and have a non-empty call stack.
      Parameters:
      state - The old state
      pid - The PID of the process making the call
      function - The function being called
      arguments - The (actual) arguments to the function being called
      Returns:
      A new state that is the same as the old state with the given process having a new entry on its call stack.

    • pushCallStack

      State pushCallStack(State state, int pid, CIVLFunction function, int functionParentDyscope, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)
      Pushes a new entry onto the call stack for a process. Used when a process calls a function. The process should already exist and have a non-empty call stack.
      Parameters:
      state - The old state
      pid - The PID of the process making the call
      function - The function being called
      functionParentDyscope - The dyscope ID of the parent of the new function
      arguments - The (actual) arguments to the function being called
      Returns:
      A new state that is the same as the old state with the given process having a new entry on its call stack.

    • pushContract

      State pushContract(State state, int pid, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments)
      Pushes a new frame onto the call stack where static scope of the frame is the contract scope of a function. This can be used to evaluate expressions in contract clauses.

      Precondition: the function must have a contract.

      Parameters:
      state - The old state
      pid - The PID of the process making the call
      function - The function being called
      arguments - The (actual) arguments to the function being called
      Returns:
      A new state that is the same as the old state with the given process having a new entry on its call stack corresponding to the contract of the function

    • popCallStack

      State popCallStack(State state, int pid)
      Pops an entry off the call stack for a process. Does not modify or remove and dynamic scopes (even if they become unreachable). Does not nullify or remove the process state (even if the call stack becomes empty).
      Parameters:
      state - The old state.
      pid - The PID of the process returning from a call.
      Returns:
      A new state that is the same as the old state but with the call stack for the given process popped.

    • simplify

      State simplify(State state)
      Simplifies all variable values in the state, using the path condition as the simplification context. A symbolic constant which is determined to have a concrete value (based on the path condition), may be entirely removed from the state by replacing every occurrence of that symbol with the concrete value.
      Parameters:
      state - Any State
      Returns:
      The simplified state

    • simplify

      State simplify(State state, int pid)

    • simplify

      State simplify(State state, Set<dev.civl.sarl.IF.expr.SymbolicConstant> aggressiveSet)

    • simplify

      State simplify(State state, int pid, Set<dev.civl.sarl.IF.expr.SymbolicConstant> aggressiveSet)

    • getNumStateInstances

      long getNumStateInstances()
      Returns the number of objects of type State that have been instantiated since this JVM started.
      Returns:
      the number of states instantiated

    • collectHeaps

      State collectHeaps(State state, Set<CIVLHeapException.HeapErrorKind> toBeIgnored) throws CIVLStateException
      Performs a garbage collection and canonicalization of heaps. Computes the set of reachable heap objects, and removes all unreachable heap objects. Renumbers heap objects in a canonic way. Updates all pointers in the state accordingly. This operation should be completely invisible to the user.
      Parameters:
      state - a state
      Returns:
      the state after canonicalizing heaps, which may be this state or a new one
      Throws:
      CIVLStateException

    • collectScopes

      State collectScopes(State state, Set<CIVLHeapException.HeapErrorKind> toBeIgnored) throws CIVLStateException
      Performs a garbage collection and canonicalization of dynamic scopes. Compute the set of reachable dynamic scopes, and removes any which are unreachable. Renumbers the dynamic scopes in a canonic way. Updates all scope references in the state. This operation should be completely invisible to the user.
      Parameters:
      state - a state
      Returns:
      the state after canonicalizing scopes, which may be this state or a new one
      Throws:
      CIVLStateException

    • collectProcesses

      State collectProcesses(State state)
      Performs a garbage collection and canonicalization of the process states. Removes any process state that is null. Renumbers the PIDs so that there are no gaps (and start from 0).
      Parameters:
      state - any non-null CIVL state
      Returns:
      the state with processes collected

    • lockedByAtomic

      boolean lockedByAtomic(State state)
      Checks if any process at the state is holding the atomic lock, i.e, the process is executing some atomic blocks.

      This information is maintained as a global variable of $proc type in the root scope in the CIVL model (always with index 0), and it gets automatically updated when process id's are renumbered.

      Parameters:
      state - The state to be checked
      Returns:
      True iff the value of the variable atomic lock is not undefined.

    • processInAtomic

      int processInAtomic(State state)
      Returns the PID of the process that holds the atomic lock at a certain state
      Parameters:
      state - The state to be checked
      Returns:
      -1 iff there is no process holding the atomic lock, otherwise return the process that holds the atomic lock

    • getAtomicLock

      State getAtomicLock(State state, int pid)
      Declares that the process with the given PID now owns the atomic lock. Precondition: no process is holding the atomic lock in the given state.
      Parameters:
      state - any non-null CIVL state
      pid - The PID of the process that is going to take the atomic lock
      Returns:
      a state equivalent to given one except that process PID now owns the atomic lock

    • enterAtomic

      State enterAtomic(State state, int pid)
      Process pid enters a new atomic section.
      Precondition: no other processes hold the atomic lock
      If the process already holds the atomic lock, then its atomic count is incremented;
      if the process doesn't hold the atomic lock, then the atomic lock is obtained and its atomic count is set to be 1.
      Parameters:
      state -
      pid -
      Returns:
      the new state after process pid enters a new atomic section

    • leaveAtomic

      State leaveAtomic(State state, int pid)
      Process pid leaves an atomic section.
      Precondition: in the given state, the process pid holds the atomic lock and its atomic count is greater than zero.
      The atomic count is decremented by 1 after this method;
      if the resultant atomic count is 0, then the atomic lock is released as well.
      Parameters:
      state -
      pid -
      Returns:
      the new state after process pid leaves an atomic section

    • releaseAtomicLock

      State releaseAtomicLock(State state)
      Releases the atomic lock, by updating the atomic lock variable with the undefined process value. If atomic lock of the given state is already released, this is a no op.
      Parameters:
      state - any non-null CIVL state
      Returns:
      a state equivalent to given one except that no state owns the atomic lock

    • setProcessState

      State setProcessState(State state, ProcessState processState)

      Updates the state by replacing the process state with the given one where the PID of the old process state is the same as the given process state.

      Precondition: the PID of the given process state should be in [0, numProcs-1].

      Parameters:
      state - A non-null CIVL state
      processState - The process state to assign to PID
      Returns:
      The new state after updating the process with the specified PID

    • isDescendantOf

      boolean isDescendantOf(State state, int ancestor, int descendant)
      Checks if one dyscope is strictly the descendant of the other (not equal to).
      Parameters:
      state - The current state.
      ancestor - The ID of the ancestor dyscope.
      descendant - The ID of the descendant dyscope.
      Returns:
      True iff ancestor dyscope is really an ancestor of the descendant dyscope and they must not be equal to each other.

    • lowestCommonAncestor

      int lowestCommonAncestor(State state, int one, int another)
      Computes the lowest common ancestor of two given dyscopes. The returned value is always a dyscope ID.
      Parameters:
      state - The current state.
      one - One dyscope.
      another - Another dynamic scope.
      Returns:
      The dyscope ID of the lowest common ancestor of the two given dyscopes.

    • malloc

      Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression> malloc(State state, int dyscopeID, int mallocID, dev.civl.sarl.IF.expr.SymbolicExpression heapObject)
      Allocates an object, of the given value, for the given malloc ID in the heap of the given dyscope. For handle objects that are allocated by system functions instead of malloc statement, they all have a corresponding fake malloc ID assigned by the model builder.
      Parameters:
      state - The pre-state.
      dyscopeID - The dyscope ID.
      mallocID - The ID the malloc statement.
      heapObject - The value of the new heap object.
      Returns:
      The new state after the new heap object

    • malloc

      Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression> malloc(State state, int pid, int dyscopeID, int mallocID, dev.civl.sarl.IF.type.SymbolicType elementType, dev.civl.sarl.IF.expr.NumericExpression elementCount)
      Allocates an object for the given malloc ID in the heap of the given dyscope. For handle objects that are allocated by system functions instead of malloc statement, they all have a corresponding fake malloc ID assigned by the model builder. Since no value of the heap object is provided, the method will create a symbolic constant representing the heap object.
      Parameters:
      state - The pre-state.
      pid - The PID of the process that triggers this execution.
      dyscopeID - The dyscope ID.
      mallocID - The ID the malloc statement.
      elementType - The symbolic type of the element to be contained in the new heap object.
      elementCount - The number of elements contained by the new heap object.
      Returns:
      The new state after the new heap object is added.

    • deallocate

      State deallocate(State state, dev.civl.sarl.IF.expr.SymbolicExpression heapObjectPointer, dev.civl.sarl.IF.expr.SymbolicExpression scopeOfPointer, int mallocId, int index)
      Deallocates a heap object from the heap of a given dyscope. It marks the heap object as INVALID instead of removing it, updates any pointer to that removed object to be an UNDEFINED pointer, which is defined by the symbolic utility. The removal of the heap object happens later when the heap gets collected during state canonicalization.
      Parameters:
      state - The pre-state.
      heapObjectPointer - The pointer which points to the heap object to be removed.
      scopeOfPointer - The scope that is referred by the heapObjectPointer
      mallocId - The malloc ID of the heap object to be removed, i.e., the index of the heap field in the heap.
      index - The index of the heap object in the heap field.
      Returns:
      A new state after the heap object is removed from the heap, and corresponding pointers updated.
      See Also:

    • memUnitFactory

      MemoryUnitFactory memUnitFactory()
      returns the memory unit factory associated with this state factory, which contains utility functions for
      Returns:
      the memory unit factory associated with this state factory.

    • inputVariableValueMap

      Map<Variable,dev.civl.sarl.IF.expr.SymbolicExpression> inputVariableValueMap(State state)
      Returns the map of input variable and their value at the given state; empty map if there are no input variables.
      Parameters:
      state - the given state
      Returns:
      the map of input variable and their value at the given state

    • getFreshSymbol

      Pair<State,dev.civl.sarl.IF.expr.SymbolicConstant> getFreshSymbol(State state, int index, dev.civl.sarl.IF.type.SymbolicType type)
      Creates a fresh symbolic constant of the given type at the given state. The name of the symbolic constant is formed by a sequence of alphabets (i.e., the prefix) followed by an integer (i.e., the unique id), like "X4", "Y5", "H10". The prefix is decided by the index and ModelConfiguration.SYMBOL_PREFIXES. This method has side effect on the state because it increases the count of the corresponding symbol. Precondition: the index is greater than or equal to zero and is less than the length of ModelConfiguration.SYMBOL_PREFIXES.
      Parameters:
      state - the given state
      index - the index of the prefix to be used in the name of the symbolic constant to be created
      type - the type of the symbolic constant to be created
      Returns:
      the new state and the new symbolic constant of the given type with a unique name and has the prefix corresponding to the given index

    • valueSetHavoc

      Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression> valueSetHavoc(State state, dev.civl.sarl.IF.expr.SymbolicExpression value, dev.civl.sarl.IF.expr.SymbolicExpression valueSetTemplate)
      Performs a value-set havoc operation that replaces parts of a value specified by a value set template with fresh symbolic constants using the havoc prefix (Y). The fresh constants are tracked in the state's collectible counts so they can be renumbered during state normalization.
      Parameters:
      state - the current state
      value - the value to havoc
      valueSetTemplate - the value set template specifying which parts to havoc
      Returns:
      a pair of the new state (with updated collectible count) and the havoced value

    • emptyState

      State emptyState(int nprocs)
      Creates an empty state which contains no dyscopes but an array of process states with length 'nprocs'. Each process state has an empty call stack.
      Parameters:
      nprocs - Number of process states in the created state.
      Returns:
      A new state which contains no dyscopes but an array of process states with length 'nprocs'. Each process state has an empty call stack. The path condtion is simply 'true'.

    • addReadWriteRecords

      State addReadWriteRecords(State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression memValue, boolean isRead)
      Records a collection of pointers to changed memory locations. The change was done by the given process.
      Parameters:
      state - The current state
      pid - The PID of the calling process who may change some memory locations.
      memValue - a symbolic expression of CIVLType.getDynamicType(SymbolicUniverse) which includes references to objects
      isRead - true iff the given memory locations are added to read set; false iff the given memory locations are added to write set.
      Returns:
      A state in which the given memory locations are recorded.

    • peekReadWriteSet

      DynamicMemoryLocationSet peekReadWriteSet(State state, int pid, boolean isRead)
      Parameters:
      state - The current state
      pid - The PID of the calling process whose write set stack will be peeked.
      isRead - true iff peek a read set; false iff peek a write set.
      Returns:
      the top frame in the write set stack associates to the given process or Java null if the stack is empty.

    • pushEmptyReadWrite

      State pushEmptyReadWrite(State state, int pid, boolean isRead)
      Parameters:
      state - The current state
      isRead - true iff push an empty read set; false iff push an empty write set.
      The - PID of the calling process whose write set stack will be pushed.
      Returns:
      A new state in which the process state of the given pid will be updated. The write set stack of the process state has one more empty stack.

    • popReadWriteSet

      State popReadWriteSet(State state, int pid, boolean isRead)
      Parameters:
      state - The current state
      isRead - true iff pop a read set; false iff pop a write set.
      The - PID of the calling process whose write set stack will be popped.
      Returns:
      A new state in which the process state of the given pid will be updated. The write set stack of the process state has been popped

    • pushAssumption

      State pushAssumption(State state, int pid, dev.civl.sarl.IF.expr.BooleanExpression assumption)
      Parameters:
      state - The current state
      The - PID of the calling process whose partial path condition stack will be pushed.
      Returns:
      A new state in which the process state of the given pid will be updated. The partial path condition stack of the process state has one more empty stack.

    • popAssumption

      State popAssumption(State state, int pid)
      Parameters:
      state - The current state
      The - PID of the calling process whose partial path condition stack will be popped.
      Returns:
      A new state in which the process state of the given pid will be updated. The partial path condition stack of the process state has been popped.

    • scopeValue

      dev.civl.sarl.IF.expr.SymbolicExpression scopeValue(int sid)
      Converts an integer dynamic scope id into a symbolic expression
      Parameters:
      sid - The scope id to be translated
      Returns:
      The symbolic expression representing the scope id

    • getDyscopeId

      int getDyscopeId(dev.civl.sarl.IF.expr.SymbolicExpression scopeValue)
      Converts a value of scope type to a dynamic scope ID.
      Parameters:
      scopeValue - a value of scope type
      Returns:
      The dynamic scope ID which is associated with the given scope type value.

    • undefinedScopeValue

      dev.civl.sarl.IF.expr.SymbolicExpression undefinedScopeValue()
      Returns:
      constant value of scope type which represents an undefined scope.

    • nullScopeValue

      dev.civl.sarl.IF.expr.SymbolicExpression nullScopeValue()
      Returns:
      constant value of scope type which represents an collected scope.

    • isScopeIdDefined

      boolean isScopeIdDefined(int sid)
      Parameters:
      sid - a dynamic scope ID
      Returns:
      true iff the given dynamic scope ID stands for an undefined scope

    • setConfiguration

      void setConfiguration(CIVLConfiguration config)

    • processValue

      dev.civl.sarl.IF.expr.SymbolicExpression processValue(int pid)

    • setSymbolicUtility

      void setSymbolicUtility(SymbolicUtility symbolicUtility)