Processor/memory state after at beginning of a block.

Update the block state to point to a specific IP address.

Returns true if return address is known to sit on stack.

Minimal information needed to update stack constraints after a call.

This updates the registers after a call has been performed.

The AbsBlockStack describes offsets of the stack. Values that are not in the map may denote any values.

The stack grows down, so negative keys are in the stack frame.

This constructs the abstract state for the start of the function.

It populates the register state with abstract values from the provided map, along with defaults for the instruction pointer and stack pointer. The provided list provides abstract values to be placed on the stack.

NOTE: It does not place the return address as where that is stored is architecture-specific.

The type of abstract values associated with a given architecture.

This is only a function of the address width.

The abstract information that is associated with values of a given type.

The first parameter is the width of pointers on the value. It is expected to be at most 64 bits.

Denotes that we do not know of any value that could be in set.

Construct a abstract value for a pointer to a code address.

Join the old and new states and return the updated state iff the result is larger than the old state. This also returns any addresses that are discarded during joining.

Smart constructor for sub-values. This ensures that the subvalues are sorted on size.

Returns a set of concrete integers that this value may be. This function will neither return the complete set or an known under-approximation.

Returns single value, if the abstract value can only take on one value.

This represents an lattice order.

Elements are comparable for equality, have a partial order, a top element, and the ability to join to elements.

This stores the abstract state of the system which may be within a block.

Recognizer for code addresses.

Construct a abstate processor state for the start of block execution.

A lens that allows one to lookup and update the value of an assignment in map from assignments to abstract values.

Smart constructor for strided intervals which takes care of top

Return state for after value has run.

Update the processor state with a memory write.

Update the processor state with a potential memory write.

Compute abstract value from value and current registers.

abstractULt x y refines x and y with the knowledge that x < y is unsigned. For example, given {2, 3} and {2, 3, 4}, we know (only) that {2, 3} and {3, 4} because we may pick any element from either set.

abstractULeq u v returns a pair (u',v') where for each x in u, and y in v, such that x <= y, we have that x in u' and y in v'.

Returns true if this value represents the empty set.