claripy.frontends.composite_frontend.CompositeFrontend

class documentation

class CompositeFrontend(ConstrainedFrontend): (source)

Known subclasses: claripy.solvers.SolverComposite

Undocumented

Method	`__getstate__`	Undocumented
Method	`__init__`	Undocumented
Method	`__setstate__`	Undocumented
Method	`add`	Adds constraint(s) to constraints list.
Method	`batch_eval`	Evaluates `exprs`, returning a list of tuples (one tuple of `n` solutions for expression).
Method	`check_satisfiability`	Checks the satisfiability of stored constraints conjunction.
Method	`combine`	Undocumented
Method	`downsize`	Undocumented
Method	`eval`	Evaluates expression `e`, returning a tuple of `n` solutions.
Method	`finalize`	Undocumented
Method	`is_false`	Checks if `e` can only (and TRIVIALLY) evaluate to False. If this function returns True, then the expression cannot ever be True, regardless of constraints or anything else. If the expression returns False, then the expression might STILL not ever be True; it's just that we can't trivially prove it...
Method	`is_true`	Checks if `e` can only (and TRIVIALLY) evaluate to True. If this function returns True, then the expression cannot ever be False, regardless of constraints or anything else. If the expression returns False, then the expression might STILL not ever be False; it's just that we can't trivially prove it...
Method	`max`	Evaluates `e`, returning its max possible value.
Method	`max_memory.setter`	Undocumented
Method	`merge`	Undocumented
Method	`min`	Evaluates `e`, returning its min possible value.
Method	`satisfiable`	Checks if stored constraints conjunction is satisfiable.
Method	`simplify`	Simplifies the stored constraints conjunction.
Method	`solution`	Checks if `v` is a possible solution to `e`.
Method	`split`	Undocumented
Method	`timeout.setter`	Undocumented
Method	`unsat_core`	Undocumented
Method	`variables.setter`	Undocumented
Instance Variable	`constraints`	Undocumented
Property	`max_memory`	Undocumented
Property	`timeout`	Undocumented
Property	`variables`	Undocumented
Static Method	`_merge_with_ancestor`	Undocumented
Static Method	`_names_for`	Undocumented
Method	`_add_dependent_constraints`	Undocumented
Method	`_blank_copy`	Undocumented
Method	`_claim`	Undocumented
Method	`_copy`	Undocumented
Method	`_ensure_sat`	Undocumented
Method	`_merged_solver_for`	Undocumented
Method	`_reabsorb_solver`	Undocumented
Method	`_shared_solvers`	Returns a sequence of the solvers that self and others share.
Method	`_shared_varsets`	Undocumented
Method	`_solver_for_names`	Get a merged child solver for variables specified in `names`.
Method	`_solvers_for_variables`	Undocumented
Method	`_split_child`	Undocumented
Method	`_store_child`	Undocumented
Method	`_variable_sets`	Undocumented
Instance Variable	`_owned_solvers`	Undocumented
Instance Variable	`_solvers`	Undocumented
Instance Variable	`_template_frontend`	Undocumented
Instance Variable	`_template_frontend_string`	Undocumented
Instance Variable	`_track`	Undocumented
Instance Variable	`_unchecked_solvers`	Undocumented
Instance Variable	`_unsat`	Undocumented
Property	`_solver_list`	Undocumented

Inherited from ConstrainedFrontend:

Method	`independent_constraints`	Undocumented
Instance Variable	`_finalized`	Undocumented

Inherited from Frontend (via ConstrainedFrontend):

Method	`blank_copy`	Undocumented
Method	`branch`	Undocumented
Method	`eval_to_ast`	Evaluates expression `e`, returning a list of `n` concrete ASTs.
Static Method	`_split_constraints`	Returns independent constraints, split from this Frontend's `constraints`.
Method	`_concrete_value`	Undocumented
Method	`_constraint_filter`	Undocumented

def __getstate__(self): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.__getstate__

Undocumented

def __init__(self, template_frontend, template_frontend_string, track=False, **kwargs): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.__init__

overridden in claripy.solvers.SolverComposite

Undocumented

def __setstate__(self, s): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.__setstate__

Undocumented

def add(self, constraints, **kwargs): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.add

Adds constraint(s) to constraints list. :param constraints: constraint(s) to add :return:

def batch_eval(self, exprs, n, extra_constraints=(), exact=None): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.batch_eval

Evaluates `exprs`, returning a list of tuples (one tuple of `n` solutions for expression). :param exprs: expressions :param n: the number of solutions to return :param extra_constraints: extra constraints to consider when performing the evaluation :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: list of tuples of python primitives representing results

def check_satisfiability(self, extra_constraints=(), exact=None): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.check_satisfiability

Checks the satisfiability of stored constraints conjunction. :param extra_constraints: extra constraints to consider when checking satisfiability :param exact: whether or not to perform exact checking. Ignored by non-approximating backends. :return: 'SAT' if the conjunction is satisfiable otherwise 'UNSAT'

def combine(self, others): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.combine

Undocumented

def downsize(self): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.downsize

Undocumented

def eval(self, e, n, extra_constraints=(), exact=None): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.eval

Evaluates expression `e`, returning a tuple of `n` solutions. :param e: the expression :param n: the number of solutions to return :param extra_constraints: extra constraints to consider when performing the evaluation :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: tuple of python primitives representing results

def finalize(self): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.finalize

Undocumented

def is_false(self, e, extra_constraints=(), exact=None): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.is_false

Checks if `e` can only (and TRIVIALLY) evaluate to False. If this function returns True, then the expression cannot ever be True, regardless of constraints or anything else. If the expression returns False, then the expression might STILL not ever be True; it's just that we can't trivially prove it. In other words, a return value of False gives you no information whatsoever. :param e: the expression :param extra_constraints: extra constraints to consider when performing the evaluation :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: True if it can only evaluate to False otherwise False

def is_true(self, e, extra_constraints=(), exact=None): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.is_true

Checks if `e` can only (and TRIVIALLY) evaluate to True. If this function returns True, then the expression cannot ever be False, regardless of constraints or anything else. If the expression returns False, then the expression might STILL not ever be False; it's just that we can't trivially prove it. In other words, a return value of False gives you no information whatsoever. :param e: the expression :param extra_constraints: extra constraints to consider when performing the evaluation :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: True if it can only evaluate to True otherwise False

def max(self, e, extra_constraints=(), signed=False, exact=None): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.max

Evaluates `e`, returning its max possible value. :param e: the expression :param extra_constraints: extra constraints to consider when performing the evaluation :param signed: whether the value should be treated as a signed integer :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: max possible value

@max_memory.setter
def max_memory(self, val): (source) ¶

Undocumented

def merge(self, others, merge_conditions, common_ancestor=None): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.merge

Undocumented

def min(self, e, extra_constraints=(), signed=False, exact=None): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.min

Evaluates `e`, returning its min possible value. :param e: the expression :param extra_constraints: extra constraints to consider when performing the evaluation :param signed: whether the value should be treated as a signed integer :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: min possible value

def satisfiable(self, extra_constraints=(), exact=None): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.satisfiable

Checks if stored constraints conjunction is satisfiable. :param extra_constraints: extra constraints to consider when checking satisfiability :param exact: whether or not to perform exact checking. Ignored by non-approximating backends. :return: True if the conjunction is satisfiable otherwise False

def simplify(self): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.simplify

Simplifies the stored constraints conjunction.

def solution(self, e, v, extra_constraints=(), exact=None): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.solution

Checks if `v` is a possible solution to `e`. :param e: the expression :param v: the value :param extra_constraints: extra constraints to consider when performing the evaluation :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: True if it is a possible solution otherwise False

def split(self): (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.split

Undocumented

@timeout.setter
def timeout(self, t): (source) ¶

Undocumented

def unsat_core(self, extra_constraints=()): (source) ¶

Undocumented

@variables.setter
def variables(self, v): (source) ¶

Undocumented

constraints = (source) ¶

overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.constraints

Undocumented