CommonEvaluator.java
package edu.udel.cis.vsl.civl.semantics.common;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;
import edu.udel.cis.vsl.civl.dynamic.IF.SymbolicUtility;
//import edu.udel.cis.vsl.civl.kripke.IF.Enabler;
import edu.udel.cis.vsl.civl.log.IF.CIVLErrorLogger;
import edu.udel.cis.vsl.civl.log.IF.CIVLExecutionException;
import edu.udel.cis.vsl.civl.model.IF.AbstractFunction;
import edu.udel.cis.vsl.civl.model.IF.CIVLException;
import edu.udel.cis.vsl.civl.model.IF.CIVLException.Certainty;
import edu.udel.cis.vsl.civl.model.IF.CIVLException.ErrorKind;
import edu.udel.cis.vsl.civl.model.IF.CIVLFunction;
import edu.udel.cis.vsl.civl.model.IF.CIVLInternalException;
import edu.udel.cis.vsl.civl.model.IF.CIVLSource;
import edu.udel.cis.vsl.civl.model.IF.CIVLUnimplementedFeatureException;
import edu.udel.cis.vsl.civl.model.IF.ModelFactory;
import edu.udel.cis.vsl.civl.model.IF.Scope;
import edu.udel.cis.vsl.civl.model.IF.SystemFunction;
import edu.udel.cis.vsl.civl.model.IF.expression.AbstractFunctionCallExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.AddressOfExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.ArrayLiteralExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.BinaryExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.BinaryExpression.BINARY_OPERATOR;
import edu.udel.cis.vsl.civl.model.IF.expression.BooleanLiteralExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.BoundVariableExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.CastExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.CharLiteralExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.DereferenceExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.DerivativeCallExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.DomainGuardExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.DotExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.DynamicTypeOfExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.Expression;
import edu.udel.cis.vsl.civl.model.IF.expression.Expression.ExpressionKind;
import edu.udel.cis.vsl.civl.model.IF.expression.FunctionGuardExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.FunctionIdentifierExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.HereOrRootExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.InitialValueExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.IntegerLiteralExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.LHSExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.ProcnullExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.QuantifiedExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.RealLiteralExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.RecDomainLiteralExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.RegularRangeExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.ResultExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.ScopeofExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.SelfExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.SizeofExpressionExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.SizeofTypeExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.StructOrUnionLiteralExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.SubscriptExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.SystemGuardExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.UnaryExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.VariableExpression;
import edu.udel.cis.vsl.civl.model.IF.expression.WaitGuardExpression;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLArrayType;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLBundleType;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLCompleteArrayType;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLCompleteDomainType;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLDomainType;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLEnumType;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLHeapType;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLPointerType;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLPrimitiveType;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLPrimitiveType.PrimitiveTypeKind;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLStructOrUnionType;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLType;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLType.TypeKind;
import edu.udel.cis.vsl.civl.model.IF.type.StructOrUnionField;
import edu.udel.cis.vsl.civl.model.IF.variable.Variable;
import edu.udel.cis.vsl.civl.semantics.IF.Evaluation;
import edu.udel.cis.vsl.civl.semantics.IF.Evaluator;
import edu.udel.cis.vsl.civl.semantics.IF.LibraryEvaluator;
import edu.udel.cis.vsl.civl.semantics.IF.LibraryEvaluatorLoader;
import edu.udel.cis.vsl.civl.semantics.IF.LibraryLoaderException;
import edu.udel.cis.vsl.civl.semantics.IF.SymbolicAnalyzer;
import edu.udel.cis.vsl.civl.state.IF.ProcessState;
import edu.udel.cis.vsl.civl.state.IF.State;
import edu.udel.cis.vsl.civl.state.IF.StateFactory;
import edu.udel.cis.vsl.civl.state.IF.UnsatisfiablePathConditionException;
import edu.udel.cis.vsl.civl.util.IF.Pair;
import edu.udel.cis.vsl.civl.util.IF.Singleton;
import edu.udel.cis.vsl.civl.util.IF.Triple;
import edu.udel.cis.vsl.sarl.IF.Reasoner;
import edu.udel.cis.vsl.sarl.IF.SARLException;
import edu.udel.cis.vsl.sarl.IF.SymbolicUniverse;
import edu.udel.cis.vsl.sarl.IF.ValidityResult.ResultType;
import edu.udel.cis.vsl.sarl.IF.expr.ArrayElementReference;
import edu.udel.cis.vsl.sarl.IF.expr.BooleanExpression;
import edu.udel.cis.vsl.sarl.IF.expr.NumericExpression;
import edu.udel.cis.vsl.sarl.IF.expr.NumericSymbolicConstant;
import edu.udel.cis.vsl.sarl.IF.expr.OffsetReference;
import edu.udel.cis.vsl.sarl.IF.expr.ReferenceExpression;
import edu.udel.cis.vsl.sarl.IF.expr.SymbolicConstant;
import edu.udel.cis.vsl.sarl.IF.expr.SymbolicExpression;
import edu.udel.cis.vsl.sarl.IF.expr.SymbolicExpression.SymbolicOperator;
import edu.udel.cis.vsl.sarl.IF.expr.TupleComponentReference;
import edu.udel.cis.vsl.sarl.IF.number.IntegerNumber;
import edu.udel.cis.vsl.sarl.IF.number.NumberFactory;
import edu.udel.cis.vsl.sarl.IF.object.IntObject;
import edu.udel.cis.vsl.sarl.IF.object.StringObject;
import edu.udel.cis.vsl.sarl.IF.object.SymbolicObject;
import edu.udel.cis.vsl.sarl.IF.type.SymbolicArrayType;
import edu.udel.cis.vsl.sarl.IF.type.SymbolicCompleteArrayType;
import edu.udel.cis.vsl.sarl.IF.type.SymbolicFunctionType;
import edu.udel.cis.vsl.sarl.IF.type.SymbolicTupleType;
import edu.udel.cis.vsl.sarl.IF.type.SymbolicType;
import edu.udel.cis.vsl.sarl.IF.type.SymbolicUnionType;
import edu.udel.cis.vsl.sarl.collections.IF.SymbolicCollection;
import edu.udel.cis.vsl.sarl.collections.IF.SymbolicSequence;
import edu.udel.cis.vsl.sarl.number.Numbers;
/**
* An evaluator is used to evaluate expressions.
*
* @author Timothy K. Zirkel (zirkel)
* @author Manchun Zheng (zmanchun)
*
*/
public class CommonEvaluator implements Evaluator {
/* *************************** Instance Fields ************************* */
/**
* The library evaluator loader.
*/
private LibraryEvaluatorLoader libLoader;
/**
* An uninterpreted function used to evaluate "BigO" of an expression. It
* takes as input one expression of real type and return a real type,
* <code>real $O(real x)</code>.
*/
private SymbolicExpression bigOFunction;
/**
* TODO: clean up boundVariables, which becomes a "state" of the evaluator
* but it is not necessary. Possible solution: creates an evaluator worker<br>
* LinkedList used to store a stack of bound variables during evaluation of
* (possibly nested) quantified expressions. LinkedList is used instead of
* Stack because of its more intuitive iteration order.
*/
private LinkedList<SymbolicConstant> boundVariables = new LinkedList<>();
/**
* The symbolic bundle type.
*/
private SymbolicUnionType bundleType;
/**
* The dynamic heap type.
*/
private SymbolicTupleType heapType;
/**
* The identity reference expression.
*/
private ReferenceExpression identityReference;
/**
* The unique model factory used in the system.
*/
private ModelFactory modelFactory;
/**
* The symbolic expression of NULL expression, i.e., the undefined value.
*/
private SymbolicExpression nullExpression;
/**
* The unique real number factory used in the system.
*/
private NumberFactory numberFactory = Numbers.REAL_FACTORY;
/**
* The symbolic numeric expression of 1.
*/
private NumericExpression one;
/**
* The symbolic int object of 1.
*/
private IntObject oneObj;
/**
* The pointer value is a triple <s,v,r> where s identifies the dynamic
* scope, v identifies the variable within that scope, and r identifies a
* point within that variable. The type of s is scopeType, which is just a
* tuple wrapping a single integer which is the dynamic scope ID number. The
* type of v is integer; it is the (static) variable ID number for the
* variable in its scope. The type of r is ReferenceExpression from SARL.
*/
private SymbolicTupleType pointerType;
/**
* TODO make function pointer type normal pointer type.
*
* The function pointer value is a pair <s,n> where s identifies the dynamic
* scope, n identifies the name of the function that the pointer points to.
* The type of s is scopeType, which is just a tuple wrapping a single
* integer which is the dynamic scope ID number. The type of n is array of
* characters.
*/
private SymbolicTupleType functionPointerType;
/**
* An uninterpreted function used to evaluate "sizeof" on a type. It takes
* as input one expression of type dynamicType and returns an integer
* expression.
*/
private SymbolicExpression sizeofFunction;
/**
* The unique state factory used in the system.
*/
private StateFactory stateFactory;
/**
* The unique symbolic universe used in the system.
*/
private SymbolicUniverse universe;
/**
* The symbolic int object of 0.
*/
private IntObject zeroObj;
/**
* The symbolic int object of 2.
*/
private IntObject twoObj;
/**
* The symbolic numeric expression of 0 of integer type.
*/
private NumericExpression zero;
/**
* The symbolic numeric expression of 0 of real type.
*/
private NumericExpression zeroR;
/** The SARL character type. */
private SymbolicType charType;
/**
* The SARL character 0, i.e., '\0' or '\u0000', used as the
* "null character constant" in C.
*/
private SymbolicExpression nullCharExpr;
/**
* The symbolic utility for manipulations of symbolic expressions.
*/
private SymbolicUtility symbolicUtil;
/**
* The error logger to report errors.
*/
private CIVLErrorLogger errorLogger;
/**
* The abstract function for bitwise and.
*/
private SymbolicConstant bitAndFunc;
/**
* The abstract function for bitwise complement.
*/
private SymbolicConstant bitComplementFunc;
/**
* The abstract function for bitwise or.
*/
private SymbolicConstant bitOrFunc;
/**
* The abstract function for bitwise xor.
*/
private SymbolicConstant bitXorFunc;
/**
* The abstract function for bitwise left shift.
*/
private SymbolicConstant shiftLeftFunc;
/**
* The abstract function for bitwise right shift.
*/
private SymbolicConstant shiftRightFunc;
/**
* The symbolic numeric expression that has the value of either zero or one.
*/
private NumericExpression zeroOrOne;
/**
* The symbolic analyzer to be used.
*/
private SymbolicAnalyzer symbolicAnalyzer;
/* ***************************** Constructors ************************** */
/**
* Create a new instance of evaluator for evaluating expressions.
*
* @param modelFactory
* The model factory of the system.
* @param stateFactory
* The state factory of the system.
* @param loader
* The loader for library evaluators.
* @param symbolicUtil
* The symbolic utility.
* @param symbolicAnalyzer
* The symbolic analyzer used in the system.
* @param errorLogger
* The error logger for logging errors.
*/
public CommonEvaluator(ModelFactory modelFactory,
StateFactory stateFactory, LibraryEvaluatorLoader loader,
SymbolicUtility symbolicUtil, SymbolicAnalyzer symbolicAnalyzer,
CIVLErrorLogger errorLogger) {
this.libLoader = loader;
this.errorLogger = errorLogger;
this.symbolicUtil = symbolicUtil;
this.symbolicAnalyzer = symbolicAnalyzer;
this.modelFactory = modelFactory;
this.stateFactory = stateFactory;
this.universe = stateFactory.symbolicUniverse();
pointerType = modelFactory.pointerSymbolicType();
functionPointerType = modelFactory.functionPointerSymbolicType();
heapType = modelFactory.heapSymbolicType();
bundleType = modelFactory.bundleSymbolicType();
zeroObj = (IntObject) universe.canonic(universe.intObject(0));
oneObj = (IntObject) universe.canonic(universe.intObject(1));
twoObj = (IntObject) universe.canonic(universe.intObject(2));
identityReference = (ReferenceExpression) universe.canonic(universe
.identityReference());
zero = (NumericExpression) universe.canonic(universe.integer(0));
zeroR = (NumericExpression) universe.canonic(universe.zeroReal());
one = (NumericExpression) universe.canonic(universe.integer(1));
nullExpression = universe.nullExpression();
sizeofFunction = symbolicUtil.sizeofFunction();
bigOFunction = universe.symbolicConstant(
universe.stringObject("BIG_O"), universe.functionType(
new Singleton<SymbolicType>(universe.realType()),
universe.realType()));
bigOFunction = universe.canonic(bigOFunction);
charType = universe.characterType();
nullCharExpr = universe.canonic(universe.character('\u0000'));
this.bitAndFunc = universe.symbolicConstant(universe
.stringObject("bitand"), universe.functionType(
Arrays.asList(universe.integerType(), universe.integerType()),
universe.integerType()));
this.bitComplementFunc = universe.symbolicConstant(universe
.stringObject("bitcomplement"), universe.functionType(
Arrays.asList(universe.integerType(), universe.integerType()),
universe.integerType()));
this.bitOrFunc = universe.symbolicConstant(universe
.stringObject("bitor"), universe.functionType(
Arrays.asList(universe.integerType(), universe.integerType()),
universe.integerType()));
this.bitXorFunc = universe.symbolicConstant(universe
.stringObject("bitxor"), universe.functionType(
Arrays.asList(universe.integerType(), universe.integerType()),
universe.integerType()));
this.shiftLeftFunc = universe.symbolicConstant(universe
.stringObject("shiftleft"), universe.functionType(
Arrays.asList(universe.integerType(), universe.integerType()),
universe.integerType()));
this.shiftRightFunc = universe.symbolicConstant(universe
.stringObject("shiftright"), universe.functionType(
Arrays.asList(universe.integerType(), universe.integerType()),
universe.integerType()));
this.zeroOrOne = (NumericExpression) universe.symbolicConstant(
universe.stringObject("ZeroOrOne"), universe.integerType());
}
/* ************************** Private Methods ************************** */
/**
* Does the type contains some non-concrete state? e.g., int[N] where N is
* an input variable contains the non-concrete state N if N can't be
* simplified to a concrete value at the given state.
*
* @param state
* The current state
* @param pid
* The PID of the process that calls this method
* @param type
* The type to be checked
* @return true iff the type contains some non-concrete state.
* @throws UnsatisfiablePathConditionException
*/
@SuppressWarnings("unused")
private boolean hasNonConcreteState(State state, int pid, CIVLType type)
throws UnsatisfiablePathConditionException {
TypeKind kind = type.typeKind();
switch (kind) {
case ARRAY:
return true;
case COMPLETE_ARRAY: {
CIVLCompleteArrayType arrayType = (CIVLCompleteArrayType) type;
Expression extent = arrayType.extent();
Reasoner reasoner = universe.reasoner(state.getPathCondition());
Evaluation eval = this.evaluate(state, pid, extent);
IntegerNumber extent_num;
state = eval.state;
extent_num = (IntegerNumber) reasoner
.extractNumber((NumericExpression) eval.value);
if (extent_num == null)
return true;
else
return this.hasNonConcreteState(state, pid,
arrayType.elementType());
}
case BUNDLE:
return true;
case DOMAIN: {
// CIVLDomainType domainType = (CIVLDomainType) type;
//
// if (domainType.dimension() > 0)
// return false;
return false;
}
case ENUM:
return false;
case POINTER:
return false;
case PRIMITIVE:
return false;
case STRUCT_OR_UNION: {
CIVLStructOrUnionType strOrUnionType = (CIVLStructOrUnionType) type;
int numFields = strOrUnionType.numFields();
for (int i = 0; i < numFields; i++) {
CIVLType fieldType = strOrUnionType.getField(i).type();
if (this.hasNonConcreteState(state, pid, fieldType))
return true;
}
return false;
}
default:// FUNCTION/HEAP
return false;
}
}
/**
* Dereferences a pointer. Logs error when the dereference fails, like when
* the pointer is null.
*
* @param source
* Source code information for error report.
* @param state
* The state where the dereference happens.
* @param process
* The process name for error report.
* @param pointer
* The pointer to be dereferenced.
* @param checkOutput
* Is reading of output variable to be checked?
* @param analysisOnly
* Is this called from pointer reachability analysis?
* @return A possibly new state and the value of memory space pointed by the
* pointer.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation dereference(CIVLSource source, State state,
String process, SymbolicExpression pointer, boolean checkOutput,
boolean analysisOnly) throws UnsatisfiablePathConditionException {
if (pointer.operator() != SymbolicOperator.CONCRETE) {
CIVLExecutionException se = new CIVLExecutionException(
ErrorKind.UNDEFINED_VALUE, Certainty.PROVEABLE, process,
"Attempt to deference a pointer that is never initialized",
this.symbolicAnalyzer.stateToString(state), source);
errorLogger.reportError(se);
throw new UnsatisfiablePathConditionException();
} else if (symbolicUtil.isNullPointer(pointer)) {
// null pointer dereference
CIVLExecutionException se = new CIVLExecutionException(
ErrorKind.DEREFERENCE, Certainty.PROVEABLE, process,
"Attempt to deference a null pointer",
this.symbolicAnalyzer.stateToString(state), source);
errorLogger.reportError(se);
throw new UnsatisfiablePathConditionException();
} else {
try {
int sid = symbolicUtil.getDyscopeId(source, pointer);
if (sid < 0) {
errorLogger.logSimpleError(source, state, process,
symbolicAnalyzer.stateToString(state),
ErrorKind.DEREFERENCE,
"Attempt to dereference pointer into scope"
+ " which has been removed from state");
throw new UnsatisfiablePathConditionException();
} else {
int vid = symbolicUtil.getVariableId(source, pointer);
ReferenceExpression symRef = symbolicUtil
.getSymRef(pointer);
SymbolicExpression variableValue;
SymbolicExpression deref;
if (!analysisOnly && checkOutput) {
Variable variable = state.getDyscope(sid)
.lexicalScope().variable(vid);
if (variable.isOutput()) {
errorLogger.logSimpleError(source, state, process,
symbolicAnalyzer.stateToString(state),
ErrorKind.OUTPUT_READ,
"Attempt to read output variable "
+ variable.name().name());
throw new UnsatisfiablePathConditionException();
}
}
variableValue = state.getDyscope(sid).getValue(vid);
try {
deref = universe.dereference(variableValue, symRef);
} catch (SARLException e) {
errorLogger.logSimpleError(
source,
state,
process,
symbolicAnalyzer.stateToString(state),
ErrorKind.DEREFERENCE,
"Illegal pointer dereference: "
+ e.getMessage() + source.getSummary());
throw new UnsatisfiablePathConditionException();
}
return new Evaluation(state, deref);
}
} catch (CIVLInternalException e) {
CIVLExecutionException se = new CIVLExecutionException(
ErrorKind.DEREFERENCE, Certainty.MAYBE, process,
"Undefined pointer value?",
this.symbolicAnalyzer.stateToString(state), source);
errorLogger.reportError(se);
throw new UnsatisfiablePathConditionException();
}
}
}
/**
* Evaluates the dynamic type of a given CIVL type at a certain state. When
* the CIVL type has some state, e.g., an array type with a variable as the
* extent, the type needs to be evaluated.
*
* @param state
* The current state.
* @param pid
* The ID of the process where the computation happens.
* @param type
* The CIVL type to be evaluated for the dynamic type.
* @param source
* The source code element for error report.
* @param isDeclaration
* The flag denoting if the type is part of a variable/function
* declaration.
* @return The dynamic type of the given type.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation dynamicTypeOf(State state, int pid, CIVLType type,
CIVLSource source, boolean isDeclaration)
throws UnsatisfiablePathConditionException {
TypeEvaluation typeEval = getDynamicType(state, pid, type, source,
isDeclaration);
SymbolicExpression expr = symbolicUtil.expressionOfType(typeEval.type);
Evaluation result = new Evaluation(typeEval.state, expr);
return result;
}
/**
* Evaluates an abstract function call.
*
* @param state
* The current state.
* @param pid
* The ID of the process that the expression belongs to.
* @param expression
* The abstract function call expression to be evaluated.
* @return The value of the expression and the new state.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateAbstractFunctionCall(State state, int pid,
AbstractFunctionCallExpression expression)
throws UnsatisfiablePathConditionException {
AbstractFunction function = expression.function();
SymbolicType returnType = function.returnType()
.getDynamicType(universe);
List<SymbolicType> argumentTypes = new ArrayList<SymbolicType>();
List<SymbolicExpression> arguments = new ArrayList<SymbolicExpression>();
SymbolicType functionType;
SymbolicExpression functionExpression;
SymbolicExpression functionApplication;
Evaluation result;
for (Variable param : function.parameters()) {
argumentTypes.add(param.type().getDynamicType(universe));
}
for (Expression arg : expression.arguments()) {
Evaluation eval = evaluate(state, pid, arg);
arguments.add(eval.value);
}
functionType = universe.functionType(argumentTypes, returnType);
functionExpression = universe.symbolicConstant(
universe.stringObject(function.name().name()), functionType);
functionApplication = universe.apply(functionExpression, arguments);
result = new Evaluation(state, functionApplication);
return result;
}
/**
* Evaluates an address-of expression <code>&e</code>.
*
* @param state
* the pre-state
* @param pid
* PID of the process performing the evaluation
* @param expression
* the address-of expression
* @return the symbolic expression of pointer type resulting from evaluating
* the address of the argument and a new state (if there is
* side-effect, otherwise just return the original state)
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateAddressOf(State state, int pid,
AddressOfExpression expression)
throws UnsatisfiablePathConditionException {
return reference(state, pid, expression.operand());
}
/**
* Evaluates a short-circuit "and" expression <code>p && q</code>.
*
* @param state
* the pre-state
* @param pid
* PID of the process evaluating this expression
* @param expression
* the and expression
* @return the result of applying the AND operator to the two arguments
* together with the post-state whose path condition may contain the
* side-effects resulting from evaluation
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateAnd(State state, int pid,
BinaryExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.left());
BooleanExpression p = (BooleanExpression) eval.value;
BooleanExpression assumption = eval.state.getPathCondition();
Reasoner reasoner = universe.reasoner(assumption);
// true && x = x;
if (reasoner.isValid(p))
return evaluate(eval.state, pid, expression.right());
if (reasoner.isValid(universe.not(p))) {
// false && x = false;
eval.value = universe.falseExpression();
return eval;
} else {
BooleanExpression assumptionAndp = universe.and(assumption, p);
State s1 = eval.state.setPathCondition(assumptionAndp);
Evaluation eval1 = evaluate(s1, pid, expression.right());
BooleanExpression pcTemp = eval1.state.getPathCondition();
if (!assumptionAndp.equals(pcTemp)) {
BooleanExpression pc = universe.or(pcTemp,
universe.and(assumption, universe.not(p)));
eval.state = eval.state.setPathCondition(pc);
}
// Reason for above: In the common case where there
// are no side effects, this would set the path condition to
// (assumption && p) || (assumption && !p),
// which does not get simplified to just "assumption",
// as one would like. So it is handled as a special case:
// check whether pcTemp equals (assumption && p)
// (i.e., the evaluation of expression.right() did not
// add any side-effects). If this holds, then pc is just
// assumption.
eval.value = universe.and(p, (BooleanExpression) eval1.value);
return eval;
}
}
/**
* Evaluates an array literal expression, like
* <code>{[1] = a, [2] = 3, [6]=9}</code>;
*
* @param state
* The state of the program.
* @param pid
* The pid of the currently executing process.
* @param expression
* The array literal expression.
* @return The symbolic representation of the array literal expression and
* the new state if there is side effect.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateArrayLiteral(State state, int pid,
ArrayLiteralExpression expression)
throws UnsatisfiablePathConditionException {
Expression[] elements = expression.elements();
SymbolicType symbolicElementType = expression.elementType()
.getDynamicType(universe);
List<SymbolicExpression> symbolicElements = new ArrayList<>();
Evaluation eval;
for (Expression element : elements) {
eval = evaluate(state, pid, element);
symbolicElements.add(eval.value);
state = eval.state;
}
return new Evaluation(state, universe.array(symbolicElementType,
symbolicElements));
}
/**
* Evaluates a binary expression.
*
* @param state
* The state of the program.
* @param pid
* The PID of the currently executing process.
* @param process
* The name of the process for error report.
* @param expression
* The binary expression.
* @return A symbolic expression for the binary operation and a new state if
* there is side-effect.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateBinary(State state, int pid, String process,
BinaryExpression expression)
throws UnsatisfiablePathConditionException {
BINARY_OPERATOR operator = expression.operator();
switch (operator) {
case AND:
return evaluateAnd(state, pid, expression);
case OR:
return evaluateOr(state, pid, expression);
// TODO code review
case IMPLIES:
return evaluateImplies(state, pid, expression);
case BITAND:
return evaluateBitand(state, pid, expression);
case BITCOMPLEMENT:
return evaluateBitcomplement(state, pid, expression);
case BITOR:
return evaluateBitor(state, pid, expression);
case BITXOR:
return evaluateBitxor(state, pid, expression);
case SHIFTLEFT:
return evaluateShiftleft(state, pid, expression);
case SHIFTRIGHT:
return evaluateShiftright(state, pid, expression);
default:// numeric expression like +,-,*,/,%,etc
if (expression.left().getExpressionType() != null
&& expression.left().getExpressionType()
.equals(modelFactory.scopeType())) {
return evaluateScopeOperations(state, pid, expression);
} else {
return evaluateNumericOperations(state, pid, process,
expression);
}
}
}
/**
* Evaluates a bit and expression.
*
* @param state
* The state where the evaluation happens.
* @param pid
* The PID of the process that triggers the evaluation.
* @param expression
* The bit and expression to be evaluated.
* @return A possibly new state resulted from side effects during the
* evaluation and the value of the bit and expression.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateBitand(State state, int pid,
BinaryExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.left());
SymbolicExpression left = eval.value, right, result;
eval = evaluate(eval.state, pid, expression.right());
right = eval.value;
state = eval.state;
result = universe.apply(this.bitAndFunc, Arrays.asList(left, right));
return new Evaluation(state, result);
}
/**
* Evaluates a bit complement expression.
*
* @param state
* The state where the evaluation happens.
* @param pid
* The PID of the process that triggers the evaluation.
* @param expression
* The bit complement expression to be evaluated.
* @return A possibly new state resulted from side effects during the
* evaluation and the value of the bit complement expression.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateBitcomplement(State state, int pid,
BinaryExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.left());
SymbolicExpression left = eval.value, right, result;
eval = evaluate(eval.state, pid, expression.right());
right = eval.value;
state = eval.state;
result = universe.apply(this.bitComplementFunc,
Arrays.asList(left, right));
return new Evaluation(state, result);
}
/**
* Evaluates a bit or expression.
*
* @param state
* The state where the evaluation happens.
* @param pid
* The PID of the process that triggers the evaluation.
* @param expression
* The bit or expression to be evaluated.
* @return A possibly new state resulted from side effects during the
* evaluation and the value of the bit or expression.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateBitor(State state, int pid,
BinaryExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.left());
SymbolicExpression left = eval.value, right, result;
eval = evaluate(eval.state, pid, expression.right());
right = eval.value;
state = eval.state;
result = universe.apply(this.bitOrFunc, Arrays.asList(left, right));
return new Evaluation(state, result);
}
/**
* Evaluates a bit xor expression.
*
* @param state
* The state where the evaluation happens.
* @param pid
* The PID of the process that triggers the evaluation.
* @param expression
* The bit xor expression to be evaluated.
* @return A possibly new state resulted from side effects during the
* evaluation and the value of the bit xor expression.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateBitxor(State state, int pid,
BinaryExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.left());
SymbolicExpression left = eval.value, right, result;
eval = evaluate(eval.state, pid, expression.right());
right = eval.value;
state = eval.state;
result = universe.apply(this.bitXorFunc, Arrays.asList(left, right));
return new Evaluation(state, result);
}
/**
* Evaluate a boolean literal expression.
*
* @param state
* The state of the program.
* @param pid
* The pid of the currently executing process.
* @param expression
* The boolean literal expression.
* @return The symbolic representation of the boolean literal expression and
* the new state if there is side effect during the evaluation.
*/
private Evaluation evaluateBooleanLiteral(State state, int pid,
BooleanLiteralExpression expression) {
return new Evaluation(state, universe.bool(expression.value()));
}
/**
* Evaluates a bound variable expression.
*
* @param state
* The state where the evaluation happens.
* @param pid
* The PID of the process that triggers the evaluation.
* @param expression
* The bound variable expression to be evaluated.
* @return A possibly new state resulted from side effects during the
* evaluation and the value of the bound variable expression.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateBoundVariable(State state, int pid,
BoundVariableExpression expression) {
Iterator<SymbolicConstant> boundVariableIterator = boundVariables
.iterator();
Evaluation result = null;
while (boundVariableIterator.hasNext()) {
SymbolicConstant boundVariable = boundVariableIterator.next();
if (boundVariable.name().toString()
.equals(expression.name().name())) {
result = new Evaluation(state, boundVariable);
break;
}
}
if (result != null) {
return result;
}
throw new CIVLException("Unknown bound variable",
expression.getSource());
}
/**
* Evaluates a cast expression.
*
* @param state
* The state of the program.
* @param pid
* The pid of the currently executing process.
* @param process
* The process name for error report.
* @param expression
* The cast expression.
* @return A possibly new state resulted from side effects during the
* evaluation and the value of the cast expression.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateCast(State state, int pid, String process,
CastExpression expression)
throws UnsatisfiablePathConditionException {
Expression arg = expression.getExpression();
CIVLType argType = arg.getExpressionType();
Evaluation eval = evaluate(state, pid, arg);
SymbolicExpression value = eval.value;
CIVLType castType = expression.getCastType();
TypeEvaluation typeEval = getDynamicType(eval.state, pid, castType,
expression.getSource(), false);
SymbolicType endType = typeEval.type;
state = typeEval.state;
if (argType.isDomainType() && castType.isDomainType()) {
return new Evaluation(state, value);
} else if (argType.isBoolType() && castType.isIntegerType()) {
if (value.isTrue())
eval.value = universe.integer(1);
else if (value.isFalse())
eval.value = universe.integer(0);
else {
BooleanExpression assumption = universe.or(
universe.equals(this.zeroOrOne, this.zero),
universe.equals(this.zeroOrOne, this.one));
Reasoner reasoner = universe.reasoner(state.getPathCondition());
if (reasoner.valid(assumption).getResultType() != ResultType.YES)
eval.state = state.setPathCondition(universe.and(
state.getPathCondition(), assumption));
eval.value = this.zeroOrOne;
}
return eval;
} else if (argType.isIntegerType() && castType.isPointerType()) {
// only good cast is from 0 to null pointer
BooleanExpression assumption = state.getPathCondition();
BooleanExpression claim = universe.equals(zero, value);
ResultType resultType = universe.reasoner(assumption).valid(claim)
.getResultType();
if (resultType != ResultType.YES) {
if (((CIVLPointerType) castType).baseType().isVoidType())
eval.value = value;
else {
state = errorLogger.logError(expression.getSource(), state,
process,
this.symbolicAnalyzer.stateToString(state), claim,
resultType, ErrorKind.INVALID_CAST,
"Cast from non-zero integer to pointer");
eval.state = state;
}
} else
eval.value = this.symbolicUtil.nullPointer();
return eval;
} else if (argType.isPointerType() && castType.isIntegerType()) {
if (this.symbolicUtil.isNullPointer(value))
eval.value = universe.integer(0);
else
eval.value = value;
return eval;
} else if (argType.isPointerType() && castType.isPointerType()) {
// pointer to pointer: for now...no change.
return eval;
} else if (argType.isIntegerType() && castType.isBoolType()) {
if (value.isZero())
eval.value = universe.bool(false);
else if (value.isNumeric())
eval.value = universe.bool(true);
else
throw new CIVLExecutionException(ErrorKind.INVALID_CAST,
Certainty.CONCRETE, process,
"Cast from integer to boolean", arg.getSource());
return eval;
} else if (argType.isIntegerType() && castType.isCharType()) {
NumericExpression integerValue = (NumericExpression) value;
Number concreteValue = null;
Reasoner reasoner = universe.reasoner(state.getPathCondition());
CIVLSource source = expression.getSource();
// If integerValue is concrete and is inside the range [0, 255],
// return corresponding character by using java casting.
// Else if it's only outside of the range [0, 255], return abstract
// function.
if (integerValue.operator() == SymbolicOperator.CONCRETE) {
int int_value;
concreteValue = symbolicUtil.extractInt(source, integerValue);
assert (concreteValue != null) : "NumericExpression with concrete operator cannot "
+ "provide concrete numeric value";
assert (!(concreteValue instanceof IntegerNumber)) : "A Number object which suppose "
+ "has integer type cannot cast to IntegerNumber type";
int_value = concreteValue.intValue();
if (int_value < 0 || int_value > 255) {
throw new CIVLUnimplementedFeatureException(
"Converting integer whose value is larger than UCHAR_MAX or is less than UCHAR_MIN to char type\n");
} else
eval.value = universe.character((char) int_value);
} else {
SymbolicExpression func;
SymbolicFunctionType funcType;
BooleanExpression insideRangeClaim;
SymbolicExpression newCharValue;
ResultType retType;
insideRangeClaim = universe.and(
universe.lessThan(zero, integerValue),
universe.lessThan(integerValue, universe.integer(255)));
retType = reasoner.valid(insideRangeClaim).getResultType();
if (retType == ResultType.YES) {
// If not concrete, return abstract function.
funcType = universe.functionType(
Arrays.asList(universe.integerType()),
universe.characterType());
func = universe.canonic(universe.symbolicConstant(
universe.stringObject("int2char"), funcType));
newCharValue = universe.apply(func,
Arrays.asList(integerValue));
eval.value = newCharValue;
} else {
Certainty certain;
if (retType == ResultType.MAYBE)
certain = Certainty.MAYBE;
else
certain = Certainty.PROVEABLE;
CIVLExecutionException error = new CIVLExecutionException(
ErrorKind.INVALID_CAST,
certain,
process,
"Cast operation may involves casting a integer, whose value is larger than UCHAR_MAX or less than UCHAR_MIN, to char type object which is considered as unimplemented feature of CIVL",
this.symbolicAnalyzer.stateToString(state),
expression.getSource());
errorLogger.reportError(error);
throw new UnsatisfiablePathConditionException();
}
}
return eval;
}
try {
eval.value = universe.cast(endType, eval.value);
} catch (SARLException e) {
CIVLExecutionException error = new CIVLExecutionException(
ErrorKind.INVALID_CAST, Certainty.NONE, process,
"SARL could not cast: " + e,
this.symbolicAnalyzer.stateToString(state),
expression.getSource());
errorLogger.reportError(error);
throw new UnsatisfiablePathConditionException();
}
return eval;
}
/**
* Evaluates a char literal expression.
*
* @param state
* The state of the program.
* @param pid
* The pid of the currently executing process.
* @param expression
* The char literal expression.
* @return A possibly new state resulted from side effects during the
* evaluation and the value of the char literal expression.
*/
private Evaluation evaluateCharLiteral(State state, int pid,
CharLiteralExpression expression) {
return new Evaluation(state, universe.character(expression.value()));
}
/**
* Evaluates a dereference expression <code>*e</code>.
*
* @param state
* the pre-state
* @param pid
* PID of the process performing the evaluation
* @param process
* The process name for error report.
* @param expression
* the dereference expression
* @return the evaluation with the properly updated state and the value
* after the dereference.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateDereference(State state, int pid,
String process, DereferenceExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.pointer());
if (eval.value.isNull()) {
CIVLExecutionException err = new CIVLExecutionException(
ErrorKind.UNDEFINED_VALUE, Certainty.PROVEABLE, process,
"Attempt to dereference an uninitialized pointer.",
symbolicAnalyzer.stateToString(state), expression.pointer()
.getSource());
this.errorLogger.reportError(err);
// TODO: throw UnsatisfiablePathConditionException?
}
return dereference(expression.pointer().getSource(), eval.state,
process, eval.value, true);
}
/**
* Evaluates a derivative call expression.
*
* @param state
* the pre-state
* @param pid
* the PID of the process running this call
* @param expression
* the derivative call expression to be evaluated
* @return the evaluation with the properly updated state and the value of
* the derivative call expression.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateDerivativeCall(State state, int pid,
DerivativeCallExpression expression)
throws UnsatisfiablePathConditionException {
AbstractFunction function = expression.function();
SymbolicType returnType = function.returnType()
.getDynamicType(universe);
List<SymbolicType> argumentTypes = new ArrayList<SymbolicType>();
List<SymbolicExpression> arguments = new ArrayList<SymbolicExpression>();
SymbolicType functionType;
SymbolicExpression functionExpression;
SymbolicExpression functionApplication;
Evaluation result;
String derivativeName;
for (Variable param : function.parameters()) {
argumentTypes.add(param.type().getDynamicType(universe));
}
for (Expression arg : expression.arguments()) {
Evaluation eval = evaluate(state, pid, arg);
arguments.add(eval.value);
}
functionType = universe.functionType(argumentTypes, returnType);
// The derivative name is the name of the function concatenated with the
// names and degrees of the partials. e.g. the name of
// $D[rho,{x,1},{y,2}]() is "rhox1y2"
derivativeName = function.name().name();
for (Pair<Variable, IntegerLiteralExpression> partial : expression
.partials()) {
derivativeName += partial.left.name().name()
+ partial.right.value();
}
functionExpression = universe.symbolicConstant(
universe.stringObject(derivativeName), functionType);
functionApplication = universe.apply(functionExpression, arguments);
result = new Evaluation(state, functionApplication);
return result;
}
/**
* Evaluates a domain guard expression, the value of which is true iff there
* is a subsequent element of of the current one in the domain object. See
* also {@link DomainGuardExpression}.
*
* @param state
* The current state
* @param pid
* The PID of the process
* @param domainGuard
* The domain guard expression to be evaluated, which contains
* the information of the current domain element and the domain
* object.
* @return the evaluation with the properly updated state and the value of
* the domain guard expression.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateDomainGuard(State state, int pid,
DomainGuardExpression domainGuard)
throws UnsatisfiablePathConditionException {
Expression domain = domainGuard.domain();
int dimension = domainGuard.dimension();
// Collection for storing given domain element.
List<SymbolicExpression> domElement = new LinkedList<>();
SymbolicExpression domainValue;
// The value of the domain union.
SymbolicExpression domainUnion;
Evaluation eval = this.evaluate(state, pid, domain);
// Result, if there is a subsequence.
boolean hasNext = false;
// Flag indicating the given domain element only contains NULLs.
boolean isAllNull = true;
state = eval.state;
domainValue = eval.value;
domainUnion = universe.tupleRead(domainValue, twoObj);
// Evaluating the value of the given element.
for (int i = 0; i < dimension; i++) {
SymbolicExpression varValue = state.valueOf(pid,
domainGuard.variableAt(i));
domElement.add(varValue);
if (!varValue.isNull())
isAllNull = false;
}
// If the domain object is a rectangular domain
if (symbolicUtil.isRecDomain(domainValue)) {
SymbolicExpression recDom = universe.unionExtract(zeroObj,
domainUnion);
if (isAllNull)
hasNext = !symbolicUtil.isEmptyDomain(domainValue, dimension,
domain.getSource());
else
hasNext = symbolicUtil.recDomainHasNext(recDom, dimension,
domElement);
eval.state = state;
// TODO:rectangular domain always has concrete ranges so that the
// result
// is always concrete ?
eval.value = universe.bool(hasNext);
} else if (symbolicUtil.isLiteralDomain(domainValue)) {
Variable literalDomCounterVar;
// TODO: is there a domain that contains none elements ?
if (isAllNull)
hasNext = !symbolicUtil.isEmptyDomain(domainValue, dimension,
domain.getSource());
else {
NumericExpression literalCounter;
NumericExpression domainSize = symbolicUtil
.getDomainSize(domainValue);
int counter, size;
// Compare the literal domain counter and the size of the
// domain.
literalDomCounterVar = domainGuard.getLiteralDomCounter();
literalCounter = (NumericExpression) state.valueOf(pid,
literalDomCounterVar);
counter = ((IntegerNumber) universe
.extractNumber(literalCounter)).intValue();
size = ((IntegerNumber) universe.extractNumber(domainSize))
.intValue();
hasNext = counter < size;
}
} else
throw new CIVLInternalException(
"A domain object is neither a rectangular domain nor a literal domain",
domainGuard.getSource());
eval.state = state;
eval.value = universe.bool(hasNext);
return eval;
/************** old *******************/
// Expression domain = domainGuard.domain();
// int dimension = domainGuard.dimension();
// BooleanExpression result = universe.trueExpression();
// SymbolicExpression domainValue;
// Evaluation eval = this.evaluate(state, pid, domain);
// List<SymbolicExpression> varValues = new ArrayList<>(dimension);
//
// domainValue = eval.value;
// state = eval.state;
// for (int i = 0; i < dimension; i++) {
// SymbolicExpression varValue;
//
// eval = this.evaluate(state, pid, domainGuard.variableAt(i));
// state = eval.state;
// varValue = eval.value;
// varValues.add(varValue);
// }
// result = symbolicUtil.domainHasNext(domainValue, varValues);
// return new Evaluation(state, result);
}
/**
* Evaluates the value of a rectangular domain literal expression.
*
* @param state
* The current state
* @param pid
* The PID of the process
* @param recDomain
* The expression of the rectangular domain
* @return The evaluation with the properly updated state and the value of
* the rectangular domain literal expression.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateRecDomainLiteral(State state, int pid,
RecDomainLiteralExpression recDomain)
throws UnsatisfiablePathConditionException {
int dim = recDomain.dimension();
List<SymbolicExpression> ranges = new ArrayList<>();
Evaluation eval;
SymbolicExpression domainV;
SymbolicType domainType;
// For a rectangular domain, its range types are all the same.
// because rectangular domain is an array of ranges
SymbolicType rangeType;
List<SymbolicExpression> domValueComponents = new LinkedList<>();
// ranges should be in form of an array inside a domain.
SymbolicExpression rangesArray;
CIVLDomainType civlDomType;
CIVLType civlRangeType;
for (int i = 0; i < dim; i++) {
eval = evaluate(state, pid, recDomain.rangeAt(i));
state = eval.state;
ranges.add(eval.value);
}
rangeType = ranges.get(0).type();
civlRangeType = modelFactory.rangeType();
civlDomType = modelFactory.domainType(civlRangeType);
domainType = civlDomType.getDynamicType(universe);
assert domainType instanceof SymbolicTupleType : "Dynamic $domain type is not a tuple type";
assert rangeType instanceof SymbolicTupleType : "Dynamic $range type is not a tuple type";
// Adding components
domValueComponents.add(universe.integer(dim));
// Union field index which indicates it's a rectangular domain.
domValueComponents.add(zero);
rangesArray = universe.array(rangeType, ranges);
domValueComponents.add(universe.unionInject(
civlDomType.getDynamicSubTypesUnion(universe), zeroObj,
rangesArray));
// The cast is guaranteed
// TODO: when is the appropriate time to call universe.canonic() ?
domainV = universe.canonic(universe.tuple(
(SymbolicTupleType) domainType, domValueComponents));
return new Evaluation(state, domainV);
}
/**
* Evaluates a "dot" expression used to navigate to a field in a record,
* <code>e.f</code>.
*
* @param state
* The state of the model
* @param pid
* The PID of the process evaluating this expression
* @param expression
* The dot expression to evaluated
* @return The evaluation which contains the result of evaluating the
* expression together with the post-state which may incorporate
* side-effects resulting from the evaluation
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateDot(State state, int pid, String process,
DotExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.structOrUnion());
SymbolicExpression structValue = eval.value;
int fieldIndex = expression.fieldIndex();
if (expression.isStruct()) {
eval.value = universe.tupleRead(structValue,
universe.intObject(fieldIndex));
} else {
BooleanExpression test = universe.unionTest(
universe.intObject(fieldIndex), structValue);
if (test.isFalse()) {
errorLogger.logSimpleError(expression.getSource(), eval.state,
process, this.symbolicAnalyzer.stateToString(state),
ErrorKind.UNION,
"Attempt to access an invalid union member");
throw new UnsatisfiablePathConditionException();
}
eval.value = universe.unionExtract(universe.intObject(fieldIndex),
structValue);
}
return eval;
}
/**
* Evaluates a dynamic type of expression. TODO what's this for?
*
* @param state
* @param pid
* @param expression
* @return
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateDynamicTypeOf(State state, int pid,
DynamicTypeOfExpression expression)
throws UnsatisfiablePathConditionException {
return dynamicTypeOf(state, pid, expression.getType(),
expression.getSource(), true);
}
/**
* Evaluates a function guard expression. When the function is a system
* function, the evaluation inquires the corresponding library for its
* evaluation; otherwise, the result is always the true value.
*
* @param state
* @param pid
* @param process
* @param expression
* @return
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateFunctionGuard(State state, int pid,
String process, FunctionGuardExpression expression)
throws UnsatisfiablePathConditionException {
Triple<State, CIVLFunction, Integer> eval = this
.evaluateFunctionPointer(state, pid,
expression.functionExpression(), expression.getSource());
CIVLFunction function;
state = eval.first;
function = eval.second;
if (function == null) {
errorLogger.logSimpleError(expression.getSource(), state, process,
symbolicAnalyzer.stateToString(state), ErrorKind.OTHER,
"function body cann't be found");
throw new UnsatisfiablePathConditionException();
}
if (function.isSystem()) {
SystemFunction systemFunction = (SystemFunction) function;
return getSystemGuard(expression.getSource(), state, pid,
systemFunction.getLibrary(), systemFunction.name().name(),
expression.arguments());
}
return new Evaluation(state, universe.trueExpression());
}
private Evaluation evaluateFunctionPointer(State state, int pid,
FunctionIdentifierExpression expression) {
Scope scope = expression.scope();
String function = expression.function().name().name();
SymbolicExpression dyScopeId = modelFactory.scopeValue(state
.getDyscope(pid, scope));
SymbolicExpression functionPointer = universe.tuple(
this.functionPointerType,
Arrays.asList(new SymbolicExpression[] { dyScopeId,
universe.stringExpression(function) }));
return new Evaluation(state, functionPointer);
}
private Evaluation evaluateHereOrRootScope(State state, int pid,
HereOrRootExpression expression) {
int dyScopeID = expression.isRoot() ? state.rootDyscopeID() : state
.getProcessState(pid).getDyscopeId();
return new Evaluation(state, modelFactory.scopeValue(dyScopeID));
}
/**
* Evaluates a short-circuit "implies" expression "p=?q".
*
* @param state
* the pre-state
* @param pid
* PID of the process evaluating this expression
* @param expression
* the and expression
* @return the result of applying the IMPLIES operator to the two arguments
* together with the post-state whose path condition may contain the
* side-effects resulting from evaluation
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateImplies(State state, int pid,
BinaryExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.left());
BooleanExpression p = (BooleanExpression) eval.value;
BooleanExpression assumption = eval.state.getPathCondition();
Reasoner reasoner = universe.reasoner(assumption);
// If p is false, the implication will evaluate to true.
if (reasoner.isValid(universe.not(p))) {
eval.value = universe.trueExpression();
return eval;
} else {
State s1 = eval.state.setPathCondition(universe.and(assumption, p));
Evaluation eval1 = evaluate(s1, pid, expression.right());
BooleanExpression pc = universe.or(eval1.state.getPathCondition(),
universe.and(assumption, p));
eval.state = eval.state.setPathCondition(pc);
eval.value = universe.implies(p, (BooleanExpression) eval1.value);
return eval;
}
}
/**
* Evaluates an initial value expression.
*
* @param state
* @param pid
* @param expression
* @return
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateInitialValue(State state, int pid,
InitialValueExpression expression)
throws UnsatisfiablePathConditionException {
Variable variable = expression.variable();
CIVLType type = variable.type();
TypeEvaluation typeEval = getDynamicType(state, pid, type,
expression.getSource(), false);
int sid = typeEval.state.getDyscopeID(pid, variable);
return computeInitialValue(typeEval.state, pid, variable,
typeEval.type, sid);
}
@SuppressWarnings("unused")
private Evaluation initialNullValue(State state, int pid, CIVLType type)
throws UnsatisfiablePathConditionException {
TypeKind kind = type.typeKind();
Evaluation eval;
switch (kind) {
case COMPLETE_ARRAY: {
CIVLCompleteArrayType arrayType = (CIVLCompleteArrayType) type;
CIVLType elementType = arrayType.elementType();
Expression extent = arrayType.extent();
SymbolicExpression extentValue, elementValue, arrayValue;
Reasoner reasoner;
int extentCount;
List<SymbolicExpression> eleValues = new LinkedList<>();
eval = this.evaluate(state, pid, extent);
state = eval.state;
extentValue = eval.value;
eval = this.initialNullValue(state, pid, elementType);
state = eval.state;
elementValue = eval.value;
reasoner = universe.reasoner(state.getPathCondition());
extentCount = ((IntegerNumber) reasoner
.extractNumber((NumericExpression) extentValue)).intValue();
for (int i = 0; i < extentCount; i++)
eleValues.add(elementValue);
arrayValue = universe.array(elementType.getDynamicType(universe),
eleValues);
return new Evaluation(state, arrayValue);
}
case DOMAIN:
case ENUM:
case POINTER:
case PRIMITIVE:
case HEAP:
return new Evaluation(state, universe.nullExpression());
case STRUCT_OR_UNION: {
CIVLStructOrUnionType strOrUnionType = (CIVLStructOrUnionType) type;
int numFields = strOrUnionType.numFields();
List<SymbolicExpression> fieldValues = new LinkedList<>();
SymbolicExpression strValue;
for (int i = 0; i < numFields; i++) {
eval = this.initialNullValue(state, pid, strOrUnionType
.getField(i).type());
fieldValues.add(eval.value);
state = eval.state;
}
strValue = universe
.tuple((SymbolicTupleType) strOrUnionType
.getDynamicType(universe), fieldValues);
return new Evaluation(state, strValue);
}
default:
throw new CIVLInternalException("Unreachable", (CIVLSource) null);
}
}
/**
* Computes the symbolic initial value of a variable.
*
* @param state
* The state where the computation happens.
* @param pid
* The PID of the process that triggers the computation.
* @param variable
* The variable to be evaluated.
* @param dynamicType
* The symbolic type of the variable.
* @param dyscopeId
* The dynamic scope ID of the current state.
* @return The symbolic initial value of the given variable
* @throws UnsatisfiablePathConditionException
*/
private Evaluation computeInitialValue(State state, int pid,
Variable variable, SymbolicType dynamicType, int dyscopeId)
throws UnsatisfiablePathConditionException {
CIVLType type = variable.type();
int vid = variable.vid();
SymbolicExpression result;
if (!variable.isInput() && variable.isStatic()) {
return initialValueOfType(state, pid, type);
} else if (!variable.isInput()
&& !variable.isBound()
&& (type instanceof CIVLPrimitiveType || type.isPointerType() || type
.isDomainType())) {
result = nullExpression;
} else {// the case of an input variable or a variable of
// array/struct/union type.
String name;
StringObject nameObj;
if (variable.scope().id() == 0 && variable.isInput())
name = "I" + vid;
else
name = "X_s" + dyscopeId + "v" + vid;
nameObj = universe.stringObject(name);
result = universe.symbolicConstant(nameObj, dynamicType);
}
return new Evaluation(state, result);
}
/**
* Evaluates an integer literal expression.
*
* @param state
* The state of the program.
* @param pid
* The pid of the currently executing process.
* @param expression
* The integer literal expression.
* @return The symbolic representation of the integer literal expression.
*/
private Evaluation evaluateIntegerLiteral(State state, int pid,
IntegerLiteralExpression expression) {
return new Evaluation(state, universe.integer(expression.value()
.intValue()));
}
private Evaluation evaluateNumericOperations(State state, int pid,
String process, BinaryExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.left());
SymbolicExpression left = eval.value;
SymbolicExpression right;
eval = evaluate(eval.state, pid, expression.right());
right = eval.value;
switch (expression.operator()) {
case PLUS:
eval.value = universe.add((NumericExpression) left,
(NumericExpression) right);
break;
case MINUS:
eval.value = universe.subtract((NumericExpression) left,
(NumericExpression) right);
break;
case TIMES:
eval.value = universe.multiply((NumericExpression) left,
(NumericExpression) right);
break;
case DIVIDE: {
BooleanExpression assumption = eval.state.getPathCondition();
NumericExpression denominator = (NumericExpression) right;
BooleanExpression claim = universe.neq(
zeroOf(expression.getSource(),
expression.getExpressionType()), denominator);
ResultType resultType = universe.reasoner(assumption).valid(claim)
.getResultType();
if (resultType != ResultType.YES) {
eval.state = errorLogger.logError(expression.getSource(),
eval.state, process,
this.symbolicAnalyzer.stateToString(eval.state), claim,
resultType, ErrorKind.DIVISION_BY_ZERO,
"Division by zero");
}
eval.value = universe.divide((NumericExpression) left, denominator);
}
break;
case LESS_THAN:
eval.value = universe.lessThan((NumericExpression) left,
(NumericExpression) right);
break;
case LESS_THAN_EQUAL:
eval.value = universe.lessThanEquals((NumericExpression) left,
(NumericExpression) right);
break;
// equal and not_equal operators support scope, process, and pointer
// types. If the value of those types is undefined (e.g., process -1,
// scope -1, pointer<-1, ..., ...>), an error should be reported.
case EQUAL:
this.isValueDefined(eval.state, process, expression.left(), left);
this.isValueDefined(eval.state, process, expression.right(), right);
eval.value = universe.equals(left, right);
break;
case NOT_EQUAL:
this.isValueDefined(eval.state, process, expression.left(), left);
this.isValueDefined(eval.state, process, expression.right(), right);
eval.value = universe.neq(left, right);
break;
case MODULO: {
BooleanExpression assumption = eval.state.getPathCondition();
NumericExpression denominator = (NumericExpression) right;
BooleanExpression claim = universe.neq(
zeroOf(expression.getSource(),
expression.getExpressionType()), denominator);
ResultType resultType = universe.reasoner(assumption).valid(claim)
.getResultType();
// TODO: check not negative
if (resultType != ResultType.YES) {
eval.state = errorLogger.logError(expression.getSource(),
eval.state, process,
this.symbolicAnalyzer.stateToString(eval.state), claim,
resultType, ErrorKind.DIVISION_BY_ZERO,
"Modulus denominator is zero");
}
eval.value = universe.modulo((NumericExpression) left, denominator);
break;
}
case POINTER_ADD:
eval = pointerAdd(eval.state, pid, process, expression, left,
(NumericExpression) right);
break;
case POINTER_SUBTRACT:
eval = pointerSubtraction(eval.state, pid, process, expression,
left, right);
break;
case IMPLIES:
case AND:
case OR:
throw new CIVLInternalException("unreachable", expression);
default:
throw new CIVLUnimplementedFeatureException("Operator "
+ expression.operator(), expression);
}
return eval;
}
/**
* Evaluates a short-circuit "or" expression "p||q".
*
* @param state
* the pre-state
* @param pid
* PID of the process evaluating this expression
* @param expression
* the OR expression
* @return the result of applying the OR operator to the two arguments
* together with the post-state whose path condition may contain the
* side-effects resulting from evaluation
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateOr(State state, int pid,
BinaryExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.left());
BooleanExpression p = (BooleanExpression) eval.value;
BooleanExpression assumption = eval.state.getPathCondition();
Reasoner reasoner = universe.reasoner(assumption);
// TODO: handle special common case as in evaluateAnd.
// Look at evaluation of ternary operator too?
if (reasoner.isValid(p)) {
eval.value = universe.trueExpression();
return eval;
}
if (reasoner.isValid(universe.not(p))) {
return evaluate(eval.state, pid, expression.right());
} else {
State s1 = eval.state.setPathCondition(universe.and(assumption,
universe.not(p)));
Evaluation eval1 = evaluate(s1, pid, expression.right());
BooleanExpression pc = universe.or(eval1.state.getPathCondition(),
universe.and(assumption, p));
eval.state = eval.state.setPathCondition(pc);
eval.value = universe.or(p, (BooleanExpression) eval1.value);
return eval;
}
}
private Evaluation evaluateQuantifiedExpression(State state, int pid,
QuantifiedExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation result;
Evaluation quantifiedExpression;
BooleanExpression context;
Reasoner reasoner;
BooleanExpression simplifiedExpression;
SymbolicConstant boundVariable = universe.symbolicConstant(expression
.boundVariableName().stringObject(), expression
.boundVariableType().getDynamicType(universe));
State stateWithRestriction;
boundVariables.push(boundVariable);
if (expression.isRange()) {
Evaluation lower = evaluate(state, pid, expression.lower());
Evaluation upper = evaluate(state, pid, expression.upper());
SymbolicExpression rangeRestriction;
assert lower.value instanceof NumericExpression;
assert upper.value instanceof NumericExpression;
rangeRestriction = universe.and(universe.lessThanEquals(
(NumericExpression) lower.value,
(NumericExpression) boundVariable), universe
.lessThanEquals((NumericExpression) boundVariable,
(NumericExpression) upper.value));
stateWithRestriction = state.setPathCondition(universe.and(
(BooleanExpression) rangeRestriction,
state.getPathCondition()));
quantifiedExpression = evaluate(stateWithRestriction, pid,
expression.expression());
switch (expression.quantifier()) {
case EXISTS:
result = new Evaluation(state, universe.existsInt(
(NumericSymbolicConstant) boundVariable,
(NumericExpression) lower.value,
(NumericExpression) upper.value,
(BooleanExpression) quantifiedExpression.value));
break;
case FORALL:
result = new Evaluation(state, universe.forallInt(
(NumericSymbolicConstant) boundVariable,
(NumericExpression) lower.value,
(NumericExpression) upper.value,
(BooleanExpression) quantifiedExpression.value));
break;
case UNIFORM:
result = new Evaluation(state, universe.forallInt(
(NumericSymbolicConstant) boundVariable,
(NumericExpression) lower.value,
(NumericExpression) upper.value,
(BooleanExpression) quantifiedExpression.value));
break;
default:
throw new CIVLException("Unknown quantifier ",
expression.getSource());
}
} else {
Evaluation restriction = evaluate(state, pid,
expression.boundRestriction());
stateWithRestriction = state.setPathCondition(universe.and(
(BooleanExpression) restriction.value,
state.getPathCondition()));
quantifiedExpression = evaluate(stateWithRestriction, pid,
expression.expression());
// By definition, the restriction should be boolean valued.
assert restriction.value instanceof BooleanExpression;
context = universe.and(state.getPathCondition(),
(BooleanExpression) restriction.value);
reasoner = universe.reasoner(context);
simplifiedExpression = (BooleanExpression) reasoner
.simplify(quantifiedExpression.value);
switch (expression.quantifier()) {
case EXISTS:
result = new Evaluation(state, universe.exists(boundVariable,
universe.and((BooleanExpression) restriction.value,
simplifiedExpression)));
break;
case FORALL:
result = new Evaluation(state, universe.forall(boundVariable,
universe.implies((BooleanExpression) restriction.value,
simplifiedExpression)));
break;
case UNIFORM:
result = new Evaluation(state, universe.forall(boundVariable,
universe.implies((BooleanExpression) restriction.value,
simplifiedExpression)));
break;
default:
throw new CIVLException("Unknown quantifier ",
expression.getSource());
}
}
boundVariables.pop();
return result;
}
private Evaluation evaluateRegularRange(State state, int pid,
RegularRangeExpression range)
throws UnsatisfiablePathConditionException {
SymbolicTupleType type = (SymbolicTupleType) range.getExpressionType()
.getDynamicType(universe);
Evaluation eval = this.evaluate(state, pid, range.getLow());
SymbolicExpression low, high, step, rangeValue;
BooleanExpression claim;
boolean negativeStep = false;
ResultType validity;
String process = state.getProcessState(pid).name() + "(id = " + pid
+ ")";
low = eval.value;
state = eval.state;
eval = evaluate(state, pid, range.getHigh());
high = eval.value;
state = eval.state;
eval = evaluate(state, pid, range.getStep());
step = eval.value;
state = eval.state;
claim = universe.equals(this.zero, step);
validity = universe.reasoner(state.getPathCondition()).valid(claim)
.getResultType();
if (validity == ResultType.YES) {
CIVLExecutionException err = new CIVLExecutionException(
ErrorKind.OTHER, Certainty.PROVEABLE, process,
"A regular range expression requires a non-zero step.",
symbolicAnalyzer.stateToString(state), range.getSource());
errorLogger.reportError(err);
}
claim = universe.lessThan(this.zero, (NumericExpression) step);
validity = universe.reasoner(state.getPathCondition()).valid(claim)
.getResultType();
if (validity == ResultType.NO)
negativeStep = true;
if (negativeStep) {
SymbolicExpression tmp = low;
low = high;
high = tmp;
}
rangeValue = universe.tuple(type, Arrays.asList(low, high, step));
return new Evaluation(state, rangeValue);
}
private Evaluation evaluateScopeOperations(State state, int pid,
BinaryExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.left());
int left = modelFactory.getScopeId(expression.left().getSource(),
eval.value);
int right;
boolean result;
state = eval.state;
eval = evaluate(state, pid, expression.right());
state = eval.state;
right = modelFactory.getScopeId(expression.right().getSource(),
eval.value);
switch (expression.operator()) {
case PLUS:
int lowestCommonAncestor = stateFactory.lowestCommonAncestor(state,
left, right);
eval.value = modelFactory.scopeValue(lowestCommonAncestor);
break;
case LESS_THAN:
result = stateFactory.isDescendantOf(state, right, left);
eval.value = universe.bool(result);
break;
case LESS_THAN_EQUAL:
result = (left == right) ? true : stateFactory.isDescendantOf(
state, right, left);
eval.value = universe.bool(result);
break;
case EQUAL:
eval.value = universe.bool(left == right);
break;
case NOT_EQUAL:
eval.value = universe.bool(left != right);
break;
default:
throw new CIVLInternalException("unreachable",
expression.getSource());
}
return eval;
}
private Evaluation evaluateSizeofExpressionExpression(State state, int pid,
SizeofExpressionExpression expression)
throws UnsatisfiablePathConditionException {
return evaluateSizeofType(expression.getSource(), state, pid,
expression.getArgument().getExpressionType());
}
private Evaluation evaluateSizeofTypeExpression(State state, int pid,
SizeofTypeExpression expression)
throws UnsatisfiablePathConditionException {
return evaluateSizeofType(expression.getSource(), state, pid,
expression.getTypeArgument());
}
/**
* Evaluate a subscript expression.
*
* @param state
* The state of the program.
* @param pid
* The pid of the currently executing process.
* @param expression
* The array index expression.
* @return A symbolic expression for an array read.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateSubscript(State state, int pid, String process,
SubscriptExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.array());
SymbolicExpression array = eval.value;
SymbolicArrayType arrayType = (SymbolicArrayType) array.type();
NumericExpression index;
eval = evaluate(state, pid, expression.index());
index = (NumericExpression) eval.value;
if (arrayType.isComplete()) {
NumericExpression length = universe.length(array);
BooleanExpression assumption = eval.state.getPathCondition();
BooleanExpression claim = universe.and(
universe.lessThanEquals(zero, index),
universe.lessThan(index, length));
ResultType resultType = universe.reasoner(assumption).valid(claim)
.getResultType();
if (resultType != ResultType.YES) {
eval.state = errorLogger.logError(expression.getSource(),
eval.state, process,
symbolicAnalyzer.stateToString(eval.state), claim,
resultType, ErrorKind.OUT_OF_BOUNDS,
"Out of bounds array index:\nindex = " + index
+ "\nlength = " + length);
}
}
eval.value = universe.arrayRead(array, index);
return eval;
}
private Evaluation evaluateSelf(State state, int pid,
SelfExpression expression) {
return new Evaluation(state, modelFactory.processValue(pid));
}
private Evaluation evaluateProcnull(State state, int pid,
ProcnullExpression expression) {
return new Evaluation(state, modelFactory.nullProcessValue());
}
/**
* Evaluate a real literal expression.
*
* @param state
* The state of the program.
* @param pid
* The pid of the currently executing process.
* @param expression
* The real literal expression.
* @return The symbolic representation of the real literal expression.
*/
private Evaluation evaluateRealLiteral(State state, int pid,
RealLiteralExpression expression) {
return new Evaluation(state, universe.number(universe
.numberObject(numberFactory.rational(expression.value()
.toPlainString()))));
}
private Evaluation evaluateResult(State state, int pid,
ResultExpression expression) {
// TODO
// this is used in a contract post-condition as a variable to
// refer to the result returned by a function. $result.
// get rid of ResultExpression and instead create a variable
// in the outermost scope of any function with non-void
// return type, store the result of return in that variable.
// Add method in Function to get that variable. (and set it?)
// Model builder will translate $result to that variable.
throw new CIVLUnimplementedFeatureException(
"$result not yet implemented: " + expression.getSource());
}
private Evaluation evaluateScopeofExpression(State state, int pid,
String process, ScopeofExpression expression)
throws UnsatisfiablePathConditionException {
LHSExpression argument = expression.argument();
return evaluateScopeofExpressionWorker(state, pid, process, argument);
}
private Evaluation evaluateScopeofExpressionWorker(State state, int pid,
String process, LHSExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval;
switch (expression.lhsExpressionKind()) {
case DEREFERENCE:
Expression pointer = ((DereferenceExpression) expression).pointer();
eval = evaluate(state, pid, pointer);
int sid = symbolicUtil
.getDyscopeId(pointer.getSource(), eval.value);
state = eval.state;
if (sid < 0) {
errorLogger
.logSimpleError(pointer.getSource(), state, process,
symbolicAnalyzer.stateToString(state),
ErrorKind.DEREFERENCE,
"Attempt to dereference pointer into scope which has been removed from state");
throw new UnsatisfiablePathConditionException();
}
return new Evaluation(state, modelFactory.scopeValue(sid));
case DOT:
return evaluateScopeofExpressionWorker(state, pid, process,
(LHSExpression) (((DotExpression) expression)
.structOrUnion()));
case SUBSCRIPT:
return evaluateScopeofExpressionWorker(
state,
pid,
process,
(LHSExpression) (((SubscriptExpression) expression).array()));
default:// VARIABLE
int scopeId = state.getDyscopeID(pid,
((VariableExpression) expression).variable());
return new Evaluation(state, modelFactory.scopeValue(scopeId));
}
}
private Evaluation evaluateShiftleft(State state, int pid,
BinaryExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.left());
SymbolicExpression left = eval.value, right, result;
eval = evaluate(eval.state, pid, expression.right());
right = eval.value;
state = eval.state;
result = universe.apply(this.shiftLeftFunc, Arrays.asList(left, right));
return new Evaluation(state, result);
}
private Evaluation evaluateShiftright(State state, int pid,
BinaryExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.left());
SymbolicExpression left = eval.value, right, result;
eval = evaluate(eval.state, pid, expression.right());
right = eval.value;
state = eval.state;
result = universe
.apply(this.shiftRightFunc, Arrays.asList(left, right));
return new Evaluation(state, result);
}
/**
* Evaluate a struct literal expression.
*
* @param state
* The state of the program.
* @param pid
* The pid of the currently executing process.
* @param expression
* The struct literal expression.
* @return The symbolic representation of the struct literal expression.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateStructOrUnionLiteral(State state, int pid,
StructOrUnionLiteralExpression expression)
throws UnsatisfiablePathConditionException {
Expression[] fields = expression.fields();
SymbolicType dynamicStructType = expression.getExpressionType()
.getDynamicType(universe);
ArrayList<SymbolicExpression> symbolicFields = new ArrayList<>();
Evaluation eval;
if (expression.isStruct()) {
for (Expression field : fields) {
eval = evaluate(state, pid, field);
symbolicFields.add(eval.value);
state = eval.state;
}
assert dynamicStructType instanceof SymbolicTupleType;
return new Evaluation(state, universe.tuple(
(SymbolicTupleType) dynamicStructType, symbolicFields));
} else {
int numberOfMembers = fields.length;
SymbolicExpression unionValue;
SymbolicUnionType unionType = (SymbolicUnionType) dynamicStructType;
assert dynamicStructType instanceof SymbolicUnionType;
eval = evaluate(state, pid, fields[numberOfMembers - 1]);
state = eval.state;
unionValue = universe.unionInject(unionType,
universe.intObject(numberOfMembers - 1), eval.value);
return new Evaluation(state, unionValue);
}
}
/**
* Evaluate a unary expression.
*
* @param state
* The state of the program.
* @param pid
* The pid of the currently executing process.
* @param expression
* The unary expression.
* @return The symbolic representation of the unary expression.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateUnary(State state, int pid,
UnaryExpression expression)
throws UnsatisfiablePathConditionException {
Evaluation eval = evaluate(state, pid, expression.operand());
switch (expression.operator()) {
case NEGATIVE:
eval.value = universe.minus((NumericExpression) eval.value);
break;
case NOT:
eval.value = universe.not((BooleanExpression) eval.value);
break;
case BIG_O:
eval.value = universe.apply(bigOFunction,
new Singleton<SymbolicExpression>(eval.value));
break;
default:
throw new CIVLInternalException("Unknown unary operator "
+ expression.operator(), expression);
}
return eval;
}
/**
* Evaluate a variable expression.
*
* @param state
* The state of the program.
* @param pid
* The pid of the currently executing process.
* @param expression
* The variable expression.
* @return
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateVariable(State state, int pid, String process,
VariableExpression expression)
throws UnsatisfiablePathConditionException {
if (expression.variable().isOutput()) {
CIVLExecutionException e = new CIVLExecutionException(
ErrorKind.OUTPUT_READ, Certainty.CONCRETE, process,
"Attempt to read the output variable "
+ expression.variable().name(),
this.symbolicAnalyzer.stateToString(state),
expression.getSource());
errorLogger.reportError(e);
throw new UnsatisfiablePathConditionException();
} else {
SymbolicExpression value = state
.valueOf(pid, expression.variable());
if (value == null || value.isNull()) {
CIVLExecutionException e = new CIVLExecutionException(
ErrorKind.UNDEFINED_VALUE, Certainty.PROVEABLE,
process, "Attempt to read uninitialized variable "
+ expression,
this.symbolicAnalyzer.stateToString(state),
expression.getSource());
errorLogger.reportError(e);
throw new UnsatisfiablePathConditionException();
}
return new Evaluation(state, value);
}
}
private Evaluation evaluateWaitGuard(State state, int pid,
WaitGuardExpression expression) {
SymbolicExpression joinProcess, guard;
int pidValue;
Evaluation eval;
try {
eval = evaluate(state, pid, expression.joinedProcess());
} catch (UnsatisfiablePathConditionException e) {
return new Evaluation(state, universe.falseExpression());
}
joinProcess = eval.value;
state = eval.state;
pidValue = modelFactory.getProcessId(expression.getSource(),
joinProcess);
if (!state.getProcessState(pidValue).hasEmptyStack())
guard = universe.falseExpression();
else
guard = universe.trueExpression();
return new Evaluation(state, guard);
}
/**
* evaluate a system guard expression
*
* @param state
* The state where the computation happens.
* @param pid
* The ID of the process that wants to evaluate the guard.
* @param expression
* The system guard expression to be evaluated.
* @return The result of the evaluation, including the state and the
* symbolic expression of the value.
* @throws UnsatisfiablePathConditionException
*/
private Evaluation evaluateSystemGuard(State state, int pid,
SystemGuardExpression expression)
throws UnsatisfiablePathConditionException {
return getSystemGuard(expression.getSource(), state, pid,
expression.library(), expression.functionName(),
expression.arguments());
}
/**
* Finds pointers contained in a given expression recursively.
*
* @param expr
* @param set
* @param state
*/
private void findPointersInExpression(SymbolicExpression expr,
Set<SymbolicExpression> set, State state, String process) {
SymbolicType type = expr.type();
// TODO check comm type
if (type != null && !type.equals(heapType) && !type.equals(bundleType)) {
// need to eliminate heap type as well. each proc has its own.
if (pointerType.equals(type)) {
SymbolicExpression pointerValue;
Evaluation eval;
set.add(expr);
try {
if (expr.operator() == SymbolicOperator.CONCRETE
&& symbolicUtil.getDyscopeId(null, expr) >= 0) {
// if (getScopeId(null, expr) >= 0) {
/*
* If the expression is an arrayElementReference
* expression, and finally it turns that the array type
* has length 0, return immediately. Because we can not
* dereference it and the dereference exception
* shouldn't report here.
*/
if (symbolicUtil.getSymRef(expr)
.isArrayElementReference()) {
SymbolicExpression arrayPointer = symbolicUtil
.parentPointer(null, expr);
eval = this.dereference(null, state, process,
arrayPointer, false, true);
/* Check if it's length == 0 */
if (universe.length(eval.value).isZero())
return;
}
eval = this.dereference(null, state, process, expr,
false, true);
pointerValue = eval.value;
state = eval.state;
if (pointerValue.operator() == SymbolicOperator.CONCRETE
&& pointerValue.type() != null
&& pointerValue.type().equals(pointerType))
findPointersInExpression(pointerValue, set, state,
process);
}
} catch (UnsatisfiablePathConditionException e) {
// // TODO Auto-generated catch block
// e.printStackTrace();
}
} else {
int numArgs = expr.numArguments();
for (int i = 0; i < numArgs; i++) {
SymbolicObject arg = expr.argument(i);
findPointersInObject(arg, set, state, process);
}
}
}
}
/**
* Finds all the pointers that can be dereferenced inside a symbolic object.
*
* @param object
* a symbolic object
* @param set
* a set to which the pointer values will be added
* @param heapType
* the heap type, which will be ignored
*/
private void findPointersInObject(SymbolicObject object,
Set<SymbolicExpression> set, State state, String process) {
switch (object.symbolicObjectKind()) {
case EXPRESSION:
findPointersInExpression((SymbolicExpression) object, set, state,
process);
break;
case EXPRESSION_COLLECTION:
for (SymbolicExpression expr : (SymbolicCollection<?>) object)
findPointersInExpression(expr, set, state, process);
break;
default:
// ignore types and primitives, they don't have any pointers
// you can dereference.
}
}
/**
* Evaluates the dynamic type of a given CIVL type at a certain state. When
* the CIVL type has some state, e.g., an array type with a variable as the
* extent, the type needs to be evaluated.
*
* @param state
* The current state.
* @param pid
* The ID of the process where the computation happens.
* @param type
* The CIVL type to be evaluated for the dynamic type.
* @param source
* The source code element for error report.
* @param isDefinition
* The flag denoting if the type is a definition.
* @return The dynamic type of the given type.
* @throws UnsatisfiablePathConditionException
*/
private TypeEvaluation getDynamicType(State state, int pid, CIVLType type,
CIVLSource source, boolean isDefinition)
throws UnsatisfiablePathConditionException {
TypeEvaluation result;
// if type has a state variable and computeStructs is false, use
// variable else compute
if (type instanceof CIVLPrimitiveType) {
result = new TypeEvaluation(state, type.getDynamicType(universe));
} else if (type instanceof CIVLPointerType) {
result = new TypeEvaluation(state, pointerType);
} else if (type.getStateVariable() != null && !isDefinition) {
SymbolicExpression value = state.valueOf(pid,
type.getStateVariable());
result = new TypeEvaluation(state, getType(source, value));
} else if (type instanceof CIVLArrayType) {
CIVLArrayType arrayType = (CIVLArrayType) type;
TypeEvaluation elementTypeEval = getDynamicType(state, pid,
arrayType.elementType(), source, false);
if (arrayType.isComplete()) {
Evaluation lengthEval = evaluate(elementTypeEval.state, pid,
((CIVLCompleteArrayType) arrayType).extent());
NumericExpression length = (NumericExpression) lengthEval.value;
result = new TypeEvaluation(lengthEval.state,
universe.arrayType(elementTypeEval.type, length));
} else {
result = new TypeEvaluation(elementTypeEval.state,
universe.arrayType(elementTypeEval.type));
}
} else if (type instanceof CIVLStructOrUnionType) {
CIVLStructOrUnionType structType = (CIVLStructOrUnionType) type;
int numFields = structType.numFields();
LinkedList<SymbolicType> componentTypes = new LinkedList<SymbolicType>();
for (int i = 0; i < numFields; i++) {
StructOrUnionField field = structType.getField(i);
TypeEvaluation componentEval = getDynamicType(state, pid,
field.type(), source, false);
state = componentEval.state;
componentTypes.add(componentEval.type);
}
result = new TypeEvaluation(state, universe.tupleType(structType
.name().stringObject(), componentTypes));
} else if (type instanceof CIVLBundleType) {
result = new TypeEvaluation(state, type.getDynamicType(universe));
} else if (type instanceof CIVLHeapType) {
result = new TypeEvaluation(state, this.heapType);
} else if (type instanceof CIVLEnumType) {
result = new TypeEvaluation(state, type.getDynamicType(universe));
} else if (type instanceof CIVLDomainType) {
result = new TypeEvaluation(state, type.getDynamicType(universe));
} else
throw new CIVLInternalException("Unreachable", source);
return result;
}
private Evaluation getSystemGuard(CIVLSource source, State state, int pid,
String library, String function, List<Expression> arguments)
throws UnsatisfiablePathConditionException {
LibraryEvaluator libEvaluator;
try {
libEvaluator = this.libLoader.getLibraryEvaluator(library, this,
this.modelFactory, symbolicUtil, symbolicAnalyzer);
return libEvaluator.evaluateGuard(source, state, pid, function,
arguments);
} catch (LibraryLoaderException exception) {
String process = state.getProcessState(pid).name() + "(id=" + pid
+ ")";
CIVLExecutionException err = new CIVLExecutionException(
ErrorKind.LIBRARY, Certainty.PROVEABLE, process,
"An error is encountered when loading the library evaluator for "
+ library + ": " + exception.getMessage(),
this.symbolicAnalyzer.stateToString(state), source);
this.errorLogger.reportError(err);
}
return new Evaluation(state, universe.falseExpression());
}
/**
* Given a symbolic expression returned by the method
* {@link #expressionOfType}, this extracts the type that was used to create
* that expression. If the given expression is not an expression that was
* created by {@link #expressionOfType}, the behavior is undefined.
*
* @param expr
* a symbolic expression returned by method
* {@link #expressionOfType}
* @return the symbolic type used to create that expression
*/
private SymbolicType getType(CIVLSource source, SymbolicExpression expr) {
int id = symbolicUtil.extractIntField(source, expr, zeroObj);
return (SymbolicType) universe.objectWithId(id);
}
private Set<SymbolicExpression> heapCells(State state, int dyscopeId) {
SymbolicExpression heapValue = state.getVariableValue(dyscopeId, 0);
if (heapValue.isNull())
return new HashSet<>();
else {
CIVLHeapType heapType = modelFactory.heapType();
int numMallocs = heapType.getNumMallocs();
Set<SymbolicExpression> result = new HashSet<>();
for (int i = 0; i < numMallocs; i++) {
ReferenceExpression ref = universe.tupleComponentReference(
identityReference, universe.intObject(i));
SymbolicExpression heapCell = symbolicUtil.makePointer(
dyscopeId, 0, ref);
result.add(heapCell);
}
return result;
}
}
// TODO: add doc here
private Evaluation initialValueOfType(State state, int pid, CIVLType type)
throws UnsatisfiablePathConditionException {
TypeKind kind = type.typeKind();
Evaluation eval = null;
switch (kind) {
case ARRAY: {
CIVLArrayType arrayType = (CIVLArrayType) type;
CIVLType elementType = arrayType.elementType();
eval = new Evaluation(state, universe.emptyArray(elementType
.getDynamicType(universe)));
break;
}
case COMPLETE_ARRAY: {
CIVLCompleteArrayType arrayType = (CIVLCompleteArrayType) type;
CIVLType elementType = arrayType.elementType();
SymbolicExpression elementValue;
NumericExpression extent;
eval = initialValueOfType(state, pid, elementType);
state = eval.state;
elementValue = eval.value;
eval = this.evaluate(state, pid, arrayType.extent());
state = eval.state;
extent = (NumericExpression) eval.value;
eval.value = symbolicUtil.newArray(state.getPathCondition(),
elementType.getDynamicType(universe), extent, elementValue);
break;
}
case BUNDLE:
break;
case DOMAIN: {
CIVLDomainType domainType = (CIVLDomainType) type;
SymbolicExpression initDomainValue;
int dim;
SymbolicType integerType = universe.integerType();
SymbolicTupleType tupleType = universe.tupleType(universe
.stringObject("domain"), Arrays.asList(integerType,
integerType,
universe.arrayType(universe.arrayType(integerType))));
List<SymbolicExpression> tupleComponents = new LinkedList<>();
tupleComponents.add(one);
tupleComponents.add(one);
tupleComponents.add(universe.emptyArray(universe
.arrayType(integerType)));
if (domainType.isComplete()) {
CIVLCompleteDomainType compDomainType = (CIVLCompleteDomainType) domainType;
dim = compDomainType.getDimension();
tupleComponents.set(0, universe.integer(dim));
}
initDomainValue = universe.tuple(tupleType, tupleComponents);
eval = new Evaluation(state, initDomainValue);
break;
}
case ENUM: {
CIVLEnumType enumType = (CIVLEnumType) type;
eval = new Evaluation(state,
universe.integer(enumType.firstValue()));
break;
}
case POINTER:
eval = new Evaluation(state, symbolicUtil.nullPointer());
break;
case PRIMITIVE: {
CIVLPrimitiveType primitiveType = (CIVLPrimitiveType) type;
eval = new Evaluation(state, primitiveType.initialValue(universe));
break;
}
default:// STRUCT_OR_UNION{
{
CIVLStructOrUnionType strOrUnion = (CIVLStructOrUnionType) type;
if (strOrUnion.isUnionType()) {
eval = this.initialValueOfType(state, pid,
strOrUnion.getField(0).type());
eval.value = universe
.unionInject((SymbolicUnionType) strOrUnion
.getDynamicType(universe), this.zeroObj,
eval.value);
} else {
int size = strOrUnion.numFields();
List<SymbolicExpression> components = new ArrayList<>(size);
for (int i = 0; i < size; i++) {
eval = this.initialValueOfType(state, pid, strOrUnion
.getField(i).type());
state = eval.state;
components.add(eval.value);
}
eval = new Evaluation(state,
universe.tuple((SymbolicTupleType) strOrUnion
.getDynamicType(universe), components));
}
}
}
return eval;
}
/**
* Checks if a value of type scope, process, or pointer type is defined. If
* the value of those types is undefined (e.g., process -1, scope -1,
* pointer<-1, ..., ...>), an error should be reported.
*
* @param state
* The state where the checking happens.
* @param expression
* The static representation of the value.
* @param expressionValue
* The symbolic value to be checked if it is defined.
* @throws UnsatisfiablePathConditionException
*/
private void isValueDefined(State state, String process,
Expression expression, SymbolicExpression expressionValue)
throws UnsatisfiablePathConditionException {
CIVLSource source = expression.getSource();
CIVLType expressionType = expression.getExpressionType();
if (expressionType.equals(modelFactory.scopeType())) {
if (expressionValue.equals(modelFactory.undefinedScopeValue())) {
errorLogger.logSimpleError(source, state, process,
symbolicAnalyzer.stateToString(state),
ErrorKind.MEMORY_LEAK,
"Attempt to evaluate an invalid scope reference");
throw new UnsatisfiablePathConditionException();
}
} else if (expressionType.equals(modelFactory.processType())) {
if (expressionValue.equals(modelFactory.undefinedProcessValue())) {
errorLogger.logSimpleError(source, state, process,
symbolicAnalyzer.stateToString(state),
ErrorKind.MEMORY_LEAK,
"Attempt to evaluate an invalid process reference");
throw new UnsatisfiablePathConditionException();
}
} else if (expressionValue.type().equals(this.pointerType)) {
if (this.symbolicUtil.isNullPointer(expressionValue))
return;
try {
int scopeID = symbolicUtil
.getDyscopeId(source, expressionValue);
if (scopeID < 0) {
errorLogger
.logSimpleError(source, state, process,
symbolicAnalyzer.stateToString(state),
ErrorKind.MEMORY_LEAK,
"Attempt to evaluate a pointer refererring to memory of an invalid scope");
throw new UnsatisfiablePathConditionException();
}
} catch (Exception e) {
errorLogger.logSimpleError(source, state, process,
symbolicAnalyzer.stateToString(state),
ErrorKind.UNDEFINED_VALUE,
"Attempt to use undefined pointer");
throw new UnsatisfiablePathConditionException();
}
}
}
/**
* Returns the set of pointer values that occur inside a symbolic
* expression, excluding any pointers that occur inside a heap. TODO
* Optimization: you only need to call this method on variables that could
* have pointers in them, otherwise don't bother
*
* @param expr
* a symbolic expression
* @param heapType
* the heap type
* @return set of pointer values occurring a subexpression of expression
* (including expression itself) but not in a heap
*/
private Set<SymbolicExpression> pointersInExpression(
SymbolicExpression expr, State state, String process) {
Set<SymbolicExpression> result = new HashSet<>();
findPointersInExpression(expr, result, state, process);
return result;
}
/**
* zero
*
* @param source
* @param type
* @return
*/
private NumericExpression zeroOf(CIVLSource source, CIVLType type) {
if (type instanceof CIVLPrimitiveType) {
if (((CIVLPrimitiveType) type).primitiveTypeKind() == PrimitiveTypeKind.INT)
return zero;
if (((CIVLPrimitiveType) type).primitiveTypeKind() == PrimitiveTypeKind.REAL)
return zeroR;
}
throw new CIVLInternalException("Expected integer or real type, not "
+ type, source);
}
/* ********************* Pointer addition helpers ************************ */
/**
* Helper function for @link{pointerAdd}. Returns the new pointer after
* adding an increment or decrement and the array capacities
* information(@link{setDataBetween}) of the array pointed by the original
* pointer. If the pointer addition operation can be done only on one
* dimension (like for<code>int a[3][3];</code>, addition operation
* "&a[0][0] + 2" can be done without known the whole array information),
* the returned map container will be null.
*/
private Pair<Evaluation, Map<Integer, NumericExpression>> pointerAddWorker(
State state, String process, SymbolicExpression pointer,
NumericExpression offset, boolean checkOutput, CIVLSource source)
throws UnsatisfiablePathConditionException {
SymbolicExpression arrayPtr;
SymbolicExpression parentPtr;
ReferenceExpression parentRef;
NumericExpression extent, index;
ReferenceExpression ref;
ReferenceExpression newRef;
BooleanExpression claim, over, equal, drown;
Evaluation eval;
int scopeId, vid;
Reasoner reasoner = universe.reasoner(state.getPathCondition());
if (pointer.operator() != SymbolicOperator.CONCRETE)
errorLogger.logSimpleError(source, state, process,
symbolicAnalyzer.stateToString(state),
ErrorKind.DEREFERENCE,
"Attempt to dereference a invalid pointer");
claim = universe.equals(offset, zero);
if (reasoner.isValid(claim))
return new Pair<>(new Evaluation(state, pointer), null);
scopeId = symbolicUtil.getDyscopeId(source, pointer);
vid = symbolicUtil.getVariableId(source, pointer);
ref = symbolicUtil.getSymRef(pointer);
// Checking if the pointer addition will be out of bound at the current
// dimension.
if (ref.isArrayElementReference()) {
arrayPtr = symbolicUtil.parentPointer(source, pointer);
index = universe.integer(symbolicUtil
.getArrayIndex(source, pointer));
eval = dereference(source, state, process, arrayPtr, false);
state = eval.state;
if (!(eval.value.type() instanceof SymbolicCompleteArrayType))
throw new CIVLInternalException(
"Pointer addition on a pointer to incomplete array",
source);
extent = ((SymbolicCompleteArrayType) eval.value.type()).extent();
// beyond the bound
over = universe.lessThan(extent, universe.add(index, offset));
// lower than the bound
drown = universe.lessThan(universe.add(index, offset), zero);
equal = universe.equals(universe.add(index, offset), extent);
// out of bound condition:
// If index + offset > extent, out of bound.
// If index + offset < 0, out of bound.
// If index + offset == extent and the parent reference is an array
// element reference, out of bound.(e.g. int a[2], b[2][2]. &a[2] is
// a valid pointer, &b[0][2] should be cast to &b[1][0] unless it's
// a sequence of memory space)
if (reasoner.isValid(over)
|| reasoner.isValid(drown)
|| (reasoner.isValid(equal)
&& symbolicUtil.getSymRef(arrayPtr)
.isArrayElementReference() && vid != 0)) {
NumericExpression newIndex, remainder = index;
NumericExpression capacity = one;
SymbolicExpression arrayRootPtr;
List<NumericExpression> indexes = new LinkedList<>();
Map<Integer, NumericExpression> dimCapacities;
int dim = 1;
// Checking if the array is an allocated memory space
if (vid == 0)
errorLogger.reportError(new CIVLExecutionException(
ErrorKind.OUT_OF_BOUNDS, Certainty.PROVEABLE,
process, "Array out of bound\n", source));
// Computes remainder
arrayRootPtr = symbolicUtil.arrayRootPtr(arrayPtr, source);
eval = dereference(source, state, process, arrayRootPtr, false);
state = eval.state;
dimCapacities = symbolicUtil.getArrayElementsSizes(eval.value,
source);
parentPtr = arrayPtr;
while (dimCapacities.containsKey(dim)) {
NumericExpression oldIndex;
try {
oldIndex = universe.integer(symbolicUtil.getArrayIndex(
source, parentPtr));
} catch (ClassCastException e) {
errorLogger.reportError(new CIVLExecutionException(
ErrorKind.OUT_OF_BOUNDS, Certainty.PROVEABLE,
process, "Array out of bound\n", source));
return new Pair<>(new Evaluation(state, pointer), null);
}
capacity = dimCapacities.get(dim);
remainder = universe.add(remainder,
universe.multiply(oldIndex, capacity));
dim++;
parentPtr = symbolicUtil.parentPointer(source, parentPtr);
}
remainder = universe.add(remainder, offset);
// computes new indexes
dim--;
while (dimCapacities.containsKey(dim)) {
capacity = dimCapacities.get(dim);
newIndex = universe.divide(remainder, capacity);
remainder = universe.modulo(remainder, capacity);
indexes.add(newIndex);
dim--;
}
claim = universe.equals(remainder, zero);
if (!reasoner.isValid(claim))
errorLogger.reportError(new CIVLExecutionException(
ErrorKind.OUT_OF_BOUNDS, Certainty.PROVEABLE,
process, "Array out of bound\n", source));
newRef = symbolicUtil.updateArrayElementReference(
(ArrayElementReference) ref, indexes);
eval = new Evaluation(state, symbolicUtil.makePointer(scopeId,
vid, newRef));
return new Pair<>(eval, dimCapacities);
} else {
// The (offset + index) < extent at the given dimension,
// return new pointer easily.
parentRef = symbolicUtil.getSymRef(arrayPtr);
newRef = universe.arrayElementReference(parentRef,
universe.add(index, offset));
eval = new Evaluation(state, symbolicUtil.makePointer(scopeId,
vid, newRef));
return new Pair<>(eval, null);
}
} else {
errorLogger.reportError(new CIVLExecutionException(
ErrorKind.OUT_OF_BOUNDS, Certainty.PROVEABLE, process,
"Array out of bound\n", source));
eval = new Evaluation(state, pointer);
return new Pair<>(eval, null);
}
}
/* ********************** Methods from Evaluator *********************** */
@Override
public Evaluation evaluate(State state, int pid, Expression expression)
throws UnsatisfiablePathConditionException {
ExpressionKind kind = expression.expressionKind();
Evaluation result;
int processIdentifier = state.getProcessState(pid).identifier();
String process = "p" + processIdentifier + " (id = " + pid + ")";
if (expression.hasConstantValue())
return new Evaluation(state, expression.constantValue());
switch (kind) {
case ABSTRACT_FUNCTION_CALL:
result = evaluateAbstractFunctionCall(state, pid,
(AbstractFunctionCallExpression) expression);
break;
case ADDRESS_OF:
result = evaluateAddressOf(state, pid,
(AddressOfExpression) expression);
break;
case ARRAY_LITERAL:
result = evaluateArrayLiteral(state, pid,
(ArrayLiteralExpression) expression);
break;
case BINARY:
result = evaluateBinary(state, pid, process,
(BinaryExpression) expression);
break;
case BOOLEAN_LITERAL:
result = evaluateBooleanLiteral(state, pid,
(BooleanLiteralExpression) expression);
break;
case BOUND_VARIABLE:
result = evaluateBoundVariable(state, pid,
(BoundVariableExpression) expression);
break;
case CAST:
result = evaluateCast(state, pid, process,
(CastExpression) expression);
break;
case CHAR_LITERAL:
result = evaluateCharLiteral(state, pid,
(CharLiteralExpression) expression);
break;
case COND:
throw new CIVLInternalException("Conditional expressions should "
+ "be translated away by CIVL model builder ",
expression.getSource());
case DEREFERENCE:
result = evaluateDereference(state, pid, process,
(DereferenceExpression) expression);
break;
case DERIVATIVE:
result = evaluateDerivativeCall(state, pid,
(DerivativeCallExpression) expression);
break;
case DOMAIN_GUARD:
result = evaluateDomainGuard(state, pid,
(DomainGuardExpression) expression);
break;
case REC_DOMAIN_LITERAL:
result = evaluateRecDomainLiteral(state, pid,
(RecDomainLiteralExpression) expression);
break;
case DOT:
result = evaluateDot(state, pid, process,
(DotExpression) expression);
break;
case DYNAMIC_TYPE_OF:
result = evaluateDynamicTypeOf(state, pid,
(DynamicTypeOfExpression) expression);
break;
case FUNCTION_POINTER:
result = evaluateFunctionPointer(state, pid,
(FunctionIdentifierExpression) expression);
break;
case FUNCTION_GUARD:
result = evaluateFunctionGuard(state, pid, process,
(FunctionGuardExpression) expression);
break;
case HERE_OR_ROOT:
result = evaluateHereOrRootScope(state, pid,
(HereOrRootExpression) expression);
break;
case INITIAL_VALUE:
result = evaluateInitialValue(state, pid,
(InitialValueExpression) expression);
break;
case INTEGER_LITERAL:
result = evaluateIntegerLiteral(state, pid,
(IntegerLiteralExpression) expression);
break;
case REAL_LITERAL:
result = evaluateRealLiteral(state, pid,
(RealLiteralExpression) expression);
break;
case REGULAR_RANGE:
result = evaluateRegularRange(state, pid,
(RegularRangeExpression) expression);
break;
case RESULT:
result = evaluateResult(state, pid, (ResultExpression) expression);
break;
case SCOPEOF:
result = evaluateScopeofExpression(state, pid, process,
(ScopeofExpression) expression);
break;
case SELF:
result = evaluateSelf(state, pid, (SelfExpression) expression);
break;
case PROC_NULL:
result = this.evaluateProcnull(state, pid,
(ProcnullExpression) expression);
break;
case SIZEOF_TYPE:
result = evaluateSizeofTypeExpression(state, pid,
(SizeofTypeExpression) expression);
break;
case SIZEOF_EXPRESSION:
result = evaluateSizeofExpressionExpression(state, pid,
(SizeofExpressionExpression) expression);
break;
case STRUCT_OR_UNION_LITERAL:
result = evaluateStructOrUnionLiteral(state, pid,
(StructOrUnionLiteralExpression) expression);
break;
case SUBSCRIPT:
result = evaluateSubscript(state, pid, process,
(SubscriptExpression) expression);
break;
case SYSTEM_GUARD:
result = evaluateSystemGuard(state, pid,
(SystemGuardExpression) expression);
break;
case UNARY:
result = evaluateUnary(state, pid, (UnaryExpression) expression);
break;
case UNDEFINED_PROC:
result = new Evaluation(state, modelFactory.undefinedProcessValue());
break;
case VARIABLE:
result = evaluateVariable(state, pid, process,
(VariableExpression) expression);
break;
case WAIT_GUARD:
result = evaluateWaitGuard(state, pid,
(WaitGuardExpression) expression);
break;
case QUANTIFIER:
result = evaluateQuantifiedExpression(state, pid,
(QuantifiedExpression) expression);
break;
default:
throw new CIVLInternalException("Unknown kind of expression: "
+ kind, expression.getSource());
}
return result;
}
@Override
public Evaluation evaluateSizeofType(CIVLSource source, State state,
int pid, CIVLType type) throws UnsatisfiablePathConditionException {
Evaluation eval;
if (type instanceof CIVLPrimitiveType) {
NumericExpression value = ((CIVLPrimitiveType) type).getSizeof();
BooleanExpression facts = ((CIVLPrimitiveType) type).getFacts();
BooleanExpression pathCondition = universe.and(facts,
state.getPathCondition());
// TODO: this will modify state if state is mutable!
state = state.setPathCondition(pathCondition);
eval = new Evaluation(state, value);
} else if (type instanceof CIVLCompleteArrayType) {
NumericExpression extentValue;
eval = evaluate(state, pid, ((CIVLCompleteArrayType) type).extent());
extentValue = (NumericExpression) eval.value;
eval = evaluateSizeofType(source, eval.state, pid,
((CIVLArrayType) type).elementType());
eval.value = universe.multiply(extentValue,
(NumericExpression) eval.value);
} else if (type instanceof CIVLArrayType) {
throw new CIVLInternalException(
"sizeof applied to incomplete array type", source);
} else {
NumericExpression sizeof;
BooleanExpression pathCondition;
eval = dynamicTypeOf(state, pid, type, source, false);
sizeof = (NumericExpression) universe.apply(sizeofFunction,
new Singleton<SymbolicExpression>(eval.value));
pathCondition = universe.and(eval.state.getPathCondition(),
universe.lessThan(zero, sizeof));
eval.value = sizeof;
eval.state = state.setPathCondition(pathCondition);
}
return eval;
}
@Override
public Triple<State, CIVLFunction, Integer> evaluateFunctionPointer(
State state, int pid, Expression functionPointer, CIVLSource source)
throws UnsatisfiablePathConditionException {
CIVLFunction function;
Evaluation eval = this.evaluate(state, pid, functionPointer);
int scopeId = modelFactory.getScopeId(functionPointer.getSource(),
universe.tupleRead(eval.value, this.zeroObj));
SymbolicExpression symFuncName = universe.tupleRead(eval.value,
this.oneObj);
SymbolicSequence<?> originalArray = (SymbolicSequence<?>) symFuncName
.argument(0);
String funcName = "";
if (scopeId < 0) {
ProcessState procState = state.getProcessState(pid);
CIVLExecutionException err = new CIVLExecutionException(
ErrorKind.MEMORY_LEAK, Certainty.PROVEABLE,
procState.name() + "(id=" + pid + ")",
"Invalid function pointer: " + functionPointer,
symbolicAnalyzer.stateToString(state), source);
errorLogger.reportError(err);
}
state = eval.state;
for (int j = 0; j < originalArray.size(); j++) {
funcName += originalArray.get(j).toString().charAt(1);
}
function = state.getDyscope(scopeId).lexicalScope()
.getFunction(funcName);
return new Triple<>(state, function, scopeId);
}
@Override
public Evaluation initialValueOfStateVariable(CIVLSource source,
State state, int pid, CIVLType type)
throws UnsatisfiablePathConditionException {
TypeKind kind = type.typeKind();
Evaluation eval = null;
switch (kind) {
case COMPLETE_ARRAY: {
CIVLCompleteArrayType arrayType = (CIVLCompleteArrayType) type;
NumericExpression size;
SymbolicExpression element;
eval = this.evaluate(state, pid, arrayType.extent());
size = (NumericExpression) eval.value;
state = eval.state;
eval = this.initialValueOfStateVariable(source, state, pid,
arrayType.elementType());
state = eval.state;
element = eval.value;
eval.value = symbolicUtil.newArray(state.getPathCondition(),
arrayType.elementType().getDynamicType(universe), size,
element);
break;
}
case STRUCT_OR_UNION: {
CIVLStructOrUnionType strType = (CIVLStructOrUnionType) type;
if (strType.isStructType()) {
List<SymbolicExpression> comps = new ArrayList<>(
strType.numFields());
for (StructOrUnionField field : strType.fields()) {
eval = this.initialValueOfStateVariable(source, state, pid,
field.type());
state = eval.state;
comps.add(eval.value);
}
eval.value = universe.tuple(
(SymbolicTupleType) strType.getDynamicType(universe),
comps);
} else {
// TODO union Think about it
}
break;
}
case PRIMITIVE:
case ENUM:
case POINTER:
eval = new Evaluation(state, universe.integer(-1));
break;
default:
throw new CIVLInternalException("Invalid type of state variables",
source);
}
return eval;
}
@Override
public CIVLErrorLogger errorLogger() {
return this.errorLogger;
}
@Override
public Evaluation dereference(CIVLSource source, State state,
String process, SymbolicExpression pointer, boolean checkOutput)
throws UnsatisfiablePathConditionException {
return dereference(source, state, process, pointer, checkOutput, false);
}
/**
* * Only three types (represented differently in CIVL) of the symbolic
* expression "charPointer" is acceptable:<br>
* A pointer to char <br>
* A pointer to an element of array of char. (e.g. char a[N][M]; a[x] or
* &a[x][0] are acceptable. Address of an element of array of char or
* pointer to an array of char are same as this situation.)<br>
* A complete char array
*
* @param source
* The CIVL source of the pointer to char expression
* @param state
* The current state
* @param process
* The identifier of the process
* @param charPointer
* The pointer to char
* @return
* @throws UnsatisfiablePathConditionException
*/
@Override
public Pair<State, StringBuffer> getString(CIVLSource source, State state,
String process, SymbolicExpression charPointer)
throws UnsatisfiablePathConditionException {
if (charPointer.operator() == SymbolicOperator.CONCRETE) {
SymbolicSequence<?> originalArray = null;
int int_arrayIndex = -1;
StringBuffer result = new StringBuffer();
ReferenceExpression ref = null;
Evaluation eval;
if (charPointer.type() instanceof SymbolicCompleteArrayType) {
originalArray = (SymbolicSequence<?>) charPointer.argument(0);
int_arrayIndex = 0;
} else {
ref = symbolicUtil.getSymRef(charPointer);
if (ref instanceof ArrayElementReference) {
SymbolicExpression pointerCharArray = symbolicUtil
.parentPointer(source, charPointer);
SymbolicExpression charArray;
eval = dereference(source, state, process,
pointerCharArray, false);
state = eval.state;
charArray = eval.value;
try {
originalArray = (SymbolicSequence<?>) charArray
.argument(0);
} catch (ClassCastException e) {
throw new CIVLUnimplementedFeatureException(
"non-concrete strings", source);
} catch (ArrayIndexOutOfBoundsException e) {
CIVLExecutionException err = new CIVLExecutionException(
ErrorKind.UNDEFINED_VALUE, Certainty.PROVEABLE,
process,
"Reading undefined or uninitialized value from some pointer to heap: "
+ charArray.argument(0),
symbolicAnalyzer.stateToString(state), source);
errorLogger.reportError(err);
}
int_arrayIndex = symbolicUtil.extractInt(source,
((ArrayElementReference) ref).getIndex());
} else {
eval = dereference(source, state, process, charPointer,
false);
state = eval.state;
// A single character is not acceptable.
if (eval.value.arguments().length <= 1)
throw new CIVLExecutionException(ErrorKind.OTHER,
Certainty.PROVEABLE, process,
"Try to obtain a string from a sequence of char has length"
+ " less than or equal to one", source);
else {
originalArray = (SymbolicSequence<?>) eval.value
.argument(0);
int_arrayIndex = 0;
}
}
}
result = symbolicUtil.charArrayToString(source, originalArray,
int_arrayIndex, false);
return new Pair<>(state, result);
} else
throw new CIVLUnimplementedFeatureException("non-concrete strings",
source);
}
@Override
public Evaluation getStringExpression(State state, String process,
CIVLSource source, SymbolicExpression charPointer)
throws UnsatisfiablePathConditionException {
BooleanExpression pc = state.getPathCondition();
Reasoner reasoner = universe.reasoner(pc);
ReferenceExpression symRef = symbolicUtil.getSymRef(charPointer);
if (symRef.isArrayElementReference()) {
ArrayElementReference arrayEltRef = (ArrayElementReference) symRef;
SymbolicExpression arrayReference = symbolicUtil.parentPointer(
source, charPointer);
NumericExpression indexExpr = arrayEltRef.getIndex();
Evaluation eval = this.dereference(source, state, process,
arrayReference, false);
int index;
if (indexExpr.isZero())
index = 0;
else {
IntegerNumber indexNum = (IntegerNumber) reasoner
.extractNumber(indexExpr);
if (indexNum == null)
throw new CIVLUnimplementedFeatureException(
"non-concrete symbolic index into string", source);
index = indexNum.intValue();
}
if (index == 0)
return eval;
else if (index > 0) {
SymbolicExpression arrayValue = eval.value;
SymbolicArrayType arrayType = (SymbolicArrayType) arrayValue
.type();
LinkedList<SymbolicExpression> charExprList = new LinkedList<>();
int length;
if (arrayType.isComplete()) {
NumericExpression extent = ((SymbolicCompleteArrayType) arrayType)
.extent();
IntegerNumber extentNum = (IntegerNumber) reasoner
.extractNumber(extent);
if (extentNum == null)
throw new CIVLUnimplementedFeatureException(
"pointer into string of non-concrete length",
source);
length = extentNum.intValue();
} else
throw new CIVLUnimplementedFeatureException(
"pointer into string of unknown length", source);
for (int i = index; i < length; i++) {
SymbolicExpression charExpr = universe.arrayRead(
arrayValue, universe.integer(i));
charExprList.add(charExpr);
// if you wanted to get heavy-weight, call the prover to see
// if charExpr equals the null character instead of this:
if (nullCharExpr.equals(charExpr))
break;
}
eval.value = universe.array(charType, charExprList);
return eval;
} else
throw new CIVLInternalException("negative pointer index: "
+ index, source);
}
throw new CIVLUnimplementedFeatureException(
"pointer to char is not into an array of char", source);
}
@Override
public void memoryUnitsOfExpression(State state, int pid,
Expression expression, Set<SymbolicExpression> memoryUnits)
throws UnsatisfiablePathConditionException {
ExpressionKind kind = expression.expressionKind();
Evaluation eval;
int processIdentifier = state.getProcessState(pid).identifier();
String process = "p" + processIdentifier + " (id = " + pid + ")";
switch (kind) {
case ADDRESS_OF:
AddressOfExpression addressOfExpression = (AddressOfExpression) expression;
Expression operand = addressOfExpression.operand();
memoryUnitsOfExpression(state, pid, operand, memoryUnits);
break;
case ARRAY_LITERAL:
Expression[] elements = ((ArrayLiteralExpression) expression)
.elements();
for (Expression element : elements) {
memoryUnitsOfExpression(state, pid, element, memoryUnits);
}
break;
case BINARY:
BinaryExpression binaryExpression = (BinaryExpression) expression;
memoryUnitsOfExpression(state, pid, binaryExpression.left(),
memoryUnits);
memoryUnitsOfExpression(state, pid, binaryExpression.right(),
memoryUnits);
break;
case BOOLEAN_LITERAL:
break;
case CAST:
CastExpression castExpression = (CastExpression) expression;
memoryUnitsOfExpression(state, pid, castExpression.getExpression(),
memoryUnits);
break;
case CHAR_LITERAL:
break;
case DEREFERENCE:
DereferenceExpression deferenceExpression = (DereferenceExpression) expression;
memoryUnitsOfExpression(state, pid, deferenceExpression.pointer(),
memoryUnits);
break;
case DOT:
DotExpression dotExpression = (DotExpression) expression;
memoryUnitsOfExpression(state, pid, dotExpression.structOrUnion(),
memoryUnits);
break;
case DYNAMIC_TYPE_OF:
break;
case INITIAL_VALUE:
break;
case INTEGER_LITERAL:
break;
case REAL_LITERAL:
break;
case SELF:
break;
case PROC_NULL:
break;
case SCOPEOF:
ScopeofExpression scopeofExpression = (ScopeofExpression) expression;
memoryUnitsOfExpression(state, pid, scopeofExpression.argument(),
memoryUnits);
break;
case SIZEOF_TYPE:
break;
case SIZEOF_EXPRESSION:
SizeofExpressionExpression sizeofExpression = (SizeofExpressionExpression) expression;
memoryUnitsOfExpression(state, pid, sizeofExpression.getArgument(),
memoryUnits);
break;
case STRUCT_OR_UNION_LITERAL:
Expression[] fields = ((StructOrUnionLiteralExpression) expression)
.fields();
for (Expression field : fields) {
memoryUnitsOfExpression(state, pid, field, memoryUnits);
}
break;
case SUBSCRIPT:
SubscriptExpression subscriptExpression = (SubscriptExpression) expression;
memoryUnitsOfExpression(state, pid, subscriptExpression.array(),
memoryUnits);
memoryUnitsOfExpression(state, pid, subscriptExpression.index(),
memoryUnits);
break;
case UNARY:
UnaryExpression unaryExpression = (UnaryExpression) expression;
memoryUnitsOfExpression(state, pid, unaryExpression.operand(),
memoryUnits);
break;
case UNDEFINED_PROC:
break;
case VARIABLE:
Variable variable = ((VariableExpression) expression).variable();
int sid,
vid;
CIVLType type;
try {
sid = state.getDyscopeID(pid, variable);
vid = variable.vid();
type = variable.type();
} catch (IllegalArgumentException ex) {
break;
}
// if (!variable.name().name().equals(
// modelFactory.atomicLockVariableExpression().variable()
// .name().name())) {
// atomic_enter statement is always considered as dependent with all
// processes since it accesses the global variable __atomic_lock_var
if (!variable.isConst() && !type.isHandleObjectType()) {
eval = new Evaluation(state, symbolicUtil.makePointer(sid, vid,
identityReference));
memoryUnits.addAll(pointersInExpression(eval.value, state,
process));
}
// }
break;
case ABSTRACT_FUNCTION_CALL:
for (Expression arg : ((AbstractFunctionCallExpression) expression)
.arguments()) {
memoryUnitsOfExpression(state, pid, arg, memoryUnits);
}
break;
case REGULAR_RANGE: {
RegularRangeExpression rangeExpr = (RegularRangeExpression) expression;
memoryUnitsOfExpression(state, pid, rangeExpr.getLow(), memoryUnits);
memoryUnitsOfExpression(state, pid, rangeExpr.getHigh(),
memoryUnits);
memoryUnitsOfExpression(state, pid, rangeExpr.getStep(),
memoryUnits);
}
break;
case REC_DOMAIN_LITERAL: {
RecDomainLiteralExpression domain = (RecDomainLiteralExpression) expression;
int dim = domain.dimension();
for (int i = 0; i < dim; i++)
memoryUnitsOfExpression(state, pid, domain.rangeAt(i),
memoryUnits);
}
break;
case DOMAIN_GUARD:
memoryUnitsOfExpression(state, pid,
((DomainGuardExpression) expression).domain(), memoryUnits);
break;
case WAIT_GUARD:
break;
case QUANTIFIER:
break;
case FUNCTION_GUARD:// arguments already handled by the call
// statement
break;
case SYSTEM_GUARD:// arguments already handled by the call statement
break;
case HERE_OR_ROOT:
break;
case FUNCTION_POINTER:
break;
default:
throw new CIVLUnimplementedFeatureException(
"Computing impact memory units of " + kind + " expressions",
expression.getSource());
}
}
@Override
public Set<SymbolicExpression> memoryUnitsReachableFromVariable(
CIVLType variableType, SymbolicExpression variableValue,
int dyScopeID, int vid, State state, String process) {
if (variableType.isHeapType())
return heapCells(state, dyScopeID);
return pointersInExpression(
symbolicUtil.makePointer(dyScopeID, vid, identityReference),
state, process);
}
@Override
public ModelFactory modelFactory() {
return modelFactory;
}
@Override
public Evaluation pointerAdd(State state, int pid, String process,
BinaryExpression expression, SymbolicExpression pointer,
NumericExpression offset)
throws UnsatisfiablePathConditionException {
if (symbolicUtil.isUndefinedPointer(pointer)) {
errorLogger.logSimpleError(expression.getSource(), state, process,
symbolicAnalyzer.stateToString(state),
ErrorKind.DEREFERENCE,
"Attempt to dereference a pointer that refers to a "
+ "memory space that is already deallocated");
throw new UnsatisfiablePathConditionException();
} else {
ReferenceExpression symRef = symbolicUtil.getSymRef(pointer);
if (symRef.isArrayElementReference()) {
return (this.pointerAddWorker(state, process, pointer, offset,
false, expression.left().getSource())).left;
} else if (symRef.isOffsetReference()) {
OffsetReference offsetRef = (OffsetReference) symRef;
NumericExpression oldOffset = offsetRef.getOffset();
NumericExpression newOffset = universe.add(oldOffset, offset);
BooleanExpression claim = universe.and(
universe.lessThanEquals(zero, newOffset),
universe.lessThanEquals(newOffset, one));
BooleanExpression assumption = state.getPathCondition();
ResultType resultType = universe.reasoner(assumption)
.valid(claim).getResultType();
Evaluation eval;
if (resultType != ResultType.YES) {
state = errorLogger.logError(expression.getSource(), state,
process, symbolicAnalyzer.stateToString(state),
claim, resultType, ErrorKind.OUT_OF_BOUNDS,
"Pointer addition resulted in out of bounds object pointer:\noffset = "
+ newOffset);
}
eval = new Evaluation(state, symbolicUtil.setSymRef(pointer,
universe.offsetReference(offsetRef.getParent(),
newOffset)));
return eval;
} else if (symRef.isIdentityReference()) {
BooleanExpression claim = universe.equals(zero, offset);
BooleanExpression assumption = state.getPathCondition();
ResultType resultType = universe.reasoner(assumption)
.valid(claim).getResultType();
if (resultType != ResultType.YES) {
state = errorLogger.logError(expression.getSource(), state,
process, symbolicAnalyzer.stateToString(state),
claim, resultType, ErrorKind.OUT_OF_BOUNDS,
"Pointer addition resulted in out of bounds object pointer:\noffset = "
+ offset);
}
return new Evaluation(state, pointer);
} else
throw new CIVLUnimplementedFeatureException(
"Pointer addition for anything other than array elements or variables",
expression);
}
}
@Override
public Evaluation pointerSubtraction(State state, int pid, String process,
BinaryExpression expression, SymbolicExpression leftPtr,
SymbolicExpression rightPtr)
throws UnsatisfiablePathConditionException {
int leftVid, leftSid, rightVid, rightSid;
SymbolicExpression array, arrayPtr;
NumericExpression leftPos = zero, rightPos = zero;
Map<Integer, NumericExpression> leftPtrIndexes, rightPtrIndexes;
Map<Integer, NumericExpression> dimCapacities;
Evaluation eval;
int dim = 0;
// ModelFactory already checked type compatibility, so here we just
// check if these two pointers are pointing to same object and array
// element reference pointers.
leftVid = symbolicUtil.getVariableId(expression.left().getSource(),
leftPtr);
leftSid = symbolicUtil.getDyscopeId(expression.left().getSource(),
leftPtr);
rightVid = symbolicUtil.getVariableId(expression.right().getSource(),
rightPtr);
rightSid = symbolicUtil.getDyscopeId(expression.right().getSource(),
rightPtr);
// Check if the two point to the same object
if ((rightVid != leftVid) || (rightSid != leftSid))
state = errorLogger.logError(expression.getSource(), state,
process, symbolicAnalyzer.stateToString(state), null,
ResultType.NO, ErrorKind.POINTER,
"Operands of pointer subtraction point to the same obejct");
// Check if two pointers are array element reference pointers. Based on
// C11 Standard 6.5.6, entry 9: When two pointers are subtracted, both
// shall point to elements of the same array object, or one past the
// last element of the array object; the result is the difference of the
// subscripts of the two array elements.
// Thus, any pointer which is not an array element reference is invalid
// for pointer subtraction.
if (!(symbolicUtil.getSymRef(leftPtr).isArrayElementReference() && symbolicUtil
.getSymRef(rightPtr).isArrayElementReference()))
state = errorLogger
.logError(expression.getSource(), state, process,
symbolicAnalyzer.stateToString(state), null,
ResultType.NO, ErrorKind.POINTER,
"Not both of the operands of pointer subtraction points to an array element");
// Get the pointer to the whole array
arrayPtr = symbolicUtil.arrayRootPtr(leftPtr, expression.left()
.getSource());
leftPtrIndexes = symbolicAnalyzer.arrayIndexesByPointer(state,
expression.left().getSource(), leftPtr, true);
rightPtrIndexes = symbolicAnalyzer.arrayIndexesByPointer(state,
expression.right().getSource(), rightPtr, true);
// Check compatibility for heap objects:
// If VID == 0, all ancestor indexes of left pointer should be same as
// right pointer. Because different heap objects all have variable ID of
// number zero and ancestor indexes indicate if they are same heap
// objects.
if (leftVid == 0) {
boolean isCompatiable = true;
if (leftPtrIndexes.size() != rightPtrIndexes.size())
isCompatiable = false;
else {
for (int i = leftPtrIndexes.size() - 1; i >= 1; i--) {
if (!(leftPtrIndexes.get(i).equals(rightPtrIndexes.get(i)))) {
isCompatiable = false;
break;
}
}
}
if (!isCompatiable)
state = errorLogger
.logError(expression.getSource(), state, process,
symbolicAnalyzer.stateToString(state), null,
ResultType.NO, ErrorKind.POINTER,
"Operands of pointer subtraction point to different heap obejcts");
}
// Get array by dereferencing array pointer
eval = this.dereference(expression.left().getSource(), state, process,
arrayPtr, false);
state = eval.state;
array = eval.value;
dimCapacities = symbolicUtil.getArrayElementsSizes(array, expression
.left().getSource());
while (leftPtrIndexes.containsKey(dim)) {
NumericExpression leftIdx, rightIdx;
NumericExpression capacity = dimCapacities.get(dim);
leftIdx = leftPtrIndexes.get(dim);
rightIdx = rightPtrIndexes.get(dim);
leftPos = universe.add(leftPos,
universe.multiply(leftIdx, capacity));
rightPos = universe.add(rightPos,
universe.multiply(rightIdx, capacity));
dim++;
}
eval.state = state;
eval.value = universe.subtract(leftPos, rightPos);
return eval;
}
@Override
public Evaluation reference(State state, int pid, LHSExpression operand)
throws UnsatisfiablePathConditionException {
Evaluation result;
if (operand instanceof VariableExpression) {
Variable variable = ((VariableExpression) operand).variable();
int sid = state.getDyscopeID(pid, variable);
int vid = variable.vid();
result = new Evaluation(state, symbolicUtil.makePointer(sid, vid,
identityReference));
} else if (operand instanceof SubscriptExpression) {
Evaluation refEval = reference(state, pid,
((SubscriptExpression) operand).array());
SymbolicExpression arrayPointer = refEval.value;
ReferenceExpression oldSymRef = symbolicUtil
.getSymRef(arrayPointer);
NumericExpression index;
ReferenceExpression newSymRef;
result = evaluate(refEval.state, pid,
((SubscriptExpression) operand).index());
index = (NumericExpression) result.value;
newSymRef = universe.arrayElementReference(oldSymRef, index);
result.value = symbolicUtil.setSymRef(arrayPointer, newSymRef);
} else if (operand instanceof DereferenceExpression) {
// &(*p) = p, so just evaluate the pointer and return.
result = evaluate(state, pid,
((DereferenceExpression) operand).pointer());
} else if (operand instanceof DotExpression) {
DotExpression dot = (DotExpression) operand;
int index = dot.fieldIndex();
if (dot.isStruct()) {
Evaluation eval = reference(state, pid,
(LHSExpression) dot.structOrUnion());
SymbolicExpression structPointer = eval.value;
ReferenceExpression oldSymRef = symbolicUtil
.getSymRef(structPointer);
ReferenceExpression newSymRef = universe
.tupleComponentReference(oldSymRef,
universe.intObject(index));
eval.value = symbolicUtil.setSymRef(structPointer, newSymRef);
result = eval;
} else {
// when u is a union type, then &(u.x) = &u.
return reference(state, pid,
(LHSExpression) dot.structOrUnion());
}
} else
throw new CIVLInternalException("Unknown kind of LHSExpression",
operand);
return result;
}
@Override
public SymbolicType referencedType(CIVLSource source, State state,
SymbolicExpression pointer) {
int sid = symbolicUtil.getDyscopeId(source, pointer);
int vid = symbolicUtil.getVariableId(source, pointer);
ReferenceExpression symRef = symbolicUtil.getSymRef(pointer);
SymbolicExpression variableValue = state.getDyscope(sid).getValue(vid);
SymbolicType variableType = variableValue.type();
SymbolicType result = universe.referencedType(variableType, symRef);
return result;
}
public StateFactory stateFactory() {
return stateFactory;
}
@Override
public SymbolicUtility symbolicUtility() {
return symbolicUtil;
}
public SymbolicUniverse universe() {
return universe;
}
@Override
public Pair<Evaluation, Map<Integer, NumericExpression>> evaluatePointerAdd(
State state, String process, SymbolicExpression ptr,
NumericExpression offset, boolean ifCheckOutput, CIVLSource source)
throws UnsatisfiablePathConditionException {
SymbolicExpression newPtr = symbolicAnalyzer
.castToArrayElementReference(state, ptr, source);
return this.pointerAddWorker(state, process, newPtr, offset,
ifCheckOutput, source);
}
@Override
public List<ReferenceExpression> leafNodeReferencesOfType(
CIVLSource source, State state, int pid, CIVLType type)
throws UnsatisfiablePathConditionException {
return this.leafNodeReferencesOfType(source, state, pid, type,
universe.identityReference());
}
private List<ReferenceExpression> leafNodeReferencesOfType(
CIVLSource source, State state, int pid, CIVLType type,
ReferenceExpression parent)
throws UnsatisfiablePathConditionException {
List<ReferenceExpression> result = new ArrayList<>();
TypeKind typeKind = type.typeKind();
switch (typeKind) {
case ARRAY:
throw new CIVLUnimplementedFeatureException(
"sub-references of incomplete arrays", source);
case COMPLETE_ARRAY: {
CIVLCompleteArrayType arrayType = (CIVLCompleteArrayType) type;
Expression extent = arrayType.extent();
Evaluation eval = this.evaluate(state, pid, extent);
NumericExpression extentValue = (NumericExpression) eval.value;
CIVLType eleType = arrayType.elementType();
state = eval.state;
Reasoner reasoner = universe.reasoner(state.getPathCondition());
IntegerNumber length_number = (IntegerNumber) reasoner
.extractNumber(extentValue);
if (length_number != null) {
int length_int = length_number.intValue();
for (int i = 0; i < length_int; i++) {
ArrayElementReference arrayEle = universe
.arrayElementReference(parent, universe.integer(i));
result.addAll(this.leafNodeReferencesOfType(source, state,
pid, eleType, arrayEle));
}
} else
throw new CIVLUnimplementedFeatureException(
"sub-references of arrays with non-concrete extent",
source);
break;
}
case DOMAIN:
case ENUM:
case POINTER:
case BUNDLE:
case PRIMITIVE:
if (type.isVoidType())
throw new CIVLUnimplementedFeatureException(
"sub-references of void type", source);
result.add(parent);
break;
case STRUCT_OR_UNION: {
CIVLStructOrUnionType structOrUnion = (CIVLStructOrUnionType) type;
int numFields = structOrUnion.numFields();
if (structOrUnion.isUnionType())
throw new CIVLUnimplementedFeatureException(
"sub-references of union type", source);
for (int i = 0; i < numFields; i++) {
CIVLType filedType = structOrUnion.getField(i).type();
TupleComponentReference tupleComp = universe
.tupleComponentReference(parent, universe.intObject(i));
result.addAll(this.leafNodeReferencesOfType(source, state, pid,
filedType, tupleComp));
}
break;
}
default:
throw new CIVLUnimplementedFeatureException("sub-references of "
+ typeKind, source);
}
return result;
}
}