claripy.frontends.light_frontend.LightFrontend

class documentation

class LightFrontend(ConstrainedFrontend): (source)

Known subclasses: claripy.solvers.SolverConcrete, claripy.solvers.SolverVSA

View In Hierarchy

Undocumented

Method __getstate__ Undocumented
Method __init__ Undocumented
Method __setstate__ Undocumented
Method batch_eval Evaluates `exprs`, returning a list of tuples (one tuple of `n` solutions for expression).
Method eval Evaluates expression `e`, returning a tuple of `n` solutions.
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 merge Undocumented
Method min Evaluates `e`, returning its min possible value.
Method satisfiable Checks if stored constraints conjunction is satisfiable.
Method solution Checks if `v` is a possible solution to `e`.
Method _blank_copy Undocumented
Method _copy Undocumented
Instance Variable _solver_backend Undocumented

Inherited from ConstrainedFrontend:

Method add Adds constraint(s) to constraints list.
Method check_satisfiability Checks the satisfiability of stored constraints conjunction.
Method combine Undocumented
Method downsize Undocumented
Method finalize Undocumented
Method independent_constraints Undocumented
Method simplify Simplifies the stored constraints conjunction.
Method split Undocumented
Instance Variable constraints Undocumented
Instance Variable variables 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, solver_backend, **kwargs): (source)
overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.__init__
overridden in claripy.solvers.SolverConcrete, claripy.solvers.SolverVSA

Undocumented

def __setstate__(self, s): (source)
overrides claripy.frontends.constrained_frontend.ConstrainedFrontend.__setstate__

Undocumented

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 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 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

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 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 _blank_copy(self, c): (source)
overrides claripy.frontends.constrained_frontend.ConstrainedFrontend._blank_copy

Undocumented

def _copy(self, c): (source)
overrides claripy.frontends.constrained_frontend.ConstrainedFrontend._copy

Undocumented

_solver_backend = (source)

Undocumented