CommonSymbolicUtility.java
package dev.civl.mc.dynamic.common;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.BitSet;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;
import java.util.Stack;
import java.util.stream.Collectors;
import dev.civl.mc.dynamic.IF.SymbolicUtility;
import dev.civl.mc.dynamic.IF.ValueSetUtility;
import dev.civl.mc.dynamic.common.HeapAnalyzer.CIVLMemoryBlock;
import dev.civl.mc.model.IF.CIVLInternalException;
import dev.civl.mc.model.IF.CIVLSource;
import dev.civl.mc.model.IF.CIVLTypeFactory;
import dev.civl.mc.model.IF.CIVLUnimplementedFeatureException;
import dev.civl.mc.model.IF.ModelFactory;
import dev.civl.mc.state.IF.StateFactory;
import dev.civl.mc.util.IF.Pair;
import dev.civl.sarl.IF.Reasoner;
import dev.civl.sarl.IF.SARLException;
import dev.civl.sarl.IF.SymbolicUniverse;
import dev.civl.sarl.IF.ValidityResult.ResultType;
import dev.civl.sarl.IF.expr.ArrayElementReference;
import dev.civl.sarl.IF.expr.BooleanExpression;
import dev.civl.sarl.IF.expr.NTReferenceExpression;
import dev.civl.sarl.IF.expr.NumericExpression;
import dev.civl.sarl.IF.expr.NumericSymbolicConstant;
import dev.civl.sarl.IF.expr.ReferenceExpression;
import dev.civl.sarl.IF.expr.SymbolicConstant;
import dev.civl.sarl.IF.expr.SymbolicExpression;
import dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator;
import dev.civl.sarl.IF.expr.TupleComponentReference;
import dev.civl.sarl.IF.expr.UnionMemberReference;
import dev.civl.sarl.IF.number.IntegerNumber;
import dev.civl.sarl.IF.object.IntObject;
import dev.civl.sarl.IF.object.NumberObject;
import dev.civl.sarl.IF.object.SymbolicObject;
import dev.civl.sarl.IF.object.SymbolicObject.SymbolicObjectKind;
import dev.civl.sarl.IF.object.SymbolicSequence;
import dev.civl.sarl.IF.type.SymbolicArrayType;
import dev.civl.sarl.IF.type.SymbolicCompleteArrayType;
import dev.civl.sarl.IF.type.SymbolicTupleType;
import dev.civl.sarl.IF.type.SymbolicType;
import dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind;
import dev.civl.sarl.IF.type.SymbolicTypeSequence;
import dev.civl.sarl.IF.type.SymbolicUnionType;
public class CommonSymbolicUtility implements SymbolicUtility {
/* *************************** Instance Fields ************************* */
/**
* Symbolic universe for operations on symbolic expressions.
*/
private SymbolicUniverse universe;
/**
* The type factory of the CIVL model.
*/
private CIVLTypeFactory typeFactory;
/**
* Integer object 0.
*/
private IntObject zeroObj;
/**
* Integer object 1.
*/
private IntObject oneObj;
/**
* Integer object 2.
*/
private IntObject twoObj;
/**
* Integer 0.
*/
private NumericExpression zero;
/**
* Integer 1.
*/
private NumericExpression one;
/**
* Symbolic dynamic type.
*/
private SymbolicTupleType dynamicType;
/**
* The symbolic expression of boolean false.
*/
private BooleanExpression falseValue;
/**
* The symbolic expression of boolean true.
*/
private BooleanExpression trueValue;
/**
* The symbolic expression of NULL pointer.
*/
private SymbolicExpression nullPointer;
/**
* The symbolic expression of undefined pointer, i.e., a pointer that has been
* deallocated.
*/
private SymbolicExpression undefinedPointer;
/**
* The heap analyzer for heap related semantics.
*/
private HeapAnalyzer heapAnalyzer;
/**
* The symbolic pointer type.
*/
private SymbolicTupleType pointerType;
private final static String abstractGuard = "_guard_";
private SymbolicType stringType;
private SymbolicTupleType functionPointerType;
private SymbolicExpression nullFunctionPointer;
private StateFactory stateFactory;
/* ***************************** Constructor *************************** */
/**
* creates a new instance of symbolic utility.
*
* @param universe the symbolic universe to be used by the symbolic utility.
* @param modelFactory the model factory to be used by the symbolic utility.
*/
public CommonSymbolicUtility(SymbolicUniverse universe, ModelFactory modelFactory, StateFactory stateFactory) {
this.stateFactory = stateFactory;
this.universe = universe;
this.typeFactory = modelFactory.typeFactory();
this.heapAnalyzer = new HeapAnalyzer(stateFactory, universe, this);
dynamicType = typeFactory.dynamicSymbolicType();
this.zeroObj = universe.intObject(0);
this.oneObj = universe.intObject(1);
this.twoObj = universe.intObject(2);
zero = universe.integer(0);
one = universe.integer(1);
this.falseValue = universe.falseExpression();
this.trueValue = universe.trueExpression();
this.pointerType = this.typeFactory.pointerSymbolicType();
this.functionPointerType = this.typeFactory.functionPointerSymbolicType();
this.nullPointer = makePointer(-1, -1, universe.identityReference());
this.nullFunctionPointer = makeFunctionPointer(-1, -1);
this.undefinedPointer = modelFactory.undefinedValue(typeFactory.pointerSymbolicType());
this.stringType = universe.arrayType(universe.characterType());
}
/* *********************** Package-Private Methods ********************* */
/**
* Returns the list of ancestor references of a given reference expressions, in
* the bottom-up order, i.e., the first element of the list will be the parent
* of the reference.
*
* @param ref The reference expression whose ancestors are to be computed.
* @return the list ancestor references of the given reference.
*/
List<ReferenceExpression> ancestorsOfRef(ReferenceExpression ref) {
if (ref.isIdentityReference())
return new ArrayList<>();
else {
List<ReferenceExpression> result;
result = ancestorsOfRef(((NTReferenceExpression) ref).getParent());
result.add(ref);
return result;
}
}
/* ********************** Private Methods ************************** */
/**
* Get the element in literal domain pointed by the given index.
*
* @param domValue The symbolic expression of the domain
* @param index The index points to the position of the returned element
* @return The element in literal domain pointed by the given index
*/
private SymbolicExpression getEleInLiteralDomain(SymbolicExpression literalDom, int index) {
SymbolicExpression element;
try {
element = universe.arrayRead(literalDom, universe.integer(index));
} catch (SARLException e) {
throw new CIVLInternalException("read literal domain out of bound", (CIVLSource) null);
}
return element;
}
/**
* Returns the size of a given regular range.
*
* @param range The regular range whose size is to be computed.
* @return the size of the given regular range.
*/
private NumericExpression getRegRangeSize(SymbolicExpression range) {
NumericExpression low = (NumericExpression) universe.tupleRead(range, this.zeroObj);
NumericExpression high = (NumericExpression) universe.tupleRead(range, oneObj);
NumericExpression step = (NumericExpression) universe.tupleRead(range, this.twoObj);
NumericExpression size = universe.subtract(high, low);
NumericExpression remainder;
BooleanExpression claim = universe.lessThan(step, zero);
ResultType resultType = universe.reasoner(this.trueValue).valid(claim).getResultType();
if (resultType == ResultType.YES) {
step = universe.minus(step);
size = universe.minus(size);
}
remainder = universe.modulo(size, step);
size = universe.subtract(size, remainder);
size = universe.divide(size, step);
size = universe.add(size, this.one);
return size;
}
/**
* Are the two given references disjoint?
*
* @param ref1 The first reference expression.
* @param ref2 The second reference expression.
* @return True iff the two given references do NOT have any intersection.
*/
private boolean isDisjoint(ReferenceExpression ref1, ReferenceExpression ref2) {
List<ReferenceExpression> ancestors1, ancestors2;
int numAncestors1, numAncestors2, minNum;
ancestors1 = this.ancestorsOfRef(ref1);
ancestors2 = this.ancestorsOfRef(ref2);
numAncestors1 = ancestors1.size();
numAncestors2 = ancestors2.size();
minNum = numAncestors1 <= numAncestors2 ? numAncestors1 : numAncestors2;
for (int i = 0; i < minNum; i++) {
ReferenceExpression ancestor1 = ancestors1.get(i), ancestor2 = ancestors2.get(i);
if (!ancestor1.equals(ancestor2))
return true;
}
return false;
}
/**
* Is the given reference applicable to the specified symbolic type?
*
* @param ref The reference expression to be checked.
* @param type The symbolic type specified.
* @return True iff the given reference is applicable to the specified symbolic
* type
*/
private boolean isValidRefOfType(ReferenceExpression ref, SymbolicType type) {
// sub-references are ordered starting from the IdentityReference
LinkedList<ReferenceExpression> subRefOrderedSet = new LinkedList<>();
subRefOrderedSet.addFirst(ref);
while (ref instanceof NTReferenceExpression) {
ReferenceExpression parent = ((NTReferenceExpression) ref).getParent();
subRefOrderedSet.addFirst(parent);
ref = parent;
}
ReferenceExpression subRef;
SymbolicType subType = type;
// Check type against references:
while (!subRefOrderedSet.isEmpty()) {
subRef = subRefOrderedSet.removeFirst();
switch (subRef.referenceKind()) {
case ARRAY_ELEMENT:
if (subType.typeKind() == SymbolicTypeKind.ARRAY) {
subType = ((SymbolicArrayType) subType).elementType();
continue;
} else
return false;
case IDENTITY:
continue;
case TUPLE_COMPONENT:
if (subType.typeKind() == SymbolicTypeKind.TUPLE) {
int fieldIdx = ((TupleComponentReference) subRef).getIndex().getInt();
SymbolicTypeSequence fieldTypes = ((SymbolicTupleType) subType).sequence();
if (fieldTypes.numTypes() <= fieldIdx)
return false;
subType = fieldTypes.getType(fieldIdx);
continue;
} else
return false;
case UNION_MEMBER:
if (subType.typeKind() == SymbolicTypeKind.UNION) {
int fieldIdx = ((UnionMemberReference) subRef).getIndex().getInt();
SymbolicTypeSequence fieldTypes = ((SymbolicUnionType) subType).sequence();
if (fieldTypes.numTypes() <= fieldIdx)
return false;
subType = fieldTypes.getType(fieldIdx);
continue;
} else
return false;
default:
return false;
}
}
return true;
}
/**
* Combines two references by using one as the parent of the other.
*
* @param parent The reference to be used as the parent.
* @param ref The reference to be used as the base.
* @return A new reference which is the combination of the given two references.
*/
private ReferenceExpression makeParentOf(ReferenceExpression parent, ReferenceExpression ref) {
if (ref.isIdentityReference())
return parent;
else {
ReferenceExpression myParent = makeParentOf(parent, ((NTReferenceExpression) ref).getParent());
if (ref.isArrayElementReference())
return universe.arrayElementReference(myParent, ((ArrayElementReference) ref).getIndex());
else if (ref.isTupleComponentReference())
return universe.tupleComponentReference(myParent, ((TupleComponentReference) ref).getIndex());
else
return universe.unionMemberReference(myParent, ((UnionMemberReference) ref).getIndex());
}
}
/**
* Computes the components contained by a given reference expression.
*
* @param ref The reference expression whose components are to be computed.
* @return The components of the reference.
*/
private List<ReferenceExpression> referenceComponents(ReferenceExpression ref) {
List<ReferenceExpression> components = new ArrayList<>();
if (!ref.isIdentityReference()) {
components.add(ref);
components.addAll(referenceComponents(((NTReferenceExpression) ref).getParent()));
}
return components;
}
/**
* Checks if the given value in a range has a subsequence. e.g. range: from 0 to
* 10 step 2. Given a value 8 and it has a subsequence 10.
*
* @param range
* @param value
* @return
*/
private BooleanExpression rangeHasNext(SymbolicExpression range, SymbolicExpression value) {
NumericExpression step = this.getStepOfRegularRange(range);
SymbolicExpression next = universe.add((NumericExpression) value, step);
return this.isInRange(next, range);
}
/* ********************* Methods from SymbolicUtility ******************* */
/**
* Given a symbolic expression of type array of char, returns a string
* representation. If it is a concrete array of char consisting of concrete
* characters, this will be the obvious string. Otherwise the result is
* something readable but unspecified.
*/
@Override
public StringBuffer charArrayToString(CIVLSource source, SymbolicExpression charArray, int startIndex,
boolean forPrint) {
StringBuffer result = new StringBuffer();
int numChars = charArray.numArguments();
if (charArray.operator() != SymbolicOperator.ARRAY)
throw new CIVLUnimplementedFeatureException("extracting string from a non-concrete array of characters",
source);
// assert charArray.operator() == SymbolicOperator.ARRAY;
// ignoring the '\0' at the end of the string.
for (int j = startIndex; j < numChars; j++) {
SymbolicExpression charExpr = (SymbolicExpression) charArray.argument(j);
Character theChar = universe.extractCharacter(charExpr);
if (theChar == null) {
result.append(charArray);
return result;
// throw new CIVLUnimplementedFeatureException(
// "non-concrete character in string at position " + j,
// source);
}
// if (theChar != '\0') {
if (forPrint) {
String theCharToString;
switch (theChar) {
case '\0':
theCharToString = "\0";
break;
case '\u000C':
theCharToString = "\\f";
break;
case '\u0007':
theCharToString = "\\a";
break;
case '\b':
theCharToString = "\\b";
break;
case '\n':
theCharToString = "\\n";
break;
case '\t':
theCharToString = "\\t";
break;
case '\r':
theCharToString = "\\r";
break;
default:
theCharToString = theChar.toString();
}
result.append(theCharToString);
} else {
result.append(theChar);
}
// }
}
return result;
}
/**
* A pointer can be only concrete for the current implementation of CIVL,
* because the only way to make one is through <code>$malloc</code> or
* <code>&</code>.
*/
@Override
public BooleanExpression contains(SymbolicExpression pointer1, SymbolicExpression pointer2) {
ReferenceExpression ref1 = (ReferenceExpression) universe.tupleRead(pointer1, twoObj);
ReferenceExpression ref2 = (ReferenceExpression) universe.tupleRead(pointer2, twoObj);
SymbolicExpression scope1 = universe.tupleRead(pointer1, zeroObj);
SymbolicExpression scope2 = universe.tupleRead(pointer2, zeroObj);
SymbolicExpression vid1 = universe.tupleRead(pointer1, oneObj);
SymbolicExpression vid2 = universe.tupleRead(pointer2, oneObj);
List<ReferenceExpression> refComps1 = new ArrayList<>();
List<ReferenceExpression> refComps2 = new ArrayList<>();
int numRefs1, numRefs2, offset;
BooleanExpression result = this.trueValue;
if (ref1.isIdentityReference() && ref2.isIdentityReference()) {
return universe.equals(ref1, ref2);
}
if (ref2.isIdentityReference() // second contains first
|| universe.equals(scope1, scope2).isFalse() // different scope
// id
|| universe.equals(vid1, vid2).isFalse()) // different vid
return this.falseValue;
if (ref1.isIdentityReference() && !ref2.isIdentityReference())
return this.trueValue;
refComps1 = referenceComponents(ref1);
refComps2 = referenceComponents(ref2);
numRefs1 = refComps1.size();
numRefs2 = refComps2.size();
if (numRefs1 > numRefs2)
return this.falseValue;
offset = numRefs2 - numRefs1;
for (int i = offset; i < numRefs1; i++) {
result = universe.and(result, universe.equals(refComps1.get(i), refComps2.get(i + offset)));
}
return result;
}
@Override
public int extractInt(CIVLSource source, NumericExpression expression) {
if (expression.operator() == SymbolicOperator.CONCRETE) {
SymbolicObject object = expression.argument(0);
if (object.symbolicObjectKind() == SymbolicObjectKind.NUMBER)
return ((IntegerNumber) ((NumberObject) object).getNumber()).intValue();
}
throw new CIVLInternalException("Unable to extract concrete int from " + expression, source);
}
@Override
public int extractIntField(CIVLSource source, SymbolicExpression tuple, IntObject fieldIndex) {
NumericExpression field = (NumericExpression) universe.tupleRead(tuple, fieldIndex);
return this.extractInt(source, field);
}
@Override
public int getArrayIndex(CIVLSource source, SymbolicExpression pointer) throws CIVLInternalException {
int int_arrayIndex;
if (pointer.type() instanceof SymbolicArrayType) {
int_arrayIndex = 0;
} else {
ArrayElementReference arrayRef;
NumericExpression arrayIndex;
try {
arrayRef = (ArrayElementReference) getSymRef(pointer);
} catch (ClassCastException e) {
throw new CIVLInternalException("pointer is not a array element reference", source);
}
arrayIndex = arrayRef.getIndex();
int_arrayIndex = extractInt(source, arrayIndex);
}
return int_arrayIndex;
}
@Override
public SymbolicExpression getScopeValue(SymbolicExpression pointer) {
return universe.tupleRead(pointer, zeroObj);
}
@Override
public ReferenceExpression getSymRef(SymbolicExpression pointer) {
SymbolicExpression result = universe.tupleRead(pointer, twoObj);
assert result instanceof ReferenceExpression;
return (ReferenceExpression) result;
}
@Override
public SymbolicExpression setSymRef(SymbolicExpression pointer, ReferenceExpression symRef) {
return universe.tupleWrite(pointer, twoObj, symRef);
}
@Override
public int getVariableId(CIVLSource source, SymbolicExpression pointer) {
return extractIntField(source, pointer, oneObj);
}
@Override
public SymbolicExpression heapMemUnit(SymbolicExpression pointer) {
return this.heapAnalyzer.heapMemUnit(pointer);
}
@Override
public SymbolicConstant invalidHeapObject(SymbolicType heapObjectType) {
return heapAnalyzer.invalidHeapObject(heapObjectType);
}
@Override
public boolean isDisjointWith(SymbolicExpression pointer1, SymbolicExpression pointer2) {
if (pointer1.equals(pointer2))
return false;
{
SymbolicExpression scope1 = universe.tupleRead(pointer1, zeroObj),
var1 = universe.tupleRead(pointer1, oneObj);
SymbolicExpression scope2 = universe.tupleRead(pointer2, zeroObj),
var2 = universe.tupleRead(pointer2, oneObj);
ReferenceExpression ref1 = (ReferenceExpression) universe.tupleRead(pointer1, twoObj);
ReferenceExpression ref2 = (ReferenceExpression) universe.tupleRead(pointer2, twoObj);
if (!scope1.equals(scope2))
return true;
if (!var1.equals(var2))
return true;
if (ref1.equals(ref2))
return false;
return isDisjoint(ref1, ref2);
}
}
@Override
public boolean isEmptyHeap(SymbolicExpression heapValue) {
return heapAnalyzer.isEmptyHeap(heapValue);
}
@Override
public boolean isMallocPointer(CIVLSource source, SymbolicExpression pointer) {
return heapAnalyzer.isHeapAtomicObjectPointer(source, pointer);
}
@Override
public boolean isInitialized(SymbolicExpression value) {
if (value.isNull())
return false;
return true;
}
@Override
public BooleanExpression isInRange(SymbolicExpression value, SymbolicExpression range) {
SymbolicExpression high = universe.tupleRead(range, oneObj);
SymbolicExpression step = universe.tupleRead(range, twoObj);
BooleanExpression positiveStep = universe.lessThan(zero, (NumericExpression) step);
BooleanExpression negativeStep = universe.lessThan((NumericExpression) step, zero);
BooleanExpression positiveStepResult = universe.and(positiveStep,
universe.lessThanEquals((NumericExpression) value, (NumericExpression) high));
BooleanExpression negativeStepResult = universe.and(negativeStep,
universe.lessThanEquals((NumericExpression) high, (NumericExpression) value));
if (positiveStep.isTrue())
return universe.lessThanEquals((NumericExpression) value, (NumericExpression) high);
if (negativeStep.isTrue())
return universe.lessThanEquals((NumericExpression) high, (NumericExpression) value);
return universe.or(positiveStepResult, negativeStepResult);
}
@Override
public BooleanExpression isInRange(NumericExpression value, NumericExpression low, NumericExpression upper,
NumericExpression step) {
return universe.and(Arrays.asList(universe.lessThanEquals(low, value), universe.lessThan(value, upper),
universe.equals(universe.modulo(universe.subtract(value, low), step), zero)));
}
@Override
public boolean isInvalidHeapObject(SymbolicExpression heapObject) {
return heapAnalyzer.isInvalidHeapObject(heapObject);
}
@Override
public boolean isNullPointer(SymbolicExpression pointer) {
return universe.equals(this.nullPointer, pointer).isTrue();
}
@Override
public boolean isPointerToHeap(SymbolicExpression pointer) {
return heapAnalyzer.isPointerToHeap(pointer);
}
@Override
public boolean isValidRefOf(ReferenceExpression ref, SymbolicType objectValueType) {
return isValidRefOfType(ref, objectValueType);
}
@Override
public SymbolicExpression makePointer(int scopeId, int varId, ReferenceExpression symRef) {
SymbolicExpression scopeField = stateFactory.scopeValue(scopeId);
SymbolicExpression varField = universe.integer(varId);
SymbolicExpression result = universe.tuple(this.pointerType,
Arrays.asList(new SymbolicExpression[] { scopeField, varField, symRef }));
return result;
}
@Override
public SymbolicExpression makePointer(SymbolicExpression oldPointer, ReferenceExpression symRef) {
return universe.tupleWrite(oldPointer, this.twoObj, symRef);
}
@Override
public SymbolicExpression extendPointer(SymbolicExpression objectPointer, ReferenceExpression reference) {
ReferenceExpression objRef = (ReferenceExpression) universe.tupleRead(objectPointer, twoObj);
SymbolicExpression scope = universe.tupleRead(objectPointer, zeroObj);
SymbolicExpression vid = universe.tupleRead(objectPointer, oneObj);
if (!objRef.isIdentityReference())
reference = makeParentOf(objRef, reference);
return universe.tuple(pointerType, Arrays.asList(scope, vid, reference));
}
@Override
public SymbolicExpression newArray(BooleanExpression context, SymbolicType elementValueType,
NumericExpression length, SymbolicExpression eleValue) {
Reasoner reasoner = universe.reasoner(context);
IntegerNumber length_number = (IntegerNumber) reasoner.extractNumber(length);
if (length_number != null) {
int length_int = length_number.intValue();
List<SymbolicExpression> values = new ArrayList<>(length_int);
for (int i = 0; i < length_int; i++)
values.add(eleValue);
return universe.array(elementValueType, values);
} else {
NumericSymbolicConstant index = (NumericSymbolicConstant) universe
.symbolicConstant(universe.stringObject("i"), universe.integerType());
SymbolicExpression arrayEleFunction = universe.lambda(index, eleValue);
SymbolicCompleteArrayType arrayValueType = universe.arrayType(elementValueType, length);
return universe.arrayLambda(arrayValueType, arrayEleFunction);
}
}
@Override
public SymbolicExpression nullPointer() {
return this.nullPointer;
}
@Override
public SymbolicExpression parentPointer(SymbolicExpression pointer) {
ReferenceExpression symRef = getSymRef(pointer);
assert !symRef.isNullReference() && !symRef.isIdentityReference();
return setSymRef(pointer, ((NTReferenceExpression) symRef).getParent());
}
@Override
public ReferenceExpression referenceOfPointer(SymbolicExpression pointer) {
ReferenceExpression ref = (ReferenceExpression) universe.tupleRead(pointer, twoObj);
if (this.isPointerToHeap(pointer)) {
Pair<ReferenceExpression, Integer> refResult = heapAnalyzer.heapReference(ref, true);
if (refResult.right == 3)
return universe.identityReference();
else
return refResult.left;
} else
return ref;
}
@Override
public ReferenceExpression referenceToHeapMemUnit(SymbolicExpression pointer) {
return this.heapAnalyzer.referenceToHeapMemUnit(pointer);
}
@Override
public SymbolicExpression undefinedPointer() {
return this.undefinedPointer;
}
@Override
public ReferenceExpression makeArrayElementReference(ReferenceExpression arrayReference,
NumericExpression[] newIndices) {
int dimension = newIndices.length;
ReferenceExpression newRef;
newRef = arrayReference;
for (int i = 0; i < dimension; i++) {
newRef = universe.arrayElementReference(newRef, newIndices[i]);
}
return newRef;
}
/* *********************** Package-Private Methods ********************* */
@Override
public NumericExpression[] arraySlicesSizes(NumericExpression[] array_extents) {
int dim = array_extents.length;
NumericExpression[] sliceSizes = new NumericExpression[dim];
NumericExpression sliceSize = one;
for (int i = dim; --i >= 0;) {
sliceSizes[i] = sliceSize;
sliceSize = universe.multiply(sliceSize, array_extents[i]);
}
return sliceSizes;
}
@Override
public NumericExpression[] arrayDimensionExtents(SymbolicCompleteArrayType arrayType) {
int dimension, i = 0;
NumericExpression[] extents;
dimension = arrayType.dimensions();
extents = new NumericExpression[dimension];
do {
extents[i++] = arrayType.extent();
if (i < dimension)
arrayType = (SymbolicCompleteArrayType) arrayType.elementType();
else
break;
} while (true);
return extents;
}
@Override
public SymbolicExpression arrayRootPtr(SymbolicExpression arrayPtr) {
SymbolicExpression arrayRootPtr = arrayPtr;
if (heapAnalyzer.isPointerToHeap(arrayPtr)) {
// Since the heap is modeled as a tuple of array of array of T, the
// parent searching must stop once the pointer already points to the
// first element of an heap memory block (i.e. the block of memory
// allocated by one malloc call).
while (getSymRef(arrayRootPtr).isArrayElementReference() && !isPointer2MemoryBlock(arrayRootPtr))
arrayRootPtr = parentPointer(arrayRootPtr);
return arrayRootPtr;
} else {
while (getSymRef(arrayRootPtr).isArrayElementReference())
arrayRootPtr = parentPointer(arrayRootPtr);
return arrayRootPtr;
}
}
@Override
public NumericExpression[] extractArrayIndicesFrom(SymbolicExpression pointerToArrayElement) {
Stack<NumericExpression> tmpStack = new Stack<>();
NumericExpression[] indices;
ReferenceExpression ref = getSymRef(pointerToArrayElement);
int size;
if (!heapAnalyzer.isPointerToHeap(pointerToArrayElement))
while (ref.isArrayElementReference()) {
ArrayElementReference tmpEleRef = (ArrayElementReference) ref;
tmpStack.push(tmpEleRef.getIndex());
ref = tmpEleRef.getParent();
}
else {
SymbolicExpression tmpPointer = pointerToArrayElement;
while (ref.isArrayElementReference() && !isPointer2MemoryBlock(tmpPointer)) {
ArrayElementReference tmpEleRef = (ArrayElementReference) ref;
tmpStack.push(tmpEleRef.getIndex());
ref = tmpEleRef.getParent();
tmpPointer = setSymRef(tmpPointer, ref);
}
}
size = tmpStack.size();
indices = new NumericExpression[size];
for (int i = 0; !tmpStack.isEmpty();)
indices[i++] = tmpStack.pop();
return indices;
}
/*
* ************************ Domain Operations ****************************
*/
@Override
public Iterator<List<SymbolicExpression>> getDomainIterator(SymbolicExpression domain) {
Iterator<List<SymbolicExpression>> domIterator;
SymbolicExpression domainUnionField = universe.tupleRead(domain, twoObj);
NumericExpression dim = (NumericExpression) universe.tupleRead(domain, zeroObj);
final int concreteDim = ((IntegerNumber) universe.extractNumber(dim)).intValue();
if (isRectangularDomain(domain)) {
final SymbolicExpression recDomainField = universe.unionExtract(zeroObj, domainUnionField);
final List<SymbolicExpression> domStartPos = this.getDomainInit(domain);
// anonymous class of iterator
domIterator = new Iterator<List<SymbolicExpression>>() {
private List<SymbolicExpression> startPos = domStartPos;
private List<SymbolicExpression> currentPos = null;
private SymbolicExpression recDom = recDomainField;
private int dim = concreteDim;
@Override
public boolean hasNext() {
BooleanExpression hasNext = universe.falseExpression();
for (int i = 0; i < dim; i++) {
SymbolicExpression range = universe.arrayRead(recDom, universe.integer(i));
if (getRegRangeSize(range).isZero())
return false;
}
if (this.currentPos == null) {
return startPos != null;
} else {
for (int i = 0; i < this.dim; i++) {
SymbolicExpression range = universe.arrayRead(this.recDom, universe.integer(i));
BooleanExpression rangeIHasNext = rangeHasNext(range, currentPos.get(i));
hasNext = universe.or(hasNext, rangeIHasNext);
}
Boolean result = universe.extractBoolean(hasNext);
if (result == null) {
// TODO: Pass the source into this function.
throw new CIVLInternalException("The domain has to be concrete before iterating ",
(CIVLSource) null);
}
return result;
}
}
@Override
public List<SymbolicExpression> next() {
if (this.currentPos == null)
return (this.currentPos = this.startPos);
else {
this.currentPos = getNextInRectangularDomain(this.recDom, this.currentPos, this.dim);
return this.currentPos;
}
}
@Override
public void remove() {
throw new CIVLInternalException("Remove elements in domain is not support yet", (CIVLSource) null);
}
};
} else if (this.isLiteralDomain(domain)) {
final SymbolicExpression literalDomainField = universe.unionExtract(oneObj, domainUnionField);
// anonymous class of iterator
domIterator = new Iterator<List<SymbolicExpression>>() {
private int currentPos = -1;
private SymbolicExpression literalDom = literalDomainField;
private int literalDomainSize = ((IntegerNumber) universe.extractNumber(universe.length(literalDom)))
.intValue();
private int dim = concreteDim;
@Override
public boolean hasNext() {
NumericExpression domLength = universe.length(literalDom);
// array length can never be negative and here it also
// should always be concrete.
if (domLength.isZero())
return false;
else
return ((literalDomainSize > (currentPos + 1) && (currentPos + 1) >= 0));
}
@Override
public List<SymbolicExpression> next() {
SymbolicExpression element;
List<SymbolicExpression> literalElement = new LinkedList<>();
this.currentPos++;
element = getEleInLiteralDomain(this.literalDom, this.currentPos);
for (int i = 0; i < this.dim; i++) {
literalElement.add(universe.arrayRead(element, universe.integer(i)));
}
return literalElement;
}
@Override
public void remove() {
throw new CIVLInternalException("Remove elements in domain is not support yet", (CIVLSource) null);
}
};
} else {
throw new CIVLInternalException(
"$domain type other than rectangular domain or literal domain is not supported", (CIVLSource) null);
}
return domIterator;
}
@Override
public List<SymbolicExpression> getDomainInit(SymbolicExpression domValue) {
SymbolicExpression domainUnionField = universe.tupleRead(domValue, twoObj);
NumericExpression dim = (NumericExpression) universe.tupleRead(domValue, zeroObj);
int concreteDim = ((IntegerNumber) universe.extractNumber(dim)).intValue();
List<SymbolicExpression> varValues = new ArrayList<>(concreteDim);
if (this.isRectangularDomain(domValue)) {
SymbolicExpression recDomainField = universe.unionExtract(zeroObj, domainUnionField);
SymbolicExpression range;
if (universe.length(recDomainField).isZero())
return null;
for (int i = 0; i < concreteDim; i++) {
range = universe.arrayRead(recDomainField, universe.integer(i));
varValues.add(this.getLowOfRegularRange(range));
}
return varValues;
} else {
SymbolicExpression literalDomainField = universe.unionExtract(oneObj, domainUnionField);
if (universe.length(literalDomainField).isZero())
return null;
else {
SymbolicExpression firstElement = universe.arrayRead(literalDomainField, zero);
for (int i = 0; i < concreteDim; i++)
varValues.add(universe.arrayRead(firstElement, universe.integer(i)));
return varValues;
}
}
}
@Override
public boolean isLiteralDomain(SymbolicExpression domValue) {
// Domain type is a tuple type{dim, field, union{...}}
SymbolicType type = domValue.type();
NumericExpression unionField; // Indicates weather rectangular or
// literal
int concreteUnionField;
assert (type instanceof SymbolicTupleType);
// The following 2 casts should be safe as long as domValue has $domian
// type.
unionField = (NumericExpression) universe.tupleRead(domValue, oneObj);
concreteUnionField = ((IntegerNumber) universe.extractNumber(unionField)).intValue();
if (concreteUnionField == 1)
return true;
return false;
}
@Override
public NumericExpression getDomainSize(SymbolicExpression domain) {
SymbolicExpression domainUnionField; // union{rec,literal}
domainUnionField = universe.tupleRead(domain, twoObj);
if (this.isRectangularDomain(domain)) {
SymbolicExpression recDomainField; // array of ranges
NumericExpression size = universe.oneInt();// Init size
NumericExpression dim = (NumericExpression) universe.tupleRead(domain, zeroObj);
int concreteDim;
concreteDim = ((IntegerNumber) universe.extractNumber(dim)).intValue();
recDomainField = universe.unionExtract(zeroObj, domainUnionField);
for (int i = 0; i < concreteDim; i++) {
SymbolicExpression range = universe.arrayRead(recDomainField, universe.integer(i));
size = universe.multiply(size, this.getRegRangeSize(range));
}
return size;
} else if (this.isLiteralDomain(domain)) {
// literal domain is an array of array of integers. Also can be
// explained as array of elements(elements are arrays of integers).
SymbolicExpression literalDomainField = universe.unionExtract(oneObj, domainUnionField);
return universe.length(literalDomainField);
} else
throw new CIVLInternalException("The argument: 'domain' of the function getDomainSize() is incorrect",
(CIVLSource) null);
}
@Override
public SymbolicType getDomainElementType(SymbolicExpression domain) {
NumericExpression dim;
SymbolicArrayType domainElementType;
dim = (NumericExpression) universe.tupleRead(domain, zeroObj);
domainElementType = universe.arrayType(universe.integerType(), dim);
return domainElementType;
}
@Override
public boolean recDomainHasNext(SymbolicExpression recDomainUnion, int concreteDim,
List<SymbolicExpression> domElement) {
boolean hasNext = false;
SymbolicExpression range;
for (int i = 0; i < concreteDim; i++) {
boolean rangeHasNext = false;
range = universe.arrayRead(recDomainUnion, universe.integer(i));
rangeHasNext = rangeHasNext(range, domElement.get(i)).isTrue();
hasNext = (rangeHasNext | hasNext);
}
return hasNext;
}
@Override
public int literalDomainSearcher(SymbolicExpression literalDomain, List<SymbolicExpression> literalDomElement,
int dim) {
NumericExpression literalDomLength = universe.length(literalDomain);
int concreteLength;
concreteLength = ((IntegerNumber) universe.extractNumber(literalDomLength)).intValue();
for (int i = 0; i < concreteLength; i++) {
SymbolicExpression symElement = universe.arrayRead(literalDomain, universe.integer(i));
for (int j = 0; j < dim; j++) {
SymbolicExpression elementComp = universe.arrayRead(symElement, universe.integer(j));
if (elementComp.equals(literalDomElement.get(j)))
if (j == dim - 1) {
return i;
} else
continue;
else
break;
}
}
return -1;
}
@Override
public List<SymbolicExpression> getNextInRectangularDomain(SymbolicExpression recDom,
List<SymbolicExpression> varValues, int concreteDim) {
SymbolicExpression recDomainField = recDom;
SymbolicExpression range;
SymbolicExpression newValues[] = new SymbolicExpression[concreteDim];
for (int i = concreteDim - 1; i >= 0; i--) {
SymbolicExpression current = varValues.get(i);
BooleanExpression rangeHasNext;
range = universe.arrayRead(recDomainField, universe.integer(i));
rangeHasNext = rangeHasNext(range, current);
if (rangeHasNext.isTrue()) {
newValues[i] = universe.add((NumericExpression) current, this.getStepOfRegularRange(range));
for (int j = i - 1; j >= 0; j--) {
newValues[j] = varValues.get(j);
}
break;
} else {
newValues[i] = this.getLowOfRegularRange(range);
}
}
return Arrays.asList(newValues);
}
@Override
public boolean isEmptyDomain(SymbolicExpression domain, int dim, CIVLSource source) {
SymbolicExpression domUnion = universe.tupleRead(domain, twoObj);
if (this.isLiteralDomain(domain)) {
SymbolicExpression literalDom = universe.unionExtract(oneObj, domUnion);
NumericExpression domLength = universe.length(literalDom);
// array length can never be negative and here it also should always
// be concrete.
if (domLength.isZero())
return true;
else
return false;
} else if (this.isRectangularDomain(domain)) {
SymbolicExpression recDom = universe.unionExtract(zeroObj, domUnion);
for (int i = 0; i < dim; i++) {
SymbolicExpression range = universe.arrayRead(recDom, universe.integer(i));
if (!this.getRegRangeSize(range).isZero())
return false;
}
return true;
} else
throw new CIVLInternalException("A domain object is neither a rectangular domain nor a literal domain",
source);
}
@Override
public Pair<NumericExpression, NumericExpression> arithmeticIntDivide(NumericExpression dividend,
NumericExpression denominator) {
NumericExpression quotient, remainder;
assert dividend.type().isInteger();
assert denominator.type().isInteger();
quotient = universe.divide(dividend, denominator);
remainder = universe.subtract(dividend, universe.multiply(quotient, denominator));
return new Pair<>(quotient, remainder);
}
@Override
public SymbolicTupleType dynamicType() {
return this.dynamicType;
}
@Override
public boolean isRectangularDomain(SymbolicExpression domain) {
// a domain is the tuple (dimension, type, value)
return universe.tupleRead(domain, oneObj).isZero();
}
@Override
public boolean isRegularRange(SymbolicExpression range) {
if (range.type().toString().equals("$regular_range"))
return true;
return false;
}
@Override
public SymbolicExpression getRangeOfRectangularDomain(SymbolicExpression domain, int index) {
if (!isRectangularDomain(domain))
return null;
SymbolicExpression ranges = universe.unionExtract(zeroObj, universe.tupleRead(domain, twoObj));
return universe.arrayRead(ranges, universe.integer(index));
}
@Override
public NumericExpression getHighOfRegularRange(SymbolicExpression range) {
return (NumericExpression) universe.tupleRead(range, oneObj);
}
@Override
public NumericExpression getLowOfRegularRange(SymbolicExpression range) {
return (NumericExpression) universe.tupleRead(range, zeroObj);
}
@Override
public NumericExpression getStepOfRegularRange(SymbolicExpression range) {
return (NumericExpression) universe.tupleRead(range, twoObj);
}
@Override
public NumericExpression getDimensionOf(SymbolicExpression domain) {
return (NumericExpression) universe.tupleRead(domain, zeroObj);
}
@Override
public BooleanExpression[] getConjunctiveClauses(BooleanExpression clause) {
SymbolicOperator operator = clause.operator();
BooleanExpression[] result;
if (operator != SymbolicOperator.AND) {
result = new BooleanExpression[1];
result[0] = clause;
} else {
int numArgs = clause.numArguments();
result = new BooleanExpression[numArgs];
for (int i = 0; i < numArgs; i++) {
result[i] = (BooleanExpression) clause.argument(i);
}
}
return result;
}
@Override
public SymbolicExpression getAbstractGuardOfFunctionCall(String library, String function,
SymbolicExpression[] argumentValues) {
String functionName = abstractGuard + library + "_" + function;
List<SymbolicType> argumentTypes = new ArrayList<>();
SymbolicConstant abstractFunction;
SymbolicType functionType;
List<SymbolicExpression> argValues = new ArrayList<>(argumentValues.length + 1);
argumentTypes.add(this.stringType);
for (int i = 0; i < argumentValues.length; i++) {
argumentTypes.add(argumentValues[i].type());
}
functionType = universe.functionType(argumentTypes, universe.booleanType());
abstractFunction = universe.symbolicConstant(universe.stringObject(functionName), functionType);
argValues.add(universe.stringExpression(functionName));
for (int i = 0; i < argumentValues.length; i++) {
argValues.add(argumentValues[i]);
}
return universe.apply(abstractFunction, argValues);
}
@Override
public SymbolicExpression applyReverseFunction(String originalFunction, SymbolicExpression argument) {
if (argument.operator() == SymbolicOperator.APPLY) {
SymbolicConstant function = (SymbolicConstant) argument.argument(0);
SymbolicSequence<? extends SymbolicExpression> args = (SymbolicSequence<? extends SymbolicExpression>) argument
.argument(1);
if (args.size() == 1) {
if (function.name().getString().equals(originalFunction)) {
return args.get(0);
}
}
}
return null;
}
@Override
public BitSet range2BitSet(SymbolicExpression range, Reasoner reasoner) {
BitSet results = new BitSet();
if (range.isNumeric()) {
results.set(((IntegerNumber) reasoner.extractNumber((NumericExpression) range)).intValue());
} else {
// else it's range
NumericExpression high = getHighOfRegularRange(range);
NumericExpression low = getLowOfRegularRange(range);
NumericExpression step = getStepOfRegularRange(range);
int highInt, lowInt, stepInt;
highInt = ((IntegerNumber) reasoner.extractNumber((NumericExpression) high)).intValue();
lowInt = ((IntegerNumber) reasoner.extractNumber((NumericExpression) low)).intValue();
stepInt = ((IntegerNumber) reasoner.extractNumber((NumericExpression) step)).intValue();
for (int i = lowInt; i <= highInt; i += stepInt)
results.set(i);
}
return results;
}
public IntObject getMallocID(SymbolicExpression heapPointer) {
// As long as the argument "heapPointer" is a valid result of function
// #heapMemUnit, it must have the form
// ArrayELementReference<TupleComponentReference, a>, b>:
ReferenceExpression symref = getSymRef(heapPointer);
TupleComponentReference tupleRef = (TupleComponentReference) ((ArrayElementReference) symref).getParent();
return tupleRef.getIndex();
}
@Override
public SymbolicExpression nullFunctionPointer() {
return this.nullFunctionPointer;
}
@Override
public SymbolicExpression makeFunctionPointer(int dyscopeID, int fid) {
return universe.tuple(this.functionPointerType,
Arrays.asList(stateFactory.scopeValue(dyscopeID), universe.integer(fid)));
}
/* *************** methods for specific heap structures ************* */
@Override
public SymbolicExpression getPointer2MemoryBlock(SymbolicExpression heapPointer) {
while (!isPointer2MemoryBlock(heapPointer))
heapPointer = parentPointer(heapPointer);
return heapPointer;
}
@Override
public boolean isPointer2MemoryBlock(SymbolicExpression pointer) {
return heapAnalyzer.isPointer2MemoryBlock(pointer);
}
@Override
public boolean arePoint2SameMemoryBlock(SymbolicExpression ptr0, SymbolicExpression ptr1) {
assert isPointerToHeap(ptr0) && isPointerToHeap(ptr1);
CIVLMemoryBlock blk0 = heapAnalyzer.memoryBlock(ptr0);
CIVLMemoryBlock blk1 = heapAnalyzer.memoryBlock(ptr1);
return blk0.compare(blk1);
}
/* ********** end-of methods for specific heap structures ******** */
/* ********** end-of methods for specific heap structures ******** */
@Override
public SymbolicConstant freshBoundVariableFor(SymbolicType type, SymbolicExpression... exprs) {
return freshBoundVariablesForWorker(1, type, exprs).get(0);
}
@Override
public List<SymbolicConstant> freshBoundVariablesFor(int num, SymbolicType type, SymbolicExpression... exprs) {
return freshBoundVariablesForWorker(num, type, exprs);
}
// TODO: need a good way to get free bound variables when necessary
private List<SymbolicConstant> freshBoundVariablesForWorker(int num, SymbolicType type,
SymbolicExpression... exprs) {
Set<SymbolicConstant> symConsts = new HashSet<>();
Set<String> freeVarNames;
for (SymbolicExpression e : exprs)
symConsts.addAll(e.getFreeVars());
freeVarNames = symConsts.stream().map(c -> c.name().getString()).collect(Collectors.toSet());
String boundVarNamePrefix = "i";
int boundVarNameCounter = 0;
List<SymbolicConstant> boundVars = new LinkedList<>();
for (int i = 0; i < num; i++) {
while (freeVarNames.contains(boundVarNamePrefix + boundVarNameCounter))
boundVarNameCounter++;
String name = boundVarNamePrefix + boundVarNameCounter++;
boundVars.add(universe.symbolicConstant(universe.stringObject(name), type));
}
return boundVars;
}
@Override
public SymbolicExpression[] symbolicArrayToConcreteArray(SymbolicExpression array) {
NumericExpression numElements = universe.length(array);
IntegerNumber numElementsNumber = (IntegerNumber) universe.extractNumber(numElements);
assert array.operator() == SymbolicOperator.ARRAY
: "A symbolic " + "expression without ARRAY operator " + "cannot be converted to a concrete array.";
int numElementsInt = numElementsNumber.intValue();
SymbolicExpression results[] = new SymbolicExpression[numElementsInt];
for (int i = 0; i < numElementsInt; i++)
results[i] = (SymbolicExpression) array.argument(i);
return results;
}
// TODO: what is the point of all these checks? If the type
// is the pointer symbolic type, and the kind is tuple, the 3
// components must be expressions and they must have types
// integer (dynamic scope ID), integer (variable ID), reference type.
// Note this does not check that the two integer components are concrete.
@Override
public boolean isConcretePointer(SymbolicExpression pointer) {
if (pointer.type() != typeFactory.pointerSymbolicType())
return false;
if (pointer.operator() != SymbolicOperator.TUPLE)
return false;
if (pointer.argument(0).symbolicObjectKind() != SymbolicObjectKind.EXPRESSION)
return false;
if (((SymbolicExpression) pointer.argument(0)).type() != typeFactory.scopeSymbolicType())
return false;
if (pointer.argument(1).symbolicObjectKind() != SymbolicObjectKind.EXPRESSION)
return false;
if (((SymbolicExpression) pointer.argument(1)).type() != universe.integerType())
return false;
if (pointer.argument(2).symbolicObjectKind() != SymbolicObjectKind.EXPRESSION)
return false;
if (((SymbolicExpression) pointer.argument(2)).type() != universe.referenceType())
return false;
return true;
}
@Override
public ValueSetUtility getValueSetUtility() {
return new CommonValueSetUtility(universe, this);
}
}