Choice.py

from pymwp import Choices

Choice module generates a compact representation of analysis derivation result.

The Choice module allows determining valid derivation choices and analyzing available choices. By default, the term valid means derivations that do not fail, i.e., give \(\infty\) in matrix; but other interpretations of valid choice can be defined also.

Determining valid derivation choices

Inputs:

• index: int degree of choice; total number of derivation choices in an analyzed program.
• domain: List[int] possible inference choices at a program point, e.g. [0,1,2].
• delta_sequences: Set[SEQ] sequences of choices to negate.

For example, to obtain derivation choices excluding failing derivations (\(\infty\) in matrix), the delta_sequences should be all sequences of deltas with scalar i.

The choice module converts the delta sequences to their negated choices, in a compact regular expression-like format:

# Input:
index = 3
domain = [0, 1, 2]
delta_sequences = {((0, 0), (2, 1)), ((1, 1),)}

# Output:
[[[1, 2], [0, 2], [0, 1, 2]], 
 [[0, 1, 2], [0], [0, 1, 2]]] 

A regular expression matching the output is ([1|2][0|2][0-2])|([0-2]0[0-2]).

Steps

1. Simplify. Using \(\delta\)-sequences set, simplify it:

   1. Replace combinations that can be represented by a single shorter sequence.
   2. Remove supersets.
   3. Preemptively remove deltas that would lead to invalid choice vectors.

   Apply simplifications iteratively until convergence.

   Simplifications

   This example assumes domain = [0,1,2].

   (A) All possible choices occur at index 0: any choice followed by sequence (2,1)(1,2) results in infinity. Therefore, remove \(a, b, c\) and insert [(2,1)(1,2)] in their place. Choices are reduced similarly from both ends.

   BEFORE                           AFTER
   [(0,0)(2,1)(1,2)]     # a        [(2,1)(1,2)]
   [(1,0)(2,1)(1,2)]     # b
   [(2,0)(2,1)(1,2)]     # c
   

   (B) Sequence \(a\) is subset of \(b\). Since \(b\) cannot be selected without selecting \(a\), discard \(b\).

   BEFORE                           AFTER
   [(0,0)]               # a        [(0,0)]
   [(0,0)(0,1)(2,2)]     # b
   

   (C) Constructing a choice vector requires selecting deltas from each remaining sequence \(a, b, c\). Therefore, deltas (0,0) and (1,0) must always be selected, and one of \(c\), [(2,0)(2,1)(1,2)]. However, selecting (0,0), (1,0), and (2,0) eliminates all choices at index 0. This allows to reduce sequences \(c\) to (2,1)(1,2).

   BEFORE                           AFTER
   [(0,0)]               # a        [(0,0)]
   [(1,0)]               # b        [(1,0)] 
   [(2,0)(2,1)(1,2)]     # c        [(2,1)(1,2)]
   

2. Build choice vectors. Initially consider all choices as valid. Then eliminate unwanted sequences, for all possible combinations.

   Compute cross product of remaining \(\delta\)-sequences. Iterate the product, for each:

   • Create a vector whose length is index.
   • Each vector element is a set of choices defined by domain.
   • Eliminate choices that lead to an unwanted outcome.

   Discard invalid and redundant vectors. Add remaining vectors to result.

   Choice vector generation

   # remaining after simplification
   sequences = [[(0,0)], [(1,0)], [(2,1)(1,2)], [(2,0)(1,1)(1,2)]]
   
   # compute a cross product of sequences (6 total)
   choice_paths = [[(0,0) (1,0) (2,1) (2,0)],
                   [(0,0) (1,0) (2,1) (1,1)],
                   [(0,0) (1,0) (2,1) (1,2)],…]
   
   for each path:
   
       # initialize a vector with all choices at each index
       vector_init = [{0,1,2}, {0,1,2}, {0,1,2}]
   
       # eliminate path choices, and add to result:
       vector_final = [[2], [0], [0,1,2]] 
   

3. Result. The result is a disjunction of choice vectors. Choose one vector, then select one value at each vector index. This yields a valid derivation result. For example, for a choice vector,

   [[[2], [0],   [0,1,2]],
    [[1], [1,2], [0,1,2]]]  
   

   selecting \((1, 2, 2)\) is valid choice, so is \((2, 0, 2)\) and \((1, 1, 0)\), …etc.

   • If all choices are valid, the Choice vector has a single vector permitting all choices.
   • If no valid derivation exists, the result is empty choice: [ ].
   • If index=0, i.e., no choice needs to be made, also result is empty [ ].

---

Choices

Choices(valid: CHOICES = None, index: int = -1)

A compact representation of derivation choices.

Attributes:

Name	Type	Description
valid	CHOICES	list of choice vectors.
index	int	degree of choice.

Initialize representation from a precomputed vector.

This is primarily useful for restoring a result from file. To create a choice representation, call generate() instead.

first property

first: Optional[tuple[int]]

Gets the first valid derivation choice, if at least one exists.

infinite property

infinite

True if no valid choice exists.

n_bounds property

n_bounds: int

Number of bounds that can be generated from a choice vector. This is calculated directly from the vector form. It is the product of number of choices at each index: \(\prod_{c \in v} |c|\).

Example

1. Vector [[0, 1, 2], [0, 1, 2], [0]] allows making [3, 3, 1] choices/index. It has \(3 * 3 * 1 = 9\) total bounds.

2. A vector with choices/index: [3, 1, 2, 1, 3, 3] has \(3^3 * 2^1 * 1^2 = 54\) possible bounds.

Returns:

Type	Description
int	Number of possible choices (non-distinct).

all

all() -> Generator[Tuple[int, ...]]

Generator for all valid derivation choices.

Note

Calling this method is very inefficient. Generally, we do not want to generate all choices. The method yields the next value in series, so it is possible to step through the choices one at a time. Use with caution/only call if necessary.

Yields:

Type	Description
Generator[Tuple[int, ...]]	The next valid choice.

build_choices staticmethod

build_choices(domain: List[int], index: int, infinities: Set[SEQ]) -> CHOICES

Build a list of distinct choice vectors excluding unwanted choices.

This method works by taking a list of delta paths that give unwanted scalars (e.g., \(\infty\)) and then negates those choices; the result is a list of choice vectors such that any remaining choice will give a valid derivation.

Example

• Assume paths leading to \(\infty\) are: [(0,0)], [(1,0)], [(1,1)(0,3)].
• The choices that do not lead to \(\infty\) are: [[[2], [0,2], [0,1,2]] or [[2], [0,1,2], [1,2]]].

Parameters:

Name	Type	Description	Default
domain	List[int]	list of valid choices for one index, e.g. [0, 1, 2].	required
index	int	the length of the vector, e.g. 10.	required
infinities	Set[SEQ]	set of deltas that lead to unwanted choices.	required

Returns:

Type	Description
CHOICES	Choice vector that excludes all paths leading to unwanted choices.

except_one staticmethod

except_one(domain: List[int], sequences: Set[SEQ]) -> Set[SEQ]

Look for deltas of length=1 where all-but-one choices are made at same index. The remaining one choice can be eliminated from paths that contain it, because it would yield an invalid choice vector.

Example

Given sequence ((0,0),), ((1,0),), ((2,0),(2,1),(1,4),) and the goal to build a choice vector. Deltas (0,0) and (1,0) must be chosen. For ((2,0),(2,1),(1,4),) one of the deltas must be chosen. But choosing (0,0), (1,0), (2,0) eliminates all choices at index 0. It suffices to keep sequence ((0,0),), ((1,0),), ((2,1),(1,4),).

Parameters:

Name	Type	Description	Default
domain	List[int]	list of valid per index choices, e.g. [0, 1, 2].	required
sequences	Set[SEQ]	set of delta sequences.	required

Returns:

Type	Description
Set[SEQ]	A set of sequences after applying simplification.

generate staticmethod

generate(domain: List[int], index: int, inf: Set[SEQ]) -> Choices

Generate the choice representation.

This works in two steps: (1) simplify delta sequences, (2) build choice vectors.

Parameters:

Name	Type	Description	Default
domain	List[int]	valid choices at index, e.g. [0, 1, 2].	required
index	int	the length of the vector, e.g. 10. This is the same as number of assignments in the analyzed function.	required
inf	Set[SEQ]	set of deltas that lead to infinity.	required

Returns:

Type	Description
Choices	Generated choice object.

intersection staticmethod

intersection(c1: Choices, c2: Choices) -> Choices

Intersection of two choice vectors.

Intersection is a cross-product of non-empty vector intersections. If the none of the vectors intersect, the resulting Choice is empty.

Parameters:

Name	Type	Description	Default
c1	Choices	First Choice vector.	required
c2	Choices	Second Choice vector.	required

Returns:

Type	Description
Choices	New Choices representing the intersection of the two arguments.

is_valid

is_valid(*choices: int) -> bool

Checks if sequence of choices can be made without infinity.

Example

choice_obj.is_valid(0, 1, 2, 1, 1, 0)

Parameters:

Name	Type	Description	Default
choices	int	sequences of delta values to check.	()

Returns:

Type	Description
bool	True if the given choices can be made without infinity.

prod staticmethod

prod(values: list) -> int

Compute the product of numeric list.

Parameters:

Name	Type	Description	Default
values	list	1d list of numbers.	required

Returns:

Type	Description
int	Product of values.

reduce staticmethod

reduce(domain: List[int], sequences: Set[SEQ]) -> bool

Look for first reducible sequence, if exists, then replace it.

Example

We can reduce a sequences where deltas differ only on first value, never on index, and all possible choice values are represented in the first delta. Below, it does not matter which choice is made at index 0. The 3 paths can be collapsed into a single, shorter path: (2,1)(1,4).

(0,0) (2,1) (1,4)
(1,0) (2,1) (1,4)
(2,0) (2,1) (1,4)

Parameters:

Name	Type	Description	Default
domain	List[int]	list of valid per index choices, e.g. [0, 1, 2].	required
sequences	Set[SEQ]	set of delta sequences.	required

Returns:

Type	Description
bool	True if a reduction occurred and False otherwise. The meaning of False is to say the operation is done and should not be repeated any further.

reduce_end staticmethod

reduce_end(domain: List[int], sequences: Set[SEQ]) -> bool

Like reduce, but from end of sequence.

Example

When deltas only differ at last index, and all choices occur at last index, reduce choices to a shorter path. E.g., Below, choice at index 5 is irrelevant; keep (2,1) (1,4).

(2,1) (1,4) (0,5)
(2,1) (1,4) (1,5)
(2,1) (1,4) (2,5)

Parameters:

Name	Type	Description	Default
domain	List[int]	list of valid per index choices, e.g. [0, 1, 2].	required
sequences	Set[SEQ]	set of delta sequences.	required

Returns:

Type	Description
bool	True if a reduction occurred and False otherwise.

remove_subset staticmethod

remove_subset(match: SEQ, items: Union[Set, List])

If match is a subset of any item in items, removes the superset from items, in place.

Parameters:

Name	Type	Description	Default
match	SEQ	single delta sequence.	required
items	Union[Set, List]	list of delta sequences to check against match.	required

simplify staticmethod

simplify(domain: List[int], sequences: Set[SEQ]) -> Set[SEQ]

Generate the most simplified, equivalent representation of the set of choices that cause unwanted derivation results.

Reduce sequences of deltas, until set of sequences cannot be reduced any further. Then remove all superset contained by some shorter sequence. Lastly, remove deltas that would generate an invalid choice vector. This process repeats until no more simplification can be applied.

Parameters:

Name	Type	Description	Default
domain	List[int]	list of valid per index choices, e.g. [0, 1, 2].	required
sequences	Set[SEQ]	set of delta sequences.	required

Returns:

Type	Description
Set[SEQ]	Simplified list of infinity paths.

sub_equal staticmethod

sub_equal(first: SEQ, second: SEQ) -> bool

Compare two delta sequences for equality, except their 0th value.

Parameters:

Name	Type	Description	Default
first	SEQ	first delta sequence.	required
second	SEQ	second delta sequence.	required

Returns:

Type	Description
bool	True if two delta sequences are equal excluding the 0th value, and False otherwise.

sub_equal_end staticmethod

sub_equal_end(first: SEQ, second: SEQ) -> bool

Compare two delta sequences for equality, except their N-th value. This is like sub_equal, but comparison is done at the end of sequences.

Parameters:

Name	Type	Description	Default
first	SEQ	first delta sequence.	required
second	SEQ	second delta sequence.	required

Returns:

Type	Description
bool	True if two delta sequences are equal excluding the N-th value, and False otherwise.

to_choices staticmethod

to_choices(vectors: List[VECT]) -> CHOICES

Convert a list of vectors to CHOICES type. This is a simple type conversion over the inner collection-types.

unique_sequences staticmethod

unique_sequences(infinities: Set[SEQ]) -> Set[SEQ]

Remove superset delta sequences.

Parameters:

Name	Type	Description	Default
infinities	Set[SEQ]	set of delta sequences causing infinity.	required

Returns:

Type	Description
Set[SEQ]	A list where all longer sequences, whose pattern is covered by some shorter sequence, are removed.

vect_contains staticmethod

vect_contains(a: VECT, b: VECT) -> bool

Check if A allows making all choices of B.

Parameters:

Name	Type	Description	Default
a	VECT	first vector.	required
b	VECT	second vector.	required

Returns:

Type	Description
bool	True if A contains B, and False otherwise.

vect_intersection staticmethod

vect_intersection(a: VECT, b: VECT) -> Optional[VECT]

Intersection of two vectors.

The intersection is the maximal choice at each index, permitted by both vectors A and B. The intersection is empty if, at some index, no choice exists.

Example

Let a=((0,1),(0,2)), b=((1,),(1,2)), and c=((1,),(1,)).

• The intersection of a&b is ((1,),(2,)).
• The intersection of a&c is None.
• The intersection of b&c is ((1,),(1,)).

Parameters:

Name	Type	Description	Default
a	VECT	first vector.	required
b	VECT	second vector.	required

Returns:

Type	Description
Optional[VECT]	A new vector that is the intersection of A and B; None when the intersection is empty.

vect_new staticmethod

vect_new(vectors: Set[VECT], vector: VECT) -> bool

Determines if a vector is distinct from all existing vectors.

Parameters:

Name	Type	Description	Default
vectors	Set[VECT]	a set of known vectors.	required
vector	VECT	vector to check.	required

Returns:

Type	Description
bool	True if vector does not occur in vectors.

vect_rm staticmethod

vect_rm(vectors: Set[VECT], vector: VECT) -> None

Remove from vectors those that are contained by vector.

Parameters:

Name	Type	Description	Default
vectors	Set[VECT]	a set of vectors.	required
vector	VECT	vector compare against.	required