edu.nyu.cascade.ir.expr
Class BitVectorExpressionFactory

java.lang.Object
  edu.nyu.cascade.ir.expr.AbstractExpressionFactory<BitVectorExpression,BooleanExpression,ArrayType<BitVectorType,BitVectorType>>
      edu.nyu.cascade.ir.expr.BitVectorExpressionFactory

All Implemented Interfaces:

ExpressionFactory<BitVectorExpression,BooleanExpression,ArrayType<BitVectorType,BitVectorType>>

public class BitVectorExpressionFactory
extends AbstractExpressionFactory<BitVectorExpression,BooleanExpression,ArrayType<BitVectorType,BitVectorType>>

Field Summary

Fields inherited from class edu.nyu.cascade.ir.expr.AbstractExpressionFactory

FUN_ALLOCATED

Method Summary

BooleanExpression	allocated(BitVectorExpression loc, BitVectorExpression size) Returns a boolean expression representing the proposition that the memory location identified by ptr represents an allocated block of storage of size bytes (used in source code annotations).
BooleanExpression	and(BooleanExpression lhs, BooleanExpression rhs) Returns a boolean expression representing the conjunction of the two boolean arguments.
Expression<ArrayType<BitVectorType,BitVectorType>>	assign(Expression<ArrayType<BitVectorType,BitVectorType>> mem, BitVectorExpression var, BitVectorExpression val) Returns a new program state, representing the assignment of the value rval to the memory location lval in pre-state state.
BitVectorExpression	bitwiseAnd(BitVectorExpression lhs, BitVectorExpression rhs) Returns a boolean expression representing the bitwise AND of the two integer arguments.
BooleanExpression	castToBoolean(BitVectorExpression bv) Returns a boolean expression representing the integer value expr, according to the conversion rule of the underlying encoding.
BitVectorExpression	castToInteger(BooleanExpression bool) Returns an integer expression representing the boolean value bool, according to the conversion rule of the underlying encoding.
static BitVectorExpressionFactory	create(Map<File,? extends SymbolTable> symbolTables, ExpressionManager exprManager, int addressSize, int cellSize) Create an expression factory with the given pointer and word sizes.
static BitVectorExpressionFactory	create(Map<File,SymbolTable> symbolTables, ExpressionManager exprManager, ArrayType<BitVectorType,BitVectorType> memArrayType) Create an expression factory with the given array type to model memory.
static BitVectorExpressionFactory	create(Map<File,SymbolTable> symbolTables, ExpressionManager exprManager, ArrayVariableExpression<BitVectorType,BitVectorType> memArray)
BitVectorExpression	deref(BitVectorExpression expr) Returns an integer expression representing the value stored at the memory location identified by expression p.
BooleanExpression	eq(BitVectorExpression lhs, BitVectorExpression rhs) Returns a boolean expression comparing integers lhs and rhs for equality.
BooleanExpression	evalBoolean(BooleanExpression bool, Expression<ArrayType<BitVectorType,BitVectorType>> state) Evaluate the boolean expression e in state.
BitVectorExpression	evalExpression(BitVectorExpression expr, Expression<ArrayType<BitVectorType,BitVectorType>> state)
BooleanExpression	ff() Returns a boolean expression representing false.
protected BitVectorType	getAddressType()
ImmutableSet<? extends BooleanExpression>	getAssumptions() Get logical assumptions used in the underlying encoding.
protected BitVectorType	getCellType()
ArrayType<BitVectorType,BitVectorType>	getStateType() Returns the program state type of the underlying encoding.
BooleanExpression	greaterThan(BitVectorExpression lhs, BitVectorExpression rhs) Returns a boolean expression comparing integers lhs and rhs.
BooleanExpression	greaterThanOrEqual(BitVectorExpression lhs, BitVectorExpression rhs) Returns a boolean expression comparing integers lhs and rhs.
BitVectorExpression	ifThenElse(BooleanExpression bool, BitVectorExpression thenExpr, BitVectorExpression elseExpr) Returns an integer expression with the value of thenExpr if bool holds and the value of elseExpr otherwise.
<I extends Type<I>,E extends Type<E>> BitVectorExpression	indexArray(Expression<ArrayType<I,E>> array, BitVectorExpression index)
<I extends Type<I>,E extends Type<E>> BitVectorExpression	indexArray(Expression<ArrayType<I,E>> array, Iterable<? extends BitVectorExpression> indices)
BitVectorExpression	integerConstant(int c) Returns an integer expression representing the constant c.
BitVectorExpression	integerVar(String id, boolean fresh) Returns a integer expression representing the variable with name id.
BooleanExpression	lessThan(BitVectorExpression lhs, BitVectorExpression rhs) Returns a boolean expression comparing integers lhs and rhs.
BooleanExpression	lessThanOrEqual(BitVectorExpression lhs, BitVectorExpression rhs) Returns a boolean expression comparing integers lhs and rhs.
BitVectorExpression	minus(BitVectorExpression lhs, BitVectorExpression rhs) Returns an integer expression representing subtraction of the two integer arguments.
BooleanExpression	neq(BitVectorExpression lhs, BitVectorExpression rhs) Returns a boolean expression comparing integers lhs and rhs for disequality.
BooleanExpression	nor(Iterable<BooleanExpression> disjuncts) Returns an boolean expression that holds if none of the boolean elements of the Iterable disjuncts is true.
BooleanExpression	not(BooleanExpression b) Returns a boolean expression representing the negation of expression b.
BitVectorExpression	one() Returns an integer expression representing one.
BooleanExpression	or(BooleanExpression lhs, BooleanExpression rhs) Returns a boolean expression representing the logical OR the two boolean arguments.
BitVectorExpression	plus(BitVectorExpression lhs, BitVectorExpression rhs) Returns an integer expression representing the sum of the two integer arguments.
BooleanExpression	tt() Returns a boolean expression representing true.
Type<?>	type(IRType t)
BitVectorExpression	unknown() Returns an integer expression representing an unknown value.
Object	variable(String name, IRType type, boolean fresh)
BitVectorExpression	zero() Returns an integer expression representing zero.

Methods inherited from class edu.nyu.cascade.ir.expr.AbstractExpressionFactory

decr, functionCall, functionCall, functionCall, getExpressionManager, getInitialState, incr, integerAnd, integerNot, integerOr

Methods inherited from class java.lang.Object

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

Method Detail

create

public static BitVectorExpressionFactory create(Map<File,SymbolTable> symbolTables,
                                                ExpressionManager exprManager,
                                                ArrayVariableExpression<BitVectorType,BitVectorType> memArray)
                                         throws ExpressionFactoryException

Throws:

ExpressionFactoryException

create

public static BitVectorExpressionFactory create(Map<File,SymbolTable> symbolTables,
                                                ExpressionManager exprManager,
                                                ArrayType<BitVectorType,BitVectorType> memArrayType)
                                         throws ExpressionFactoryException

Create an expression factory with the given array type to model memory. The size of the index type of the memory array (i.e., the size of a pointer) must be a multiple of the size of the element type (i.e., the size of a memory word).

Parameters:

symbolTables -

exprManager -

addressSize - the desired size of a pointer

cellSize - the desired size of a memory word (i.e., the unit of a pointer "step")

Throws:

IllegalArgumentException - if addressSize is not a multiple of cellSize

ExpressionFactoryException

create

public static BitVectorExpressionFactory create(Map<File,? extends SymbolTable> symbolTables,
                                                ExpressionManager exprManager,
                                                int addressSize,
                                                int cellSize)
                                         throws ExpressionFactoryException

Create an expression factory with the given pointer and word sizes. A pointer must be an integral number of words.

Parameters:

symbolTables -

exprManager -

addressSize - the desired size of a pointer

cellSize - the desired size of a memory word (i.e., the unit of a pointer "step")

Throws:

IllegalArgumentException - if addressSize is not a multiple of cellSize

ExpressionFactoryException

allocated

public BooleanExpression allocated(BitVectorExpression loc,
                                   BitVectorExpression size)
                            throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression representing the proposition that the memory location identified by ptr represents an allocated block of storage of size bytes (used in source code annotations). NOTE: Optional operation.

Throws:

ExpressionFactoryException

and

public BooleanExpression and(BooleanExpression lhs,
                             BooleanExpression rhs)
                      throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression representing the conjunction of the two boolean arguments.

Throws:

ExpressionFactoryException

assign

public Expression<ArrayType<BitVectorType,BitVectorType>> assign(Expression<ArrayType<BitVectorType,BitVectorType>> mem,
                                                                 BitVectorExpression var,
                                                                 BitVectorExpression val)
                                                          throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a new program state, representing the assignment of the value rval to the memory location lval in pre-state state.

Throws:

ExpressionFactoryException

bitwiseAnd

public BitVectorExpression bitwiseAnd(BitVectorExpression lhs,
                                      BitVectorExpression rhs)
                               throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression representing the bitwise AND of the two integer arguments.

Throws:

ExpressionFactoryException

castToBoolean

public BooleanExpression castToBoolean(BitVectorExpression bv)
                                throws ExpressionFactoryException

Description copied from class: AbstractExpressionFactory

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<BitVectorExpression,BooleanExpression,ArrayType<BitVectorType,BitVectorType>>

Overrides:

castToBoolean in class AbstractExpressionFactory<BitVectorExpression,BooleanExpression,ArrayType<BitVectorType,BitVectorType>>

Throws:

ExpressionFactoryException

castToInteger

public BitVectorExpression castToInteger(BooleanExpression bool)
                                  throws ExpressionFactoryException

Description copied from class: AbstractExpressionFactory

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<BitVectorExpression,BooleanExpression,ArrayType<BitVectorType,BitVectorType>>

Overrides:

castToInteger in class AbstractExpressionFactory<BitVectorExpression,BooleanExpression,ArrayType<BitVectorType,BitVectorType>>

Throws:

ExpressionFactoryException

deref

public BitVectorExpression deref(BitVectorExpression expr)
                          throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns an integer expression representing the value stored at the memory location identified by expression p. NOTE: Optional operation.

Throws:

ExpressionFactoryException

eq

public BooleanExpression eq(BitVectorExpression lhs,
                            BitVectorExpression rhs)
                     throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression comparing integers lhs and rhs for equality.

Throws:

ExpressionFactoryException

evalBoolean

public BooleanExpression evalBoolean(BooleanExpression bool,
                                     Expression<ArrayType<BitVectorType,BitVectorType>> state)
                              throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Evaluate the boolean expression e in state. The method is responsible for converting the underlying encoding of booleans Bool into an object of type IExpression<IBooleanType> that can be queried for validity/satisfiability.

Throws:

ExpressionFactoryException

evalExpression

public BitVectorExpression evalExpression(BitVectorExpression expr,
                                          Expression<ArrayType<BitVectorType,BitVectorType>> state)
                                   throws ExpressionFactoryException

Throws:

ExpressionFactoryException

ff

public BooleanExpression ff()
                     throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression representing false.

Throws:

ExpressionFactoryException

getAddressType

protected BitVectorType getAddressType()

getAssumptions

public ImmutableSet<? extends BooleanExpression> getAssumptions()
                                                         throws ExpressionFactoryException

Description copied from class: AbstractExpressionFactory

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<BitVectorExpression,BooleanExpression,ArrayType<BitVectorType,BitVectorType>>

Overrides:

getAssumptions in class AbstractExpressionFactory<BitVectorExpression,BooleanExpression,ArrayType<BitVectorType,BitVectorType>>

Throws:

ExpressionFactoryException

getCellType

protected BitVectorType getCellType()

getStateType

public ArrayType<BitVectorType,BitVectorType> getStateType()
                                                    throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns the program state type of the underlying encoding.

Throws:

ExpressionFactoryException

greaterThan

public BooleanExpression greaterThan(BitVectorExpression lhs,
                                     BitVectorExpression rhs)
                              throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression comparing integers lhs and rhs.

Throws:

ExpressionFactoryException

greaterThanOrEqual

public BooleanExpression greaterThanOrEqual(BitVectorExpression lhs,
                                            BitVectorExpression rhs)
                                     throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression comparing integers lhs and rhs.

Throws:

ExpressionFactoryException

ifThenElse

public BitVectorExpression ifThenElse(BooleanExpression bool,
                                      BitVectorExpression thenExpr,
                                      BitVectorExpression elseExpr)
                               throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns an integer expression with the value of thenExpr if bool holds and the value of elseExpr otherwise.

Throws:

ExpressionFactoryException

integerConstant

public BitVectorExpression integerConstant(int c)
                                    throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns an integer expression representing the constant c.

Throws:

ExpressionFactoryException

integerVar

public BitVectorExpression integerVar(String id,
                                      boolean fresh)
                               throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a integer expression representing the variable with name id.

fresh - TODO

Throws:

ExpressionFactoryException

lessThan

public BooleanExpression lessThan(BitVectorExpression lhs,
                                  BitVectorExpression rhs)
                           throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression comparing integers lhs and rhs.

Throws:

ExpressionFactoryException

lessThanOrEqual

public BooleanExpression lessThanOrEqual(BitVectorExpression lhs,
                                         BitVectorExpression rhs)
                                  throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression comparing integers lhs and rhs.

Throws:

ExpressionFactoryException

minus

public BitVectorExpression minus(BitVectorExpression lhs,
                                 BitVectorExpression rhs)

Description copied from interface: ExpressionFactory

Returns an integer expression representing subtraction of the two integer arguments.

neq

public BooleanExpression neq(BitVectorExpression lhs,
                             BitVectorExpression rhs)
                      throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression comparing integers lhs and rhs for disequality.

Throws:

ExpressionFactoryException

nor

public BooleanExpression nor(Iterable<BooleanExpression> disjuncts)
                      throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns an boolean expression that holds if none of the boolean elements of the Iterable disjuncts is true.

Throws:

ExpressionFactoryException

not

public BooleanExpression not(BooleanExpression b)
                      throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression representing the negation of expression b.

Throws:

ExpressionFactoryException

one

public BitVectorExpression one()
                        throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns an integer expression representing one.

Throws:

ExpressionFactoryException

or

public BooleanExpression or(BooleanExpression lhs,
                            BooleanExpression rhs)
                     throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression representing the logical OR the two boolean arguments.

Throws:

ExpressionFactoryException

plus

public BitVectorExpression plus(BitVectorExpression lhs,
                                BitVectorExpression rhs)

Description copied from interface: ExpressionFactory

Returns an integer expression representing the sum of the two integer arguments.

tt

public BooleanExpression tt()
                     throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns a boolean expression representing true.

Throws:

ExpressionFactoryException

unknown

public BitVectorExpression unknown()
                            throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns an integer expression representing an unknown value.

Throws:

ExpressionFactoryException

zero

public BitVectorExpression zero()
                         throws ExpressionFactoryException

Description copied from interface: ExpressionFactory

Returns an integer expression representing zero.

Throws:

ExpressionFactoryException

indexArray

public <I extends Type<I>,E extends Type<E>> BitVectorExpression indexArray(Expression<ArrayType<I,E>> array,
                                                                            BitVectorExpression index)

indexArray

public <I extends Type<I>,E extends Type<E>> BitVectorExpression indexArray(Expression<ArrayType<I,E>> array,
                                                                            Iterable<? extends BitVectorExpression> indices)

type

public Type<?> type(IRType t)
             throws ExpressionFactoryException

Throws:

ExpressionFactoryException

variable

public Object variable(String name,
                       IRType type,
                       boolean fresh)
                throws ExpressionFactoryException

Throws:

ExpressionFactoryException