Merge branch 'master' into native-arb-cf-redirect-detector

* master: (28 commits)
  AArch64: fix ldrb size (#1433)
  System Call Audit (#1384)
  ManticoreBase refactor (#1385)
  Add missing checks for ARM boundaries (#1429)
  aarch64: add instruction tests: T-U (#1423)
  aarch64: add instruction tests: M-S (#1422)
  aarch64: add instruction tests: C-L (#1421)
  aarch64: add instruction tests: A-B (#1420)
  aarch64: add everything except instructions (#1418)
  fixup: support ARM64 in '_reg_name'
  Revert "fixup: remove x86-specific code from '_reg_name'"
  review: avoid wildcard imports
  review: rename the file
  fixup: remove x86-specific code from '_reg_name'
  fixup: do not use relative imports
  Generates a more sensible symbolic default for constructor arguments (#1414)
  aarch64: add instructions
  aarch64: add everything except instructions
  Switches the Travis-CI badge from .org to .com (#1416)
  Performance optimization : use set instead of list (#1415)
  ...

.codeclimate.yml

@@ -13,13 +13,13 @@ checks:
     config:
       threshold: 9000
   method-complexity:
-    enabled: true
+    enabled: false
     config:
       threshold: 40
   method-count:
-    enabled: true
+    enabled: false
     config:
-      threshold: 35
+      threshold: 45
   method-lines:
     enabled: true
     config:

.travis.yml

@@ -14,7 +14,7 @@ stages:
 env:
   global:
     - CC_TEST_REPORTER_ID=db72f1ed59628c16eb0c00cbcd629c4c71f68aa1892ef42d18c7c2b8326f460a
-    - JOB_COUNT=2 # Two jobs generate test coverage
+    - JOB_COUNT=3 # Three jobs generate test coverage: ethereum, native, and other
     - PYTHONWARNINGS="default::ResourceWarning" # Enable ResourceWarnings
   matrix:
     - TEST_TYPE=examples

README.md

@@ -5,7 +5,7 @@
 <br />
 
 
-[![Build Status](https://travis-ci.org/trailofbits/manticore.svg?branch=master)](https://travis-ci.org/trailofbits/manticore)
+[![Build Status](https://travis-ci.com/trailofbits/manticore.svg?branch=master)](https://travis-ci.com/trailofbits/manticore)
 [![PyPI version](https://badge.fury.io/py/manticore.svg)](https://badge.fury.io/py/manticore)
 [![Slack Status](https://empireslacking.herokuapp.com/badge.svg)](https://empireslacking.herokuapp.com)
 [![Documentation Status](https://readthedocs.org/projects/manticore/badge/?version=latest)](http://manticore.readthedocs.io/en/latest/?badge=latest)
@@ -37,13 +37,13 @@ Manticore has a command line interface which can be used to easily symbolically
 Use the CLI to explore possible states in Ethereum smart contracts. Manticore includes _detectors_ that flag potentially vulnerable code in discovered states; output from them will be written to stdout and the results directory.
 Solidity smart contracts must have a `.sol` extension for analysis by Manticore. See a [demo](https://asciinema.org/a/154012).
 
-```
+```bash
 $ manticore ./path/to/contract.sol  # runs, and creates a mcore_* directory with analysis results
 ```
 
 The command line can also be used to simply explore a Linux binary:
 
-```
+```bash
 $ manticore ./path/to/binary        # runs, and creates a mcore_* directory with analysis results
 $ manticore ./path/to/binary ab cd  # use concrete strings "ab", "cd" as program arguments
 $ manticore ./path/to/binary ++ ++  # use two symbolic strings of length two as program arguments
@@ -114,7 +114,7 @@ m.run()
 
 Install and try Manticore in a few shell commands:
 
-```
+```bash
 # Install system dependencies
 sudo apt-get update && sudo apt-get install python3 python3-pip -y
 
@@ -139,7 +139,7 @@ python3 count_instructions.py ../linux/helloworld
 
 You can also use Docker to quickly install and try Manticore:
 
-```
+```bash
 # Run container with a shared examples/ directory
 # Note that `--rm` will make the container be deleted if you exit it
 # (if you want to persist data from the container, use docker volumes)
@@ -173,15 +173,15 @@ install these also, substitute `manticore[native]` for `manticore` in any `pip`
 
 Option 1: Perform a user install (requires `~/.local/bin` in your `PATH`).
 
-```
+```bash
 echo "PATH=\$PATH:~/.local/bin" >> ~/.profile
 source ~/.profile
 pip3 install --user manticore
 ```
 
 Option 2: Use a virtual environment (requires [virtualenvwrapper](https://virtualenvwrapper.readthedocs.io/en/latest/) or [similar](https://virtualenv.pypa.io/en/stable/)).
 
-```
+```bash
 sudo pip3 install virtualenvwrapper
 echo "source /usr/local/bin/virtualenvwrapper.sh" >> ~/.profile
 source ~/.profile
@@ -191,13 +191,13 @@ sudo ./manticore/bin/pip3 install manticore
 
 Option 3: Perform a system install.
 
-```
+```bash
 sudo pip3 install manticore
 ```
 
 Option 4: Install via Docker.
 
-```
+```bash
 docker pull trailofbits/manticore
 ```
 
@@ -207,7 +207,7 @@ For installing a development version of Manticore, see our [wiki](https://github
 
 If you use Mac OS X you may need to install dependencies manually:
 
-```
+```bash
 brew install capstone
 export MACOS_UNIVERSAL=no && pip install capstone
 
@@ -217,7 +217,7 @@ UNICORN_QEMU_FLAGS="--python=`whereis python`" pip install unicorn
 
 ## Getting Help
 
-Feel free to stop by our [Slack channel](https://empirehacking.slack.com/messages/C3PTWK7UM) for help on using or extending Manticore.
+Feel free to stop by our #manticore slack channel in [Empire Hacking](https://empireslacking.herokuapp.com/) for help using or extending Manticore.
 
 
 Documentation is available in several places:

examples/evm/coverage.sol

@@ -2,7 +2,6 @@
 `explore` is the first level of exploration; you have to call it multiple times to explore the path
 `explore2` is a bit more complex; the owner has to call first the `enable_exploration` function
 */
-pragma solidity ^0.4.15;
 
 contract Coverage{
     address private owner;
@@ -74,7 +73,7 @@ contract Coverage{
         if(give){
             remove(msg.sender, value);
             add(user, value);
-            Give(msg.sender, user, value);
+            emit Give(msg.sender, user, value);
         }
         else{
             if( balances[user] > balances[msg.sender]){
@@ -84,7 +83,7 @@ contract Coverage{
                 value = diff >value ? value : diff;
                 add(msg.sender, value);
                 remove(user, value);
-                Take(msg.sender, user, value);
+                emit Take(msg.sender, user, value);
             }
             else{
                 // If you try to take to someone poorer than you
@@ -104,7 +103,7 @@ contract Coverage{
         if(give){
             remove(msg.sender, value);
             add(user, value);
-            Give(msg.sender, user, value);
+            emit Give(msg.sender, user, value);
         }
         else{
             uint diff;
@@ -113,7 +112,7 @@ contract Coverage{
             value = diff >value ? value : diff;
             add(msg.sender, value);
             remove(user, value);
-            Take(msg.sender, user, value);
+            emit Take(msg.sender, user, value);
         }
     }
 }

examples/evm/simple_int_overflow.sol

@@ -1,4 +1,3 @@
-pragma solidity ^0.4.15;
 contract Overflow {
     uint private sellerBalance=0;
 

examples/evm/simple_multi_func.sol

@@ -1,5 +1,3 @@
-pragma solidity ^0.4.13;
-
 contract Test {
     event Log(string);
     mapping(address => uint) private balances;

examples/evm/simple_value_check.sol

@@ -1,13 +1,12 @@
-pragma solidity ^0.4.13;
 
 contract Test {
     event Log(string);
 
     function target() payable public {
         if (msg.value > 10)
-            Log("Value greater than 10");
+            emit Log("Value greater than 10");
         else
-            Log("Value less or equal than 10");
+            emit Log("Value less or equal than 10");
 
     } 
 

examples/evm/two_tx_ovf.sol

@@ -1,5 +1,3 @@
-pragma solidity ^0.4.15;
-
 contract SymExExample {
     uint did_init = 0;
 
@@ -9,18 +7,18 @@ contract SymExExample {
     function test_me(int input) {
         if (did_init == 0) {
             did_init = 1;
-            Log("initialized");
+            emit Log("initialized");
             return;
         }
 
         if (input < 42) {
             // safe
-            Log("safe");
+            emit Log("safe");
             return;
         } else {
             // overflow possibly!
             int could_overflow = input + 1;
-            Log("overflow");
+            emit Log("overflow");
         }
 
     }

examples/evm/umd_example.sol

@@ -2,8 +2,6 @@
 // by Michael Hicks, University of Maryland.
 // https://www.cs.umd.edu/~mwh/se-tutorial/symbolic-exec.pdf
 
-pragma solidity ^0.4.15;
-
 contract SymExExample {
 
 

examples/script/aarch64/basic.c

@@ -0,0 +1,28 @@
+// gcc -g -static -o basic basic.c
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <unistd.h>
+
+int main(int argc, char* argv[], char* envp[]){
+    unsigned int cmd;
+
+    if (read(0, &cmd, sizeof(cmd)) != sizeof(cmd))
+    {
+        printf("Error reading stdin!");
+        exit(-1);
+    }
+
+    if (cmd > 0x41)
+    {
+        printf("Message: It is greater than 0x41\n");
+    }
+    else 
+    {
+        printf("Message: It is less than or equal to 0x41\n");
+    }
+
+return 0;
+}
+
+

examples/script/aarch64/basic.py

@@ -0,0 +1,72 @@
+#!/usr/bin/env python3
+
+import os
+import struct
+import sys
+
+from manticore.native import Manticore
+
+# Examples:
+# printf "\x41\x00\x00\x00" | PYTHONPATH=. ./examples/script/aarch64/basic.py
+# printf "++\x00\x00"       | PYTHONPATH=. ./examples/script/aarch64/basic.py
+# printf "++++"             | PYTHONPATH=. ./examples/script/aarch64/basic.py
+# printf "ffffff"           | PYTHONPATH=. ./examples/script/aarch64/basic.py
+
+DIR = os.path.dirname(__file__)
+FILE = os.path.join(DIR, 'basic')
+STDIN = sys.stdin.readline()
+
+# Avoid writing anything to 'STDIN' here.  Do it in the 'init' hook as that's
+# more flexible.
+m = Manticore(FILE, concrete_start='', stdin_size=0)
+
+
+@m.init
+def init(m, ready_states):
+    for state in ready_states:
+        state.platform.input.write(state.symbolicate_buffer(STDIN, label='STDIN'))
+
+
+# Hook the 'if' case.
+@m.hook(0x4006bc)
+def hook_if(state):
+    print('hook if')
+    state.abandon()
+
+
+# Hook the 'else' case.
+@m.hook(0x4006cc)
+def hook_else(state):
+    print('hook else')
+    # See how the constraints are affected by input.
+    print_constraints(state, 6)
+
+    w0 = state.cpu.W0
+
+    if isinstance(w0, int):  # concrete
+        print(hex(w0))
+    else:
+        print(w0)            # symbolic
+
+    solved = state.solve_one(w0)
+    print(struct.pack("<I", solved))
+
+
+# Hook 'puts' in the 'else' case.
+@m.hook(0x4006d4)
+def hook_puts(state):
+    print('hook puts')
+    cpu = state.cpu
+    print(cpu.read_string(cpu.X0))
+
+
+def print_constraints(state, nlines):
+    i = 0
+    for c in str(state.constraints).split('\n'):
+        if i >= nlines:
+            break
+        print(c)
+        i += 1
+
+
+m.run()

examples/script/aarch64/hello42.c

@@ -0,0 +1,8 @@
+// gcc -g -static -o hello42 hello42.c
+#include <stdio.h>
+
+int main()
+{
+  puts("hello");
+  return 42;
+}

examples/script/aarch64/hello42.py

@@ -0,0 +1,50 @@
+#!/usr/bin/env python3
+
+import os
+
+from manticore.native import Manticore
+
+# Modified 'count_instructions.py' to demonstrate execution of a
+# statically-linked "Hello, world!" AArch64 binary.
+
+DIR = os.path.dirname(__file__)
+FILE = os.path.join(DIR, 'hello42')
+
+if __name__ == '__main__':
+    m = Manticore(FILE)
+
+    with m.locked_context() as context:
+        context['count'] = 0
+
+    @m.hook(None)
+    def explore(state):
+        with m.locked_context() as context:
+            context['count'] += 1
+
+            if state.cpu.PC == 0x406f10:  # puts
+                s = state.cpu.read_string(state.cpu.X0)
+                assert s == 'hello'
+                print(f'puts argument: {s}')
+
+            elif state.cpu.PC == 0x40706c:  # puts result
+                result = state.cpu.X0
+                assert result >= 0
+                print(f'puts result: {result}')
+
+            elif state.cpu.PC == 0x415e50:  # exit
+                status = state.cpu.X0
+                syscall = state.cpu.X8
+                assert syscall == 94  # sys_exit_group
+                print(f'exit status: {status}')
+
+    def execute_instruction(self, insn, msg):
+        print(f'{msg}: 0x{insn.address:x}: {insn.mnemonic} {insn.op_str}')
+
+    m.subscribe('will_execute_instruction', lambda self, state, pc, insn:
+                execute_instruction(self, insn, 'next'))
+    m.subscribe('did_execute_instruction', lambda self, state, last_pc, pc, insn:
+                execute_instruction(self, insn, 'done'))
+
+    m.run(procs=1)
+
+    print(f"Executed {m.context['count']} instructions")