Web Assembly

ManticoreWASM

class manticore.wasm.manticore.ManticoreWASM(path_or_state, env={}, sup_env={}, workspace_url=None, policy='random', **kwargs)

Manticore class for interacting with WASM, analagous to ManticoreNative or ManticoreEVM.

collect_returns(n=1)

Iterates over the terminated states and collects the top n values from the stack. Generally only used for testing.

Parameters:n – Number of values to collect
Returns:A list of list of lists. > One list for each state
> One list for each n
> The output from solver.get_all_values
default_invoke(func_name: str = 'main')

Looks for a main function or start function and invokes it with symbolic arguments :param func_name: Optional name of function to look for

exported_functions = None

List of exported function names in the default module

finalize()

Finish a run and solve for test cases. Calls save_run_data

generate_testcase(state, message='test', name='test')
invoke(name='main', argv_generator=<function ManticoreWASM.<lambda>>)

Maps the “invoke” command over all the ready states :param name: The function to invoke :param argv_generator: A function that takes the current state and returns a list of arguments

run(timeout=None)

Begins the Manticore run

Parameters:timeout – number of seconds after which to kill execution
save_run_data()

WASM World

class manticore.platforms.wasm.WASMWorld(filename, name='self', **kwargs)

Manages global environment for a WASM state. Analagous to EVMWorld.

advice = None

Stores concretized information used to advise execution of the next instruction.

constraints = None

Initial set of constraints

exec_for_test(funcname, module=None)

Helper method that simulates the evaluation loop without creating workers or states, forking, or concretizing symbolic values. Only used for concrete unit testing.

Parameters:
  • funcname – The name of the function to test
  • module – The name of the module to test the function in (if not the default module)
Returns:

The top n items from the stack where n is the expected number of return values from the function
execute(current_state)

Tells the underlying ModuleInstance to execute a single WASM instruction. Raises TerminateState if there are no more instructions to execute, or if the instruction raises a Trap.

get_export(export_name, mod_name=None) → Union[manticore.wasm.structure.ProtoFuncInst, manticore.wasm.structure.TableInst, manticore.wasm.structure.MemInst, manticore.wasm.structure.GlobalInst, Callable, None]

Gets the export _instance_ for a given export & module name (basically just dereferences _get_export_addr into the store)

Parameters:
  • export_name – Name of the export to look for
  • mod_name – Name of the module the export lives in
Returns:

The export itself
get_module_imports(module, exec_start, stub_missing) → List[Union[manticore.wasm.structure.FuncAddr, manticore.wasm.structure.TableAddr, manticore.wasm.structure.MemAddr, manticore.wasm.structure.GlobalAddr]]

Builds the list of imports that should be passed to the given module upon instantiation

Parameters:
  • module – The module to find the imports for
  • exec_start – Whether to execute the start function of the module
  • stub_missing – Whether to replace missing imports with stubs (TODO: symbolicate)
Returns:

List of addresses for the imports within the store
import_module(module_name, exec_start, stub_missing)

Collect all of the imports for the given module and instantiate it

Parameters:
  • module_name – module to import
  • exec_start – whether to run the start functions automatically
  • stub_missing – whether to replace missing imports with stubs
Returns:

None
instance
Returns:the ModuleInstance for the first module registered
instantiate(env_import_dict: Dict[str, Union[manticore.wasm.structure.ProtoFuncInst, manticore.wasm.structure.TableInst, manticore.wasm.structure.MemInst, manticore.wasm.structure.GlobalInst, Callable]], supplemental_env: Dict[str, Dict[str, Union[manticore.wasm.structure.ProtoFuncInst, manticore.wasm.structure.TableInst, manticore.wasm.structure.MemInst, manticore.wasm.structure.GlobalInst, Callable]]] = {}, exec_start=False, stub_missing=True)

Prepares the underlying ModuleInstance for execution. Calls import_module under the hood, so this is probably the only import-y function you ever need to call externally.

TODO: stubbed imports should be symbolic

Parameters:
  • env_import_dict – Dict mapping strings to functions. Functions should accept the current ConstraintSet as the first argument.
  • supplemental_env – Maps strings w/ module names to environment dicts using the same format as env_import_dict
  • exec_start – Whether or not to automatically execute the start function, if it is set.
  • stub_missing – Whether or not to replace missing imports with empty stubs
Returns:

None
instantiated = None

Prevents users from calling run without instantiating the module

invoke(name='main', argv=[], module=None)

Sets up the WASMWorld to run the function specified by name when ManticoreWASM.run is called

Parameters:
  • name – Name of the function to invoke
  • argv – List of arguments to pass to the function. Should typically be I32, I64, F32, or F64
  • module – name of a module to call the function in (if not the default module)
Returns:

None
module
Returns:The first module registered
register_module(name, filename_or_alias)

Provide an explicit path to a WASM module so the importer will know where to find it

Parameters:
  • name – Module name to register the module under
  • filename_or_alias – Name of the .wasm file that module lives in
Returns:
set_env(exports: Dict[str, Union[manticore.wasm.structure.ProtoFuncInst, manticore.wasm.structure.TableInst, manticore.wasm.structure.MemInst, manticore.wasm.structure.GlobalInst, Callable]], mod_name='env')

Manually insert exports into the global environment

Parameters:
  • exports – Dict mapping names to functions/tables/globals/memories
  • mod_name – The name of the module these exports should fall under
stack = None

Stores numeric values, branch labels, and execution frames

store = None

Backing store for functions, memories, tables, and globals

manticore.platforms.wasm.stub(arity, _state, *args)

Default function used for hostfunc calls when a proper import wasn’t provided

Executor

class manticore.wasm.executor.Executor(*args, **kwargs)

Contains execution semantics for all WASM instructions that don’t involve control flow (and thus only need access to the store and the stack).

In lieu of annotating every single instruction with the relevant link to the docs, we direct you here: https://www.w3.org/TR/wasm-core-1/#a7-index-of-instructions

check_overflow(expression) → bool
check_zero_div(expression) → bool
current_memory(store, stack, imm: manticore.wasm.types.CurGrowMemImm)
dispatch(inst, store, stack)

Selects the correct semantics for the given instruction, and executes them

Parameters:
  • inst – the Instruction to execute
  • store – the current Store
  • stack – the current Stack
Returns:

the result of the semantic function, which is (probably) always None
drop(store, stack)
f32_abs(store, stack)
f32_add(store, stack)
f32_binary(store, stack, op, rettype: type = <class 'manticore.wasm.types.I32'>)
f32_ceil(store, stack)
f32_const(store, stack, imm: manticore.wasm.types.F32ConstImm)
f32_convert_s_i32(store, stack)
f32_convert_s_i64(store, stack)
f32_convert_u_i32(store, stack)
f32_convert_u_i64(store, stack)
f32_copysign(store, stack)
f32_demote_f64(store, stack)
f32_div(store, stack)
f32_eq(store, stack)
f32_floor(store, stack)
f32_ge(store, stack)
f32_gt(store, stack)
f32_le(store, stack)
f32_load(store, stack, imm: manticore.wasm.types.MemoryImm)
f32_lt(store, stack)
f32_max(store, stack)
f32_min(store, stack)
f32_mul(store, stack)
f32_ne(store, stack)
f32_nearest(store, stack)
f32_neg(store, stack)
f32_reinterpret_i32(store, stack)
f32_sqrt(store, stack)
f32_store(store, stack, imm: manticore.wasm.types.MemoryImm)
f32_sub(store, stack)
f32_trunc(store, stack)
f32_unary(store, stack, op, rettype: type = <class 'manticore.wasm.types.I32'>)
f64_abs(store, stack)
f64_add(store, stack)
f64_binary(store, stack, op, rettype: type = <class 'manticore.wasm.types.I32'>)
f64_ceil(store, stack)
f64_const(store, stack, imm: manticore.wasm.types.F64ConstImm)
f64_convert_s_i32(store, stack)
f64_convert_s_i64(store, stack)
f64_convert_u_i32(store, stack)
f64_convert_u_i64(store, stack)
f64_copysign(store, stack)
f64_div(store, stack)
f64_eq(store, stack)
f64_floor(store, stack)
f64_ge(store, stack)
f64_gt(store, stack)
f64_le(store, stack)
f64_load(store, stack, imm: manticore.wasm.types.MemoryImm)
f64_lt(store, stack)
f64_max(store, stack)
f64_min(store, stack)
f64_mul(store, stack)
f64_ne(store, stack)
f64_nearest(store, stack)
f64_neg(store, stack)
f64_promote_f32(store, stack)
f64_reinterpret_i64(store, stack)
f64_sqrt(store, stack)
f64_store(store, stack, imm: manticore.wasm.types.MemoryImm)
f64_sub(store, stack)
f64_trunc(store, stack)
f64_unary(store, stack, op, rettype: type = <class 'manticore.wasm.types.F64'>)
float_load(store, stack, imm: manticore.wasm.types.MemoryImm, ty: type)
float_push_compare_return(stack, v, rettype=<class 'manticore.wasm.types.I32'>)
float_store(store, stack, imm: manticore.wasm.types.MemoryImm, ty: type, n=None)
get_global(store, stack, imm: manticore.wasm.types.GlobalVarXsImm)
get_local(store, stack, imm: manticore.wasm.types.LocalVarXsImm)
grow_memory(store, stack, imm: manticore.wasm.types.CurGrowMemImm)
i32_add(store, stack)
i32_and(store, stack)
i32_clz(store, stack)
i32_const(store, stack, imm: manticore.wasm.types.I32ConstImm)
i32_ctz(store, stack)
i32_div_s(store, stack)
i32_div_u(store, stack)
i32_eq(store, stack)
i32_eqz(store, stack)
i32_ge_s(store, stack)
i32_ge_u(store, stack)
i32_gt_s(store, stack)
i32_gt_u(store, stack)
i32_le_s(store, stack)
i32_le_u(store, stack)
i32_load(store, stack, imm: manticore.wasm.types.MemoryImm)
i32_load16_s(store, stack, imm: manticore.wasm.types.MemoryImm)
i32_load16_u(store, stack, imm: manticore.wasm.types.MemoryImm)
i32_load8_s(store, stack, imm: manticore.wasm.types.MemoryImm)
i32_load8_u(store, stack, imm: manticore.wasm.types.MemoryImm)
i32_lt_s(store, stack)
i32_lt_u(store, stack)
i32_mul(store, stack)
i32_ne(store, stack)
i32_or(store, stack)
i32_popcnt(store, stack)
i32_reinterpret_f32(store, stack)
i32_rem_s(store, stack)
i32_rem_u(store, stack)
i32_rotl(store, stack)
i32_rotr(store, stack)
i32_shl(store, stack)
i32_shr_s(store, stack)
i32_shr_u(store, stack)
i32_store(store, stack, imm: manticore.wasm.types.MemoryImm)
i32_store16(store, stack, imm: manticore.wasm.types.MemoryImm)
i32_store8(store, stack, imm: manticore.wasm.types.MemoryImm)
i32_sub(store, stack)
i32_trunc_s_f32(store, stack)
i32_trunc_s_f64(store, stack)
i32_trunc_u_f32(store, stack)
i32_trunc_u_f64(store, stack)
i32_wrap_i64(store, stack)
i32_xor(store, stack)
i64_add(store, stack)
i64_and(store, stack)
i64_clz(store, stack)
i64_const(store, stack, imm: manticore.wasm.types.I64ConstImm)
i64_ctz(store, stack)
i64_div_s(store, stack)
i64_div_u(store, stack)
i64_eq(store, stack)
i64_eqz(store, stack)
i64_extend_s_i32(store, stack)
i64_extend_u_i32(store, stack)
i64_ge_s(store, stack)
i64_ge_u(store, stack)
i64_gt_s(store, stack)
i64_gt_u(store, stack)
i64_le_s(store, stack)
i64_le_u(store, stack)
i64_load(store, stack, imm: manticore.wasm.types.MemoryImm)
i64_load16_s(store, stack, imm: manticore.wasm.types.MemoryImm)
i64_load16_u(store, stack, imm: manticore.wasm.types.MemoryImm)
i64_load32_s(store, stack, imm: manticore.wasm.types.MemoryImm)
i64_load32_u(store, stack, imm: manticore.wasm.types.MemoryImm)
i64_load8_s(store, stack, imm: manticore.wasm.types.MemoryImm)
i64_load8_u(store, stack, imm: manticore.wasm.types.MemoryImm)
i64_lt_s(store, stack)
i64_lt_u(store, stack)
i64_mul(store, stack)
i64_ne(store, stack)
i64_or(store, stack)
i64_popcnt(store, stack)
i64_reinterpret_f64(store, stack)
i64_rem_s(store, stack)
i64_rem_u(store, stack)
i64_rotl(store, stack)
i64_rotr(store, stack)
i64_shl(store, stack)
i64_shr_s(store, stack)
i64_shr_u(store, stack)
i64_store(store, stack, imm: manticore.wasm.types.MemoryImm)
i64_store16(store, stack, imm: manticore.wasm.types.MemoryImm)
i64_store32(store, stack, imm: manticore.wasm.types.MemoryImm)
i64_store8(store, stack, imm: manticore.wasm.types.MemoryImm)
i64_sub(store, stack)
i64_trunc_s_f32(store, stack)
i64_trunc_s_f64(store, stack)
i64_trunc_u_f32(store, stack)
i64_trunc_u_f64(store, stack)
i64_xor(store, stack)
int_load(store, stack, imm: manticore.wasm.types.MemoryImm, ty: type, size: int, signed: bool)
int_store(store, stack, imm: manticore.wasm.types.MemoryImm, ty: type, n=None)
nop(store, stack)
select(store, stack)
set_global(store, stack, imm: manticore.wasm.types.GlobalVarXsImm)
set_local(store, stack, imm: manticore.wasm.types.LocalVarXsImm)
tee_local(store, stack, imm: manticore.wasm.types.LocalVarXsImm)
unreachable(store, stack)
manticore.wasm.executor.operator_ceil(a)
manticore.wasm.executor.operator_div(a, b)
manticore.wasm.executor.operator_floor(a)
manticore.wasm.executor.operator_max(a, b)
manticore.wasm.executor.operator_min(a, b)
manticore.wasm.executor.operator_nearest(a)
manticore.wasm.executor.operator_trunc(a)

Module Structure

class manticore.wasm.structure.Activation(arity, frame, expected_block_depth=0)

Pushed onto the stack with each function invocation to keep track of the call stack

https://www.w3.org/TR/wasm-core-1/#activations-and-frames%E2%91%A0

arity = None

The expected number of return values from the function call associated with the underlying frame

expected_block_depth = None

Internal helper used to track the expected block depth when we exit this label

frame = None

The nested frame

class manticore.wasm.structure.Addr
class manticore.wasm.structure.AtomicStack(parent: manticore.wasm.structure.Stack)

Allows for the rolling-back of the stack in the event of a concretization exception. Inherits from Stack so that the types will be correct, but never calls super. Provides a context manager that will intercept Concretization Exceptions before raising them.

class PopItem(val: Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec, manticore.wasm.structure.Label, manticore.wasm.structure.Activation])
class PushItem
empty()
Returns:True if the stack is empty, otherwise False
find_type(t: type)
Parameters:t – The type to look for
Returns:The depth of the first value of type t
get_frame() → manticore.wasm.structure.Activation
Returns:the topmost frame (Activation) on the stack
get_nth(t: type, n: int)
Parameters:
  • t – type to look for
  • n – number to look for
Returns:

the nth item of type t from the top of the stack, or None
has_at_least(t: type, n: int)
Parameters:
  • t – type to look for
  • n – number to look for
Returns:

whether the stack contains at least n values of type t
has_type_on_top(t: Union[type, Tuple[type, ...]], n: int)

Asserts that the stack has at least n values of type t or type BitVec on the top

Parameters:
  • t – type of value to look for (Bitvec is always included as an option)
  • n – Number of values to check
Returns:

True
peek()
Returns:the item on top of the stack (without removing it)
pop() → Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec, manticore.wasm.structure.Label, manticore.wasm.structure.Activation]

Pop a value from the stack

Returns:the popped value
push(val: Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec, manticore.wasm.structure.Label, manticore.wasm.structure.Activation]) → None

Push a value to the stack

Parameters:val – The value to push
Returns:None
rollback()
exception manticore.wasm.structure.ConcretizeCondition(message: str, condition: manticore.core.smtlib.expression.Bool, current_advice: Optional[List[bool]], **kwargs)

Tells Manticore to concretize a condition required to direct execution.

class manticore.wasm.structure.Data(data: manticore.wasm.types.MemIdx, offset: List[manticore.wasm.types.Instruction], init: List[int])

Vector of bytes that initializes part of a memory

https://www.w3.org/TR/wasm-core-1/#data-segments%E2%91%A0

data = None

Which memory to put the data in. Currently only supports 0

init = None

List of bytes to copy into the memory

offset = None

WASM instructions that calculate offset into the memory

class manticore.wasm.structure.Elem(table: manticore.wasm.types.TableIdx, offset: List[manticore.wasm.types.Instruction], init: List[manticore.wasm.types.FuncIdx])

List of functions to initialize part of a table

https://www.w3.org/TR/wasm-core-1/#element-segments%E2%91%A0

init = None

list of function indices that get copied into the table

offset = None

WASM instructions that calculate an offset to add to the table index

table = None

Which table to initialize

class manticore.wasm.structure.Export(name: manticore.wasm.types.Name, desc: Union[manticore.wasm.types.FuncIdx, manticore.wasm.types.TableIdx, manticore.wasm.types.MemIdx, manticore.wasm.types.GlobalIdx])

Something the module exposes to the outside world once it’s been instantiated

https://www.w3.org/TR/wasm-core-1/#exports%E2%91%A0

desc = None

Whether this is a function, table, memory, or global

name = None

The name of the thing we’re exporting

class manticore.wasm.structure.ExportInst(name: manticore.wasm.types.Name, value: Union[manticore.wasm.structure.FuncAddr, manticore.wasm.structure.TableAddr, manticore.wasm.structure.MemAddr, manticore.wasm.structure.GlobalAddr])

Runtime representation of any thing that can be exported

https://www.w3.org/TR/wasm-core-1/#export-instances%E2%91%A0

name = None

The name to export under

value = None

FuncAddr, TableAddr, MemAddr, or GlobalAddr

class manticore.wasm.structure.Frame(locals: List[Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec]], module: manticore.wasm.structure.ModuleInstance)

Holds more call data, nested inside an activation (for reasons I don’t understand)

https://www.w3.org/TR/wasm-core-1/#activations-and-frames%E2%91%A0

locals = None

The values of the local variables for this function call

module = None

A reference to the parent module instance in which the function call was made

class manticore.wasm.structure.FuncAddr
class manticore.wasm.structure.FuncInst(type: manticore.wasm.types.FunctionType, module: manticore.wasm.structure.ModuleInstance, code: manticore.wasm.structure.Function)

Instance type for WASM functions

class manticore.wasm.structure.Function(type: manticore.wasm.types.TypeIdx, locals: List[type], body: List[manticore.wasm.types.Instruction])

A WASM Function

https://www.w3.org/TR/wasm-core-1/#functions%E2%91%A0

allocate(store: manticore.wasm.structure.Store, module: manticore.wasm.structure.ModuleInstance) → manticore.wasm.structure.FuncAddr

https://www.w3.org/TR/wasm-core-1/#functions%E2%91%A5

Parameters:
  • store – Destination Store that we’ll insert this Function into after allocation
  • module – The module containing the type referenced by self.type
Returns:

The address of this within store
body = None

Sequence of WASM instructions, should leave the appropriate type on the stack

locals = None

Vector of mutable local variables (and their types)

type = None

The index of a type defined in the module that corresponds to this function’s type signature

class manticore.wasm.structure.Global(type: manticore.wasm.types.GlobalType, init: List[manticore.wasm.types.Instruction])

A global variable of a given type

https://www.w3.org/TR/wasm-core-1/#globals%E2%91%A0

allocate(store: manticore.wasm.structure.Store, val: Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec]) → manticore.wasm.structure.GlobalAddr

https://www.w3.org/TR/wasm-core-1/#globals%E2%91%A5

Parameters:
  • store – Destination Store that we’ll insert this Global into after allocation
  • val – The initial value of the new global
Returns:

The address of this within store
init = None

A (constant) sequence of WASM instructions that calculates the value for the global

type = None

The type of the variable

class manticore.wasm.structure.GlobalAddr
class manticore.wasm.structure.GlobalInst(value: Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec], mut: bool)

Instance of a global variable. Stores the value (calculated from evaluating a Global.init) and the mutable flag (taken from GlobalType.mut)

https://www.w3.org/TR/wasm-core-1/#global-instances%E2%91%A0

mut = None

Whether the global can be modified

value = None

The actual value of this global

class manticore.wasm.structure.HostFunc(type: manticore.wasm.types.FunctionType, hostcode: function)

Instance type for native functions that have been provided via import

allocate(store: manticore.wasm.structure.Store, functype: manticore.wasm.types.FunctionType, host_func: function) → manticore.wasm.structure.FuncAddr

Currently not needed.

https://www.w3.org/TR/wasm-core-1/#host-functions%E2%91%A2

hostcode = None

the native function. Should accept ConstraintSet as the first argument

class manticore.wasm.structure.Import(module: manticore.wasm.types.Name, name: manticore.wasm.types.Name, desc: Union[manticore.wasm.types.TypeIdx, manticore.wasm.types.TableType, manticore.wasm.types.LimitType, manticore.wasm.types.GlobalType])

Something imported from another module (or the environment) that we need to instantiate a module

https://www.w3.org/TR/wasm-core-1/#imports%E2%91%A0

desc = None

Specifies whether this is a function, table, memory, or global

module = None

The name of the module we’re importing from

name = None

The name of the thing we’re importing

class manticore.wasm.structure.Label(arity: int, instr: List[manticore.wasm.types.Instruction])

A branch label that can be pushed onto the stack and then jumped to

https://www.w3.org/TR/wasm-core-1/#labels%E2%91%A0

arity = None

the number of values this branch expects to read from the stack

instr = None

The sequence of instructions to execute if we branch to this label

class manticore.wasm.structure.MemAddr
class manticore.wasm.structure.MemInst(starting_data, max=None, *args, **kwargs)

Runtime representation of a memory. As with tables, if you’re dealing with a memory at runtime, it’s probably a MemInst. Currently doesn’t support any sort of symbolic indexing, although you can read and write symbolic bytes using smtlib. There’s a minor quirk where uninitialized data is stored as bytes, but smtlib tries to convert concrete data into ints. That can cause problems if you try to read from the memory directly (without using smtlib) but shouldn’t break any of the built-in WASM instruction implementations.

Memory in WASM is broken up into 65536-byte pages. All pages behave the same way, but note that operations that deal with memory size do so in terms of pages, not bytes.

TODO: We should implement some kind of symbolic memory model

https://www.w3.org/TR/wasm-core-1/#memory-instances%E2%91%A0

dump()
grow(n: int) → bool

Adds n blank pages to the current memory

See: https://www.w3.org/TR/wasm-core-1/#grow-mem

Parameters:n – The number of pages to attempt to add
Returns:True if the operation succeeded, otherwise False
max = None

Optional maximum number of pages the memory can contain

npages
read_bytes(base: int, size: int) → List[Union[int, bytes]]

Reads bytes from memory

Parameters:
  • base – Address to read from
  • size – number of bytes to read
Returns:

List of bytes
read_int(base: int, size: int = 32) → int

Reads bytes from memory and combines them into an int

Parameters:
  • base – Address to read the int from
  • size – Size of the int (in bits)
Returns:

The int in question
write_bytes(base: int, data: Union[str, Sequence[int], Sequence[bytes]])

Writes a stream of bytes into memory

Parameters:
  • base – Index to start writing at
  • data – Data to write
write_int(base: int, expression: Union[manticore.core.smtlib.expression.Expression, int], size: int = 32)

Writes an integer into memory.

Parameters:
  • base – Index to write at
  • expression – integer to write
  • size – Optional size of the integer
class manticore.wasm.structure.Memory(type: manticore.wasm.types.LimitType)

Big chunk o’ raw bytes

https://www.w3.org/TR/wasm-core-1/#memories%E2%91%A0

allocate(store: manticore.wasm.structure.Store) → manticore.wasm.structure.MemAddr

https://www.w3.org/TR/wasm-core-1/#memories%E2%91%A5

Parameters:store – Destination Store that we’ll insert this Memory into after allocation
Returns:The address of this within store
type = None

secretly a LimitType that specifies how big or small the memory can be

class manticore.wasm.structure.Module

Internal representation of a WASM Module

data
elem
exports
funcs
function_names
get_funcnames() → List[manticore.wasm.types.Name]
globals
imports
classmethod load(filename: str)

Converts a WASM module in binary format into Python types that Manticore can understand

Parameters:filename – name of the WASM module
Returns:Module
local_names
mems
start

https://www.w3.org/TR/wasm-core-1/#start-function%E2%91%A0

tables
types
class manticore.wasm.structure.ModuleInstance(constraints=None)

Runtime instance of a module. Stores function types, list of addresses within the store, and exports. In this implementation, it’s also responsible for managing the instruction queue and executing control-flow instructions.

https://www.w3.org/TR/wasm-core-1/#module-instances%E2%91%A0

allocate(store: manticore.wasm.structure.Store, module: manticore.wasm.structure.Module, extern_vals: List[Union[manticore.wasm.structure.FuncAddr, manticore.wasm.structure.TableAddr, manticore.wasm.structure.MemAddr, manticore.wasm.structure.GlobalAddr]], values: List[Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec]])

Inserts imports into the store, then creates and inserts function instances, table instances, memory instances, global instances, and export instances.

https://www.w3.org/TR/wasm-core-1/#allocation%E2%91%A0 https://www.w3.org/TR/wasm-core-1/#modules%E2%91%A6

Parameters:
  • store – The Store to put all of the allocated subcomponents in
  • module – Tne Module containing all the items to allocate
  • extern_vals – Imported values
  • values – precalculated global values
block(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.Stack, ret_type: List[type], insts: List[manticore.wasm.types.Instruction])

Execute a block of instructions. Creates a label with an empty continuation and the proper arity, then enters the block of instructions with that label.

https://www.w3.org/TR/wasm-core-1/#exec-block

Parameters:
  • ret_type – List of expected return types for this block. Really only need the arity
  • insts – Instructions to execute
br(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack, label_depth: int)

Branch to the `label_depth`th label deep on the stack

https://www.w3.org/TR/wasm-core-1/#exec-br

br_if(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack, imm: manticore.wasm.types.BranchImm)

Perform a branch if the value on top of the stack is nonzero

https://www.w3.org/TR/wasm-core-1/#exec-br-if

br_table(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack, imm: manticore.wasm.types.BranchTableImm)

Branch to the nth label deep on the stack where n is found by looking up a value in a table given by the immediate, indexed by the value on top of the stack.

https://www.w3.org/TR/wasm-core-1/#exec-br-table

call(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack, imm: manticore.wasm.types.CallImm)

Invoke the function at the address in the store given by the immediate.

https://www.w3.org/TR/wasm-core-1/#exec-call

call_indirect(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack, imm: manticore.wasm.types.CallIndirectImm)

A function call, but with extra steps. Specifically, you find the index of the function to call by looking in the table at the index given by the immediate.

https://www.w3.org/TR/wasm-core-1/#exec-call-indirect

else_(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack)

Marks the end of the first block of an if statement. Typically, if blocks look like: if <instructions> else <instructions> end. That’s not always the case. See: https://webassembly.github.io/spec/core/text/instructions.html#abbreviations

end(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack)

Marks the end of an instruction block or function

enter_block(insts, label: manticore.wasm.structure.Label, stack: manticore.wasm.structure.Stack)

Push the instructions for the next block to the queue and bump the block depth number

https://www.w3.org/TR/wasm-core-1/#exec-instr-seq-enter

Parameters:
  • insts – Instructions for this block
  • label – Label referencing the continuation of this block
  • stack – The execution stack (where we push the label)
exec_expression(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.Stack, expr: List[manticore.wasm.types.Instruction])

Pushes the given expression to the stack, calls exec_instruction until there are no more instructions to exec, then returns the top value on the stack. Used during initialization to calculate global values, memory offsets, element offsets, etc.

Parameters:expr – The expression to execute
Returns:The result of the expression
exec_instruction(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.Stack, advice: Optional[List[bool]] = None, current_state=None) → bool

The core instruction execution function. Pops an instruction from the queue, then dispatches it to the Executor if it’s a numeric instruction, or executes it internally if it’s a control-flow instruction.

Parameters:store – The execution Store to use, passed in from the parent WASMWorld. This is passed to almost all
instruction implementations, but for brevity’s sake, it’s only explicitly documented here.
Parameters:stack – The execution Stack to use, likewise passed in from the parent WASMWorld and only documented here,
despite being passed to all the instruction implementations.
Parameters:advice – A list of concretized conditions to advice execution of the instruction.
Returns:True if execution succeeded, False if there are no more instructions to execute
executor

Contains instruction implementations for all non-control-flow instructions

exit_block(stack: manticore.wasm.structure.Stack)

Cleans up after execution of a code block.

https://www.w3.org/TR/wasm-core-1/#exiting–hrefsyntax-instrmathitinstrast-with-label–l

exit_function(stack: manticore.wasm.structure.AtomicStack)

Discards the current frame, allowing execution to return to the point after the call

https://www.w3.org/TR/wasm-core-1/#returning-from-a-function%E2%91%A0

export_map

Maps the names of exports to their index in the list of exports

exports

Stores records of everything exported by this module

extract_block(partial_list: Deque[manticore.wasm.types.Instruction]) → Deque[manticore.wasm.types.Instruction]

Recursively extracts blocks from a list of instructions, similar to self.look_forward. The primary difference is that this version takes a list of instructions to operate over, instead of popping instructions from the instruction queue.

Parameters:partial_list – List of instructions to extract the block from
Returns:The extracted block
funcaddrs

Stores the indices of functions within the store

function_names

Stores names of store functions, if available

get_export(name: str, store: manticore.wasm.structure.Store) → Union[manticore.wasm.structure.ProtoFuncInst, manticore.wasm.structure.TableInst, manticore.wasm.structure.MemInst, manticore.wasm.structure.GlobalInst, Callable]

Retrieves a value exported by this module instance from store

Parameters:
  • name – The name of the exported value to get
  • store – The current execution store (where the export values live)
Returns:

The value of the export
get_export_address(name: str) → Union[manticore.wasm.structure.FuncAddr, manticore.wasm.structure.TableAddr, manticore.wasm.structure.MemAddr, manticore.wasm.structure.GlobalAddr]

Retrieves the address of a value exported by this module within the store

Parameters:name – The name of the exported value to get
Returns:The address of the desired export
globaladdrs

Stores the indices of globals

if_(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack, ret_type: List[type])

Brackets two nested sequences of instructions. If the value on top of the stack is nonzero, enter the first block. If not, enter the second.

https://www.w3.org/TR/wasm-core-1/#exec-if

instantiate(store: manticore.wasm.structure.Store, module: manticore.wasm.structure.Module, extern_vals: List[Union[manticore.wasm.structure.FuncAddr, manticore.wasm.structure.TableAddr, manticore.wasm.structure.MemAddr, manticore.wasm.structure.GlobalAddr]], exec_start: bool = False)

Type checks the module, evaluates globals, performs allocation, and puts the element and data sections into their proper places. Optionally calls the start function _outside_ of a symbolic context if exec_start is true.

https://www.w3.org/TR/wasm-core-1/#instantiation%E2%91%A1

Parameters:
  • store – The store to place the allocated contents in
  • module – The WASM Module to instantiate in this instance
  • extern_vals – Imports needed to instantiate the module
  • exec_start – whether or not to execute the start section (if present)
instantiated = None

Prevents the user from invoking functions before instantiation

invoke(stack: manticore.wasm.structure.Stack, funcaddr: manticore.wasm.structure.FuncAddr, store: manticore.wasm.structure.Store, argv: List[Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec]])

Invocation wrapper. Checks the function type, pushes the args to the stack, and calls _invoke_inner. Unclear why the spec separates the two procedures, but I’ve tried to implement it as close to verbatim as possible.

Note that this doesn’t actually _run_ any code. It just sets up the instruction queue so that when you call `exec_instruction, it’ll actually have instructions to execute.

https://www.w3.org/TR/wasm-core-1/#invocation%E2%91%A1

Parameters:
  • funcaddr – Address (in Store) of the function to call
  • argv – Arguments to pass to the function. Can be BitVecs or Values
invoke_by_name(name: str, stack, store, argv)

Iterates over the exports, attempts to find the function specified by name. Calls invoke with its FuncAddr, passing argv

Parameters:
  • name – Name of the function to look for
  • argv – Arguments to pass to the function. Can be BitVecs or Values
local_names

Stores names of local variables, if available

look_forward(*opcodes) → List[manticore.wasm.types.Instruction]

Pops contents of the instruction queue until it finds an instruction with an opcode in the argument *opcodes. Used to find the end of a code block in the flat instruction queue. For this reason, it calls itself recursively (looking for the end instruction) if it encounters a block, loop, or if instruction.

Parameters:opcodes – Tuple of instruction opcodes to look for
Returns:The list of instructions popped before encountering the target instruction.
loop(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack, loop_inst)

Enter a loop block. Creates a label with a copy of the loop as a continuation, then enters the loop instructions with that label.

https://www.w3.org/TR/wasm-core-1/#exec-loop

Parameters:loop_inst – The current insrtuction
memaddrs

Stores the indices of memories (at time of writing, WASM only allows one memory)

push_instructions(insts: List[manticore.wasm.types.Instruction])

Pushes instructions into the instruction queue. :param insts: Instructions to push

reset_internal()

Empties the instruction queue and clears the block depths

return_(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack)

Return from the function (ie branch to the outermost block)

https://www.w3.org/TR/wasm-core-1/#exec-return

tableaddrs

Stores the indices of tables

types

Stores the type signatures of all the functions

manticore.wasm.structure.PAGESIZE = 65536

Size of a standard WASM memory page

class manticore.wasm.structure.ProtoFuncInst(type: manticore.wasm.types.FunctionType)

Groups FuncInst and HostFuncInst into the same category

type = None

The type signature of this function

class manticore.wasm.structure.Stack(init_data=None)

Stores the execution stack & provides helper methods

https://www.w3.org/TR/wasm-core-1/#stack%E2%91%A0

data = None

Underlying datastore for the “stack”

empty() → bool
Returns:True if the stack is empty, otherwise False
find_type(t: type) → Optional[int]
Parameters:t – The type to look for
Returns:The depth of the first value of type t
get_frame() → manticore.wasm.structure.Activation
Returns:the topmost frame (Activation) on the stack
get_nth(t: type, n: int) → Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec, manticore.wasm.structure.Label, manticore.wasm.structure.Activation, None]
Parameters:
  • t – type to look for
  • n – number to look for
Returns:

the nth item of type t from the top of the stack, or None
has_at_least(t: type, n: int) → bool
Parameters:
  • t – type to look for
  • n – number to look for
Returns:

whether the stack contains at least n values of type t
has_type_on_top(t: Union[type, Tuple[type, ...]], n: int)

Asserts that the stack has at least n values of type t or type BitVec on the top

Parameters:
  • t – type of value to look for (Bitvec is always included as an option)
  • n – Number of values to check
Returns:

True
peek() → Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec, manticore.wasm.structure.Label, manticore.wasm.structure.Activation, None]
Returns:the item on top of the stack (without removing it)
pop() → Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec, manticore.wasm.structure.Label, manticore.wasm.structure.Activation]

Pop a value from the stack

Returns:the popped value
push(val: Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec, manticore.wasm.structure.Label, manticore.wasm.structure.Activation]) → None

Push a value to the stack

Parameters:val – The value to push
Returns:None
class manticore.wasm.structure.Store

Implementation of the WASM store. Nothing fancy here, just collects lists of functions, tables, memories, and globals. Because the store is not atomic, instructions SHOULD NOT make changes to the Store or any of its contents (including memories and global variables) before raising a Concretize exception.

https://www.w3.org/TR/wasm-core-1/#store%E2%91%A0

funcs
globals
mems
tables
class manticore.wasm.structure.Table(type: manticore.wasm.types.TableType)

Vector of opaque values of type self.type

https://www.w3.org/TR/wasm-core-1/#tables%E2%91%A0

allocate(store: manticore.wasm.structure.Store) → manticore.wasm.structure.TableAddr

https://www.w3.org/TR/wasm-core-1/#tables%E2%91%A5

Parameters:store – Destination Store that we’ll insert this Table into after allocation
Returns:The address of this within store
type = None

union of a limit and a type (currently only supports funcref)s

class manticore.wasm.structure.TableAddr
class manticore.wasm.structure.TableInst(elem: List[Optional[manticore.wasm.structure.FuncAddr]], max: Optional[manticore.wasm.types.U32])

Runtime representation of a table. Remember that the Table type stores the type of the data contained in the table and basically nothing else, so if you’re dealing with a table at runtime, it’s probably a TableInst. The WASM spec has a lot of similar-sounding names for different versions of one thing.

https://www.w3.org/TR/wasm-core-1/#table-instances%E2%91%A0

elem = None

A list of FuncAddrs (any of which can be None) that point to funcs in the Store

max = None

Optional maximum size of the table

manticore.wasm.structure.strip_quotes(rough_name: str) → manticore.wasm.types.Name

For some reason, the parser returns the function names with quotes around them

Parameters:rough_name –
Returns:

Types

class manticore.wasm.types.BlockImm(sig: int)
class manticore.wasm.types.BranchImm(relative_depth: manticore.wasm.types.U32)
class manticore.wasm.types.BranchTableImm(target_count: manticore.wasm.types.U32, target_table: List[manticore.wasm.types.U32], default_target: manticore.wasm.types.U32)
class manticore.wasm.types.CallImm(function_index: manticore.wasm.types.U32)
class manticore.wasm.types.CallIndirectImm(type_index: manticore.wasm.types.U32, reserved: manticore.wasm.types.U32)
exception manticore.wasm.types.ConcretizeStack(depth: int, ty: type, message: str, expression, policy=None, **kwargs)

Tells Manticore to concretize the value depth values from the end of the stack.

class manticore.wasm.types.CurGrowMemImm(reserved: bool)
manticore.wasm.types.ExternType = typing.Union[manticore.wasm.types.FunctionType, manticore.wasm.types.TableType, manticore.wasm.types.LimitType, manticore.wasm.types.GlobalType]

https://www.w3.org/TR/wasm-core-1/#external-types%E2%91%A0

class manticore.wasm.types.F32

Subclass of float that’s restricted to 32-bit values

classmethod cast(other)
Parameters:other – Value to convert to F32
Returns:If other is symbolic, other. Otherwise, F32(other)
class manticore.wasm.types.F32ConstImm(value: manticore.wasm.types.F32)
class manticore.wasm.types.F64

Subclass of float that’s restricted to 64-bit values

classmethod cast(other)
Parameters:other – Value to convert to F64
Returns:If other is symbolic, other. Otherwise, F64(other)
class manticore.wasm.types.F64ConstImm(value: manticore.wasm.types.F64)
class manticore.wasm.types.FuncIdx
class manticore.wasm.types.FunctionType(param_types: List[type], result_types: List[type])

https://www.w3.org/TR/wasm-core-1/#syntax-functype

param_types = None

Sequential types of each of the parameters

result_types = None

Sequential types of each of the return values

class manticore.wasm.types.GlobalIdx
class manticore.wasm.types.GlobalType(mut: bool, value: type)

https://www.w3.org/TR/wasm-core-1/#syntax-globaltype

mut = None

Whether or not this global is mutable

value = None

The value of the global

class manticore.wasm.types.GlobalVarXsImm(global_index: manticore.wasm.types.U32)
class manticore.wasm.types.I32

Subclass of int that’s restricted to 32-bit values

classmethod cast(other)
Parameters:other – Value to convert to I32
Returns:If other is symbolic, other. Otherwise, I32(other)
static to_unsigned(val)

Reinterprets the argument from a signed integer to an unsigned 32-bit integer

Parameters:val – Signed integer to reinterpret
Returns:The unsigned equivalent
class manticore.wasm.types.I32ConstImm(value: manticore.wasm.types.I32)
class manticore.wasm.types.I64

Subclass of int that’s restricted to 64-bit values

classmethod cast(other)
Parameters:other – Value to convert to I64
Returns:If other is symbolic, other. Otherwise, I64(other)
static to_unsigned(val)

Reinterprets the argument from a signed integer to an unsigned 64-bit integer

Parameters:val – Signed integer to reinterpret
Returns:The unsigned equivalent
class manticore.wasm.types.I64ConstImm(value: manticore.wasm.types.I64)
manticore.wasm.types.ImmType = typing.Union[manticore.wasm.types.BlockImm, manticore.wasm.types.BranchImm, manticore.wasm.types.BranchTableImm, manticore.wasm.types.CallImm, manticore.wasm.types.CallIndirectImm, manticore.wasm.types.LocalVarXsImm, manticore.wasm.types.GlobalVarXsImm, manticore.wasm.types.MemoryImm, manticore.wasm.types.CurGrowMemImm, manticore.wasm.types.I32ConstImm, manticore.wasm.types.F32ConstImm, manticore.wasm.types.F64ConstImm]

Types of all immediates

class manticore.wasm.types.Instruction(inst: wasm.decode.Instruction, imm=None)

Internal instruction class that’s pickle-friendly and works with the type system

imm

A class with the immediate data for this instruction

mnemonic

Used for debugging

opcode

Opcode, used for dispatching instructions

exception manticore.wasm.types.InvalidConversionTrap(ty, val)
class manticore.wasm.types.LabelIdx
class manticore.wasm.types.LimitType(min: manticore.wasm.types.U32, max: Optional[manticore.wasm.types.U32])

https://www.w3.org/TR/wasm-core-1/#syntax-limits

class manticore.wasm.types.LocalIdx
class manticore.wasm.types.LocalVarXsImm(local_index: manticore.wasm.types.U32)
class manticore.wasm.types.MemIdx
class manticore.wasm.types.MemoryImm(flags: manticore.wasm.types.U32, offset: manticore.wasm.types.U32)
manticore.wasm.types.MemoryType

https://www.w3.org/TR/wasm-core-1/#syntax-memtype

alias of manticore.wasm.types.LimitType

exception manticore.wasm.types.MissingExportException(name)
class manticore.wasm.types.Name
exception manticore.wasm.types.NonExistentFunctionCallTrap
exception manticore.wasm.types.OutOfBoundsMemoryTrap(addr)
exception manticore.wasm.types.OverflowDivisionTrap
class manticore.wasm.types.TableIdx
class manticore.wasm.types.TableType(limits: manticore.wasm.types.LimitType, elemtype: type)

https://www.w3.org/TR/wasm-core-1/#syntax-tabletype

elemtype = None

the type ot the element. Currently, the only element type is funcref

limits = None

Minimum and maximum size of the table

exception manticore.wasm.types.Trap

Subclass of Exception, used for WASM errors

class manticore.wasm.types.TypeIdx
exception manticore.wasm.types.TypeMismatchTrap(ty1, ty2)
class manticore.wasm.types.U32
class manticore.wasm.types.U64
exception manticore.wasm.types.UnreachableInstructionTrap
manticore.wasm.types.ValType

alias of builtins.type

manticore.wasm.types.Value = typing.Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec]

https://www.w3.org/TR/wasm-core-1/#syntax-val

exception manticore.wasm.types.ZeroDivisionTrap
manticore.wasm.types.convert_instructions(inst_seq) → List[manticore.wasm.types.Instruction]

Converts instructions output from the parser into full-fledged Python objects that will work with Manticore. This is necessary because the pywasm module uses lots of reflection to generate structures on the fly, which doesn’t play nicely with Pickle or the type system. That’s why we need the debug method above to print out immediates, and also why we’ve created a separate class for every different type of immediate.

Parameters:inst_seq – Sequence of raw instructions to process
Returns:The properly-typed instruction sequence in a format Manticore can use
manticore.wasm.types.debug(imm)

Attempts to pull meaningful data out of an immediate, which has a dynamic GeneratedStructure type

Parameters:imm – the instruction immediate
Returns:a printable representation of the immediate, or the immediate itself