dwarfcore.plugins.under_constrained_symex.errors module

class dwarfcore.plugins.under_constrained_symex.errors.AccessKind(value)

Bases: str, enum.Enum

An enumeration.

READ = 'read'
WRITE = 'write'
class dwarfcore.plugins.under_constrained_symex.errors.ErrorManager

Bases: object

A class used to check and handle for memory access errors during underconstrained symbolic execution.

check_oob_access(access: dwarfcore.plugins.under_constrained_symex.errors.AccessKind, obj, offset: Union[manticore.core.smtlib.expression.Expression, int], size: int, memory, pc: int, fix_oob: bool = False)

Check whether a memory access can exceed the bounds of a memory object. If the offset can be out of bounds, create an error case.

Parameters

  • access – type of memory access (read or write)

  • obj – memory object to access

  • offset – offset at which to read/write in ‘obj’

  • size – number of bytes to read/write

  • memory – the current UC memory

  • pc – the address of the instruction reading memory

  • fix_error – if set to True and if offset can be out of bounds, try to add a constraint to the constraint set such that to enforce ‘offset’ to be in within the bounds of ‘obj’

  • access (dwarfcore.plugins.under_constrained_symex.errors.AccessKind) –

  • offset (Union[manticore.core.smtlib.expression.Expression, int]) –

  • size (int) –

  • pc (int) –

  • fix_oob (bool) –

record_error(error)
class dwarfcore.plugins.under_constrained_symex.errors.ExecError

Bases: object

A base class representing an error during execution.

property is_oob: bool
class dwarfcore.plugins.under_constrained_symex.errors.OOBError(pc: int, cond: manticore.core.smtlib.expression.Expression, constraints: manticore.core.smtlib.constraints.ConstraintSet)

Bases: dwarfcore.plugins.under_constrained_symex.errors.ExecError

A base class representing an out of bounds memory access error.

Parameters

  • pc (int) –

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

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

property is_oob: bool
class dwarfcore.plugins.under_constrained_symex.errors.OOBReadError(pc: int, cond: manticore.core.smtlib.expression.Expression, constraints: manticore.core.smtlib.constraints.ConstraintSet)

Bases: dwarfcore.plugins.under_constrained_symex.errors.OOBError

Parameters

  • pc (int) –

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

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

class dwarfcore.plugins.under_constrained_symex.errors.OOBWriteError(pc: int, cond: manticore.core.smtlib.expression.Expression, constraints: manticore.core.smtlib.constraints.ConstraintSet)

Bases: dwarfcore.plugins.under_constrained_symex.errors.OOBError

Parameters

  • pc (int) –

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

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

class dwarfcore.plugins.under_constrained_symex.errors.UnderconstrainedOOB(manticore: manticore.native.manticore.Manticore)

Bases: manticore.core.plugin.Plugin

Detector for under-constrained OOB errors.

Parameters

manticore (manticore.native.manticore.Manticore) –

MCORE_TESTCASE_LIST: Final[str] = 'UnderconstrainedOOBDetector_test_cases'
manticore
classmethod new_testcase_uid()
record_testcases(state: manticore.native.state.State) → None
Parameters

state (manticore.native.state.State) –

Return type

None

property results: List[mate_common.models.integration.UnderconstrainedTestCase]

Any test case results found during execution.

will_terminate_state_callback(state, _reason)