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¶: 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¶: Stores concretized information used to advise execution of the next instruction.

constraints¶: 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) → Optional[Union[manticore.wasm.structure.ProtoFuncInst, manticore.wasm.structure.TableInst, manticore.wasm.structure.MemInst, manticore.wasm.structure.GlobalInst, Callable]]¶

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

property instance: manticore.wasm.structure.ModuleInstance¶

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¶: 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

property module: manticore.wasm.structure.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¶: Stores numeric values, branch labels, and execution frames

store¶: 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: int¶: The expected number of return values from the function call associated with the underlying frame

expected_block_depth: int¶: Internal helper used to track the expected block depth when we exit this label

frame: manticore.wasm.structure.Frame¶: 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])¶

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¶

data: Deque[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]]¶: Underlying datastore for the “stack”

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: manticore.wasm.types.MemIdx¶: Which memory to put the data in. Currently only supports 0

init: List[int]¶: List of bytes to copy into the memory

offset: List[manticore.wasm.types.Instruction]¶: 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: List[manticore.wasm.types.FuncIdx]¶: list of function indices that get copied into the table

offset: List[manticore.wasm.types.Instruction]¶: WASM instructions that calculate an offset to add to the table index

table: manticore.wasm.types.TableIdx¶: 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: Union[manticore.wasm.types.FuncIdx, manticore.wasm.types.TableIdx, manticore.wasm.types.MemIdx, manticore.wasm.types.GlobalIdx]¶: Whether this is a function, table, memory, or global

name: manticore.wasm.types.Name¶: 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: manticore.wasm.types.Name¶: The name to export under

value: Union[manticore.wasm.structure.FuncAddr, manticore.wasm.structure.TableAddr, manticore.wasm.structure.MemAddr, manticore.wasm.structure.GlobalAddr]¶: 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: List[Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec]]¶: The values of the local variables for this function call

module: manticore.wasm.structure.ModuleInstance¶: 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

code: manticore.wasm.structure.Function¶

module: manticore.wasm.structure.ModuleInstance¶

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: List[manticore.wasm.types.Instruction]¶: Sequence of WASM instructions, should leave the appropriate type on the stack

locals: List[type]¶: Vector of mutable local variables (and their types)

type: manticore.wasm.types.TypeIdx¶: 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: List[manticore.wasm.types.Instruction]¶: A (constant) sequence of WASM instructions that calculates the value for the global

type: manticore.wasm.types.GlobalType¶: 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: bool¶: Whether the global can be modified

value: Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec]¶: 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: function¶: 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: Union[manticore.wasm.types.TypeIdx, manticore.wasm.types.TableType, manticore.wasm.types.LimitType, manticore.wasm.types.GlobalType]¶: Specifies whether this is a function, table, memory, or global

module: manticore.wasm.types.Name¶: The name of the module we’re importing from

name: manticore.wasm.types.Name¶: 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: int¶: the number of values this branch expects to read from the stack

instr: List[manticore.wasm.types.Instruction]¶: 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: Optional[manticore.wasm.types.U32]¶: Optional maximum number of pages the memory can contain

property 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: manticore.wasm.types.LimitType¶: 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: List[manticore.wasm.structure.Data]¶

elem: List[manticore.wasm.structure.Elem]¶

exports: List[manticore.wasm.structure.Export]¶

funcs: List[manticore.wasm.structure.Function]¶

function_names: Dict[manticore.wasm.structure.FuncAddr, str]¶

get_funcnames() → List[manticore.wasm.types.Name]¶

globals: List[manticore.wasm.structure.Global]¶

imports: List[manticore.wasm.structure.Import]¶

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: Dict[manticore.wasm.structure.FuncAddr, Dict[int, str]]¶

mems: List[manticore.wasm.structure.Memory]¶

start: Optional[manticore.wasm.types.FuncIdx]¶: https://www.w3.org/TR/wasm-core-1/#start-function%E2%91%A0

tables: List[manticore.wasm.structure.Table]¶

types: List[manticore.wasm.types.FunctionType]¶

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: manticore.wasm.executor.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: Dict[str, int]¶: Maps the names of exports to their index in the list of exports

exports: List[manticore.wasm.structure.ExportInst]¶: 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: List[manticore.wasm.structure.FuncAddr]¶: Stores the indices of functions within the store

function_names: Dict[manticore.wasm.structure.FuncAddr, str]¶: 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: List[manticore.wasm.structure.GlobalAddr]¶: 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: bool¶: 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: Dict[manticore.wasm.structure.FuncAddr, Dict[int, str]]¶: 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: List[manticore.wasm.structure.MemAddr]¶: 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: List[manticore.wasm.structure.TableAddr]¶: Stores the indices of tables

types: List[manticore.wasm.types.FunctionType]¶: 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: manticore.wasm.types.FunctionType¶: 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: Deque[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]]¶: 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) → Optional[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]]¶

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() → Optional[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]]¶

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: List[manticore.wasm.structure.ProtoFuncInst]¶

globals: List[manticore.wasm.structure.GlobalInst]¶

mems: List[manticore.wasm.structure.MemInst]¶

tables: List[manticore.wasm.structure.TableInst]¶

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: manticore.wasm.types.TableType¶: 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: List[Optional[manticore.wasm.structure.FuncAddr]]¶: A list of FuncAddrs (any of which can be None) that point to funcs in the Store

max: Optional[manticore.wasm.types.U32]¶: 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)¶

sig: int¶

class manticore.wasm.types.BranchImm(relative_depth: manticore.wasm.types.U32)¶

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)¶

default_target: manticore.wasm.types.U32¶

target_count: manticore.wasm.types.U32¶

target_table: List[manticore.wasm.types.U32]¶

class manticore.wasm.types.CallImm(function_index: manticore.wasm.types.U32)¶

function_index: manticore.wasm.types.U32¶

class manticore.wasm.types.CallIndirectImm(type_index: manticore.wasm.types.U32, reserved: manticore.wasm.types.U32)¶

reserved: manticore.wasm.types.U32¶

type_index: 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)¶

reserved: bool¶

manticore.wasm.types.ExternType¶

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

alias of Union[manticore.wasm.types.FunctionType, manticore.wasm.types.TableType, manticore.wasm.types.LimitType, manticore.wasm.types.GlobalType]

class manticore.wasm.types.F32(val)¶

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)¶

value: manticore.wasm.types.F32¶

class manticore.wasm.types.F64(val)¶

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)¶

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: List[type]¶: Sequential types of each of the parameters

result_types: List[type]¶: 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: bool¶: Whether or not this global is mutable

value: type¶: The value of the global

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

global_index: manticore.wasm.types.U32¶

class manticore.wasm.types.I32(val)¶

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)¶

value: manticore.wasm.types.I32¶

class manticore.wasm.types.I64(val)¶

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)¶

value: manticore.wasm.types.I64¶

manticore.wasm.types.ImmType¶

Types of all immediates

alias of 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]

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: 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]¶: A class with the immediate data for this instruction

mnemonic: str¶: Used for debugging

opcode: int¶: 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

max: Optional[manticore.wasm.types.U32]¶

min: manticore.wasm.types.U32¶

class manticore.wasm.types.LocalIdx¶

class manticore.wasm.types.LocalVarXsImm(local_index: manticore.wasm.types.U32)¶

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)¶

flags: manticore.wasm.types.U32¶

offset: manticore.wasm.types.U32¶

manticore.wasm.types.MemoryType¶: https://www.w3.org/TR/wasm-core-1/#syntax-memtype

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: type¶: the type ot the element. Currently, the only element type is funcref

limits: manticore.wasm.types.LimitType¶: 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 type

manticore.wasm.types.Value¶

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

alias of Union[manticore.wasm.types.I32, manticore.wasm.types.I64, manticore.wasm.types.F32, manticore.wasm.types.F64, manticore.core.smtlib.expression.BitVec]

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

Web Assembly¶

ManticoreWASM¶

WASM World¶

Executor¶

Module Structure¶

Types¶

Manticore

Navigation

Related Topics