From 1208759e553047f7f31e683ede24439558a24fe4 Mon Sep 17 00:00:00 2001 From: Eric Hennenfent Date: Fri, 8 Nov 2019 07:58:24 -0800 Subject: [PATCH] WASM Support MVP (#1495) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The WASM branch is ready to be included in the rest of Manticore. It doesn't include several advanced features, including a symbolic memory model, symbolic floating point support, or a standard library implementation (WASI/emscripten), but it does have full symbolic semantics for all of the integer instructions. ### Commit log: * Empty WASM Module Will run on a .wasm file and do nothing forever * Read and parse sections /shrug * Can partially allocate modules Just pushing for the weekend * Blacken * Can allocate with exports now * Static initialization Doesn't evaluate any of the starting expressions, but that's okay * Make type hints a little more pycharm-friendly * First part of invocation * Blacken... * Barebones execution poc Can execute the following snippet: ``` main(){ return 42; } ``` * blacken * Add some loads and stores * Add global operations * Move float methods further down * Support internal function calls ``` 18:20:42 (mc) ehennenfent@nessie:~/wasm ➜ cat loop_check.c #include #include bool check(int arg){ if (((arg << 2) ^ 16) == 36) { return true; } else{ return false; } } int main(){ printf("Hello world!\n"); int g = getchar(); printf("Got: %d\n", g); int y = 0; for (int i = 0; i < 20; i++){ y++; if (y > 18){ return check(g) ? 0 : -1; } } return -1; } 18:20:54 (mc) ehennenfent@nessie:~/wasm ➜ manticore loop_check.wasm 65: i32.const (16) 11: end 65: i32.const (32) 11: end Initialization Complete 65: i32.const (0) 65: i32.const (0) 40: i32.load (Offset 4) 65: i32.const (16) 107: i32.sub 34: tee_local (Local 1) 54: i32.store (Offset 4) 65: i32.const (32) 16: call (Func Idx 2) Called stub function with args: (32,) HostFunc returned [13] 26: drop 32: get_local (Local 1) 16: call (Func Idx 0) Called stub function with args: () HostFunc returned [13] 34: tee_local (Local 0) 54: i32.store (Offset 0) 65: i32.const (16) 32: get_local (Local 1) 16: call (Func Idx 1) Called stub function with args: (16, 16) HostFunc returned [13] 26: drop 65: i32.const (0) 32: get_local (Local 1) 65: i32.const (16) 106: i32.add 54: i32.store (Offset 4) 65: i32.const (-1) 65: i32.const (0) 32: get_local (Local 0) 65: i32.const (1073741823) 113: i32.and 65: i32.const (13) 71: i32.ne 27: select 11: end [0] 2019-07-25 18:20:58,138: [13842] m.c.manticore:INFO: Generated testcase No. 0 - test 2019-07-25 18:20:58,143: [13842] m.c.manticore:INFO: Results in /home/ehennenfent/wasm/mcore_1evptpip ``` * Improve pickle-friendliness * Convert wasm module instructions into internal type s * Fix class naming conflict Thanks Pickle * Support bitvecs as an integer type * Refactor execution to handle single instructions at a time * Add Atomic Stacks It's a very inefficient implementation, but we'll make it better * Handle Concretize Exceptions Needs a lot of fine tuning but it's a start * Propagate symbols all the way to return * Add test generation infrastructure Still very basic but it's a start * Attempt to make Travis happy * Fix missing generation step * Ignore stack exhaustsion and invalid modules * Add basic shift instructions * Add lots of arithmetic instructions * Fix global initialization * Add optimization for fixed size left shift * Make Travis tests less verbose * Blacken * Properly handle modulo in shifting * Add several control flow instructions * Blacken * Partially Fix return instruction * Fix missing return value from look_forward * Update look_forward to handle nested blocks * Fix type sigs and executor copy/paste errors, deduplicate test names * Fix an instruction exit issue * Fix local ordering * Blacken * test_address now passes for wasm Fixed issue with json2mc.py issue with testname uniqueness Started some work on floating point * i hate git * i hate git * Adding linenumber to testcase function name minor float progress * f32_cmp passed for wasm * f64_cmp passes for wasm * f32_bitwise passes except for the problem with assertEqual not working with nan * f64_bitwise passes except for the problem with assertEqual not working with nan * Fixed the tests to handle [nan] comparisons * better handling of nans and infinites * added integer backing value for f64 * Blacken * Blacken * f64.nearest * Fix argument ordering and implement N-bit memory stores * Use subtests * Switch print to logger * Modify control flow instructions to match spec "Continuation" != the thing that goes inside the Label * Teporarily disable call instructions to prevent infinite loop Still need to figure out control flow for nested function calls * Blacken * Fixed infinite loop in _call via block depth tracking The behavior of `end` needs to depend on how many labels and activations are on the stack. Every time we push or pop a label, we increment or decrement the counter for the current call frame. * Blacken * Initial `br` implementation Probably still bugged * Support if blocks without an else instruction * Add call_indirect * Add grow_memory * i32_wrap_i64 * Add several arithmetic operators * Copy i32.ctz impl from x86 TZCNT * Fix off-by-one in br I think this is the correct fix (it makes all the _br tests pass) but I'm leaving the TODO there just in case. * Blacken... * Fix lingering issue with if block splitting * Fix bad args to sextend in i64_extend_s_i32 * Fix indirect call null check and Float binop return types * Improve br_table indexing See comment * Remove vestigial argument popping in invoke * Fix looking forward in _return and _block * Blacken * Generate trap and action tests * Fix extraneous call to exec_for_test * Fix missing traps in load instructions * Fix c1=0 case in ctz/clz Hopefully this also fixes the fact that the original CTZ implementations seems to have been intended for little-endian architectures * Handle traps in-stride during test execution * Treat zero division as trap * Use ctypes to convert integers * Blacken * Apparently I was wrong about the CTZ endianness thing * Better range checks for offsets This really hammers home why checking whether ea + size is _greater than_ len(mem.data) is strange if mem.data is 0-indexed, but idk, that's what the spec says. * Make stub functions return the correct number of results * ctypes can't handle floats * Add option to run the start function * Correctly handle functions with unacceptable names * Blacken * Treat NotImplemented as a Skip Also counts individual subtests directly instead of screwing around with trying to grep for them in the log. * Fix unhandled negative indices * Fixed some integer instruction bugs i64/32: div_s/u shr_s/u shl clz * Fix global and memory imports * CC * Make default loglevel debug * Rework conversion from int * Make float_store work * _actually_ fix float_store * Restore old float creation method * Blacken * Add range checks to float load/store * Force cast to unsigned in _u instructions * Fix yet another I32 -> I64 copy paste error How many times do we have to teach you this lesson, ~old~ young man? * Skip problematic float tests for now * Handle floating point inaccuracies when dividing large ints * Skip conversion and endianness tests * Rotl, rotl, popcnt * Blacken * Add some conversion stubs * Maybe fix conversions * Improve reinterpret and float demotion * Re-enable endianness tests * Include WASM logging in verbosity controls * Propagate constraints to executor * Blacken * Add prototype symbolic tests * Add api for invocation to Manticore object * Temporarily disable native/evm tests There's no reason to tie up Travis for 40 minutes every time I push a commit. * Fix wasmworld import * Concretize br_if * Pass arg generator to invoke * Download updated WABT It's fixed now! * Generate Symbolic tests (partial) * Follow m.run format * Blacken * Reinitialize Manticore every 50 tests This should cut down on the performance issues we've been seeing * Revert "Temporarily disable native/evm tests" This reverts commit 7abd6c1333ed99fbf0a21a87767bd4e540d049e8. * I32 and I64 pass Symbolic * Create new MC on reinit * Blacken * Fix return handling in test generation * Concretize operand in `if_` * Concretize memory addresses before access In the long run, we should have a symbolic memory model * Better memory access concretization (and br_table) * Concretize float converions and indirect call operands * Run start method * Handle size errors in wrap+i64 and select * Add timeout (and skip extra-problematic tests) * Blacken * Aggressively concretize floats * Recast ints that should have been floats * Better trap handling * Unstash float concretization * Fix log-lived 'trap' attr * Blacken * Concretize F32 when promoting to F64 _shouldn't_ strictly be necesssary, but the lazy conversion means that one of the tests fails. Until we get symbolic floating point, this will have to do. * Docstrings for platforms/wasm.py * Docstrings for ManticoreWASM * Add docs for the module structure * Add WASM to RTD * missing docstring for Module itself * Fix sphinx errors * Bump RTD python version I'm sorry and I swear I'll fix it later * Reformat docstrings for sphinx * Pacify RTD by adding newlines before params * Missed a few * Document the types * Document executor * A few more type docstrings * Partial runtime_structure docs * Finish documenting runtime structure * Fix trailing whitespace * Add collatz conjecture example * Include undocumented members in RTD * Add a bunch of events * Appropriately connect event publishers * Generate useful testcases * Blacken * Attempt at 3.6 backporting * Optimize AtomicStack * Sort solve_n output in test_solve_n Very unclear why this is happening, but it's breaking a travis build https://travis-ci.com/trailofbits/manticore/jobs/246451527 * Roll back to trusty? Unsure if this is what's causing the EVM issues * Create custom trap types * Lazily evaluate overflows May need to revert this if it slows down the Travis tests. It's 0.7% slower in the example I'm looking at, but that may not carry over. * Blacken * Address Dominik's feedback, remove stale TODOs * Expand & Test Examples * Fix relative path * Fix relative path? * capitalize Path * Fix relative path for real * Blacken... * Test finalize * Add supplemental tests for coverage * Use dedicated helper for store access * Handle quoted strings in imported module names * Allow WASMWorld to hold multiple modules Necessary for getting imports/exports to work, but still needs some changes before it passes the tests. * Actually use export maps * Fix most of the control flow issues with import tests * Use available cores for test generation * Escape module name * Don't reinit modules that have already been initialized * Use addresses for imports instead of copying * Fix removed timeout argument * Interleave registration and aliases * Fix broken "None" check for address * Blacken * Make manual exports work with address syntax * Import all registered modules Only necessary for elem, but it's tricky to make changes just for one test, so *shrug emoji* * Remove stringified annotations Turns out those only work in the same file... * Fix easy type issues in all but runtime structure * Fix easy type issues in runtime_structure * Fix* everything but imports * Blacken * Blacken 2 * Typo * Merge module structure and runtime structure * Fix instance vs type confusion * Fix mypy and concrete tests Still an issue with the symbolic tests * Still generate symbolic tests though I keep forgetting not to commit that file... * Attempt to fix env for symbolic tests * Blacken/mypy * Fix missing supplemental environment variables arg * Fix docstrings for new import style * CC * Bump timeout duration to 70 minutes I don't like it, but adding more jobs to Travis isn't going to make our builds any faster * Fix pycharm type, import, and docstring errors * Explain type: ignore * Missed two type:ignore's * Fix CLI so it doesn't throw up on arbitrary modules --- .travis.yml | 5 +- docs/index.rst | 1 + docs/wasm.rst | 42 + examples/wasm/collatz/collatz.c | 15 + examples/wasm/collatz/collatz.py | 145 ++ examples/wasm/collatz/collatz.wasm | Bin 0 -> 268 bytes examples/wasm/collatz/collatz.wat | 116 ++ manticore/__main__.py | 3 + manticore/core/manticore.py | 2 +- manticore/core/smtlib/operators.py | 2 + manticore/platforms/wasm.py | 369 +++++ manticore/utils/helpers.py | 13 +- manticore/utils/log.py | 3 +- manticore/wasm/__init__.py | 1 + manticore/wasm/cli.py | 30 + manticore/wasm/executor.py | 1575 ++++++++++++++++++++ manticore/wasm/manticore.py | 231 +++ manticore/wasm/state.py | 27 + manticore/wasm/structure.py | 1712 ++++++++++++++++++++++ manticore/wasm/types.py | 474 ++++++ mypy.ini | 3 + readthedocs.yml | 2 +- scripts/travis_test.sh | 16 +- setup.py | 10 +- tests/native/test_state.py | 2 +- tests/wasm/generate_tests.sh | 44 + tests/wasm/json2mc.py | 166 +++ tests/wasm/json2smc.py | 162 ++ tests/wasm/skipped_test_sets | 7 + tests/wasm/symbolic_test_template.jinja2 | 139 ++ tests/wasm/test_examples.py | 93 ++ tests/wasm/test_stack_supplemental.py | 113 ++ tests/wasm/test_template.jinja2 | 121 ++ 33 files changed, 5632 insertions(+), 12 deletions(-) create mode 100644 docs/wasm.rst create mode 100644 examples/wasm/collatz/collatz.c create mode 100644 examples/wasm/collatz/collatz.py create mode 100644 examples/wasm/collatz/collatz.wasm create mode 100644 examples/wasm/collatz/collatz.wat create mode 100644 manticore/platforms/wasm.py create mode 100644 manticore/wasm/__init__.py create mode 100644 manticore/wasm/cli.py create mode 100644 manticore/wasm/executor.py create mode 100644 manticore/wasm/manticore.py create mode 100644 manticore/wasm/state.py create mode 100644 manticore/wasm/structure.py create mode 100644 manticore/wasm/types.py create mode 100755 tests/wasm/generate_tests.sh create mode 100644 tests/wasm/json2mc.py create mode 100644 tests/wasm/json2smc.py create mode 100644 tests/wasm/skipped_test_sets create mode 100644 tests/wasm/symbolic_test_template.jinja2 create mode 100644 tests/wasm/test_examples.py create mode 100644 tests/wasm/test_stack_supplemental.py create mode 100644 tests/wasm/test_template.jinja2 diff --git a/.travis.yml b/.travis.yml index be87845b..ffbc37b1 100644 --- a/.travis.yml +++ b/.travis.yml @@ -15,13 +15,14 @@ stages: env: global: - CC_TEST_REPORTER_ID=db72f1ed59628c16eb0c00cbcd629c4c71f68aa1892ef42d18c7c2b8326f460a - - JOB_COUNT=4 # Four jobs generate test coverage: ethereum, ethereum_vm, native, and other + - JOB_COUNT=5 # Five jobs generate test coverage: ethereum, ethereum_vm, native, wasm, and other - PYTHONWARNINGS="default::ResourceWarning" # Enable ResourceWarnings matrix: - TEST_TYPE=examples - TEST_TYPE=ethereum - TEST_TYPE=ethereum_vm - TEST_TYPE=native + - TEST_TYPE=wasm - TEST_TYPE=other branches: @@ -61,7 +62,7 @@ install: - scripts/travis_install.sh $TEST_TYPE script: - - travis_wait 60 scripts/travis_test.sh $TEST_TYPE + - travis_wait 70 scripts/travis_test.sh $TEST_TYPE after_success: - ./cc-test-reporter format-coverage -t coverage.py -o "coverage/codeclimate.$TEST_TYPE.json" diff --git a/docs/index.rst b/docs/index.rst index 5aa9194e..eedbff96 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -14,6 +14,7 @@ Manticore is a symbolic execution tool for analysis of binaries and smart contra states evm native + wasm plugins gotchas diff --git a/docs/wasm.rst b/docs/wasm.rst new file mode 100644 index 00000000..5e9e4f3d --- /dev/null +++ b/docs/wasm.rst @@ -0,0 +1,42 @@ +Web Assembly +------------ + + +ManticoreWASM +^^^^^^^^^^^^^ + +.. automodule:: manticore.wasm.manticore + :members: + :undoc-members: + + +WASM World +^^^^^^^^^^ + +.. automodule:: manticore.platforms.wasm + :members: + :undoc-members: + + +Executor +^^^^^^^^ + +.. automodule:: manticore.wasm.executor + :members: + :undoc-members: + + +Module Structure +^^^^^^^^^^^^^^^^^ + +.. automodule:: manticore.wasm.structure + :members: + :undoc-members: + + +Types +^^^^^ + +.. automodule:: manticore.wasm.types + :members: + :undoc-members: diff --git a/examples/wasm/collatz/collatz.c b/examples/wasm/collatz/collatz.c new file mode 100644 index 00000000..0cf5cb58 --- /dev/null +++ b/examples/wasm/collatz/collatz.c @@ -0,0 +1,15 @@ +int collatz(int x){ + if (x <= 1){ + return 0; + } + if (x % 2 == 0){ + return collatz(x / 2) + 1; + } + else{ + return collatz(3 * x + 1) + 1; + } +} + +int main() { + return collatz(getchar(">")); +} \ No newline at end of file diff --git a/examples/wasm/collatz/collatz.py b/examples/wasm/collatz/collatz.py new file mode 100644 index 00000000..280d8257 --- /dev/null +++ b/examples/wasm/collatz/collatz.py @@ -0,0 +1,145 @@ +""" +Three different ways of evaluating the Collatz conjecture. + +Example 1: Pass a symbolic argument to the `collatz` function +Example 2: Pass a symbolic version of `getchar` as an imported function +Example 3: Concretely evaluate `collatz(1337)` and count the instructions executed + +See: examples/collatz.c +""" + +from manticore.wasm import ManticoreWASM +from manticore.wasm.types import I32 +from manticore.core.plugin import Plugin +from manticore.utils.log import set_verbosity + + +print( + """ + +============ Example 1 ============ +""" +) + +m = ManticoreWASM("collatz.wasm") +set_verbosity(2) + + +def arg_gen(state): + # Generate a symbolic argument to pass to the collatz function. + # Possible values: 4, 6, 8 + arg = state.new_symbolic_value(32, "collatz_arg") + state.constrain(arg > 3) + state.constrain(arg < 9) + state.constrain(arg % 2 == 0) + return [arg] + + +# Set up Manticore to run the collatz function with the given argument generator. +# We use an argument generator function instead of a list of arguments because Manticore +# might have multiple states waiting to begin execution, and we can conveniently map a +# generator function over all the ready states and get access to their respective +# constraint sets. +m.invoke("collatz", arg_gen) + +# Run the collatz function +m.run() + +# Manually collect return values +for idx, val_list in enumerate(m.collect_returns()): + print("State", idx, "::", val_list[0]) + +# Finalize the run (dump testcases) +m.finalize() + + +print( + """ + +============ Example 2 ============ +""" +) + + +def getchar(constraints, _addr): + """ + Stub implementation of the getchar function. All WASM cares about is that it accepts the right + number of arguments and returns the correct type. All _we_ care about is that it returns a symbolic + value, for which Manticore will produce all possible outputs. + + :param constraints: The current constraint set + :param _addr: Memory index of the string that gets printed by getchar + :return: A symbolic value of the interval [1, 7] + """ + res = constraints.new_bitvec(32, "getchar_res") + constraints.add(res > 0) + constraints.add(res < 8) + return [res] + + +# Pass our symbolic implementation of the `getchar` function into the WASM environment +# as an import. +m = ManticoreWASM("collatz.wasm", env={"getchar": getchar}) + +# Invoke the main function, which will call getchar +m.invoke("main") + +# Run the example +m.run() + +# Manually collect return values +for idx, val_list in enumerate(m.collect_returns()): + print("State", idx, "::", val_list[0]) + +# Finalize the run (dump testcases) +m.finalize() + + +print( + """ + +============ Example 3 ============ +""" +) + + +class CounterPlugin(Plugin): + """ + A plugin that counts the number of times each instruction occurs + """ + + def did_execute_instruction_callback(self, state, instruction): + with self.locked_context("counter", dict) as ctx: + val = ctx.setdefault(instruction.mnemonic, 0) + ctx[instruction.mnemonic] = val + 1 + + def did_terminate_state_callback(self, state, *args): + insn_sum = 0 + with self.locked_context("counter") as ctx: + for mnemonic, count in sorted(ctx.items(), key=lambda x: x[1], reverse=True): + print("{: <10} {: >4}".format(mnemonic, count)) + insn_sum += count + print(insn_sum, "instructions executed") + + +def arg_gen(_state): + return [I32(1337)] + + +m = ManticoreWASM("collatz.wasm") + +# Registering the plugin connects its callbacks to the correct events +m.register_plugin(CounterPlugin()) + +# Invoke `collatz(1337)` +m.invoke("collatz", arg_gen) + +# Run the collatz function +m.run() + +# Manually collect return values +for idx, val_list in enumerate(m.collect_returns()): + print("State", idx, "::", val_list[0]) + +# Finalize the run (dump testcases) +m.finalize() diff --git a/examples/wasm/collatz/collatz.wasm b/examples/wasm/collatz/collatz.wasm new file mode 100644 index 0000000000000000000000000000000000000000..0f1a8ad3927d210675eda3470f331a73af0cebbe GIT binary patch literal 268 zcmb7+OA3Ne7=_RIErl+D^Cs3p!aIvrp@{TA?Il7@Gzy9)EugJ5XldPhX#-9E^PdMF z(nCoAd~{t0Nx(K?%T}J&)61(SSmbrKO!vlJ+=%F1UAqPPE+XikZG_-u#q-O&-0Y8n zAlnp0TA#pPnXW3x;AV!9w*#=%7*pa1T4qC7\00") + (export "memory" (memory $0)) + (export "collatz" (func $collatz)) + (export "main" (func $main)) + (func $collatz (; 1 ;) (param $0 i32) (result i32) + (local $1 i32) + (set_local $1 + (i32.const 0) + ) + (block $label$0 + (br_if $label$0 + (i32.lt_s + (get_local $0) + (i32.const 2) + ) + ) + (set_local $1 + (i32.const 0) + ) + (loop $label$1 + (set_local $1 + (i32.add + (get_local $1) + (i32.const 1) + ) + ) + (br_if $label$1 + (i32.gt_s + (tee_local $0 + (select + (i32.add + (i32.mul + (get_local $0) + (i32.const 3) + ) + (i32.const 1) + ) + (i32.shr_u + (get_local $0) + (i32.const 1) + ) + (i32.and + (get_local $0) + (i32.const 1) + ) + ) + ) + (i32.const 1) + ) + ) + ) + ) + (get_local $1) + ) + (func $main (; 2 ;) (result i32) + (local $0 i32) + (local $1 i32) + (set_local $1 + (i32.const 0) + ) + (block $label$0 + (br_if $label$0 + (i32.lt_s + (tee_local $0 + (call $getchar + (i32.const 16) + ) + ) + (i32.const 2) + ) + ) + (set_local $1 + (i32.const 0) + ) + (loop $label$1 + (set_local $1 + (i32.add + (get_local $1) + (i32.const 1) + ) + ) + (br_if $label$1 + (i32.gt_s + (tee_local $0 + (select + (i32.add + (i32.mul + (get_local $0) + (i32.const 3) + ) + (i32.const 1) + ) + (i32.shr_u + (get_local $0) + (i32.const 1) + ) + (i32.and + (get_local $0) + (i32.const 1) + ) + ) + ) + (i32.const 1) + ) + ) + ) + ) + (get_local $1) + ) +) \ No newline at end of file diff --git a/manticore/__main__.py b/manticore/__main__.py index bcfc7265..3e39ea3f 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -10,6 +10,7 @@ import pkg_resources from crytic_compile import is_supported, cryticparser from .core.manticore import ManticoreBase, set_verbosity from .ethereum.cli import ethereum_main +from .wasm.cli import wasm_main from .utils import config, log, install_helper consts = config.get_group("main") @@ -39,6 +40,8 @@ def main(): if args.argv[0].endswith(".sol") or is_supported(args.argv[0]): ethereum_main(args, logger) + elif args.argv[0].endswith(".wasm") or args.argv[0].endswith(".wat"): + wasm_main(args, logger) else: install_helper.ensure_native_deps() native_main(args, logger) diff --git a/manticore/core/manticore.py b/manticore/core/manticore.py index 27422328..35545f28 100644 --- a/manticore/core/manticore.py +++ b/manticore/core/manticore.py @@ -327,7 +327,7 @@ class ManticoreBase(Eventful): to the ready list. """ - assert isinstance(expression, Expression) + assert isinstance(expression, Expression), f"{type(expression)} is not an Expression" if setstate is None: diff --git a/manticore/core/smtlib/operators.py b/manticore/core/smtlib/operators.py index a051a3a5..cbc5e4e3 100644 --- a/manticore/core/smtlib/operators.py +++ b/manticore/core/smtlib/operators.py @@ -248,6 +248,8 @@ def SREM(a, b): return a.srem(b) elif isinstance(b, BitVec): return b.rsrem(a) + elif isinstance(a, int) and isinstance(b, int): + return a - int(a / b) * b return a % b diff --git a/manticore/platforms/wasm.py b/manticore/platforms/wasm.py new file mode 100644 index 00000000..52fd2c06 --- /dev/null +++ b/manticore/platforms/wasm.py @@ -0,0 +1,369 @@ +from .platform import Platform +from ..wasm.structure import ( + ModuleInstance, + Store, + FuncAddr, + HostFunc, + Stack, + ProtoFuncInst, + MemInst, + MemAddr, + GlobalInst, + GlobalAddr, + TableInst, + TableAddr, + ExternVal, + Module, +) +from ..wasm.types import Trap, TypeIdx, TableType, MemoryType, GlobalType, MissingExportException +from ..core.state import TerminateState +from ..core.smtlib import ConstraintSet +from functools import partial +import typing +import logging +import os + +logger = logging.getLogger(__name__) +# logger.setLevel(logging.DEBUG) + + +def stub(arity, _constraints, *args): + """Default function used for hostfunc calls when a proper import wasn't provided """ + logger.info("Called stub function with args: %s", args) + return [0 for _ in range(arity)] + + +class WASMWorld(Platform): + """Manages global environment for a WASM state. Analagous to EVMWorld.""" + + def __init__(self, filename, name="self", **kwargs): + """ + :param filename: The WASM module to execute + :param kwargs: Accepts "constraints" to pass in an initial ConstraintSet + """ + super().__init__(filename, **kwargs) + #: Initial set of constraints + self.constraints = kwargs.get("constraints", ConstraintSet()) + #: Prevents users from calling run without instantiating the module + self.instantiated = [] + #: Backing store for functions, memories, tables, and globals + self.store = Store() + + self.modules = [] + self.module_names = {} + self.manual_exports = {} + self.default_module = name + self.register_module(name, filename) + + #: Stores numeric values, branch labels, and execution frames + self.stack = Stack() + + self.forward_events_from(self.stack) + self.forward_events_from(self.instance) + self.forward_events_from(self.instance.executor) + + def __getstate__(self): + state = super().__getstate__() + state["modules"] = self.modules + state["store"] = self.store + state["stack"] = self.stack + state["constraints"] = self.constraints + state["instantiated"] = self.instantiated + state["module_names"] = self.module_names + state["default_module"] = self.default_module + state["manual_exports"] = self.manual_exports + return state + + def __setstate__(self, state): + self.modules = state["modules"] + self.store = state["store"] + self.stack = state["stack"] + self.constraints = state["constraints"] + self.instantiated = state["instantiated"] + self.module_names = state["module_names"] + self.default_module = state["default_module"] + self.manual_exports = state["manual_exports"] + self.forward_events_from(self.stack) + self.forward_events_from(self.instance) + self.forward_events_from(self.instance.executor) + super().__setstate__(state) + + @property + def instance(self) -> ModuleInstance: + """ + :return: the ModuleInstance for the first module registered + """ + return self.modules[self.module_names[self.default_module]][1] + + @property + def module(self) -> Module: + """ + :return: The first module registered + """ + return self.modules[self.module_names[self.default_module]][0] + + def register_module(self, name, filename_or_alias): + """ + Provide an explicit path to a WASM module so the importer will know where to find it + + :param name: Module name to register the module under + :param filename_or_alias: Name of the .wasm file that module lives in + :return: + """ + if filename_or_alias in self.module_names: + self.module_names[name] = self.module_names[filename_or_alias] + if name not in self.module_names: + self.modules.append((Module.load(filename_or_alias), ModuleInstance(self.constraints))) + self.module_names[name] = len(self.modules) - 1 + self.instantiated.append(False) + + def set_env( + self, + exports: typing.Dict[str, typing.Union[ProtoFuncInst, TableInst, MemInst, GlobalInst]], + mod_name="env", + ): + """ + Manually insert exports into the global environment + + :param exports: Dict mapping names to functions/tables/globals/memories + :param mod_name: The name of the module these exports should fall under + """ + self.manual_exports.setdefault(mod_name, {}).update(exports) + + def import_module(self, module_name, exec_start, stub_missing): + """ + Collect all of the imports for the given module and instantiate it + + :param module_name: module to import + :param exec_start: whether to run the start functions automatically + :param stub_missing: whether to replace missing imports with stubs + :return: None + """ + search_paths = {"."} + # If the module isn't registered, look for it on the filesystem + if module_name not in self.module_names: + logger.debug("Module %s was not provided, attempting to load from disk", module_name) + for pth in search_paths: + possible_path = os.path.join(pth, module_name + ".wasm") + if os.path.isfile(possible_path): + self.register_module(module_name, possible_path) + break + else: + raise RuntimeError("Missing imported module: " + module_name) + + if self.instantiated[self.module_names[module_name]]: + return + + # Get the module and the instance from the world + module, instance = self.modules[self.module_names[module_name]] + + imports = self.get_module_imports(module, exec_start, stub_missing) + + instance.instantiate(self.store, module, imports, exec_start) + self.instantiated[self.module_names[module_name]] = True + logger.info("Imported %s", module_name) + + def _get_export_addr( + self, export_name, mod_name=None + ) -> typing.Optional[typing.Union[FuncAddr, TableAddr, MemAddr, GlobalAddr]]: + """ + Gets the address in the store of a given export + + :param export_name: Name of the export to look for + :param mod_name: Name of the module the export lives in + :return: The address of the export + """ + try: + if mod_name in self.module_names: # TODO - handle mod_name.export_name + return self.modules[self.module_names[mod_name]][1].get_export_address(export_name) + except MissingExportException as exc: + logger.error("Couldn't find export %s.%s", mod_name, exc.name) + return None + + def get_export( + self, export_name, mod_name=None + ) -> typing.Optional[typing.Union[ProtoFuncInst, TableInst, MemInst, GlobalInst]]: + """ + Gets the export _instance_ for a given export & module name + (basically just dereferences _get_export_addr into the store) + + :param export_name: Name of the export to look for + :param mod_name: Name of the module the export lives in + :return: The export itself + """ + mod_name = self.default_module if not mod_name else mod_name + if mod_name in self.manual_exports: + if export_name in self.manual_exports[mod_name]: + return self.manual_exports[mod_name][export_name] + addr = self._get_export_addr(export_name, mod_name) + if addr is not None: + if isinstance(addr, FuncAddr): + return self.store.funcs[addr] + if isinstance(addr, TableAddr): + return self.store.funcs[addr] + if isinstance(addr, MemAddr): + return self.store.mems[addr] + if isinstance(addr, GlobalAddr): + return self.store.globals[addr] + + return None + + def get_module_imports(self, module, exec_start, stub_missing) -> typing.List[ExternVal]: + """ + Builds the list of imports that should be passed to the given module upon instantiation + + :param module: The module to find the imports for + :param exec_start: Whether to execute the start function of the module + :param stub_missing: Whether to replace missing imports with stubs (TODO: symbolicate) + :return: List of addresses for the imports within the store + """ + imports: typing.List[ExternVal] = [] + for i in module.imports: + logger.info("Importing %s:%s", i.module, i.name) + if i.module not in self.module_names: # If the module isn't registered + if i.module not in self.manual_exports: # or manually provided + # Attempt to load it from the filesystem + self.import_module( + i.module, exec_start, stub_missing + ) # TODO - prevent circular imports + # If it's registered, but hasn't been imported yet, import it + elif not self.instantiated[self.module_names[i.module]]: + self.import_module(i.module, exec_start, stub_missing) + imported_version = self._get_export_addr(i.name, i.module) + if imported_version is None: + # check for manually provided version + # Possibly overwriting imported_version from an address to an instance here + imported_version = self.get_export(i.name, i.module) # type: ignore + if imported_version is None and not stub_missing: + raise RuntimeError(f"Could not find import {i.module}:{i.name}") + + if isinstance(imported_version, (FuncAddr, TableAddr, MemAddr, GlobalAddr)): + imports.append(imported_version) # TODO - Import type matching + else: + if isinstance(i.desc, TypeIdx): # Imported function + func_type = module.types[i.desc] + if i.module == "env" and imported_version: + if callable(imported_version): + imported_version = HostFunc(func_type, imported_version) + self.store.funcs.append( + imported_version + if imported_version + else HostFunc( + # mypy doesn't like that we're using a partial function instead of a proper function + func_type, + partial(stub, len(func_type.result_types)), # type: ignore + ) + ) + imports.append(FuncAddr(len(self.store.funcs) - 1)) + + elif isinstance(i.desc, TableType): + self.store.tables.append( + imported_version + if imported_version + else TableInst([None] * i.desc.limits.min, i.desc.limits.max) + ) + imports.append(TableAddr(len(self.store.tables) - 1)) + # Create an empty memory of the correct size and provide it as an import + elif isinstance(i.desc, MemoryType): + self.store.mems.append( + imported_version + if imported_version + else MemInst([0x0] * i.desc.min * 64 * 1024, i.desc.max) + ) + imports.append(MemAddr(len(self.store.mems) - 1)) + # Create a global and set its value to 0. + elif isinstance(i.desc, GlobalType): + self.store.globals.append( + imported_version + if imported_version + else GlobalInst(i.desc.value(0), i.desc.mut) + ) + imports.append(GlobalAddr(len(self.store.globals) - 1)) + else: + raise RuntimeError(f"Don't know how to handle imports of type {type(i.desc)}") + + return imports + + def instantiate( + self, + env_import_dict: typing.Dict[ + str, typing.Union[ProtoFuncInst, TableInst, MemInst, GlobalInst] + ], + supplemental_env: typing.Dict[ + str, typing.Dict[str, typing.Union[ProtoFuncInst, TableInst, MemInst, 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 + + :param env_import_dict: Dict mapping strings to functions. Functions should accept the current ConstraintSet as the first argument. + :param supplemental_env: Maps strings w/ module names to environment dicts using the same format as env_import_dict + :param exec_start: Whether or not to automatically execute the `start` function, if it is set. + :param stub_missing: Whether or not to replace missing imports with empty stubs + :return: None + """ + self.set_env(env_import_dict) + for k in supplemental_env: + self.set_env(supplemental_env[k], k) + self.import_module(self.default_module, exec_start, stub_missing) + + def invoke(self, name="main", argv=[], module=None): + """ + Sets up the WASMWorld to run the function specified by `name` when `ManticoreWASM.run` is called + + :param name: Name of the function to invoke + :param argv: List of arguments to pass to the function. Should typically be I32, I64, F32, or F64 + :param module: name of a module to call the function in (if not the default module) + :return: None + """ + module = self.default_module if module is None else module + instance = self.modules[self.module_names[module]][1] + instance.invoke_by_name(name, self.stack, self.store, list(argv)) + + def exec_for_test(self, 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. + + :param funcname: The name of the function to test + :param module: The name of the module to test the function in (if not the default module) + :return: The top n items from the stack where n is the expected number of return values from the function + """ + module = self.default_module if module is None else module + instance = self.modules[self.module_names[module]][1] + + # Grab the appropriate number of return values for the function being invoked + rets = 0 + for export in instance.exports: + if export.name == funcname and isinstance(export.value, FuncAddr): + rets = len(self.store.funcs[export.value].type.result_types) + + # Call exec_instruction until it returns false or throws an error + try: + while instance.exec_instruction(self.store, self.stack): + pass + # Return the top `rets` values from the stack + return [self.stack.pop() for _i in range(rets)] + except (Trap, NotImplementedError) as e: # Reset the internals if we have any problems + instance.reset_internal() + self.stack = Stack() + raise e + + def execute(self): + """ + 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. + """ + if not self.instantiated: + raise RuntimeError("Trying to execute before instantiation!") + try: + if not self.instance.exec_instruction(self.store, self.stack): + raise TerminateState(f"Execution returned {self.stack.peek()}") + except Trap as e: + raise TerminateState(f"Execution raised Trap: {str(e)}") diff --git a/manticore/utils/helpers.py b/manticore/utils/helpers.py index 7896c3a7..fb8bd5b1 100644 --- a/manticore/utils/helpers.py +++ b/manticore/utils/helpers.py @@ -28,10 +28,15 @@ class CacheDict(OrderedDict): super().__init__(*args, **kwargs) def __del__(self): - log = logging.getLogger(self.__class__.__name__) - log.debug( - f"DictCache: hits: {self._hits}, misses: {self._misses}, flushes: {self._flushes}, size: {self.__len__()}" - ) + try: + log = logging.getLogger(self.__class__.__name__) + log.debug( + f"DictCache: hits: {self._hits}, misses: {self._misses}, flushes: {self._flushes}, size: {self.__len__()}" + ) + except TypeError: + # Prevent "TypeError: attribute of type 'NoneType' is not callable" on line 32 + # TODO - figure out why this happens (I think it's only on concrete runs?) + pass def __setitem__(self, key, value): if len(self) > self._max_size: diff --git a/manticore/utils/log.py b/manticore/utils/log.py index f4af65fa..5a9240f1 100644 --- a/manticore/utils/log.py +++ b/manticore/utils/log.py @@ -100,11 +100,12 @@ def get_levels(): ("manticore.platforms.*", logging.DEBUG), ("manticore.ethereum", logging.DEBUG), ("manticore.core.plugin", logging.DEBUG), + ("manticore.wasm.*", logging.INFO), ("manticore.utils.emulate", logging.INFO), ("manticore.utils.helpers", logging.INFO), ], # 3 (-vv) - [("manticore.native.cpu.*", logging.DEBUG)], + [("manticore.native.cpu.*", logging.DEBUG), ("manticore.wasm.*", logging.DEBUG)], # 4 (-vvv) [ ("manticore.native.memory", logging.DEBUG), diff --git a/manticore/wasm/__init__.py b/manticore/wasm/__init__.py new file mode 100644 index 00000000..35a366e2 --- /dev/null +++ b/manticore/wasm/__init__.py @@ -0,0 +1 @@ +from .manticore import ManticoreWASM diff --git a/manticore/wasm/cli.py b/manticore/wasm/cli.py new file mode 100644 index 00000000..9b2d4880 --- /dev/null +++ b/manticore/wasm/cli.py @@ -0,0 +1,30 @@ +from .manticore import ManticoreWASM + +from ..core.plugin import Profiler +from ..utils import config + +consts = config.get_group("cli") +consts.add("target_func", default="main", description="WASM Function to execute") + + +def wasm_main(args, _logger): + + m = ManticoreWASM( + args.argv[0], + argv=args.argv[1:], + env={}, + exec_start=True, + workspace_url=args.workspace, + policy=args.policy, + ) + + if consts.profile: + profiler = Profiler() + m.register_plugin(profiler) + + m.default_invoke(func_name=consts.target_func) + + with m.kill_timeout(): + m.run() + + m.finalize() diff --git a/manticore/wasm/executor.py b/manticore/wasm/executor.py new file mode 100644 index 00000000..cda8a2bd --- /dev/null +++ b/manticore/wasm/executor.py @@ -0,0 +1,1575 @@ +# from ..utils.event import Eventful +from wasm.immtypes import ( + LocalVarXsImm, + GlobalVarXsImm, + MemoryImm, + CurGrowMemImm, + I32ConstImm, + I64ConstImm, + F32ConstImm, + F64ConstImm, +) +import struct +from ctypes import c_int32 +from .types import ( + I32, + I64, + F32, + F64, + Value_t, + UnreachableInstructionTrap, + ConcretizeStack, + ZeroDivisionTrap, + OverflowDivisionTrap, + InvalidConversionTrap, + OutOfBoundsMemoryTrap, +) +from ..core.smtlib import Operators, BitVec, issymbolic +from ..utils.event import Eventful +from decimal import Decimal, InvalidOperation + +import operator +import math + + +class Executor(Eventful): + """ + 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 + """ + + _published_events = { + "write_memory", + "read_memory", + "set_global", + "read_global", + "set_local", + "read_local", + } + + def __init__(self, constraints, *args, **kwargs): + + self._mapping = { + 0x00: self.unreachable, + 0x01: self.nop, + 0x02: self.nop, # block + 0x03: self.nop, # loop + 0x04: self.nop, # if + 0x05: self.nop, # else + 0x0B: self.nop, # end + 0x0C: self.nop, # br + 0x0D: self.nop, # br_if + 0x0E: self.nop, # br_table + 0x0F: self.nop, # return + 0x10: self.nop, # call + 0x11: self.nop, # call_indirect + 0x1A: self.drop, + 0x1B: self.select, + 0x20: self.get_local, + 0x21: self.set_local, + 0x22: self.tee_local, + 0x23: self.get_global, + 0x24: self.set_global, + 0x28: self.i32_load, + 0x29: self.i64_load, + 0x2A: self.f32_load, + 0x2B: self.f64_load, + 0x2C: self.i32_load8_s, + 0x2D: self.i32_load8_u, + 0x2E: self.i32_load16_s, + 0x2F: self.i32_load16_u, + 0x30: self.i64_load8_s, + 0x31: self.i64_load8_u, + 0x32: self.i64_load16_s, + 0x33: self.i64_load16_u, + 0x34: self.i64_load32_s, + 0x35: self.i64_load32_u, + 0x36: self.i32_store, + 0x37: self.i64_store, + 0x38: self.f32_store, + 0x39: self.f64_store, + 0x3A: self.i32_store8, + 0x3B: self.i32_store16, + 0x3C: self.i64_store8, + 0x3D: self.i64_store16, + 0x3E: self.i64_store32, + 0x3F: self.current_memory, + 0x40: self.grow_memory, + 0x41: self.i32_const, + 0x42: self.i64_const, + 0x43: self.f32_const, + 0x44: self.f64_const, + 0x45: self.i32_eqz, + 0x46: self.i32_eq, + 0x47: self.i32_ne, + 0x48: self.i32_lt_s, + 0x49: self.i32_lt_u, + 0x4A: self.i32_gt_s, + 0x4B: self.i32_gt_u, + 0x4C: self.i32_le_s, + 0x4D: self.i32_le_u, + 0x4E: self.i32_ge_s, + 0x4F: self.i32_ge_u, + 0x50: self.i64_eqz, + 0x51: self.i64_eq, + 0x52: self.i64_ne, + 0x53: self.i64_lt_s, + 0x54: self.i64_lt_u, + 0x55: self.i64_gt_s, + 0x56: self.i64_gt_u, + 0x57: self.i64_le_s, + 0x58: self.i64_le_u, + 0x59: self.i64_ge_s, + 0x5A: self.i64_ge_u, + 0x5B: self.f32_eq, + 0x5C: self.f32_ne, + 0x5D: self.f32_lt, + 0x5E: self.f32_gt, + 0x5F: self.f32_le, + 0x60: self.f32_ge, + 0x61: self.f64_eq, + 0x62: self.f64_ne, + 0x63: self.f64_lt, + 0x64: self.f64_gt, + 0x65: self.f64_le, + 0x66: self.f64_ge, + 0x67: self.i32_clz, + 0x68: self.i32_ctz, + 0x69: self.i32_popcnt, + 0x6A: self.i32_add, + 0x6B: self.i32_sub, + 0x6C: self.i32_mul, + 0x6D: self.i32_div_s, + 0x6E: self.i32_div_u, + 0x6F: self.i32_rem_s, + 0x70: self.i32_rem_u, + 0x71: self.i32_and, + 0x72: self.i32_or, + 0x73: self.i32_xor, + 0x74: self.i32_shl, + 0x75: self.i32_shr_s, + 0x76: self.i32_shr_u, + 0x77: self.i32_rotl, + 0x78: self.i32_rotr, + 0x79: self.i64_clz, + 0x7A: self.i64_ctz, + 0x7B: self.i64_popcnt, + 0x7C: self.i64_add, + 0x7D: self.i64_sub, + 0x7E: self.i64_mul, + 0x7F: self.i64_div_s, + 0x80: self.i64_div_u, + 0x81: self.i64_rem_s, + 0x82: self.i64_rem_u, + 0x83: self.i64_and, + 0x84: self.i64_or, + 0x85: self.i64_xor, + 0x86: self.i64_shl, + 0x87: self.i64_shr_s, + 0x88: self.i64_shr_u, + 0x89: self.i64_rotl, + 0x8A: self.i64_rotr, + 0x8B: self.f32_abs, + 0x8C: self.f32_neg, + 0x8D: self.f32_ceil, + 0x8E: self.f32_floor, + 0x8F: self.f32_trunc, + 0x90: self.f32_nearest, + 0x91: self.f32_sqrt, + 0x92: self.f32_add, + 0x93: self.f32_sub, + 0x94: self.f32_mul, + 0x95: self.f32_div, + 0x96: self.f32_min, + 0x97: self.f32_max, + 0x98: self.f32_copysign, + 0x99: self.f64_abs, + 0x9A: self.f64_neg, + 0x9B: self.f64_ceil, + 0x9C: self.f64_floor, + 0x9D: self.f64_trunc, + 0x9E: self.f64_nearest, + 0x9F: self.f64_sqrt, + 0xA0: self.f64_add, + 0xA1: self.f64_sub, + 0xA2: self.f64_mul, + 0xA3: self.f64_div, + 0xA4: self.f64_min, + 0xA5: self.f64_max, + 0xA6: self.f64_copysign, + 0xA7: self.i32_wrap_i64, + 0xA8: self.i32_trunc_s_f32, + 0xA9: self.i32_trunc_u_f32, + 0xAA: self.i32_trunc_s_f64, + 0xAB: self.i32_trunc_u_f64, + 0xAC: self.i64_extend_s_i32, + 0xAD: self.i64_extend_u_i32, + 0xAE: self.i64_trunc_s_f32, + 0xAF: self.i64_trunc_u_f32, + 0xB0: self.i64_trunc_s_f64, + 0xB1: self.i64_trunc_u_f64, + 0xB2: self.f32_convert_s_i32, + 0xB3: self.f32_convert_u_i32, + 0xB4: self.f32_convert_s_i64, + 0xB5: self.f32_convert_u_i64, + 0xB6: self.f32_demote_f64, + 0xB7: self.f64_convert_s_i32, + 0xB8: self.f64_convert_u_i32, + 0xB9: self.f64_convert_s_i64, + 0xBA: self.f64_convert_u_i64, + 0xBB: self.f64_promote_f32, + 0xBC: self.i32_reinterpret_f32, + 0xBD: self.i64_reinterpret_f64, + 0xBE: self.f32_reinterpret_i32, + 0xBF: self.f64_reinterpret_i64, + } + + #: Constraint set to use for checking overflows and boundary conditions + self.constraints = constraints + + self.zero_div = False + self.overflow = False + + super().__init__() + + def __getstate__(self): + state = super().__getstate__() + state["mapping"] = self._mapping + state["constraints"] = self.constraints + state["zero_div"] = self.zero_div + state["overflow"] = self.overflow + return state + + def __setstate__(self, state): + self._mapping = state["mapping"] + self.constraints = state["constraints"] + self.zero_div = state["zero_div"] + self.overflow = state["overflow"] + super().__setstate__(state) + + def check_overflow(self, expression) -> bool: + if issymbolic(expression): + self.overflow = Operators.OR(self.overflow, expression) + return False + return expression + + def check_zero_div(self, expression) -> bool: + if issymbolic(expression): + self.zero_div = Operators.OR(self.zero_div, expression) + return False + return expression + + def dispatch(self, inst, store, stack): + """ + Selects the correct semantics for the given instruction, and executes them + + :param inst: the Instruction to execute + :param store: the current Store + :param stack: the current Stack + :return: the result of the semantic function, which is (probably) always None + """ + opcode = inst.opcode + assert opcode in self._mapping + func = self._mapping[opcode] + try: + if inst.imm: + return func(store, stack, inst.imm) + else: + return func(store, stack) + except (ZeroDivisionError, InvalidOperation): + raise ZeroDivisionTrap() + + def unreachable(self, store, stack): + raise UnreachableInstructionTrap() + + def nop(self, store, stack): + pass + + def drop(self, store, stack): + stack.has_type_on_top(Value_t, 1) + stack.pop() + + def select(self, store, stack): + c = stack.pop() + v2 = stack.pop() + v1 = stack.pop() + assert isinstance(c, (I32, BitVec)), f"{type(c)} is not I32" + if not issymbolic(v2) and not issymbolic(v1): + assert type(v2) == type(v1), f"{type(v2)} is not the same as {type(v1)}" + + if issymbolic(c): + stack.push(Operators.ITEBV(getattr(v1, "size", 32), c != 0, v1, v2)) + else: + if c != 0: + stack.push(v1) + else: + stack.push(v2) + + def get_local(self, store, stack, imm: LocalVarXsImm): + f = stack.get_frame().frame + assert imm.local_index in range(len(f.locals)) + self._publish("will_get_local", imm.local_index) + stack.push(f.locals[imm.local_index]) + self._publish("did_get_local", imm.local_index, stack.peek()) + + def set_local(self, store, stack, imm: LocalVarXsImm): + f = stack.get_frame().frame + assert imm.local_index in range(len(f.locals)) + stack.has_type_on_top(Value_t, 1) + self._publish("will_set_local", imm.local_index, stack.peek()) + f.locals[imm.local_index] = stack.pop() + self._publish("did_set_local", imm.local_index, f.locals[imm.local_index]) + + def tee_local(self, store, stack, imm: LocalVarXsImm): + stack.has_type_on_top(Value_t, 1) + v = stack.pop() + stack.push(v) + stack.push(v) + self.set_local(store, stack, imm) + + def get_global(self, store, stack, imm: GlobalVarXsImm): + f = stack.get_frame().frame + assert imm.global_index in range(len(f.module.globaladdrs)) + a = f.module.globaladdrs[imm.global_index] + assert a in range(len(store.globals)) + glob = store.globals[a] + self._publish("will_get_global", imm.global_index, glob.value) + stack.push(glob.value) + self._publish("did_get_global", imm.global_index, stack.peek()) + + def set_global(self, store, stack, imm: GlobalVarXsImm): + f = stack.get_frame().frame + assert imm.global_index in range(len(f.module.globaladdrs)) + a = f.module.globaladdrs[imm.global_index] + assert a in range(len(store.globals)) + stack.has_type_on_top(Value_t, 1) + self._publish("did_set_global", imm.global_index, stack.peek()) + store.globals[a].value = stack.pop() + self._publish("did_set_global", imm.global_index, store.globals[a].value) + + def i32_load(self, store, stack, imm: MemoryImm): + f = stack.get_frame().frame + assert f.module.memaddrs + a = f.module.memaddrs[0] + assert a in range(len(store.mems)) + mem = store.mems[a] + stack.has_type_on_top(I32, 1) + i = stack.pop() + if issymbolic(i): + raise ConcretizeStack( + -1, I32, "Concretizing memory read", i + ) # TODO - Implement a symbolic memory model + ea = i + imm.offset + if (ea + 4) not in range(len(mem.data) + 1): + raise OutOfBoundsMemoryTrap(ea + 4) + self._publish("will_read_memory", ea, ea + 4) + c = Operators.CONCAT(32, *map(Operators.ORD, reversed(mem.data[ea : ea + 4]))) + stack.push(I32.cast(c)) + self._publish("did_read_memory", ea, stack.peek()) + + def i64_load(self, store, stack, imm: MemoryImm): + f = stack.get_frame().frame + assert f.module.memaddrs + a = f.module.memaddrs[0] + assert a in range(len(store.mems)) + mem = store.mems[a] + stack.has_type_on_top(I32, 1) + i = stack.pop() + if issymbolic(i): + raise ConcretizeStack( + -1, I32, "Concretizing memory read", i + ) # TODO - Implement a symbolic memory model + ea = i + imm.offset + if (ea + 8) not in range(len(mem.data) + 1): + raise OutOfBoundsMemoryTrap(ea + 8) + self._publish("will_read_memory", ea, ea + 8) + c = Operators.CONCAT(64, *map(Operators.ORD, reversed(mem.data[ea : ea + 8]))) + stack.push(I64.cast(c)) + self._publish("did_read_memory", ea, stack.peek()) + + def int_load(self, store, stack, imm: MemoryImm, ty: type, size: int, signed: bool): + assert ty in {I32, I64}, f"{type(ty)} is not an I32 or I64" + f = stack.get_frame().frame + assert f.module.memaddrs + a = f.module.memaddrs[0] + assert a in range(len(store.mems)) + mem = store.mems[a] + stack.has_type_on_top(I32, 1) + i = stack.pop() + if issymbolic(i): + raise ConcretizeStack( + -1, I32, "Concretizing memory read", i + ) # TODO - Implement a symbolic memory model + ea = i + imm.offset + if ea not in range(len(mem.data)): + raise OutOfBoundsMemoryTrap(ea) + if ea + (size // 8) not in range(len(mem.data) + 1): + raise OutOfBoundsMemoryTrap(ea + (size // 8)) + self._publish("will_read_memory", ea, ea + size // 8) + c = Operators.CONCAT(size, *map(Operators.ORD, reversed(mem.data[ea : ea + (size // 8)]))) + width = 32 if ty is I32 else 64 + if signed: + c = Operators.SEXTEND(c, size, width) + else: + c = Operators.ZEXTEND(c, width) + # Mypy can't figure out that that ty will definitely have a cast method, so we ignore the type + stack.push(ty.cast(c)) # type: ignore + self._publish("did_read_memory", ea, stack.peek()) + + def i32_load8_s(self, store, stack, imm: MemoryImm): + self.int_load(store, stack, imm, I32, 8, True) + + def i32_load8_u(self, store, stack, imm: MemoryImm): + self.int_load(store, stack, imm, I32, 8, False) + + def i32_load16_s(self, store, stack, imm: MemoryImm): + self.int_load(store, stack, imm, I32, 16, True) + + def i32_load16_u(self, store, stack, imm: MemoryImm): + self.int_load(store, stack, imm, I32, 16, False) + + def i64_load8_s(self, store, stack, imm: MemoryImm): + self.int_load(store, stack, imm, I64, 8, True) + + def i64_load8_u(self, store, stack, imm: MemoryImm): + self.int_load(store, stack, imm, I64, 8, False) + + def i64_load16_s(self, store, stack, imm: MemoryImm): + self.int_load(store, stack, imm, I64, 16, True) + + def i64_load16_u(self, store, stack, imm: MemoryImm): + self.int_load(store, stack, imm, I64, 16, False) + + def i64_load32_s(self, store, stack, imm: MemoryImm): + self.int_load(store, stack, imm, I64, 32, True) + + def i64_load32_u(self, store, stack, imm: MemoryImm): + self.int_load(store, stack, imm, I64, 32, False) + + def int_store(self, store, stack, imm: MemoryImm, ty: type, n=None): + assert ty in {I32, I64}, f"{type(ty)} is not an I32 or I64" + f = stack.get_frame().frame + assert f.module.memaddrs + a = f.module.memaddrs[0] + assert a in range(len(store.mems)) + mem = store.mems[a] + stack.has_type_on_top(ty, 1) + c = stack.pop() + stack.has_type_on_top(I32, 1) + i = stack.pop() + if issymbolic(i): + raise ConcretizeStack( + -2, I32, "Concretizing integer memory write", i + ) # TODO - Implement a symbolic memory model + ea = i + imm.offset + N = n if n else (32 if ty is I32 else 64) + if ea not in range(len(mem.data)): + raise OutOfBoundsMemoryTrap(ea) + if (ea + (N // 8)) not in range(len(mem.data) + 1): + raise OutOfBoundsMemoryTrap(ea + (N // 8)) + if n: + b = [ + Operators.CHR(Operators.EXTRACT(c % 2 ** N, offset, 8)) for offset in range(0, N, 8) + ] + else: + b = [Operators.CHR(Operators.EXTRACT(c, offset, 8)) for offset in range(0, N, 8)] + + self._publish("will_write_memory", ea, ea + len(b), b) + for idx, v in enumerate(b): + mem.data[ea + idx] = v + self._publish("did_write_memory", ea, b) + + def i32_store(self, store, stack, imm: MemoryImm): + self.int_store(store, stack, imm, I32) + + def i64_store(self, store, stack, imm: MemoryImm): + self.int_store(store, stack, imm, I64) + + def i32_store8(self, store, stack, imm: MemoryImm): + self.int_store(store, stack, imm, I32, 8) + + def i32_store16(self, store, stack, imm: MemoryImm): + self.int_store(store, stack, imm, I32, 16) + + def i64_store8(self, store, stack, imm: MemoryImm): + self.int_store(store, stack, imm, I64, 8) + + def i64_store16(self, store, stack, imm: MemoryImm): + self.int_store(store, stack, imm, I64, 16) + + def i64_store32(self, store, stack, imm: MemoryImm): + self.int_store(store, stack, imm, I64, 32) + + def current_memory(self, store, stack, imm: CurGrowMemImm): + f = stack.get_frame().frame + assert f.module.memaddrs + a = f.module.memaddrs[0] + assert a in range(len(store.mems)) + mem = store.mems[a] + stack.push(I32(len(mem.data) // 65536)) + + def grow_memory(self, store, stack, imm: CurGrowMemImm): + f = stack.get_frame().frame + assert f.module.memaddrs + a = f.module.memaddrs[0] + assert a in range(len(store.mems)) + mem = store.mems[a] + sz = len(mem.data) // 65536 + stack.has_type_on_top(I32, 1) + if issymbolic(stack.peek()): + raise ConcretizeStack(-1, I32, "Concretizing memory grow operand", stack.peek()) + if mem.grow(stack.pop()): + stack.push(I32(sz)) + else: + stack.push(I32(-1)) + + def i32_const(self, store, stack, imm: I32ConstImm): + stack.push(I32.cast(imm.value)) + + def i64_const(self, store, stack, imm: I64ConstImm): + stack.push(I64.cast(imm.value)) + + def i32_eqz(self, store, stack): + stack.has_type_on_top(I32, 1) + c1 = stack.pop() + v = c1 == 0 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i32_eq(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + v = c2 == c1 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i32_ne(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + v = c2 != c1 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i32_lt_s(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + v = c1 < c2 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i32_lt_u(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + v = Operators.ULT(c1, c2) + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i32_gt_s(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + v = c1 > c2 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i32_gt_u(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + v = Operators.UGT(c1, c2) + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i32_le_s(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + v = c1 <= c2 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i32_le_u(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + v = Operators.ULE(c1, c2) + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i32_ge_s(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + v = c1 >= c2 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i32_ge_u(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + v = Operators.UGE(c1, c2) + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i64_eqz(self, store, stack): + stack.has_type_on_top(I64, 1) + c1 = stack.pop() + v = c1 == 0 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i64_eq(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + v = c2 == c1 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i64_ne(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + v = c2 != c1 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i64_lt_s(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + v = c1 < c2 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i64_lt_u(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + v = Operators.ULT(c1, c2) + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i64_gt_s(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + v = c1 > c2 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i64_gt_u(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + v = Operators.UGT(c1, c2) + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i64_le_s(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + v = c1 <= c2 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i64_le_u(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + v = Operators.ULE(c1, c2) + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i64_ge_s(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + v = c1 >= c2 + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i64_ge_u(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + v = Operators.UGE(c1, c2) + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(I32.cast(I32(1) if v else I32(0))) + + def i32_clz(self, store, stack): + stack.has_type_on_top(I32, 1) + c1 = stack.pop() + flag = Operators.EXTRACT(c1, 31, 1) == 1 + res = 0 + for pos in range(1, 32): + res = Operators.ITEBV(32, flag, res, pos) + flag = Operators.OR(flag, Operators.EXTRACT(c1, 31 - pos, 1) == 1) + res = Operators.ITEBV(32, flag, res, 32) + stack.push(I32.cast(res)) + + def i32_ctz(self, store, stack): # Copied from x86 TZCNT + stack.has_type_on_top(I32, 1) + c1 = stack.pop() + flag = Operators.EXTRACT(c1, 0, 1) == 1 + res = 0 + for pos in range(1, 32): + res = Operators.ITEBV(32, flag, res, pos) + flag = Operators.OR(flag, Operators.EXTRACT(c1, pos, 1) == 1) + res = Operators.ITEBV(32, flag, res, 32) + stack.push(I32.cast(res)) + + def i32_popcnt(self, store, stack): + stack.has_type_on_top(I32, 1) + c1 = stack.pop() + flag = Operators.EXTRACT(c1, 0, 1) != 0 + res = 0 + for pos in range(1, 32): + res = Operators.ITEBV(32, flag, res + 1, res) + flag = Operators.EXTRACT(c1, pos, 1) != 0 + res = Operators.ITEBV(32, flag, res + 1, res) + stack.push(I32.cast(res)) + + def i32_add(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I32.cast((c2 + c1) % 2 ** 32)) + + def i32_sub(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I32.cast((c1 - c2 + 2 ** 32) % 2 ** 32)) + + def i32_mul(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I32.cast((c2 * c1) % 2 ** 32)) + + def i32_div_s(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + can_div_0 = c2 == 0 + if self.check_zero_div(can_div_0): + raise ZeroDivisionTrap() + res = Operators.SDIV(c1, c2) + can_overflow = res == 2 ** 31 + if self.check_overflow(can_overflow): + raise OverflowDivisionTrap() + stack.push(I32.cast(res)) + + def i32_div_u(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + can_div_0 = c2 == 0 + if self.check_zero_div(can_div_0): + raise ZeroDivisionTrap() + if not issymbolic(c2): + c2 = I32.to_unsigned(c2) + if not issymbolic(c1): + c1 = I32.to_unsigned(c1) + stack.push(I32.cast(Operators.UDIV(c1, c2))) + + def i32_rem_s(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + if self.check_zero_div(c2 == 0): + raise ZeroDivisionTrap() + stack.push(I32.cast(Operators.SREM(c1, c2))) + + def i32_rem_u(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + if not issymbolic(c2): + c2 = I32.to_unsigned(c2) + if not issymbolic(c1): + c1 = I32.to_unsigned(c1) + if self.check_zero_div(c2 == 0): + raise ZeroDivisionTrap() + stack.push(I32.cast(Operators.UREM(c1, c2))) + + def i32_and(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I32.cast(c2 & c1)) + + def i32_or(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I32.cast(c2 | c1)) + + def i32_xor(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I32.cast(c2 ^ c1)) + + def i32_shl(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I32.cast((c1 << (c2 % 32)) % 2 ** 32)) + + def i32_shr_s(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + k = c2 % 32 + stack.push(I32.cast(Operators.SAR(32, c1, k))) + + def i32_shr_u(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + if not issymbolic(c2): + c2 = I32.to_unsigned(c2) + if not issymbolic(c1): + c1 = I32.to_unsigned(c1) + stack.push(I32.cast(c1 >> (c2 % 32))) + + def i32_rotl(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + if not issymbolic(c1): + c1 = I32.to_unsigned(c1) + k = c2 % 32 + stack.push(I32.cast((c1 << k) | c1 >> (32 - k))) + + def i32_rotr(self, store, stack): + stack.has_type_on_top(I32, 2) + c2 = stack.pop() + c1 = stack.pop() + if not issymbolic(c1): + c1 = I32.to_unsigned(c1) + k = c2 % 32 + stack.push(I32.cast((c1 >> k) | c1 << (32 - k))) + + def i64_clz(self, store, stack): + stack.has_type_on_top(I64, 1) + c1 = stack.pop() + flag = Operators.EXTRACT(c1, 63, 1) == 1 + res = 0 + for pos in range(1, 64): + res = Operators.ITEBV(64, flag, res, pos) + flag = Operators.OR(flag, Operators.EXTRACT(c1, 63 - pos, 1) == 1) + + res = Operators.ITEBV(64, flag, res, 64) + stack.push(I64.cast(res)) + + def i64_ctz(self, store, stack): + stack.has_type_on_top(I64, 1) + c1 = stack.pop() + flag = Operators.EXTRACT(c1, 0, 1) == 1 + res = 0 + for pos in range(1, 64): + res = Operators.ITEBV(64, flag, res, pos) + flag = Operators.OR(flag, Operators.EXTRACT(c1, pos, 1) == 1) + res = Operators.ITEBV(64, flag, res, 64) + stack.push(I64.cast(res)) + + def i64_popcnt(self, store, stack): + stack.has_type_on_top(I64, 1) + c1 = stack.pop() + flag = Operators.EXTRACT(c1, 0, 1) != 0 + res = 0 + for pos in range(1, 64): + res = Operators.ITEBV(64, flag, res + 1, res) + flag = Operators.EXTRACT(c1, pos, 1) != 0 + res = Operators.ITEBV(64, flag, res + 1, res) + stack.push(I64.cast(res)) + + def i64_add(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I64.cast((c2 + c1) % 2 ** 64)) + + def i64_sub(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I64.cast((c1 - c2 + 2 ** 64) % 2 ** 64)) + + def i64_mul(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I64.cast((c2 * c1) % 2 ** 64)) + + def i64_div_s(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + can_div_0 = c2 == 0 + if self.check_zero_div(can_div_0): + raise ZeroDivisionTrap() + if issymbolic(c1) or issymbolic(c2): + res = Operators.SDIV(c1, c2) + else: + res = int(math.trunc(Decimal(c1) / Decimal(c2))) + can_overflow = res == 2 ** 63 + if self.check_overflow(can_overflow): + raise OverflowDivisionTrap() + stack.push(I64.cast(res)) + + def i64_div_u(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + can_div_0 = c2 == 0 + if self.check_zero_div(can_div_0): + raise ZeroDivisionTrap() + if not issymbolic(c2): + c2 = I64.to_unsigned(c2) + if not issymbolic(c1): + c1 = I64.to_unsigned(c1) + stack.push(I64.cast(Operators.UDIV(c1, c2))) + + def i64_rem_s(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + if self.check_zero_div(c2 == 0): + raise ZeroDivisionTrap() + if issymbolic(c1) or issymbolic(c2): + res = Operators.SREM(c1, c2) + else: + res = c1 - int(Decimal(c1) / Decimal(c2)) * c2 + stack.push(I64.cast(res)) + + def i64_rem_u(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + if not issymbolic(c2): + c2 = I64.to_unsigned(c2) + if not issymbolic(c1): + c1 = I64.to_unsigned(c1) + if self.check_zero_div(c2 == 0): + raise ZeroDivisionTrap() + stack.push(I64.cast(Operators.UREM(c1, c2))) + + def i64_and(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I64.cast(c2 & c1)) + + def i64_or(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I64.cast(c2 | c1)) + + def i64_xor(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I64.cast(c2 ^ c1)) + + def i64_shl(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + stack.push(I64.cast((c1 << (c2 % 64)) % 2 ** 64)) + + def i64_shr_s(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + k = c2 % 64 + stack.push(I64.cast(Operators.SAR(64, c1, k))) + + def i64_shr_u(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + if not issymbolic(c2): + c2 = I64.to_unsigned(c2) + if not issymbolic(c1): + c1 = I64.to_unsigned(c1) + stack.push(I64.cast(c1 >> (c2 % 64))) + + def i64_rotl(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + if not issymbolic(c1): + c1 = I64.to_unsigned(c1) + k = c2 % 64 + stack.push(I64.cast((c1 << k) | c1 >> (64 - k))) + + def i64_rotr(self, store, stack): + stack.has_type_on_top(I64, 2) + c2 = stack.pop() + c1 = stack.pop() + if not issymbolic(c1): + c1 = I64.to_unsigned(c1) + k = c2 % 64 + stack.push(I64.cast((c1 >> k) | c1 << (64 - k))) + + def i32_wrap_i64(self, store, stack): + stack.has_type_on_top(I64, 1) + c1: I64 = stack.pop() + c1 %= 2 ** 32 + c1 = Operators.EXTRACT(c1, 0, 32) + stack.push(I32.cast(c1)) + + def i32_trunc_s_f32(self, store, stack): + stack.has_type_on_top(F32, 1) + c1: F32 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, F32, "Concretizing for float->int conversion", c1) + if math.isnan(c1): + raise InvalidConversionTrap(I32, "NaN") + if math.isinf(c1): + raise InvalidConversionTrap(I32, "infinity") + if c1 >= 2 ** 31 or c1 <= -(2 ** 31) - 1: + raise InvalidConversionTrap(I32, c1) + stack.push(I32.cast(c1)) + + def i32_trunc_u_f32(self, store, stack): + stack.has_type_on_top(F32, 1) + c1: F32 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, F32, "Concretizing for float->int conversion", c1) + if math.isnan(c1): + raise InvalidConversionTrap(I32, "NaN") + if math.isinf(c1): + raise InvalidConversionTrap(I32, "infinity") + if c1 >= 2 ** 32 or c1 <= -1: + raise InvalidConversionTrap(I32, c1) + stack.push(I32.cast(c1)) + + def i32_trunc_s_f64(self, store, stack): + stack.has_type_on_top(F64, 1) + c1: F64 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, F64, "Concretizing for float->int conversion", c1) + if math.isnan(c1): + raise InvalidConversionTrap(I32, "NaN") + if math.isinf(c1): + raise InvalidConversionTrap(I32, "infinity") + if c1 >= 2 ** 31 or c1 <= -(2 ** 31) - 1: + raise InvalidConversionTrap(I32, c1) + stack.push(I32.cast(c1)) + + def i32_trunc_u_f64(self, store, stack): + stack.has_type_on_top(F64, 1) + c1: F64 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, F64, "Concretizing for float->int conversion", c1) + if math.isnan(c1): + raise InvalidConversionTrap(I32, "NaN") + if math.isinf(c1): + raise InvalidConversionTrap(I32, "infinity") + if c1 >= 2 ** 32 or c1 <= -1: + raise InvalidConversionTrap(I32, c1) + stack.push(I32.cast(c1)) + + def i64_extend_s_i32(self, store, stack): + stack.has_type_on_top(I32, 1) + c1: I32 = stack.pop() + stack.push(I64.cast(Operators.SEXTEND(c1, 32, 64))) + + def i64_extend_u_i32(self, store, stack): + stack.has_type_on_top(I32, 1) + c1: I32 = stack.pop() + if issymbolic( + c1 + ): # ZEXTEND doesn't have a concept of sized ints, so it will promote a negative I32 + # to a negative I64 with the same value. + stack.push(I64.cast(Operators.ZEXTEND(c1, 64))) + else: + stack.push(I64.cast(struct.unpack("q", bytes(c_int32(c1)) + b"\x00" * 4)[0])) + + def i64_trunc_s_f32(self, store, stack): + stack.has_type_on_top(F32, 1) + c1: F32 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, F32, "Concretizing float", c1) + if math.isnan(c1): + raise InvalidConversionTrap(I64, "NaN") + if math.isinf(c1): + raise InvalidConversionTrap(I64, "infinity") + if c1 >= 2 ** 63 or c1 <= -(2 ** 63) - 1: + raise InvalidConversionTrap(I64, c1) + stack.push(I64.cast(c1)) + + def i64_trunc_u_f32(self, store, stack): + stack.has_type_on_top(F32, 1) + c1: F32 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, F32, "Concretizing float", c1) + if math.isnan(c1): + raise InvalidConversionTrap(I64, "NaN") + if math.isinf(c1): + raise InvalidConversionTrap(I64, "infinity") + if c1 >= 2 ** 64 or c1 <= -1: + raise InvalidConversionTrap(I64, c1) + stack.push(I64.cast(c1)) + + def i64_trunc_s_f64(self, store, stack): + stack.has_type_on_top(F64, 1) + c1: F64 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, F64, "Concretizing float", c1) + if math.isnan(c1): + raise InvalidConversionTrap(I64, "NaN") + if math.isinf(c1): + raise InvalidConversionTrap(I64, "infinity") + if c1 >= 2 ** 63 or c1 <= -(2 ** 63) - 1: + raise InvalidConversionTrap(I64, c1) + stack.push(I64.cast(c1)) + + def i64_trunc_u_f64(self, store, stack): + stack.has_type_on_top(F64, 1) + c1: F64 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, F64, "Concretizing float", c1) + if math.isnan(c1): + raise InvalidConversionTrap(I64, "NaN") + if math.isinf(c1): + raise InvalidConversionTrap(I64, "infinity") + if c1 >= 2 ** 64 or c1 <= -1: + raise InvalidConversionTrap(I64, c1) + stack.push(I64.cast(c1)) + + def i32_reinterpret_f32(self, store, stack): + stack.has_type_on_top(F32, 1) + c1: F32 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, F32, "Concretizing float", c1) + c1 = struct.unpack("i", struct.pack("f", c1))[0] + stack.push(I32.cast(c1)) + + def i64_reinterpret_f64(self, store, stack): + stack.has_type_on_top(F64, 1) + c1: F64 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, F64, "Concretizing float", c1) + c1 = struct.unpack("q", struct.pack("d", c1))[0] + stack.push(I64.cast(c1)) + + ########################################################################################################### + # Floating point instructions# Floating point instructions + def float_load(self, store, stack, imm: MemoryImm, ty: type): + assert ty in {F32, F64}, f"{type(ty)} is not an F32 or F64" + size = 32 if ty == F32 else 64 + f = stack.get_frame().frame + a = f.module.memaddrs[0] + mem = store.mems[a] + stack.has_type_on_top(I32, 1) + i = stack.pop() + if issymbolic(i): + raise ConcretizeStack( + -1, I32, "Concretizing float memory read", i + ) # TODO - Implement a symbolic memory model + ea = i + imm.offset + if ea not in range(len(mem.data)): + raise OutOfBoundsMemoryTrap(ea) + if (ea + (size // 8)) not in range(len(mem.data) + 1): + raise OutOfBoundsMemoryTrap(ea + (size // 8)) + self._publish("will_read_memory", ea, ea + (size // 8)) + c = Operators.CONCAT(size, *map(Operators.ORD, reversed(mem.data[ea : ea + (size // 8)]))) + # Mypy can't figure out that that ty will definitely have a cast method, so we ignore the type + ret = ty.cast(c) # type: ignore + stack.push(ret) + self._publish("did_read_memory", ea, stack.peek()) + + def f32_load(self, store, stack, imm: MemoryImm): + return self.float_load(store, stack, imm, F32) + + def f64_load(self, store, stack, imm: MemoryImm): + return self.float_load(store, stack, imm, F64) + + def float_store(self, store, stack, imm: MemoryImm, ty: type, n=None): + f = stack.get_frame().frame + a = f.module.memaddrs[0] + mem = store.mems[a] + c = stack.pop() + i = stack.pop() + if issymbolic(i): + raise ConcretizeStack(-2, I32, "Concretizing memory address for float_store", i) + ea = i + imm.offset + if ty == F32: + size = 32 + else: + size = 64 + if ea not in range(len(mem.data)): + raise OutOfBoundsMemoryTrap(ea) + if (ea + (size // 8)) not in range(len(mem.data) + 1): + raise OutOfBoundsMemoryTrap(ea + (size // 8)) + if not issymbolic(c): + c = struct.unpack( + "i" if size == 32 else "q", struct.pack("f" if size == 32 else "d", c) + )[0] + b = [Operators.CHR(Operators.EXTRACT(c, offset, 8)) for offset in range(0, size, 8)] + self._publish("did_write_memory", ea, ea + len(b), b) + for idx, v in enumerate(b): + mem.data[ea + idx] = v + self._publish("did_write_memory", ea, b) + + def float_push_compare_return(self, stack, v, rettype=I32): + if issymbolic(v): + stack.push(Operators.ITEBV(32, v, I32(1), I32(0))) + else: + stack.push(rettype(v)) + + def f32_store(self, store, stack, imm: MemoryImm): + self.float_store(store, stack, imm, F32) + + def f64_store(self, store, stack, imm: MemoryImm): + self.float_store(store, stack, imm, F64) + + def f32_const(self, store, stack, imm: F32ConstImm): + stack.push(F32.cast(imm.value)) + + def f64_const(self, store, stack, imm: F64ConstImm): + stack.push(F64.cast(imm.value)) + + def f32_unary(self, store, stack, op, rettype: type = I32): + stack.has_type_on_top(F32, 1) + if issymbolic(stack.peek()): + raise ConcretizeStack(-1, F32, "Concretizing before float op", stack.peek()) + v1 = stack.pop() + v = op(v1) + self.float_push_compare_return(stack, v, rettype) + + def f32_binary(self, store, stack, op, rettype: type = I32): + stack.has_type_on_top(F32, 2) + if issymbolic(stack.peek()): + raise ConcretizeStack(-1, F32, "Concretizing before float op", stack.peek()) + v2 = stack.pop() + if issymbolic(stack.peek()): + raise ConcretizeStack(-2, F32, "Concretizing before float op", stack.peek()) + v1 = stack.pop() + v = op(v1, v2) + self.float_push_compare_return(stack, v, rettype) + + def f64_unary(self, store, stack, op, rettype: type = F64): + stack.has_type_on_top(F64, 1) + if issymbolic(stack.peek()): + raise ConcretizeStack(-1, F64, "Concretizing before float op", stack.peek()) + v1 = stack.pop() + v = op(v1) + self.float_push_compare_return(stack, v, rettype) + + def f64_binary(self, store, stack, op, rettype: type = I32): + stack.has_type_on_top(F64, 2) + if issymbolic(stack.peek()): + raise ConcretizeStack(-1, F64, "Concretizing before float op", stack.peek()) + v2 = stack.pop() + if issymbolic(stack.peek()): + raise ConcretizeStack(-2, F64, "Concretizing before float op", stack.peek()) + v1 = stack.pop() + v = op(v1, v2) + self.float_push_compare_return(stack, v, rettype) + + def f32_eq(self, store, stack): + return self.f32_binary(store, stack, operator.eq) + + def f32_ne(self, store, stack): + return self.f32_binary(store, stack, operator.ne) + + def f32_lt(self, store, stack): + return self.f32_binary(store, stack, operator.lt) + + def f32_gt(self, store, stack): + return self.f32_binary(store, stack, operator.gt) + + def f32_le(self, store, stack): + return self.f32_binary(store, stack, operator.le) + + def f32_ge(self, store, stack): + return self.f32_binary(store, stack, operator.ge) + + def f64_eq(self, store, stack): + return self.f64_binary(store, stack, operator.eq) + + def f64_ne(self, store, stack): + return self.f64_binary(store, stack, operator.ne) + + def f64_lt(self, store, stack): + return self.f64_binary(store, stack, operator.lt) + + def f64_gt(self, store, stack): + return self.f64_binary(store, stack, operator.gt) + + def f64_le(self, store, stack): + return self.f64_binary(store, stack, operator.le) + + def f64_ge(self, store, stack): + return self.f64_binary(store, stack, operator.ge) + + def f32_abs(self, store, stack): + return self.f32_unary(store, stack, operator.abs, F32) + + def f32_neg(self, store, stack): + return self.f32_unary(store, stack, operator.neg, F32) + + def f32_ceil(self, store, stack): + return self.f32_unary(store, stack, operator_ceil, F32) + + def f32_floor(self, store, stack): + return self.f32_unary(store, stack, operator_floor, F32) + + def f32_trunc(self, store, stack): + return self.f32_unary(store, stack, operator_trunc, F32) + + def f32_nearest(self, store, stack): + return self.f32_unary(store, stack, operator_nearest, F32) + + def f32_sqrt(self, store, stack): + return self.f32_unary(store, stack, math.sqrt, F32) + + def f32_add(self, store, stack): + return self.f32_binary(store, stack, operator.add, F32) + + def f32_sub(self, store, stack): + return self.f32_binary(store, stack, operator.sub, F32) + + def f32_mul(self, store, stack): + return self.f32_binary(store, stack, operator.mul, F32) + + def f32_div(self, store, stack): + return self.f32_binary(store, stack, operator_div, F32) + + def f32_min(self, store, stack): + return self.f32_binary(store, stack, operator_min, F32) + + def f32_max(self, store, stack): + return self.f32_binary(store, stack, operator_max, F32) + + def f32_copysign(self, store, stack): + return self.f32_binary(store, stack, math.copysign, F32) + + def f64_abs(self, store, stack): + return self.f64_unary(store, stack, operator.abs, F64) + + def f64_neg(self, store, stack): + return self.f64_unary(store, stack, operator.neg, F64) + + def f64_ceil(self, store, stack): + return self.f64_unary(store, stack, operator_ceil, F64) + + def f64_floor(self, store, stack): + return self.f64_unary(store, stack, operator_floor, F64) + + def f64_trunc(self, store, stack): + return self.f64_unary(store, stack, operator_trunc, F64) + + def f64_nearest(self, store, stack): + return self.f32_unary(store, stack, operator_nearest, F64) + + def f64_sqrt(self, store, stack): + return self.f64_unary(store, stack, math.sqrt, F64) + + def f64_add(self, store, stack): + return self.f64_binary(store, stack, operator.add, F64) + + def f64_sub(self, store, stack): + return self.f64_binary(store, stack, operator.sub, F64) + + def f64_mul(self, store, stack): + return self.f64_binary(store, stack, operator.mul, F64) + + def f64_div(self, store, stack): + return self.f64_binary(store, stack, operator_div, F64) + + def f64_min(self, store, stack): + return self.f64_binary(store, stack, operator_min, F64) + + def f64_max(self, store, stack): + return self.f64_binary(store, stack, operator_max, F64) + + def f64_copysign(self, store, stack): + return self.f64_binary(store, stack, math.copysign, F64) + + def f32_convert_s_i32(self, store, stack): + stack.has_type_on_top(I32, 1) + c1: I32 = stack.pop() + stack.push(F32.cast(float(c1))) + + def f32_convert_u_i32(self, store, stack): + stack.has_type_on_top(I32, 1) + c1: I32 = stack.pop() + stack.push(F32.cast(float(I32.to_unsigned(c1)))) + + def f32_convert_s_i64(self, store, stack): + stack.has_type_on_top(I64, 1) + c1: I64 = stack.pop() + stack.push(F32.cast(float(c1))) + + def f32_convert_u_i64(self, store, stack): + stack.has_type_on_top(I64, 1) + c1: I64 = stack.pop() + stack.push(F32.cast(float(I64.to_unsigned(c1)))) + + def f32_demote_f64(self, store, stack): + stack.has_type_on_top(F64, 1) + c1: F64 = stack.pop() + if math.isnan(c1) or math.isinf(c1) or c1 == 0.0 or c1 == -0.0: + stack.push(F32.cast(c1)) + return + raise NotImplementedError("f32_demote_f64") + c1 = struct.unpack("f", struct.pack("d", c1)[:4])[0] + stack.push(F32.cast(c1)) + + def f64_convert_s_i32(self, store, stack): + stack.has_type_on_top(I32, 1) + c1: I32 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, I32, "Concretizing int for float conversion", c1) + stack.push(F64.cast(float(c1))) + + def f64_convert_u_i32(self, store, stack): + stack.has_type_on_top(I32, 1) + c1: I32 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, I32, "Concretizing int for float conversion", c1) + stack.push(F64.cast(float(I32.to_unsigned(c1)))) + + def f64_convert_s_i64(self, store, stack): + stack.has_type_on_top(I64, 1) + c1: I64 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, I64, "Concretizing int for float conversion", c1) + stack.push(F64.cast(float(c1))) + + def f64_convert_u_i64(self, store, stack): + stack.has_type_on_top(I64, 1) + c1: I64 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, I64, "Concretizing int for float conversion", c1) + stack.push(F64.cast(float(I64.to_unsigned(c1)))) + + def f64_promote_f32(self, store, stack): + stack.has_type_on_top(F32, 1) + c1: F32 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, F32, "Concretizing F32 for F64 promotion", c1) + stack.push(F64.cast(c1)) + + def f32_reinterpret_i32(self, store, stack): + stack.has_type_on_top(I32, 1) + c1: I32 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, I32, "Concretizing int for float conversion", c1) + c1 = struct.unpack("f", struct.pack("i", c1))[0] + stack.push(F32.cast(c1)) + + def f64_reinterpret_i64(self, store, stack): + stack.has_type_on_top(I64, 1) + c1: I64 = stack.pop() + if issymbolic(c1): + raise ConcretizeStack(-1, I64, "Concretizing int for float conversion", c1) + c1 = struct.unpack("d", struct.pack("q", c1))[0] + stack.push(F64.cast(c1)) + + +################################################################################################ +# Unary and binary operators for floats that don't fit python +def operator_nearest(a): + if math.isnan(a) or math.isinf(a): + return a.integer + else: + return round(a) + + +def operator_trunc(a): + if math.isnan(a) or math.isinf(a): + return a.integer + else: + return math.trunc(a) + + +def operator_ceil(a): + if math.isnan(a) or math.isinf(a): + return a.integer + else: + return math.ceil(a) + + +def operator_floor(a): + if math.isnan(a) or math.isinf(a): + return a.integer + else: + return math.floor(a) + + +def operator_div(a, b): + if b == 0: + return math.inf + else: + return operator.truediv(a, b) + + +def operator_min(a, b): + return a if a < b else b + + +def operator_max(a, b): + return a if a > b else b diff --git a/manticore/wasm/manticore.py b/manticore/wasm/manticore.py new file mode 100644 index 00000000..dfb6e115 --- /dev/null +++ b/manticore/wasm/manticore.py @@ -0,0 +1,231 @@ +import logging +import os +import time +import typing + +from .state import State +from ..core.manticore import ManticoreBase +from ..core.smtlib import ConstraintSet, issymbolic, Z3Solver +from .types import I32, I64, F32, F64 +from .structure import FuncInst + +logger = logging.getLogger(__name__) + + +class ManticoreWASM(ManticoreBase): + """ + Manticore class for interacting with WASM, analagous to ManticoreNative or ManticoreEVM. + """ + + def __init__( + self, path_or_state, env={}, sup_env={}, workspace_url=None, policy="random", **kwargs + ): + """ + :param path_or_state: Path to binary or a state (object) to begin from. + :param env: Dict of imports to place under the "env" module + :param sup_env: Maps module names to import dicts (a la {"env":{}}) + """ + if isinstance(path_or_state, str): + if not os.path.isfile(path_or_state): + raise OSError(f"{path_or_state} is not an existing regular file") + initial_state = _make_initial_state(path_or_state, env, sup_env, **kwargs) + else: + initial_state = path_or_state + + super().__init__(initial_state, workspace_url=workspace_url, policy=policy, **kwargs) + + self.subscribe("will_terminate_state", self._terminate_state_callback) + + def run(self, timeout=None): + """ + Begins the Manticore run + + :param timeout: number of seconds after which to kill execution + """ + with self.locked_context() as context: + context["time_started"] = time.time() + + with self.kill_timeout(timeout): + super().run() + + def finalize(self): + """ + Finish a run and solve for test cases. + Calls save_run_data + """ + super().finalize() + self.save_run_data() + + def save_run_data(self): + super().save_run_data() + + time_ended = time.time() + + with self.locked_context() as context: + time_elapsed = time_ended - context["time_started"] + + logger.info("Total time: %s", time_elapsed) + + context["time_ended"] = time_ended + context["time_elapsed"] = time_elapsed + + @ManticoreBase.at_not_running + def invoke(self, name="main", argv_generator=lambda s: []): + """ + 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 + """ + for state in self.ready_states: + args = argv_generator(state) + logger.info("Invoking: %s(%s)", name, ", ".join(str(a) for a in args)) + state.platform.invoke(name=name, argv=args) + + @ManticoreBase.at_not_running + def default_invoke(self, 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 + """ + funcs = [func_name] + if "main" not in func_name: + funcs.append("main") + + state = next(self.ready_states) + for name in funcs: + func_inst: typing.Optional[FuncInst] = state.platform.get_export(name) + if isinstance(func_inst, FuncInst): + func_ty = func_inst.type + + args = [] + for idx, ty in enumerate(func_ty.param_types): + if ty in {I32, F32}: + args.append(state.new_symbolic_value(32, f"arg{idx}_{ty.__name__}")) + elif ty in {I64, F64}: + args.append(state.new_symbolic_value(64, f"arg{idx}_{ty.__name__}")) + + self.invoke(name=name, argv_generator=lambda s: args) + break + + @ManticoreBase.at_not_running + def collect_returns(self, n=1): + """ + Iterates over the terminated states and collects the top n values from the stack. + Generally only used for testing. + + :param n: Number of values to collect + :return: A list of list of lists. + > One list for each state + > One list for each n + > The output from solver.get_all_values + """ + outer = [] + for state in self.terminated_states: + inner = [] + p = state.platform + for _i in range(n): + ret = None + if not p.stack.empty(): + ret = p.stack.pop() + if issymbolic(ret): + if ret.size == 32: + inner.append( + list( + I32(a) # TODO - eventually we'll need to support floats as well. + for a in Z3Solver.instance().get_all_values(state.constraints, ret) + ) + ) + elif ret.size == 64: + inner.append( + list( + I64( + a + ) # TODO - that'll probably require us to subclass bitvecs into IxxBV and FxxBV + for a in Z3Solver.instance().get_all_values(state.constraints, ret) + ) + ) + else: + inner.append([ret]) + outer.append(inner) + return outer + + def _terminate_state_callback(self, state, e): + """ + Adds state to the wasm.saved_states list + + :param state: the terminated state + :param e: any exception raised + """ + with self.locked_context("wasm.saved_states", list) as saved_states: + saved_states.append(state.id) + + @ManticoreBase.at_not_running + def _reinit(self): + """ + Moves terminated states back into the ready states list. Only used for testing, may promote to + a part of the official API in the future. + """ + # If there are ready states still then it was a paused execution + assert not self._ready_states + assert not self._busy_states + + with self.locked_context("wasm.saved_states", list) as saved_states: + while saved_states: + state_id = saved_states.pop() + self._terminated_states.remove(state_id) + self._ready_states.append(state_id) + + def generate_testcase(self, state, message="test", name="test"): + testcase = super().generate_testcase(state, message) + self._output.save_input_symbols(testcase, state) + + with testcase.open_stream("stack") as stackf: + stackf.write(str(state.stack.data)) + + with testcase.open_stream("memory") as memoryf: + memoryf.write(str(state.mem.data)) + + term = getattr(state, "_terminated_by", None) + if term: + with testcase.open_stream("status") as summary: + summary.write(f"{str(term)}\n\n") + + +def _make_initial_state(binary_path, env={}, sup_env={}, **kwargs): + """ + Wraps _make_wasm_bin + + :param binary_path: filename of the wasm module + :param env: Import dict + :param sup_env: Maps module names to import dicts (a la {"env":{}}) + :param kwargs: + :return: initial state + """ + if binary_path.endswith(".wasm"): + return _make_wasm_bin(binary_path, env=env, sup_env=sup_env, **kwargs) + + +def _make_wasm_bin(program, env={}, sup_env={}, **kwargs) -> State: + """ + Returns an initial state for a binary WASM module + + :param program: filename of the wasm module + :param env: Import dict + :param sup_env: Maps module names to import dicts (a la {"env":{}}) + :return: initial state + """ + from ..platforms import wasm + + logger.info("Loading program %s", program) + + constraints = kwargs.get("constraints", ConstraintSet()) + platform = wasm.WASMWorld(program, constraints=constraints) + platform.instantiate( + env, + sup_env, + exec_start=kwargs.get("exec_start", False), + stub_missing=kwargs.get("stub_missing", True), + ) + initial_state = State(constraints, platform) + + return initial_state diff --git a/manticore/wasm/state.py b/manticore/wasm/state.py new file mode 100644 index 00000000..d959cf34 --- /dev/null +++ b/manticore/wasm/state.py @@ -0,0 +1,27 @@ +from ..core.state import StateBase + + +class State(StateBase): + @property + def stack(self): + """ + Current execution Stack + """ + return self._platform.stack + + @property + def store(self): + """ + Current execution Store + """ + return self._platform.store + + @property + def mem(self): + """ + The first memory in the current execution Store + """ + return self.store.mems[0] + + def execute(self): + return self._platform.execute() diff --git a/manticore/wasm/structure.py b/manticore/wasm/structure.py new file mode 100644 index 00000000..ba89d4c7 --- /dev/null +++ b/manticore/wasm/structure.py @@ -0,0 +1,1712 @@ +# from __future__ import annotations +import typing +import types +import logging +from dataclasses import dataclass +from .executor import Executor +from collections import deque +from wasm.immtypes import BranchImm, BranchTableImm, CallImm, CallIndirectImm +from .types import ( + U32, + I32, + I64, + F32, + F64, + Value, + Value_t, + ValType, + FunctionType, + Name, + TypeIdx, + FuncIdx, + TableIdx, + MemIdx, + GlobalIdx, + WASMExpression, + Instruction, + TableType, + MemoryType, + GlobalType, + LimitType, + convert_instructions, + debug, + Trap, + ZeroDivisionTrap, + OverflowDivisionTrap, + NonExistentFunctionCallTrap, + TypeMismatchTrap, + MissingExportException, + ConcretizeStack, +) +from ..core.smtlib import BitVec, issymbolic +from ..core.state import Concretize +from ..utils.event import Eventful + +from wasm import decode_module, Section +from wasm.wasmtypes import ( + SEC_TYPE, + SEC_IMPORT, + SEC_FUNCTION, + SEC_TABLE, + SEC_MEMORY, + SEC_GLOBAL, + SEC_EXPORT, + SEC_START, + SEC_ELEMENT, + SEC_CODE, + SEC_DATA, +) + +from ..core.smtlib.solver import Z3Solver + +solver = Z3Solver.instance() + +logger = logging.getLogger(__name__) +# logger.setLevel(logging.DEBUG) + + +# Wrappers around integers that we use for indexing the store. +class Addr(int): + pass + + +class FuncAddr(Addr): + pass + + +class TableAddr(Addr): + pass + + +class MemAddr(Addr): + pass + + +class GlobalAddr(Addr): + pass + + +ExternVal = typing.Union[FuncAddr, TableAddr, MemAddr, GlobalAddr] +FuncElem = typing.Optional[FuncAddr] + +ExportDesc = typing.Union[FuncIdx, TableIdx, MemIdx, GlobalIdx] +ImportDesc = typing.Union[TypeIdx, TableType, MemoryType, GlobalType] + + +@dataclass +class Function: + """ + A WASM Function + + https://www.w3.org/TR/wasm-core-1/#functions%E2%91%A0 + """ + + type: TypeIdx #: The index of a type defined in the module that corresponds to this function's type signature + locals: typing.List[ValType] #: Vector of mutable local variables (and their types) + body: WASMExpression #: Sequence of WASM instructions, should leave the appropriate type on the stack + + def allocate(self, store: "Store", module: "ModuleInstance") -> FuncAddr: + """ + https://www.w3.org/TR/wasm-core-1/#functions%E2%91%A5 + + :param store: Destination Store that we'll insert this Function into after allocation + :param module: The module containing the type referenced by self.type + :return: The address of this within `store` + """ + a = FuncAddr(len(store.funcs)) + store.funcs.append(FuncInst(module.types[self.type], module, self)) + return a + + +@dataclass +class Table: + """ + Vector of opaque values of type self.type + + https://www.w3.org/TR/wasm-core-1/#tables%E2%91%A0 + """ + + type: TableType #: union of a limit and a type (currently only supports funcref)s + + def allocate(self, store: "Store") -> TableAddr: + """ + https://www.w3.org/TR/wasm-core-1/#tables%E2%91%A5 + + :param store: Destination Store that we'll insert this Table into after allocation + :return: The address of this within `store` + """ + a = TableAddr(len(store.tables)) + store.tables.append( + TableInst([None for _i in range(self.type.limits.min)], self.type.limits.max) + ) + return a + + +@dataclass +class Memory: + """ + Big chunk o' raw bytes + + https://www.w3.org/TR/wasm-core-1/#memories%E2%91%A0 + """ + + type: MemoryType #: secretly a LimitType that specifies how big or small the memory can be + + def allocate(self, store: "Store") -> MemAddr: + """ + https://www.w3.org/TR/wasm-core-1/#memories%E2%91%A5 + + :param store: Destination Store that we'll insert this Memory into after allocation + :return: The address of this within `store` + """ + a = MemAddr(len(store.mems)) + store.mems.append(MemInst([0x0] * self.type.min * 64 * 1024, self.type.max)) + return a + + +@dataclass +class Global: + """ + A global variable of a given type + + https://www.w3.org/TR/wasm-core-1/#globals%E2%91%A0 + """ + + type: GlobalType #: The type of the variable + init: WASMExpression #: A (constant) sequence of WASM instructions that calculates the value for the global + + def allocate(self, store: "Store", val: Value) -> GlobalAddr: + """ + https://www.w3.org/TR/wasm-core-1/#globals%E2%91%A5 + + :param store: Destination Store that we'll insert this Global into after allocation + :param val: The initial value of the new global + :return: The address of this within `store` + """ + a = GlobalAddr(len(store.globals)) + store.globals.append(GlobalInst(val, self.type.mut)) + return a + + +@dataclass +class Elem: + """ + List of functions to initialize part of a table + + https://www.w3.org/TR/wasm-core-1/#element-segments%E2%91%A0 + """ + + table: TableIdx #: Which table to initialize + offset: WASMExpression #: WASM instructions that calculate an offset to add to the table index + init: typing.List[FuncIdx] #: list of function indices that get copied into the table + + +@dataclass +class Data: + """ + Vector of bytes that initializes part of a memory + + https://www.w3.org/TR/wasm-core-1/#data-segments%E2%91%A0 + """ + + data: MemIdx #: Which memory to put the data in. Currently only supports 0 + offset: WASMExpression #: WASM instructions that calculate offset into the memory + init: typing.List[int] #: List of bytes to copy into the memory + + +@dataclass +class Import: + """ + 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 + """ + + module: Name #: The name of the module we're importing from + name: Name #: The name of the thing we're importing + desc: ImportDesc #: Specifies whether this is a function, table, memory, or global + + +@dataclass +class Export: + """ + 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 + """ + + name: Name #: The name of the thing we're exporting + desc: ExportDesc #: Whether this is a function, table, memory, or global + + +def strip_quotes(rough_name: str) -> Name: + """ + For some reason, the parser returns the function names with quotes around them + + :param rough_name: + :return: + """ + return Name(rough_name[1:-1]) + + +class Module: + """ + Internal representation of a WASM Module + """ + + __slots__ = [ + "types", + "funcs", + "tables", + "mems", + "globals", + "elem", + "data", + "start", + "imports", + "exports", + "_raw", + ] + _raw: bytes + + def __init__(self): + self.types: typing.List[FunctionType] = [] + self.funcs: typing.List[Function] = [] + self.tables: typing.List[Table] = [] + self.mems: typing.List[Memory] = [] + self.globals: typing.List[Global] = [] + self.elem: typing.List[Elem] = [] + self.data: typing.List[Data] = [] + self.start: typing.Optional[ + FuncIdx + ] = None #: https://www.w3.org/TR/wasm-core-1/#start-function%E2%91%A0 + self.imports: typing.List[Import] = [] + self.exports: typing.List[Export] = [] + + def __getstate__(self): + state = { + "types": self.types, + "funcs": self.funcs, + "tables": self.tables, + "mems": self.mems, + "globals": self.globals, + "elem": self.elem, + "data": self.data, + "start": self.start, + "imports": self.imports, + "exports": self.exports, + "_raw": self._raw, + } + return state + + def __setstate__(self, state): + self.types = state["types"] + self.funcs = state["funcs"] + self.tables = state["tables"] + self.mems = state["mems"] + self.globals = state["globals"] + self.elem = state["elem"] + self.data = state["data"] + self.start = state["start"] + self.imports = state["imports"] + self.exports = state["exports"] + self._raw = state["_raw"] + + @classmethod + def load(cls, filename: str): + """ + Converts a WASM module in binary format into Python types that Manticore can understand + + :param filename: name of the WASM module + :return: Module + """ + type_map = {-16: types.FunctionType, -4: F64, -3: F32, -2: I64, -1: I32} + + m: Module = cls() + with open(filename, "rb") as wasm_file: + m._raw = wasm_file.read() + + module_iter = decode_module(m._raw) + _header = next(module_iter) + section: Section + # Parse the sections from the WASM module into internal types. For each section, the code usually resembles: + # `module..append((data, from, binary, module))` + for section, section_data in module_iter: + sec_id = section_data.id + if sec_id == SEC_TYPE: # https://www.w3.org/TR/wasm-core-1/#type-section%E2%91%A0 + for ft in section_data.payload.entries: + m.types.append( + FunctionType( + [type_map[p_type] for p_type in ft.param_types], + [type_map[ft.return_type] for _i in range(ft.return_count)], + ) + ) + elif sec_id == SEC_IMPORT: # https://www.w3.org/TR/wasm-core-1/#import-section%E2%91%A0 + for i in section_data.payload.entries: + ty_map = i.get_decoder_meta()["types"] + mod_name = strip_quotes(ty_map["module_str"].to_string(i.module_str)) + field_name = strip_quotes(ty_map["field_str"].to_string(i.field_str)) + if i.kind == 0: + m.imports.append(Import(mod_name, field_name, TypeIdx(i.type.type))) + + elif i.kind == 1: + m.imports.append( + Import( + mod_name, + field_name, + TableType( + LimitType(i.type.limits.initial, i.type.limits.maximum), + type_map[i.type.element_type], + ), + ) + ) + + elif i.kind == 2: + m.imports.append( + Import( + mod_name, + field_name, + MemoryType(i.type.limits.initial, i.type.limits.maximum), + ) + ) + + elif i.kind == 3: + m.imports.append( + Import( + mod_name, + field_name, + GlobalType(bool(i.type.mutability), type_map[i.type.content_type]), + ) + ) + + else: + raise RuntimeError("Can't decode kind field of:", i.kind) + + elif ( + sec_id == SEC_FUNCTION + ): # https://www.w3.org/TR/wasm-core-1/#function-section%E2%91%A0 + for f in section_data.payload.types: + m.funcs.append( + Function(TypeIdx(f), [], []) + ) # The expressions and locals are stored in the code section + elif sec_id == SEC_TABLE: # https://www.w3.org/TR/wasm-core-1/#table-section%E2%91%A0 + for t in section_data.payload.entries: + m.tables.append( + Table( + TableType(LimitType(t.limits.initial, t.limits.maximum), FunctionType) + ) + ) + elif sec_id == SEC_MEMORY: # https://www.w3.org/TR/wasm-core-1/#memory-section%E2%91%A0 + for mem in section_data.payload.entries: + m.mems.append(Memory(LimitType(mem.limits.initial, mem.limits.maximum))) + elif sec_id == SEC_GLOBAL: # https://www.w3.org/TR/wasm-core-1/#global-section%E2%91%A0 + for g in section_data.payload.globals: + m.globals.append( + Global( + GlobalType(g.type.mutability, type_map[g.type.content_type]), + convert_instructions(g.init), + ) + ) + elif sec_id == SEC_EXPORT: # https://www.w3.org/TR/wasm-core-1/#export-section%E2%91%A0 + mapping = (FuncIdx, TableIdx, MemIdx, GlobalIdx) + for e in section_data.payload.entries: + ty = e.get_decoder_meta()["types"]["field_str"] + m.exports.append( + Export(strip_quotes(ty.to_string(e.field_str)), mapping[e.kind](e.index)) + ) + elif sec_id == SEC_START: # https://www.w3.org/TR/wasm-core-1/#start-section%E2%91%A0 + m.start = FuncIdx(section_data.payload.index) + elif ( + sec_id == SEC_ELEMENT + ): # https://www.w3.org/TR/wasm-core-1/#element-section%E2%91%A0 + for e in section_data.payload.entries: + m.elem.append( + Elem( + TableIdx(e.index), + convert_instructions(e.offset), + [FuncIdx(i) for i in e.elems], + ) + ) + elif sec_id == SEC_CODE: # https://www.w3.org/TR/wasm-core-1/#code-section%E2%91%A0 + for idx, c in enumerate(section_data.payload.bodies): + m.funcs[idx].locals = [ + type_map[e.type] for e in c.locals for _i in range(e.count) + ] + m.funcs[idx].body = convert_instructions(c.code) + elif sec_id == SEC_DATA: # https://www.w3.org/TR/wasm-core-1/#data-section%E2%91%A0 + for d in section_data.payload.entries: + m.data.append( + Data(MemIdx(d.index), convert_instructions(d.offset), d.data.tolist()) + ) + # TODO - custom sections (https://www.w3.org/TR/wasm-core-1/#custom-section%E2%91%A0) + + return m + + +@dataclass +class ProtoFuncInst: + """ + Groups FuncInst and HostFuncInst into the same category + """ + + type: FunctionType #: The type signature of this function + + +@dataclass +class TableInst: + """ + 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 + """ + + #: A list of FuncAddrs (any of which can be None) that point to funcs in the Store + elem: typing.List[FuncElem] + max: typing.Optional[U32] #: Optional maximum size of the table + + +@dataclass +class MemInst: + """ + 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 + """ + + data: typing.List[int] #: The backing array for this memory + max: typing.Optional[U32] #: Optional maximum number of pages the memory can contain + + def grow(self, n: int) -> bool: + """ + Adds n blank pages to the current memory + + See: https://www.w3.org/TR/wasm-core-1/#grow-mem + + :param n: The number of pages to attempt to add + :return: True if the operation succeeded, otherwise False + """ + assert len(self.data) % 65536 == 0 + ln = n + (len(self.data) // 65536) + if ln > (2 ** 16): + return False + if self.max is not None: + if ln > self.max: + return False + self.data.extend(0x0 for _ in range(n * 65536)) # TODO - these should also be symbolic + return True + + +@dataclass +class GlobalInst: + """ + 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 + """ + + value: Value #: The actual value of this global + mut: bool #: Whether the global can be modified + + +@dataclass +class ExportInst: + """ + Runtime representation of any thing that can be exported + + https://www.w3.org/TR/wasm-core-1/#export-instances%E2%91%A0 + """ + + name: Name #: The name to export under + value: ExternVal #: FuncAddr, TableAddr, MemAddr, or GlobalAddr + + +class 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 + """ + + __slots__ = ["funcs", "tables", "mems", "globals"] + funcs: typing.List[ProtoFuncInst] + tables: typing.List[TableInst] + mems: typing.List[MemInst] + globals: typing.List[GlobalInst] + + def __init__(self): + self.funcs = [] + self.tables = [] + self.mems = [] + self.globals = [] + + def __getstate__(self): + state = { + "funcs": self.funcs, + "tables": self.tables, + "mems": self.mems, + "globals": self.globals, + } + return state + + def __setstate__(self, state): + self.funcs = state["funcs"] + self.tables = state["tables"] + self.mems = state["mems"] + self.globals = state["globals"] + + +def _eval_maybe_symbolic(constraints, expression) -> bool: + if issymbolic(expression): + return solver.must_be_true(constraints, expression) + return True if expression else False + + +class ModuleInstance(Eventful): + """ + 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 + """ + + __slots__ = [ + "types", + "funcaddrs", + "tableaddrs", + "memaddrs", + "globaladdrs", + "exports", + "export_map" "executor", + "_instruction_queue", + "_block_depths", + ] + + _published_events = {"execute_instruction", "call_hostfunc", "exec_expression", "raise_trap"} + + #: Stores the type signatures of all the functions + types: typing.List[FunctionType] + #: Stores the *indices* of functions within the store + funcaddrs: typing.List[FuncAddr] + #: Stores the indices of tables + tableaddrs: typing.List[TableAddr] + #: Stores the indices of memories (at time of writing, WASM only allows one memory) + memaddrs: typing.List[MemAddr] + #: Stores the indices of globals + globaladdrs: typing.List[GlobalAddr] + #: Stores records of everything exported by this module + exports: typing.List[ExportInst] + #: Maps the names of exports to their index in the list of exports + export_map: typing.Dict[str, int] + #: Contains instruction implementations for all non-control-flow instructions + executor: Executor + #: Stores the unpacked sequence of instructions in the order they should be executed + _instruction_queue: typing.Deque[Instruction] + #: Keeps track of the current call depth, both for functions and for code blocks. Each function call is represented + # by appending another 0 to the list, and each code block is represented by incrementing the digit at the end of the + # list. This is necessary because we unroll the WASM S-Expressions (nested execution trees) into a single + # instruction queue, so the meaning of an `end` instruction could be otherwise ambiguous. Loosely put, the sum of + # all the digits in this list is the number of `end` instructions we need to see before execution is finished. + _block_depths: typing.List[int] + #: Prevents the user from invoking functions before instantiation + instantiated: bool + + def __init__(self, constraints=None): + self.types = [] + self.funcaddrs = [] + self.tableaddrs = [] + self.memaddrs = [] + self.globaladdrs = [] + self.exports = [] + self.export_map = {} + self.executor = Executor(constraints) + self._instruction_queue = deque() + self._block_depths = [0] + + super().__init__() + + def __getstate__(self): + state = super().__getstate__() + state.update( + { + "types": self.types, + "funcaddrs": self.funcaddrs, + "tableaddrs": self.tableaddrs, + "memaddrs": self.memaddrs, + "globaladdrs": self.globaladdrs, + "exports": self.exports, + "export_map": self.export_map, + "executor": self.executor, + "_instruction_queue": self._instruction_queue, + "_block_depths": self._block_depths, + } + ) + return state + + def __setstate__(self, state): + self.types = state["types"] + self.funcaddrs = state["funcaddrs"] + self.tableaddrs = state["tableaddrs"] + self.memaddrs = state["memaddrs"] + self.globaladdrs = state["globaladdrs"] + self.exports = state["exports"] + self.export_map = state["export_map"] + self.executor = state["executor"] + self._instruction_queue = state["_instruction_queue"] + self._block_depths = state["_block_depths"] + super().__setstate__(state) + + def reset_internal(self): + """ + Empties the instruction queue and clears the block depths + """ + self._instruction_queue.clear() + self._block_depths = [0] + + def instantiate( + self, + store: Store, + module: "Module", + extern_vals: typing.List[ExternVal], + 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 + + :param store: The store to place the allocated contents in + :param module: The WASM Module to instantiate in this instance + :param extern_vals: Imports needed to instantiate the module + :param exec_start: whether or not to execute the start section (if present) + """ + # #1 Assert: module is valid + assert module # close enough + + # TODO: #2 Assert: module is valid with external types _externtype_ classifying its imports. + # for ext in module.imports: + # assert isinstance(ext, ExternType.__args__) + + # #3 Assert the same number of imports and external values + assert len(module.imports) == len( + extern_vals + ), f"Expected {len(module.imports)} imports, got {len(extern_vals)}" + + # #4 TODO + + # #5 - evaluate globals + stack = Stack() + + aux_mod = ModuleInstance() + aux_mod.globaladdrs = [i for i in extern_vals if isinstance(i, GlobalAddr)] + aux_frame = Frame([], aux_mod) + stack.push(Activation(1, aux_frame)) + + vals = [self.exec_expression(store, stack, gb.init) for gb in module.globals] + + last_frame = stack.pop() + assert isinstance(last_frame, Activation) + assert last_frame.frame == aux_frame + + # #6, #7, #8 - Allocate all the things + self.allocate(store, module, extern_vals, vals) + f = Frame(locals=[], module=self) + stack.push(Activation(0, f)) + + # #9 & #13 - emplace element sections into tables + for elem in module.elem: + eoval = self.exec_expression(store, stack, elem.offset) + assert isinstance(eoval, I32) + assert elem.table in range(len(self.tableaddrs)) + tableaddr: TableAddr = self.tableaddrs[elem.table] + assert tableaddr in range(len(store.tables)) + tableinst: TableInst = store.tables[tableaddr] + eend = eoval + len(elem.init) + assert eend <= len(tableinst.elem) + + func_idx: FuncIdx + for j, func_idx in enumerate(elem.init): + assert func_idx in range(len(self.funcaddrs)) + funcaddr = self.funcaddrs[func_idx] + tableinst.elem[eoval + j] = funcaddr + + # #10 & #14 - emplace data sections into memory + for data in module.data: + doval = self.exec_expression(store, stack, data.offset) + assert isinstance(doval, I32), f"{type(doval)} is not an I32" + assert data.data in range(len(self.memaddrs)) + memaddr = self.memaddrs[data.data] + assert memaddr in range(len(store.mems)) + meminst = store.mems[memaddr] + dend = doval + len(data.init) + assert dend <= len(meminst.data) + + for j, b in enumerate(data.init): + meminst.data[doval + j] = b + + # #11 & #12 + last_frame = stack.pop() + assert isinstance(last_frame, Activation) + assert last_frame.frame == f + + # #15 run start function + if module.start is not None: + assert module.start in range(len(self.funcaddrs)) + funcaddr = self.funcaddrs[module.start] + assert funcaddr in range(len(store.funcs)) + self.invoke(stack, self.funcaddrs[module.start], store, []) + if exec_start: + stack.push(self.exec_expression(store, stack, [])) + logger.info("Initialization Complete") + + def allocate( + self, + store: Store, + module: "Module", + extern_vals: typing.List[ExternVal], + values: typing.List[Value], + ): + """ + 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 + + :param store: The Store to put all of the allocated subcomponents in + :param module: Tne Module containing all the items to allocate + :param extern_vals: Imported values + :param values: precalculated global values + """ + self.types = module.types + + for ev in extern_vals: + if isinstance(ev, FuncAddr): + self.funcaddrs.append(ev) + if isinstance(ev, TableAddr): + self.tableaddrs.append(ev) + if isinstance(ev, MemAddr): + self.memaddrs.append(ev) + if isinstance(ev, GlobalAddr): + self.globaladdrs.append(ev) + + for func_i in module.funcs: + self.funcaddrs.append(func_i.allocate(store, self)) + for table_i in module.tables: + self.tableaddrs.append(table_i.allocate(store)) + for memory_i in module.mems: + self.memaddrs.append(memory_i.allocate(store)) + for idx, global_i in enumerate(module.globals): + assert isinstance(values[idx], global_i.type.value) + self.globaladdrs.append(global_i.allocate(store, values[idx])) + for idx, export_i in enumerate(module.exports): + if isinstance(export_i.desc, FuncIdx): + self.exports.append(ExportInst(export_i.name, self.funcaddrs[export_i.desc])) + elif isinstance(export_i.desc, TableIdx): + self.exports.append(ExportInst(export_i.name, self.tableaddrs[export_i.desc])) + elif isinstance(export_i.desc, MemIdx): + self.exports.append(ExportInst(export_i.name, self.memaddrs[export_i.desc])) + elif isinstance(export_i.desc, GlobalIdx): + self.exports.append(ExportInst(export_i.name, self.globaladdrs[export_i.desc])) + else: + raise RuntimeError("Export desc wasn't a function, table, memory, or global") + self.export_map[export_i.name] = len(self.exports) - 1 + + def invoke_by_name(self, name: str, stack, store, argv): + """ + Iterates over the exports, attempts to find the function specified by `name`. Calls `invoke` with its FuncAddr, + passing argv + + :param name: Name of the function to look for + :param argv: Arguments to pass to the function. Can be BitVecs or Values + """ + for export in self.exports: + if export.name == name and isinstance(export.value, FuncAddr): + return self.invoke(stack, export.value, store, argv) + raise RuntimeError("Can't find a function called", name) + + def invoke(self, stack: "Stack", funcaddr: FuncAddr, store: Store, argv: typing.List[Value]): + """ + 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 + + :param funcaddr: Address (in Store) of the function to call + :param argv: Arguments to pass to the function. Can be BitVecs or Values + """ + assert funcaddr in range(len(store.funcs)) + funcinst = store.funcs[funcaddr] + ty = funcinst.type + assert len(ty.param_types) == len( + argv + ), f"Function {funcaddr} expects {len(ty.param_types)} arguments" + # for t, v in zip(ty.param_types, argv): + # assert type(v) == type(t) + + # Create dummy frame, which is required by the spec but doesn't serve any obvious purpose. It also never + # gets popped. + dummy_frame = Frame([], ModuleInstance()) + stack.push( + dummy_frame # type: ignore # This isn't an activation/label/value, but we'll let it slide + ) + for v in argv: + stack.push(v) + + # https://www.w3.org/TR/wasm-core-1/#exec-invoke + self._invoke_inner(stack, funcaddr, store) + + # In the spec, once the function has returned, you pop the returns from the stack and return them to the + # caller. Since Manticore executes functions via the `run` method (ie separately from invocation), we don't + # do that here. + + def _invoke_inner(self, stack: "Stack", funcaddr: FuncAddr, store: Store): + """ + Invokes the function at address funcaddr. Validates the function type, sets up the Activation with the local + variables, and executes the function. If the function is a HostFunc (native code), it executes it blindly and + pushes the return values to the stack. If it's a WASM function, it enters the outermost code block. + + https://www.w3.org/TR/wasm-core-1/#exec-invoke + + :param stack: The current stack, to use for execution + :param funcaddr: The address of the function to invoke + :param store: The current store, to use for execution + """ + assert funcaddr in range(len(store.funcs)) + f: ProtoFuncInst = store.funcs[funcaddr] + ty = f.type + assert len(ty.result_types) <= 1 + local_vars: typing.List[Value] = [] + for v in [stack.pop() for _t in ty.param_types][::-1]: + assert not isinstance(v, (Label, Activation)) + local_vars.append(v) + if isinstance(f, HostFunc): # Call native function + self._publish("will_call_hostfunc", f, local_vars) + res = list(f.hostcode(self.executor.constraints, *local_vars)) + self._publish("did_call_hostfunc", f, local_vars, res) + logger.info("HostFunc returned: %s", res) + assert len(res) == len(ty.result_types) + for r, t in zip(res, ty.result_types): + assert t in {I32, I64, F32, F64} + # Even though I32, I64, F32, and F64 all have `cast` class methods, mypy can't figure out that + # t has to be one of those since it doesn't evaluate the previous assert. Note that `isinstance` + # won't work here since we're using the actual types, not instances of them. + stack.push(t.cast(r)) # type: ignore + else: # Call WASM function + assert isinstance(f, FuncInst), "Got a non-WASM function! (Maybe cast to HostFunc?)" + for cast in f.code.locals: + local_vars.append(cast(0)) + frame = Frame(local_vars, f.module) + stack.push( + Activation( + len(ty.result_types), frame, expected_block_depth=len(self._block_depths) + ) # When we pop this frame, we expect to be expected_block_depth call frames deep + ) + self._block_depths.append(0) # We're entering a new function call context + self.block(store, stack, ty.result_types, f.code.body) + + def exec_expression(self, store: Store, stack: "Stack", expr: WASMExpression): + """ + 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. + + :param expr: The expression to execute + :return: The result of the expression + """ + self.push_instructions(expr) + self._publish("will_exec_expression", expr) + while self.exec_instruction(store, stack): + pass + self._publish("did_exec_expression", expr, stack.peek()) + return stack.pop() + + def enter_block(self, insts, label: "Label", stack: "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 + + :param insts: Instructions for this block + :param label: Label referencing the continuation of this block + :param stack: The execution stack (where we push the label) + """ + stack.push(label) + self._block_depths[-1] += 1 + self.push_instructions(insts) + + def exit_block(self, stack: "Stack"): + """ + Cleans up after execution of a code block. + + https://www.w3.org/TR/wasm-core-1/#exiting--hrefsyntax-instrmathitinstrast-with-label--l + """ + # Look for a label on the stack + label_idx = stack.find_type(Label) + if label_idx is not None: + logger.debug( + "EXITING BLOCK (FD: %d, BD: %d)", len(self._block_depths), self._block_depths[-1] + ) + # Pop the values above the label + vals = [] + while not isinstance(stack.peek(), Label): + vals.append(stack.pop()) + assert isinstance(vals[-1], Value_t), f"{type(vals[-1])} is not a value or a label" + label = stack.pop() + assert isinstance(label, Label), f"Stack contained a {type(label)} instead of a Label" + # Decrement the block number + self._block_depths[-1] -= 1 + # Put the values back on the stack and discard the label + for v in vals[::-1]: + stack.push(v) + + def exit_function(self, stack: "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 + """ + if len(self._block_depths) > 1: # Only if we're in a _real_ function, not initialization + logger.debug( + "EXITING FUNCTION (FD: %d, BD: %d)", len(self._block_depths), self._block_depths[-1] + ) + # Pop return values + f = stack.get_frame() + n = f.arity + stack.has_type_on_top(Value_t, n) + vals = [stack.pop() for _ in range(n)] + assert isinstance( + stack.peek(), Activation + ), f"Stack should have an activation on top, instead has {type(stack.peek())}" + + # Discard call frame + self._block_depths.pop() + stack.pop() + + # Replace return values + for v in vals[::-1]: + stack.push(v) + + def push_instructions(self, insts: WASMExpression): + """ + Pushes instructions into the instruction queue. + :param insts: Instructions to push + """ + for i in insts[::-1]: + self._instruction_queue.appendleft(i) + + def look_forward(self, *opcodes) -> typing.List[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. + + :param opcodes: Tuple of instruction opcodes to look for + :return: The list of instructions popped before encountering the target instruction. + """ + out = [] + i = self._instruction_queue.popleft() + while i.opcode not in opcodes: + out.append(i) + + # Call recursively if we encounter another block + if i.opcode in {0x02, 0x03, 0x04}: + out += self.look_forward(0x0B) + + if len(self._instruction_queue) == 0: + raise RuntimeError( + "Couldn't find an instruction with opcode " + + ", ".join(hex(op) for op in opcodes) + ) + i = self._instruction_queue.popleft() + out.append(i) + return out + + def exec_instruction(self, store: Store, stack: "Stack") -> 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. + + :param 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. + :param 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. + :return: True if execution succeeded, False if there are no more instructions to execute + """ + # Maps return types from instruction immediates into actual types + ret_type_map = {-1: [I32], -2: [I64], -3: [F32], -4: [F64], -64: []} + # Use the AtomicStack context manager to catch Concretization and roll back changes + with AtomicStack(stack) as aStack: + # print("Instructions:", self._instruction_queue) + if self._instruction_queue: + try: + inst = self._instruction_queue.popleft() + logger.info( + "%s: %s (%s)", + hex(inst.opcode), + inst.mnemonic, + debug(inst.imm) if inst.imm else "", + ) + self._publish("will_execute_instruction", inst) + if 0x2 <= inst.opcode <= 0x11: # This is a control-flow instruction + self.executor.zero_div = _eval_maybe_symbolic( + self.executor.constraints, self.executor.zero_div + ) + if self.executor.zero_div: + raise ZeroDivisionTrap() + self.executor.overflow = _eval_maybe_symbolic( + self.executor.constraints, self.executor.overflow + ) + if self.executor.overflow: + raise OverflowDivisionTrap() + + if inst.opcode == 0x02: + self.block( + store, + aStack, + # Get return type from the immediate. Unfortunately, since mypy doesn't know the + # immediate type, it doesn't like this and we have to ignore the type + ret_type_map[inst.imm.sig], # type: ignore + self.look_forward(0x0B), # Get the contents of this block + ) + elif inst.opcode == 0x03: + self.loop(store, aStack, inst) + elif inst.opcode == 0x04: + # Get the appropriate return type based on the immediate. Same issue w/ immediate types + self.if_(store, aStack, ret_type_map[inst.imm.sig]) # type: ignore + elif inst.opcode == 0x05: + self.else_(store, aStack) + elif inst.opcode == 0x0B: + self.end(store, aStack) + elif inst.opcode == 0x0C: + # Extract the relative depth from the immediate because it makes br's interface + # a little bit cleaner. Same issue w/ mypy not understanding immediate types + self.br(store, aStack, inst.imm.relative_depth) # type: ignore + elif inst.opcode == 0x0D: + self.br_if(store, aStack, inst.imm) + elif inst.opcode == 0x0E: + self.br_table(store, aStack, inst.imm) + elif inst.opcode == 0x0F: + self.return_(store, aStack) + elif inst.opcode == 0x10: + self.call(store, aStack, inst.imm) + elif inst.opcode == 0x11: + self.call_indirect(store, aStack, inst.imm) + else: + raise Exception("Unhandled control flow instruction") + else: # This is a numeric instruction, hand it to the Executor + self.executor.dispatch(inst, store, aStack) + self._publish("did_execute_instruction", inst) + return True + except Concretize as exc: + # Push the last instruction back to the queue so it will be reattempted after concretization + self._instruction_queue.appendleft(inst) + raise exc + except Trap as exc: + # Treat traps as an exit from the current call frame. This is something of a kludge to make + # the tests pass. I may need to revisit this in the future because I haven't thoroughly explored + # or thought about what the correct behavior is here. + self._block_depths.pop() + logger.info("Trap: %s", str(exc)) + self._publish("will_raise_trap", exc) + raise exc + + elif aStack.find_type(Label): + # This used to raise a runtime error, but since we have some capacity to recover after a trap, we + # demote it to a logger.info + logger.info( + "The instruction queue is empty, but there are still labels on the stack. This should only happen when re-executing after a Trap" + ) + return False + + def get_export( + self, name: str, store: Store + ) -> typing.Union[ProtoFuncInst, TableInst, MemInst, GlobalInst]: + """ + Retrieves a value exported by this module instance from store + + :param name: The name of the exported value to get + :param store: The current execution store (where the export values live) + :return: The value of the export + """ + export_addr = self.get_export_address(name) + if isinstance(export_addr, FuncAddr): + return store.funcs[export_addr] + if isinstance(export_addr, TableAddr): + return store.tables[export_addr] + if isinstance(export_addr, MemAddr): + return store.mems[export_addr] + if isinstance(export_addr, GlobalAddr): + return store.globals[export_addr] + raise RuntimeError("Unkown export type: " + str(type(export_addr))) + + def get_export_address( + self, name: str + ) -> typing.Union[FuncAddr, TableAddr, MemAddr, GlobalAddr]: + """ + Retrieves the address of a value exported by this module within the store + + :param name: The name of the exported value to get + :return: The address of the desired export + """ + if name not in self.export_map: + raise MissingExportException(name) + export: ExportInst = self.exports[self.export_map[name]] + assert export.name == name, f"Export name mismatch (expected {name}, got {export.name})" + return export.value + + def block( + self, store: "Store", stack: "Stack", ret_type: typing.List[ValType], insts: WASMExpression + ): + """ + 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 + + :param ret_type: List of expected return types for this block. Really only need the arity + :param insts: Instructions to execute + """ + arity = len(ret_type) + label = Label(arity, []) + self.enter_block(insts, label, stack) + + def loop(self, store: "Store", stack: "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 + + :param loop_inst: The current insrtuction + """ + # Grab the instructions that make up the loop + insts = self.look_forward(0x0B) + # Create a label with the full loop + label = Label(0, [loop_inst] + insts) + # Enter the rest of the block + self.enter_block(insts, label, stack) + + def extract_block(self, partial_list: typing.Deque[Instruction]) -> typing.Deque[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. + + :param partial_list: List of instructions to extract the block from + :return: The extracted block + """ + out: typing.Deque[Instruction] = deque() + i = partial_list.popleft() + while i.opcode != 0x0B: + out.append(i) + if i.opcode in {0x02, 0x03, 0x04}: + out += self.extract_block(partial_list) + if len(partial_list) == 0: + raise RuntimeError("Couldn't find an end to this block!") + i = partial_list.popleft() + out.append(i) + return out + + def _split_if_block( + self, partial_list: typing.Deque[Instruction] + ) -> typing.Tuple[typing.Deque[Instruction], typing.Deque[Instruction]]: + """ + Splits an if block into its true and false portions. Handles nested blocks in both the true and false branches, + and when one branch is empty and/or the else instruction is missing. + + :param partial_list: Complete if block that needs to be split + :return: The true block and the false block + """ + t_block: typing.Deque[Instruction] = deque() + assert partial_list[-1].opcode == 0x0B, "This block is missing an end instruction!" + i = partial_list.popleft() + while i.opcode not in {0x05, 0x0B}: + t_block.append(i) + if i.opcode in {0x02, 0x03, 0x04}: + t_block += self.extract_block(partial_list) + if len(partial_list) == 0: + raise RuntimeError("Couldn't find an end to this if statement!") + i = partial_list.popleft() + t_block.append(i) + + return t_block, partial_list + + def if_(self, store: "Store", stack: "AtomicStack", ret_type: typing.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 + """ + stack.has_type_on_top(I32, 1) + c = stack.pop() + if issymbolic(c): + raise ConcretizeStack(-1, I32, "Concretizing if_", c) + insn_block = self.look_forward(0x0B) # Get the entire `if` block + # Split it into the true and false branches + t_block, f_block = self._split_if_block(deque(insn_block)) + label = Label(len(ret_type), []) + + # Enter the true branch if the top of the stack is nonzero + if c != 0: + self.enter_block(list(t_block), label, stack) + # Otherwise, take the false branch + else: + # Handle if there wasn't an `else` instruction + if len(f_block) == 0: + assert t_block[-1].opcode == 0x0B # The true block is just an `end` + f_block.append(t_block[-1]) + self.enter_block(list(f_block), label, stack) + + def else_(self, store: "Store", stack: "AtomicStack"): + """ + Marks the end of the first block of an if statement. + Typically, `if` blocks look like: `if else end`. That's not always the case. See: + https://webassembly.github.io/spec/core/text/instructions.html#abbreviations + """ + self.exit_block(stack) + + def end(self, store: "Store", stack: "AtomicStack"): + """ + Marks the end of an instruction block or function + """ + if self._block_depths[-1] > 0: + # We're at the end of a block, but haven't finished the function + self.exit_block(stack) + if self._block_depths[-1] == 0: + # We've finished all the blocks in the function + self.exit_function(stack) + + def br(self, store: "Store", stack: "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 + """ + assert stack.has_at_least(Label, label_depth + 1) + + label: Label = stack.get_nth(Label, label_depth) + stack.has_type_on_top(Value_t, label.arity) + vals = [stack.pop() for _ in range(label.arity)] + + # Pop the higher labels and values from the stack and discard them + for _ in range(label_depth + 1): + while isinstance(stack.peek(), Value_t): + stack.pop() + assert isinstance(stack.peek(), Label) + stack.pop() + assert self._block_depths[-1] > 0, "Trying to break out of a function call" + self._block_depths[-1] -= 1 + + # Push the values expected by this branch back onto the stack + for v in vals[::-1]: + stack.push(v) + + # Purge the next label_depth blocks of instructions from the queue until we've reached the appropriate depth + for _ in range(label_depth + 1): + self.look_forward(0x0B, 0x05) + # Push the instructions from the label + self.push_instructions(label.instr) + + def br_if(self, store: "Store", stack: "AtomicStack", imm: 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 + """ + stack.has_type_on_top(I32, 1) + c = stack.pop() + if issymbolic(c): + raise ConcretizeStack(-1, I32, "Concretizing br_if", c) + if c != 0: + self.br(store, stack, imm.relative_depth) + + def br_table(self, store: "Store", stack: "AtomicStack", imm: 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 + """ + stack.has_type_on_top(I32, 1) + i = stack.pop() + if issymbolic(i): + raise ConcretizeStack(-1, I32, "Concretizing br_table", i) + + # The spec (https://www.w3.org/TR/wasm-core-1/#exec-br-table) says that if i < the length of the table, + # execute br target_table[i]. The tests, however, pass a negative i, which doesn't make sense in this + # situation. For that reason, we use `in range` even though it's a different behavior. + if i in range(imm.target_count): + lab = imm.target_table[i] + else: + lab = imm.default_target + self.br(store, stack, lab) + + def return_(self, store: "Store", stack: "AtomicStack"): + """ + Return from the function (ie branch to the outermost block) + + https://www.w3.org/TR/wasm-core-1/#exec-return + """ + # Pop everything from the stack until we get to the current call frame, then push back the topmost + # n values, where n is the number of expected returns for the current function + f = stack.get_frame() + n = f.arity + stack.has_type_on_top(Value_t, n) + ret = [stack.pop() for _i in range(n)] + while not isinstance(stack.peek(), (Activation, Frame)): + stack.pop() + assert stack.peek() == f + stack.pop() + for r in ret[::-1]: + stack.push(r) + + # Ensure that we've returned to the correct block depth for the frame we just popped + while len(self._block_depths) > f.expected_block_depth: + # Discard the rest of the current block, then keep discarding blocks from the instruction queue + # until we've purged the rest of this function. + for i in range(self._block_depths[-1]): + self.look_forward(0x0B, 0x05) + # Pop the current function call from the block depth tracker + self._block_depths.pop() + + def call(self, store: "Store", stack: "AtomicStack", imm: CallImm): + """ + Invoke the function at the address in the store given by the immediate. + + https://www.w3.org/TR/wasm-core-1/#exec-call + """ + f = stack.get_frame() + assert imm.function_index in range(len(f.frame.module.funcaddrs)) + a = f.frame.module.funcaddrs[imm.function_index] + self._invoke_inner(stack, a, store) + + def call_indirect(self, store: "Store", stack: "AtomicStack", imm: 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 + """ + f = stack.get_frame() + assert f.frame.module.tableaddrs + ta = f.frame.module.tableaddrs[0] + assert ta in range(len(store.tables)) + tab = store.tables[ta] + assert imm.type_index in range(len(f.frame.module.types)) + ft_expect = f.frame.module.types[imm.type_index] + stack.has_type_on_top(I32, 1) + # mypy can't figure out that I32 is a Value + i: I32 = stack.pop() # type: ignore + if issymbolic(i): + raise ConcretizeStack(-1, I32, "Concretizing call_indirect operand", i) + if i not in range(len(tab.elem)): + raise NonExistentFunctionCallTrap() + if tab.elem[i] is None: + raise NonExistentFunctionCallTrap() + a = tab.elem[i] + assert a is not None + assert a in range(len(store.funcs)) + func = store.funcs[a] + ft_actual = func.type + if ft_actual != ft_expect: + raise TypeMismatchTrap(ft_actual, ft_expect) + self._invoke_inner(stack, a, store) + + +@dataclass +class Label: + """ + 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: typing.List[ + Instruction + ] #: The sequence of instructions to execute if we branch to this label + + +@dataclass +class Frame: + """ + 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: typing.List[Value] #: The values of the local variables for this function call + module: ModuleInstance #: A reference to the parent module instance in which the function call was made + + +@dataclass +class Activation: + """ + 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 + frame: Frame #: The nested frame + expected_block_depth: int #: Internal helper used to track the expected block depth when we exit this label + + def __init__(self, arity, frame, expected_block_depth=0): + self.arity = arity + self.frame = frame + self.expected_block_depth = expected_block_depth + + +class Stack(Eventful): + """ + Stores the execution stack & provides helper methods + + https://www.w3.org/TR/wasm-core-1/#stack%E2%91%A0 + """ + + data: typing.Deque[ + typing.Union[Value, Label, Activation] + ] #: Underlying datastore for the "stack" + + _published_events = {"push_item", "pop_item"} + + def __init__(self, init_data=None): + """ + :param init_data: Optional initialization value + """ + self.data = init_data if init_data else deque() + super().__init__() + + def __getstate__(self): + state = super().__getstate__() + state["data"] = self.data + return state + + def __setstate__(self, state): + self.data = state["data"] + super().__setstate__(state) + + def push(self, val: typing.Union[Value, Label, Activation]) -> None: + """ + Push a value to the stack + + :param val: The value to push + :return: None + """ + if isinstance(val, list): + raise RuntimeError("Don't push lists") + logger.debug("+%d %s (%s)", len(self.data), val, type(val)) + self._publish("will_push_item", val, len(self.data)) + self.data.append(val) + self._publish("did_push_item", val, len(self.data)) + + def pop(self) -> typing.Union[Value, Label, Activation]: + """ + Pop a value from the stack + + :return: the popped value + """ + logger.debug("-%d %s (%s)", len(self.data) - 1, self.peek(), type(self.peek())) + self._publish("will_pop_item", len(self.data)) + item = self.data.pop() + self._publish("did_pop_item", item, len(self.data)) + return item + + def peek(self) -> typing.Optional[typing.Union[Value, Label, Activation]]: + """ + :return: the item on top of the stack (without removing it) + """ + if self.data: + return self.data[-1] + return None + + def empty(self) -> bool: + """ + :return: True if the stack is empty, otherwise False + """ + return len(self.data) == 0 + + def has_type_on_top(self, t: typing.Union[type, typing.Tuple[type]], n: int): + """ + *Asserts* that the stack has at least n values of type t or type BitVec on the top + + :param t: type of value to look for (Bitvec is always included as an option) + :param n: Number of values to check + :return: True + """ + for i in range(1, n + 1): + assert isinstance( + self.data[i * -1], (t, BitVec) + ), f"{type(self.data[i * -1])} is not an {t}!" + return True + + def find_type(self, t: type) -> typing.Optional[int]: + """ + :param t: The type to look for + :return: The depth of the first value of type t + """ + for idx, v in enumerate(reversed(self.data)): + if isinstance(v, t): + return -1 * idx + return None + + def has_at_least(self, t: type, n: int) -> bool: + """ + :param t: type to look for + :param n: number to look for + :return: whether the stack contains at least n values of type t + """ + count = 0 + for v in reversed(self.data): + if isinstance(v, t): + count += 1 + if count == n: + return True + return False + + def get_nth(self, t: type, n: int) -> typing.Optional[typing.Union[Value, Label, Activation]]: + """ + :param t: type to look for + :param n: number to look for + :return: the nth item of type t from the top of the stack, or None + """ + seen = 0 + for v in reversed(self.data): + if isinstance(v, t): + if seen == n: + return v + seen += 1 + return None + + def get_frame(self) -> Activation: + """ + :return: the topmost frame (Activation) on the stack + """ + for item in reversed(self.data): + if isinstance(item, Activation): + return item + raise RuntimeError("Couldn't find a frame on the stack") + + +class AtomicStack(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 PushItem: + pass + + @dataclass + class PopItem: + val: typing.Union[Value, Label, Activation] + + def __init__(self, parent: Stack): + self.parent = parent + self.actions: typing.List[typing.Union[AtomicStack.PushItem, AtomicStack.PopItem]] = [] + + def __getstate__(self): + state = {"parent": self.parent, "actions": self.actions} + return state + + def __setstate__(self, state): + self.parent = state["parent"] + self.actions = state["actions"] + + def __enter__(self): + return self + + def __exit__(self, exc_type, exc_val, exc_tb): + if exc_val and isinstance(exc_val, Concretize): + logger.info("Rolling back stack for concretization") + self.rollback() + else: + pass + + def rollback(self): + while self.actions: + action = self.actions.pop() + if isinstance(action, AtomicStack.PopItem): + self.parent.push(action.val) + elif isinstance(action, AtomicStack.PushItem): + self.parent.pop() + + def push(self, val: typing.Union[Value, Label, Activation]) -> None: + self.actions.append(AtomicStack.PushItem()) + self.parent.push(val) + + def pop(self) -> typing.Union[Value, Label, Activation]: + val = self.parent.pop() + self.actions.append(AtomicStack.PopItem(val)) + return val + + def peek(self): + return self.parent.peek() + + def empty(self): + return self.parent.empty() + + def has_type_on_top(self, t: typing.Union[type, typing.Tuple[type]], n: int): + return self.parent.has_type_on_top(t, n) + + def find_type(self, t: type): + return self.parent.find_type(t) + + def has_at_least(self, t: type, n: int): + return self.parent.has_at_least(t, n) + + def get_nth(self, t: type, n: int): + return self.parent.get_nth(t, n) + + def get_frame(self) -> Activation: + return self.parent.get_frame() + + +@dataclass +class FuncInst(ProtoFuncInst): + """ + Instance type for WASM functions + """ + + module: ModuleInstance + code: "Function" + + +@dataclass +class HostFunc(ProtoFuncInst): + """ + Instance type for native functions that have been provided via import + """ + + hostcode: types.FunctionType #: the native function. Should accept ConstraintSet as the first argument + + def allocate( + self, store: Store, functype: FunctionType, host_func: types.FunctionType + ) -> FuncAddr: + """ + Currently not needed. + + https://www.w3.org/TR/wasm-core-1/#host-functions%E2%91%A2 + """ + pass diff --git a/manticore/wasm/types.py b/manticore/wasm/types.py new file mode 100644 index 00000000..efaa4725 --- /dev/null +++ b/manticore/wasm/types.py @@ -0,0 +1,474 @@ +import typing +from dataclasses import dataclass +from ..core.smtlib import issymbolic, BitVec +from ctypes import * +import wasm +import struct +from ..core.state import Concretize + +# Do I like this? No. Is it necessary to get mypy to pass without destroying the WASM type system? Yes. +# Look how much cleaner the version below is instead of having a separate class for every type... +""" +U32: type = type("U32", (int,), {}) +U64: type = type("U64", (int,), {}) +""" + + +class U32(int): + pass + + +class U64(int): + pass + + +def debug(imm): + """ + Attempts to pull meaningful data out of an immediate, which has a dynamic GeneratedStructure type + + :param imm: the instruction immediate + :return: a printable representation of the immediate, or the immediate itself + """ + if hasattr(imm, "value"): + return imm.value + if hasattr(imm, "function_index"): + return f"Func Idx {imm.function_index}" + if hasattr(imm, "offset"): + return f"Offset {imm.offset}" + if hasattr(imm, "local_index"): + return f"Local {imm.local_index}" + if hasattr(imm, "global_index"): + return f"Global {imm.global_index}" + return getattr(imm, "value", imm) + + +def _reinterpret(ty1: type, ty2: type, val): + """ + Attempts to convert a value from one ctypes type to another + + :param ty1: The type of the value + :param ty2: The desired type of the value + :param val: The value itself + :return: The converted value + """ + ptr = pointer(ty1(val)) + # mypy worries that `contents` won't always exist for the pointer type + return cast(ptr, POINTER(ty2)).contents.value # type: ignore + + +class I32(int): + """ + Subclass of int that's restricted to 32-bit values + """ + + def __new__(cls, val): + val = struct.unpack("i", c_int32(int(val) & 0xFFFFFFFF))[0] + return super(I32, cls).__new__(cls, val) + + @classmethod + def cast(cls, other): + """ + :param other: Value to convert to I32 + :return: If other is symbolic, other. Otherwise, I32(other) + """ + if issymbolic(other): + return other + return cls(other) + + @staticmethod + def to_unsigned(val): + """ + Reinterprets the argument from a signed integer to an unsigned 32-bit integer + + :param val: Signed integer to reinterpret + :return: The unsigned equivalent + """ + return _reinterpret(c_int32, c_uint32, val) + + +class I64(int): + """ + Subclass of int that's restricted to 64-bit values + """ + + def __new__(cls, val): + val = struct.unpack("q", c_int64(int(val)))[0] + return super(I64, cls).__new__(cls, val) + + @classmethod + def cast(cls, other): + """ + :param other: Value to convert to I64 + :return: If other is symbolic, other. Otherwise, I64(other) + """ + if issymbolic(other): + return other + return cls(other) + + @staticmethod + def to_unsigned(val): + """ + Reinterprets the argument from a signed integer to an unsigned 64-bit integer + + :param val: Signed integer to reinterpret + :return: The unsigned equivalent + """ + return _reinterpret(c_int64, c_uint64, val) + + +class F32(float): + """ + Subclass of float that's restricted to 32-bit values + """ + + def __new__(cls, val): + if isinstance(val, int): + val = _reinterpret(c_int32, c_float, val & 0xFFFFFFFF) + val = struct.unpack("f", c_float(val))[0] + self = super(F32, cls).__new__(cls, val) + self.integer = val + return self + + @classmethod + def cast(cls, other): + """ + :param other: Value to convert to F32 + :return: If other is symbolic, other. Otherwise, F32(other) + """ + if issymbolic(other): + return other + return cls(other) + + +class F64(float): + """ + Subclass of float that's restricted to 64-bit values + """ + + def __new__(cls, val): + if isinstance(val, int): + val = _reinterpret(c_int64, c_double, val) + val = struct.unpack("d", c_double(val))[0] + self = super(F64, cls).__new__(cls, val) + self.integer = val + return self + + @classmethod + def cast(cls, other): + """ + :param other: Value to convert to F64 + :return: If other is symbolic, other. Otherwise, F64(other) + """ + if issymbolic(other): + return other + return cls(other) + + +ValType = type #: https://www.w3.org/TR/wasm-core-1/#syntax-valtype +# For reasons I don't understand, Tuple[Type] != Tuple[I32] +Value_t: typing.Tuple[typing.Type] = (I32, I64, F32, F64, BitVec) # type: ignore +# Value = typing.TypeVar('Value', I32, I64, F32, F64, BitVec) #: https://www.w3.org/TR/wasm-core-1/#syntax-val +Value = typing.Union[I32, I64, F32, F64, BitVec] #: https://www.w3.org/TR/wasm-core-1/#syntax-val + + +class Name(str): + pass + + +@dataclass +class FunctionType: + """ + https://www.w3.org/TR/wasm-core-1/#syntax-functype + """ + + param_types: typing.List[ValType] #: Sequential types of each of the parameters + result_types: typing.List[ValType] #: Sequential types of each of the return values + + +@dataclass +class LimitType: + """ + https://www.w3.org/TR/wasm-core-1/#syntax-limits + """ + + min: U32 + max: typing.Optional[U32] + + +@dataclass +class TableType: + """https://www.w3.org/TR/wasm-core-1/#syntax-tabletype""" + + limits: LimitType #: Minimum and maximum size of the table + elemtype: type #: the type ot the element. Currently, the only element type is `funcref` + + +@dataclass +class GlobalType: + """https://www.w3.org/TR/wasm-core-1/#syntax-globaltype""" + + mut: bool #: Whether or not this global is mutable + value: ValType #: The value of the global + + +# https://www.w3.org/TR/wasm-core-1/#indices%E2%91%A0 +class TypeIdx(U32): + pass + + +class FuncIdx(U32): + pass + + +class TableIdx(U32): + pass + + +class MemIdx(U32): + pass + + +class GlobalIdx(U32): + pass + + +class LocalIdx(U32): + pass + + +class LabelIdx(U32): + pass + + +@dataclass +class BlockImm: + sig: int + + +@dataclass +class BranchImm: + relative_depth: U32 + + +@dataclass +class BranchTableImm: + target_count: U32 + target_table: typing.List[U32] + default_target: U32 + + +@dataclass +class CallImm: + function_index: U32 + + +@dataclass +class CallIndirectImm: + type_index: U32 + reserved: U32 + + +@dataclass +class LocalVarXsImm: + local_index: U32 + + +@dataclass +class GlobalVarXsImm: + global_index: U32 + + +@dataclass +class MemoryImm: + flags: U32 + offset: U32 + + +@dataclass +class CurGrowMemImm: + reserved: bool + + +@dataclass +class I32ConstImm: + value: I32 + + +@dataclass +class I64ConstImm: + value: I64 + + +@dataclass +class F32ConstImm: + value: F32 + + +@dataclass +class F64ConstImm: + value: F64 + + +ImmType = typing.Union[ + BlockImm, + BranchImm, + BranchTableImm, + CallImm, + CallIndirectImm, + LocalVarXsImm, + GlobalVarXsImm, + MemoryImm, + CurGrowMemImm, + I32ConstImm, + F32ConstImm, + F64ConstImm, +] #: Types of all immediates + + +class Instruction: + """Internal instruction class that's pickle-friendly and works with the type system """ + + __slots__ = ["opcode", "mnemonic", "imm"] + opcode: int #: Opcode, used for dispatching instructions + mnemonic: str #: Used for debugging + imm: ImmType #: A class with the immediate data for this instruction + + def __init__(self, inst: wasm.decode.Instruction, imm=None): + self.opcode = inst.op.id + self.mnemonic = inst.op.mnemonic + self.imm = imm + + def __repr__(self): + return f"" + + +MemoryType = LimitType #: https://www.w3.org/TR/wasm-core-1/#syntax-memtype +ExternType = typing.Union[ + FunctionType, TableType, MemoryType, GlobalType +] #: https://www.w3.org/TR/wasm-core-1/#external-types%E2%91%A0 +WASMExpression = typing.List[Instruction] + + +def convert_instructions(inst_seq) -> WASMExpression: + """ + 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. + + :param inst_seq: Sequence of raw instructions to process + :return: The properly-typed instruction sequence in a format Manticore can use + """ + out = [] + if not isinstance(inst_seq, list): + inst_seq = list(wasm.decode_bytecode(inst_seq)) + i: wasm.decode.Instruction + for i in inst_seq: + if 0x02 <= i.op.id <= 0x04: + out.append(Instruction(i, BlockImm(i.imm.sig))) + elif i.op.id in (0x0C, 0x0D): + out.append(Instruction(i, BranchImm(i.imm.relative_depth))) + elif i.op.id == 0x0E: + out.append( + Instruction( + i, BranchTableImm(i.imm.target_count, i.imm.target_table, i.imm.default_target) + ) + ) + elif i.op.id == 0x10: + out.append(Instruction(i, CallImm(i.imm.function_index))) + elif i.op.id == 0x11: + out.append(Instruction(i, CallIndirectImm(i.imm.type_index, i.imm.reserved))) + elif 0x20 <= i.op.id <= 0x22: + out.append(Instruction(i, LocalVarXsImm(i.imm.local_index))) + elif i.op.id in (0x23, 0x24): + out.append(Instruction(i, GlobalVarXsImm(i.imm.global_index))) + elif 0x28 <= i.op.id <= 0x3E: + out.append(Instruction(i, MemoryImm(i.imm.flags, i.imm.offset))) + elif i.op.id in (0x3F, 0x40): + out.append(Instruction(i, CurGrowMemImm(i.imm.reserved))) + elif i.op.id == 0x41: + out.append(Instruction(i, I32ConstImm(i.imm.value))) + elif i.op.id == 0x42: + out.append(Instruction(i, I64ConstImm(i.imm.value))) + elif i.op.id == 0x43: + out.append(Instruction(i, F32ConstImm(i.imm.value))) + elif i.op.id == 0x44: + out.append(Instruction(i, F64ConstImm(i.imm.value))) + else: + out.append(Instruction(i)) + + return out + + +class Trap(Exception): + """ + Subclass of Exception, used for WASM errors + """ + + pass + + +class UnreachableInstructionTrap(Trap): + def __init__(self): + super().__init__("Tried to execute an unreachable instruction") + + +class ZeroDivisionTrap(Trap): + def __init__(self): + super().__init__("Zero division") + + +class OverflowDivisionTrap(Trap): + def __init__(self): + super().__init__("Overflow in signed division") + + +class NonExistentFunctionCallTrap(Trap): + def __init__(self): + super().__init__("Indirect call to non-existent function") + + +class OutOfBoundsMemoryTrap(Trap): + def __init__(self, addr): + super().__init__("Out of bounds memory access at " + hex(addr)) + + +class InvalidConversionTrap(Trap): + def __init__(self, ty, val): + super().__init__("Can't convert " + str(val) + " to " + str(ty)) + + +class TypeMismatchTrap(Trap): + def __init__(self, ty1, ty2): + super().__init__(f"Type signature mismatch: {ty1} != {ty2}") + + +class ConcretizeStack(Concretize): + """Tells Manticore to concretize the value `depth` values from the end of the stack. """ + + def __init__(self, depth: int, ty: type, message: str, expression, policy=None, **kwargs): + """ + :param depth: Index in the stack (should typically be negative) + :param ty: The type to cast the + :param message: Debug message describing the reason for concretization + :param expression: The expression to concretize, either a Value or a BitVec + """ + if policy is None: + policy = "ALL" + if policy not in self._ValidPolicies: + raise Exception(f'Policy ({policy}) must be one of: {", ".join(self._ValidPolicies)}') + + def setstate(state, value): + state.platform.stack.data[depth] = ty(value) + + self.setstate = setstate + self.expression = expression + self.policy = policy + self.message = f"Concretize: {message} (Policy: {policy})" + super().__init__(message, expression, setstate=self.setstate, **kwargs) + + +class MissingExportException(Trap): + def __init__(self, name): + self.name = name + super().__init__(f"Couldn't find an export called `{name}`") diff --git a/mypy.ini b/mypy.ini index 7a79ab4f..45f51de1 100644 --- a/mypy.ini +++ b/mypy.ini @@ -38,3 +38,6 @@ ignore_missing_imports = True [mypy-wrapt.*] ignore_missing_imports = True + +[mypy-wasm.*] +ignore_missing_imports = True diff --git a/readthedocs.yml b/readthedocs.yml index 87fa516b..56c58720 100644 --- a/readthedocs.yml +++ b/readthedocs.yml @@ -2,4 +2,4 @@ build: image: latest python: - version: 3.6 + version: 3.7 diff --git a/scripts/travis_test.sh b/scripts/travis_test.sh index 0af57f63..ea177d6f 100755 --- a/scripts/travis_test.sh +++ b/scripts/travis_test.sh @@ -74,6 +74,17 @@ make_vmtests(){ cd $DIR } +make_wasm_tests(){ + DIR=`pwd` + if [ ! -f .wasm_done ]; then + echo "Automaking WASM Tests" `pwd` + cd ./tests/wasm + ./generate_tests.sh + touch .wasm_done + fi + cd $DIR +} + install_truffle(){ curl -o- https://raw.githubusercontent.com/creationix/nvm/v0.34.0/install.sh | bash source ~/.nvm/nvm.sh @@ -147,7 +158,8 @@ case $1 in run_truffle_tests RV=$(($RV + $?)) ;; - + wasm) + make_wasm_tests ;& # Fallthrough native) ;& # Fallthrough ethereum) ;& # Fallthrough other) @@ -171,6 +183,8 @@ case $1 in RV=$(($RV + $?)) make_vmtests; run_tests_from_dir ethereum_vm RV=$(($RV + $?)) + make_wasm_tests; run_tests_from_dir wasm + RV=$(($RV + $?)) run_tests_from_dir other RV=$(($RV + $?)) run_examples diff --git a/setup.py b/setup.py index a2b843d4..63abdf7c 100644 --- a/setup.py +++ b/setup.py @@ -1,4 +1,5 @@ import os +import sys from setuptools import setup, find_packages on_rtd = os.environ.get("READTHEDOCS") == "True" @@ -12,6 +13,10 @@ def rtd_dependent_deps(): return ["z3-solver"] +version = sys.version_info +dataclass_deps = ["dataclasses"] if version.major == 3 and version.minor < 7 else [] + + # If you update native_deps please update the `REQUIREMENTS_TO_IMPORTS` dict in `utils/install_helper.py` # (we need to know how to import a given native dependency so we can check if native dependencies are installed) native_deps = ["capstone==4.0.1", "pyelftools", "unicorn==1.0.2rc1"] @@ -46,8 +51,11 @@ setup( "rlp", "ply", "crytic-compile>=0.1.1", + "wasm", + "black", ] - + rtd_dependent_deps(), + + rtd_dependent_deps() + + dataclass_deps, extras_require=extra_require, entry_points={"console_scripts": ["manticore = manticore.__main__:main"]}, ) diff --git a/tests/native/test_state.py b/tests/native/test_state.py index b6accd5f..d4cb7bd4 100644 --- a/tests/native/test_state.py +++ b/tests/native/test_state.py @@ -84,7 +84,7 @@ class StateTest(unittest.TestCase): expr = BitVecVariable(32, "tmp") self.state.constrain(expr > 4) self.state.constrain(expr < 7) - solved = self.state.solve_n(expr, 2) + solved = sorted(self.state.solve_n(expr, 2)) self.assertEqual(solved, [5, 6]) def test_solve_n2(self): diff --git a/tests/wasm/generate_tests.sh b/tests/wasm/generate_tests.sh new file mode 100755 index 00000000..785e1787 --- /dev/null +++ b/tests/wasm/generate_tests.sh @@ -0,0 +1,44 @@ +#!/usr/bin/env bash + +rm -rf */ +touch __init__.py + +wget -nc -nv -O wabt.tgz -c https://github.com/WebAssembly/wabt/releases/download/1.0.12/wabt-1.0.12-linux.tar.gz +wget -nc -nv -O spec.zip -c https://github.com/WebAssembly/spec/archive/ace189a8f906f4f0760656a2aa53b6dc7046e771.zip + +yes | unzip -q -j spec.zip 'spec-*/test/core/*' -d . +rm run.py README.md +rm spec.zip + +tar --wildcards --strip=1 -xf wabt.tgz 'wabt-*/wast2json' +rm wabt.tgz + +mkdir skipped_tests +while read skip; do + mv $skip.wast skipped_tests/ +done < skipped_test_sets + +for x in *"-"*.wast; do + mv -- "$x" "${x//-/_}" +done + +ls *.wast | sed 's/\.wast//g' > modules.txt + +cores=$(python -c "import multiprocessing; print(max(multiprocessing.cpu_count() - 2, 1))") + +cat > gen.sh << EOF +module=\$1 +echo "Preparing \$module" +mkdir _\$module +touch _\$module/__init__.py +./wast2json --debug-names \$module.wast -o _\$module/\$module.json +mv \$module.wast _\$module/ +python3 json2smc.py _\$module/\$module.json | black --quiet --fast - > _\$module/test_symbolic_\$module.py +python3 json2mc.py _\$module/\$module.json | black --quiet --fast - > _\$module/test_\$module.py +EOF + +chmod +x gen.sh +cat modules.txt | xargs -n1 -P"$cores" ./gen.sh +rm gen.sh + +exit 0 \ No newline at end of file diff --git a/tests/wasm/json2mc.py b/tests/wasm/json2mc.py new file mode 100644 index 00000000..3611cc1c --- /dev/null +++ b/tests/wasm/json2mc.py @@ -0,0 +1,166 @@ +import argparse +import json +from jinja2 import Environment, FileSystemLoader +from base64 import b64encode +from copy import copy + +parser = argparse.ArgumentParser("Generate Manticore tests from the WASM Spec") +parser.add_argument("filename", type=argparse.FileType("r"), help="JSON file output from wast2json") +args = parser.parse_args() + +data = json.load(args.filename)["commands"] +args.filename.close() + + +class Module: + def __init__(self, filename, tests, name=None): + self.name = filename.replace(".wasm", "").replace(".wast", "").replace(".", "_").strip() + self.filename = filename + self.tests = tests + self.registered_name = name + self.imports = [] + + def add_test(self, name, line, args, rets, type_="assert_return", mod_name=None): + self.tests.append( + { + "func": name, + "line": line, + "args": args, + "rets": rets, + "type": type_, + "mod_name": mod_name, + } + ) + + def __repr__(self): + return f"" + + +def convert_types(to_convert): + """ Convert unsigned ints from JSON into WASM Types (I32, F64, etc) """ + out = [] + for item in to_convert: + out.append(f"{item['type'].upper()}({item.get('value', 0)})") + return ", ".join(out) + + +env = Environment(loader=FileSystemLoader(".")) + + +def escape_null(in_str: str): + """Base64-encode function names if they contain nonprintable characters""" + if in_str.isprintable() and not any((c in in_str) for c in {'"', "'", ";"}): + return f'"{in_str}"' + else: + return f"str(b64decode(\"{b64encode(in_str.encode('utf-8')).decode('utf-8')}\"), 'utf-8')" + + +env.filters["escape_null"] = escape_null + +template = env.get_template("test_template.jinja2") + + +modules = [] +registered_modules = {} +imports = [] +current_module = None +for d in data: + + if d["type"] == "action": + if d["action"]["type"] == "invoke": + if isinstance(current_module, int): + modules[current_module].add_test( + d["action"]["field"], + d["line"], + convert_types(d["action"]["args"]), + convert_types(d["expected"]), + "action", + mod_name=d["action"].get("module", None), + ) + else: + raise NotImplementedError("action with action type: " + d["action"]["type"]) + elif d["type"] == "assert_exhaustion": + pass + elif d["type"] == "assert_invalid": + if current_module: + modules[current_module].imports = copy(imports) + current_module = None + elif d["type"] == "assert_malformed": + if current_module: + modules[current_module].imports = copy(imports) + current_module = None + elif d["type"] == "assert_return": + if d["action"]["type"] == "invoke": + if isinstance(current_module, int): + modules[current_module].add_test( + d["action"]["field"], + d["line"], + convert_types(d["action"]["args"]), + convert_types(d["expected"]), + mod_name=d["action"].get("module", None), + ) + elif d["action"]["type"] == "get": + modules[current_module].add_test( + d["action"]["field"], + d["line"], + [], + convert_types(d["expected"]), + "assert_global", + d["action"].get("module", None), + ) + else: + raise NotImplementedError("assert_return with action type: " + d["action"]["type"]) + elif d["type"] == "assert_return_arithmetic_nan": + # XXX Eventually implement, but if we raise here it eliminates other valid tests + # raise NotImplementedError("assert_return_arithmetic_nan") + pass + + elif d["type"] == "assert_return_canonical_nan": + # XXX Eventually implement, but if we raise here it eliminates other valid tests + # raise NotImplementedError("assert_return_canonical_nan") + pass + + elif d["type"] == "assert_trap": + if d["action"]["type"] == "invoke": + if isinstance(current_module, int): + modules[current_module].add_test( + d["action"]["field"], + d["line"], + convert_types(d["action"]["args"]), + convert_types(d["expected"]), + "assert_trap", + mod_name=d["action"].get("module", None), + ) + else: + raise NotImplementedError("assert_trap with action type: " + d["action"]["type"]) + elif d["type"] == "assert_uninstantiable": + if current_module: + modules[current_module].imports = copy(imports) + current_module = None + elif d["type"] == "assert_unlinkable": + if current_module: + modules[current_module].imports = copy(imports) + current_module = None + elif d["type"] == "module": + modules.append(Module(d["filename"], [], d.get("name", None))) + if current_module: + modules[current_module].imports = copy(imports) + if d.get("name", None): + imports.append({"type": "import", "name": d["name"], "filename": d["filename"]}) + current_module = len(modules) - 1 + if "name" in d: + registered_modules[d["name"]] = modules[current_module].filename + elif d["type"] == "register": # Allow a module to go by another name + maybe_name = d.get("name", False) + if maybe_name: # This is an alias for another registered module + imports.append({"type": "alias", "alias": d["as"], "orig": maybe_name}) + else: # This is an alias for the current module + imports.append( + {"type": "import", "name": d["as"], "filename": modules[current_module].filename} + ) + modules[current_module].registered_name = d["as"] + + if current_module: + modules[current_module].imports = copy(imports) + +print(template.render(modules=modules)) diff --git a/tests/wasm/json2smc.py b/tests/wasm/json2smc.py new file mode 100644 index 00000000..e9732036 --- /dev/null +++ b/tests/wasm/json2smc.py @@ -0,0 +1,162 @@ +import argparse +import json +from jinja2 import Environment, FileSystemLoader +from base64 import b64encode +import string + +parser = argparse.ArgumentParser("Generate Manticore tests from the WASM Spec") +parser.add_argument("filename", type=argparse.FileType("r"), help="JSON file output from wast2json") +args = parser.parse_args() + +data = json.load(args.filename)["commands"] +args.filename.close() + +# Individual unit tests that we skip due to timeouts or problematic statefulness +skip = { + "fib_L261", + "check-memory-zero_L87", + "check-memory-zero_L89", + "check-memory-zero_L91", + "check-memory-zero_L93", + "check-memory-zero_L95", + "check-memory-zero_L97", + "odd_L269", + "fib-i64_L527", +} +# Modules with statefeulness for which we disallow reinitialization +disallow_reinit_modules = { + "call_0", + "call_indirect_0", + "globals_0", + "memory_grow_0", + "memory_grow_3", +} + + +class Module: + def __init__(self, filename, tests): + self.name = filename.replace(".wasm", "").replace(".wast", "").replace(".", "_").strip() + self.filename = filename + self.tests = tests + self.allow_reinit = True if self.name not in disallow_reinit_modules else False + + def add_test(self, name, line, args, rets, type_="assert_return"): + self.tests.append({"func": name, "line": line, "args": args, "rets": rets, "type": type_}) + + def __repr__(self): + return f"" + + +def convert_args(to_convert): + """ + Convert a set of unsigned ints from JSON into an appropriate set of constraints + :param to_convert: + :return: + """ + out = [] + for idx, item in enumerate(to_convert): + if "32" in item["type"]: + out.append( + {"constraint": f"state.new_symbolic_value(32)", "val": int(item.get("value", 0))} + ) + elif "64" in item["type"]: + out.append( + {"constraint": f"state.new_symbolic_value(64)", "val": int(item.get("value", 0))} + ) + else: + raise RuntimeError("garbage type") + return out + + +def convert_rets(to_convert): + """Convert unsigned int from JSON into concrete values""" + out = [] + for item in to_convert: + out.append(f"{item['type'].upper()}({item.get('value', 0)})") + return ", ".join(out) + + +env = Environment(loader=FileSystemLoader(".")) + + +def escape_null(in_str: str): + """ Base-64 encode non-printable characters in test names so we can handle that obnoxious names module """ + if in_str.isprintable() and not any((c in in_str) for c in {'"', "'", ";"}): + return f'"{in_str}"' + else: + return f"str(b64decode(\"{b64encode(in_str.encode('utf-8')).decode('utf-8')}\"), 'utf-8')" + + +env.filters["escape_null"] = escape_null + +template = env.get_template("symbolic_test_template.jinja2") + + +modules = [] +current_module = None +for d in data: + if f"{d.get('action', {}).get('field', None)}_L{d['line']}" in skip: + continue + + if d["type"] == "action": + if d["action"]["type"] == "invoke": + if isinstance(current_module, int): + modules[current_module].add_test( + d["action"]["field"], + d["line"], + convert_args(d["action"]["args"]), + convert_rets(d["expected"]), + "action", + ) + else: + raise NotImplementedError("action with action type: " + d["action"]["type"]) + elif d["type"] == "assert_exhaustion": + pass + elif d["type"] == "assert_invalid": + current_module = None + elif d["type"] == "assert_malformed": + current_module = None + elif d["type"] == "assert_return": + if d["action"]["type"] == "invoke": + if isinstance(current_module, int): + modules[current_module].add_test( + d["action"]["field"], + d["line"], + convert_args(d["action"]["args"]), + convert_rets(d["expected"]), + ) + else: + raise NotImplementedError("assert_return with action type: " + d["action"]["type"]) + elif d["type"] == "assert_return_arithmetic_nan": + # XXX Eventually implement, but if we raise here it eliminates other valid tests + # raise NotImplementedError("assert_return_arithmetic_nan") + pass + + elif d["type"] == "assert_return_canonical_nan": + # XXX Eventually implement, but if we raise here it eliminates other valid tests + # raise NotImplementedError("assert_return_canonical_nan") + pass + + elif d["type"] == "assert_trap": + if d["action"]["type"] == "invoke": + if isinstance(current_module, int): + modules[current_module].add_test( + d["action"]["field"], + d["line"], + convert_args(d["action"]["args"]), + convert_rets(d["expected"]), + "assert_trap", + ) + else: + raise NotImplementedError("assert_trap with action type: " + d["action"]["type"]) + elif d["type"] == "assert_uninstantiable": + current_module = None + elif d["type"] == "assert_unlinkable": + current_module = None + elif d["type"] == "module": + modules.append(Module(d["filename"], [])) + current_module = len(modules) - 1 + elif d["type"] == "register": + raise NotImplementedError("register") + +print(template.render(modules=modules)) diff --git a/tests/wasm/skipped_test_sets b/tests/wasm/skipped_test_sets new file mode 100644 index 00000000..ffe58af4 --- /dev/null +++ b/tests/wasm/skipped_test_sets @@ -0,0 +1,7 @@ +conversions +f32 +f64 +float_exprs +float_literals +float_memory +float_misc diff --git a/tests/wasm/symbolic_test_template.jinja2 b/tests/wasm/symbolic_test_template.jinja2 new file mode 100644 index 00000000..e1c19725 --- /dev/null +++ b/tests/wasm/symbolic_test_template.jinja2 @@ -0,0 +1,139 @@ +{%block imports %} +import unittest +from os.path import dirname, abspath, join +from manticore.platforms import wasm +from manticore.wasm import ManticoreWASM +from manticore.wasm.types import I32, F32, I64, F64, Trap, FunctionType +from manticore.wasm.structure import TableInst, MemInst, GlobalInst, HostFunc +from manticore.core.plugin import Plugin +from manticore.core.state import TerminateState +from base64 import b64decode +import math + + +from manticore.utils import config +consts = config.get_group("core") +consts.mprocessing = consts.mprocessing.single + +def assertEqualNan(testcase, a_list, b): + """ b_list: list of exected return values + a_list: 3-nested lists: One for each state, containing one for each of the n possible return values, each containing the output of solver.get_all_values """ + assert len(a_list) == 1, f"Diverged into {len(a_list)} states!" + for state_a in a_list: + assert len(state_a) == len(b), f"Returned {len(a)} values! (Expected {len(b)})" + for a in state_a: + assert len(a) <= 1, "Found multiple possible values!" + for a_item, b_item in zip(a, b): + if isinstance(b_item, F32) and isinstance(a_item, int): + a_item = F32.cast(a_item) + if isinstance(b_item, F64) and isinstance(a_item, int): + a_item = F64.cast(a_item) + if math.isnan(b_item): + testcase.assertTrue(math.isnan(a_item)) + else: + testcase.assertAlmostEqual(a_item, b_item) +{% endblock %} + +def noarg(_ctx): + return [] +def onearg(_ctx, _c): + return [] +def twoarg(_ctx, _x, _y): + return [] + +spectest = { + "print": HostFunc(FunctionType([], []), noarg), + "print_i32": HostFunc(FunctionType([I32], []), onearg), + "print_i32_f32": HostFunc(FunctionType([I32, F32], []), twoarg), + "print_f64_f64": HostFunc(FunctionType([F64, F64], []), twoarg), + "print_f32": HostFunc(FunctionType([F32], []), onearg), + "print_f64": HostFunc(FunctionType([F64], []), onearg), + "global_i32": GlobalInst(I32(666), True), + "global_f32": GlobalInst(F32(666), True), + "global_f64": GlobalInst(F64(666), True), + "table": TableInst([None] * 10, 20), + "memory": MemInst([0x0] * 64 * 1024, 2) +} + +class RaiseExceptionPlugin(Plugin): + + def did_terminate_state_callback(self, current_state, exc): + if "raised Trap" in str(exc): + self.manticore.trapped = True + +{% for module in modules %} +class WASMTest_{{ module.name }}(unittest.TestCase): + _multiprocess_can_split_ = False + filename = join(dirname(abspath(__file__)), "{{ module.filename }}") + subtest_count = 0 + + def run(self, result=None): + result = super().run(result) + setattr(result, "testsRun", self.subtest_count + getattr(result, "testsRun", 0) - 1) + return result + + def test_{{ module.name }}(self): + m = ManticoreWASM(self.filename, sup_env={"spectest":spectest}, exec_start=True) + m.register_plugin(RaiseExceptionPlugin()) + + {% for test in module.tests %} + name = {{ test.func | escape_null }} + "_L{{test.line}}" + with self.subTest(msg=name): + print("======V======", name, "(Symbolic)", "======V======") + self.subtest_count += 1 + + if self.subtest_count % 50 == 0: + if {{module.allow_reinit}}: + print("Reinitializing Manticore object after 50 symbolic tests") + m = ManticoreWASM(self.filename, sup_env={"spectest":spectest}, exec_start=True) + m.register_plugin(RaiseExceptionPlugin()) + + def create_argv(state): + argv = [] + {% for arg in test.args %} + argv.append({{arg.constraint}}) + state.constrain(argv[-1] == {{arg.val}}) + {% endfor %} + return argv + + expected = [{{ test.rets }}] + {% if test.type == "assert_return" %} + with m.kill_timeout(150): + m.invoke(name={{ test.func | escape_null }}, argv_generator=create_argv) + setattr(m, 'trapped', False) + m.run() + self.assertFalse(getattr(m, 'trapped', False)) + if not getattr(m, '_killed', False): + rets = m.collect_returns(len(expected)) + m._reinit() + assertEqualNan(self, rets, expected) + else: + m._killed.value = False + print(name, "Timed Out, Reinitializing Manticore") + m = ManticoreWASM(self.filename, sup_env={"spectest":spectest}, exec_start=True) + m.register_plugin(RaiseExceptionPlugin()) + {% endif %} + {% if test.type == "assert_trap" %} + with m.kill_timeout(150): + m.invoke(name={{ test.func | escape_null }}, argv_generator=create_argv) + m.run() + self.assertTrue(getattr(m, 'trapped', False)) + if {{module.allow_reinit}}: + print("Reinitializing after Trap") + m = ManticoreWASM(self.filename, sup_env={"spectest":spectest}, exec_start=True) + m.register_plugin(RaiseExceptionPlugin()) + else: + m._reinit() + {% endif %} + {% if test.type == "action" %} + with m.kill_timeout(150): + m.invoke(name={{ test.func | escape_null }}, argv_generator=create_argv) + m.run() + m._reinit() + {% endif %} + {% endfor %} + +{% endfor %} + +if __name__ == "__main__": + unittest.main() diff --git a/tests/wasm/test_examples.py b/tests/wasm/test_examples.py new file mode 100644 index 00000000..c6af275e --- /dev/null +++ b/tests/wasm/test_examples.py @@ -0,0 +1,93 @@ +import unittest +from manticore.wasm import ManticoreWASM +from manticore.wasm.types import I32 +from manticore.core.plugin import Plugin +from pathlib import Path +import glob + + +def getchar(constraints, addr): + res = constraints.new_bitvec(32, "getchar_res") + constraints.add(res > 0) + constraints.add(res < 8) + return [res] + + +def arg_gen(state): + arg = state.new_symbolic_value(32, "collatz_arg") + state.constrain(arg > 3) + state.constrain(arg < 9) + state.constrain(arg % 2 == 0) + return [arg] + + +class CallCounterPlugin(Plugin): + def did_execute_instruction_callback(self, state, instruction): + with self.locked_context("counter", dict) as ctx: + val = ctx.setdefault(instruction.mnemonic, 0) + ctx[instruction.mnemonic] = val + 1 + + +wasm_file = str( + Path(__file__).parent.parent.parent.joinpath("examples", "wasm", "collatz", "collatz.wasm") +) + + +class TestExamples(unittest.TestCase): + def test_getchar(self): + m = ManticoreWASM(wasm_file, env={"getchar": getchar}) + m.invoke("main") + m.run() + results = [] + for idx, val_list in enumerate(m.collect_returns()): + results.append(val_list[0][0]) + + self.assertEqual(sorted(results), [0, 1, 2, 5, 7, 8, 16]) + + def test_symbolic_args(self): + m = ManticoreWASM(wasm_file, env={}) + m.invoke("collatz", arg_gen) + m.run() + + results = [] + for idx, val_list in enumerate(m.collect_returns()): + results.append(val_list[0][0]) + + self.assertEqual(sorted(results), [2, 3, 8]) + + m.finalize() + + inputs = [] + for fn in glob.glob(m.workspace + "/*.input"): + with open(fn, "r") as f: + raw = f.read().strip() + inputs.append(int(raw.replace("collatz_arg: ", ""))) + + self.assertEqual(sorted(inputs), [4, 6, 8]) + + def test_plugin(self): + def arg_gen(_state): + return [I32(1337)] + + m = ManticoreWASM(wasm_file) + counter_plugin = CallCounterPlugin() + m.register_plugin(counter_plugin) + m.invoke("collatz", arg_gen) + m.run() + + # counts = m.context.get("").get("counter") + counts = counter_plugin.context.get("counter") + + self.assertEqual(counts["br_if"], 45) + self.assertEqual(counts["loop"], 44) + self.assertEqual(counts["i32.add"], 88) + + results = [] + for idx, val_list in enumerate(m.collect_returns()): + results.append(val_list[0][0]) + + self.assertEqual(sorted(results), [44]) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/wasm/test_stack_supplemental.py b/tests/wasm/test_stack_supplemental.py new file mode 100644 index 00000000..071e4eae --- /dev/null +++ b/tests/wasm/test_stack_supplemental.py @@ -0,0 +1,113 @@ +import unittest +from manticore.wasm import ManticoreWASM +from manticore.wasm.types import I32 +from manticore.core.plugin import Plugin +from manticore.wasm.structure import Stack, AtomicStack + +from pathlib import Path + + +class StackTrackerPlugin(Plugin): + def will_pop_item_callback(self, state, depth): + with self.locked_context("push_pop_seq", list) as seq: + seq.append("+") + + def did_pop_item_callback(self, state, item, depth): + with self.locked_context("push_pop_seq", list) as seq: + seq.append("-") + + +wasm_file = str( + Path(__file__).parent.parent.parent.joinpath("examples", "wasm", "collatz", "collatz.wasm") +) + + +class TestStack(unittest.TestCase): + def test_trace(self): + """ + This checks the sequence of pushes and pops that take place during an example execution. + That sequence isn't meant to be invariant, so if you change the implementation and break + this test, by all means, replace it with the new sequence. + :return: + """ + + def arg_gen(_state): + return [I32(1337)] + + m = ManticoreWASM(wasm_file) + tracker_plugin = StackTrackerPlugin() + m.register_plugin(tracker_plugin) + m.invoke("collatz", arg_gen) + m.run() + + results = [] + for idx, val_list in enumerate(m.collect_returns()): + results.append(val_list[0][0]) + + self.assertEqual(sorted(results), [44]) + push_pop_seq = "".join(tracker_plugin.context.get("push_pop_seq")) + + self.assertEqual(push_pop_seq, "+-" * 892) + + def test_has_at_least(self): + s = Stack() + s.push(I32(1)) + self.assertFalse(s.has_at_least(I32, 2)) + s.push(I32(2)) + self.assertTrue(s.has_at_least(I32, 2)) + + def test_empty(self): + s = Stack() + with AtomicStack(s) as a: + a.push(1) + a.push(2) + + self.assertEqual(len(s.data), 2) + self.assertFalse(a.empty()) + a.pop() + a.pop() + + self.assertTrue(a.empty()) + self.assertTrue(s.empty()) + + def test_rollback(self): + orig = [i for i in range(10)] + + s = Stack() + for i in range(10): + s.push(i) + a = AtomicStack(s) + self.assertEqual(list(s.data), orig) + + a.push(10) + self.assertEqual(list(s.data), [i for i in range(11)]) + + a.rollback() + self.assertEqual(list(s.data), orig) + + for i in range(3): + a.pop() + self.assertEqual(list(s.data), [i for i in range(7)]) + + a.rollback() + self.assertEqual(list(s.data), orig) + + a.pop() + a.pop() + for i in range(9): + a.push(20 + i) + a.pop() + a.pop() + for i in range(5): + a.push(30 + i) + + self.assertEqual( + list(s.data), [0, 1, 2, 3, 4, 5, 6, 7, 20, 21, 22, 23, 24, 25, 26, 30, 31, 32, 33, 34] + ) + + a.rollback() + self.assertEqual(list(s.data), orig) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/wasm/test_template.jinja2 b/tests/wasm/test_template.jinja2 new file mode 100644 index 00000000..cdeba6f0 --- /dev/null +++ b/tests/wasm/test_template.jinja2 @@ -0,0 +1,121 @@ +{%block imports %} +import unittest +from os.path import dirname, abspath, join +from manticore.platforms import wasm +from manticore.core import state +from manticore.core.smtlib import Operators, ConstraintSet +from manticore.wasm.types import I32, F32, I64, F64, Trap, FunctionType +from manticore.wasm.structure import TableInst, MemInst, GlobalInst, HostFunc +from base64 import b64decode +import math + +def assertEqualNan(testcase, a, b): + if len(b) and len(a) and math.isnan(b[0]): + testcase.assertTrue(math.isnan(a[0])) + else: + assert len(a) == len(b) + for a_item, b_item in zip(a, b): + # Tests for equality out to 10^-7, helpful for avoiding floating-point rounding errors + testcase.assertAlmostEqual(a_item, b_item) +{% endblock %} + + +spectest = { + "print": HostFunc(FunctionType([], []), lambda ct: []), + "print_i32": HostFunc(FunctionType([I32], []), lambda ct, x: []), + "print_i32_f32": HostFunc(FunctionType([I32, F32], []), lambda ct, x, y: []), + "print_f64_f64": HostFunc(FunctionType([F64, F64], []), lambda ct, x, y: []), + "print_f32": HostFunc(FunctionType([F32], []), lambda ct, x: []), + "print_f64": HostFunc(FunctionType([F64], []), lambda ct, x: []), + "global_i32": GlobalInst(I32(666), True), + "global_f32": GlobalInst(F32(666), True), + "global_f64": GlobalInst(F64(666), True), + "table": TableInst([None] * 10, 20), + "memory": MemInst([0x0] * 64 * 1024, 2) +} + + +{% for module in modules %} +class WASMTest_{{ module.name }}(unittest.TestCase): + _multiprocess_can_split_ = False + filename = join(dirname(abspath(__file__)), "{{ module.filename }}") + subtest_count = 0 + + def run(self, result=None): + result = super().run(result) + setattr(result, "testsRun", self.subtest_count + getattr(result, "testsRun", 0) - 1) + return result + + def test_{{ module.name }}(self): + print("\n======V======", "{{ module.name }}", "======V======") + constraints = ConstraintSet() + {% if module.registered_name != None %} + world = wasm.WASMWorld(self.filename, name="{{ module.registered_name }}") + {% else %} + world = wasm.WASMWorld(self.filename) + {% endif %} + world.set_env(spectest, mod_name="spectest") + + {% for item in module.imports %} + {% if item['type'] == "import" %} + world.register_module("{{ item['name'] }}", join(dirname(abspath(__file__)), "{{ item['filename'] }}")) + world.import_module("{{ item['name'] }}", True, False) + {% endif %} + {% if item['type'] == "alias" %} + world.register_module("{{ item['alias'] }}", "{{ item['orig'] }}") + {% endif %} + {% endfor %} + + world.instantiate({}, {}, exec_start=True) + {% for test in module.tests %} + with self.subTest(msg={{ test.func | escape_null }} + "_L{{test.line}}"): + print("===V===", {{ test.func | escape_null }} + "_L{{test.line}}", "===V===") + self.subtest_count += 1 + {% if test.args | length > 0 %} + argv=[{{ test.args }}] + {% else %} + argv=[] + {% endif %} + {% if test.mod_name != None %} + module = "{{ test.mod_name }}" + world.import_module(module, True, False) + {% else %} + module = None + {% endif %} + expected = [{{ test.rets }}] + {% if test.type == "assert_return" %} + world.invoke(name={{ test.func | escape_null }}, argv=argv, module=module) + try: + real = world.exec_for_test({{ test.func | escape_null }}, module=module) + assertEqualNan(self, real, expected) + except NotImplementedError as e: + self.skipTest(f"NotImplementedError: {str(e)}") + {% endif %} + {% if test.type == "assert_global" %} + {% if test.mod_name != None %} + assertEqualNan(self, [world.get_export("{{ test.func }}", "{{ test.mod_name }}").value], expected) + {% else %} + assertEqualNan(self, [world.get_export("{{ test.func }}").value], expected) + {% endif %} + {% endif %} + {% if test.type == "assert_trap" %} + world.invoke(name={{ test.func | escape_null }}, argv=argv, module=module) + with self.assertRaises(Trap): + try: + world.exec_for_test({{ test.func | escape_null }}, module=module) + except NotImplementedError as e: + self.skipTest(f"NotImplementedError: {str(e)}") + {% endif %} + {% if test.type == "action" %} + world.invoke(name={{ test.func | escape_null }}, argv=argv, module=module) + try: + world.exec_for_test({{ test.func | escape_null }}, module=module) + except NotImplementedError as e: + self.skipTest(f"NotImplementedError: {str(e)}") + {% endif %} + {% endfor %} + +{% endfor %} + +if __name__ == "__main__": + unittest.main()