SimpleSolver is, by its name, a simple solver. Most of this solver is based on the (complex) simplification logic that the retypd paper describes and the retypd re-implementation (https://github.com/GrammaTech/retypd) implements. Additionally, we add some improvements to allow type propagation of known struct names, among a few other improvements.

__init__(bits, constraints, typevars, constraint_set_degradation_threshold=150, stackvar_max_sizes=None, tv_manager=None)¶

Parameters:

bits (int)
typevars (dict[TypeVariable, set[TypeVariable]])
constraint_set_degradation_threshold (int)
stackvar_max_sizes (dict[TypeVariable, int] | None)
tv_manager (TypeVariableManager | None)

processed_constraints_count: int

simplified_constraints_count: int

eqclass_constraints_count: list[int]

get_tv_max_stack_size(tv)¶

Get the potential maximum stack variable size of a given type variable, if any. Also considers other type variables that are equivalent to the given type variable.

Return type:: int | None
Parameters:: tv (TypeVariable)

preprocess(func_tv)¶

Parameters:: func_tv (TypeVariable)

solve()¶

Steps:

For each type variable, - Infer the shape in its sketch - Build the constraint graph - Collect all constraints - Apply constraints to derive the lower and upper bounds - Determine a solution for type variables with constraints - Rewrite the constraint graph by replacing determined type variables with their solutions - Solve repeatedly until all interesting type variables have solutions

By repeatedly solving until exhausting interesting type variables, we ensure the S-Trans rule is applied.

infer_shapes(typevars, constraints)¶

Computing sketches from constraint sets. Implements Algorithm E.1 in the retypd paper.

Return type:

tuple[dict, dict[TypeVariable, Sketch]]

Parameters:

typevars (set[TypeVariable])
constraints (set[TypeConstraint])

compute_quotient_graph(constraints)¶

Compute the quotient graph (the constraint graph modulo ~ in Algorithm E.1 in the retypd paper) with respect to a given set of type constraints.

Parameters:: constraints (set[TypeConstraint])

join(t1, t2)¶

Return type:

TypeConstant

Parameters:

t1 (TypeConstant)
t2 (TypeConstant)

meet(t1, t2)¶

Return type:

TypeConstant

Parameters:

t1 (TypeConstant)
t2 (TypeConstant)

classmethod join_simtypes(t1, t2, arch)¶

Compute the join (the least general common supertype) of two SimTypes on the type lattice.

The two types are lifted to internal type constants, joined on the base lattice for arch.bits, and the result is translated back into a SimType. When the two types have no meaningful common supertype, the result is a SimTypeBottom.

Parameters:

t1 (SimType) – The first SimType.
t2 (SimType) – The second SimType.
arch (Arch) – The architecture, used to determine the pointer size and to build the resulting SimType.

Return type:

SimType

Returns:

The join of t1 and t2 as a SimType.

classmethod meet_simtypes(t1, t2, arch)¶

Compute the meet (the greatest common subtype) of two SimTypes on the type lattice.

See join_simtypes() for details. When the two types have no meaningful common subtype, the result is a SimTypeBottom.

Return type:

SimType

Parameters:

t1 (SimType)
t2 (SimType)
arch (Arch)

static abstract(t)¶

Return type:: TypeConstant | TypeVariable
Parameters:: t (TypeConstant | TypeVariable)

determine(sketches, tvs, equivalence_classes, solution, nodes=None)¶

Determine C-like types from sketches.

Parameters:

sketches – A dictionary storing sketches for each type variable.
solution (dict) – The dictionary storing C-like types for each type variable. Output.
nodes (set[SketchNode] | None) – Optional. Nodes that should be considered in the sketch.
equivalence_classes (dict[TypeVariable, TypeVariable])

Return type:

None

Returns:

None

static dump_constraint_graph(graph, filename)¶

Dump the constraint graph to a file.

Return type:

None

Parameters:

graph (DiGraph)
filename (str)