From 0d336bd4d6555f931e934596e6d035ebd60423c4 Mon Sep 17 00:00:00 2001 From: Peter Goodman Date: Sat, 28 Oct 2017 01:11:59 -0400 Subject: [PATCH] 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 | 4 +-- examples/ArithmeticProperties.cpp | 30 +++++++++++++++++++++ examples/CMakeLists.txt | 3 +++ src/include/mctest/McTest.h | 37 +++++++++++--------------- src/include/mctest/McTest.hpp | 44 +++++++++++++++++-------------- src/include/mctest/Quantified.hpp | 38 ++++++++++++++++++++++++++ src/lib/McTest.c | 2 +- 7 files changed, 114 insertions(+), 44 deletions(-) create mode 100644 examples/ArithmeticProperties.cpp create mode 100644 src/include/mctest/Quantified.hpp diff --git a/bin/mctest/__main__.py b/bin/mctest/__main__.py index ee9235b..60be841 100644 --- a/bin/mctest/__main__.py +++ b/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 diff --git a/examples/ArithmeticProperties.cpp b/examples/ArithmeticProperties.cpp new file mode 100644 index 0000000..d7157e1 --- /dev/null +++ b/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 + +using namespace mctest; + +__attribute__((noinline)) +int add(int x, int y) { + return x + y; +} + +McTest_EntryPoint(AdditionIsCommutative) { + ForAll([] (int x, int y) { + McTest_Assert(add(x, y) == add(y, x)); + }); +} diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index ab6262b..2209292 100644 --- a/examples/CMakeLists.txt +++ b/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) diff --git a/src/include/mctest/McTest.h b/src/include/mctest/McTest.h index ba1706e..b96d1dc 100644 --- a/src/include/mctest/McTest.h +++ b/src/include/mctest/McTest.h @@ -17,10 +17,16 @@ #ifndef INCLUDE_MCTEST_MCTEST_H_ #define INCLUDE_MCTEST_MCTEST_H_ +#include #include #include #include +#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) diff --git a/src/include/mctest/McTest.hpp b/src/include/mctest/McTest.hpp index 676ae56..37d7492 100644 --- a/src/include/mctest/McTest.hpp +++ b/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 @@ -136,31 +136,35 @@ class Symbolic { T value; }; -template +template 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 : public SymbolicLinearContainer {}; +class Symbolic : public SymbolicLinearContainer { + using SymbolicLinearContainer::SymbolicLinearContainer; +}; template <> -class Symbolic : public SymbolicLinearContainer {}; +class Symbolic : public SymbolicLinearContainer { + using SymbolicLinearContainer::SymbolicLinearContainer; +}; template class Symbolic> : @@ -170,8 +174,8 @@ class Symbolic> : template <> \ class Symbolic { \ public: \ - inline Symbolic(void) - : value(McTest_ ## Tname) {} \ + inline Symbolic(void) \ + : value(McTest_ ## Tname()) {} \ inline operator tname (void) const { \ return value; \ } \ diff --git a/src/include/mctest/Quantified.hpp b/src/include/mctest/Quantified.hpp new file mode 100644 index 0000000..543fbf6 --- /dev/null +++ b/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 + +#include + +namespace mctest { + +template +inline static void ForAll(void (*func)(Args...)) { + func(Symbolic()...); +} + +template +inline static void ForAll(Closure func) { + func(Symbolic()...); +} + +} // namespace mctest + +#endif // INCLUDE_MCTEST_QUANTIFIED_HPP_ diff --git a/src/lib/McTest.c b/src/lib/McTest.c index 9150aaf..3fe9024 100644 --- a/src/lib/McTest.c +++ b/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;