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.
-
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, 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]], supplemental_env: Dict[str, Dict[str, Union[manticore.wasm.structure.ProtoFuncInst, manticore.wasm.structure.TableInst, manticore.wasm.structure.MemInst, manticore.wasm.structure.GlobalInst]]] = {}, 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]], 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
(constraints, *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¶
-
constraints
= None¶ Constraint set to use for checking overflows and boundary conditions
-
current_memory
(store, stack, imm: wasm.immtypes.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: wasm.immtypes.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: wasm.immtypes.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: wasm.immtypes.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: wasm.immtypes.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: wasm.immtypes.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: wasm.immtypes.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: wasm.immtypes.MemoryImm, ty: type)¶
-
float_push_compare_return
(stack, v, rettype=<class 'manticore.wasm.types.I32'>)¶
-
float_store
(store, stack, imm: wasm.immtypes.MemoryImm, ty: type, n=None)¶
-
get_global
(store, stack, imm: wasm.immtypes.GlobalVarXsImm)¶
-
get_local
(store, stack, imm: wasm.immtypes.LocalVarXsImm)¶
-
grow_memory
(store, stack, imm: wasm.immtypes.CurGrowMemImm)¶
-
i32_add
(store, stack)¶
-
i32_and
(store, stack)¶
-
i32_clz
(store, stack)¶
-
i32_const
(store, stack, imm: wasm.immtypes.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: wasm.immtypes.MemoryImm)¶
-
i32_load16_s
(store, stack, imm: wasm.immtypes.MemoryImm)¶
-
i32_load16_u
(store, stack, imm: wasm.immtypes.MemoryImm)¶
-
i32_load8_s
(store, stack, imm: wasm.immtypes.MemoryImm)¶
-
i32_load8_u
(store, stack, imm: wasm.immtypes.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: wasm.immtypes.MemoryImm)¶
-
i32_store16
(store, stack, imm: wasm.immtypes.MemoryImm)¶
-
i32_store8
(store, stack, imm: wasm.immtypes.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: wasm.immtypes.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: wasm.immtypes.MemoryImm)¶
-
i64_load16_s
(store, stack, imm: wasm.immtypes.MemoryImm)¶
-
i64_load16_u
(store, stack, imm: wasm.immtypes.MemoryImm)¶
-
i64_load32_s
(store, stack, imm: wasm.immtypes.MemoryImm)¶
-
i64_load32_u
(store, stack, imm: wasm.immtypes.MemoryImm)¶
-
i64_load8_s
(store, stack, imm: wasm.immtypes.MemoryImm)¶
-
i64_load8_u
(store, stack, imm: wasm.immtypes.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: wasm.immtypes.MemoryImm)¶
-
i64_store16
(store, stack, imm: wasm.immtypes.MemoryImm)¶
-
i64_store32
(store, stack, imm: wasm.immtypes.MemoryImm)¶
-
i64_store8
(store, stack, imm: wasm.immtypes.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: wasm.immtypes.MemoryImm, ty: type, size: int, signed: bool)¶
-
int_store
(store, stack, imm: wasm.immtypes.MemoryImm, ty: type, n=None)¶
-
nop
(store, stack)¶
-
select
(store, stack)¶
-
set_global
(store, stack, imm: wasm.immtypes.GlobalVarXsImm)¶
-
set_local
(store, stack, imm: wasm.immtypes.LocalVarXsImm)¶
-
tee_local
(store, stack, imm: wasm.immtypes.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
()¶
-
class
-
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: 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.
-
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
¶
-
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
-
br_if
(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack, imm: wasm.immtypes.BranchImm)¶ Perform a branch if the value on top of the stack is nonzero
-
br_table
(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack, imm: wasm.immtypes.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.
-
call
(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack, imm: wasm.immtypes.CallImm)¶ Invoke the function at the address in the store given by the immediate.
-
call_indirect
(store: manticore.wasm.structure.Store, stack: manticore.wasm.structure.AtomicStack, imm: wasm.immtypes.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.
-
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, 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.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]¶ 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.
-
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)
-
state
= None¶ Stickies the current state before each instruction
-
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]¶
-
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)
-
classmethod
-
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)
-
classmethod
-
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
-
classmethod
-
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
-
classmethod
-
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])¶
-
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]¶
-
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