dwarfcore.plugins.under_constrained_symex.user_constraints module

class dwarfcore.plugins.under_constrained_symex.user_constraints.GetAllVariables

Bases: lark.visitors.Visitor

Visitor that returns the names of all symbolic variables present in a parsed constraint tree.

atom(tree)
class dwarfcore.plugins.under_constrained_symex.user_constraints.InstanciateClassConstraintForType(obj_type: mate_query.cpg.models.node.dwarf.DWARFType)

Bases: lark.visitors.Transformer

See lark_instanciate_class_constraint_for_type() for documentation.

typesize(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

class dwarfcore.plugins.under_constrained_symex.user_constraints.MakeVariablesSmtCompliant(visit_tokens: bool = True)

Bases: lark.visitors.Transformer

Transformer that transforms symbolic variable names to make them SMT compliant.

It replaces characters not supported by smtlib such as “[“, “]”, …

CAPACITY_METAVAR(token)
LEN_METAVAR(token)
SIZE_METAVAR(token)
VAR(token)
class dwarfcore.plugins.under_constrained_symex.user_constraints.Metavar(value)

Bases: enum.Enum

Types of meta variables for objects.

CAPACITY = 'CAPACITY'
LEN = 'LEN'
SIZE = 'SIZE'
class dwarfcore.plugins.under_constrained_symex.user_constraints.ParsedClassConstraint(original_constraint: mate_common.models.manticore.UserDefinedConstraint, tree: Union[lark.tree.Tree, NoneType], class_spec: str, used_at_least_once: bool = False)

Bases: dwarfcore.plugins.under_constrained_symex.user_constraints.ParsedConstraint

Parameters
Return type

None

class_spec: str
used_at_least_once: bool = False
class dwarfcore.plugins.under_constrained_symex.user_constraints.ParsedConstraint(original_constraint: mate_common.models.manticore.UserDefinedConstraint, tree: Union[lark.tree.Tree, NoneType])

Bases: object

Parameters
Return type

None

original_constraint: mate_common.models.manticore.UserDefinedConstraint
tree: Optional[lark.tree.Tree]
class dwarfcore.plugins.under_constrained_symex.user_constraints.ParsedPointsWithinConstraint(original_constraint: mate_common.models.manticore.UserDefinedConstraint, tree: Union[lark.tree.Tree, NoneType], points_within: Tuple[str, str])

Bases: dwarfcore.plugins.under_constrained_symex.user_constraints.ParsedConstraint

Parameters
Return type

None

points_within: Tuple[str, str]
class dwarfcore.plugins.under_constrained_symex.user_constraints.ReplacePatternInVariables(old: str, new: str)

Bases: lark.visitors.Transformer

Transformer replaces a string by another in all variable names.

CAPACITY_METAVAR(token: lark.lexer.Token)
Parameters

token (lark.lexer.Token) –

LEN_METAVAR(token: lark.lexer.Token)
Parameters

token (lark.lexer.Token) –

SIZE_METAVAR(token: lark.lexer.Token)
Parameters

token (lark.lexer.Token) –

VAR(token: lark.lexer.Token)
Parameters

token (lark.lexer.Token) –

class dwarfcore.plugins.under_constrained_symex.user_constraints.SplitGenericClassConstraint(visit_tokens: bool = True)

Bases: lark.visitors.Transformer

Transformer that splits a generic class constraint into the class specifier string and the actual parsed constraint.

CLASS_SPEC(token: lark.lexer.Token)
Parameters

token (lark.lexer.Token) –

generic_class_constraint(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

class dwarfcore.plugins.under_constrained_symex.user_constraints.TranslateConstraint(constraints: manticore.core.smtlib.constraints.ConstraintSet)

Bases: lark.visitors.Transformer

Transformer that translates a parsed user constraint tree into an actual Expression object to be used by Manticore.

CAPACITY_METAVAR(token: lark.lexer.Token)
Parameters

token (lark.lexer.Token) –

LEN_METAVAR(token: lark.lexer.Token)
Parameters

token (lark.lexer.Token) –

NUMBER(token: lark.lexer.Token)
Parameters

token (lark.lexer.Token) –

OPERATOR_MAP = {'op_add': <built-in function add>, 'op_and': <built-in function and_>, 'op_concat': <function TranslateConstraint.<lambda>>, 'op_eq': <built-in function eq>, 'op_ge': <built-in function ge>, 'op_gt': <built-in function gt>, 'op_inv': <built-in function inv>, 'op_le': <built-in function le>, 'op_lt': <built-in function lt>, 'op_mod': <built-in function mod>, 'op_mul': <built-in function mul>, 'op_neg': <built-in function neg>, 'op_neq': <built-in function ne>, 'op_or': <built-in function or_>, 'op_sar': <function TranslateConstraint.<lambda>>, 'op_sdiv': <function TranslateConstraint.<lambda>>, 'op_shl': <built-in function lshift>, 'op_shr': <built-in function rshift>, 'op_sub': <built-in function sub>, 'op_uge': <function TranslateConstraint.<lambda>>, 'op_ugt': <function TranslateConstraint.<lambda>>, 'op_ule': <function TranslateConstraint.<lambda>>, 'op_ult': <function TranslateConstraint.<lambda>>, 'op_xor': <built-in function xor>}
SIZE_METAVAR(token: lark.lexer.Token)
Parameters

token (lark.lexer.Token) –

VAR(token: lark.lexer.Token)
Parameters

token (lark.lexer.Token) –

atom(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

binary_operation(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

constraint(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

constraint_disjunction(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

expr(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

extract_operation(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

funclike_comparison(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

funclike_operation(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

points_within_constraint(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

regular_comparison(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

unary_operation(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

class dwarfcore.plugins.under_constrained_symex.user_constraints.TranslatePointsWithinConstraint(visit_tokens: bool = True)

Bases: lark.visitors.Transformer

Transformer that translates a parsed $POINTS_WITHIN constraint tree into an tuple (ptr_pointing_within_ptr2, ptr2)

VAR(token: lark.lexer.Token)
Parameters

token (lark.lexer.Token) –

points_within_constraint(tokens: List[lark.lexer.Token])
Parameters

tokens (List[lark.lexer.Token]) –

class dwarfcore.plugins.under_constrained_symex.user_constraints.UserConstraintManager

Bases: object

Class that manages constraints supplied by the user.

Its intended usage is roughly: - Use add() to add user-defined constraints (which are just strings) - Use apply_constraints(<var>) to apply any pending parsed constraints that involves variable

<var>. The parsed constraint tree is then translated into a Manticore Expression object and added to the Manticore state

Example constraints:

a < 10000 ULE(a, b+1) arg1->x == arg2.y arg.array[5] > 6 $LEN(arg.array) < 100 a == 1 || b == 5 Extract(d, 16, 32)

CONSTRAINT_GRAMMAR = '\n            %import common.WS\n            %ignore WS\n\n            constraint: regular_comparison\n                | funclike_comparison\n                | "(" constraint ")"\n                | constraint_disjunction\n\n            constraint_disjunction: constraint "||" constraint\n\n            funclike_cmp_op: "ULE" -> op_ule\n                | "ULT" -> op_ult\n                | "UGT" -> op_ugt\n                | "UGE" -> op_uge\n\n            funclike_comparison: funclike_cmp_op "(" expr "," expr ")"\n            regular_comparison: expr cmp_op expr\n\n            expr: atom\n                | binary_operation\n                | unary_operation\n                | funclike_operation\n                | extract_operation\n                | "(" expr ")"\n                | special_operation\n\n            special_operation: "$TYPESIZE(" TEMPLATE_VAR ")" -> typesize\n\n            funclike_op: "CONCAT" -> op_concat\n                | "SDIV" -> op_sdiv\n                | "SAR" -> op_sar\n\n            funclike_operation: funclike_op "(" expr "," expr ")"\n\n            extract_operation: "EXTRACT" "(" expr "," NUMBER "," NUMBER ")"\n\n            binary_operation: expr binop expr\n\n            unary_operation: unop expr\n\n            atom: VAR | NUMBER | LEN_METAVAR | CAPACITY_METAVAR | SIZE_METAVAR\n\n            cmp_op: "==" -> op_eq\n                | "!=" -> op_neq\n                | "<" -> op_lt\n                | "<=" -> op_le\n                | ">" -> op_gt\n                | ">=" -> op_ge\n\n            binop: "+" -> op_add\n                | "-" -> op_sub\n                | "*" -> op_mul\n                | "&" -> op_and\n                | "|" -> op_or\n                | "^" -> op_xor\n                | ">>" -> op_shr\n                | "<<" -> op_shl\n                | "%" -> op_mod\n\n            unop: "-" -> op_neg\n                | "~" -> op_inv\n\n\n            %import common.LETTER\n            %import common.DIGIT\n            // We add $OBJ. for variables in generic class constraints\n            VAR: (("$OBJ.")? ("_"|LETTER) ("_"|"."|"->"|LETTER|DIGIT|IDX)*)\n                | "$OBJ"\n\n            LEN_METAVAR: "$LEN(" VAR ")"\n            CAPACITY_METAVAR: "$CAPACITY(" VAR ")"\n            SIZE_METAVAR: "$SIZE(" VAR ")"\n\n            TEMPLATE_VAR: "#" (DIGIT)+\n\n            IDX: "[" (DIGIT)+ "]"\n\n            %import common.SIGNED_INT\n            %import common.HEXDIGIT\n            NUMBER: SIGNED_INT | ("0x" (HEXDIGIT)+)\n\n            points_within_constraint: "$POINTS_WITHIN(" VAR "," VAR ")"\n\n            generic_class_constraint: CLASS_SPEC ":" (constraint|points_within_constraint)\n\n            CLASS_SPEC: ("_"|LETTER) (CLASS_SPEC_CHAR)*\n            CLASS_SPEC_CHAR: "::"|","|"_"|"<"|">"|"#"|LETTER|DIGIT|WS\n            '
add(constraint: mate_common.models.manticore.UserDefinedConstraint)

Add and parse a user-defined constraint.

  • The user is parsed according to the constraint grammar and stored as a ‘parsed constraint tree’ which is an intermediate representation on which we can easily run visitors

  • The symbolic variable names in the constraint that aren’t smtlibv2-compliant are transformed (unique predefined strings replace non-compliant characters)

  • The parsed constraint is added to an internal list of pending constraints that will later be applied to a Manticore state

If a constraint is invalid and can not be parsed, this method raises an ‘InputError’ exception

Parameters
Returns

None

apply_class_constraints(obj_name: str, obj_type: mate_query.cpg.models.node.dwarf.DWARFType)

Apply generic class constraints to an object, if applicable. This generates new constraints specific to that object, to be apply later by a call to apply_constraints()

Parameters

the dereference operator (‘a.’) or (‘a->’) :param _sphinx_paramlinks_dwarfcore.plugins.under_constrained_symex.user_constraints.UserConstraintManager.apply_class_constraints.obj_type: The DWARFType of the object

apply_constraints(constraints: manticore.core.smtlib.constraints.ConstraintSet, var: str)

Apply pending user defined constraints related to a given expression to a constraint set.

  • A parsed constraint is applied only if all the variables it contains are already defined in the ‘constraints’ constraint set (not only ‘var’)

  • A parsed constraint being applied is translated into a Manticore Expression and then added to the constraint set

  • Parsed constraints that are applied are removed from the list of pending parsed constraints

Parameters

  • constraints – The constraint set to which to add user defined constraints

  • var – The name of the variable to which user constraints must be related in order to

  • constraints (manticore.core.smtlib.constraints.ConstraintSet) –

  • var (str) –

be added to the constraint set :return None:

get_points_within_destination(var_name: str) → str
Parameters

var_name (str) –

Return type

str

get_unused_constraints() → List[str]

Return the list of user constraints that were not used during execution.

Return type

List[str]

is_generic_class_constraint(parsed)
is_points_within_constraint(parsed)
points_within_other_variable(var_name: str) → bool
Parameters

var_name (str) –

Return type

bool

variable_is_used(variable_name: str) → bool

Return true if ‘variable_name’ is used in at least one instanciated user constraint.

This ignores generic class constraints that haven’t been instanciated

Parameters

variable_name (str) –

Return type

bool

dwarfcore.plugins.under_constrained_symex.user_constraints.lark_get_all_variables(parsed_constraint: lark.tree.Tree) → Set[str]

Get all the names of symbolic variables present in a parsed constraint.

Parameters

parsed_constraint (lark.tree.Tree) –

Return type

Set[str]

dwarfcore.plugins.under_constrained_symex.user_constraints.lark_instanciate_class_constraint_for_type(parsed_constraint: lark.tree.Tree, obj_type: mate_query.cpg.models.node.dwarf.DWARFType) → lark.tree.Tree

Instanciate a generic class constraint for a given type. This method will replace special variables and special operators that are specific to generic class constraints, such as getting the size of template type arguments, etc.

Parameters

  • parsed_constraint – the intermediate parsed constraint to instanciate for the given type

  • obj_type – type for which to instanciate the class constraint. In most cases,

  • parsed_constraint (lark.tree.Tree) –

  • obj_type (mate_query.cpg.models.node.dwarf.DWARFType) –

Return type

lark.tree.Tree

‘obj_type’ will simply be the type specified by the generic constraint class specifier. But when dealing with templated types the same generic constraint can be instanciated for different combinations of template type arguments

dwarfcore.plugins.under_constrained_symex.user_constraints.lark_make_variables_smt_compliant(parsed_constraint: lark.tree.Tree) → lark.tree.Tree

Make all VAR tokens SMT compliant in a parsed constraint.

Parameters

parsed_constraint (lark.tree.Tree) –

Return type

lark.tree.Tree

dwarfcore.plugins.under_constrained_symex.user_constraints.lark_replace_pattern_in_variables(parsed_constraint: lark.tree.Tree, old: str, new: str) → lark.tree.Tree

Replace a given string in all variables in a parsed constraint.

Parameters

  • old – string to replace

  • new – string to substitute to ‘old’

  • parsed_constraint (lark.tree.Tree) –

  • old (str) –

  • new (str) –

Return type

lark.tree.Tree

dwarfcore.plugins.under_constrained_symex.user_constraints.lark_split_generic_class_constraint(parsed_constraint: lark.tree.Tree) → Tuple[str, lark.tree.Tree]

Split a generic class constraint into the class specifier string and the actual parsed constraint.

Parameters

parsed_constraint (lark.tree.Tree) –

Return type

Tuple[str, lark.tree.Tree]

dwarfcore.plugins.under_constrained_symex.user_constraints.lark_translate_constraint(parsed_constraint: lark.tree.Tree, constraints: manticore.core.smtlib.constraints.ConstraintSet) → manticore.core.smtlib.expression.Expression

Translate a parsed user constraint tree into an actual Expression object to be used by Manticore.

Parameters

  • parsed_constraint (lark.tree.Tree) –

  • constraints (manticore.core.smtlib.constraints.ConstraintSet) –

Return type

manticore.core.smtlib.expression.Expression

dwarfcore.plugins.under_constrained_symex.user_constraints.lark_translate_points_within_constraint(parsed_constraint: lark.tree.Tree) → manticore.core.smtlib.expression.Expression

Translate a parsed $POINTS_WITHIN constraint into an tuple (ptr_pointing_within_ptr2, ptr2)

Parameters

parsed_constraint (lark.tree.Tree) –

Return type

manticore.core.smtlib.expression.Expression