Adding logger support, and other things.

bin/mctest/main_angr.py

@@ -14,14 +14,19 @@
 # limitations under the License.
 
 from __future__ import absolute_import
+
 import angr
+import argparse
 import collections
 import logging
+import multiprocessing
 import sys
 
+
 L = logging.getLogger("mctest")
 L.setLevel(logging.INFO)
 
+
 def hook_function(project, ea, cls):
   """Hook the function `name` with the SimProcedure `cls`."""
   project.hook(ea, cls(project=project))
@@ -141,23 +146,134 @@ class Pass(angr.SimProcedure):
   """Implements McTest_Pass, which notifies us of a passing test."""
   def run(self):
     L.info("Passed test case")
-    self.exit(0)
+    self.exit(self.state.globals['failed'])
 
 
 class Fail(angr.SimProcedure):
   """Implements McTest_Fail, which notifies us of a passing test."""
   def run(self):
     L.error("Failed test case")
+    self.state.globals['failed'] = 1
     self.exit(1)
 
 
+class SoftFail(angr.SimProcedure):
+  """Implements McTest_SoftFail, which notifies us of a passing test."""
+  def run(self):
+    L.error("Soft failure in test case, continuing")
+    self.state.globals['failed'] = 1
+
+
+class Log(angr.SimProcedure):
+  """Implements McTest_Log, which lets Angr intercept and handle the printing
+  of log messages from the simulated tests."""
+
+  LEVEL_TO_LOGGER = {
+    0: L.debug,
+    1: L.info,
+    2: L.warning,
+    3: L.error,
+    4: L.critical
+  }
+
+  def run(self, level, begin_ea, end_ea):
+    print self.state.regs.rdi, level
+    print self.state.regs.rsi, begin_ea
+    print self.state.regs.rdx, end_ea
+    level = self.state.solver.eval(level, cast_to=int)
+    assert level in self.LEVEL_TO_LOGGER
+
+    begin_ea = self.state.solver.eval(begin_ea, cast_to=int)
+    end_ea = self.state.solver.eval(end_ea, cast_to=int)
+    assert begin_ea <= end_ea
+
+    print level, begin_ea, end_ea
+
+    # Read the message from memory.
+    message = ""
+    if begin_ea < end_ea:
+      size = end_ea - begin_ea
+
+      # If this is an error message, then concretize the message, adding the
+      # concretizations to the state so that errors we output will eventually
+      # match the concrete inputs that we generate.
+      if 3 <= level:
+        message_bytes = []
+        for i in xrange(size):
+          byte = self.state.memory.load(begin_ea + i, size=8)
+          byte_as_ord = self.state.solver.eval(byte, cast_to=int)
+          if self.state.se.symbolic(byte):
+            self.state.solver.add(byte == byte_as_ord)
+          message_bytes.append(chr(byte_as_ord))
+
+        message = "".join(message_bytes)
+      
+      # Warning/informational message, don't assert any new constraints.
+      else:
+        data = self.state.memory.load(begin_ea, size=size)
+        message = self.state.solver.eval(data, cast_to=str)
+
+    # Log the message (produced by the program) through to the Python-based
+    # logger.
+    self.LEVEL_TO_LOGGER[level](message)
+
+    if 3 == level:
+      L.error("Soft failure in test case, continuing")
+      self.state.globals['failed'] = 1  # Soft failure on an error log message.
+    elif 4 == level:
+      L.error("Failed test case")
+      self.state.globals['failed'] = 1
+      self.exit(1)  # Hard failure on a fatal/critical log message.
+
+
+def run_test(project, test, run_state):
+  """Symbolically executes a single test function."""
+  test_state = project.factory.call_state(
+      test.ea,
+      base_state=run_state)
+
+  errored = []
+  test_manager = angr.SimulationManager(
+      project=project,
+      active_states=[test_state],
+      errored=errored)
+
+  L.info("Running test case {} from {}:{}".format(
+      test.name, test.file_name, test.line_number))
+  print 'running...'
+  try:
+    test_manager.run()
+  except Exception as e:
+    import traceback
+    print e
+    print traceback.format_exc()
+    print test_manager
+  print 'done running'
+  print errored
+  for state in test_manager.deadended:
+    last_event = state.history.events[-1]
+    if 'terminate' == last_event.type:
+      code = last_event.objects['exit_code']._model_concrete.value
+  print '???'
+  print test_manager
+
 def main():
   """Run McTest."""
-  if 2 > len(sys.argv):
-    return 1
+
+  parser = argparse.ArgumentParser(
+      description="Symbolically execute unit tests with Angr")
+
+  parser.add_argument(
+      "--num_workers", default=1, type=int,
+      help="Number of workers to spawn for testing and test generation.")
+
+  parser.add_argument(
+      "binary", type=str, help="Path to the test binary to run.")
+
+  args = parser.parse_args()
 
   project = angr.Project(
-      sys.argv[1],
+      args.binary,
       use_sim_procedures=True,
       translation_cache=True,
       support_selfmodifying_code=False,
@@ -170,8 +286,8 @@ def main():
   concrete_manager = angr.SimulationManager(
         project=project,
         active_states=[entry_state])
-  run_ea = project.kb.labels.lookup('McTest_Run')
-  concrete_manager.explore(find=run_ea)
+  setup_ea = project.kb.labels.lookup('McTest_Setup')
+  concrete_manager.explore(find=setup_ea)
   run_state = concrete_manager.found[0]
     
   # Read the API table, which will tell us about the location of various
@@ -190,31 +306,32 @@ def main():
   hook_function(project, apis['Assume'], Assume)
   hook_function(project, apis['Pass'], Pass)
   hook_function(project, apis['Fail'], Fail)
+  hook_function(project, apis['SoftFail'], SoftFail)
+  hook_function(project, apis['Log'], Log)
 
   # Find the test cases that we want to run.
   tests = find_test_cases(run_state, apis['LastTestInfo'])
 
+  # This will track whether or not a particular state has failed. Some states
+  # will soft fail, but continue their execution, and so we want to make sure
+  # that if they continue to a pass function, that they nonetheless are treated
+  # as failing.
+  run_state.globals['failed'] = 0
+  run_state.globals['log_messages'] = []
+
+  pool = multiprocessing.Pool(processes=max(1, args.num_workers))
+  results = []
+
   # For each test, create a simulation manager whose initial state calls into
   # the test case function.
   test_managers = []
   for test in tests:
-    test_state = project.factory.call_state(
-        test.ea,
-        base_state=run_state)
+    res = pool.apply_async(run_test, (project, test, run_state))
+    results.append(res)
 
-    test_manager = angr.SimulationManager(
-        project=project,
-        active_states=[test_state])
+  pool.close()
+  pool.join()
 
-    L.info("Running test case {} from {}:{}".format(
-        test.name, test.file_name, test.line_number))
-    test_manager.run()
-
-    for state in test_manager.deadended:
-      last_event = state.history.events[-1]
-      if 'terminate' == last_event.type:
-        code = last_event.objects['exit_code']._model_concrete.value
-    
   return 0
 
 if "__main__" == __name__:

bin/setup.py.in

@@ -34,6 +34,6 @@ setuptools.setup(
     entry_points={
         'console_scripts': [
             'mctest = mctest.__main__:main',
-            'mctest-angr = mctest.angr:main'
+            'mctest-angr = mctest.main_angr:main'
         ]
     })

examples/ArithmeticProperties.cpp

@@ -14,20 +14,37 @@
  * limitations under the License.
  */
 
+#include <mctest/McUnit.hpp>
 #include <mctest/Quantified.hpp>
 
 using namespace mctest;
 
-MCTEST_NOINLINE int add(int x, int y) {
-  return x + y;
-}
+// MCTEST_NOINLINE int add(int x, int y) {
+//   return x + y;
+// }
 
-McTest_EntryPoint(AdditionIsCommutative) {
+// TEST(Arithmetic, AdditionIsCommutative) {
+//   ForAll<int, int>([] (int x, int y) {
+//     ASSERT_EQ(add(x, y), add(y, x))
+//         << "Addition of signed integers must commute.";
+//   });
+// }
+
+// TEST(Arithmetic, AdditionIsAssociative) {
+//   ForAll<int, int, int>([] (int x, int y, int z) {
+//     ASSERT_EQ(add(x, add(y, z)), add(add(x, y), z))
+//         << "Addition of signed integers must associate.";
+//   });
+// }
+
+TEST(Arithmetic, InvertibleMultiplication_CanFail) {
   ForAll<int, int>([] (int x, int y) {
-    McTest_Assert(add(x, y) == add(y, x));
+    ASSUME_NE(y, 0);
+    ASSERT_EQ(x, (x / y) * y)
+        << x << " != (" << x << " / " << y << ") * " << y;
   });
 }
 
-int main(int argc, char *argv[]) {
+int main(void) {
   return McTest_Run();
 }

examples/CMakeLists.txt

@@ -17,3 +17,7 @@ target_link_libraries(OutOfBoundsInt mctest)
 
 add_executable(ArithmeticProperties ArithmeticProperties.cpp)
 target_link_libraries(ArithmeticProperties mctest)
+
+add_executable(Lists Lists.cpp)
+target_link_libraries(Lists mctest)
+

examples/Lists.cpp

@@ -0,0 +1,37 @@
+/*
+ * Copyright (c) 2017 Trail of Bits, Inc.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#include <mctest/McUnit.hpp>
+#include <mctest/Quantified.hpp>
+
+#include <algorithm>
+#include <vector>
+
+using namespace mctest;
+
+TEST(Vector, DoubleReversal) {
+  ForAll<std::vector<int>>([] (const std::vector<int> &vec1) {
+    std::vector<int> vec2 = vec1;
+    std::reverse(vec2.begin(), vec2.end());
+    std::reverse(vec2.begin(), vec2.end());
+    ASSERT_EQ(vec1, vec2)
+        << "Double reverse of vectors must be equal.";
+  });
+}
+
+int main(void) {
+  McTest_Run();
+}

src/include/mctest/McTest.h

@@ -18,9 +18,12 @@
 #define INCLUDE_MCTEST_MCTEST_H_
 
 #include <assert.h>
+#include <setjmp.h>
 #include <stddef.h>
 #include <stdint.h>
+#include <stdio.h>
 #include <stdlib.h>
+#include <string.h>
 
 #include <mctest/Compiler.h>
 
@@ -43,6 +46,11 @@ extern int16_t McTest_Short(void);
 extern uint8_t McTest_UChar(void);
 extern int8_t McTest_Char(void);
 
+/* Returns `1` if `expr` is true, and `0` otherwise. This is kind of an indirect
+ * way to take a symbolic value, introduce a fork, and on each size, replace its
+* value with a concrete value. */
+extern int McTest_IsTrue(int expr);
+
 /* Symbolize the data in the range `[begin, end)`. */
 extern void McTest_SymbolizeData(void *begin, void *end);
 
@@ -91,16 +99,40 @@ extern void _McTest_Assume(int expr);
 MCTEST_NORETURN
 extern void McTest_Fail(void);
 
+/* Mark this test as failing, but don't hard exit. */
+extern void McTest_SoftFail(void);
+
 MCTEST_NORETURN
 extern void McTest_Pass(void);
 
-/* Asserts that `expr` must hold. */
+/* Asserts that `expr` must hold. If it does not, then the test fails and
+ * immediately stops. */
 MCTEST_INLINE static void McTest_Assert(int expr) {
   if (!expr) {
     McTest_Fail();
   }
 }
 
+/* Asserts that `expr` must hold. If it does not, then the test fails, but
+ * nonetheless continues on. */
+MCTEST_INLINE static void McTest_Check(int expr) {
+  if (!expr) {
+    McTest_SoftFail();
+  }
+}
+
+enum McTest_LogLevel {
+  McTest_LogDebug = 0,
+  McTest_LogInfo = 1,
+  McTest_LogWarning = 2,
+  McTest_LogError = 3,
+  McTest_LogFatal = 4,
+};
+
+/* Outputs information to a log, using a specific log level. */
+extern void McTest_Log(enum McTest_LogLevel level, const char *begin,
+                       const char *end);
+
 /* Return a symbolic value in a the range `[low_inc, high_inc]`. */
 #define MCTEST_MAKE_SYMBOLIC_RANGE(Tname, tname) \
     MCTEST_INLINE static tname McTest_ ## Tname ## InRange( \
@@ -211,9 +243,68 @@ extern struct McTest_TestInfo *McTest_LastTestInfo;
     } \
     void McTest_Test_ ## test_name(void)
 
+/* Set up McTest. */
+extern void McTest_Setup(void);
+
+/* Return the first test case to run. */
+extern struct McTest_TestInfo *McTest_FirstTest(void);
+
+/* Returns 1 if a failure was caught, otherwise 0. */
+extern int McTest_CatchFail(void);
+
+/* Jump buffer for returning to `McTest_Run`. */
+extern jmp_buf McTest_ReturnToRun;
 
 /* Start McTest and run the tests. Returns the number of failed tests. */
-extern int McTest_Run(void);
+static int McTest_Run(void) {
+  int num_failed_tests = 0;
+  struct McTest_TestInfo *test = NULL;
+  char buff[1024];
+  int num_buff_bytes_used = 0;
+
+  McTest_Setup();
+
+  for (test = McTest_FirstTest(); test != NULL; test = test->prev) {
+
+    /* Print the test that we're going to run. */
+    num_buff_bytes_used = sprintf(buff, "Running: %s from %s:%u",
+                                  test->test_name, test->file_name,
+                                  test->line_number);
+    McTest_Log(McTest_LogInfo, buff, &(buff[num_buff_bytes_used]));
+
+    /* Run the test. */
+    if (!setjmp(McTest_ReturnToRun)) {
+      
+      /* Convert uncaught C++ exceptions into a test failure. */
+#if defined(__cplusplus) && defined(__cpp_exceptions)
+      try {
+#endif  /* __cplusplus */
+
+      test->test_func();  /* Run the test function. */
+      McTest_Pass();
+
+#if defined(__cplusplus) && defined(__cpp_exceptions)
+      } catch(...) {
+        McTest_Fail();
+      }
+#endif  /* __cplusplus */
+
+    /* We caught a failure when running the test. */
+    } else if (McTest_CatchFail()) {
+      ++num_failed_tests;
+
+      num_buff_bytes_used = sprintf(buff, "Failed: %s", test->test_name);
+      McTest_Log(McTest_LogInfo, buff, &(buff[num_buff_bytes_used]));
+
+    /* The test passed. */
+    } else {
+      num_buff_bytes_used = sprintf(buff, "Passed: %s", test->test_name);
+      McTest_Log(McTest_LogInfo, buff, &(buff[num_buff_bytes_used]));
+    }
+  }
+
+  return num_failed_tests;
+}
 
 MCTEST_END_EXTERN_C
 

src/include/mctest/McTest.hpp

@@ -137,8 +137,8 @@ class SymbolicLinearContainer {
  public:
   MCTEST_INLINE explicit SymbolicLinearContainer(size_t len)
       : value(len) {
-    if (len) {
-      McTest_SymbolizeData(&(value.begin()), &(value.end()));
+    if (!value.empty()) {
+      McTest_SymbolizeData(&(value.front()), &(value.back()));
     }
   }
 

src/include/mctest/McUnit.hpp

@@ -0,0 +1,115 @@
+/*
+ * Copyright (c) 2017 Trail of Bits, Inc.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#ifndef INCLUDE_MCTEST_MCUNIT_HPP_
+#define INCLUDE_MCTEST_MCUNIT_HPP_
+
+#include <mctest/McTest.hpp>
+
+#include <sstream>
+
+#define TEST(category, name) \
+    McTest_EntryPoint(category ## _ ## name)
+
+namespace mctest {
+
+/* Base logger */
+class Logger {
+ public:
+  MCTEST_INLINE Logger(McTest_LogLevel level_, bool expr_,
+                       const char *file_, unsigned line_)
+      : level(level_),
+        expr(!!McTest_IsTrue(expr_)),
+        file(file_),
+        line(line_) {}
+
+  MCTEST_INLINE ~Logger(void) {
+    if (!expr) {
+      std::stringstream report_ss;
+      report_ss << file << "(" << line << "): " << ss.str();
+      auto report_str = report_ss.str();
+      auto report_c_str = report_str.c_str();
+      McTest_Log(level, report_c_str, report_c_str + report_str.size());
+    }
+  }
+
+  MCTEST_INLINE std::stringstream &stream(void) {
+    return ss;
+  }
+
+ private:
+  Logger(void) = delete;
+  Logger(const Logger &) = delete;
+  Logger &operator=(const Logger &) = delete;
+
+  const McTest_LogLevel level;
+  const bool expr;
+  const char * const file;
+  const unsigned line;
+  std::stringstream ss;
+};
+
+}  // namespace mctest
+
+#define MCTEST_LOG_BINOP(a, b, op, level) \
+    ::mctest::Logger( \
+        level, ((a) op (b)), __FILE__, __LINE__).stream()
+
+#define ASSERT_EQ(a, b) MCTEST_LOG_BINOP(a, b, ==, McTest_LogFatal)
+#define ASSERT_NE(a, b) MCTEST_LOG_BINOP(a, b, !=, McTest_LogFatal)
+#define ASSERT_LT(a, b) MCTEST_LOG_BINOP(a, b, <, McTest_LogFatal)
+#define ASSERT_LE(a, b) MCTEST_LOG_BINOP(a, b, <=, McTest_LogFatal)
+#define ASSERT_GT(a, b) MCTEST_LOG_BINOP(a, b, >, McTest_LogFatal)
+#define ASSERT_GE(a, b) MCTEST_LOG_BINOP(a, b, >=, McTest_LogFatal)
+
+#define CHECK_EQ(a, b) MCTEST_LOG_BINOP(a, b, ==, McTest_LogError)
+#define CHECK_NE(a, b) MCTEST_LOG_BINOP(a, b, !=, McTest_LogError)
+#define CHECK_LT(a, b) MCTEST_LOG_BINOP(a, b, <, McTest_LogError)
+#define CHECK_LE(a, b) MCTEST_LOG_BINOP(a, b, <=, McTest_LogError)
+#define CHECK_GT(a, b) MCTEST_LOG_BINOP(a, b, >, McTest_LogError)
+#define CHECK_GE(a, b) MCTEST_LOG_BINOP(a, b, >=, McTest_LogError)
+
+#define ASSERT(expr) \
+    ::mctest::Logger( \
+        McTest_LogFatal, !!(expr), __FILE__, __LINE__).stream()
+
+#define ASSERT_TRUE ASSERT
+#define ASSERT_FALSE(expr) ASSERT(!(expr))
+
+#define CHECK(expr) \
+    ::mctest::Logger( \
+        McTest_LogError, !!(expr), __FILE__, __LINE__).stream()
+
+#define CHECK_TRUE CHECK
+#define CHECK_FALSE(expr) CHECK(!(expr))
+
+#define ASSUME(expr) \
+    McTest_Assume(expr), ::mctest::Logger( \
+        McTest_LogInfo, false, __FILE__, __LINE__).stream()
+
+
+#define MCTEST_ASSUME_BINOP(a, b, op) \
+    McTest_Assume(((a) op (b))), ::mctest::Logger( \
+        McTest_LogInfo, false, __FILE__, __LINE__).stream()
+
+#define ASSUME_EQ(a, b) MCTEST_ASSUME_BINOP(a, b, ==)
+#define ASSUME_NE(a, b) MCTEST_ASSUME_BINOP(a, b, !=)
+#define ASSUME_LT(a, b) MCTEST_ASSUME_BINOP(a, b, <)
+#define ASSUME_LE(a, b) MCTEST_ASSUME_BINOP(a, b, <=)
+#define ASSUME_GT(a, b) MCTEST_ASSUME_BINOP(a, b, >)
+#define ASSUME_GE(a, b) MCTEST_ASSUME_BINOP(a, b, >=)
+
+#endif  // INCLUDE_MCTEST_MCUNIT_HPP_

src/lib/McTest.c

@@ -18,6 +18,7 @@
 
 #include <assert.h>
 #include <setjmp.h>
+#include <stdio.h>
 
 #if defined(unix) || defined(__unix) || defined(__unix__)
 # define _GNU_SOURCE
@@ -41,23 +42,26 @@ static volatile uint8_t McTest_Input[McTest_InputLength];
  * been consumed. */
 static uint32_t McTest_InputIndex = 0;
 
-/* Jump buffer for returning to `McTest_Main`. */
-static jmp_buf McTest_ReturnToMain;
+/* Jump buffer for returning to `McTest_Run`. */
+jmp_buf McTest_ReturnToRun = {};
 
-static int McTest_TestPassed = 0;
+static int McTest_TestFailed = 0;
 
 /* Mark this test as failing. */
 MCTEST_NORETURN
-extern void McTest_Fail(void) {
-  McTest_TestPassed = 0;
-  longjmp(McTest_ReturnToMain, 1);
+void McTest_Fail(void) {
+  McTest_TestFailed = 1;
+  longjmp(McTest_ReturnToRun, 1);
 }
 
 /* Mark this test as passing. */
 MCTEST_NORETURN
-extern void McTest_Pass(void) {
-  McTest_TestPassed = 1;
-  longjmp(McTest_ReturnToMain, 0);
+void McTest_Pass(void) {
+  longjmp(McTest_ReturnToRun, 0);
+}
+
+void McTest_SoftFail(void) {
+  McTest_TestFailed = 1;
 }
 
 void McTest_SymbolizeData(void *begin, void *end) {
@@ -76,6 +80,25 @@ void McTest_SymbolizeData(void *begin, void *end) {
   }
 }
 
+MCTEST_NOINLINE int McTest_One(void) {
+  return 1;
+}
+
+MCTEST_NOINLINE int McTest_Zero(void) {
+  return 0;
+}
+
+/* Returns `1` if `expr` is true, and `0` otherwise. This is kind of an indirect
+ * way to take a symbolic value, introduce a fork, and on each size, replace its
+* value with a concrete value. */
+int McTest_IsTrue(int expr) {
+  if (expr == McTest_Zero()) {
+    return McTest_Zero();
+  } else {
+    return McTest_One();
+  }
+}
+
 /* Return a symbolic value of a given type. */
 int McTest_Bool(void) {
   return McTest_Input[McTest_InputIndex++] & 1;
@@ -91,6 +114,9 @@ int McTest_Bool(void) {
       return val; \
     }
 
+
+MAKE_SYMBOL_FUNC(Size, size_t)
+
 MAKE_SYMBOL_FUNC(UInt64, uint64_t)
 int64_t McTest_Int64(void) {
   return (int64_t) McTest_UInt64();
@@ -122,6 +148,39 @@ int McTest_IsSymbolicUInt(uint32_t x) {
   return 0;
 }
 
+/* Returns a printable string version of the log level. */
+static const char *McTest_LogLevelStr(enum McTest_LogLevel level) {
+  switch (level) {
+    case McTest_LogDebug:
+      return "DEBUG";
+    case McTest_LogInfo:
+      return "INFO";
+    case McTest_LogWarning:
+      return "WARNING";
+    case McTest_LogError:
+      return "ERROR";
+    case McTest_LogFatal:
+      return "FATAL";
+    default:
+      return "UNKNOWN";
+  }
+}
+
+/* Outputs information to a log, using a specific log level. */
+void McTest_Log(enum McTest_LogLevel level, const char *begin,
+                const char *end) {
+  int str_len = (int) (end - begin);
+  fprintf(stderr, "%s: %.*s\n", McTest_LogLevelStr(level),
+          str_len, begin);
+  
+  if (McTest_LogError == level) {
+    McTest_SoftFail();
+
+  } else if (McTest_LogFatal == level) {
+    McTest_Fail();
+  }
+}
+
 /* A McTest-specific symbol that is needed for hooking. */
 struct McTest_IndexEntry {
   const char * const name;
@@ -133,6 +192,8 @@ struct McTest_IndexEntry {
 const struct McTest_IndexEntry McTest_API[] = {
   {"Pass",            (void *) McTest_Pass},
   {"Fail",            (void *) McTest_Fail},
+  {"SoftFail",        (void *) McTest_SoftFail},
+  {"Log",             (void *) McTest_Log},
   {"Assume",          (void *) _McTest_Assume},
   {"IsSymbolicUInt",  (void *) McTest_IsSymbolicUInt},
   {"InputBegin",      (void *) &(McTest_Input[0])},
@@ -142,8 +203,8 @@ const struct McTest_IndexEntry McTest_API[] = {
   {NULL, NULL},
 };
 
-int McTest_Run(void) {
-
+/* Set up McTest. */
+void McTest_Setup(void) {
   /* Manticore entrypoint. Manticore doesn't (yet?) support symbol lookups, so
    * we instead interpose on this fake system call, and discover the API table
    * via the first argument to the system call. */
@@ -153,25 +214,17 @@ int McTest_Run(void) {
   syscall(0x41414141, &McTest_API);
 #endif
 
-  int num_failed_tests = 0;
-  for (struct McTest_TestInfo *info = McTest_LastTestInfo;
-       info != NULL;
-       info = info->prev) {
+  /* TODO(pag): Sort the test cases by file name and line number. */
+}
 
-    McTest_TestPassed = 0;
-    if (!setjmp(McTest_ReturnToMain)) {
-      printf("Running %s from %s:%u\n", info->test_name, info->file_name,
-             info->line_number);
-      info->test_func();
+/* Return the first test case to run. */
+struct McTest_TestInfo *McTest_FirstTest(void) {
+  return McTest_LastTestInfo;
+}
 
-    } else if (McTest_TestPassed) {
-      printf("  %s Passed\n", info->test_name);
-    } else {
-      printf("  %s Failed\n", info->test_name);
-      num_failed_tests += 1;
-    }
-  }
-  return num_failed_tests;
+/* Returns 1 if a failure was caught, otherwise 0. */
+int McTest_CatchFail(void) {
+  return McTest_TestFailed;
 }
 
 MCTEST_END_EXTERN_C