cozy.concrete

Classes

CompatiblePairInput

Stores information about the concretization of a compatible state pair.

TerminalStateInput

Stores information about the concretization of a TerminalState.

Functions

concretize(→ list)

This function concretizes a bundle of symbolic data by generating up to n models for the symbols with respect to the constraints given in the passed solver

Module Contents

cozy.concrete.concretize(solver: claripy.Solver, symbolic_bundle: claripy.ast.Bits | list | tuple | dict | set | cozy.side_effect.PerformedSideEffect | cozy.nested_dict.NestedDict[claripy.ast.Bits], n: int = 1) → list

This function concretizes a bundle of symbolic data by generating up to n models for the symbols with respect to the constraints given in the passed solver

Parameters:

  • solver – The solver which contains the constraints over the symbols in the state bundle

  • symbolic_bundle – A bundle of symbolic or concrete mixed data, stored in arbitrarily nested Python data structures

  • n – The number of examples that we should attempt to generate

Returns:

A list of concretized examples generated for this specific symbolic_bundle. Note that the nesting of the data structures in the return list will be the same as the input bundle.

class cozy.concrete.CompatiblePairInput(args, mem_diff: dict[range, tuple[claripy.ast.Bits, claripy.ast.Bits]], reg_diff: dict[str, tuple[claripy.ast.Bits, claripy.ast.Bits]], left_side_effects: dict[str, list[cozy.side_effect.ConcretePerformedSideEffect]], right_side_effects: dict[str, list[cozy.side_effect.ConcretePerformedSideEffect]], left_annotation: cozy.nested_dict.NestedDict[claripy.ast.Base], right_annotation: cozy.nested_dict.NestedDict[claripy.ast.Base], left_ret_annotation: cozy.nested_dict.NestedDict[claripy.ast.Base], right_ret_annotation: cozy.nested_dict.NestedDict[claripy.ast.Base])

Stores information about the concretization of a compatible state pair.

Variables:

  • args (any) – The same Python datastructures as the arguments passed to concrete_examples, except that all claripy symbolic variables are replaced with concrete values.

  • mem_diff (dict[range, tuple[claripy.ast.Bits, claripy.ast.Bits]]) – Concretized version of memory difference. Each key is a memory address range, and each value is a concretized version of the data stored at that location for the prepatched, postpatched runs.

  • reg_diff (dict[str, tuple[claripy.ast.Bits, claripy.ast.Bits]]) – Concretized version of register difference. Each key is a register name, and each value is a concretized version of the data stored at that register for the prepatched, postpatched runs.

  • left_side_effects (dict[str, list[ConcretePerformedSideEffect]]) – Concretized versions of side effects made by the prepatched state.

  • right_side_effects (dict[str, list[ConcretePerformedSideEffect]]) – Concretized versions of side_effects made by the postpatched state.

  • left_annotation (NestedDict[claripy.ast.Base]) – Concretized version of the memory annotated with cozy.session.Session.annotate_memory() for the first program.

  • right_annotation (NestedDict[claripy.ast.Base]) – Concretized version of the memory annotated with cozy.session.Session.annotate_memory() for the second program.

  • left_ret_annotation (NestedDict[claripy.ast.Base]) – Concretized version of the annotated return results for the first program. These annotations were created via cozy.session.RunResult.annotate_return().

  • right_ret_annotation (NestedDict[claripy.ast.Base]) – Concretized version of the annotated return results for the second program. These annotations were created via cozy.session.RunResult.annotate_return()

args
mem_diff
reg_diff
left_side_effects
right_side_effects
left_annotation
right_annotation
left_ret_annotation
right_ret_annotation
class cozy.concrete.TerminalStateInput(args, side_effects: dict[str, list[cozy.side_effect.ConcretePerformedSideEffect]])

Stores information about the concretization of a TerminalState.

Variables:

  • args (any) – The same Python datastructures as the arguments passed to concrete_examples, except that all claripy symbolic variables are replaced with concrete values.

  • side_effects (dict[str, list[PerformedSideEffect]]) – Concretized side effects outputted by the singleton state.

args
side_effects