Constraints on start of block.

This datatype maintains equality constraints between locations and stack offsets. It is used in jump bounds and other analysis libraries where we want to know when two registers or stack locations are equal.

A constraint on the value stored in a location (i.e., register or stack offset) at the start of block executino.

Pretty print the lines in stack constraints.

Return an expression equivalent to the location in the constraint map.

This attempts to normalize the expression to get a representative.

blockStartLocStackOffset c l determines if l has the form stack_frame + o using the constraints c for some stack offset o.

If it does, then this returns Just o. Otherwise it returns Nothing.

Constraint on a class representative

boundsLocRep cns loc returns the representative location for loc.

This representative location has the property that a location must have the same value as its representative location, and if two locations have provably equal values in cns, then they must have the same representative.

A location within a function tracked by our bounds analysis algorithms.

Locations for these purposes are registers, stack offsets, and global memory offsets.

Return a jump bounds that implies both input bounds, or Nothing if every fact inx the old bounds is implied by the new bounds.

Maps representatives from old and new join constraints to representative in merged map.

Information about bounds for a particular value within a block.

Create index bounds from initial index bounds.

Bounds at execution start.

Return the value of the index expression given the bounds.

This is an expression that represents the value of stack locations and assignments during steping through the block.

The main diference between this and the Value type, index expressions do not depend on values read and written to memory during execution of the block, and are purely functions of the input

This is different from ClassPred in that ClassPred is a property assigned to equivalence classes

Return an expression associated with the AssignRhs.

Associate the given bound expression with the assignment.

Discard information about memory due to an operation that may affect arbitrary memory.

Update the stack to point to the given expression.

Bounds for block after jump

Minimal information needed to update stack constraints after a call.

Return the index bounds after a function call.

A map from BoundLoc locations to values.

An empty location map.

Return true if map is null.

Construct a list out of a location map.

Return value associated with location or nothing if it is not defined.

This associates the location with a value in the map, replacing any existing binding.

It is prefixed with "nonOverlap" because it doesn't guarantee that stack values are non-overlapping -- the user should ensure this before calling this.

Pretty print a location map.

Fold over values in a location map.

This is a data structure for representing values written to concrete offsets in memory.

The offset type is a parameter so that we can use signed or unsigned offsets.

Empty stack map

Lookup value (if any) at given offset and representation.

Lookup value (if any) at given offset and representation.

This generalized memMapLookup below to not require exact matches, but just some overlap.

Result returned by memMapLookup.

This assigns a region of bytes to a particular value in the stack.

It overwrites any values that overlap with the location.

Return a list of locations and associated expressions that represent equivalence classes in the next state.

Note that each equivalence class has a unique stack expression, so all the locations in an equivalence class should have the same expression.

A value with a particular type along with a MemRepr indicating how the type is encoded in memory.