LibraryComponent.java
package edu.udel.cis.vsl.civl.library.common;
import edu.udel.cis.vsl.civl.dynamic.IF.SymbolicUtility;
import edu.udel.cis.vsl.civl.semantics.IF.LibraryEvaluatorLoader;
import edu.udel.cis.vsl.civl.log.IF.CIVLExecutionException;
import edu.udel.cis.vsl.civl.model.IF.CIVLException.Certainty;
import edu.udel.cis.vsl.civl.model.IF.CIVLException.ErrorKind;
import edu.udel.cis.vsl.civl.model.IF.CIVLInternalException;
import edu.udel.cis.vsl.civl.model.IF.CIVLSource;
import edu.udel.cis.vsl.civl.model.IF.CIVLUnimplementedFeatureException;
import edu.udel.cis.vsl.civl.semantics.IF.SymbolicAnalyzer;
import edu.udel.cis.vsl.civl.state.IF.State;
import edu.udel.cis.vsl.sarl.IF.SARLException;
import edu.udel.cis.vsl.sarl.IF.SymbolicUniverse;
import edu.udel.cis.vsl.sarl.IF.expr.BooleanExpression;
import edu.udel.cis.vsl.sarl.IF.expr.NumericExpression;
import edu.udel.cis.vsl.sarl.IF.expr.SymbolicExpression;
import edu.udel.cis.vsl.sarl.IF.object.IntObject;
/**
* The LibraryComponent class provides the common data and operations of library
* evaluator, enabler, and executor.
*
* @author Manchun Zheng (zmanchun)
*
*/
public abstract class LibraryComponent {
// The order of these operations should be consistent with civlc.cvh
// file.
protected enum CIVLOperator {
CIVL_NO_OP, // no operation
CIVL_MAX, // maxinum
CIVL_MIN, // minimun
CIVL_SUM, // sum
CIVL_PROD, // product
CIVL_LAND, // logical and
CIVL_BAND, // bit-wise and
CIVL_LOR, // logical or
CIVL_BOR, // bit-wise or
CIVL_LXOR, // logical exclusive or
CIVL_BXOR, // bit-wise exclusive or
CIVL_MINLOC, // min value and location
CIVL_MAXLOC, // max value and location
CIVL_REPLACE // replace ? TODO: Find definition for this operation
}
/**
* Operators:
*
* <pre>
* _NO_OP, // no operation
* _MAX, // maxinum
* _MIN, // minimun
* _SUM, // sum
* _PROD, // product
* _LAND, // logical and
* _BAND, // bit-wise and
* _LOR, // logical or
* _BOR, // bit-wise or
* _LXOR, // logical exclusive or
* _BXOR, // bit-wise exclusive or
* _MINLOC, // min value and location
* _MAXLOC, // max value and location
* _REPLACE // replace ? TODO: Find definition for this operation
* </pre>
* */
private final int _NO_OP = 0;
private final int _MAX = 1;
private final int _MIN = 2;
private final int _SUM = 3;
private final int _PROD = 4;
private final int _LAND = 5;
private final int _BAND = 6;
private final int _LXOR = 7;
private final int _BXOR = 8;
private final int _MINLOC = 9;
private final int _MAXLOC = 10;
// private final int _REPLACE = 11;
/**
* The symbolic expression of one.
*/
protected NumericExpression one;
/**
* The symbolic object of integer one.
*/
protected IntObject oneObject;
/**
* The symbolic expression of three.
*/
protected NumericExpression three;
/**
* The symbolic object of integer three.
*/
protected IntObject threeObject;
/**
* The symbolic expression of two.
*/
protected NumericExpression two;
/**
* The symbolic object of integer two.
*/
protected IntObject twoObject;
/**
* The symbolic expression of zero.
*/
protected NumericExpression zero;
/**
* The symbolic object of integer zero.
*/
protected IntObject zeroObject;
/**
* The symbolic universe for symbolic computations.
*/
protected SymbolicUniverse universe;
/**
* The symbolic universe for symbolic computations.
*/
protected SymbolicUtility symbolicUtil;
/**
* The symbolic analyzer for operations on symbolic expressions and states.
*/
protected SymbolicAnalyzer symbolicAnalyzer;
protected String name;
protected BooleanExpression trueValue;
protected BooleanExpression falseValue;
protected LibraryEvaluatorLoader libEvaluatorLoader;
/**
* Creates a new instance of a library.
*
* @param universe
* The symbolic universe to be used.
* @param symbolicUtil
* The symbolic utility to be used.
* @param symbolicAnalyzer
* The symbolic analyzer to be used.
*/
protected LibraryComponent(String name, SymbolicUniverse universe,
SymbolicUtility symbolicUtil, SymbolicAnalyzer symbolicAnalyzer,
LibraryEvaluatorLoader libEvaluatorLoader) {
this.name = name;
this.universe = universe;
this.zero = universe.zeroInt();
this.one = universe.oneInt();
this.two = universe.integer(2);
this.three = universe.integer(3);
this.zeroObject = universe.intObject(0);
this.oneObject = universe.intObject(1);
this.twoObject = universe.intObject(2);
this.threeObject = universe.intObject(3);
this.symbolicUtil = symbolicUtil;
this.symbolicAnalyzer = symbolicAnalyzer;
this.trueValue = universe.trueExpression();
this.falseValue = universe.falseExpression();
this.libEvaluatorLoader = libEvaluatorLoader;
}
/**
* Returns the name associated to this library executor or enabler, for
* example, "stdio".
*
* @return
*/
public String name() {
return this.name;
}
/**
* Completing an operation (which is included in CIVLOperation enumerator).
*
* @author Ziqing Luo
* @param arg0
* The new data got from the bundle
* @param arg1
* The data has already been received previously
* @param op
* The CIVL Operation
* @return
*/
protected SymbolicExpression applyCIVLOperator(State state, String process,
SymbolicExpression arg0, SymbolicExpression arg1, CIVLOperator op,
CIVLSource civlsource) {
BooleanExpression claim;
/*
* For MAX and MIN operation, if CIVL cannot figure out a concrete
* result, make a abstract function for it.
*/
try {
switch (op) {
// TODO: consider using heuristic to switch to abstract
// functions if these expressions get too big (max,min):
case CIVL_MAX:
claim = universe.lessThan((NumericExpression) arg1,
(NumericExpression) arg0);
return universe.cond(claim, arg0, arg1);
case CIVL_MIN:
claim = universe.lessThan((NumericExpression) arg0,
(NumericExpression) arg1);
return universe.cond(claim, arg0, arg1);
case CIVL_SUM:
return universe.add((NumericExpression) arg0,
(NumericExpression) arg1);
case CIVL_PROD:
return universe.multiply((NumericExpression) arg0,
(NumericExpression) arg1);
case CIVL_LAND:
return universe.and((BooleanExpression) arg0,
(BooleanExpression) arg1);
case CIVL_LOR:
return universe.or((BooleanExpression) arg0,
(BooleanExpression) arg1);
case CIVL_LXOR:
BooleanExpression notNewData = universe
.not((BooleanExpression) arg0);
BooleanExpression notPrevData = universe
.not((BooleanExpression) arg1);
return universe.or(
universe.and(notNewData, (BooleanExpression) arg1),
universe.and((BooleanExpression) arg0, notPrevData));
case CIVL_BAND:
case CIVL_BOR:
case CIVL_BXOR:
case CIVL_MINLOC:
case CIVL_MAXLOC:
case CIVL_REPLACE:
default:
throw new CIVLUnimplementedFeatureException("CIVLOperation: "
+ op.name());
}
} catch (ClassCastException e) {
throw new CIVLExecutionException(ErrorKind.OTHER,
Certainty.PROVEABLE, process,
"Invalid operands type for CIVL Operation: " + op.name(),
civlsource);
} catch (SARLException e) {
throw new CIVLInternalException("CIVL Operation " + op
+ " exception", civlsource);
}
}
protected CIVLOperator translateOperator(int op) {
switch (op) {
case _NO_OP:
return CIVLOperator.CIVL_NO_OP;
case _MAX:
return CIVLOperator.CIVL_MAX;
case _MIN:
return CIVLOperator.CIVL_MIN;
case _SUM:
return CIVLOperator.CIVL_SUM;
case _PROD:
return CIVLOperator.CIVL_PROD;
case _LAND:
return CIVLOperator.CIVL_LAND;
case _BAND:
return CIVLOperator.CIVL_BAND;
case _LXOR:
return CIVLOperator.CIVL_LXOR;
case _BXOR:
return CIVLOperator.CIVL_BXOR;
case _MINLOC:
return CIVLOperator.CIVL_MINLOC;
case _MAXLOC:
return CIVLOperator.CIVL_MAXLOC;
default:
return CIVLOperator.CIVL_REPLACE;
}
}
}