trailofbits
diff --git a/‎.travis.yml
Lines changed: 3 additions & 2 deletions b/‎.travis.yml
Lines changed: 3 additions & 2 deletions
diff --git a/‎docs/index.rst
Lines changed: 1 addition & 0 deletions b/‎docs/index.rst
Lines changed: 1 addition & 0 deletions
diff --git a/‎docs/wasm.rst
Lines changed: 42 additions & 0 deletions b/‎docs/wasm.rst
Lines changed: 42 additions & 0 deletions
diff --git a/‎examples/wasm/collatz/collatz.c
Lines changed: 15 additions & 0 deletions b/‎examples/wasm/collatz/collatz.c
Lines changed: 15 additions & 0 deletions
diff --git a/‎examples/wasm/collatz/collatz.py
Lines changed: 145 additions & 0 deletions b/‎examples/wasm/collatz/collatz.py
Lines changed: 145 additions & 0 deletions
diff --git a/‎examples/wasm/collatz/collatz.wasm
268 Bytes b/‎examples/wasm/collatz/collatz.wasm
268 Bytes
diff --git a/‎examples/wasm/collatz/collatz.wat
Lines changed: 116 additions & 0 deletions b/‎examples/wasm/collatz/collatz.wat
Lines changed: 116 additions & 0 deletions
diff --git a/‎manticore/__main__.py
Lines changed: 3 additions & 0 deletions b/‎manticore/__main__.py
Lines changed: 3 additions & 0 deletions
diff --git a/‎manticore/core/manticore.py
Lines changed: 1 addition & 1 deletion b/‎manticore/core/manticore.py
Lines changed: 1 addition & 1 deletion
diff --git a/‎manticore/core/smtlib/operators.py
Lines changed: 2 additions & 0 deletions b/‎manticore/core/smtlib/operators.py
Lines changed: 2 additions & 0 deletions
@@ -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"
 
@@ -14,6 +14,7 @@ Manticore is a symbolic execution tool for analysis of binaries and smart contra
    states
    evm
    native
+   wasm
    plugins
    gotchas
 
 
@@ -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:
@@ -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(">"));
+}
@@ -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()
@@ -0,0 +1,116 @@
+(module
+ (type $FUNCSIG$i (func (result i32)))
+ (type $FUNCSIG$ii (func (param i32) (result i32)))
+ (import "env" "getchar" (func $getchar (param i32) (result i32)))
+ (table 0 anyfunc)
+ (memory $0 1)
+ (data (i32.const 16) ">\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)
+ )
+)
@@ -10,6 +10,7 @@
 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)
 
@@ -327,7 +327,7 @@ def _fork(self, state, expression, policy="ALL", setstate=None):
         to the ready list.
 
         """
-        assert isinstance(expression, Expression)
+        assert isinstance(expression, Expression), f"{type(expression)} is not an Expression"
 
         if setstate is None:
 
 
@@ -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
-Original file line number
+Diff line change
    states
    evm
    native
 +   wasm
    plugins
    gotchas