public interface SymbolicAnalyzer

This class provides methods dealing with symbolic expressions and states, which represent some common-used operations like obtaining a sub-array from a given array, etc.

Method Summary

Modifier and Type

Method

Description

boolean

areDynamicTypesCompatiableForAssign(dev.civl.sarl.IF.type.SymbolicType lhsType, dev.civl.sarl.IF.type.SymbolicType rhsType)

Check if the dynamic types of the left-hand side (lhs) and right-hand side (rhs) expression are compatible for assignment operation.

CIVLType

civlTypeOfObjByPointer(CIVLSource soruce, State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer)

Computes the CIVL type of the object referring to by the given pointer.

dev.civl.sarl.IF.type.SymbolicType

dynamicTypeOfObjByPointer(CIVLSource source, State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer)

Computes the SymbolicType of the object referring to by the given pointer.

Evaluator

evaluator()

Pair<State,String>

expressionEvaluation(State state, int pid, Expression expression, boolean resultOnly)

Compute a friendly string representation of an expression's evaluation.

CIVLType

getArrayBaseType(State state, CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression arrayPtr)

pre-condition: "arrayPtr" must point to an array "source" is the @{link CIVLSource} of the pointer expression post-condition: the returned CIVLType must not be an array type the returned object cannot be null Get the type of the non-array element of an array by given a pointer to an array

dev.civl.sarl.IF.expr.ReferenceExpression

getLeafNodeReference(State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer, CIVLSource source)

Spec: Returns a ReferenceExpression object which directly refer to the object which has the physical base type of the pointed array (or object) residing in memory.

dev.civl.sarl.IF.expr.SymbolicExpression

getSubArray(State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression array, dev.civl.sarl.IF.expr.NumericExpression startIndex, dev.civl.sarl.IF.expr.NumericExpression endIndex, CIVLSource source)

Given an array, a start index, and end index, returns the array which is the subsequence of the given array consisting of the elements in positions start index through end index minus one.

dev.civl.sarl.IF.SymbolicUniverse

getUniverse()

Gets the symbolic universe used by this symbolic analyzer.

StringBuffer

inputVariablesToStringBuffer(State state)

static boolean

isConcretePointer(dev.civl.sarl.IF.expr.SymbolicExpression pointer)

Pair<dev.civl.sarl.IF.expr.BooleanExpression,dev.civl.sarl.IF.ValidityResult.ResultType>

isDefinedPointer(State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer, CIVLSource civlSource)

Is this an defined pointer? A pointer is defined if one of the following holds: it can be dereferenced (derefable pointer), e.g., invalid input: '&a', invalid input: '&b'[0] where a is a scalar variable and b is an array of length 5. it is the NULL pointer. it points to the end of an array, e.g., invalid input: '&b'[5] where b is an array of length 5. For the latter two cases, the pointer is called underefable pointer.

Pair<dev.civl.sarl.IF.expr.BooleanExpression,dev.civl.sarl.IF.ValidityResult.ResultType>

isDerefablePointer(State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer)

Is this a derefable pointer? In other words, check if the pointer can be dereferenced safely.

StringBuffer

memoryUnitToString(State state, MemoryUnit mu)

Pretty representation of a memory unit.

StringBuffer

pathconditionToString(CIVLSource source, State state, String prefix, dev.civl.sarl.IF.expr.BooleanExpression pc)

Pretty representation of a path condition, which is broken into lines if it is in CNF.

dev.civl.sarl.IF.expr.SymbolicExpression

pointerArithmetics(CIVLSource source, State state, boolean isSubtract, dev.civl.sarl.IF.expr.SymbolicExpression pointer, dev.civl.sarl.IF.expr.SymbolicExpression offset)

StringBuffer

stateInformation(State state)

Computes the user-friendly and brief string representation of a state.

StringBuffer

statementEvaluation(State preState, State postState, int pid, Statement statement)

StringBuffer

stateToString(State state)

Computes the user-friendly and complete string representation of a state.

StringBuffer

stateToString(State state, int lastSavedState, int sequenceId)

Computes the user-friendly and complete string representation of a state.

String

symbolicExpressionToString(CIVLSource source, State state, CIVLType type, dev.civl.sarl.IF.expr.SymbolicExpression symbolicExpression)

Computes the user-friendly string representation of a symbolic expression.

Method Details
- isConcretePointer
  
  static boolean isConcretePointer(dev.civl.sarl.IF.expr.SymbolicExpression pointer)
  
  Parameters:
  
  pointer - A pointer type symbolic expression.
  
  Returns:
  
  true iff the given pointer is concrete.
- getSubArray
  
  dev.civl.sarl.IF.expr.SymbolicExpression getSubArray(State state, int pid, dev.civl.sarl.IF.expr.SymbolicExpression array, dev.civl.sarl.IF.expr.NumericExpression startIndex, dev.civl.sarl.IF.expr.NumericExpression endIndex, CIVLSource source) throws UnsatisfiablePathConditionException
  
  Given an array, a start index, and end index, returns the array which is the subsequence of the given array consisting of the elements in positions start index through end index minus one. The length of the new array is endIndex - startIndex. TODO move to libcivlc?
  
  Parameters:
  
  array -
  
  startIndex -
  
  endIndex -
  
  source -
  
  assumption -
  
  Returns:
  
  Throws:
  
  UnsatisfiablePathConditionException
- stateInformation
  
  StringBuffer stateInformation(State state)
  
  Computes the user-friendly and brief string representation of a state. Only the call stack is printed.
  
  Parameters:
  
  state - The state whose string representation is to be computed.
  
  Returns:
  
  The user-friendly string representation of a state.
- stateToString
  
  StringBuffer stateToString(State state)
  
  Computes the user-friendly and complete string representation of a state. Everything including dyscopes, call stacks is printed.
  
  Parameters:
  
  state -
  
  Returns:
- stateToString
  
  StringBuffer stateToString(State state, int lastSavedState, int sequenceId)
  
  Computes the user-friendly and complete string representation of a state. Everything including dyscopes, call stacks is printed.
  
  Parameters:
  
  state -
  
  lastSavedState - the last saved state that this state is generated from. -1 if the there is no such last saved state.
  
  sequenceId - the place that this state have in the sequence of intermediate states after executing the last saved state. -1 iff lastSavedState is -1.
  
  Returns:
- symbolicExpressionToString
  
  String symbolicExpressionToString(CIVLSource source, State state, CIVLType type, dev.civl.sarl.IF.expr.SymbolicExpression symbolicExpression)
  Computes the user-friendly string representation of a symbolic expression.
  
  If the given expression is a pointer, then its string representation is computed according to the object that it refers to:
  
  a variable: invalid input: '&' variable <dyscope name>;
  e.g.,
  int a = 9; int * p = &a;
  The representation of p would be invalid input: '&a'<d0> assuming that the name of the dynamic scope of a is d0.
  
  an element of an array: invalid input: '&array'<dyscope name>[index];
  e.g.,
  int a[5]; int *p = invalid input: '&a'[1];
  The representation of p would be invalid input: '&a'<d0>[1] assuming that the name of the dynamic scope of a is d0.
  
  a field of a struct: invalid input: '&struct'<dyscope name>.field;
  e.g.,
  typedef struct {int x; int y;} A; A s; int*p = invalid input: '&s'.y;
  The representation of p would be invalid input: '&a'<d0>.y assuming that the name of the dynamic scope of a is d0.
  
  a heap cell: heapObject<dyscope name, malloc ID, number of malloc call> .
  Parameters:
  
  source - The source code information related to the symbolic expression for error report if any.
  
  state - The state that the symbolic expression belongs to.
  
  symbolicExpression - The symbolic expression whose string representation is to be computed.
  
  Returns:
  
  The user-friendly string representation of a state.
- civlTypeOfObjByPointer
  
  CIVLType civlTypeOfObjByPointer(CIVLSource soruce, State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer)
  
  Computes the CIVL type of the object referring to by the given pointer.
  
  Parameters:
  
  soruce - The source code information related to the symbolic expression for error report if any.
  
  state - The state that the given pointer belongs to.
  
  pointer - The pointer the type of whose object is to be computed.
  
  Returns:
  
  The CIVL type of the object referring to by the given pointer.
- dynamicTypeOfObjByPointer
  
  dev.civl.sarl.IF.type.SymbolicType dynamicTypeOfObjByPointer(CIVLSource source, State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer)
  
  Computes the SymbolicType of the object referring to by the given pointer.
  
  Parameters:
  
  source - The source code information related to the symbolic expression for error report if any.
  
  state - The state that the given pointer belongs to.
  
  pointer - The pointer the type of whose object is to be computed.
  
  Returns:
  
  The SymbolicType of the object referring to by the given pointer.
- getArrayBaseType
  
  CIVLType getArrayBaseType(State state, CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression arrayPtr)
  pre-condition:
  
  "arrayPtr" must point to an array
  
  "source" is the @{link CIVLSource} of the pointer expression
  
  post-condition:
  
  the returned CIVLType must not be an array type
  
  the returned object cannot be null
  
  Get the type of the non-array element of an array by given a pointer to an array
  Parameters:
  
  array -
  
  Returns:
  
  the type of the non-array element of an array
- getLeafNodeReference
  
  dev.civl.sarl.IF.expr.ReferenceExpression getLeafNodeReference(State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer, CIVLSource source)
  
  Spec: Returns a ReferenceExpression object which directly refer to the object which has the physical base type of the pointed array (or object) residing in memory.
  Note: The "physical base type" means the base type of the a physical sequence of objects in memory space. For example: int ** a; int b[2][2]; int c; a = (int **)malloc(..); The "physical base type" of "a" is "int *" while both of "b" and of "c" is "int".
  
  Parameters:
  
  state - The current state
  
  source - The CIVL source of the pointer
  
  process - The information of the process
  
  Returns:
  
  The Reference to the object that has physical base type
  
  Throws:
  
  UnsatisfiablePathConditionException
- getUniverse
  
  dev.civl.sarl.IF.SymbolicUniverse getUniverse()
  
  Gets the symbolic universe used by this symbolic analyzer.
  
  Returns:
  
  the symbolic universe
- expressionEvaluation
  
  Pair<State,String> expressionEvaluation(State state, int pid, Expression expression, boolean resultOnly) throws UnsatisfiablePathConditionException
  
  Compute a friendly string representation of an expression's evaluation. Eg, if the expression is a+b, then return 8+9 supposing a=8, b=9.
  
  Returns:
  
  Throws:
  
  UnsatisfiablePathConditionException
- statementEvaluation
  
  StringBuffer statementEvaluation(State preState, State postState, int pid, Statement statement) throws UnsatisfiablePathConditionException
  
  Throws:
  
  UnsatisfiablePathConditionException
- inputVariablesToStringBuffer
  
  StringBuffer inputVariablesToStringBuffer(State state)
- evaluator
  
  Evaluator evaluator()
- pointerArithmetics
  
  dev.civl.sarl.IF.expr.SymbolicExpression pointerArithmetics(CIVLSource source, State state, boolean isSubtract, dev.civl.sarl.IF.expr.SymbolicExpression pointer, dev.civl.sarl.IF.expr.SymbolicExpression offset)
- isDefinedPointer
  
  Pair<dev.civl.sarl.IF.expr.BooleanExpression,dev.civl.sarl.IF.ValidityResult.ResultType> isDefinedPointer(State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer, CIVLSource civlSource)
  Is this an defined pointer? A pointer is defined if one of the following holds:
  
  it can be dereferenced (derefable pointer), e.g., invalid input: '&a', invalid input: '&b'[0] where a is a scalar variable and b is an array of length 5.
  
  it is the NULL pointer.
  
  it points to the end of an array, e.g., invalid input: '&b'[5] where b is an array of length 5.
  
  For the latter two cases, the pointer is called underefable pointer.
  Parameters:
  
  state - The current state
  
  pointer - The pointer.
  
  civlSource - The source related with the pointer
  
  Returns:
  
  True iff the given pointer is defined.
  
  Throws:
  
  CIVLUnimplementedFeatureException - If the given pointer is a non-concrete one.
- isDerefablePointer
  
  Pair<dev.civl.sarl.IF.expr.BooleanExpression,dev.civl.sarl.IF.ValidityResult.ResultType> isDerefablePointer(State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer)
  
  Is this a derefable pointer? In other words, check if the pointer can be dereferenced safely. Examples of derefable pointers: invalid input: '&a', invalid input: '&b'[0] where a is a scalar variable and b is an array of length 5. Examples of underefable pointers: NULL, invalid input: '&b'[5] where b is an array of length 5.
  
  Parameters:
  
  state -
  
  pointer -
  
  Returns:
- pathconditionToString
  
  StringBuffer pathconditionToString(CIVLSource source, State state, String prefix, dev.civl.sarl.IF.expr.BooleanExpression pc)
  
  Pretty representation of a path condition, which is broken into lines if it is in CNF.
  
  Parameters:
  
  state -
  
  pc -
  
  Returns:
- memoryUnitToString
  
  StringBuffer memoryUnitToString(State state, MemoryUnit mu)
  
  Pretty representation of a memory unit.
  
  Parameters:
  
  state -
  
  mu -
  
  Returns:
- areDynamicTypesCompatiableForAssign
  
  boolean areDynamicTypesCompatiableForAssign(dev.civl.sarl.IF.type.SymbolicType lhsType, dev.civl.sarl.IF.type.SymbolicType rhsType)
  Check if the dynamic types of the left-hand side (lhs) and right-hand side (rhs) expression are compatible for assignment operation.
  
  If the type of lhs or rhs is a numeric/boolean/char/uninterpreted type, their dynamic types must be exactly the same.
  
  If the type of lhs or rhs is non-scalar type, the following rules will be recursively applied to check their compatibility:
  
  IF lhs has a complete array-of-T0 type "t0", rhs must have a complete array-of-T1 type "t1". T0 and T1 must be compatible for assignment. The extent of "t0" must equal to the extent of "t1".
  
  IF lhs has an incomplete array-of-T type, rhs must have array-of-T type.
  
  IF lhs has a tuple type, rhs must have a tuple type as well. The tuple types of lhs and rhs must have same amount of component types. Each pair of component types in the tuple types of the lhs and rhs must be compatiable
  
  IF lhs has a union type, rhs must have a union type as well. The union types of lhs and rhs must have same amount of component types. Each pair of component types in the union types of the lhs and rhs must be compatiable
  Parameters:
  
  lhsType - The dynamic type of the left-hand side expression
  
  rhsType - The dynamic type of the right-hand side expression
  
  Returns:
  
  true iff the given two dynamic types are compatible for an assignment operation

Interface SymbolicAnalyzer

Method Summary

Method Details

isConcretePointer

getSubArray

stateInformation

stateToString

stateToString

symbolicExpressionToString

civlTypeOfObjByPointer

dynamicTypeOfObjByPointer

getArrayBaseType

getLeafNodeReference

getUniverse

expressionEvaluation

statementEvaluation

inputVariablesToStringBuffer

evaluator

pointerArithmetics

isDefinedPointer

isDerefablePointer

pathconditionToString

memoryUnitToString

areDynamicTypesCompatiableForAssign