pyState¶

Subpackages¶

pyState.functions package

pyState.Assign¶

pySym.pyState.Assign.handle(state, element)[source]¶

Attempt to handle the Python Assign element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.Assign) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to Assign. It is not meant to be called manually via a user.

Example

Example of ast.Assign is: x = 1

pyState.AugAssign¶

pySym.pyState.AugAssign.handle(state, element)[source]¶

Attempt to handle the Python AugAssign element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.AugAssign) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to AugAssign. It is not meant to be called manually via a user.

Example

Example of ast.Assign is: x += 1

pyState.BinOp¶

pySym.pyState.BinOp.handle(state, element, ctx=None)[source]¶

Attempt to handle the Python BinOp element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.BinOp) – element from source to be handled ctx (int, optional) – context to resolve BinOp in if not current
Returns:	list contains pyObjectManager variables (Int/Real/etc)
Return type:	list

This function handles calls to BinOp. It is not meant to be called manually via a user.

Example

Example of ast.BinOp is: x + 1

pyState.BoolOp¶

pySym.pyState.BoolOp.handle(state, element)[source]¶

Attempt to handle the Python BoolOp element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.BoolOp) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to BoolOp. It is not meant to be called manually via a user.

Example

Example of ast.BoolOp is: x == 1 and y == 2

pyState.Break¶

pySym.pyState.Break.handle(state, element)[source]¶

Attempt to handle the Python Break element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.Break) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to Break. It is not meant to be called manually via a user. Under the hood, it simply pops off the call stack until a loop change is seen (i.e.: we’ve left the for loop)

Example

Example of ast.Break is: break

pyState.Call¶

pySym.pyState.Call.handle(state, element, retObj=None)[source]¶

Attempt to handle the Python Call element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.Call) – element from source to be handled retObj (pyState.ReturnObject, optional) – retObj is an optional input to specify a ReturnObject to be used ahead of time.
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to ast.Call. It is not meant to be called manually via a user. A call will cause a context switch, populate variables, and set other internals. Upon return, the state will be inside the function.

Example

Example of ast.Call is: test()

pyState.Compare¶

pySym.pyState.Compare.handle(state, element, ctx=None)[source]¶

Attempt to handle the Python Compare element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.Compare) – element from source to be handled ctx (int, optional) – ctx is an optional input to specify a context to be used when resolving this ast object
Returns:	list contains state objects either generated or discovered through handling this ast. – or – list contains True constraints derived from input ast element as z3 elements.
Return type:	list

This function handles calls to ast.Compare. It is not meant to be called manually via a user.

Example

Example of ast.Compare is: 1 < 2

pyState.Expr¶

pySym.pyState.Expr.handle(state, element)[source]¶

Attempt to handle the Python Expr element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.Expr) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to ast.Expr. It is not meant to be called manually via a user.

Example

Example of ast.Expr is: test() (Note no assignment for call. This makes it an expression)

pyState.For¶

pySym.pyState.For.handle(state, element)[source]¶

Attempt to handle the Python For element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.For) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to ast.For. It is not meant to be called manually via a user.

Example

Example of ast.For is: for x in [1,2,3]

pyState.FunctionDef¶

pySym.pyState.FunctionDef.handle(state, element)[source]¶

Attempt to handle the Python FunctionDef element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.FunctionDef) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to ast.FunctionDef. It is not meant to be called manually via a user. Under the hood, it registers this function with the state object so that when it’s referenced later it can be found.

Example

Example of ast.FunctionDef is: def test():

pyState.GeneratorExp¶

pySym.pyState.GeneratorExp.handle(state, element, ctx=None)[source]¶

Attempt to handle the Python GeneratorExp element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.GeneratorExp) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to ast.GeneratorExp. It is not meant to be called manually via a user. Under the hood, it converts the generator expression into a list comprehension and calls the handler for list comprehension.

Example

Example of ast.GeneratorExp is: x for x in [1,2,3] (note it’s not inside List Comprehension brackets)

pyState.If¶

pySym.pyState.If.handle(state, element)[source]¶

Attempt to handle the Python If element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.If) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to ast.If. It is not meant to be called manually via a user. Under the hood, it resolves the conitional arguments, splits it’s state, and takes both possibilities as the same time.

Example

Example of ast.If is: if x > 5:

pyState.ListComp¶

pySym.pyState.ListComp.handle(state, element, ctx=None)[source]¶

Attempt to handle the Python ListComp element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.ListComp) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to ast.ListComp. It is not meant to be called manually via a user. Under the hood, it re-writes the ast into an equivalent functional form, then calls that function symbolically.

Example

Example of ast.ListComp is: [x for x in range(10)]

pyState.Pass¶

pySym.pyState.Pass.handle(state, element)[source]¶

Attempt to handle the Python Pass element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.Pass) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to ast.Pass. It is not meant to be called manually via a user. Under the hood, it very simply pops off the current instruction and returns the updated state object as a list.

Example

Example of ast.Pass is: pass

pyState.Return¶

pySym.pyState.Return.handle(state, element)[source]¶

Attempt to handle the Python Return element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.Return) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to ast.Return. It is not meant to be called manually via a user. Under the hood, it resolves the return element, sets the ReturnObject, and updates the state.

Example

Example of ast.Return is: return x

pyState.Subscript¶

pySym.pyState.Subscript.handle(state, element, ctx=None)[source]¶

Attempt to handle the Python Subscript element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.Subscript) – element from source to be handled ctx (int , optional) – Context to resolve this Subscript in (default is current context)
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to ast.Subscript. It is not meant to be called manually via a user.

Example

Example of ast.Subscript is: x[5] = 2

pyState.UnaryOp¶

pySym.pyState.UnaryOp.handle(state, element, ctx=None)[source]¶

Attempt to handle the Python UnaryOp element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.UnaryOp) – element from source to be handled ctx (int , optional) – Context to resolve this UnaryOp in (default is current context)
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to ast.UnaryOp. It is not meant to be called manually via a user.

Example

Example of ast.UnaryOp is: not True

pyState.While¶

pySym.pyState.While.handle(state, element)[source]¶

Attempt to handle the Python While element

Parameters:	state (pyState.State) – pyState.State object to handle this element under element (ast.While) – element from source to be handled
Returns:	list contains state objects either generated or discovered through handling this ast.
Return type:	list

This function handles calls to ast.While. It is not meant to be called manually via a user.

Example

Example of ast.While is: while x < 10:

pyState.z3Helpers¶

A file to hold my helper items directly relating to z3

pySym.pyState.z3Helpers.Z3_MAX_STRING_LENGTH = 256¶

def varIsUsedInSolver(var,solver,ignore=None) – ” “” Determine if the given var (z3 object) is used in solver. Optionally ignore a list of constraints. ” “” logger.warn(“varIsUsedInSolver is deprecated. Use solver.var_in_solver instead”)

ignore = [] if ignore is None else ignore

# If it’s a solo constraint, make it a list if type(ignore) is not None and type(ignore) not in [list, tuple]:

ignore = [ignore]

# Sanity check assert isZ3Object(var), “Expected var to be z3 object, got type {} instead”.format(type(var)) assert isinstance(solver,z3.Solver), “Solver must be type z3.Solver, got type {}”.format(type(z3.Solver))

# Remove any ignored assertions assertions = [ass for ass in solver.assertions() if ass not in ignore]

for ass in assertions:

if var.get_id() in [x.get_id() for x in pyState.get_all(ass)]:: return True

return False

pySym.pyState.z3Helpers.bvadd_safe(x, y, signed=False)[source]¶

BitVector addition overflow/underflow checks

Parameters:	x,y (z3.BitVecRef or z3.BitVecNumRef) – These variables are the two BitVecs that will be added together. signed (bool, optional) – Should this addition be treated as signed?
Returns:	tuple of z3 solver constraints to detect an overflow or underflow
Return type:	tuple

This function wraps Z3 C API functions to allow for a python interpretation of overflow and underflow checks. The returned tuple does not perform the addition, rather it is constraints that will perform the checks for overflow and underflow.

Example

If you want to verify the addition of x and y will not overflow/underflow:

In [1]: import z3

In [2]: from pySym import pyState.z3Helpers

In [3]: s = z3.Solver()

In [4]: x,y,z = z3.BitVecs('x y z',32)

In [5]: s.add(pyState.z3Helpers.bvadd_safe(x,y))

In [6]: s.add(x + y == z)

In [7]: s
Out[7]:
[Extract(32, 32, ZeroExt(1, x) + ZeroExt(1, y)) == 0,
 Implies(And(x < 0, y < 0), x + y < 0),
 x + y == z]

In [8]: s.check()
Out[8]: sat

pySym.pyState.z3Helpers.bvdiv_safe(x, y, signed=False)[source]¶

BitVector division overflow check

Parameters:	x,y (z3.BitVecRef or z3.BitVecNumRef) – These variables are the two BitVecs that will be divided signed (bool, optional) – Should this division be treated as signed?
Returns:	tuple of z3 solver constraints to detect an overflow
Return type:	tuple

This function wraps Z3 C API functions to allow for a python interpretation of overflow checks. The returned tuple does not perform the division, rather it is constraints that will perform the checks for overflow.

Example

If you want to verify the division of x and y will not overflow:

In [1]: import z3

In [2]: from pySym import pyState.z3Helpers

In [3]: s = z3.Solver()

In [4]: x,y,z = z3.BitVecs('x y z',32)

In [5]: s.add(pyState.z3Helpers.bvdiv_safe(x,y))

In [6]: s.add(x / y == z)

In [7]: s
Out[7]: [Not(And(x == 1 << 31, y == 4294967295)), x/y == z]

In [8]: s.check()
Out[8]: sat

pySym.pyState.z3Helpers.bvmul_safe(x, y, signed=False)[source]¶

BitVector multiplication overflow/underflow checks

Parameters:	x,y (z3.BitVecRef or z3.BitVecNumRef) – These variables are the two BitVecs that will be multiplied together. signed (bool, optional) – Should this multiplication be treated as signed?
Returns:	tuple of z3 solver constraints to detect an overflow or underflow
Return type:	tuple

This function wraps Z3 C API functions to allow for a python interpretation of overflow and underflow checks. The returned tuple does not perform the multiplication, rather it is constraints that will perform the checks for overflow and underflow.

Example

If you want to verify the multiplication of x and y will not overflow/underflow:

In [1]: import z3

In [2]: from pySym import pyState.z3Helpers

In [3]: s = z3.Solver()

In [4]: x,y,z = z3.BitVecs('x y z',32)

In [5]: s.add(pyState.z3Helpers.bvmul_safe(x,y))

In [6]: s.add(x * y == z)

In [7]: s
Out[7]: [bvumul_noovfl(x, y), bvsmul_noudfl(x, y), x*y == z]

In [8]: s.check()
Out[8]: sat

pySym.pyState.z3Helpers.bvsub_safe(x, y, signed=False)[source]¶

BitVector subtraction overflow/underflow checks

Parameters:	x,y (z3.BitVecRef or z3.BitVecNumRef) – These variables are the two BitVecs that will be subtracted. signed (bool, optional) – Should this subtraction be treated as signed?
Returns:	tuple of z3 solver constraints to detect an overflow or underflow
Return type:	tuple

This function wraps Z3 C API functions to allow for a python interpretation of overflow and underflow checks. The returned tuple does not perform the subtraction, rather it is constraints that will perform the checks for overflow and underflow.

Example

If you want to verify the subtraction of x and y will not overflow/underflow:

In [1]: import z3

In [2]: from pySym import pyState.z3Helpers

In [3]: s = z3.Solver()

In [4]: x,y,z = z3.BitVecs('x y z',32)

In [5]: s.add(pyState.z3Helpers.bvsub_safe(x,y))

In [6]: s.add(x - y == z)

In [7]: s
Out[7]:
[If(y == 1 << 31,
    x < 0,
    Implies(And(0 < x, 0 < -y), 0 < x + -y)),
 ULE(y, x),
 x - y == z]

In [8]: s.check()
Out[8]: sat

pySym.pyState.z3Helpers.isInt(x)[source]¶

Wraps Z3 C API to perform isInt check on Real object x

Parameters:	x (z3.ArithRef or z3.RatNumRef) – Real variable from calls like z3.Real(‘x’)
Returns:	z3.BoolRef asserting type x is Int (i.e.: ends in .0)
Return type:	z3.BoolRef

This function wraps Z3 C API functions to allow for a python interpretation of isInt. The returned value is a boolean that the input Real type x is an integer (i.e.: ends in .0). This call is the C API that performs the check at solve time, rather than entry time.

Example

If you want to verify that Real type x is an Int:

In [1]: import z3

In [2]: from pySym import pyState.z3Helpers

In [3]: s = z3.Solver()

In [4]: x = z3.Real('x')

In [5]: s.add(pyState.z3Helpers.isInt(x))

In [6]: s.add(x == 5.0)

In [7]: s
Out[7]: [IsInt(x), x == 5]

In [8]: s.check()
Out[8]: sat

pySym.pyState.z3Helpers.isZ3Object(obj)[source]¶

Determine if the object given is a z3 type object

Parameters:	x (any) – Object can be any type
Returns:	True if object is known z3 type, False otherwise
Return type:	bool

This function is helpful if you want to verify that a given input object is a z3 type object. Under the cover, it runs the type operator against the object and compares it to known z3 types.

Example

If you want to verify x is a valid z3 object:

In [1]: import z3

In [2]: from pySym import pyState.z3Helpers

In [3]: x = z3.Real('x')

In [4]: assert pyState.z3Helpers.isZ3Object(x)

pySym.pyState.z3Helpers.z3_bv_to_int(x)[source]¶

BitVector to Integer Z3 conversion

Parameters:	x (z3.BitVecRef or z3.BitVecNumRef) – BitVector variable to be converted to Int
Returns:	z3.ArithRef is an expression that will convert the BitVec into Integer inside Z3 rather than before insertion into the solver.
Return type:	z3.ArithRef

This function wraps Z3 C API functions to allow for a python interpretation of BitVec to Int conversions. The returned object is an expression that Z3 will evaluate as an Int rather than BitVec during solving.

Example

If you want to convert a BitVec into an Int:

In [1]: import z3

In [2]: from pySym import pyState.z3Helpers

In [3]: s = z3.Solver()

In [4]: x = z3.BitVec('x',32)

In [5]: y = z3.Int('y')

In [6]: x = pyState.z3Helpers.z3_bv_to_int(x)

In [7]: s.add(x == y)

In [8]: s
Out[8]: [BV2Int(x) == y]

In [9]: s.check()
Out[9]: sat

pySym.pyState.z3Helpers.z3_int_to_bv(x, size=64)[source]¶

Integer to BitVector Z3 conversion

Parameters:	x (z3.ArithRef or z3.IntNumRef) – Int variable to be converted to BitVec size (int, optional) – BitVec bit size. If not specified, defaults to pyState.z3Helpers.Z3_DEFAULT_BITVEC_SIZE
Returns:	This is the BitVec reference for the associated Int
Return type:	z3.BitVecRef

This function wraps Z3 C API functions to allow for a python interpretation of Int to BitVec conversions. The returned object is an expression that Z3 will evaluate as an BitVec rather than Int during solving.

Example

If you want to convert an Int int into a BitVec:

In [1]: import z3

In [2]: from pySym import pyState.z3Helpers

In [3]: s = z3.Solver()

In [4]: x = z3.BitVec('x',8)

In [5]: y = z3.Int('y')

In [6]: y = pyState.z3Helpers.z3_int_to_bv(y,8)

In [7]: s.add(x == y)

In [8]: s
Out[8]: [x == int2bv(y)]

In [9]: s.check()
Out[9]: sat

pySym.pyState.z3Helpers.z3_matchLeftAndRight(left, right, op)[source]¶

Appropriately change the two variables so that they can be used in an expression

Parameters:	left,right (pyObjectManager.Int.Int or pyObjectManager.Real.Real or pyObjectManager.BitVec.BitVec or pyObjectManager.Char.Char) – Objects to be matched op (ast.*) – Operation that will be performed
Returns:	(z3ObjectLeft,z3ObjectRight) tuple of z3 objects that can be used in an expression
Return type:	tuple

The purpose of this function is to match two pyObjectManager.* variables to a given ast operation element. Z3 needs to have matched types, and this call will not only match the objects, but also attempt to concretize input wherever possible.

Example

If you want to auto-match BitVector sizes:

In [1]: import z3, pyState.z3Helpers, ast

In [2]: from pySym.pyObjectManager.BitVec import BitVec

In [3]: from pySym.pyState import State

In [4]: state = State()

In [5]: x = BitVec("x",0,16,state=state)

In [6]: y = BitVec("y",0,32,state=state)

In [7]: l,r = pyState.z3Helpers.z3_matchLeftAndRight(x,y,ast.Add())

In [8]: s = z3.Solver()

In [9]: s.add(l + r == 12)

In [10]: s
Out[10]: [SignExt(16, 0x@0) + 0y@0 == 12]

In [11]: s.check()
Out[11]: sat

Module contents¶

class pySym.pyState.ReturnObject(retID, state=None)[source]¶

Bases: object

copy()[source]¶

Copies ReturnObject into an identical instance

Returns:	ReturnObject with the same ID and State as the previous one
Return type:	pySym.pyState.ReturnObject

retID¶

state¶

class pySym.pyState.State(path=None, solver=None, ctx=None, functions=None, simFunctions=None, retVar=None, callStack=None, backtrace=None, retID=None, loop=None, maxRetID=None, maxCtx=None, objectManager=None, vars_in_solver=None, project=None)[source]¶

Bases: object

Defines the state of execution at any given point.

Call(call, func=None, retObj=None, ctx=None)[source]¶

Input:: call = ast.Call object (optional) func = resolved function for Call (i.e.: state.resolveCall(call)). This is here to remove duplicate calls to resolveCall from resolveObject (optional) ctx = Context to execute under. If left blank, new Context will be created.
Action:: Modify state in accordance w/ call
Returns:: ReturnObject the describes this functions return var

Return(retElement)[source]¶

Input:: retElement = ast.Return element
Action:: Set return variable appropriately and remove the rest of the instructions in the queue
Returns:: Nothing for now

addConstraint(*constraints)[source]¶

Input:: constraints = Any number of z3 expressions to use as a constraint
Action:: Add constraint given
Returns:: Nothing

any_char(var, ctx=None)[source]¶

Input:: var == variable name. i.e.: “x” –or– ObjectManager object (i.e.: Char) (optional) ctx = context if not current one
Action:: Resolve a possible value for this variable
Return:: Discovered variable or None if none found

any_int(var, ctx=None, extra_constraints=None)[source]¶

Input:: var == variable name. i.e.: “x” –or– ObjectManager object (i.e.: Int) (optional) ctx = context if not current one (optional) extra_constraints = tuple of extra constraints to temporarily place on the solve.
Action:: Resolve possible value for this variable
Return:: Discovered variable or None if none found

any_list(var, ctx=None)[source]¶

Input:: var == variable name. i.e.: “x” (optional) ctx = context if not current one
Action:: Resolve possible value for this variable (list)
Return:: Discovered variable or None if none found

any_n_int(var, n, ctx=None)[source]¶

Input:: var = variable name. i.e.: “x” –or– ObjectManager object (i.e.: Int) n = number of viable solutions to find (i.e.: 5) (optional) ctx = context if not current one
Action:: Resolve n possible values for this variable
Return:: Discovered n values or [] if none found

any_n_real(var, n, ctx=None)[source]¶

Input:: var = variable name. i.e.: “x” –or– ObjectManager object (i.e.: Int) n = number of viable solutions to find (i.e.: 5) (optional) ctx = context if not current one
Action:: Resolve n possible values for this variable
Return:: Discovered possible values or [] if none found

any_real(var, ctx=None)[source]¶

Input:: var == variable name. i.e.: “x” –or– ObjectManager Object (i.e.: Int) (optional) ctx = context if not current one
Action:: Resolve possible value for this variable
Return:: Discovered variable or None if none found Note: this function will cast an Int to a Real implicitly if found

any_str(var, ctx=None)[source]¶

Input:: var == variable name. i.e.: “x” –or– ObjectManager object (i.e.: String) (optional) ctx = context if not current one
Action:: Resolve a possible value for this variable
Return:: Discovered variable or None if none found

backtrace¶

callStack¶

copy()[source]¶: Return a copy of the current state

copyCallStack()[source]¶: Make a copy of the call stack, avoiding deepcopy Returns a copy of the current call stack

ctx¶

functions¶

getVar(varName, ctx=None, varType=None, kwargs=None, softFail=None)[source]¶: Convinence function that adds current ctx to getVar request

isSat(extra_constraints=None)[source]¶

Input:: extra_constraints: Optional list of extra constraints to temporarily add before checking for sat.
Action:: Checks if the current state is satisfiable Note, it uses the local and global vars to create the solver on the fly
Returns:: Boolean True or False

lineno()[source]¶: Returns current line number. If returning from a call, returns the return line number Returns None if the program is done

loop¶

maxCtx¶

maxRetID¶

objectManager¶

path¶

popCallStack()[source]¶

Input:: Nothing
Action:: Pops from the call stack to the run stack. Adds call to completed state
Returns:: True if pop succeeded, False if there was nothing left to pop

popConstraint()[source]¶: Pop last added constraint This doesn’t seem to work…

printVars()[source]¶

Input:: Nothing
Action:: Resolves current constraints and prints viable variables
Returns:: Nothing

pushCallStack(path=None, ctx=None, retID=None, loop=None)[source]¶: Save the call stack with given variables Defaults to current variables if none given

recursiveCopy(var, ctx=None, varName=None)[source]¶: Create a recursive copy of the given ObjectManager variable. This includes creating the relevant z3 constraints (optional) ctx = Context to copy in. Defaults to ctx 1 (RETURN_CONTEXT). (optional) varName = Specify what to name this variable Returns the copy

registerFunction(func, base=None, simFunction=None)[source]¶

Input:: func = ast func definition (optional) base = base path to import as (i.e.: “telnetlib” if importing “telnetlib.Telnet”) (optional) simFunction = Boolean if this should be treated as a simFunction and therefore not handled symbolically. Defaults to False.
Action:: Register’s this function as being known to this state
Returns:: Nothing

remove_constraints(constraints)[source]¶

Removes the given z3 constraints.

Args:: constraints (list): List of z3 constraints to remove from the solver.
Returns:: int: Returns how many constraints were actually removed.

resolveCall(call, ctx=None)[source]¶

Input:: call = ast.Call object (optional) ctx = Context to resolve under
Action:: Determine correct ast.func object
Returns:: ast.func block

resolveObject(obj, parent=None, ctx=None, varType=None, kwargs=None)[source]¶

Input:

obj = Some ast object (i.e.: ast.Name, ast.Num, etc): special object “PYSYM_TYPE_RETVAL” (int) will resolve the last return value

(optional) parent = parent node of obj. This is needed for resolving calls (optional) ctx = Context other than current to resolve in (optional) varType = Type of the var to resolve. Needed if resolving a var that doesn’t exist yet (optional) kwargs = kwargs for the var, needed if resolving a var that doesn’t exist yet

Action:

Resolve object into something that can be used in a constraint

Return:

Resolved object: ast.Num == int (i.e.: 6) ast.Name == pyObjectManager object (Int, Real, BitVec, etc) ast.BinOp == z3 expression of BinOp (i.e.: x + y)

retID¶

retVar¶

setVar(varName, var, ctx=None)[source]¶: Convinence function that adds current ctx to setVar request

simFunctions¶

solver¶

step()[source]¶: Move the current path forward by one step Note, this actually makes a copy/s and returns them. The initial path isn’t modified. Returns: A list of paths or empty list if the path is done

var_in_solver(var, ignore=None)[source]¶: Checks if the variable given is in the z3 solver.

pySym.pyState.duplicateSort(obj)[source]¶

Input:

obj = z3 object to duplicate kind (i.e.: z3.IntSort()) –or–: pyObjectManager type object (i.e.: Int)

Action:

Figure out details of the object and make duplicate sort

Return:

(class, kwargs) Duplicate pyObjectManager class object for this type (i.e.: Int)

pySym.pyState.get_all(f, rs=[])[source]¶

>>> x,y = Ints('x y')
>>> a,b = Bools('a b')
>>> get_all(Implies(And(x+y==0,x*2==10),Or(a,Implies(a,b==False))))
[x, y, a, b]

pySym.pyState.hasRealComponent(expr)[source]¶

Checks for Real component to a z3 expression

Parameters:	expr (z3 expression object) –
Returns:	True if it has real componenet, False otherwise
Return type:	bool

Checks if expression contains a real/non-int value or variable. This is genereally used in determining proper variable type to create. Z3 will cast Int to Real if you don’t select the right type, which add extra complexity to the solving.

Example

Confirm that a Z3 expression has a Real component:

In [1]: import z3

In [2]: from pySym import pyState

In [3]: r = z3.Real('r')

In [4]: i = z3.Int('i')

In [5]: pyState.hasRealComponent(r + i == 5)
Out[5]: True

pySym.pyState.replaceObjectWithObject(haystack, fromObj, toObj, parent=None)[source]¶

Generic search routine to replace an arbitrary object with another

Parameters:	haystack (any) – Where to search fromObj (any) – What to replace toObj (any) – What to replace with parent (any, optional) – (depreciated) What the parent object is. This option will be removed.
Returns:	True/False if the object was successfully replaced.
Return type:	bool

Find instance of fromObj in haystack and replace with toObj. This is used to ensure we know which function return is ours. Also now matches against lineno, col_offset and type. This will likely fail on polymorphic python code

Example

Replace the ast.Compare object with a Return object:

In [1]: import ast

In [2]: from pySym import pyState

In [3]: ret = pySym.pyState.ReturnObject(5)

In [4]: s = ast.parse("if 5 > 2:\n\tpass").body[0]

In [5]: print(s.test)
<_ast.Compare object at 0x7f563acb1b70>

In [6]: assert pyState.replaceObjectWithObject(s,s.test,ret)

In [7]: print(s.test)
<pySym.pyState.ReturnObject object at 0x7f563b4c1048>