Module dev.civl.mc

Package dev.civl.mc.dynamic.IF

Interface SymbolicUtility

public interface SymbolicUtility

A SymbolicUtility provides all the common operations of symbolic expressions.

Method Summary

Modifier and Type	Method	Description
dev.civl.sarl.IF.expr.SymbolicExpression	applyReverseFunction(String originalFunction, dev.civl.sarl.IF.expr.SymbolicExpression argument)	Apply the reverse of a given uninterpreted function.
boolean	arePoint2SameMemoryBlock(dev.civl.sarl.IF.expr.SymbolicExpression ptr0, dev.civl.sarl.IF.expr.SymbolicExpression ptr1)	Returns true iff the two pointers are pointing to the same memory block.
Pair<dev.civl.sarl.IF.expr.NumericExpression,dev.civl.sarl.IF.expr.NumericExpression>	arithmeticIntDivide(dev.civl.sarl.IF.expr.NumericExpression dividend, dev.civl.sarl.IF.expr.NumericExpression denominator)	This function does an arithmetic integer division, returns the quotient and remainder
dev.civl.sarl.IF.expr.NumericExpression[]	arrayDimensionExtents(dev.civl.sarl.IF.type.SymbolicCompleteArrayType arrayType)	Pre-condition: For all the descendant types of the array type, if it is an array type, it must be complete.
dev.civl.sarl.IF.expr.SymbolicExpression	arrayRootPtr(dev.civl.sarl.IF.expr.SymbolicExpression arrayPtr)	Given a pointer to an element of an array object, returns a pointer to the whole array object.
dev.civl.sarl.IF.expr.NumericExpression[]	arraySlicesSizes(dev.civl.sarl.IF.expr.NumericExpression[] array_extents)	pre-condition: length(array_extents) > 0
StringBuffer	charArrayToString(CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression charArray, int startIndex, boolean forPrint)	Constructs the string representation of an array of characters, which contains at least one '\0' character, starting from the given index and ending at the index of '\0' minus one.
dev.civl.sarl.IF.expr.BooleanExpression	contains(dev.civl.sarl.IF.expr.SymbolicExpression container, dev.civl.sarl.IF.expr.SymbolicExpression element)	Checks if the object that the container pointer points to contains that of the element pointer.
dev.civl.sarl.IF.type.SymbolicTupleType	dynamicType()	returns the symbolic type of dynamic type which is used to model user-defined types.
dev.civl.sarl.IF.expr.SymbolicExpression	extendPointer(dev.civl.sarl.IF.expr.SymbolicExpression componentPointer, dev.civl.sarl.IF.expr.ReferenceExpression reference)	* Constructs a pointer by combining a pointer to a component, either an object (a heap atomic object or a normal object) or a sub-component of an object, and a reference expression w.r.t that component.
dev.civl.sarl.IF.expr.NumericExpression[]	extractArrayIndicesFrom(dev.civl.sarl.IF.expr.SymbolicExpression pointerToArrayElement)	Given a pointer to an array element, returns the indices of the element.
int	extractInt(CIVLSource source, dev.civl.sarl.IF.expr.NumericExpression expression)	Gets a Java concrete int from a symbolic expression
int	extractIntField(CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression tuple, dev.civl.sarl.IF.object.IntObject fieldIndex)	Gets a concrete Java int from the field of a symbolic expression of tuple type or throws exception.
dev.civl.sarl.IF.expr.SymbolicConstant	freshBoundVariableFor(dev.civl.sarl.IF.type.SymbolicType type, dev.civl.sarl.IF.expr.SymbolicExpression... expressions)	Creating a bound variable of the given "type", which is an instance of SymbolicConstant, whose name has no conflict with any other symbolic constants in the given set of "expressions".
List<dev.civl.sarl.IF.expr.SymbolicConstant>	freshBoundVariablesFor(int num, dev.civl.sarl.IF.type.SymbolicType type, dev.civl.sarl.IF.expr.SymbolicExpression... expressions)
dev.civl.sarl.IF.expr.SymbolicExpression	getAbstractGuardOfFunctionCall(String library, String function, dev.civl.sarl.IF.expr.SymbolicExpression[] argumentValues)	returns the abstract guard of a function call
int	getArrayIndex(CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Given a pointer to a certain element of some array, returns the index of the element that the pointer points to.
dev.civl.sarl.IF.expr.BooleanExpression[]	getConjunctiveClauses(dev.civl.sarl.IF.expr.BooleanExpression cnfClause)	Returns the sub-clauses of a CNF clause.
dev.civl.sarl.IF.expr.NumericExpression	getDimensionOf(dev.civl.sarl.IF.expr.SymbolicExpression domain)	Returns the dimension of the given domain.
dev.civl.sarl.IF.type.SymbolicType	getDomainElementType(dev.civl.sarl.IF.expr.SymbolicExpression domain)	Get the type of elements of domain which are also elements of literal domain object.
List<dev.civl.sarl.IF.expr.SymbolicExpression>	getDomainInit(dev.civl.sarl.IF.expr.SymbolicExpression domValue)	Get the first integer tuple of a domain.
Iterator<List<dev.civl.sarl.IF.expr.SymbolicExpression>>	getDomainIterator(dev.civl.sarl.IF.expr.SymbolicExpression domain)	Return a iterator for a domain object.
dev.civl.sarl.IF.expr.NumericExpression	getDomainSize(dev.civl.sarl.IF.expr.SymbolicExpression domain)	Computes the size of a domain, that is the number of elements contained in the domain.
dev.civl.sarl.IF.expr.NumericExpression	getHighOfRegularRange(dev.civl.sarl.IF.expr.SymbolicExpression range)	Returns the upper bound of the given range.
dev.civl.sarl.IF.expr.NumericExpression	getLowOfRegularRange(dev.civl.sarl.IF.expr.SymbolicExpression range)	Returns the lower bound of the given range.
dev.civl.sarl.IF.object.IntObject	getMallocID(dev.civl.sarl.IF.expr.SymbolicExpression pointer)	The parameter "pointer" must be a returned value of heapMemUnit(SymbolicExpression)
List<dev.civl.sarl.IF.expr.SymbolicExpression>	getNextInRectangularDomain(dev.civl.sarl.IF.expr.SymbolicExpression domValue, List<dev.civl.sarl.IF.expr.SymbolicExpression> currentTuple, int concreteDim)	Get the subsequence of the given element of the domain.
dev.civl.sarl.IF.expr.SymbolicExpression	getPointer2MemoryBlock(dev.civl.sarl.IF.expr.SymbolicExpression heapPointer)	Takes a pointer to some location inside a memory block m, returns the pointer to m, where a memory block is defined as a space in heap which is allocated by once execution of $malloc.
dev.civl.sarl.IF.expr.SymbolicExpression	getRangeOfRectangularDomain(dev.civl.sarl.IF.expr.SymbolicExpression domain, int index)	Returns the given index-th range of a rectangular domain.
dev.civl.sarl.IF.expr.SymbolicExpression	getScopeValue(dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Given a pointer value, returns the dynamic scope type component of that pointer value.
dev.civl.sarl.IF.expr.NumericExpression	getStepOfRegularRange(dev.civl.sarl.IF.expr.SymbolicExpression range)	Returns the step of the given range Precondition: range is a regular range
dev.civl.sarl.IF.expr.ReferenceExpression	getSymRef(dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Given a pointer value, returns the symbolic reference component of that value.
ValueSetUtility	getValueSetUtility()
int	getVariableId(CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Given a pointer value, returns the variable ID component of that value.
dev.civl.sarl.IF.expr.SymbolicExpression	heapMemUnit(dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Returns the heap memory unit involved by the given pointer.
dev.civl.sarl.IF.expr.SymbolicConstant	invalidHeapObject(dev.civl.sarl.IF.type.SymbolicType heapObjectType)	Constructs an invalid heap object of a certain type.
boolean	isConcretePointer(dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Tests if the given symbolic expression is a concrete pointer value.
boolean	isDisjointWith(dev.civl.sarl.IF.expr.SymbolicExpression pointer1, dev.civl.sarl.IF.expr.SymbolicExpression pointer2)	Checks if the components (either a complete object or a sub-component of an object) that the two pointers point to have no intersection.
boolean	isEmptyDomain(dev.civl.sarl.IF.expr.SymbolicExpression domain, int dim, CIVLSource source)	Returns true if and only if the given domain is empty which means there is no elements in the domain.
boolean	isEmptyHeap(dev.civl.sarl.IF.expr.SymbolicExpression heapValue)	Checks if a heap is empty, i.e., either it is the SARL null expression or all heap objects it holds are marked as INVALID (already deallocated).
boolean	isInitialized(dev.civl.sarl.IF.expr.SymbolicExpression value)	Checks if a given value is initialized.
dev.civl.sarl.IF.expr.BooleanExpression	isInRange(dev.civl.sarl.IF.expr.NumericExpression value, dev.civl.sarl.IF.expr.NumericExpression low, dev.civl.sarl.IF.expr.NumericExpression upper, dev.civl.sarl.IF.expr.NumericExpression step)	Test if the given value is within the range, which is given by an inclusibe lower bound, an exclusibe upper bound and a step
dev.civl.sarl.IF.expr.BooleanExpression	isInRange(dev.civl.sarl.IF.expr.SymbolicExpression value, dev.civl.sarl.IF.expr.SymbolicExpression range)	Checks if the given value is within the index-th range of a certain rectangular domain.
boolean	isInvalidHeapObject(dev.civl.sarl.IF.expr.SymbolicExpression heapObject)	Is this heap object invalid?
boolean	isLiteralDomain(dev.civl.sarl.IF.expr.SymbolicExpression domain)	Returns true if and only if the domain is more precisely a literal domain.
boolean	isMallocPointer(CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Is the given pointer the result of some malloc/handle create operation?
boolean	isNullPointer(dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Checks if a given pointer is a NULL pointer.
boolean	isPointer2MemoryBlock(dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Returns true iff the given pointer is a pointer to a memory block, where a memory block is defined as a space in heap which is allocated by once execution of $malloc.
boolean	isPointerToHeap(dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Is the given pointer pointing to a memory space that is part of a heap?
boolean	isRectangularDomain(dev.civl.sarl.IF.expr.SymbolicExpression domain)	Is the given domain a rectangular domain?
boolean	isRegularRange(dev.civl.sarl.IF.expr.SymbolicExpression range)	Is the given range a regular range?
boolean	isValidRefOf(dev.civl.sarl.IF.expr.ReferenceExpression ref, dev.civl.sarl.IF.type.SymbolicType objectValueType)	Checks if the given reference is valid for the symbolic type of a certain object value.
int	literalDomainSearcher(dev.civl.sarl.IF.expr.SymbolicExpression literalDomain, List<dev.civl.sarl.IF.expr.SymbolicExpression> literalDomElement, int dim)	Iterating a literal domain to match a given domain element.
dev.civl.sarl.IF.expr.ReferenceExpression	makeArrayElementReference(dev.civl.sarl.IF.expr.ReferenceExpression arrayReference, dev.civl.sarl.IF.expr.NumericExpression[] newIndices)	Returns an array element reference by giving the array reference and the coordinates to indexing the element.
dev.civl.sarl.IF.expr.SymbolicExpression	makeFunctionPointer(int dyscopeID, int fid)
dev.civl.sarl.IF.expr.SymbolicExpression	makePointer(int dyscopeId, int varId, dev.civl.sarl.IF.expr.ReferenceExpression symRef)	Makes a pointer value from the given dynamic scope ID, variable ID, and symbolic reference value.
dev.civl.sarl.IF.expr.SymbolicExpression	makePointer(dev.civl.sarl.IF.expr.SymbolicExpression oldPointer, dev.civl.sarl.IF.expr.ReferenceExpression symRef)	Constructs a new pointer by replacing the reference expression of a given pointer.
dev.civl.sarl.IF.expr.SymbolicExpression	newArray(dev.civl.sarl.IF.expr.BooleanExpression context, dev.civl.sarl.IF.type.SymbolicType elementValueType, dev.civl.sarl.IF.expr.NumericExpression length, dev.civl.sarl.IF.expr.SymbolicExpression eleValue)	Creates a new array of given length, using the given type as its element type, and each element having the given value.
dev.civl.sarl.IF.expr.SymbolicExpression	nullFunctionPointer()
dev.civl.sarl.IF.expr.SymbolicExpression	nullPointer()	Returns the NULL pointer of CIVL.
dev.civl.sarl.IF.expr.SymbolicExpression	parentPointer(dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Given a non-trivial pointer, i.e., a pointer to some location inside an object, returns the parent pointer.
BitSet	range2BitSet(dev.civl.sarl.IF.expr.SymbolicExpression range, dev.civl.sarl.IF.Reasoner reasoner)	pre-condition : The parameter range is either a range or an integer
boolean	recDomainHasNext(dev.civl.sarl.IF.expr.SymbolicExpression rectangularDomain, int concreteDim, List<dev.civl.sarl.IF.expr.SymbolicExpression> domElement)	Check if the given domain element has a subsequence in the given rectangular domain.
dev.civl.sarl.IF.expr.ReferenceExpression	referenceOfPointer(dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Computes the reference expression of a pointer.
dev.civl.sarl.IF.expr.ReferenceExpression	referenceToHeapMemUnit(dev.civl.sarl.IF.expr.SymbolicExpression heapPointer)	Computes the reference expression of a given heap pointer w.r.t the corresponding heap object.
dev.civl.sarl.IF.expr.SymbolicExpression	setSymRef(dev.civl.sarl.IF.expr.SymbolicExpression pointer, dev.civl.sarl.IF.expr.ReferenceExpression symRef)	Returns the pointer value obtained by replacing the symRef component of the given pointer value with the given symRef.
dev.civl.sarl.IF.expr.SymbolicExpression[]	symbolicArrayToConcreteArray(dev.civl.sarl.IF.expr.SymbolicExpression array)	Convert an array type symbolic expression with ARRAY operator to a concrete Java array.
dev.civl.sarl.IF.expr.SymbolicExpression	undefinedPointer()	Returns the undefined pointer of CIVL, which is an uninitialized pointer value.

Method Details

charArrayToString

StringBuffer charArrayToString(CIVLSource source,
 dev.civl.sarl.IF.expr.SymbolicExpression charArray,
 int startIndex,
 boolean forPrint)

Constructs the string representation of an array of characters, which contains at least one '\0' character, starting from the given index and ending at the index of '\0' minus one. If the result is to be printed, then special characters like '\r', '\t', etc, will be replaced as the actual string representation "\\r", "\\t", etc. For example, given an character array {'a', 'b', '\t', 'c', 'd', '\n', '\0'}, if starting index is 1, and is it not for print, then the result string will be "b\tcd\n"; if it is for print, then the result string is "b\\tcd\\n". Notions for pointer Value:
undefined: default initialized value/freed/ defined:
derefable: can be dereferenced, e.g., a, a+4 (a is int[5]) underefable: e.g., NULL, a+5 (a is int[5])

Parameters:

source - The source code information for error report.

charArray - The character array in the representation of symbolic sequence

startIndex - The index in the character array where the string starts

forPrint - Will the result be printed? If yes, then special characters need to be handled specifically, e.g., '\n' becomes "\\n".

Returns:

the string representation from the given character array with

contains

dev.civl.sarl.IF.expr.BooleanExpression contains(dev.civl.sarl.IF.expr.SymbolicExpression container,
 dev.civl.sarl.IF.expr.SymbolicExpression element)

Checks if the object that the container pointer points to contains that of the element pointer. Precondition: both pointers can be safely dereferenced.

Parameters:

container - The pointer that is expected to contain the object of the element pointer.

element - The element pointer.

Returns:

True iff the object that the first pointer points to contains that of the send pointer.

extractInt

int extractInt(CIVLSource source,
 dev.civl.sarl.IF.expr.NumericExpression expression)

Gets a Java concrete int from a symbolic expression

Parameters:

source - source code information for error report

expression - a numeric expression expected to hold concrete int value

Returns:

the concrete int

extractIntField

int extractIntField(CIVLSource source,
 dev.civl.sarl.IF.expr.SymbolicExpression tuple,
 dev.civl.sarl.IF.object.IntObject fieldIndex)

Gets a concrete Java int from the field of a symbolic expression of tuple type or throws exception.

Parameters:

source - source code information for error report

tuple - symbolic expression of tuple type

fieldIndex - index of a field in that tuple

Returns:

the concrete int value of that field

Throws:

CIVLInternalException - if a concrete integer value cannot be extracted

getArrayIndex

int getArrayIndex(CIVLSource source,
 dev.civl.sarl.IF.expr.SymbolicExpression pointer)

Given a pointer to a certain element of some array, returns the index of the element that the pointer points to.

Precondition: pointer must point to an element of some array.

Parameters:

source - The source code information for error report.

pointer - The pointer checks.

Returns:

The index of the element that the pointer points to.

getScopeValue

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

Given a pointer value, returns the dynamic scope type component of that pointer value.

Parameters:

pointer - a pointer value

Returns:

dynamic scope type value which is a component of a pointer

getSymRef

dev.civl.sarl.IF.expr.ReferenceExpression getSymRef(dev.civl.sarl.IF.expr.SymbolicExpression pointer)

Given a pointer value, returns the symbolic reference component of that value. The "symRef" refers to a sub-structure of the variable pointed to.

Parameters:

pointer - a pointer value

Returns:

the symRef component

setSymRef

dev.civl.sarl.IF.expr.SymbolicExpression setSymRef(dev.civl.sarl.IF.expr.SymbolicExpression pointer,
 dev.civl.sarl.IF.expr.ReferenceExpression symRef)

Returns the pointer value obtained by replacing the symRef component of the given pointer value with the given symRef.

Parameters:

pointer - a pointer value

symRef - a symbolic reference expression

Returns:

the pointer obtained by modifying the given one by replacing its symRef field with the given symRef

getVariableId

int getVariableId(CIVLSource source,
 dev.civl.sarl.IF.expr.SymbolicExpression pointer)

Given a pointer value, returns the variable ID component of that value.

Parameters:

source - the source code information for error report.

pointer - a pointer value

Returns:

the variable ID component of that value

heapMemUnit

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

Returns the heap memory unit involved by the given pointer.

Parameters:

pointer - A valid pointer that points to some part of a heap.

Returns:

A pointer to a heap object that is involved by the given pointer.

invalidHeapObject

dev.civl.sarl.IF.expr.SymbolicConstant invalidHeapObject(dev.civl.sarl.IF.type.SymbolicType heapObjectType)

Constructs an invalid heap object of a certain type. A heap object becomes invalid when it gets deallocated.

Parameters:

heapObjectType - The type of the heap object.

Returns:

The invalid heap object of the given type.

isDisjointWith

boolean isDisjointWith(dev.civl.sarl.IF.expr.SymbolicExpression pointer1,
 dev.civl.sarl.IF.expr.SymbolicExpression pointer2)

Checks if the components (either a complete object or a sub-component of an object) that the two pointers point to have no intersection.

Parameters:

pointer1 - The first pointer.

pointer2 - The second pointer.

Returns:

True iff there is no intersection between the components that the given two pointers point to.

isEmptyHeap

boolean isEmptyHeap(dev.civl.sarl.IF.expr.SymbolicExpression heapValue)

Checks if a heap is empty, i.e., either it is the SARL null expression or all heap objects it holds are marked as INVALID (already deallocated).

Parameters:

heapValue - The value of the heap to be checked.

Returns:

True iff the heap has null value or is empty.

isMallocPointer

boolean isMallocPointer(CIVLSource source,
 dev.civl.sarl.IF.expr.SymbolicExpression pointer)

Is the given pointer the result of some malloc/handle create operation?

Parameters:

source - The source code information for error report.

pointer - The pointer to be checked.

Returns:

True iff the given pointer is the result of some malloc/handle create operation.

isInitialized

boolean isInitialized(dev.civl.sarl.IF.expr.SymbolicExpression value)

Checks if a given value is initialized.

Parameters:

value - The value to be checked.

Returns:

True iff the value is already initialized.

isInRange

dev.civl.sarl.IF.expr.BooleanExpression isInRange(dev.civl.sarl.IF.expr.NumericExpression value,
 dev.civl.sarl.IF.expr.NumericExpression low,
 dev.civl.sarl.IF.expr.NumericExpression upper,
 dev.civl.sarl.IF.expr.NumericExpression step)

Test if the given value is within the range, which is given by an inclusibe lower bound, an exclusibe upper bound and a step

Parameters:

value - a numeric value to be tested if it is in range.

low - the inclusive lower bound of the range

upper - the exclusive upper bound of the range

step - the step of the range

Returns:

True iff the given value is within the index-th range of a certain domain.

isInRange

dev.civl.sarl.IF.expr.BooleanExpression isInRange(dev.civl.sarl.IF.expr.SymbolicExpression value,
 dev.civl.sarl.IF.expr.SymbolicExpression range)

Checks if the given value is within the index-th range of a certain rectangular domain.

Parameters:

value - The value to be tested if it is in range.

range - The range.

Returns:

True iff the given value is within the index-th range of a certain domain.

isInvalidHeapObject

boolean isInvalidHeapObject(dev.civl.sarl.IF.expr.SymbolicExpression heapObject)

Is this heap object invalid?

Parameters:

heapObject - The heap object.

Returns:

True iff the given heap object is invalid.

isNullPointer

boolean isNullPointer(dev.civl.sarl.IF.expr.SymbolicExpression pointer)

Checks if a given pointer is a NULL pointer.

Parameters:

pointer - The pointer to be checked.

Returns:

True iff the given pointer is NULL.

isPointerToHeap

boolean isPointerToHeap(dev.civl.sarl.IF.expr.SymbolicExpression pointer)

Is the given pointer pointing to a memory space that is part of a heap?

Parameters:

pointer - The pointer to be tested.

Returns:

True iff the pointer points to a certain part of some heap.

isPointer2MemoryBlock

boolean isPointer2MemoryBlock(dev.civl.sarl.IF.expr.SymbolicExpression pointer)

Returns true iff the given pointer is a pointer to a memory block, where a memory block is defined as a space in heap which is allocated by once execution of $malloc.

FYI, given a pointer, isPointer2MemoryBlock(SymbolicExpression) implies isPointerToHeap(SymbolicExpression), but not vice versa.

Parameters:

pointer - A SymbolicExpression which represents a concrete pointer.

Returns:

Returns true iff the given pointer is pointer to a memory block.

getPointer2MemoryBlock

dev.civl.sarl.IF.expr.SymbolicExpression getPointer2MemoryBlock(dev.civl.sarl.IF.expr.SymbolicExpression heapPointer)

Takes a pointer to some location inside a memory block m, returns the pointer to m, where a memory block is defined as a space in heap which is allocated by once execution of $malloc.

Parameters:

heapPointer - A pointer to some location inside a memory block. isPointerToHeap(heapPointer) must returns true.

Returns:

A pointer to the memory block

arePoint2SameMemoryBlock

boolean arePoint2SameMemoryBlock(dev.civl.sarl.IF.expr.SymbolicExpression ptr0,
 dev.civl.sarl.IF.expr.SymbolicExpression ptr1)

Returns true iff the two pointers are pointing to the same memory block. A memory block is the space in memory heap that are allocated by once execution of a $malloc.

Parameters:

ptr0 - A concrete pointer which is an operand of pointer subtraction operation.

ptr1 - A concrete pointer which is another operand of pointer subtraction operation.

Returns:

True iff the two pointers are pointing to the same memory block.

isValidRefOf

boolean isValidRefOf(dev.civl.sarl.IF.expr.ReferenceExpression ref,
 dev.civl.sarl.IF.type.SymbolicType objectValueType)

Checks if the given reference is valid for the symbolic type of a certain object value.

Parameters:

ref - The reference.

objectValueType - The symbolic type of the value of the given object.

Returns:

True iff the given reference expression is applicable for the given object value type.

makePointer

dev.civl.sarl.IF.expr.SymbolicExpression makePointer(int dyscopeId,
 int varId,
 dev.civl.sarl.IF.expr.ReferenceExpression symRef)

Makes a pointer value from the given dynamic scope ID, variable ID, and symbolic reference value.

Parameters:

dyscopeId - ID number of a dynamic scope

varId - ID number of a variable within that scope

symRef - a symbolic reference to a point within the variable

Returns:

a pointer value as specified by the 3 components

makePointer

dev.civl.sarl.IF.expr.SymbolicExpression makePointer(dev.civl.sarl.IF.expr.SymbolicExpression oldPointer,
 dev.civl.sarl.IF.expr.ReferenceExpression symRef)

Constructs a new pointer by replacing the reference expression of a given pointer. For example, given a pointer invalid input: '&a'[5] and a reference [0], the result will be invalid input: '&a'[0]. The given pointer can refer to a heap object, in which case, the heap object reference is considered the old "variable" and will remain the same.

Parameters:

oldPointer - The old pointer whose reference expression will be changed.

symRef - The new reference expression to be used for the new pointer.

Returns:

the new pointer which refers to the same variable/heap object as the given pointer, but with a new reference expression.

extendPointer

dev.civl.sarl.IF.expr.SymbolicExpression extendPointer(dev.civl.sarl.IF.expr.SymbolicExpression componentPointer,
 dev.civl.sarl.IF.expr.ReferenceExpression reference)

* Constructs a pointer by combining a pointer to a component, either an object (a heap atomic object or a normal object) or a sub-component of an object, and a reference expression w.r.t that component.

Parameters:

componentPointer - a pointer to a component

reference - a reference expression

Returns:

A new pointer by combining the component pointer and the given reference w.r.t. that component.

newArray

dev.civl.sarl.IF.expr.SymbolicExpression newArray(dev.civl.sarl.IF.expr.BooleanExpression context,
 dev.civl.sarl.IF.type.SymbolicType elementValueType,
 dev.civl.sarl.IF.expr.NumericExpression length,
 dev.civl.sarl.IF.expr.SymbolicExpression eleValue)

Creates a new array of given length, using the given type as its element type, and each element having the given value.

Parameters:

context - The context of the operation, i.e., the path condition of the current state.

elementValueType - The type of the array element. Note necessarily the type of eleValue.

length - The length of the array.

eleValue - The element value of the array.

Returns:

the new array of the given length, with each element initialized with the given symbolic expression.

nullPointer

dev.civl.sarl.IF.expr.SymbolicExpression nullPointer()

Returns the NULL pointer of CIVL.

Returns:

The NULL pointer of CIVL.

parentPointer

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

Given a non-trivial pointer, i.e., a pointer to some location inside an object, returns the parent pointer. For example, a pointer to an array element returns the pointer to the array.

Parameters:

pointer - non-trivial pointer

Returns:

pointer to parent

referenceOfPointer

dev.civl.sarl.IF.expr.ReferenceExpression referenceOfPointer(dev.civl.sarl.IF.expr.SymbolicExpression pointer)

Computes the reference expression of a pointer. If the pointer is pointing to some part of the heap, then the reference expression is the reference expression w.r.t the corresponding heap atomic object; otherwise, it is the original reference expression of the pointer.

Parameters:

pointer - The pointer to whose reference is to be computed.

Returns:

The reference expression of the pointer w.r.t the object it points to.

referenceToHeapMemUnit

dev.civl.sarl.IF.expr.ReferenceExpression referenceToHeapMemUnit(dev.civl.sarl.IF.expr.SymbolicExpression heapPointer)

Computes the reference expression of a given heap pointer w.r.t the corresponding heap object.

Parameters:

heapPointer - The heap pointer.

Returns:

The reference expression of a given pointer w.r.t the corresponding heap memory unit.

makeArrayElementReference

dev.civl.sarl.IF.expr.ReferenceExpression makeArrayElementReference(dev.civl.sarl.IF.expr.ReferenceExpression arrayReference,
 dev.civl.sarl.IF.expr.NumericExpression[] newIndices)

Returns an array element reference by giving the array reference and the coordinates to indexing the element. This function makes the ArrayElementReference based on the given array reference. For example, for an array "int a[2][3][4]", giving the reference to "a[1]" and an indices array {1,2}, it returns the new reference to "a[1][1][2]".

Parameters:

arrayReference - An reference to an array

newIndices - indexes for referencing the element

Returns:

the new arrayElementReference

undefinedPointer

dev.civl.sarl.IF.expr.SymbolicExpression undefinedPointer()

Returns the undefined pointer of CIVL, which is an uninitialized pointer value. In CIVL, a pointer becomes undefined when the memory space it points to get deallocated.

Returns:

The undefined pointer.

isLiteralDomain

boolean isLiteralDomain(dev.civl.sarl.IF.expr.SymbolicExpression domain)

Returns true if and only if the domain is more precisely a literal domain. A literal domain has the form of an array if integer tuples with fixed size (i.e., the domain's dimension).

Parameters:

domain - The symbolic expression of a domain object

Returns:

true iff the given domain is a literal domain.

getDomainInit

List<dev.civl.sarl.IF.expr.SymbolicExpression> getDomainInit(dev.civl.sarl.IF.expr.SymbolicExpression domValue)

Get the first integer tuple of a domain. Return null if domain is empty.

Parameters:

domValue - The domain object which will contribute a first element.

Returns:

the first integer tuple of a domain, null if the domain is empty

getDomainSize

dev.civl.sarl.IF.expr.NumericExpression getDomainSize(dev.civl.sarl.IF.expr.SymbolicExpression domain)

Computes the size of a domain, that is the number of elements contained in the domain.

Parameters:

domain - The symbolic expression of domain.

Returns:

The number of elements contained in the domain.

getDomainElementType

dev.civl.sarl.IF.type.SymbolicType getDomainElementType(dev.civl.sarl.IF.expr.SymbolicExpression domain)

Get the type of elements of domain which are also elements of literal domain object. For an N dimensional domain, the element type should be an array of integers of length of N, i.e. int [N].

Parameters:

domain - The symbolic expression of a domain object

Returns:

domain element type

getDomainIterator

Iterator<List<dev.civl.sarl.IF.expr.SymbolicExpression>> getDomainIterator(dev.civl.sarl.IF.expr.SymbolicExpression domain)

Return a iterator for a domain object. (This function can be applied on all domain types)

Parameters:

domain - The symbolic expression of the domain object.

Returns:

the iterator for iterating over the domain.

getNextInRectangularDomain

List<dev.civl.sarl.IF.expr.SymbolicExpression> getNextInRectangularDomain(dev.civl.sarl.IF.expr.SymbolicExpression domValue,
 List<dev.civl.sarl.IF.expr.SymbolicExpression> currentTuple,
 int concreteDim)

Get the subsequence of the given element of the domain.

Parameters:

domValue - The symbolic expression of the rectangular domain field.

currentTuple - The current integer tuple which is an element of the domain.

concreteDim - The dimension of domain, which should be concrete.

Returns:

the next integer tuple in the domain

recDomainHasNext

boolean recDomainHasNext(dev.civl.sarl.IF.expr.SymbolicExpression rectangularDomain,
 int concreteDim,
 List<dev.civl.sarl.IF.expr.SymbolicExpression> domElement)

Check if the given domain element has a subsequence in the given rectangular domain. A rectangular domain is the cartesian product of a number of ranges.s

Parameters:

rectangularDomain - The rectangular domain union object.

concreteDim - The number of the dimension of the domain

domElement - The element of the domain

Returns:

true iff there is at least one subsequent element of the given one in the given rectangular domain.

literalDomainSearcher

int literalDomainSearcher(dev.civl.sarl.IF.expr.SymbolicExpression literalDomain,
 List<dev.civl.sarl.IF.expr.SymbolicExpression> literalDomElement,
 int dim)

Iterating a literal domain to match a given domain element. Returns the index of the element.

Parameters:

literalDomain - The symbolic expression of the literal domain union field

literalDomElement - The given element will be matched

dim - The dimension of the literal domain

Returns:

the index of the element in the domain or -1 which means the given element is not a member of the domain.

isEmptyDomain

boolean isEmptyDomain(dev.civl.sarl.IF.expr.SymbolicExpression domain,
 int dim,
 CIVLSource source)

Returns true if and only if the given domain is empty which means there is no elements in the domain.

Parameters:

domain - The symbolic expression of the domain object.

dim - The concrete number of dimension of the domain. It's only significant when the domain is a rectangular domain.

source - The CIVL source of the statement involves this empty checking operation.

Returns:

true iff the given domain is empty

arraySlicesSizes

dev.civl.sarl.IF.expr.NumericExpression[] arraySlicesSizes(dev.civl.sarl.IF.expr.NumericExpression[] array_extents)

pre-condition:

length(array_extents) > 0

Computing sizes of all slices of the given array. Here an array slice is a sub-array with a lower dimension of the given array.

Parameters:

array_extents - Sizes of coordinates representing an array. e.g. {2,3,4} stands for an array T a[2][3][4].

Returns:

Sizes of all array slices. e.g. input:{2,3,4} ==> output:{12, 4, 1}

Throws:

UnsatisfiablePathConditionException

arrayRootPtr

dev.civl.sarl.IF.expr.SymbolicExpression arrayRootPtr(dev.civl.sarl.IF.expr.SymbolicExpression arrayPtr)

Given a pointer to an element of an array object, returns a pointer to the whole array object.

Parameters:

arrayPtr - A pointer refers to an array object.

Returns:

a pointer to the whole array object which is referred by the given pointer.

extractArrayIndicesFrom

dev.civl.sarl.IF.expr.NumericExpression[] extractArrayIndicesFrom(dev.civl.sarl.IF.expr.SymbolicExpression pointerToArrayElement)

Given a pointer to an array element, returns the indices of the element. Array element indices as heap structure are ignored.

Parameters:

pointerToArrayElement - A concrete pointer to an array element.

Returns:

an array of indices with the given reference. The order of indices from left to right is same as the lexical subscript order.

arrayDimensionExtents

dev.civl.sarl.IF.expr.NumericExpression[] arrayDimensionExtents(dev.civl.sarl.IF.type.SymbolicCompleteArrayType arrayType)

Pre-condition: For all the descendant types of the array type, if it is an array type, it must be complete.

Computes extent of each dimension of a given array. Returns an Java Array of extents which are in the same order as the array being declared.
For example, giving an array "int a[2][3][4]" returns {2, 3, 4}.

Parameters:

arrayType - The type of the target array.

Returns:

The Java Array contains array extents information.

arithmeticIntDivide

Pair<dev.civl.sarl.IF.expr.NumericExpression,dev.civl.sarl.IF.expr.NumericExpression> arithmeticIntDivide(dev.civl.sarl.IF.expr.NumericExpression dividend,
 dev.civl.sarl.IF.expr.NumericExpression denominator)

This function does an arithmetic integer division, returns the quotient and remainder

Parameters:

dividend - The NumericExpression of the quotient, must be a Integer number

denominator - The NumericExpression of the denominator, must be a Integer number

Returns:

A Pair of quotient (left) and remainder (right)

dynamicType

dev.civl.sarl.IF.type.SymbolicTupleType dynamicType()

returns the symbolic type of dynamic type which is used to model user-defined types. In CIVL, each user-defined type (e.g., a struct) has a unique ID and is represented as a symbolic expression of the type "dynamic type".

Returns:

the symbolic type of dynamic type

isRectangularDomain

boolean isRectangularDomain(dev.civl.sarl.IF.expr.SymbolicExpression domain)

Is the given domain a rectangular domain?

Parameters:

domain -

Returns:

true iff the given domain is a rectangular domain.

isRegularRange

boolean isRegularRange(dev.civl.sarl.IF.expr.SymbolicExpression range)

Is the given range a regular range?

Parameters:

range -

Returns:

true iff the given range is a regular range.

getRangeOfRectangularDomain

dev.civl.sarl.IF.expr.SymbolicExpression getRangeOfRectangularDomain(dev.civl.sarl.IF.expr.SymbolicExpression domain,
 int index)

Returns the given index-th range of a rectangular domain. Precondition: domain is a rectangular domain.

Parameters:

domain -

index -

Returns:

the index-th range of the given rectangular domain.

getHighOfRegularRange

dev.civl.sarl.IF.expr.NumericExpression getHighOfRegularRange(dev.civl.sarl.IF.expr.SymbolicExpression range)

Returns the upper bound of the given range. Precondition: range is a regular range

Parameters:

range -

Returns:

the upper bound of the given range.

getLowOfRegularRange

dev.civl.sarl.IF.expr.NumericExpression getLowOfRegularRange(dev.civl.sarl.IF.expr.SymbolicExpression range)

Returns the lower bound of the given range. Precondition: range is a regular range

Parameters:

range -

Returns:

the lower bound of the given range.

getStepOfRegularRange

dev.civl.sarl.IF.expr.NumericExpression getStepOfRegularRange(dev.civl.sarl.IF.expr.SymbolicExpression range)

Returns the step of the given range Precondition: range is a regular range

Parameters:

range -

Returns:

the step of the given range

getDimensionOf

dev.civl.sarl.IF.expr.NumericExpression getDimensionOf(dev.civl.sarl.IF.expr.SymbolicExpression domain)

Returns the dimension of the given domain.

Parameters:

domain -

Returns:

the dimension of the given domain.

getConjunctiveClauses

dev.civl.sarl.IF.expr.BooleanExpression[] getConjunctiveClauses(dev.civl.sarl.IF.expr.BooleanExpression cnfClause)

Returns the sub-clauses of a CNF clause. For example, if the given CNF clause is X==3 invalid input: '&'invalid input: '&' Yinvalid input: '<'5 invalid input: '&'invalid input: '&' (a[k]>2 || kinvalid input: '<'0) , then the result is an array of clauses:{ X==3, Yinvalid input: '<'5, a[k]>2 || kinvalid input: '<'0}

Parameters:

cnfClause -

Returns:

the sub-clauses of a CNF clause

getAbstractGuardOfFunctionCall

dev.civl.sarl.IF.expr.SymbolicExpression getAbstractGuardOfFunctionCall(String library,
 String function,
 dev.civl.sarl.IF.expr.SymbolicExpression[] argumentValues)

returns the abstract guard of a function call

Parameters:

function -

arguments -

Returns:

applyReverseFunction

dev.civl.sarl.IF.expr.SymbolicExpression applyReverseFunction(String originalFunction,
 dev.civl.sarl.IF.expr.SymbolicExpression argument)

Apply the reverse of a given uninterpreted function. If the argument is f(X) and the given function is f, then returns X. If the argument is f(X,Y,Z), then returns NULL. If the given function doesn't match the argument's function name, returns NULL. If the argument's operator isn't APPLY, then returns NULL.

Parameters:

originalFunction -

argument -

Returns:

range2BitSet

BitSet range2BitSet(dev.civl.sarl.IF.expr.SymbolicExpression range,
 dev.civl.sarl.IF.Reasoner reasoner)

pre-condition : The parameter range is either a range or an integer

Translate a range to a concrete BitSet. The given range can be a regular range or a simple integer which can be seen as a singleton range.

Parameters:

range -

Returns:

getMallocID

dev.civl.sarl.IF.object.IntObject getMallocID(dev.civl.sarl.IF.expr.SymbolicExpression pointer)

The parameter "pointer" must be a returned value of heapMemUnit(SymbolicExpression)

Given a pointer p to a memory heap, returns the malloc ID of the memory heap.

Parameters:

pointer -

Returns:

symbolicArrayToConcreteArray

dev.civl.sarl.IF.expr.SymbolicExpression[] symbolicArrayToConcreteArray(dev.civl.sarl.IF.expr.SymbolicExpression array)

Convert an array type symbolic expression with ARRAY operator to a concrete Java array.

Parameters:

array - the symbolic expression with ARRAY operator

Returns:

the converted Java array

isConcretePointer

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

Tests if the given symbolic expression is a concrete pointer value. A symbolic expression is a concrete pointer value iff the expression has CIVLTypeFactory.pointerSymbolicType() and the expression's operator is SymbolicExpression.SymbolicOperator.TUPLE and the arguments of the Tuple are respectively instances of: IntObject, SymbolicExpression (of Scope type), ReferenceExpression

Parameters:

pointer - a symbolic expression that will be tested if it is a concrete pointer value

Returns:

true iff the given symbolic expression satisfies the description above

freshBoundVariableFor

dev.civl.sarl.IF.expr.SymbolicConstant freshBoundVariableFor(dev.civl.sarl.IF.type.SymbolicType type,
 dev.civl.sarl.IF.expr.SymbolicExpression... expressions)

Creating a bound variable of the given "type", which is an instance of SymbolicConstant, whose name has no conflict with any other symbolic constants in the given set of "expressions".

Parameters:

type - the type of the returning bound variable

expressions - a set of expressions in the scope of the returning bound variable

Returns:

a bound variable of the given "type" whose name has no conflict with any other symbolic constants in the given set of "expressions".

freshBoundVariablesFor

List<dev.civl.sarl.IF.expr.SymbolicConstant> freshBoundVariablesFor(int num,
 dev.civl.sarl.IF.type.SymbolicType type,
 dev.civl.sarl.IF.expr.SymbolicExpression... expressions)

getValueSetUtility

ValueSetUtility getValueSetUtility()

makeFunctionPointer

dev.civl.sarl.IF.expr.SymbolicExpression makeFunctionPointer(int dyscopeID,
 int fid)

nullFunctionPointer

dev.civl.sarl.IF.expr.SymbolicExpression nullFunctionPointer()