module greed.solver.shortcuts

This module provides shortcuts to the solver API to be used in greed scripts.

function ctx_or_symbolic

ctx_or_symbolic(v, ctx, xid, nbits=256)

Given a variable name, if the var is in the context, return it, otherwise create a new symbolic variable.

Args:

  • v: The variable name
  • ctx: The context
  • xid: The transaction id
  • nbits: The number of bits of the symbolic variable

function concretize

concretize(state, val, force=False)

Given a value, if it is concrete, return it, otherwise if the symbolic variable has only one possible solution, return it. If the symbolic variable has multiple possible solutions and force is True, add a constraint and return one of the possible solutions.

Args:

  • state: The state
  • val: The value
  • force: Whether to force the concretization

Returns: The concrete value or None

function BVSort

BVSort(width)

function BVV

BVV(value, width)

function BVS

BVS(symbol, width)

function Array

Array(symbol, index_sort, value_sort)

function If

If(cond, value_if_true, value_if_false)

function Equal

Equal(a, b)

function NotEqual

NotEqual(a, b)

function Or

Or(*terms)

function And

And(*terms)

function Not

Not(a)

function bv_unsigned_value

bv_unsigned_value(bv)

function get_bv_by_name

get_bv_by_name(symbol)

function is_concrete

is_concrete(bv)

function BV_Extract

BV_Extract(start, end, bv)

function BV_Concat

BV_Concat(terms)

function BV_Add

BV_Add(a, b)

function BV_Sub

BV_Sub(a, b)

function BV_Mul

BV_Mul(a, b)

function BV_UDiv

BV_UDiv(a, b)

function BV_SDiv

BV_SDiv(a, b)

function BV_SMod

BV_SMod(a, b)

function BV_SRem

BV_SRem(a, b)

function BV_URem

BV_URem(a, b)

function BV_Sign_Extend

BV_Sign_Extend(a, b)

function BV_Zero_Extend

BV_Zero_Extend(a, b)

function BV_UGE

BV_UGE(a, b)

function BV_ULE

BV_ULE(a, b)

function BV_UGT

BV_UGT(a, b)

function BV_ULT

BV_ULT(a, b)

function BV_SGE

BV_SGE(a, b)

function BV_SLE

BV_SLE(a, b)

function BV_SGT

BV_SGT(a, b)

function BV_SLT

BV_SLT(a, b)

function BV_And

BV_And(a, b)

function BV_Or

BV_Or(a, b)

function BV_Xor

BV_Xor(a, b)

function BV_Not

BV_Not(a)

function BV_Shl

BV_Shl(a, b)

function BV_Shr

BV_Shr(a, b)

function BV_Sar

BV_Sar(a, b)

function Array_Store

Array_Store(arr, index, elem)

function Array_Select

Array_Select(arr, index)

This file was automatically generated via lazydocs.