SimpleEnablerWorker.java
package dev.civl.mc.kripke.common;
import java.io.PrintStream;
import java.util.Collection;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;
import java.util.Stack;
import dev.civl.mc.config.IF.CIVLConstants.DeadlockKind;
import dev.civl.mc.dynamic.IF.SymbolicUtility;
import dev.civl.mc.kripke.IF.Enabler;
import dev.civl.mc.model.IF.CIVLFunction;
import dev.civl.mc.model.IF.CIVLInternalException;
import dev.civl.mc.model.IF.CIVLSource;
import dev.civl.mc.model.IF.CIVLTypeFactory;
import dev.civl.mc.model.IF.ModelConfiguration;
import dev.civl.mc.model.IF.Scope;
import dev.civl.mc.model.IF.contract.DependsEvent;
import dev.civl.mc.model.IF.contract.FunctionBehavior;
import dev.civl.mc.model.IF.contract.FunctionContract;
import dev.civl.mc.model.IF.contract.MemoryEvent;
import dev.civl.mc.model.IF.contract.NamedFunctionBehavior;
import dev.civl.mc.model.IF.expression.AbstractFunctionCallExpression;
import dev.civl.mc.model.IF.expression.AddressOfExpression;
import dev.civl.mc.model.IF.expression.ArrayLambdaExpression;
import dev.civl.mc.model.IF.expression.ArrayLiteralExpression;
import dev.civl.mc.model.IF.expression.BinaryExpression;
import dev.civl.mc.model.IF.expression.BinaryExpression.BINARY_OPERATOR;
import dev.civl.mc.model.IF.expression.CastExpression;
import dev.civl.mc.model.IF.expression.ConditionalExpression;
import dev.civl.mc.model.IF.expression.DereferenceExpression;
import dev.civl.mc.model.IF.expression.DerivativeCallExpression;
import dev.civl.mc.model.IF.expression.DifferentiableExpression;
import dev.civl.mc.model.IF.expression.DomainGuardExpression;
import dev.civl.mc.model.IF.expression.DotExpression;
import dev.civl.mc.model.IF.expression.DynamicTypeOfExpression;
import dev.civl.mc.model.IF.expression.Expression;
import dev.civl.mc.model.IF.expression.Expression.ExpressionKind;
import dev.civl.mc.model.IF.expression.ExtendedQuantifiedExpression;
import dev.civl.mc.model.IF.expression.FunctionCallExpression;
import dev.civl.mc.model.IF.expression.FunctionGuardExpression;
import dev.civl.mc.model.IF.expression.LHSExpression;
import dev.civl.mc.model.IF.expression.LambdaExpression;
import dev.civl.mc.model.IF.expression.MPIContractExpression;
import dev.civl.mc.model.IF.expression.MemoryUnitExpression;
import dev.civl.mc.model.IF.expression.QuantifiedExpression;
import dev.civl.mc.model.IF.expression.RecDomainLiteralExpression;
import dev.civl.mc.model.IF.expression.RegularRangeExpression;
import dev.civl.mc.model.IF.expression.ScopeofExpression;
import dev.civl.mc.model.IF.expression.SizeofExpression;
import dev.civl.mc.model.IF.expression.SizeofTypeExpression;
import dev.civl.mc.model.IF.expression.SubscriptExpression;
import dev.civl.mc.model.IF.expression.SystemGuardExpression;
import dev.civl.mc.model.IF.expression.UnaryExpression;
import dev.civl.mc.model.IF.expression.ValueAtExpression;
import dev.civl.mc.model.IF.expression.VariableExpression;
import dev.civl.mc.model.IF.expression.reference.ArraySliceReference;
import dev.civl.mc.model.IF.expression.reference.MemoryUnitReference;
import dev.civl.mc.model.IF.location.Location;
import dev.civl.mc.model.IF.statement.AssignStatement;
import dev.civl.mc.model.IF.statement.AtomicLockAssignStatement;
import dev.civl.mc.model.IF.statement.CallOrSpawnStatement;
import dev.civl.mc.model.IF.statement.CivlParForSpawnStatement;
import dev.civl.mc.model.IF.statement.DomainIteratorStatement;
import dev.civl.mc.model.IF.statement.MallocStatement;
import dev.civl.mc.model.IF.statement.ParallelAssignStatement;
import dev.civl.mc.model.IF.statement.ReturnStatement;
import dev.civl.mc.model.IF.statement.Statement;
import dev.civl.mc.model.IF.statement.Statement.StatementKind;
import dev.civl.mc.model.IF.statement.UpdateStatement;
import dev.civl.mc.model.IF.statement.WithStatement;
import dev.civl.mc.model.IF.type.CIVLArrayType;
import dev.civl.mc.model.IF.type.CIVLCompleteArrayType;
import dev.civl.mc.model.IF.type.CIVLFunctionType;
import dev.civl.mc.model.IF.type.CIVLHeapType;
import dev.civl.mc.model.IF.type.CIVLPointerType;
import dev.civl.mc.model.IF.type.CIVLSetType;
import dev.civl.mc.model.IF.type.CIVLStructOrUnionType;
import dev.civl.mc.model.IF.type.CIVLType;
import dev.civl.mc.model.IF.type.StructOrUnionField;
import dev.civl.mc.model.IF.variable.Variable;
import dev.civl.mc.semantics.IF.Evaluator;
import dev.civl.mc.semantics.IF.Semantics;
import dev.civl.mc.semantics.IF.Transition;
import dev.civl.mc.state.IF.DynamicScope;
import dev.civl.mc.state.IF.ProcessState;
import dev.civl.mc.state.IF.StackEntry;
import dev.civl.mc.state.IF.State;
import dev.civl.mc.state.IF.StateFactory;
import dev.civl.mc.state.IF.UnsatisfiablePathConditionException;
import dev.civl.mc.util.IF.Pair;
import dev.civl.mc.util.IF.SeqSet;
import dev.civl.sarl.IF.Reasoner;
import dev.civl.sarl.IF.SymbolicUniverse;
import dev.civl.sarl.IF.ValidityResult.ResultType;
import dev.civl.sarl.IF.expr.ArrayElementReference;
import dev.civl.sarl.IF.expr.BooleanExpression;
import dev.civl.sarl.IF.expr.NTReferenceExpression;
import dev.civl.sarl.IF.expr.NumericExpression;
import dev.civl.sarl.IF.expr.ReferenceExpression;
import dev.civl.sarl.IF.expr.ReferenceExpression.ReferenceKind;
import dev.civl.sarl.IF.expr.SymbolicExpression;
import dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator;
import dev.civl.sarl.IF.expr.TupleComponentReference;
import dev.civl.sarl.IF.number.IntegerNumber;
import dev.civl.sarl.IF.object.SymbolicObject;
import dev.civl.sarl.IF.object.SymbolicSequence;
import dev.civl.sarl.IF.type.SymbolicArrayType;
import dev.civl.sarl.IF.type.SymbolicCompleteArrayType;
import dev.civl.sarl.IF.type.SymbolicFunctionType;
import dev.civl.sarl.IF.type.SymbolicMapType;
import dev.civl.sarl.IF.type.SymbolicSetType;
import dev.civl.sarl.IF.type.SymbolicTupleType;
import dev.civl.sarl.IF.type.SymbolicType;
import dev.civl.sarl.IF.type.SymbolicTypeSequence;
import dev.civl.sarl.IF.type.SymbolicUnionType;
/**
* <p>
* A worker object created to compute an ample set for one given {@link State}.
* This worker is created and owned by a {@link SimpleEnabler}. It maintains a
* reference to the enabler to access constant fields and utility methods.
* </p>
*
* <p>
* This class makes extensive use of {@link SeqSet}s to represent sets of
* objects present in the state. A leaf in the SeqSet is an {@code int} array of
* length 2, 3, or 4. The first two components are always a dynamic scope ID and
* a static variable ID. These specify a unique variable instance in the state.
* If the length is two, then the leaf represents the object which is that
* entire variable. If the variable is a heap, then the third integer represents
* a row in the heap table, which corresponds to a specific {@code $malloc}
* statement. Hence a length-3 leaf represents all objects created in a specific
* heap by a single {@code $malloc} statement. If the length is 4, the fourth
* integer specifies one object created by that {@code $malloc} statement.
* </p>
* <p>
* In the future, we might consider getting even more precise and specifying
* sub-components of objects, such as array slices, or particular fields of
* structures. But for now, only complete objects can be specified.s
* </p>
*
* @author siegel
*/
public class SimpleEnablerWorker {
// Constants ...
// /**
// * An integer which will be used to insert a pair (terminationCode, pid)
// * into a SeqSet to represent an imaginary "termination" variable for a
// * process. Every process p will have (terminationCode,p) in its
// reachWrite
// * set, as long as that process has not terminated. A process p that is at
// a
// * blocked wait statement in which the argument evaluates to q will have
// * (terminationCode,q) in its depends set. This implies that any ample set
// * including p must also include q. Otherwise, it would be possible for a
// * statement (wait on q) dependent on a statement in the ample set (any
// * enabled statement in p) to occur before anything in the ample set
// occurs.
// */
// public final static int terminationCode = Integer.MAX_VALUE;
/**
* This is the string used as prefix for symbolic constants that result from
* havoc. (E.g., "Y".)
*/
public final static String havocPrefix = ModelConfiguration.SYMBOL_PREFIXES[ModelConfiguration.HAVOC_PREFIX_INDEX];
// Fields...
/**
* The {@link Enabler} that created this worker. The {@code enabler}
* provides many constant resources that this worker can access. It would be
* inefficient to duplicate all those references in each worker, since so
* many workers will be created and destroyed constantly.
*/
SimpleEnabler enabler;
/**
* The state at which we are computing an ample set.
*/
State theState;
/**
* The number of processes in the state. Note some of the processes may have
* terminated or may be {@code null}.
*/
int nprocs;
/**
* A reasoner with context the path condition of the state.
*/
Reasoner reasoner;
/**
* The evaluator used to evaluate expressions.
*/
Evaluator evaluator;
/**
* The factory used to create new states. This is needed when analyzing
* transitions that involve a function call.
*/
StateFactory stateFactory;
/**
* A utility class for analyzing and manipulating symbolic expressions
* specific to how they are used in CIVL-C.
*/
SymbolicUtility symbolicUtil;
/**
* Factory for creating and manipulating CIVL types.
*/
CIVLTypeFactory typeFactory;
/**
* The value type (symbolic type) of a heap. A symbolic expression
* representing the current state of a heap will have this type.
*/
SymbolicType heapSymbolicType;
/**
* The value type for a pointer. All symbolic expressions representing a
* pointer value will have this type.
*/
SymbolicType pointerSymbolicType;
/**
* The symbolic universe used to create and manipulate symbolic expressions.
*/
SymbolicUniverse universe;
/**
* The guard values of the statements emanating from the current locations
* of the processes. Value in position [i][j] is the result of evaluating
* the guard of statement j of process i. These are initially {@code null}
* but are filled in as values are requested.
*/
BooleanExpression[][] theGuards;
/**
* The transitions enabled in each process. Ragged array of length nprocs.
*/
Transition[][] enabledTransitions;
/**
* After the ample set is computed, this flag tells you whether the ample
* set is the full set of enabled transitions.
*/
boolean full = false;
/**
* The set of transitions which form an ample set. The objective of this
* class is to compute this set.
*/
Transition[] ampleSet = null;
// Constructor...
/**
* Creates a new worker. Initializes all fields.
*
* @param enabler
* the {@link SimpleEnabler} that is creating this worker
* @param state
* the {@link State} that this worker has been created to
* analyze
*/
SimpleEnablerWorker(SimpleEnabler enabler, State state) {
this.enabler = enabler;
this.evaluator = enabler.evaluator;
this.typeFactory = evaluator.modelFactory().typeFactory();
this.stateFactory = evaluator.stateFactory();
this.symbolicUtil = evaluator.symbolicUtility();
this.heapSymbolicType = typeFactory.heapSymbolicType();
this.pointerSymbolicType = typeFactory.pointerSymbolicType();
this.universe = evaluator.universe();
this.reasoner = universe.reasoner(state.getPathCondition(universe));
this.nprocs = state.numProcs();
this.theGuards = new BooleanExpression[nprocs][];
this.enabledTransitions = new Transition[nprocs][];
this.theState = state;
this.nprocs = theState.numProcs();
}
// Private methods...
/**
* Adds a dyscope ID - variable pair to the given {@link SeqSet}
* {@code result}, with some exceptions. If {@code variable} is
* {@code null}, or is an input variable, or is the atomic lock variable, or
* is a heap, this method is a no-op. Otherwise the pair is added to
* {@code result}.
*
* @param result
* the {@code SeqSet} to which the pair will be added
* @param dyid
* the ID number of a dynamic scope in {@link #theState}
* @param variable
* a {@code Variable} that resides in the static scope
* corresponding to the dynamic scope {@code dyid}
*/
private void addVariable(SeqSet result, int dyid, Variable variable) {
if (variable == null || variable.isInput()
|| variable == enabler.atomicLockVariable
|| variable.type().isHeapType())
return;
int vid = variable.vid();
assert vid >= 0;
result.add(dyid, vid);
}
/**
* Adds a variable instance to a set of objects. The set represents a set of
* objects that exists at a certain state. A variable instance is
* represented as a pair (d,v), where d is the dynamic scope ID and v is the
* variable.
*
* <p>
* A variable can be instantiated multiple (or 0) times because it is
* instantiated each time control in some process enters the variable's
* scope. Because of recursion and multiple processes, many instances of the
* variable may exist in the given state. The particular instance is
* specified by the state, pid, and variable. In the given state, there is
* at most one "visible" instance of the variable from the specified
* process: the top frame of the process's call stack points to a dynamic
* scope. If the variable exists in that scope, that is the instance, else
* the parent dynamic scope is examined, and so on until the variable is
* either found or the root dynamic scope is reached. When a variable is
* used in an expression, this is how the instance of the variable is found.
* </p>
*
* <p>
* If an instance of the variable is not found, this will be a no-op. (This
* may happen when evaluating contract expressions in the next state (the
* state after the call), because the next state has a new dyscope
* corresponding to the function call and the expressions are evaluated in
* that new dyscope.) If the variable instance is already in the given set,
* this will be a no-op.
* </p>
*
* <p>
* Certain variables are ignored and will not be added. Currently there are:
* the atomic lock variable. Cases where dyscope ID < 0 are also ignored.
* E.g., if a function type has an array type in which the length n is also
* a formal parameter, then the function identifier will have a reference to
* n in its type. n does not exist until the function is called, so the
* dyscope ID of n is undefined, which is -2.
* </p>
*
* @param result
* the set to which the variable should be added
* @param state
* the state in which this variable instance exists
* @param pid
* the ID of the process which references this variable
* @param variable
* the (static) variable to search for
*/
private void addVariable(SeqSet result, State state, int pid,
Variable variable) {
if (variable == null || variable == enabler.atomicLockVariable)
return;
int dyid = state.getDyscopeID(pid, variable);
if (dyid < 0 || dyid >= theState.numDyscopes())
return;
addVariable(result, dyid, variable);
}
/**
* <p>
* Adds to {@code result} an over-approximation to the set of memory
* locations pointed to by a pointer value. The pointer value specifies a
* sub-object (which may the whole object) of an object that exists in a
* state. An object is either a variable instance or the object that is
* created by a single call to malloc. This method will find and add the
* entire object to the given set {@code result}.
* </p>
*
* <p>
* If the object does not exist at the given state (because it is not in
* scope), this is a no-op. If the object is already in {@code result}, this
* is a no-op. If the pointer value is the NULL pointer or undefined, this
* is a no-op.
* </p>
*
* @param result
* the set to which the memory locations should be added
* @param state
* the state in which the pointer is evaluated
* @param source
* source information used for error-reporting; should be
* the piece of source code that was evaluated to yield
* the pointer value
* @param pointer
* a non-null pointer value
* @throws NoReductionException
* if the pointer is not concrete, and
* therefore no reasonable over-estimate of
* the pointed-to objects can be made
*/
private void addPointer(SeqSet result, State state, CIVLSource source,
SymbolicExpression pointer) throws NoReductionException {
assert pointer.type() == typeFactory.pointerSymbolicType();
if (pointer == symbolicUtil.nullPointer()
|| pointer == symbolicUtil.undefinedPointer())
return;
if (pointer.operator() != SymbolicOperator.TUPLE)
throw new NoReductionException();
int dyscopeID = stateFactory
.getDyscopeId(symbolicUtil.getScopeValue(pointer));
// as in the case of addVariable, ignore new dyscopes from
// contracts...
if (dyscopeID < 0 || dyscopeID >= theState.numDyscopes())
return;
int variableID = symbolicUtil.getVariableId(source, pointer);
assert (variableID >= 0); // can a variable have a negative ID?
// note: every dyscope has a heap, which is variable ID 0
SymbolicExpression object = state.getVariableValue(dyscopeID,
variableID);
if (object.type() != heapSymbolicType) {
Scope scope = state.getDyscope(dyscopeID).lexicalScope();
Variable var = scope.variable(variableID);
addVariable(result, dyscopeID, var);
} else { // ... of arrayElementRef of tupleComponentRef of IdentityRef
ReferenceExpression ref = symbolicUtil.getSymRef(pointer);
ReferenceExpression ref1 = ref, ref2 = null, ref3 = null;
while (ref1 instanceof NTReferenceExpression) {
ref3 = ref2;
ref2 = ref1;
ref1 = ((NTReferenceExpression) ref1).getParent();
}
assert ref1.referenceKind() == ReferenceKind.IDENTITY;
assert ref2 instanceof TupleComponentReference;
assert ref3 instanceof ArrayElementReference;
int mallocIndex = ((TupleComponentReference) ref2).getIndex()
.getInt();
NumericExpression objectIndex = ((ArrayElementReference) ref3)
.getIndex();
IntegerNumber objectNumber = (IntegerNumber) universe
.extractNumber(objectIndex);
if (objectNumber == null)
result.add(dyscopeID, variableID, mallocIndex);
else
result.add(dyscopeID, variableID, mallocIndex,
objectNumber.intValue());
}
}
/**
* <p>
* Does a symbolic type {@code type}, contain, as a sub-type, the pointer
* type {@link #pointerSymbolicType}?
* </p>
*
* <p>
* Note: it would be better if there were a way to do this once, when the
* symbolic type is created. This may have to be implemented in SARL. Also:
* for now we are not using this method, instead relying on CIVL types to
* answer this question. But it would be more accurate to use the symbolic
* type.
* </p>
*
* @param type
* any symbolic type
* @return {@code true} iff the pointer type occurs as a sub-type of
* {@code type} (including {@code type} itself)
*/
@SuppressWarnings("unused")
private boolean containsPointer(SymbolicType type) {
if (type == pointerSymbolicType)
return true;
switch (type.typeKind()) {
case ARRAY :
return containsPointer(((SymbolicArrayType) type).baseType());
case FUNCTION : {
SymbolicFunctionType ftype = (SymbolicFunctionType) type;
return containsPointer(ftype.outputType());
}
case MAP : {
SymbolicMapType mtype = (SymbolicMapType) type;
return containsPointer(mtype.keyType())
|| containsPointer(mtype.valueType());
}
case SET :
return containsPointer(((SymbolicSetType) type).elementType());
case TUPLE :
for (SymbolicType ftype : ((SymbolicTupleType) type).sequence())
if (containsPointer(ftype))
return true;
return false;
case UNION :
for (SymbolicType ftype : ((SymbolicUnionType) type).sequence())
if (containsPointer(ftype))
return true;
return false;
case BOOLEAN :
case CHAR :
case INTEGER :
case REAL :
case UNINTERPRETED :
}
return false;
}
/**
* Determines whether an object has a static CIVL type which contains a
* reference type as a sub-type. By reference type, we mean either the
* pointer type or the {@code $mem} type.
*
* @param state
* a {@link State} of the model
* @param obj
* an integer sequence identifying an object in state
* {@code state}
* @return {@code true} iff the variable or heap-allocated object identified
* by {@code obj} has a static type which contains the CIVL pointer
* or {@code $mem} type as a sub-type
*/
private boolean containsPointerType(State state, int[] obj) {
int len = obj.length, dyid = obj[0], vid = obj[1];
DynamicScope ds = state.getDyscope(dyid);
Variable var = ds.lexicalScope().variable(vid);
CIVLType type = var.type();
if (len == 2)
return type.hasReferences();
assert type.isHeapType();
CIVLType elementType = ((CIVLHeapType) type).getMalloc(obj[2])
.getStaticElementType();
return elementType.hasReferences();
}
/**
* Finds all symbolic expressions occurring within a symbolic type, adding
* them to {@code result}. These symbolic expressions are necessarily of
* integer type, occurring as length expressions in array types.
*
* @param result
* the collection to which the symbolic expressions will
* be added
* @param type
* the type to be searched for symbolic expressions
*/
private void getExpressionsInType(Collection<SymbolicExpression> result,
SymbolicType type) {
switch (type.typeKind()) {
case ARRAY :
getExpressionsInType(result,
((SymbolicArrayType) type).baseType());
if (type instanceof SymbolicCompleteArrayType)
result.add(((SymbolicCompleteArrayType) type).extent());
break;
case FUNCTION : {
SymbolicFunctionType ftype = (SymbolicFunctionType) type;
getExpressionsInType(result, ftype.outputType());
for (SymbolicType itype : ftype.inputTypes())
getExpressionsInType(result, itype);
break;
}
case MAP : {
SymbolicMapType mtype = (SymbolicMapType) type;
getExpressionsInType(result, mtype.keyType());
getExpressionsInType(result, mtype.valueType());
break;
}
case SET :
getExpressionsInType(result,
((SymbolicSetType) type).elementType());
break;
case TUPLE :
for (SymbolicType ftype : ((SymbolicTupleType) type).sequence())
getExpressionsInType(result, ftype);
break;
case UNION :
for (SymbolicType ftype : ((SymbolicUnionType) type).sequence())
getExpressionsInType(result, ftype);
break;
case BOOLEAN :
case CHAR :
case INTEGER :
case REAL :
case UNINTERPRETED :
// no pointers, nothing to do
}
}
/**
* Computes over-approximation of set of objects that could be pointed to by
* some component of the given value.
*
* @param result
* set to which the objects will be added
* @param state
* the state in which the value exists
* @param source
* source code info for error reporting; should correspond
* to the expression that evaluated to {@code value}
* @param value
* the value to search for pointers
* @throws NoReductionException
* if a pointer found in {@code value} is
* not concrete
*/
private void getPointedObjects(SeqSet result, State state,
CIVLSource source, SymbolicExpression value)
throws NoReductionException {
Stack<SymbolicExpression> worklist = new Stack<>();
worklist.push(value);
while (!worklist.isEmpty()) {
SymbolicExpression expr = worklist.pop();
SymbolicType type = expr.type();
if (type == null) {// a NULL object has null type, ignore
} else if (expr.operator() == SymbolicOperator.APPLY
&& expr.argument(0) == enabler.hideFunction) {
// do nothing. This is a special abstract function used
// to hide pointers from this reachability analysis
} else if (type == pointerSymbolicType) {
addPointer(result, state, source, expr);
} else if (expr.operator() == SymbolicOperator.SYMBOLIC_CONSTANT) {
// if (((StringObject) expr.argument(0)).getString()
// .startsWith(havocPrefix)) {
/*
* do nothing. temporary hack. these are the "Y" symbolic
* constants used to initialize an uninitialized variable, and
* also used by havoc. we will assume for now they can't contain
* a pointer to anything. Same for inputs "X" and uninitialized
* heap cells "H".
*/
// } else if (containsPointer(type))
// throw new NoReductionException();
} else {
for (SymbolicObject obj : expr.getArguments()) {
switch (obj.symbolicObjectKind()) {
case EXPRESSION :
worklist.push((SymbolicExpression) obj);
break;
case TYPE :
getExpressionsInType(worklist, (SymbolicType) obj);
break;
case SEQUENCE :
for (SymbolicExpression se : (SymbolicSequence<?>) obj)
worklist.push(se);
break;
case TYPE_SEQUENCE :
for (SymbolicType stype : (SymbolicTypeSequence) obj)
getExpressionsInType(worklist, stype);
break;
case BOOLEAN :
case CHAR :
case INT :
case NUMBER :
case STRING :
// no pointers, nothing to do
}
}
}
}
}
/**
* Gets the value of an object in the specified state. The object is
* specified by a sequence of integers. If the object is a regular variable,
* the sequence consists of two integers: the dynamic scope ID and the
* variable ID. If the object is heap-allocated, the sequence consists of 4
* integers: ID of the dynamic scope containing the heap, the variable ID of
* the heap variable in that scope, the row ID (corresponding to the malloc
* statement) in the heap table, and the column ID (corresponding to a
* single malloc call) within that row.
*
* @param state
* the state in which the value of the object will be
* found
* @param objectID
* the sequence of integers specifying the object
* @return the value of the specified object in {@code state}
*/
private SymbolicExpression getValue(State state, int[] objectID) {
// dyscope, var; or dyscope, var, field, objID
int dyscopeID = objectID[0];
int variableID = objectID[1];
SymbolicExpression value = state.getVariableValue(dyscopeID,
variableID);
if (objectID.length == 2) {
return value;
} else {
assert objectID.length == 4;
int mallocID = objectID[2];
int objID = objectID[3];
SymbolicExpression row, result;
assert value.type() == heapSymbolicType;
if (value.operator() == SymbolicOperator.TUPLE)
row = (SymbolicExpression) value.argument(mallocID);
else
row = universe.tupleRead(value, universe.intObject(mallocID));
if (row.operator() == SymbolicOperator.ARRAY)
result = (SymbolicExpression) row.argument(objID);
else
result = universe.arrayRead(row, universe.integer(objID));
return result;
}
}
/**
* <p>
* Computes the set of objects that can be reached in one or more steps
* (pointer dereferences) from a given set of objects. There is a binary
* relation -> on the set of objects in a state: o1->o2 if o1 contains a
* pointer into some part of o2. Given a set of objects (specified as a
* {@link SeqSet}), this method will compute the set of objects that are
* reachable from the given set by traversing one or more edges of this
* relation.
* </p>
*
* <p>
* This method assumes that if an object's static type does not contain a
* pointer type, then the value of that object can never include a pointer
* value. This assumption is unsound if pointer values can be cast to
* non-pointer values, e.g., if a pointer is cast to a {@code double} and
* stored in a variable of type {@code double}. This is a known limitation.
* </p>
*
* @param result
* the result of the irreflexive transitive closure
* (out)
* @param objectSet
* the starting points; this set will not be modified
* (in)
* @param state
* the state
* @param source
* source object for this operation
* @throws NoReductionException
* if no over-approximation of the result
* can be obtained
*/
private void closeIrreflexive(SeqSet result, SeqSet objectSet, State state,
CIVLSource source) throws NoReductionException {
LinkedList<int[]> workset = new LinkedList<>();
for (int[] leaf : objectSet.getLeaves()) {
if (containsPointerType(state, leaf))
workset.add(leaf);
}
while (!workset.isEmpty()) {
int[] objId = workset.remove();
SymbolicExpression value = getValue(state, objId);
SeqSet pointedObjects = new SeqSet();
getPointedObjects(pointedObjects, state, source, value);
for (int[] pObj : pointedObjects.getLeaves())
if (result.add(pObj) && containsPointerType(state, pObj))
workset.add(pObj);
}
}
/**
* Finds all objects of a state that can be reached in one or more steps
* from the given set of variables, under the binary relation -> on the set
* of objects, where o1->o2 if o1 contains a pointer into some part of o2.
* Ignores variables that should be ignored according to the rules laid out
* in {@link #addVariable(SeqSet, int, Variable)}.
*
* @param state
* the state which specifies the values of all objects
* @param pid
* the ID of the process which is referencing the
* variables; used together with {@code state} to
* determine the variable instances and the values stored
* @param source
* a source info object used for reporting errors
* @param vars
* the set of variables which form the starting point of
* the search
* @return the set of reachable objects, represented as a {@link SeqSet}
*/
private SeqSet findReachableIrreflexive(State state, int pid,
CIVLSource source, Set<Variable> vars) throws NoReductionException {
SeqSet input = new SeqSet(), result = new SeqSet();
for (Variable var : vars)
addVariable(input, state, pid, var);
closeIrreflexive(result, input, state, source);
return result;
}
/**
* <p>
* Computes the dependencies of a function call in the case where the
* function has a contract with a "depends_on" clause. An implemented or
* system function may have a function contract, and that contract may
* include one or more "depends_on" clauses. These clauses specify "access",
* "read" or "write" events, each of which has an argument of pointer type.
* These arguments may refer to the formal parameters of the function. The
* actual arguments of the function call are evaluated, the formal
* parameters are assigned the corresponding values, and then the depends_on
* expressions are evaluated to yield a set of pointer values. The objects
* pointed to by these pointer values are collected into the set returned.
* </p>
*
* <p>
* The differences between "access", "read", and "write" are currently
* ignored. All three are treated the same.
* </p>
*
* <p>
* Missing depends clauses: a missing depends clause is interpreted to mean
* nothing, i.e., the function could depend on anything. It is equivalent to
* specifying the universal set consisting of all memory locations for the
* depends clause.
* </p>
*
*
* <p>
* Behaviors: for a contract with multiple behaviors, the effective depends
* clause is the intersection of the depends sets of the enabled behaviors.
* Rationale: similar to the case of assigns clauses in ACSL, to say a
* statement S depends on X really means it is independent of all statements
* in the complement of X. If multiple behaviors are enabled, then all of
* the claims encoded by those behaviors should hold, i.e., S is independent
* of all statements in the union of the complements of the X_i, i.e., X
* depends on the the intersection of the X_i.
* </p>
*
* TODO: need to support depends_on(a[0..n-1]) which is equivalent to
* depends_on(a[0], ..., a[n-1]). Where a is an array of pointers.
* a[0..n-1][0..1] where a is an array of array of pointers.
*
* @param result
* the set into which the dependent object of the call
* will be added
* @param state
* the state from which the function is called
* @param pid
* the ID of the process making the call
* @param statement
* the call statement
* @return <code>true</code> if the function has an enabled depends_on
* clause at {@code state}, <code>false</code> otherwise. In the
* case of {@code false} being returned, the <code>result</code> is
* not modified
* @throws UnsatisfiablePathConditionException
* if in the course of
* evaluating some
* expression it is
* discovered that the path
* condition of
* {@code state} is
* unsatisfiable
* @throws NoReductionException
* if the called function is
* a system function or
* atomic function, but no
* depends_on clause is
* specified
*/
private boolean memFromContract(SeqSet result, State state, int pid,
CallOrSpawnStatement statement)
throws UnsatisfiablePathConditionException, NoReductionException {
CIVLFunction function = enabler.getFunction(state, pid, statement);
if (function.isPureFunction())
return true; // no dependencies
FunctionContract contract = function.functionContract();
if (contract == null)
return false;
State newState = null; // after executing the call
SeqSet otherSet = null, dependSet = null;
/*
* otherSet contains ancillary references, such as the variables
* occurring in the assumes and depends_on clauses. For these, the union
* is taken over all behaviors. dependSet contains the actual objects
* pointed to by the depends_on clause. For these, the intersection is
* taken over all behaviors. The final result is the union of these two
* sets, but the result is only used if there is at least one enabled
* depends_on clause.
*/
if (contract.hasDependsClause()) { // process the default behavior
FunctionBehavior behavior0 = contract.defaultBehavior();
if (behavior0 == null) {
// nothing known
} else if (behavior0.dependsNoact()) { // depends_on \nothing
return true;
} else if (behavior0.numDependsEvents() == 0) {
// nothing known
} else { // there are some depends_on clauses
dependSet = new SeqSet();
otherSet = new SeqSet();
newState = enabler.executeContract(state, pid, function,
statement.arguments());
for (DependsEvent event : behavior0.dependsEvents()) {
if (event instanceof MemoryEvent) {
MemoryEvent memEvent = (MemoryEvent) event;
Set<Expression> memSet = memEvent.memoryUnits();
for (Expression expr : memSet) {
SymbolicExpression pointer = evaluator
.evaluate(newState, pid, expr).value;
assert pointer.type() == typeFactory
.pointerSymbolicType();
addPointer(dependSet, newState, expr.getSource(),
pointer);
findObjects(otherSet, newState, pid, expr);
}
}
}
}
}
for (NamedFunctionBehavior behavior : contract.namedBehaviors()) {
Expression assumption = behavior.assumptions();
if (assumption != null) {
if (otherSet == null)
otherSet = new SeqSet();
if (newState == null)
newState = enabler.executeContract(state, pid, function,
statement.arguments());
findObjects(otherSet, newState, pid, assumption);
BooleanExpression assumptionValue = (BooleanExpression) evaluator
.evaluate(newState, pid, assumption).value;
if (reasoner.isValid(assumptionValue)) {
if (behavior.dependsNoact()) { // depends_on \nothing
if (dependSet == null)
dependSet = new SeqSet();
dependSet.clear();
} else if (behavior.numDependsEvents() == 0) {
// nothing known
} else { // there are some depends_on clauses
// new depend set will be intersection with old...
SeqSet newDependSet = new SeqSet();
if (newState == null)
newState = enabler.executeContract(state, pid,
function, statement.arguments());
for (DependsEvent event : behavior.dependsEvents()) {
if (event instanceof MemoryEvent) {
MemoryEvent memEvent = (MemoryEvent) event;
Set<Expression> memSet = memEvent.memoryUnits();
for (Expression expr : memSet) {
SymbolicExpression pointer = evaluator
.evaluate(newState, pid,
expr).value;
SeqSet ptrSet = new SeqSet();
assert pointer.type() == typeFactory
.pointerSymbolicType();
addPointer(ptrSet, newState,
expr.getSource(), pointer);
if (dependSet == null
|| dependSet.containsAll(ptrSet))
newDependSet.addAll(ptrSet);
findObjects(otherSet, newState, pid, expr);
}
}
}
dependSet = newDependSet;
}
}
}
} // end loop over named behaviors
if (dependSet != null) {
if (otherSet != null)
result.addAll(otherSet);
result.addAll(dependSet);
return true;
}
return false;
}
/**
* Finds all objects referenced in a {@link MemoryUnitReference}, adding
* them to the specified {@code SeqSet}.
*
* @param result
* the set to which the objects should be added
* @param state
* the state to which the memory unit reference applies
* @param pid
* the ID of the process containing the memory unit
* reference
* @param ref
* the memory unit reference
* @throws UnsatisfiablePathConditionException
* if in the course of
* evaluating, it is
* determined that the path
* condition of
* {@code state} is
* unsatisfiable
* @throws NoReductionException
* if a non-concrete pointer
* is encountered
*/
private void findObjects(SeqSet result, State state, int pid,
MemoryUnitReference ref)
throws UnsatisfiablePathConditionException, NoReductionException {
if (ref == null)
return;
if (ref instanceof ArraySliceReference)
findObjects(result, state, pid,
((ArraySliceReference) ref).index());
findObjects(result, state, pid, ref.child());
}
/**
* Computes an over-approximation of the set of objects accessed (read or
* modified) by executing a statement.
*
* @param resultAll
* the set to which the computed set of all objects
* will be added (out variable)
* @param resultRO
* the set to which the computed set of read-only
* objects will be added (out variable)
* @param state
* the state from which the statement is executed
* @param pid
* the ID of the process executing the statement
* @param statement
* the statement being executed
* @throws UnsatisfiablePathConditionException
* if in the course of this
* computation it is
* discovered that
* {@code state} has an
* unsatisfiable path
* condition
* @throws NoReductionException
* if a non-concrete pointer
* is encountered
*/
private void computeMem(SeqSet resultAll, SeqSet resultWrite, State state,
int pid, Statement statement)
throws UnsatisfiablePathConditionException, NoReductionException {
StatementKind kind = statement.statementKind();
switch (kind) {
case ASSIGN : {
if (statement instanceof AtomicLockAssignStatement) {
AtomicLockAssignStatement as = (AtomicLockAssignStatement) statement;
if (as.enterAtomic())
computeMemAtomicBlock(resultAll, resultWrite, state,
pid, as);
} else {
AssignStatement as = (AssignStatement) statement;
findAccessesLHS(resultAll, resultWrite, state, pid,
as.getLhs());
findObjects(resultAll, state, pid, as.rhs());
}
break;
}
case CALL_OR_SPAWN : {
CallOrSpawnStatement cs = (CallOrSpawnStatement) statement;
if (cs.isSpawn() && enabler.config.getProcBound() > 0) {
throw new NoReductionException();
} else if (enabler.isYield(cs)) {
if (stateFactory.processInAtomic(state) != pid) {
// second part of $yield: this proc re-obtains
// atomic lock. For now, say depends on everything.
// TODO: eventually do same thing we do for atomic-enter
throw new NoReductionException();
} // else: first part of $yield: no dependencies
} else {
findObjects(resultAll, state, pid, cs.functionExpression());
for (Expression arg : cs.arguments())
findObjects(resultAll, state, pid, arg);
if (cs.lhs() != null) {
findAccessesLHS(resultAll, resultWrite, state, pid,
cs.lhs());
}
CIVLFunction function = enabler.getFunction(state, pid, cs);
if (function.isAtomicFunction()
|| function.isSystemFunction()) {
SeqSet tmpSet = new SeqSet();
if (memFromContract(tmpSet, state, pid, cs)) {
resultAll.addAll(tmpSet);
resultWrite.addAll(tmpSet);
} else if (function.startLocation() != null) {
computeMemAtomicFunction(resultAll, resultWrite,
state, pid, cs.function(), cs.arguments());
} else
throw new NoReductionException();
}
}
break;
}
case CIVL_PAR_FOR_ENTER : {
CivlParForSpawnStatement ps = (CivlParForSpawnStatement) statement;
findObjects(resultAll, state, pid, ps.domain());
findObjects(resultAll, state, pid, ps.domSizeVar());
findObjects(resultAll, state, pid, ps.parProcsVar());
break;
}
case DOMAIN_ITERATOR : {
DomainIteratorStatement ds = (DomainIteratorStatement) statement;
findObjects(resultAll, state, pid, ds.domain());
// don't think these are needed...
// computeObjectsIn(result, pid, ds.getLiteralDomCounter());
// computeObjectsIn(result, pid, ds.loopVariables());
break;
}
case MALLOC : {
MallocStatement ms = (MallocStatement) statement;
findObjects(resultAll, state, pid, ms.getScopeExpression());
findObjects(resultAll, state, pid, ms.getSizeExpression());
findAccessesLHS(resultAll, resultWrite, state, pid,
ms.getLHS());
break;
}
case NOOP :
break; // nothing to do
case PARALLEL_ASSIGN : {
ParallelAssignStatement ps = (ParallelAssignStatement) statement;
for (Pair<LHSExpression, Expression> pair : ps.assignments()) {
findObjects(resultAll, state, pid, pair.left);
findAccessesLHS(resultAll, resultWrite, state, pid,
pair.left);
findObjects(resultAll, state, pid, pair.right);
}
break;
}
case RETURN : {
ReturnStatement rs = (ReturnStatement) statement;
findObjects(resultAll, state, pid, rs.expression());
break;
}
case UPDATE : {
UpdateStatement us = (UpdateStatement) statement;
for (Expression arg : us.arguments()) {
findObjects(resultAll, state, pid, arg);
}
findObjects(resultAll, state, pid, us.collator());
computeMem(resultAll, resultWrite, state, pid, us.call());
break;
}
case WITH : {
WithStatement ws = (WithStatement) statement;
findObjects(resultAll, state, pid, ws.collateState());
break;
}
default :
throw new CIVLInternalException("unknown statement kind",
statement);
}
}
/**
* Computes over-approximation to set of object accesses within an atomic
* block or function.
*
* @param resultAll
* set of objects which could be accessed (out)
* @param resultWrite
* set of objects which could be accessed by writes
* (out)
* @param state
* the state in which the objects reside (in)
* @param pid
* the ID of the executing process (in)
* @param start
* the start location of the atomic block or function
* (in)
* @param vars
* the set of variables (in scope for process
* {@code pid} at state {@code state}) accessed
* within the atomic block or function, including
* through function calls, calls made by those
* functions, etc. (in)
* @throws NoReductionException
* if it is determined that the path
* condition of {@code state} is
* unsatisfiable
*/
private void computeAccessesAtomic(SeqSet resultAll, SeqSet resultWrite,
State state, int pid, Location start, Set<Variable> vars)
throws NoReductionException {
if (vars == null)
throw new NoReductionException();
Set<Variable> varsWrite = start.writableVariables();
// all variables occurring in the atomic section are accessible:
for (Variable var : vars)
addVariable(resultAll, state, pid, var);
// only writable variables occurring in the atomic block are writable
// by this transition:
varsWrite.retainAll(vars);
for (Variable var : varsWrite)
addVariable(resultWrite, state, pid, var);
// anything that can be reached in one or more steps by pointer
// dereference from any variable is potentially writable...
SeqSet tmpSet = findReachableIrreflexive(state, pid, start.getSource(),
vars);
resultAll.addAll(tmpSet);
resultWrite.addAll(tmpSet);
}
/**
* <p>
* Computes an over-approximation of the set of pre-existing objects
* accessed by executing an atomic statement. (The atomic statement may
* allocate and access new memory, but these are not included in this
* computation.)
* </p>
*
* <p>
* Current implementation: all objects reachable from variables that occur
* within the atomic region (which includes functions called within the
* atomic block, functions called by those functions, etc.). Here, "atomic
* region" includes a "begin local ... end local" section of code, but by
* definition of local, such code depends on nothing.
* </p>
*
* @param resultAll
* set of objects which could be accessed (out)
* @param resultWrite
* set of objects which could be accessed by writes
* (out)
* @param state
* the state from which the atomic statement is
* executed
* @param pid
* process ID for the process executing the atomic
* statement
* @param as
* the {@link Statement} that marks the entrance to
* the atomic statement by obtaining the atomic lock
* @throws NoReductionException
* if no upper bound on the set of objects
* can be found
*/
private void computeMemAtomicBlock(SeqSet resultAll, SeqSet resultWrite,
State state, int pid, AtomicLockAssignStatement as)
throws NoReductionException {
if (as.source().isEntryOfLocalBlock())
// begin_local ... end_local: depends on nothing
return;
computeAccessesAtomic(resultAll, resultWrite, state, pid, as.source(),
as.getVariables());
}
/**
* Computes over-approximation of the objects accessed by a call to an
* atomic, defined (non-system) function.
*
* @param resultAll
* objects that could be accessed (out)
* @param resultWrite
* objects that could be accessed by a write (out)
* @param state
* state from which the call is made (in)
* @param pid
* ID of the process making the call (in)
* @param function
* the atomic function being called
* @param arguments
* the arguments in the call expression
* @throws NoReductionException
* if no good approximation
* to the resulting sets can
* be obtained
* @throws UnsatisfiablePathConditionException
* if it is determined that
* the path condition of
* {@code state} is
* unsatisfiable
*/
private void computeMemAtomicFunction(SeqSet resultAll, SeqSet resultWrite,
State state, int pid, CIVLFunction function,
List<Expression> arguments)
throws NoReductionException, UnsatisfiablePathConditionException {
assert function.isAtomicFunction() && function.startLocation() != null;
State newState = enabler.executeCall(state, pid, function, arguments);
computeAccessesAtomic(resultAll, resultWrite, newState, pid,
function.startLocation(), function.getAccessesAtomicFunction());
}
/**
* Analyzes the object accesses associated to the left-hand side of an
* assignment {@code lhs = ...}. If {@code lhs} is a variable {@code x},
* then {@code x} is accessed as a write. If {@code lhs} is a dereference
* expression {@code *p}, where {@code p} is an expression, then all
* accessed arising from the evaluation of {@code p} occur, and in addition
* a write access to the object pointed to by the pointer value resulting
* from evaluating {@code p} occurs. And so on.
*
* @param resultAll
* the set of objects accessed (out)
* @param resultWrite
* the set of objects accessed by writing (out)
* @param state
* the state at which the assignment takes place
* @param pid
* the ID of the process performing the assignment
* @param lhs
* the left hand side expression of the assignment
* @throws NoReductionException
* if no good approximation
* can be obtained
* @throws UnsatisfiablePathConditionException
* if it is determined that
* the path condition of
* {@code state} is
* unsatisfiable
*/
private void findAccessesLHS(SeqSet resultAll, SeqSet resultWrite,
State state, int pid, LHSExpression lhs)
throws NoReductionException, UnsatisfiablePathConditionException {
switch (lhs.lhsExpressionKind()) {
case DEREFERENCE : { // *p = e;
// evaluate p and find the object o into which it points,
// add o to resultWrite
Expression pointerArg = ((DereferenceExpression) lhs).pointer();
SymbolicExpression pointerVal = coarsePointerEval(state, pid,
pointerArg);
CIVLSource source = pointerArg.getSource();
findObjects(resultAll, state, pid, pointerArg);
addPointer(resultAll, state, source, pointerVal);
addPointer(resultWrite, state, source, pointerVal);
break;
}
case DOT : { // s.f = ...;
LHSExpression struct = (LHSExpression) ((DotExpression) lhs)
.structOrUnion();
findAccessesLHS(resultAll, resultWrite, state, pid, struct);
break;
}
case SUBSCRIPT : { // a[i] = ...;
SubscriptExpression sub = (SubscriptExpression) lhs;
LHSExpression array = sub.array();
Expression index = sub.index();
findAccessesLHS(resultAll, resultWrite, state, pid, array);
findObjects(resultAll, state, pid, index);
break;
}
case VARIABLE : {
Variable var = ((VariableExpression) lhs).variable();
addVariable(resultAll, state, pid, var);
addVariable(resultWrite, state, pid, var);
break;
}
default :
throw new CIVLInternalException("unreachable", lhs);
}
}
/**
* Computes an over-approximation of the set of objects accessed by
* evaluating an expression of the form {@code &lhs}. If {@code lhs} is a
* variable, no objects are accessed: the variable is neither read nor
* written. If {@code lhs} has the form {@code *p} the result is the set of
* objects accessed in the course of evaluating {@code p}, but not the
* objected pointed to by the result of that evaluation, as that object is
* neither read nor modified. And so on.
*
* @param result
* the set to which the memory locations should be added
* @param state
* the state in which the expression {@code arg} occurs
* @param pid
* process ID for the process evaluating the expression
* @param arg
* the argument to the address-of operator
* @throws UnsatisfiablePathConditionException
* if it is discovered that
* the path condition of
* {@code state} is
* unsatisfiable
* @throws NoReductionException
* if no good
* over-approximation can be
* found
*/
private void findObjectsLHS(SeqSet result, State state, int pid,
LHSExpression arg)
throws UnsatisfiablePathConditionException, NoReductionException {
switch (arg.lhsExpressionKind()) {
case DEREFERENCE :
// evaluating &*e accesses the memory locations accessed when
// evaluating e
findObjects(result, state, pid,
((DereferenceExpression) arg).pointer());
break;
case DOT : {
// evaluating &e.f accesses the memory locations accessed when
// evaluating &e
LHSExpression struct = (LHSExpression) ((DotExpression) arg)
.structOrUnion();
findObjectsLHS(result, state, pid, struct);
break;
}
case SUBSCRIPT : {
// evaluating &e[f] accesses the memory locations accessed
// when evaluating &e and f
SubscriptExpression sub = (SubscriptExpression) arg;
LHSExpression array = sub.array();
Expression index = sub.index();
findObjectsLHS(result, state, pid, array);
findObjects(result, state, pid, index);
break;
}
case VARIABLE : // evaluating &x does not access any memory location
break;
default :
throw new CIVLInternalException("Unknown kind of LExpression",
arg);
}
}
/**
* Evaluates a pointer expression to get some pointer into the object
* pointed to. If the expression contains bound variables this might make it
* impossible to evaluate and the no-reduction exception is thrown.
*
* @param state
* a state
* @param pid
* ID of process evaluating the pointer expression
* @param expr
* an expression of pointer type
* @return pointer to the object pointed to, though not necessarily the
* exact location within that object
* @throws NoReductionException
* if it is not possible to evaluate the
* pointer expression
*/
private SymbolicExpression coarsePointerEval(State state, int pid,
Expression expr) throws NoReductionException {
ExpressionKind kind = expr.expressionKind();
if (kind == ExpressionKind.BINARY) {
BinaryExpression be = (BinaryExpression) expr;
BINARY_OPERATOR op = be.operator();
if (op == BINARY_OPERATOR.POINTER_ADD) {
Expression arg0 = be.left();
return arg0.getExpressionType().isPointerType()
? coarsePointerEval(state, pid, arg0)
: coarsePointerEval(state, pid, be.right());
} else if (op == BINARY_OPERATOR.POINTER_SUBTRACT)
return coarsePointerEval(state, pid, be.left());
}
try {
return evaluator.evaluate(state, pid, expr).value;
} catch (Exception e) {
throw new NoReductionException();
}
}
/**
* Computes an over-approximation to the set of objects accessed when
* evaluating an expression.
*
* @param result
* the (non-null) set to which the memory locations
* referenced in {@code expr} will be added
* @param state
* the state in which the evaluation occurs
* @param pid
* the process ID number for the process that is
* evaluating {@code expr}
* @param expr
* the expression being evaluated. may be {@code null}, in
* which case this is a no-op
* @throws UnsatisfiablePathConditionException
* if in the course of
* evaluating {@code expr}
* it is discovered that the
* path condition of the
* current state is not
* satisfiable
* @throws NoReductionException
* if no good
* over-approximation can be
* found
*/
private void findObjects(SeqSet result, State state, int pid,
Expression expr)
throws UnsatisfiablePathConditionException, NoReductionException {
if (expr == null)
return;
findObjects(result, state, pid, expr.getExpressionType());
switch (expr.expressionKind()) {
case ABSTRACT_FUNCTION_CALL :
for (Expression arg : ((AbstractFunctionCallExpression) expr)
.arguments())
findObjects(result, state, pid, arg);
break;
case ADDRESS_OF :
findObjectsLHS(result, state, pid,
((AddressOfExpression) expr).operand());
break;
case ARRAY_LAMBDA : {// (int[n])$lambda (int i,j,... | e) f
ArrayLambdaExpression ale = (ArrayLambdaExpression) expr;
for (Pair<List<Variable>, Expression> pair : ale
.boundVariableList())
findObjects(result, state, pid, pair.right);
findObjects(result, state, pid, ale.restriction());
findObjects(result, state, pid, ale.expression());
break;
}
case ARRAY_LITERAL :
for (Expression element : ((ArrayLiteralExpression) expr)
.elements())
findObjects(result, state, pid, element);
break;
case BINARY :
findObjects(result, state, pid,
((BinaryExpression) expr).left());
findObjects(result, state, pid,
((BinaryExpression) expr).right());
break;
case BOOLEAN_LITERAL : // nothing
break;
case BOUND_VARIABLE : // nothing
break;
case CAST :
findObjects(result, state, pid,
((CastExpression) expr).getExpression());
break;
case CHAR_LITERAL : // nothing
break;
case COND : {
ConditionalExpression cond = (ConditionalExpression) expr;
findObjects(result, state, pid, cond.getCondition());
findObjects(result, state, pid, cond.getTrueBranch());
findObjects(result, state, pid, cond.getFalseBranch());
break;
}
case DEREFERENCE : {
Expression pointerArg = ((DereferenceExpression) expr)
.pointer();
SymbolicExpression pointerVal = coarsePointerEval(state, pid,
pointerArg);
findObjects(result, state, pid, pointerArg);
addPointer(result, state, pointerArg.getSource(), pointerVal);
break;
}
case DERIVATIVE : {
DerivativeCallExpression de = (DerivativeCallExpression) expr;
for (Expression arg : de.arguments())
findObjects(result, state, pid, arg);
break;
}
case DIFFERENTIABLE : {
DifferentiableExpression de = (DifferentiableExpression) expr;
for (Expression lb : de.lowerBounds())
findObjects(result, state, pid, lb);
for (Expression ub : de.upperBounds())
findObjects(result, state, pid, ub);
break;
}
case DOMAIN_GUARD : {
DomainGuardExpression dge = (DomainGuardExpression) expr;
int n = dge.dimension();
findObjects(result, state, pid, dge.domain());
for (int i = 0; i < n; i++)
addVariable(result, state, pid, dge.variableAt(i));
addVariable(result, state, pid, dge.getLiteralDomCounter());
break;
}
case DOT :
findObjects(result, state, pid,
((DotExpression) expr).structOrUnion());
break;
case DYNAMIC_TYPE_OF :
findObjects(result, state, pid,
((DynamicTypeOfExpression) expr).getType());
break;
case EXTENDED_QUANTIFIER : {
ExtendedQuantifiedExpression eqf = (ExtendedQuantifiedExpression) expr;
findObjects(result, state, pid, eqf.function());
findObjects(result, state, pid, eqf.lower());
findObjects(result, state, pid, eqf.higher());
break;
}
case FUNCTION_GUARD : {
FunctionGuardExpression fge = (FunctionGuardExpression) expr;
findObjects(result, state, pid, fge.functionExpression());
for (Expression arg : fge.arguments())
findObjects(result, state, pid, arg);
break;
}
case FUNCTION_IDENTIFIER : // nothing
break;
case FUNC_CALL : {// these are atomic, pure functions
CallOrSpawnStatement call = ((FunctionCallExpression) expr)
.callStatement();
findObjects(result, state, pid, call.functionExpression());
for (Expression arg : call.arguments())
findObjects(result, state, pid, arg);
assert call.lhs() == null;
// if (call.lhs() != null) {
// findObjects(result, state, pid, call.lhs());
// findObjectsLHS(result, state, pid, call.lhs());
// }
// memFromContract(result, state, pid, call);
break;
}
case HERE_OR_ROOT : // nothing
break;
case INITIAL_VALUE : // nothing - abstract initial value
break;
case INTEGER_LITERAL : // nothing
break;
case LAMBDA :
findObjects(result, state, pid,
((LambdaExpression) expr).lambdaFunction());
break;
case MEMORY_UNIT :
findObjects(result, state, pid,
((MemoryUnitExpression) expr).reference());
break;
case MPI_CONTRACT_EXPRESSION :
for (Expression arg : ((MPIContractExpression) expr)
.arguments())
findObjects(result, state, pid, arg);
break;
case NOTHING : // nothing
break;
case NULL_LITERAL : // nothing
break;
case PROC_NULL : // nothing
break;
case QUANTIFIER : {
QuantifiedExpression qe = (QuantifiedExpression) expr;
for (Pair<List<Variable>, Expression> pair : qe
.boundVariableList())
findObjects(result, state, pid, pair.right);
findObjects(result, state, pid, qe.expression());
findObjects(result, state, pid, qe.restriction());
break;
}
case REAL_LITERAL : // nothing
break;
case REC_DOMAIN_LITERAL : {
RecDomainLiteralExpression rdl = (RecDomainLiteralExpression) expr;
int n = rdl.dimension();
for (int i = 0; i < n; i++)
findObjects(result, state, pid, rdl.rangeAt(i));
break;
}
case REGULAR_RANGE : {
RegularRangeExpression rr = (RegularRangeExpression) expr;
findObjects(result, state, pid, rr.getLow());
findObjects(result, state, pid, rr.getHigh());
findObjects(result, state, pid, rr.getStep());
break;
}
case RESULT : // nothing
break;
case SCOPEOF :
findObjectsLHS(result, state, pid,
((ScopeofExpression) expr).argument());
break;
case SELF : // nothing
break;
case SIZEOF_EXPRESSION :
findObjects(result, state, pid, ((SizeofExpression) expr)
.getArgument().getExpressionType());
// this is what the evaluator does
break;
case SIZEOF_TYPE :
findObjects(result, state, pid,
((SizeofTypeExpression) expr).getTypeArgument());
break;
case STATE_NULL : // nothing
break;
case STRING_LITERAL : // nothing
break;
case STRUCT_OR_UNION_LITERAL :
// nothing. these have constant values only (see Evaluator)
break;
case SUBSCRIPT : {
SubscriptExpression se = (SubscriptExpression) expr;
findObjectsLHS(result, state, pid, se.array());
findObjects(result, state, pid, se.index());
break;
}
case SYSTEM_GUARD :
for (Expression arg : ((SystemGuardExpression) expr)
.arguments())
findObjects(result, state, pid, arg);
break;
case UNARY :
findObjects(result, state, pid,
((UnaryExpression) expr).operand());
break;
case UNDEFINED_PROC : // nothing
break;
case VALUE_AT : {
ValueAtExpression vae = (ValueAtExpression) expr;
findObjects(result, state, pid, vae.state());
findObjects(result, state, pid, vae.pid());
findObjects(result, state, pid, vae.expression());
break;
}
case VARIABLE :
addVariable(result, state, pid,
((VariableExpression) expr).variable());
break;
case WILDCARD : // nothing to do
break;
default :
break;
}
}
/**
* Computes an over-approximation to the set of objects referenced in a CIVL
* type. These object references would occur in array length expressions.
* Example: in the type {@code int[n]} the object {@code n} is referenced.
*
* @param result
* the set to which the objects shall be added
* @param state
* the state in which this type is evaluated
* @param pid
* the ID of the process performing the evaluation
* @param type
* the CIVL type
* @throws UnsatisfiablePathConditionException
* if it is discovered that
* the path condition of
* {@code state} is
* unsatisfiable
* @throws NoReductionException
* if no good
* over-approximation can be
* found
*/
private void findObjects(SeqSet result, State state, int pid, CIVLType type)
throws UnsatisfiablePathConditionException, NoReductionException {
findObjectsHelper(result, state, pid, type, new HashSet<CIVLType>());
}
/**
* Auxiliary function used by
* {@link #findObjects(SeqSet, State, int, CIVLType)}. This is a recursive
* function that keeps track of the set of seen types.
*
* @param result
* the set to which the objects shall be added
* @param state
* the state in which this type is evaluated
* @param pid
* the ID of the process performing the evaluation
* @param type
* the CIVL type
* @param seen
* the set of types already encountered in this invocation
* of {@link #findObjects(SeqSet, State, int, CIVLType)}.
* @throws UnsatisfiablePathConditionException
* if it is discovered that
* the path condition of
* {@code state} is
* unsatisfiable
* @throws NoReductionException
* if no good
* over-approximation can be
* found
*/
private void findObjectsHelper(SeqSet result, State state, int pid,
CIVLType type, Set<CIVLType> seen)
throws UnsatisfiablePathConditionException, NoReductionException {
if (!seen.add(type))
return;
switch (type.typeKind()) {
case ARRAY :
findObjectsHelper(result, state, pid,
((CIVLArrayType) type).elementType(), seen);
break;
case COMPLETE_ARRAY : {
CIVLCompleteArrayType atype = (CIVLCompleteArrayType) type;
findObjectsHelper(result, state, pid, atype.elementType(),
seen);
findObjects(result, state, pid, atype.extent());
break;
}
case FUNCTION : {
CIVLFunctionType ftype = (CIVLFunctionType) type;
for (CIVLType ptype : ftype.parameterTypes())
findObjectsHelper(result, state, pid, ptype, seen);
findObjectsHelper(result, state, pid, ftype.returnType(), seen);
break;
}
case POINTER :
findObjectsHelper(result, state, pid,
((CIVLPointerType) type).baseType(), seen);
break;
case SET :
findObjectsHelper(result, state, pid,
((CIVLSetType) type).elementType(), seen);
break;
case STRUCT_OR_UNION : {
CIVLStructOrUnionType sutype = (CIVLStructOrUnionType) type;
if (sutype.isComplete())
for (StructOrUnionField field : sutype.fields())
findObjectsHelper(result, state, pid, field.type(),
seen);
break;
}
case BUNDLE :
case DOMAIN :
case ENUM :
case HEAP :
case MEM :
case PRIMITIVE :
default :
break;
}
}
/**
* Gets the result of evaluating a guard for a statement. This method
* handles the caching of the results. It uses
* {@link SimpleEnabler#computeGuard(State, Reasoner, int, int)} to compute
* the guard the first time. The guard is evaluated at state
* {@link #theState}.
*
* @param pid
* the process ID
* @param sid
* the statement ID, i.e., the index in the list of outgoing
* statements from the current location of the process
* @return evaluated guard
* @throws UnsatisfiablePathConditionException
* if in the course of
* evaluating it is
* discovered that the path
* condition of
* {@link #theState} is
* unsatisfiable
*/
private BooleanExpression getGuardValue(int pid, int sid)
throws UnsatisfiablePathConditionException {
if (theGuards[pid] == null) {
int numOutgoing = theState.getProcessState(pid).getLocation()
.getNumOutgoing();
theGuards[pid] = new BooleanExpression[numOutgoing];
return theGuards[pid][sid] = enabler.computeGuard(theState,
reasoner, pid, sid);
} else {
BooleanExpression evaluatedGuard = theGuards[pid][sid];
if (evaluatedGuard == null) {
evaluatedGuard = enabler.computeGuard(theState, reasoner, pid,
sid);
theGuards[pid][sid] = evaluatedGuard;
}
return evaluatedGuard;
}
}
/**
* <p>
* Computes the set of transitions enabled at {@link #theState} by a given
* statement.
* </p>
*
* <p>
* Precondition: it is not the case that some other process owns the atomic
* lock
* </p>
*
* @param result
* the list to which the enabled transitions will be
* added
* @param pid
* the ID of the process executing the statement
* @param location
* the current location of the process at state
* {@link #theState} (this could be determined from
* {@link #theState} but is an argument for efficiency)
* @param stmtID
* the ID number of the outgoing statement from
* {@code location}
* @throws UnsatisfiablePathConditionException
* if it is determined that
* the path condition of
* {@link #theState} is
* unsatisfiable
*/
private void computeEnabledFromStatement(List<Transition> result, int pid,
Location location, int stmtID)
throws UnsatisfiablePathConditionException {
Statement stmt = location.getOutgoing(stmtID);
BooleanExpression guardValue = getGuardValue(pid, stmtID);
if (guardValue.isFalse())
return;
// second half of $yield: re-obtaining lock...
if (enabler.isYield(stmt) && !stateFactory.lockedByAtomic(theState)) {
result.add(Semantics.newTransition(pid, guardValue, stmt, false));
} else if (enabler.isSystemCall(theState, pid, stmt)) {
result.addAll(enabler.enabledTransitionsOfSystemCall(theState, pid,
guardValue, (CallOrSpawnStatement) stmt));
} else {
boolean simplify = enabler.isAssume(stmt);
boolean noop = stmt.statementKind() == StatementKind.NOOP;
Transition trans = noop
? Semantics.newNoopTransition(pid, guardValue, stmt,
simplify)
: Semantics.newTransition(pid, guardValue, stmt, simplify);
result.add(trans);
}
}
/**
* <p>
* Computes the set of transitions enabled at {@link #theState} in the
* specified process.
* </p>
*
* <p>
* Precondition: the atomic lock is not held by another process at
* {@link #theState}. Hence the atomic lock may be free, or it may be held
* by the specified process.
* </p>
*
* @param result
* the list to which the enabled transitions will be added
* @param pid
* ID of the process
* @throws UnsatisfiablePathConditionException
* if it is determined that
* the path condition of
* {@link #theState} is
* unsatisfiable
*/
private void computeEnabledInProcess(List<Transition> result, int pid)
throws UnsatisfiablePathConditionException {
ProcessState ps = theState.getProcessState(pid);
if (ps == null)
return;
Location location = ps.getLocation();
if (location == null)
return;
int numStatements = location.getNumOutgoing();
for (int i = 0; i < numStatements; i++)
computeEnabledFromStatement(result, pid, location, i);
}
/**
* <p>
* Computes an over-approximation to the set of objects associated to a
* process's current location at state {@link #theState}. These are: (1) any
* object that could be read or modified by a currently enabled statement,
* and (2) all objects that are read by any guard of an (enabled or
* disabled) statement emanating from that location. Additionally, computes
* set of processes on which the given process depends, due to waiting.
* </p>
*
* <p>
* For a system function call: if the system function does not specify a
* depends_on contract clause, nothing is assumed about the call, i.e., it
* could depend on everything. Example: $wait. I think $wait should
* depends_on nothing. Nothing can disable it and it commutes with
* everything.
* </p>
*
* @param pid
* the ID of the process (in)
* @param depend
* the set of objects of the process's depend set
* (out)
* @param dependWrite
* the set of objects of the depend set that may be
* modified (out)
* @return set of PIDs of processes on which this process is waiting with
* blocked wait statements, or {@code null} if there are no such
* waitees
* @throws UnsatisfiablePathConditionException
* if it is determined that
* the path condition of
* {@link #theState} is
* unsatisfiable
*/
Set<Integer> computeDepends(int pid, SeqSet depend, SeqSet dependWrite)
throws UnsatisfiablePathConditionException {
Location location = theState.getProcessState(pid).getLocation();
int numOutgoing = location.getNumOutgoing();
Set<Integer> result = null;
try {
for (int i = 0; i < numOutgoing; i++) {
Statement statement = location.getOutgoing(i);
Expression guard = statement.guard();
BooleanExpression guardValue = getGuardValue(pid, i);
findObjects(depend, theState, pid, guard);
if (reasoner.unsat(guardValue)
.getResultType() == ResultType.YES) {
if (enabler.isWait(statement)) {
// this is a blocked wait, get the "waitee"...
Expression arg = ((CallOrSpawnStatement) statement)
.arguments().get(0);
SymbolicExpression val = enabler.evaluator
.evaluate(theState, pid, arg).value;
int pidValue = enabler.modelFactory.getProcessId(val);
if (result == null)
result = new HashSet<>(2);
result.add(pidValue);
}
} else {
computeMem(depend, dependWrite, theState, pid, statement);
}
}
} catch (NoReductionException e) {
depend.makeFull();
dependWrite.makeFull();
}
return result;
}
/**
* Computes an over-approximation of all objects reachable from a process in
* {@link #theState}. Consider the directed graph in which the nodes are the
* objects which exist at {@link #theState} and there is an edge from u to v
* if u contains a pointer which points to some part of v. The initial nodes
* are all variable instances in the dyscopes reachable from the process's
* call stack. The reachable dyscopes are those referenced by the call
* stack, the parents of those dyscopes, the parents of those, etc.
*
* <p>
* Heaps are treated specially since a heap is technically a single
* variable, but is considered to represent a set of independent objects.
* </p>
*
* <p>
* If no good over-approximation can be found, the universal set (containing
* all objects) is returned.
* </p>
*
* @param pid
* the ID of the process
* @param reach
* out variable: set to which all reachable objects
* will be added
* @param reachWrite
* out variable: set to which all reachable objects
* which are possibly modified will be added
* @return the set of reachable objects represented as a {@link SeqSet}
*/
void computeReach(int pid, SeqSet reach, SeqSet reachWrite) {
ProcessState ps = theState.getProcessState(pid);
Set<Integer> dyscopeIDs = new HashSet<>();
Set<Variable> writeableVars = new HashSet<>();
if (ps == null || ps.hasEmptyStack())
return;
for (StackEntry se : ps.getStackEntries()) {
int dyscopeID = se.scope();
Location loc = se.location();
if (loc != null)
writeableVars.addAll(loc.writableVariables());
while (dyscopeID != -1 && dyscopeIDs.add(dyscopeID))
dyscopeID = theState.getParentId(dyscopeID);
}
for (int dyscopeID : dyscopeIDs) {
DynamicScope ds = theState.getDyscope(dyscopeID);
Scope scope = ds.lexicalScope();
for (Variable var : scope.variables()) {
addVariable(reach, theState, pid, var);
if (writeableVars.contains(var))
addVariable(reachWrite, theState, pid, var);
}
}
try {
SeqSet closure = new SeqSet();
// any object that can be reached by one or more pointer derefs
// is a writable reachable object...
closeIrreflexive(closure, reach, theState,
ps.getLocation().getSource());
reach.addAll(closure);
reachWrite.addAll(closure);
} catch (NoReductionException e) {
reach.add(); // makes it the universal set
reachWrite.add(); // ditto
}
}
/**
* Prints a {@code SeqSet} representing a set of objects in a human readable
* form. The set represents a set of variable instances or heap objects in
* the current state {@link #theState}.
*
* @param out
* the stream to which the output should be printed
* @param ss
* the set representing a set of objects
*/
protected void printObjSet(PrintStream out, SeqSet ss) {
boolean first = true;
for (int[] vec : ss.getLeaves()) {
if (first)
first = false;
else
out.print(", ");
if (vec.length == 0)
out.print("all");
else {
// dyscope, variable, mallocIdx(optional), objIdx(optional)
int dyid = vec[0], vid = vec[1];
DynamicScope dyscope = theState.getDyscope(dyid);
Scope scope = dyscope.lexicalScope();
Variable var = scope.variable(vid);
out.print(var.name().name() + "#" + dyid);
if (vec.length > 2) {
out.print("." + vec[2]);
if (vec.length > 3)
out.print("[" + vec[3] + "]");
}
}
}
}
/**
* Does the specified process satisfy the simple invisibility criterion for
* the current deadlock predicate at state {@link #theState}?
*
* <p>
* This means: assuming the current state s does not satisfy the "bad"
* property p, on any execution starting from s in which the executing
* processes do not access the dependencies of process {@code pid}, p will
* not hold. Example:
*
* <pre>
* $input int X;
* p0 : { int x = X; $when x>0 ; }
* p1 : { 1; } // 1 is a no-op with guard true
* </pre>
* </p>
*
* <p>
* Absolute deadlock is the bad property which holds when the enabling
* predicate (the disjunction of guards of statements from current
* locations) is not valid, i.e., there exists an assignment of values to
* symbolic constants such that the resulting concrete state is deadlocked.
* </p>
*
* <p>
* In the state s where p0 is at the $when and p1 is at the no-op, absolute
* deadlock is false, as the enabled predicate is true, because of p1.
* However the simple invisibility criterion does not hold for pid=0. That
* is because after process 1 executes the no-op, absolute deadlock holds,
* as X>0 is not valid. Hence it would be wrong to choose {p0} as an ample
* set for s.
* </p>
*
* <p>
* A sufficient condition for the criterion to hold is that the enabling
* predicate of the single process pid is valid. By the assumption, further
* execution by other processes can only weaken the enabling predicate of
* pid, so it must remain valid. That is because the other processes cannot
* affect any variable occurring in a guard of an enabled transition in pid.
* They may affect variables which enable currently disabled transitions in
* pid, but that can only weaken the enabling predicate.
* </p>
*
* <p>
* For potential deadlock: the situation is similar except send transitions
* should be considered possibly blocking, so the disjunction of guards of
* all transitions departing from pid's location other than send transitions
* must be valid. A "send" is actually an "enqueue" operation in the comm
* library.
* </p>
*
* <p>
* $wait: $wait is a system function which should be declared as
* "depends_on" nothing. It really is independent of any transition from
* another process. Its guard is "terminated(p)", where p is the $proc that
* is the argument to $wait. If that guard evaluates to true, it will remain
* true. So there is no need for any special treatment for $wait.
* </p>
*
* <p>
* $spawn is normally always enabled, except for a process-bounded search
* (proc_bound > 0). For such a search, $spawn should never be considered
* independent. That is because a $spawn can disable another $spawn. Since
* this method should only be invoked for a set of transitions that are
* independent (of transitions in other processes), this case also requires
* no special handling.
* </p>
*
* @param pid
* process ID
* @return {@code true} if it is possible the process has a visible enabled
* transition
* @throws UnsatisfiablePathConditionException
* if it is determined that
* the path condition of
* {@link #theState} is
* unsatisfiable
*/
protected boolean allInvisible(int pid)
throws UnsatisfiablePathConditionException {
// optimization: handle the common cases first.
// TODO: perform this computation statically
DeadlockKind kind = enabler.config.checkDeadlockKind();
if (kind == DeadlockKind.NONE)
return true;
Location location = theState.getProcessState(pid).getLocation();
if (location == null)
return true; // process pid has terminated
if (location.isBinaryBranching()
|| location.isSwitchOrChooseWithDefault())
return true;
int numOutgoing = location.getNumOutgoing();
if (numOutgoing == 0)
return true;
if (numOutgoing == 1) {
Statement stmt = location.getOutgoing(0);
if (enabler.isTrue(stmt.guard())) {
if (kind == DeadlockKind.ABSOLUTE
|| !enabler.isSend(theState, pid, stmt))
return true;
}
}
BooleanExpression enabled = universe.falseExpression();
if (kind == DeadlockKind.ABSOLUTE)
for (int i = 0; i < numOutgoing; i++)
enabled = universe.or(enabled, getGuardValue(pid, i));
else
for (int i = 0; i < numOutgoing; i++)
if (!enabler.isSend(theState, pid, location.getOutgoing(i))) {
enabled = universe.or(enabled, getGuardValue(pid, i));
}
return reasoner.isValid(enabled);
}
/**
* Determines whether the specified process is at a location (at state
* {@link #theState}) from which it could enter an atomic block for which
* termination is not guaranteed.
*
* @param pid
* the ID of the process
* @return {@code} true if process {@code PID} is at a location from which
* it could enter a possibly non-terminating atomic block
*
* @see Location#isEntryOfUnsafeAtomic()
*/
protected boolean unsafeAtomic(int pid) {
ProcessState ps = theState.getProcessState(pid);
if (ps == null)
return false;
Location location = ps.getLocation();
if (location == null)
return false;
return location.isEntryOfUnsafeAtomic();
}
/**
* Returns the set of transitions enabled in the specified process at state
* {@link #theState}. If the set has been previously computed, it is
* returned immediately from a cache, otherwise it is computed and cached.
* This is the method clients should use to get the set of transitions
* enabled in a process.
*
* @param pid
* the ID of the process
* @return the set of enabled transitions, represented as an array
* @throws UnsatisfiablePathConditionException
* if it is determined that
* the path condition of
* {@link #theState} is
* unsatisfiable
*/
protected Transition[] enabledTransitionsInProcess(int pid)
throws UnsatisfiablePathConditionException {
Transition[] result = enabledTransitions[pid];
if (result == null) {
List<Transition> list = new LinkedList<>();
computeEnabledInProcess(list, pid);
enabledTransitions[pid] = result = list
.toArray(new Transition[list.size()]);
}
return result;
}
/**
* Auxiliary function used by {@link #computeAmpleSet()} to print out ample
* set information to {@link Enabler#debugOut}.
*
* @param sc
* the instance of {@link StrongConnect} already used
* to find an ample set (or fail to find one)
* @param amplePids
* the list of process IDs of the ample set, or
* {@code null} if no ample set was found and therefore
* the full set should be used
* @throws UnsatisfiablePathConditionException
* should not be thrown
*/
private void printAmpleInfo(StrongConnect sc, LinkedList<Integer> amplePids)
throws UnsatisfiablePathConditionException {
boolean first = true;
if (amplePids == null) {
amplePids = new LinkedList<Integer>();
for (int i = 0; i < nprocs; i++)
amplePids.add(i);
}
enabler.debugOut
.print("\nample processes at state " + theState + ":\t");
for (int i : amplePids) {
if (first)
first = false;
else
enabler.debugOut.print(", ");
enabler.debugOut.print("p" + i + "("
+ enabledTransitionsInProcess(i).length + ")");
}
enabler.debugOut.println();
sc.printData(enabler.debugOut);
if (!enabler.debugging && enabler.showAmpleSetWtStates)
enabler.debugOut.print(theState.callStackToString());
}
/**
* Computes an ample set for state {@link #theState}. This may be the full
* set (consisting of all enabled transitions). This method may set
* {@link #full} to {@code true}, indicating that the full set was used.
*
* @throws UnsatisfiablePathConditionException
* if it is discovered that
* the path condition of
* {@link #theState} is
* unsatisfiable
*/
protected void computeAmpleSet()
throws UnsatisfiablePathConditionException {
StrongConnect sc = new StrongConnect(this);
LinkedList<Integer> amplePids = sc.findAmple();
int size = 0, c = 0;
int numProcs = 0;
if (amplePids == null) {
full = true;
for (int i = 0; i < nprocs; i++) {
int ntrans = enabledTransitionsInProcess(i).length;
if (ntrans > 0) {
size += ntrans;
numProcs++;
}
}
ampleSet = new Transition[size];
for (int i = 0; i < nprocs; i++)
for (Transition tran : enabledTransitions[i]) {
ampleSet[c++] = tran;
}
} else {
full = false;
for (int i : amplePids) {
int ntrans = enabledTransitionsInProcess(i).length;
if (ntrans > 0) {
size += ntrans;
numProcs++;
}
}
ampleSet = new Transition[size];
for (int i : amplePids)
for (Transition tran : enabledTransitions[i]) {
ampleSet[c++] = tran;
}
}
if (numProcs > 1 && (enabler.debugging || enabler.showAmpleSet))
printAmpleInfo(sc, amplePids);
}
/**
* Returns the ample set for {@link #theState}. This method should be called
* only after {@link #computeAmpleSet()} has been called.
*
* @return the ample set
*/
protected Transition[] ampleSet() {
return ampleSet;
}
/**
* Returns the full bit. This method should be called only after
* {@link #computeAmpleSet()} has been called. If this method returns
* {@code true}, then the ample set consists of all enabled transitions at
* {@link #theState}.
*
* @return the full bit
*/
protected boolean isFull() {
return full;
}
}
/**
* An exception indicating that no good approximation of a set of dependencies
* or reachable objects can be determined.
*
* @author siegel
*/
class NoReductionException extends Exception {
private static final long serialVersionUID = 1L;
}