LibcivlcEnabler.java
package dev.civl.mc.library.civlc;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.BitSet;
import java.util.LinkedHashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;
import dev.civl.mc.config.IF.CIVLConfiguration;
import dev.civl.mc.dynamic.IF.SymbolicUtility;
import dev.civl.mc.kripke.IF.Enabler;
import dev.civl.mc.kripke.IF.LibraryEnabler;
import dev.civl.mc.kripke.IF.LibraryEnablerLoader;
import dev.civl.mc.library.common.BaseLibraryEnabler;
import dev.civl.mc.model.IF.CIVLProperty;
import dev.civl.mc.model.IF.CIVLSource;
import dev.civl.mc.model.IF.ModelFactory;
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.Expression;
import dev.civl.mc.model.IF.expression.InitialValueExpression;
import dev.civl.mc.model.IF.statement.AssignStatement;
import dev.civl.mc.model.IF.statement.CallOrSpawnStatement;
import dev.civl.mc.model.IF.statement.Statement;
import dev.civl.mc.semantics.IF.Evaluation;
import dev.civl.mc.semantics.IF.Evaluator;
import dev.civl.mc.semantics.IF.LibraryEvaluatorLoader;
import dev.civl.mc.semantics.IF.Semantics;
import dev.civl.mc.semantics.IF.SymbolicAnalyzer;
import dev.civl.mc.semantics.IF.Transition;
import dev.civl.mc.state.IF.MemoryUnitSet;
import dev.civl.mc.state.IF.State;
import dev.civl.mc.state.IF.UnsatisfiablePathConditionException;
import dev.civl.mc.util.IF.Pair;
import dev.civl.sarl.IF.Reasoner;
import dev.civl.sarl.IF.expr.BooleanExpression;
import dev.civl.sarl.IF.expr.NumericExpression;
import dev.civl.sarl.IF.expr.SymbolicConstant;
import dev.civl.sarl.IF.expr.SymbolicExpression;
import dev.civl.sarl.IF.number.IntegerNumber;
import dev.civl.sarl.IF.number.Interval;
import dev.civl.sarl.IF.number.Number;
/**
* Implementation of the enabler-related logics for system functions declared
* civlc.h.
*
* @author Manchun Zheng (zmanchun)
*
*/
public class LibcivlcEnabler extends BaseLibraryEnabler implements LibraryEnabler {
private final static int ELABORATE_UPPER_BOUND = 100;
/* **************************** Constructors *************************** */
/**
* Creates a new instance of the library enabler for civlc.h.
*
* @param primaryEnabler The enabler for normal CIVL execution.
* @param output The output stream to be used in the enabler.
* @param modelFactory The model factory of the system.
*/
public LibcivlcEnabler(String name, Enabler primaryEnabler, Evaluator evaluator, ModelFactory modelFactory,
SymbolicUtility symbolicUtil, SymbolicAnalyzer symbolicAnalyzer, CIVLConfiguration civlConfig,
LibraryEnablerLoader libEnablerLoader, LibraryEvaluatorLoader libEvaluatorLoader) {
super(name, primaryEnabler, evaluator, modelFactory, symbolicUtil, symbolicAnalyzer, civlConfig,
libEnablerLoader, libEvaluatorLoader);
}
/* ********************* Methods from LibraryEnabler ******************* */
@Override
public BitSet ampleSet(State state, int pid, CallOrSpawnStatement call, MemoryUnitSet[] setsReachableRead,
MemoryUnitSet[] setsReachableWrite) throws UnsatisfiablePathConditionException {
return this.ampleSetWork(state, pid, call);
}
@Override
public List<Transition> enabledTransitions(State state, CallOrSpawnStatement call, BooleanExpression clause,
int pid) throws UnsatisfiablePathConditionException {
String functionName = call.function().name().name();
AssignStatement assignmentCall;
Expression[] arguments = new Expression[call.arguments().size()];// call.arguments();
List<Transition> localTransitions = new LinkedList<>();
String process = "p" + pid;
Pair<State, SymbolicExpression[]> argumentsEval;
call.arguments().toArray(arguments);
switch (functionName) {
case "$assume": {
localTransitions.add(Semantics.newTransition(pid, trueValue, call, true));
return localTransitions;
}
case "$choose_int":
if (call.lhs() == null) {
// if no left-hand side expression, this is a no-op
// transition:
localTransitions.add(Semantics.newNoopTransition(pid, clause, call, false));
return localTransitions;
}
argumentsEval = evaluateArguments(state, pid, arguments);
state = argumentsEval.left;
IntegerNumber upperNumber = (IntegerNumber) universe.reasoner(state.getPathCondition(universe))
.extractNumber((NumericExpression) argumentsEval.right[0]);
int upper;
if (upperNumber == null) {
this.errorLogger.logSimpleError(arguments[0].getSource(), state, pid, process,
symbolicAnalyzer.stateInformation(state), CIVLProperty.INTERNAL,
"argument to $choose_int not concrete: " + argumentsEval.right[0]);
throw new UnsatisfiablePathConditionException();
}
upper = upperNumber.intValue();
for (int i = 0; i < upper; i++) {
Expression singleChoice = modelFactory.integerLiteralExpression(arguments[0].getSource(),
BigInteger.valueOf(i));
assignmentCall = modelFactory.assignStatement(arguments[0].getSource(), call.source(), call.lhs(),
singleChoice, (call.lhs() instanceof InitialValueExpression));
assignmentCall.setTargetTemp(call.target());
assignmentCall.setTarget(call.target());
assignmentCall.source().removeOutgoing(assignmentCall);
localTransitions.add(Semantics.newTransition(pid, clause, assignmentCall));
}
return localTransitions;
case "$elaborate":
argumentsEval = this.evaluateArguments(state, pid, arguments);
return this.elaborateIntWorker(argumentsEval.left, pid, call, call.getSource(), arguments,
argumentsEval.right);
case "$elaborate_domain":
argumentsEval = this.evaluateArguments(state, pid, arguments);
return this.elaborateRectangularDomainWorker(argumentsEval.left, pid, call, call.getSource(), arguments,
argumentsEval.right);
case "$unidirectional_when":
BooleanExpression condition = (BooleanExpression) evaluateArguments(state, pid, arguments).right[0];
// This function $unidirectional_when is same as $when but is
// guaranteed to be invisible for deadlock property by
// programmer.
if (condition.isTrue())
// If condition is simply true, enables a no-op transition:
localTransitions.add(Semantics.newNoopTransition(pid, trueValue, call, false));
else if (!universe.reasoner(state.getPathCondition(universe)).isValid(universe.not(condition)))
// If condition is satisfiable (or prover cannot prove it is
// unsatisfiable), enables a no-op transition and adds the
// condition into the path condition:
localTransitions.add(Semantics.newNoopTransition(pid, condition, call, true));
return localTransitions;
default:
return super.enabledTransitions(state, call, clause, pid);
}
}
/* *************************** Private Methods ************************* */
/**
* Computes the ample set process ID's from a system function call.
*
* @param state The current state.
* @param pid The ID of the process that the system function
* call belongs to.
* @param call The system function call statement.
* @param reachableMemUnitsMap The map of reachable memory units of all active
* processes.
* @return
* @throws UnsatisfiablePathConditionException
*/
private BitSet ampleSetWork(State state, int pid, CallOrSpawnStatement call)
throws UnsatisfiablePathConditionException {
int numArgs;
numArgs = call.arguments().size();
Expression[] arguments;
SymbolicExpression[] argumentValues;
String function = call.function().name().name();
arguments = new Expression[numArgs];
argumentValues = new SymbolicExpression[numArgs];
for (int i = 0; i < numArgs; i++) {
Evaluation eval = null;
arguments[i] = call.arguments().get(i);
try {
eval = evaluator.evaluate(state, pid, arguments[i]);
} catch (UnsatisfiablePathConditionException e) {
return new BitSet(0);
}
argumentValues[i] = eval.value;
state = eval.state;
}
switch (function) {
case "$wait":
return ampleSetOfWait(state, pid, arguments, argumentValues);
case "$waitall":
return ampleSetOfWaitall(state, pid, arguments, argumentValues);
default:
return super.ampleSet(state, pid, call, null, null);
}
}
private BitSet ampleSetOfWait(State state, int pid, Expression[] arguments, SymbolicExpression[] argumentValues) {
SymbolicExpression joinProc = argumentValues[0];
int joinPid = modelFactory.getProcessId(joinProc);
BitSet ampleSet = new BitSet();
if (modelFactory.isPocessIdDefined(joinPid) && !modelFactory.isProcNull(joinProc)) {
ampleSet.set(joinPid);
}
return ampleSet;
}
/**
* computes the ample set for $waitall. The ample set is the set of processes
* being waited for.
*
* @param state the current state
* @param pid the PID of the process which executes the $waitall
* function call
* @param arguments the arguments of $waitall, where argument 0 is a
* pointer to the first $proc object, and 1 is the number
* of processes to wait for.
* @param argumentValues the evaluation results of the arguments of $waitall
* @return the set of processes being waited for as the ample set
* @throws UnsatisfiablePathConditionException
*/
private BitSet ampleSetOfWaitall(State state, int pid, Expression[] arguments, SymbolicExpression[] argumentValues)
throws UnsatisfiablePathConditionException {
SymbolicExpression procsPointer = argumentValues[0];
SymbolicExpression numOfProcs = argumentValues[1];
Reasoner reasoner = universe.reasoner(state.getPathCondition(universe));
IntegerNumber number_nprocs = (IntegerNumber) reasoner.extractNumber((NumericExpression) numOfProcs);
String process = state.getProcessState(pid).name() + "(id=" + pid + ")";
BitSet ampleSet = new BitSet();
if (number_nprocs == null) {
this.evaluator.errorLogger().logSimpleError(arguments[1].getSource(), state, pid, process,
symbolicAnalyzer.stateInformation(state), CIVLProperty.OTHER,
"the number of processes for $waitall " + "needs a concrete value");
throw new UnsatisfiablePathConditionException();
} else {
int numOfProcs_int = number_nprocs.intValue();
BinaryExpression pointerAdd;
CIVLSource procsSource = arguments[0].getSource();
Evaluation eval;
for (int i = 0; i < numOfProcs_int; i++) {
Expression offSet = modelFactory.integerLiteralExpression(procsSource, BigInteger.valueOf(i));
NumericExpression offSetV = universe.integer(i);
SymbolicExpression procPointer, proc;
int pidValue;
pointerAdd = modelFactory.binaryExpression(procsSource, BINARY_OPERATOR.POINTER_ADD, arguments[0],
offSet);
eval = evaluator.evaluatePointerAdd(state, pid, pointerAdd, procsPointer, offSetV);
procPointer = eval.value;
state = eval.state;
eval = evaluator.dereference(procsSource, state, pid, process, procPointer, false, true);
proc = eval.value;
state = eval.state;
pidValue = modelFactory.getProcessId(proc);
if (!modelFactory.isProcessIdNull(pidValue) && modelFactory.isPocessIdDefined(pidValue))
ampleSet.set(pidValue);
}
}
return ampleSet;
}
/**
* This methods elaborates all symbolic constants contained in an integer
* expression.
*
* @param state
* @param pid
* @param source
* @param arguments
* @param argumentValues
* @param atomicLockAction
* @return
*/
private List<Transition> elaborateIntWorker(State state, int pid, Statement call, CIVLSource source,
Expression[] arguments, SymbolicExpression[] argumentValues) {
Set<SymbolicConstant> symbolicConstants = universe.getFreeSymbolicConstants(argumentValues[0]);
return this.elaborateSymbolicConstants(state, pid, call, source, symbolicConstants);
}
private List<Transition> elaborateRectangularDomainWorker(State state, int pid, CallOrSpawnStatement call,
CIVLSource source, Expression[] arguments, SymbolicExpression[] argumentValues) {
Set<SymbolicConstant> symbolicConstants = universe.getFreeSymbolicConstants(argumentValues[0]);
return this.elaborateSymbolicConstants(state, pid, call, source, symbolicConstants);
}
private List<Transition> elaborateSymbolicConstants(State state, int pid, Statement call, CIVLSource source,
Set<SymbolicConstant> symbolicConstants) {
BooleanExpression pathCondition = state.getPathCondition(universe);
List<ConstantBound> bounds = new ArrayList<>();
ConstantBound[] constantBounds;
Set<BooleanExpression> concreteValueClauses;
List<Transition> transitions = new LinkedList<>();
Reasoner reasoner = universe.reasoner(pathCondition);
if (symbolicConstants.size() < 1) {
// noop if no symbolic constant is contained
return Arrays.asList((Transition) Semantics.newNoopTransition(pid, trueValue, call, false));
}
for (SymbolicConstant var : symbolicConstants) {
// no need to elaborate non-numeric symbolic constants:
if (!var.isNumeric())
continue;
Interval interval = reasoner.intervalApproximation((NumericExpression) var);
if (interval.isIntegral()) {
Number lowerNum = interval.lower(), upperNum = interval.upper();
int lower = Integer.MIN_VALUE, upper = Integer.MAX_VALUE;
if (!lowerNum.isInfinite()) {
lower = ((IntegerNumber) lowerNum).intValue();
}
if (!upperNum.isInfinite()) {
upper = ((IntegerNumber) upperNum).intValue();
}
bounds.add(new ConstantBound(var, lower, upper));
}
}
constantBounds = new ConstantBound[bounds.size()];
bounds.toArray(constantBounds);
// If there is no elaborated constants, return a default unchanged
// transition:
if (constantBounds.length == 0) {
transitions.add(Semantics.newNoopTransition(pid, trueValue, call, true));
return transitions;
}
concreteValueClauses = this.generateConcreteValueClauses(reasoner, constantBounds, 0);
for (BooleanExpression clause : concreteValueClauses)
transitions.add(Semantics.newNoopTransition(pid, clause, call, true));
return transitions;
}
/**
* generates boolean expressions by elaborating symbolic constants according to
* their upper/lower bound. The result is the permutation of the possible values
* of all symbolic constants. For example, if the constant bounds are {(X, [2,
* 3]), (Y, [6,7]), (Z, [8,9])} then the result will be { X=2 && Y=6 && Z==8,
* X=2 && Y=6 && Z=9, X=2 && Y=7 && Z=8, X=2 && Y=7 && Z=9, X=3 && Y=6 && Z=8,
* X=3 && Y=6 && Z=9, X=3 && Y=7 && Z=8, X=3 && Y=7 && Z=9}.
*
* @param reasoner
* @param constantBounds
* @param start
* @return
*/
private Set<BooleanExpression> generateConcreteValueClauses(Reasoner reasoner, ConstantBound[] constantBounds,
int start) {
Set<BooleanExpression> myResult = new LinkedHashSet<>();
ConstantBound myConstantBound = constantBounds[start];
Set<BooleanExpression> subfixResult;
Set<BooleanExpression> result = new LinkedHashSet<>();
// last constant bound
int lower = myConstantBound.lower, upper = myConstantBound.upper;
NumericExpression symbol = (NumericExpression) myConstantBound.constant;
BooleanExpression newClause;
boolean upperBoundCluaseNeeded = false;
if (lower < 0) {
lower = 0;
newClause = universe.lessThan(symbol, universe.integer(lower));
if (!reasoner.isValid(universe.not(newClause)))
myResult.add(newClause);
}
if (upper > lower + ELABORATE_UPPER_BOUND) {
upper = lower + ELABORATE_UPPER_BOUND;
upperBoundCluaseNeeded = true;
newClause = universe.lessThan(universe.integer(upper), symbol);
if (!reasoner.isValid(universe.not(newClause)))
myResult.add(newClause);
}
for (int value = lower; value <= upper; value++) {
newClause = universe.equals(symbol, universe.integer(value));
if (!reasoner.isValid(universe.not(newClause)))
myResult.add(newClause);
}
if (upperBoundCluaseNeeded)
myResult.add(universe.lessThan(universe.integer(upper), symbol));
if (start == constantBounds.length - 1)
return myResult;
subfixResult = this.generateConcreteValueClauses(reasoner, constantBounds, start + 1);
for (BooleanExpression myClause : myResult) {
for (BooleanExpression subfixClause : subfixResult) {
result.add(universe.and(myClause, subfixClause));
}
}
return result;
}
}
/**
* This represents the bound specification of a symbolic constant.
*
* @author Manchun Zheng
*
*/
class ConstantBound {
/**
* The symbolic constant associates with this object
*/
SymbolicConstant constant;
/**
* The lower bound of the symbolic constant
*/
int lower;
/**
* The upper bound of the symbolic constant
*/
int upper;
/**
*
* @param constant the symbolic constant
* @param lower the lower bound
* @param upper the upper bound
*/
ConstantBound(SymbolicConstant constant, int lower, int upper) {
this.constant = constant;
this.lower = lower;
this.upper = upper;
}
}