pyk.cterm.cterm module

class CSubst(subst: Subst | None = None, constraints: Iterable[KInner] = ())

Bases: object

Store information about instantiation of a symbolic state (CTerm) to a more specific one.

Contains the data: - subst: assignment to apply to free variables in the state to achieve more specific one - constraints: additional constraints over the free variables of the original state and the subst to add to the new state

add_constraint(constraint: KInner) → CSubst

Return this CSubst with an additional constraint added.

apply(cterm: CTerm) → CTerm

Apply this CSubst to the given CTerm (instantiating the free variables, and adding the constraints).

property constraint: KInner

Return the set of constraints as a single flattened constraint using mlAnd.

constraints: tuple[KInner, ...]

static from_dict(dct: dict[str, Any]) → CSubst

Deserialize CSubst from a dictionary representation.

subst: Subst

to_dict() → dict[str, Any]

Serialize CSubst to dictionary representation.

class CTerm(config: KInner, constraints: Iterable[KInner] = ())

Bases: object

Represent a symbolic program state, obtained and manipulated using symbolic execution.

Contains the data: - config: the _configuration_ (structural component of the state, potentially containing free variabls) - constraints: conditiions which limit/constraint the free variables from the config

add_constraint(new_constraint: KInner) → CTerm

Return a new CTerm with the additional constraints.

anti_unify(other: CTerm, keep_values: bool = False, kdef: KDefinition | None = None) → tuple[CTerm, CSubst, CSubst]

Given two CTerm, find a more general CTerm which can instantiate to both.

Parameters:

• other – other CTerm to consider for finding a more general CTerm with this one.

• keep_values – do not discard information about abstracted variables in returned result.

• kdef – optional KDefinition to make analysis more precise.

Returns:

tuple cterm: CTerm, csubst1: CSubst1, csubst2: CSubst2 such that: - cterm: more general CTerm than either self or other - csubst1: constrained substitution to apply to cterm to obtain self - csubst2: constrained substitution to apply to cterm to obtain other

static bottom() → CTerm

Construct a CTerm representing no possible states.

cell(cell: str) → KInner

Access the contents of a named cell in the config, die on failure.

property cells: Subst

Return key-value store of the contents of each cell in the config.

config: KInner

constraints: tuple[KInner, ...]

property free_vars: frozenset[str]

Return the set of free variable names contained in this CTerm

static from_dict(dct: dict[str, Any]) → CTerm

Deserialize a CTerm from its dictionary representation.

static from_kast(kast: KInner) → CTerm

Interpret a given KInner as a CTerm by splitting the config and constraints (see CTerm.kast).

property hash: str

Unique hash representing the contents of this CTerm.

property is_bottom: bool

Check if a given CTerm is trivially empty.

property kast: KInner

Return the unstructured bare KInner representation of a CTerm (see CTerm.from_kast).

match(cterm: CTerm) → Subst | None

Find Subst instantiating this CTerm to the other, return None if no such Subst exists.

match_with_constraint(cterm: CTerm) → CSubst | None

Find CSubst instantiating this CTerm to the other, return None if no such CSubst exists.

remove_useless_constraints(keep_vars: Iterable[str] = ()) → CTerm

Return a new CTerm with constraints over unbound variables removed.

Parameters:

keep_vars – List of variables to keep constraints for even if unbound in the CTerm.

Returns:

A CTerm with the constraints over unbound variables removed.

to_dict() → dict[str, Any]

Serialize a CTerm to dictionary representation.

static top() → CTerm

Construct a CTerm representing all possible states.

try_cell(cell: str) → KInner | None

Access the contents of a named cell in the config, return None on failure.

anti_unify(state1: KInner, state2: KInner, kdef: KDefinition | None = None) → tuple[KInner, Subst, Subst]

Return a generalized state over the two input states.

Parameters:

• state1 – State to generalize over, represented as bare KInner. Assumption is that this is a bare configuration with no constraints attached.

• state2 – State to generalize over, represented as bare KInner. Assumption is that this is a bare configuration with no constraints attached.

• kdef – Optional KDefinition to make the analysis more precise.

Returns:

tuple state: KInner, subst1: Subst, subst2: Subst such that: - state: a symbolic state represented as KInner which is more general than state1 or state2. - subst1: a Subst which when applied to state recovers state1. - subst2: a Subst which when applied to state recovers state2.

cterm_build_claim(claim_id: str, init_cterm: CTerm, final_cterm: CTerm, keep_vars: Iterable[str] = ()) → tuple[KClaim, Subst]

Return a KClaim between the supplied initial and final states.

Parameters:

• claim_id – Label to give the claim.

• init_cterm – State to put on LHS of the rule (constraints interpreted as requires clause).

• final_cterm – State to put on RHS of the rule (constraints interpreted as ensures clause).

• keep_vars – Variables to leave in the side-conditions even if not bound in the configuration.

Returns:

tuple claim: KClaim, var_map: Subst: - claim: A KClaim with variable naming conventions applied so that it should be parseable by K frontend. - var_map: The variable renamings that happened to make the claim parseable by K frontend (which can be undone to recover original variables).

cterm_build_rule(rule_id: str, init_cterm: CTerm, final_cterm: CTerm, priority: int | None = None, keep_vars: Iterable[str] = ()) → tuple[KRule, Subst]

Return a KRule between the supplied initial and final states.

Parameters:

• rule_id – Label to give the rule.

• init_cterm – State to put on LHS of the rule (constraints interpreted as requires clause).

• final_cterm – State to put on RHS of the rule (constraints interpreted as ensures clause).

• priority – Rule priority to give to the generated KRule.

• keep_vars – Variables to leave in the side-conditions even if not bound in the configuration.

Returns:

tuple claim: KRule, var_map: Subst such that: - rule: A KRule with variable naming conventions applied so that it should be parseable by K frontend. - var_map: The variable renamings that happened to make the claim parseable by K frontend (which can be undone to recover original variables).