Fixed build errors for c++ test basics. Added a ForAll thingy to abstract around making symbols. Shortened section name lengths. Added a simple arithmetic properties test case.

bin/mctest/__main__.py

@@ -57,7 +57,7 @@ def find_test_cases(project, state):
   tests = []
   addr_size_bytes = state.arch.bits // 8
   for sec in obj.sections:
-    if sec.name != ".mctest_entrypoints":
+    if sec.name != ".mctest_funcs":
       continue
 
     for ea in xrange(sec.vaddr, sec.vaddr + sec.memsize, 32):
@@ -85,7 +85,7 @@ def make_symbolic_input(project, state):
   """Fill in the input data array with symbolic data."""
   obj = project.loader.main_object
   for sec in obj.sections:
-    if sec.name == ".mctest_input_data":
+    if sec.name == ".mctest_data":
       data = state.se.Unconstrained('MCTEST_INPUT', sec.memsize * 8)
       state.memory.store(sec.vaddr, data)
       return data

examples/ArithmeticProperties.cpp

@@ -0,0 +1,30 @@
+/*
+ * 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/Quantified.hpp>
+
+using namespace mctest;
+
+__attribute__((noinline))
+int add(int x, int y) {
+  return x + y;
+}
+
+McTest_EntryPoint(AdditionIsCommutative) {
+  ForAll<int, int>([] (int x, int y) {
+    McTest_Assert(add(x, y) == add(y, x));
+  });
+}

examples/CMakeLists.txt

@@ -14,3 +14,6 @@
 
 add_executable(OutOfBoundsInt OutOfBoundsInt.c)
 target_link_libraries(OutOfBoundsInt mctest)
+
+add_executable(ArithmeticProperties ArithmeticProperties.cpp)
+target_link_libraries(ArithmeticProperties mctest)

src/include/mctest/McTest.h

@@ -17,10 +17,16 @@
 #ifndef INCLUDE_MCTEST_MCTEST_H_
 #define INCLUDE_MCTEST_MCTEST_H_
 
+#include <assert.h>
 #include <stddef.h>
 #include <stdint.h>
 #include <stdlib.h>
 
+#ifdef assert
+# undef assert
+#endif
+#define assert McTest_Assert
+
 #ifdef __cplusplus
 extern "C" {
 #endif  /* __cplusplus */
@@ -103,6 +109,8 @@ inline static void McTest_Assert(int expr) {
       return x; \
     }
 
+
+MCTEST_MAKE_SYMBOLIC_RANGE(Size, size_t)
 MCTEST_MAKE_SYMBOLIC_RANGE(Int64, int64_t)
 MCTEST_MAKE_SYMBOLIC_RANGE(UInt64, uint64_t)
 MCTEST_MAKE_SYMBOLIC_RANGE(Int, int)
@@ -150,23 +158,6 @@ inline static int McTest_IsSymbolicBool(int x) {
   return McTest_IsSymbolicInt(x);
 }
 
-#pragma clang diagnostic push
-#pragma clang diagnostic ignored "-Wpointer-to-int-cast"
-
-#pragma GCC diagnostic push
-#pragma GCC diagnostic ignored "-Wpointer-to-int-cast"
-
-inline static int McTest_IsSymbolicPtr(void *x) {
-  if (sizeof(void *) == 8) {
-    return McTest_IsSymbolicUInt64((uint64_t) x);
-  } else {
-    return McTest_IsSymbolicUInt((uint32_t) x);
-  }
-}
-
-#pragma GCC diagnostic pop
-#pragma clang diagnostic pop
-
 inline static int McTest_IsSymbolicFloat(float x) {
   return McTest_IsSymbolicUInt(*((uint32_t *) &x));
 }
@@ -179,9 +170,11 @@ inline static int McTest_IsSymbolicDouble(double x) {
 #define __MCTEST_TO_STR(a) #a
 
 #ifdef __cplusplus
-# define MCTEST_EXTERN_C extern "C"
+# define MCTEST_BEGIN_EXTERN_C extern "C" {
+# define MCTEST_END_EXTERN_C }
 #else
-# define MCTEST_EXTERN_C
+# define MCTEST_BEGIN_EXTERN_C
+# define MCTEST_END_EXTERN_C
 #endif
 
 #define McTest_EntryPoint(test_name) \
@@ -201,13 +194,15 @@ struct __attribute__((packed)) McTest_TestInfo {
       McTest_Test_ ## test_name(); \
       McTest_Pass(); \
     } \
-    MCTEST_EXTERN_C struct McTest_TestInfo McTest_Register_ ## test_name \
-    __attribute__((section(".mctest_entrypoints"))) = { \
+    MCTEST_BEGIN_EXTERN_C \
+    struct McTest_TestInfo McTest_Register_ ## test_name \
+    __attribute__((section(".mctest_funcs"))) = { \
       McTest_Run_ ## test_name, \
       _MCTEST_TO_STR(test_name), \
       file, \
       line \
     }; \
+    MCTEST_END_EXTERN_C \
     void McTest_Test_ ## test_name(void)
 
 

src/include/mctest/McTest.hpp

@@ -73,7 +73,7 @@ inline static char Char(void) {
   return McTest_Char();
 }
 
-inline static int IsSymbolic(uint64_t x) {
+inline static bool IsSymbolic(uint64_t x) {
   return McTest_IsSymbolicUInt64(x);
 }
 
@@ -81,11 +81,11 @@ inline static int IsSymbolic(int64_t x) {
   return McTest_IsSymbolicInt64(x);
 }
 
-inline static int IsSymbolic(uint32_t x) {
+inline static bool IsSymbolic(uint32_t x) {
   return McTest_IsSymbolicUInt(x);
 }
 
-inline static int IsSymbolic(int32_t x) {
+inline static bool IsSymbolic(int32_t x) {
   return McTest_IsSymbolicInt(x);
 }
 
@@ -93,28 +93,28 @@ inline static int IsSymbolic(uint16_t x) {
   return McTest_IsSymbolicUShort(x);
 }
 
-inline static int IsSymbolic(int16_t x) {
+inline static bool IsSymbolic(int16_t x) {
   return McTest_IsSymbolicShort(x);
 }
 
-inline static int IsSymbolic(unsigned char x) {
+inline static bool IsSymbolic(unsigned char x) {
   return McTest_IsSymbolicUChar(x);
 }
 
-inline static int IsSymbolic(char x) {
+inline static bool IsSymbolic(char x) {
   return McTest_IsSymbolicChar(x);
 }
 
-inline static int IsSymbolic(float x) {
+inline static bool IsSymbolic(float x) {
   return McTest_IsSymbolicFloat(x);
 }
 
-inline static int IsSymbolic(double x) {
+inline static bool IsSymbolic(double x) {
   return McTest_IsSymbolicDouble(x);
 }
 
-inline static int IsSymbolic(void *x) {
-  return McTest_IsSymbolicPtr(x);
+inline static bool IsSymbolic(void *x) {
+  return IsSymbolic((uintptr_t) x);
 }
 
 template <typename T>
@@ -136,31 +136,35 @@ class Symbolic {
   T value;
 };
 
-template <T>
+template <typename T>
 class SymbolicLinearContainer {
  public:
-  inline explicit Symbolic(size_t len)
+  inline explicit SymbolicLinearContainer(size_t len)
       : value(len) {
     if (len) {
-      McTest_SymbolizeData(&(str.begin()), &(str.end()));
+      McTest_SymbolizeData(&(value.begin()), &(value.end()));
     }
   }
 
+  inline SymbolicLinearContainer(void)
+      : SymbolicLinearContainer(McTest_SizeInRange(0, 32)) {}
+
   inline operator T (void) const {
     return value;
   }
 
   T value;
-
- private:
-  Symblic(void) = delete;
 };
 
 template <>
-class Symbolic<std::string> : public SymbolicLinearContainer<std::string> {};
+class Symbolic<std::string> : public SymbolicLinearContainer<std::string> {
+  using SymbolicLinearContainer::SymbolicLinearContainer;
+};
 
 template <>
-class Symbolic<std::wstring> : public SymbolicLinearContainer<std::wstring> {};
+class Symbolic<std::wstring> : public SymbolicLinearContainer<std::wstring> {
+  using SymbolicLinearContainer::SymbolicLinearContainer;
+};
 
 template <typename T>
 class Symbolic<std::vector<T>> : 
@@ -170,8 +174,8 @@ class Symbolic<std::vector<T>> :
     template <> \
     class Symbolic<tname> { \
      public: \
-      inline Symbolic(void)
-          : value(McTest_ ## Tname) {} \
+      inline Symbolic(void) \
+          : value(McTest_ ## Tname()) {} \
       inline operator tname (void) const { \
         return value; \
       } \

src/include/mctest/Quantified.hpp

@@ -0,0 +1,38 @@
+/*
+ * 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_QUANTIFIED_HPP_
+#define INCLUDE_MCTEST_QUANTIFIED_HPP_
+
+#include <mctest/McTest.hpp>
+
+#include <functional>
+
+namespace mctest {
+
+template <typename... Args>
+inline static void ForAll(void (*func)(Args...)) {
+  func(Symbolic<Args>()...);
+}
+
+template <typename... Args, typename Closure>
+inline static void ForAll(Closure func) {
+  func(Symbolic<Args>()...);
+}
+
+}  // namespace mctest
+
+#endif  // INCLUDE_MCTEST_QUANTIFIED_HPP_

src/lib/McTest.c

@@ -23,7 +23,7 @@ extern "C" {
 #endif  /* __cplusplus */
 
 volatile uint8_t McTest_Input[8192]
-    __attribute__((section(".mctest_input_data")));
+    __attribute__((section(".mctest_data")));
 
 uint32_t McTest_InputIndex = 0;