edu.nyu.cascade.ir.expr
Class AbstractExpressionFactory<Int,Bool,StateT extends Type<StateT>>

java.lang.Object
  edu.nyu.cascade.ir.expr.AbstractExpressionFactory<Int,Bool,StateT>

Type Parameters:

Int - The underlying encoding of integer values

Bool - The underlying encoding of boolean values

StateT - The program state type in the underlying encoding

All Implemented Interfaces:

ExpressionFactory<Int,Bool,StateT>

Direct Known Subclasses:

BitVectorExpressionFactory, DualExpressionFactory, IntExpressionFactory, IntLambdaExpressionFactory, IntPredicateExpressionFactory

public abstract class AbstractExpressionFactory<Int,Bool,StateT extends Type<StateT>>
extends Object
implements ExpressionFactory<Int,Bool,StateT>

An abstract implementation of the IExpressionFactory interface, with convenience implementations of several methods.

Author:

Christopher Conway

Field Summary

protected static String

FUN_ALLOCATED An interpreted function with the following intended meaning: allocated(p,n) is true if the memory region [p,p+n] is a contiguously allocated block of memory.

Constructor Summary

protected

AbstractExpressionFactory(ExpressionManager exprManager)

Method Summary

Bool	castToBoolean(Int expr) Returns a boolean expression representing the integer value expr, according to the conversion rule of the underlying encoding.
Int	castToInteger(Bool bool) Returns an integer expression representing the boolean value bool, according to the conversion rule of the underlying encoding.
Int	decr(Int expr) Returns an integer expression representing the integer expr minus one.
Int	functionCall(String name, Iterable<Int> args) Returns an integer expression representing the interpretation of a call to function name, with variable argument list args.
Int	functionCall(String name, Iterator<Int> args) Returns an integer expression representing the interpretation of a call to function name, with variable argument list args.
Int	functionCall(String name, List<Int> args) Returns an integer expression representing the interpretation of a call to function name, with variable argument list args.
ImmutableSet<? extends Expression<BooleanType>>	getAssumptions() Get logical assumptions used in the underlying encoding.
ExpressionManager	getExpressionManager() Returns the IExpressionManager object used in the underlying expression encoding.
Expression<StateT>	getInitialState() Default implementation: a variable of type StateT.
Int	incr(Int expr) Returns an integer expression representing the integer expr plus one.
Bool	integerAnd(Int lhs, Int rhs) Returns a boolean expression representing the logical AND of the two integer arguments, when converted to boolean expressions.
Bool	integerNot(Int e) Returns a boolean expression representing the logical negation of the integer argument, when converted to a boolean expression.
Bool	integerOr(Int lhs, Int rhs) Returns a boolean expression representing the logical OR of the two integer arguments, when converted to boolean expressions.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface edu.nyu.cascade.ir.expr.ExpressionFactory

allocated, and, assign, bitwiseAnd, deref, eq, evalBoolean, ff, getStateType, greaterThan, greaterThanOrEqual, ifThenElse, indexArray, indexArray, integerConstant, integerVar, lessThan, lessThanOrEqual, minus, neq, nor, not, one, or, plus, tt, type, unknown, variable, zero

Field Detail

FUN_ALLOCATED

protected static final String FUN_ALLOCATED

An interpreted function with the following intended meaning: allocated(p,n) is true if the memory region [p,p+n] is a contiguously allocated block of memory. E.g., after the statement "p = malloc(n);", allocated(p,n) will be true. The assertions allocated(p,n) and allocated(q,m) implicitly state that p and q do not alias. NOTE: allocated(p,n) and allocated(p,m) are thus inconsistent.

See Also:

Constant Field Values

Constructor Detail

AbstractExpressionFactory

protected AbstractExpressionFactory(ExpressionManager exprManager)

Method Detail

castToBoolean

public Bool castToBoolean(Int expr)
                   throws ExpressionFactoryException

Returns a boolean expression representing the integer value expr, according to the conversion rule of the underlying encoding. Default implementation: following the C convention, an expression expr has the boolean value true iff. it is not equal to the return value of zero().

Specified by:

castToBoolean in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

Throws:

ExpressionFactoryException

castToInteger

public Int castToInteger(Bool bool)
                  throws ExpressionFactoryException

Returns an integer expression representing the boolean value bool, according to the conversion rule of the underlying encoding. Default implementation: true maps to the return value of one() and false maps to the return value of zero().

Specified by:

castToInteger in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

Throws:

ExpressionFactoryException

decr

public Int decr(Int expr)
         throws ExpressionFactoryException

Returns an integer expression representing the integer expr minus one. Default implementation: encoding using minus() and one().

Specified by:

decr in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

Throws:

ExpressionFactoryException

functionCall

public Int functionCall(String name,
                        List<Int> args)
                 throws ExpressionFactoryException

Returns an integer expression representing the interpretation of a call to function name, with variable argument list args. Default implementation: interprets the allocated annotation using allocated(). Sub-classes overriding this method should call super() to maintain this behavior.

Specified by:

functionCall in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

Throws:

ExpressionFactoryException

functionCall

public Int functionCall(String name,
                        Iterable<Int> args)
                 throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns an integer expression representing the interpretation of a call to function name, with variable argument list args.

Specified by:

functionCall in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

Throws:

ExpressionFactoryException

functionCall

public Int functionCall(String name,
                        Iterator<Int> args)
                 throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns an integer expression representing the interpretation of a call to function name, with variable argument list args.

Specified by:

functionCall in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

Throws:

ExpressionFactoryException

getAssumptions

public ImmutableSet<? extends Expression<BooleanType>> getAssumptions()
                                                               throws ExpressionFactoryException

Get logical assumptions used in the underlying encoding. E.g., if variables x, y, and z are represented as indices into an array, then getAssumptions() may return { x ≠ y, x ≠ z, y ≠ z }. Default implementation: an empty set of assumptions.

Specified by:

getAssumptions in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

Throws:

ExpressionFactoryException

getExpressionManager

public ExpressionManager getExpressionManager()

Description copied from interface: ExpressionFactory

Returns the IExpressionManager object used in the underlying expression encoding.

Specified by:

getExpressionManager in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

getInitialState

public Expression<StateT> getInitialState()
                                                        throws ExpressionFactoryException

Default implementation: a variable of type StateT.

Specified by:

getInitialState in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

Throws:

ExpressionFactoryException

incr

public Int incr(Int expr)
         throws ExpressionFactoryException

Returns an integer expression representing the integer expr plus one. Default implementation: encoding using plus() and one().

Specified by:

incr in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

Throws:

ExpressionFactoryException

integerAnd

public Bool integerAnd(Int lhs,
                       Int rhs)
                throws ExpressionFactoryException

Returns a boolean expression representing the logical AND of the two integer arguments, when converted to boolean expressions. Default implementation: encoding using and() and castToBoolean().

Specified by:

integerAnd in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

Throws:

ExpressionFactoryException

integerNot

public Bool integerNot(Int e)
                throws ExpressionFactoryException

Returns a boolean expression representing the logical negation of the integer argument, when converted to a boolean expression. Default implementation: encoding using not() and castToBoolean().

Specified by:

integerNot in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

Throws:

ExpressionFactoryException

integerOr

public Bool integerOr(Int lhs,
                      Int rhs)
               throws ExpressionFactoryException

Returns a boolean expression representing the logical OR of the two integer arguments, when converted to boolean expressions. Default implementation: encoding using or() and castToBoolean().

Specified by:

integerOr in interface ExpressionFactory<Int,Bool,StateT extends Type<StateT>>

Throws:

ExpressionFactoryException