Remove Keystone from existing tests (trailofbits#1684)

.github/workflows/ci.yml

@@ -34,7 +34,7 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        type: ["ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "wasm", "wasm_sym", "other"]
+        type: ["ethereum_truffle", "ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "wasm", "wasm_sym", "other"]
     steps:
     - uses: actions/checkout@v1
     - name: Set up Python 3.6
@@ -52,11 +52,7 @@ jobs:
         # Install solc unconditionally because it only takes a second or two
         sudo wget -O /usr/bin/solc https://github.com/ethereum/solidity/releases/download/v0.4.24/solc-static-linux
         sudo chmod +x /usr/bin/solc
-        EXTRAS="dev-noks"
-        if [[ "$TEST_TYPE" == "native" ]]; then
-          EXTRAS="dev"
-        fi
-        pip install -e .[$EXTRAS]
+        pip install -e ".[dev-noks]"
     - name: Run Tests
       env:
         TEST_TYPE: ${{ matrix.type }}
@@ -157,25 +153,23 @@ jobs:
             mkdir truffle_tests
             cd truffle_tests
             truffle unbox metacoin
-            manticore . --contract MetaCoin --workspace output
-            ### The original comment says we should get 41 states, but after implementing the shift
-            ### insructions, we get 31. Was the original comment a typo?
-
-            # The correct answer should be 41
-            # but Manticore fails to explore the paths due to the lack of the 0x1f opcode support
-            # see https://github.com/trailofbits/manticore/issues/1166
-            # if [ "$(ls output/*tx -l | wc -l)" != "41" ]; then
+            coverage run -m manticore . --contract MetaCoin --workspace output
+            # Truffle smoke test. We test if manticore is able to generate states
+            # from a truffle project. 
             if [ "$(ls output/*tx -l | wc -l)" != "34" ]; then
                 echo "Truffle test failed" `ls output/*tx -l | wc -l` "!= 34"
                 return 1
             fi
             echo "Truffle test succeded"
+            coverage xml
             cd ..
+            cp truffle_tests/coverage.xml .
             return 0
         }
 
         run_tests_from_dir() {
             DIR=$1
+            echo "Running only the tests from 'tests/$DIR' directory"
             pytest --durations=100 --cov=manticore -n auto "tests/$DIR"
             coverage xml
         }
@@ -203,30 +197,24 @@ jobs:
         case $TEST_TYPE in
             ethereum_vm)
                 make_vmtests
-                echo "Running only the tests from 'tests/$TEST_TYPE' directory"
                 run_tests_from_dir $TEST_TYPE
-                RV=$?
-
+                ;;
+            ethereum_truffle)
                 echo "Running truffle test"
                 install_truffle
                 run_truffle_tests
-                RV=$(($RV + $?))
                 ;;
             wasm)
                 make_wasm_tests
-                echo "Running only the tests from 'tests/$TEST_TYPE' directory"
                 run_tests_from_dir $TEST_TYPE
-                RV=$?
                 ;;
             wasm_sym)
-                make_wasm_sym_tests ;&
+                make_wasm_sym_tests ;&  # Fallthrough
             native)                 ;&  # Fallthrough
             ethereum)               ;&  # Fallthrough
             ethereum_bench)         ;&  # Fallthrough
             other)
-                echo "Running only the tests from 'tests/$TEST_TYPE' directory"
                 run_tests_from_dir $TEST_TYPE
-                RV=$?
                 ;;
             examples)
                 run_examples

codecov.yml

@@ -2,7 +2,7 @@ comment: false
 
 codecov:
   notify:
-    # We have 8 test steps that produce coverage data.
+    # We have 9 test steps that produce coverage data.
     # If we add or remove any, we need to change this number.
-    after_n_builds: 8
+    after_n_builds: 9
     wait_for_ci: yes

docs/index.rst

@@ -17,6 +17,7 @@ Manticore is a symbolic execution tool for analysis of binaries and smart contra
    wasm
    plugins
    gotchas
+   utilities
 
 
 Indices and tables

docs/utilities.rst

@@ -0,0 +1,7 @@
+Utilities
+---------
+
+Logging
+^^^^^^^
+
+.. autofunction:: manticore.utils.log.set_verbosity

examples/linux/Makefile

@@ -3,20 +3,22 @@ CFLAGS=-O3 -static
 NOSTDLIBFLAGS=-fno-builtin -static -nostdlib -fomit-frame-pointer -fno-stack-protector
 PYTHON=python3
 
-EXAMPLES=      \
-  arguments    \
-  basic        \
-  crackme      \
-  fclose       \
-  fileio       \
-  helloworld   \
-  ibranch      \
-  indexhell    \
-  sendmail     \
-  simpleassert \
-  simple_copy  \
-  sindex       \
-  strncmp      \
+EXAMPLES=        \
+  arguments      \
+  basic          \
+  crackme        \
+  fclose         \
+  fileio         \
+  helloworld     \
+  ibranch        \
+  indexhell      \
+  ioctl_bogus    \
+  ioctl_socket   \
+  sendmail       \
+  simpleassert   \
+  simple_copy    \
+  sindex         \
+  strncmp        \
 
 OTHER_EXAMPLES=nostdlib
 

examples/linux/fileio.c

@@ -25,7 +25,7 @@ int main(int argc, const char **argv) {
         return 3;
     }
 
-    if (strcmp("my voice is my passport verify me", line) == 0) {
+    if (strcmp("open sesame", line) == 0) {
         fprintf(stdout, "Welcome!\n");
         return 0;
     } else {

examples/linux/ioctl_bogus.c

@@ -0,0 +1,20 @@
+// This example demonstrates a particular syscall that fails at runtime.
+// Used primarily as a test of Manticore's file-related syscall implementation.
+
+#include <errno.h>
+#include <stdio.h>
+#include <string.h>
+#include <stropts.h>
+#include <sys/socket.h>
+
+int main() {
+    // try bogus ioctl on a non-open file descriptor
+    int rc = ioctl(42, I_FLUSH, FLUSHRW);
+    if (rc == -1) {
+        fprintf(stderr, "got expected error: %s\n", strerror(errno));
+        return 0;
+    } else {
+        fprintf(stdout, "unexpectedly succeeded!\n");
+        return 1;
+    }
+}

examples/linux/ioctl_socket.c

@@ -0,0 +1,26 @@
+// This example demonstrates a particular syscall that fails at runtime.
+// Used primarily as a test of Manticore's file-related syscall implementation.
+
+#include <errno.h>
+#include <stdio.h>
+#include <string.h>
+#include <stropts.h>
+#include <sys/socket.h>
+
+int main() {
+    // try bogus ioctl on a socket
+    int sockfd = socket(AF_INET, SOCK_STREAM, 0);
+    if (sockfd < 0) {
+        fprintf(stderr, "error opening socket: %s\n", strerror(errno));
+        return 1;
+    }
+
+    int rc = ioctl(sockfd, I_FLUSH, FLUSHRW);
+    if (rc == -1) {
+        fprintf(stderr, "got expected error calling ioctl: %s\n", strerror(errno));
+        return 0;
+    } else {
+        fprintf(stdout, "unexpectedly succeeded!\n");
+        return 2;
+    }
+}

manticore/__main__.py

@@ -25,7 +25,7 @@
     from manticore.native.cli import native_main
 
 
-def main():
+def main() -> None:
     """
     Dispatches execution into one of Manticore's engines: evm or native.
     """
@@ -50,7 +50,7 @@ def main():
         native_main(args, logger)
 
 
-def parse_arguments():
+def parse_arguments() -> argparse.Namespace:
     def positive(value):
         ivalue = int(value)
         if ivalue <= 0:

manticore/core/manticore.py

@@ -243,9 +243,9 @@ def __init__(self, initial_state, workspace_url=None, outputspace_url=None, **kw
         *State list: KILLED*
 
         KILLED contains all the READY and BUSY states found at a cancel event.
-        Manticore supports interactive analysis and has a prominetnt event system
-        A useror ui can stop or cancel the exploration at any time. The unfinnished
-        states cought at this situation are simply moved to its own list for
+        Manticore supports interactive analysis and has a prominent event system.
+        A user can stop or cancel the exploration at any time. The unfinished
+        states caught in this situation are simply moved to their own list for
         further user action. This is a final list.
 
 
@@ -395,7 +395,7 @@ def setstate(x, y):
     @staticmethod
     @deprecated("Use utils.log.set_verbosity instead.")
     def verbosity(level):
-        """ Sets global vervosity level.
+        """ Sets global verbosity level.
             This will activate different logging profiles globally depending
             on the provided numeric value
         """

manticore/core/smtlib/constraints.py

@@ -106,7 +106,19 @@ def _get_sid(self) -> int:
         return self._sid
 
     def __get_related(self, related_to=None):
-        if related_to is not None:
+        # sam.moelius: There is a flaw in how __get_related works: when called on certain
+        # unsatisfiable sets, it can return a satisfiable one. The flaw arises when:
+        #   * self consists of a single constraint C
+        #   * C is the value of the related_to parameter
+        #   * C contains no variables
+        #   * C is unsatisfiable
+        # Since C contains no variables, it is not considered "related to" itself and is thrown out
+        # by __get_related. Since C was the sole element of self, __get_related returns the empty
+        # set. Thus, __get_related was called on an unsatisfiable set, {C}, but it returned a
+        # satisfiable one, {}.
+        #   In light of the above, the core __get_related logic is currently disabled.
+        # if related_to is not None:
+        if False:
             number_of_constraints = len(self.constraints)
             remaining_constraints = set(self.constraints)
             related_variables = get_variables(related_to)

manticore/core/smtlib/solver.py

@@ -164,6 +164,11 @@ def __init__(self):
             "(set-logic QF_AUFBV)",
             # The declarations and definitions will be scoped
             "(set-option :global-decls false)",
+            # sam.moelius: Option "tactic.solve_eqs.context_solve" was turned on by this commit in z3:
+            #   https://github.com/Z3Prover/z3/commit/3e53b6f2dbbd09380cd11706cabbc7e14b0cc6a2
+            # Turning it off greatly improves Manticore's performance on test_integer_overflow_storageinvariant
+            # in test_consensys_benchmark.py.
+            "(set-option :tactic.solve_eqs.context_solve false)",
         ]
 
         self._get_value_fmt = (RE_GET_EXPR_VALUE_FMT, 16)

manticore/core/worker.py

@@ -132,7 +132,7 @@ def run(self, *args):
                         assert current_state is None
                     # Handling Forking and terminating exceptions
                     except Concretize as exc:
-                        logger.info("[%r] Debug %r", self.id, exc)
+                        logger.info("[%r] Performing %r", self.id, exc.message)
                         # The fork() method can decides which state to keep
                         # exploring. For example when the fork results in a
                         # single state it is better to just keep going.