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

Interface Evaluator

public interface Evaluator
This is the CIVL main evaluator. First, it is responsible for evaluating all expressions. Second, it also provides some utility methods to be used by library executor/evaluator/enabler, like the methods related to heap. Third, it implements helper methods for the partial order reduction in pointer reachability analysis. TODO: does it have state?

  • Method Details

    • dereference

      Evaluation dereference(CIVLSource source, State state, int pid, String process, dev.civl.sarl.IF.expr.SymbolicExpression pointer, boolean checkedOutput, boolean strict) throws UnsatisfiablePathConditionException
      Given a pointer value, dereferences it in the given state to yield the symbolic expression value stored at the referenced location.
      Parameters:
      source - Source code information for error report.
      state - The state where the operation happens.
      process - The process information (name, PID) for error report.
      pointer - A pointer value which refers to some sub-structure in the state, and is to dereferenced.
      checkedOutput - If this dereference operation is to read the variable (opposed to write).
      strict - this method will report "undefined value" only when the value of strict is true and the value pointed to by the pointer is null. Currently, this value is false only when this method is called by LibpointerExecutor.executeCopy.
      Returns:
      the value pointed to
      Throws:
      UnsatisfiablePathConditionException

    • errorLogger

      CIVLErrorLogger errorLogger()
      Returns the error logger object of this evaluator.
      Returns:
      The error logger object of this evaluator.

    • evaluate

      Evaluation evaluate(State state, int pid, Expression expression, boolean checkUndefinedValue) throws UnsatisfiablePathConditionException
      Evaluates the expression and returns the result, which is a symbolic expression value. If a potential error is encountered while evaluating the expression (e.g. possible division by 0 in x/y), the error is logged, a correcting side effect (e.g. y!=0) is added to the path condition, and execution continues. It is possible for the side effect to make the path condition unsatisfiable. When this happens, an UnsatisfiablePathConditionException is thrown.
      Parameters:
      state - the state in which the evaluation takes place
      pid - the PID of the process which is evaluating the expression
      expression - the (static) expression being evaluated
      Returns:
      the result of the evaluation
      Throws:
      UnsatisfiablePathConditionException - if a side effect that results from evaluating the expression causes the path condition to become unsatisfiable

    • evaluate

      Evaluation evaluate(State state, int pid, Expression expression) throws UnsatisfiablePathConditionException
      Throws:
      UnsatisfiablePathConditionException

    • evaluateFunctionIdentifier

      Triple<State,CIVLFunction,Integer> evaluateFunctionIdentifier(State state, int pid, Expression functionPointer, CIVLSource source) throws UnsatisfiablePathConditionException
      Evaluates a function pointer expression. TODO: add ID for functions in the model. TODO: get rid of this function by adding a helper function to extract a function from a function pointer value. No need to have special handling for function pointer: can treat it like ordinary pointers.
      Parameters:
      state - The state where the evaluation happens.
      pid - The PID of the process that triggers this evaluation.
      functionPointer - The function pointer expression to be evaluated.
      source - The source code information for error report
      Returns:
      The new state after the evaluation with possible side effect, the function that the function pointer points to, and the dyscope ID of the function that the given function pointer refers to.
      Throws:
      UnsatisfiablePathConditionException

    • evaluateSizeofType

      Evaluation evaluateSizeofType(CIVLSource source, State state, int pid, CIVLType type) throws UnsatisfiablePathConditionException
      Evaluate the size of a CIVL type. TODO is this necessarily public?
      Parameters:
      source - The source code element to be used for error report.
      state - The state where the evaluation happens.
      pid - The ID of the process that triggers the evaluation.
      type - The CIVL type whose size is to be evaluated.
      Returns:
      the result of the evaluation, including the symbolic expression of the size of the type and a state
      Throws:
      UnsatisfiablePathConditionException

    • getStringExpression

      Evaluation getStringExpression(State state, int pid, String process, CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression charPointer) throws UnsatisfiablePathConditionException
      Given a pointer to char, returns the symbolic expression of type array of char which is the string pointed to. The method will succeed if any of the following holds: (1) the pointer points to element 0 of an array of char. In that case, it is just assumed that the string is the whole array. (2) the pointer points to element i of an array of char, where i is a concrete positive integer and the array length is also concrete. In that case, the elements of the array are scanned starting from position i until the first null character is reached, or the end of the array is reached, and the string is constructed from those scanned characters (including the null character). In other situations, this method may fail, in which case it throws an exception.
      Parameters:
      state - the state in which this evaluation is taking place
      source - the source information used to report errors
      charPointer - a symbolic expression which is a pointer to a char
      Returns:
      the symbolic expression which is an array of type char representing the string pointed to
      Throws:
      UnsatisfiablePathConditionException - of something goes wrong evaluating the string
      CIVLUnimplementedFeatureException - if it is not possible to extract the string expression.

    • modelFactory

      ModelFactory modelFactory()
      The model factory should be the unique one used in the system.
      Returns:
      The model factory of the evaluator.

    • evaluatePointerAdd

      Evaluation evaluatePointerAdd(State state, int pid, BinaryExpression expression, dev.civl.sarl.IF.expr.SymbolicExpression pointer, dev.civl.sarl.IF.expr.SymbolicExpression offset) throws UnsatisfiablePathConditionException
      Evaluates pointer addition. Pointer addition involves the addition of a pointer expression and an integer. TODO: check if BinaryExpression expression is necessary.
      Note: The given pointer for this function won't be casted to the deepest array element reference which is the only difference from the other function
      invalid reference 
      #pointerAdd(State, String, SymbolicExpression, NumericExpresion, boolean, CIVLSource)
      .
      e.g. for int a[2][2], passing pointer "a[0] + 1" will turn out a new pointer "a[1]".
      Parameters:
      state - the pre-state
      pid - the PID of the process evaluating the pointer addition
      expression - the pointer addition expression
      pointer - the result of evaluating argument 0 of expression
      offset - the result of evaluating argument 1 of expression
      Returns:
      the result of evaluating the sum of the pointer and the integer
      Throws:
      UnsatisfiablePathConditionException

    • pointerSubtraction

      Evaluation pointerSubtraction(State state, int pid, String process, BinaryExpression expression, dev.civl.sarl.IF.expr.SymbolicExpression leftPtr, dev.civl.sarl.IF.expr.SymbolicExpression rightPtr) throws UnsatisfiablePathConditionException
      Evaluation pointer subtraction. Pointer subtraction operation, a binary operation, whose two operands are both pointers to qualified or unqualified versions of compatible complete object types. Returns the difference of the two operands. Both pointers must point to elements of the same array or one past the last element of the same array.
      Parameters:
      state - The current state
      pid - The PID of the process
      process - The information of the process
      expression - The expression of the pointer subtraction statement
      leftPtr - The pointer at the left side of the minus operator
      rightPtr - The pointer at the right side of the minus operator
      Returns:
      the difference of the subscripts of the two array elements
      Throws:
      UnsatisfiablePathConditionException

    • reference

      Evaluation reference(State state, int pid, LHSExpression operand) throws UnsatisfiablePathConditionException
      Creates a pointer value by evaluating a left-hand-side expression in the given state.
      Parameters:
      state - a CIVL model state
      pid - the process ID of the process in which this evaluation is taking place
      operand - the left hand side expression we are taking the address of
      Returns:
      the pointer value
      Throws:
      UnsatisfiablePathConditionException

    • stateFactory

      StateFactory stateFactory()
      The state factory should be the unique one used in the system.
      Returns:
      The state factory of the evaluator.

    • symbolicUtility

      SymbolicUtility symbolicUtility()
      Returns the symbolic utility object of this evaluator.
      Returns:
      The symbolic utility object of this evaluator.

    • symbolicAnalyzer

      SymbolicAnalyzer symbolicAnalyzer()
      Returns the symbolic analyzer object of this evaluator.
      Returns:
      The symbolic analyzer object of this evaluator.

    • universe

      dev.civl.sarl.IF.SymbolicUniverse universe()
      The symbolic universe should be the unique one used in the system.
      Returns:
      The symbolic universe of the evaluator.

    • getString

      Triple<State,StringBuffer,Boolean> getString(CIVLSource source, State state, int pid, String process, Expression charPointerExpr, dev.civl.sarl.IF.expr.SymbolicExpression charPointer) throws UnsatisfiablePathConditionException
      extracts a string based on a given character pointer or string literal.
      Parameters:
      source -
      state -
      process -
      charPointerExpr -
      charPointer -
      Returns:
      Throws:
      UnsatisfiablePathConditionException

    • arrayElementReferenceAdd

      Pair<Evaluation,dev.civl.sarl.IF.expr.NumericExpression[]> arrayElementReferenceAdd(State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression ptr, dev.civl.sarl.IF.expr.NumericExpression offset, CIVLSource source) throws UnsatisfiablePathConditionException
      Do a pointer addition operation on the given pointer with the given offset. The given pointer will be casted to the deepest array element reference before the operation (e.g. for int a[2][2];, if giving pointer invalid input: '&a', it will be casted to invalid input: '&a'[0][0]).
      Parameters:
      state - The current state
      pid - The PID of the calling process
      ptr - The pointer will be added by a offset
      offset - The numeric offset will be added to a pointer
      source - The CIVLSource of the statement.
      Returns:
      A pair of evaluation of the result of the operation and a Java-array of the array slice sizes information of the array pointed by the given pointer which may helps saving computing time for caller functions.
      Throws:
      UnsatisfiablePathConditionException

    • leafNodeReferencesOfType

      List<dev.civl.sarl.IF.expr.ReferenceExpression> leafNodeReferencesOfType(CIVLSource source, State state, int pid, CIVLType type) throws UnsatisfiablePathConditionException
      Throws:
      UnsatisfiablePathConditionException

    • evaluateCIVLArrayType

      Pair<State,dev.civl.sarl.IF.type.SymbolicArrayType> evaluateCIVLArrayType(State state, int pid, CIVLArrayType type) throws UnsatisfiablePathConditionException
      Evaluating the symbolic array type from a CIVLArrayType based on current state and specific process. This function supplements the built-in function CIVLType.getDynamicType(SymbolicUniverse) by providing the missing extent information.
      Parameters:
      state - The current state
      pid - The PID of the process
      type - The CIVLArrayType object
      Returns:
      Throws:
      UnsatisfiablePathConditionException

    • memoryUnitEvaluator

      MemoryUnitExpressionEvaluator memoryUnitEvaluator()

    • evaluateCastWorker

      Evaluation evaluateCastWorker(State state, int pid, String process, CIVLType castType, Expression arg) throws UnsatisfiablePathConditionException
      Throws:
      UnsatisfiablePathConditionException

    • memEvaluator

      dev.civl.mc.semantics.common.MemEvaluator memEvaluator()
      Returns:
      a reference to MemEvaluator

    • havoc

      Evaluation havoc(State state, dev.civl.sarl.IF.type.SymbolicType type)
      returns an arbitrary symbolic constant with the given type.
      Parameters:
      state -
      Returns:

    • getDynamicType

      TypeEvaluation getDynamicType(State state, int pid, CIVLType type, CIVLSource source, boolean isDefinition) throws UnsatisfiablePathConditionException
      Evaluates the dynamic type of a given CIVL type at a certain state. When the CIVL type has some state, e.g., an array type with a variable as the extent, the type needs to be evaluated.
      Parameters:
      state - The current state.
      pid - The ID of the process where the computation happens.
      type - The CIVL type to be evaluated for the dynamic type.
      source - The source code element for error report.
      isDefinition - The flag denoting if the type is a definition.
      Returns:
      The dynamic type of the given type.
      Throws:
      UnsatisfiablePathConditionException

    • initialValueOfType

      Evaluation initialValueOfType(State state, int pid, CIVLType type) throws UnsatisfiablePathConditionException
      Given a CIVLType t, returns the default initial value of an object of t as if the object has static storage.
      Parameters:
      state - the current state
      pid - the PID of the running process
      type - the CIVLType, of which variable's initial value will be returned
      Throws:
      UnsatisfiablePathConditionException

    • newArrayToolBox

      ArrayToolBox newArrayToolBox(dev.civl.sarl.IF.SymbolicUniverse universe)
      Return a new ArrayToolBox
      Parameters:
      universe - A reference to a SymbolicUniverse
      Returns:
      a new ArrayToolBox

    • setConfiguration

      void setConfiguration(CIVLConfiguration config)

    • newReadSetCollectEvaluator

      dev.civl.mc.semantics.common.ReadSetCollectEvaluator newReadSetCollectEvaluator()
      Returns:
      a new instance of a ReadSetCollectEvaluator, which is a sub-class of CommonEvaluator.