Module dev.civl.mc
Package dev.civl.mc.semantics.IF

Interface Executor

public interface Executor

  • Method Summary

    Modifier and Type
    Method
    Description
    State
    assign(CIVLSource source, State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression pointer, dev.civl.sarl.IF.expr.SymbolicExpression value)
    Assigns a value to the referenced cell in the state.
    State
    assign(State state, int pid, String process, LHSExpression lhs, dev.civl.sarl.IF.expr.SymbolicExpression value, boolean isInitializer)
    Assigns a value to the memory location specified by the given left-hand-side expression.
    State
    assign2(CIVLSource source, State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression pointerToVarOrHeapObject, dev.civl.sarl.IF.expr.SymbolicExpression newValueOfVarOrHeapObject, dev.civl.sarl.IF.expr.SymbolicExpression valueSetTemplate)
    Given a "pointer" to a variable (Variable) or a memory heap object (see SymbolicUtility.isPointerToHeap(SymbolicExpression)), a symbolic expression "newValue" that represents the new value of the variable or the memory heap object and a symbolic expression "valueSetTemplate" of CoreUniverse.valueSetTemplateType(), which refers to a set of regions in the variable or the heap object, this method carves the part that is referred by the "valueSetTemplate" out of the "newValue" and assigns it to the counterpart in the variable or the heap object.
    CIVLErrorLogger
    errorLogger()
    Returns the error logger used by this executor.
    Evaluator
    evaluator()
     
    State
    execute(State state, int pid, Transition transition)
    Returns the state that results from executing the statement, or null if path condition becomes unsatisfiable.
    Evaluation
    execute_printf(CIVLSource source, State state, int pid, String process, Expression[] arguments, dev.civl.sarl.IF.expr.SymbolicExpression[] argumentValues, boolean forcePrint)
     
    long
    getNumSteps()
    Returns the number of "steps" executed since this Executor was created.
    Evaluation
    malloc(CIVLSource source, State state, int pid, String process, Expression scopeExpression, dev.civl.sarl.IF.expr.SymbolicExpression scopeValue, CIVLType objectType, dev.civl.sarl.IF.expr.SymbolicExpression objectValue)
    Adds a new object to the heap of a certain scope; returns the pointer of the object in the heap.
    void
    printf(PrintStream printStream, CIVLSource source, String process, List<Format> formats, List<StringBuffer> arguments)
    If there are insufficient arguments for the format, the behavior is undefined.
    void
    setConfiguration(CIVLConfiguration config)
     
    List<Format>
    splitFormat(CIVLSource source, StringBuffer formatBuffer)
     
    StateFactory
    stateFactory()
     

  • Method Details

    • assign

      State assign(CIVLSource source, State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression pointer, dev.civl.sarl.IF.expr.SymbolicExpression value) throws UnsatisfiablePathConditionException
      Assigns a value to the referenced cell in the state. Returns a new state which is equivalent to the old state except that the memory specified by the given pointer value is assigned the given value.
      Parameters:
      source - the source code information for error report
      state - a CIVL model state
      pid - the PID of the calling process
      pointer - a pointer value
      value - a value to be assigned to the referenced memory location
      Returns:
      the new state
      Throws:
      UnsatisfiablePathConditionException

    • assign2

      State assign2(CIVLSource source, State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression pointerToVarOrHeapObject, dev.civl.sarl.IF.expr.SymbolicExpression newValueOfVarOrHeapObject, dev.civl.sarl.IF.expr.SymbolicExpression valueSetTemplate) throws UnsatisfiablePathConditionException

      Given a "pointer" to a variable (Variable) or a memory heap object (see SymbolicUtility.isPointerToHeap(SymbolicExpression)), a symbolic expression "newValue" that represents the new value of the variable or the memory heap object and a symbolic expression "valueSetTemplate" of CoreUniverse.valueSetTemplateType(), which refers to a set of regions in the variable or the heap object, this method carves the part that is referred by the "valueSetTemplate" out of the "newValue" and assigns it to the counterpart in the variable or the heap object.

      Parameters:
      source - the CIVLSource that is related to this assignment
      state - the state where the assignment happens
      pid - the PID of the running process
      pointerToVarOrHeapObject - a pointer to a variable or a memory heap object
      newValueOfVarOrHeapObject - a symbolic expression that represents the new value of the referred variable or the memory heap object; the type of this symbolic expression will be equal to the dynamic type of the variable of the heap object
      valueSetTemplate - a symbolic expression of type CoreUniverse.valueSetTemplateType() that represents a specific (sub-)region that will be assigned.
      Returns:
      the state after assignment
      Throws:
      UnsatisfiablePathConditionException

    • assign

      State assign(State state, int pid, String process, LHSExpression lhs, dev.civl.sarl.IF.expr.SymbolicExpression value, boolean isInitializer) throws UnsatisfiablePathConditionException
      Assigns a value to the memory location specified by the given left-hand-side expression.
      Parameters:
      state - a CIVL model state
      pid - the PID of the process executing the assignment
      process - the process information (process name + PID) for error report
      lhs - a left-hand-side expression
      value - the value being assigned to the left-hand-side
      isInitializer - boolean value indicating if the given left-hand side expression will be INITIALIZED by the given value
      Returns:
      the new state
      Throws:
      UnsatisfiablePathConditionException

    • stateFactory

      StateFactory stateFactory()
      Returns:
      The state factory associated with this executor.

    • evaluator

      Evaluator evaluator()
      Returns:
      The evaluator used by this executor.

    • getNumSteps

      long getNumSteps()
      Returns the number of "steps" executed since this Executor was created.
      Returns:
      the number of steps executed

    • malloc

      Evaluation malloc(CIVLSource source, State state, int pid, String process, Expression scopeExpression, dev.civl.sarl.IF.expr.SymbolicExpression scopeValue, CIVLType objectType, dev.civl.sarl.IF.expr.SymbolicExpression objectValue) throws UnsatisfiablePathConditionException
      Adds a new object to the heap of a certain scope; returns the pointer of the object in the heap.
      Parameters:
      source - The source code element to be used to report errors.
      state - The current state.
      pid - The ID of the process where this computation happens.
      scopeExpression - The static expression of the scope value.
      scopeValue - The symbolic expression of the scope.
      objectType - The CIVL type of the object to be added, needed to decide the field index in the heap.
      objectValue - The object to be added to the heap.
      Returns:
      The new state after allocating the specified object in the heap and the pointer of the object in the heap.
      Throws:
      UnsatisfiablePathConditionException

    • execute

      State execute(State state, int pid, Transition transition) throws UnsatisfiablePathConditionException
      Returns the state that results from executing the statement, or null if path condition becomes unsatisfiable.
      Parameters:
      state - the state that the transition emanates from
      pid - the PID of the process that the transition
      transition - a deterministic transition to be executed
      Returns:
      The state after the transition is executed.
      Throws:
      UnsatisfiablePathConditionException - when an error is encountered during the execution

    • errorLogger

      CIVLErrorLogger errorLogger()
      Returns the error logger used by this executor.
      Returns:
      The error logger used by this executor.

    • execute_printf

      Evaluation execute_printf(CIVLSource source, State state, int pid, String process, Expression[] arguments, dev.civl.sarl.IF.expr.SymbolicExpression[] argumentValues, boolean forcePrint) throws UnsatisfiablePathConditionException
      Throws:
      UnsatisfiablePathConditionException

    • splitFormat

      List<Format> splitFormat(CIVLSource source, StringBuffer formatBuffer)

    • printf

      void printf(PrintStream printStream, CIVLSource source, String process, List<Format> formats, List<StringBuffer> arguments)
      If there are insufficient arguments for the format, the behavior is undefined. If the format is exhausted while arguments remain, the excess arguments are evaluated (as always) but are otherwise ignored.
      Parameters:
      printStream -
      source -
      formats -
      arguments -

    • setConfiguration

      void setConfiguration(CIVLConfiguration config)