dwarfcore.plugins.under_constrained_symex.smt module

class dwarfcore.plugins.under_constrained_symex.smt.SmtNameTranslator

Bases: object

Small helper class that transforms arbitrary variable names into SMTlib v2 compliant names.

TO_SMT = {'$CAPACITY': '_____CAPACITY_OF_____', '$LEN': '_____LENGTH_OF_____', '$SIZE': '_____SIZE_OF_____', '(': '______openbracket______', ')': '______closebracket______', '[': '______at_____', ']': '______ta_____'}

static make_name_smt_compliant(name: str) → str

Parameters

name (str) –

Return type

str

static revert_to_original_name(name: str) → str

Parameters

name (str) –

Return type

str

class dwarfcore.plugins.under_constrained_symex.smt.UCPrettyPrinter(**kwargs)

Bases: manticore.core.smtlib.visitors.Visitor

op_map: Dict[str, str] = {'BitVecAdd': '+', 'BitVecAnd': '&', 'BitVecArithmeticShiftLeft': '<<', 'BitVecArithmeticShiftRight': 'SAR', 'BitVecConcat': 'CONCAT', 'BitVecDiv': '/', 'BitVecITE': 'ITE', 'BitVecMod': '%', 'BitVecMul': '*', 'BitVecNeg': '-', 'BitVecNot': '~', 'BitVecOr': '|', 'BitVecRem': 'REM', 'BitVecShiftLeft': '<<', 'BitVecShiftRight': '>>', 'BitVecSignExtend': 'SEXT', 'BitVecSub': '-', 'BitVecUnsignedDiv': 'UDIV', 'BitVecUnsignedRem': 'UREM', 'BitVecXor': '^', 'BitVecZeroExtend': 'ZEXT', 'BoolAnd': '&&', 'BoolEqual': '==', 'BoolNot': '!', 'BoolOr': '||', 'BoolXor': 'BoolXOR', 'GreaterOrEqual': '>=', 'GreaterThan': '>', 'LessOrEqual': '<=', 'LessThan': '<', 'UnsignedGreaterOrEqual': 'UGE', 'UnsignedGreaterThan': 'UGT', 'UnsignedLessOrEqual': 'ULE', 'UnsignedLessThan': 'ULT'}

property result: str

visit(expression: manticore.core.smtlib.expression.Expression) → str

Overload Visitor.visit because:

• We need a pre-order traversal

• We use a recursion as it makes it easier to keep track of the indentation

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_ArrayVariable(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecArithmeticShiftRight(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecConcat(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecConstant(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecExtract(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecITE(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecNeg(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecNot(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecOperation(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecRem(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecSignExtend(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecUnsignedDiv(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecUnsignedRem(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecVariable(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BitVecZeroExtend(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BoolConstant(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BoolNot(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BoolOperation(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BoolVariable(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_BoolXor(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_UnsignedGreaterOrEqual(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_UnsignedGreaterThan(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_UnsignedLessOrEqual(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

visit_UnsignedLessThan(expression: manticore.core.smtlib.expression.Expression) → str

Parameters

expression (manticore.core.smtlib.expression.Expression) –

Return type

str

dwarfcore.plugins.under_constrained_symex.smt.uc_pretty_print(expression: manticore.core.smtlib.expression.Expression)

Parameters

expression (manticore.core.smtlib.expression.Expression) –