:py:mod:`cozy.analysis`
=======================

.. py:module:: cozy.analysis


Module Contents
---------------

Classes
~~~~~~~

.. autoapisummary::

   cozy.analysis.StateDiff
   cozy.analysis.CompatiblePair
   cozy.analysis.Comparison



Functions
~~~~~~~~~

.. autoapisummary::

   cozy.analysis._invalid_stack_addrs
   cozy.analysis._invalid_stack_overlap
   cozy.analysis.hexify



.. py:function:: _invalid_stack_addrs(st: angr.SimState) -> range


.. py:function:: _invalid_stack_overlap(invalid_stack_left: range, invalid_stack_right: range, stack_change: int)


.. py:class:: StateDiff


   StateDiff encapsulates the memoized state used by the difference method. This class is used internally by    Comparison and is typically not for external use.

   .. py:method:: difference(sl: angr.SimState, sr: angr.SimState, ignore_addrs: collections.abc.Iterable[range] | None = None, compute_mem_diff=True, compute_reg_diff=True, use_unsat_core=True) -> tuple[dict[range, tuple[claripy.ast.bits, claripy.ast.bits]], dict[str, tuple[claripy.ast.bits, claripy.ast.bits]]] | None

      Compares two states to find differences in memory. This function will return None if the two states have        non-intersecting inputs. Otherwise, it will return a dict of addresses and a dict of registers which are        different between the two. This function is based off of        angr.analyses.congruency_check.CongruencyCheck().compare_states, but has been customized for our purposes. Note        that this function may use memoization to enhance performance.

      :param SimState sl: The first state to compare
      :param SimState sr: The second state to compare
      :param collections.abc.Iterable[range] | None ignore_addrs: Memory addresses to ignore when doing the memory        diffing. This representation is more efficient than a set of integers since the ranges involved can be quite        large.
      :param bool compute_mem_diff: If this flag is True, then we will diff the memory. If this is false, then the        first element of the return tuple will be None.
      :param bool compute_reg_diff: If this flag is True, then we will diff the registers. If this is false, then the        second element of the return tuple will be None.
      :param bool use_unsat_core: If this flag is True, then we will use unsat core optimization to speed up        comparison of pairs of states. This option may cause errors in Z3, so disable if this occurs.
      :return: None if the two states are not compatible, otherwise returns a tuple containing the memory and        register differences.
      :rtype: tuple[dict[range, tuple[claripy.ast.bits, claripy.ast.bits]], dict[str, tuple[claripy.ast.bits, claripy.ast.bits]]] | None



.. py:function:: hexify(val0)

   Recursively transforms all integers in a Python datastructure (that is mappable with functools_ext.fmap) to hex strings.

   :param val0: The datastructure to traverse.
   :return: A deep copy of the datastructure, with all integers converted to hex strings.


.. py:class:: CompatiblePair(state_left: cozy.terminal_state.TerminalState, state_right: cozy.terminal_state.TerminalState, mem_diff: dict[range, tuple[claripy.ast.Base, claripy.ast.Base]], reg_diff: dict[str, tuple[claripy.ast.Base, claripy.ast.Base]], mem_diff_ip: dict[int, tuple[frozenset[claripy.ast.Base]], frozenset[claripy.ast.Base]], compare_std_out: bool, compare_std_err: bool)


   Stores information about comparing two compatible states.

   :ivar TerminalState state_left: Information pertaining specifically to the pre-patched state being compared.
   :ivar TerminalState state_right: Information pertaining specifically to the post-patched state being compared.
   :ivar dict[range, tuple[claripy.ast.Base, claripy.ast.Base]] mem_diff: Maps memory addresses to pairs of claripy    ASTs, where the left element of the tuple is the data in memory for state_left, and the right element of the tuple    is what was found in memory for state_right. Only memory locations that are different are saved in this dict.
   :ivar dict[str, tuple[claripy.ast.Base, claripy.ast.Base]] reg_diff: Similar to mem_diff, except that the dict is    keyed by register names. Note that some registers may be subparts of another. For example in x64, EAX is a    subregister of RAX.
   :ivar dict[int, tuple[frozenset[claripy.ast.Base]], frozenset[claripy.ast.Base]] mem_diff_ip: Maps memory addresses    to a set of instruction pointers that the program was at when it wrote that byte in memory. In most cases the    frozensets will have a single element, but this may not be the case in the scenario where a symbolic value    determined the write address.
   :ivar bool compare_std_out: If True then we should consider stdout when checking if the two input states are equal.
   :ivar bool compare_std_err: If True then we should consider stderr when checking if the two input states are equal.

   .. py:method:: equal() -> bool

      Determines if the two compatible states are observationally equal. That is, they contain the same memory        contents, registers, stdout, and stderr after execution.

      :return: True if the two compatible states are observationally equal, and False otherwise.
      :rtype: bool


   .. py:method:: concrete_examples(args: any, num_examples=3) -> list[cozy.concrete.CompatiblePairInput]

      Concretizes the arguments used to put the program in these states by jointly using the constraints attached to        the compatible states.

      :param any args: The input arguments to concretize. This argument may be a Python datastructure, the        concretizer will make a deep copy with claripy symbolic variables replaced with concrete values.
      :param int num_examples: The maximum number of concrete examples to generate for this particular pair.
      :return: A list of concrete inputs that satisfy both constraints attached to the states.
      :rtype: list[CompatiblePairInput]



.. py:class:: Comparison(pre_patched: cozy.session.RunResult, post_patched: cozy.session.RunResult, ignore_addrs: list[range] | None = None, ignore_invalid_stack=True, compare_memory=True, compare_registers=True, compare_std_out=False, compare_std_err=False, use_unsat_core=True)


   This class stores all compatible pairs and orphaned states. An orphan state is one in which there is no compatible    state in the other execution tree. In most scenarios there will be no orphaned states.

   :ivar dict[tuple[SimState, SimState], CompatiblePair] pairs: pairs stores a dictionary that maps a pair of    (pre_patch_state, post_patch_state) compatible states to their comparison information
   :ivar set[TerminalState] orphans_left: Pre-patched states for which there are 0 corresponding compatible states in    the post-patch
   :ivar set[TerminalState] orphans_right: Post-patched states for which there are 0 corresponding compatible states    in the pre-patch

   Compares a bundle of pre-patched states with a bundle of post-patched states.

   :param project.RunResult pre_patched: The pre-patched state bundle
   :param project.RunResult post_patched: The post-patched state bundle
   :param list[range] | None ignore_addrs: A list of addresses ranges to ignore when comparing memory.
   :param bool ignore_invalid_stack: If this flag is True, then memory differences in locations previously        occupied by the stack are ignored.
   :param bool compare_memory: If True, then the analysis will compare locations in the program memory.
   :param bool compare_registers: If True, then the analysis will compare registers used by the program.
   :param bool compare_std_out: If True, then the analysis will save stdout written by the program in the results.        Note that angr currently concretizes values written to stdout, so these values will be binary strings.
   :param bool compare_std_err: If True, then the analysis will save stderr written by the program in the results.
   :param bool use_unsat_core: If this flag is True, then we will use unsat core optimization to speed up        comparison of pairs of states. This option may cause errors in Z3, so disable if this occurs.

   .. py:method:: get_pair(state_left: angr.SimState, state_right: angr.SimState) -> CompatiblePair

      Retrieves a CompatiblePair given two compatible input states.

      :param SimState state_left: The pre-patched state
      :param SimState state_right: The post-patched state
      :return: The CompatiblePair object corresponding to this compatible state pair.
      :rtype: CompatiblePair


   .. py:method:: is_compatible(state_left: angr.SimState, state_right: angr.SimState) -> bool

      Returns True when the two input states are compatible based on the pairs stored in this object, and False        otherwise.

      :param SimState state_left: The pre-patched state
      :param SimState state_right: The post-patched state
      :return: True if the input states are compatible, and False otherwise
      :rtype: bool


   .. py:method:: __iter__() -> collections.abc.Iterator[CompatiblePair]

      Iterates over compatible pairs stored in the comparison.

      :return: An iterator over compatible pairs.
      :rtype: Iterator[CompatiblePair]


   .. py:method:: verify(verification_assertion: Callable[[CompatiblePair], claripy.ast.Base | bool]) -> list[CompatiblePair]

      Determines what compatible state pairs are valid with respect to a verification assertion. Note that the        comparison results are verified with respect to the verification_assertion if the returned list is empty        (has length 0).

      :param Callable[[CompatiblePair], claripy.ast.Base | bool] verification_assertion: A function which takes in a        compatible pair and returns a claripy expression which must be satisfiable for all inputs while under the        joint constraints of the state pair. Alternatively the function can return a bool. If the return value        is False, this will be considered a verification failure. If the return value is True, this will be considered        a verification success.
      :return: A list of all compatible pairs for which there was a concrete input that caused the verification        assertion to fail.
      :rtype: list[CompatiblePair]


   .. py:method:: report(args: any, concrete_arg_mapper: Callable[[any], any] | None = None, num_examples: int = 3) -> str

      Generates a human-readable report of the result object, saved as a string. This string is suitable for printing.

      :param any args: The symbolic/concolic arguments used during exeuction, here these args are concretized so that        we can give examples of concrete input.
      :param Callable[[any], any] | None concrete_arg_mapper: This function is used to post-process concretized        versions of args before they are added to the return string. Some examples of this function include converting        an integer to a negative number due to use of two's complement, or slicing off parts of the argument based on        another part of the input arguments.
      :param int num_examples: The number of concrete examples to show the user.
      :return: A human-readable summary of the comparison.
      :rtype: str



