From 8248bbdcbcd7dc7a1fc61ddaafef87564f0399c1 Mon Sep 17 00:00:00 2001 From: Peter Goodman Date: Sun, 10 Dec 2017 14:39:05 -0500 Subject: [PATCH] Removed usage of old name, added in a Euler power of like primes example. When the pairwise ASSERT_NEs are absent, you get interesting results that show examples of integer overflows. --- bin/deepstate/common.py | 7 ++ examples/CMakeLists.txt | 3 + examples/Euler.cpp | 44 +++++++ src/include/deepstate/Compiler.h | 6 + src/include/deepstate/DeepState.h | 9 ++ src/include/deepstate/DeepState.hpp | 186 +++++++++++++++++++++------- src/lib/DeepState.c | 8 +- src/lib/Stream.c | 8 +- 8 files changed, 221 insertions(+), 50 deletions(-) create mode 100644 examples/Euler.cpp diff --git a/bin/deepstate/common.py b/bin/deepstate/common.py index 59c2a94..e62f7ba 100644 --- a/bin/deepstate/common.py +++ b/bin/deepstate/common.py @@ -407,6 +407,13 @@ class DeepState(object): def api_assume(self, arg, expr_ea, file_ea, line): """Implements the `DeepState_Assume` API function, which injects a constraint into the solver.""" + if not self.is_symbolic(arg): + concrete_arg = self.concretize(arg) + if concrete_arg == 0: + self.abandon_test() + else: + return + constraint = arg != 0 if not self.add_constraint(constraint): expr, _ = self.read_c_string(expr_ea, concretize=False) diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index f79acb8..a78eedc 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -19,6 +19,9 @@ target_link_libraries(Fixture deepstate) add_executable(Primes Primes.cpp) target_link_libraries(Primes deepstate) +add_executable(Euler Euler.cpp) +target_link_libraries(Euler deepstate) + add_executable(IntegerOverflow IntegerOverflow.cpp) target_link_libraries(IntegerOverflow deepstate) diff --git a/examples/Euler.cpp b/examples/Euler.cpp new file mode 100644 index 0000000..8a341f7 --- /dev/null +++ b/examples/Euler.cpp @@ -0,0 +1,44 @@ +/* + * 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 deepstate; + +static unsigned pow5(unsigned v) { + return v * v * v * v * v; +} + +TEST(Euler, SumsOfLikePowers) { + symbolic_unsigned a, b, c, d, e; + ASSERT_GT(a, 1); + ASSERT_GT(b, 1); + ASSERT_GT(c, 1); + ASSERT_GT(d, 1); + ASSERT_GT(e, 1); + ASSERT_NE(a, b); ASSERT_NE(a, c); ASSERT_NE(a, d); ASSERT_NE(a, e); + ASSERT_NE(b, c); ASSERT_NE(b, d); ASSERT_NE(b, e); + ASSERT_NE(c, d); ASSERT_NE(c, e); + ASSERT_NE(d, e); + ASSERT_NE(pow5(a) + pow5(b) + pow5(c) + pow5(d), pow5(e)) + << a << "^5 + " << b << "^5" << " + " << c + << "^5 + " << d << "^5 = " << e << "^5"; +} + +int main(void) { + return DeepState_Run(); +} diff --git a/src/include/deepstate/Compiler.h b/src/include/deepstate/Compiler.h index 038f0c1..efa2073 100644 --- a/src/include/deepstate/Compiler.h +++ b/src/include/deepstate/Compiler.h @@ -93,4 +93,10 @@ static void f(void) #endif +#define DEEPSTATE_BARRIER() \ + asm volatile ("":::"memory") + +#define DEEPSTATE_USED(x) \ + asm volatile (""::"m"(x):"memory") + #endif /* SRC_INCLUDE_DEEPSTATE_COMPILER_H_ */ diff --git a/src/include/deepstate/DeepState.h b/src/include/deepstate/DeepState.h index 57f191e..66ebfa3 100644 --- a/src/include/deepstate/DeepState.h +++ b/src/include/deepstate/DeepState.h @@ -104,6 +104,15 @@ DEEPSTATE_INLINE static int8_t DeepState_MaxChar(int8_t v) { * value with a concrete value. */ extern int DeepState_IsTrue(int expr); +/* Always returns `1`. */ +extern int DeepState_One(void); + +/* Always returns `0`. */ +extern int DeepState_Zero(void); + +/* Always returns `0`. */ +extern int DeepState_ZeroSink(int); + /* Symbolize the data in the exclusive range `[begin, end)`. */ extern void DeepState_SymbolizeData(void *begin, void *end); diff --git a/src/include/deepstate/DeepState.hpp b/src/include/deepstate/DeepState.hpp index 1a6852f..3df4b41 100644 --- a/src/include/deepstate/DeepState.hpp +++ b/src/include/deepstate/DeepState.hpp @@ -22,6 +22,7 @@ #include #include +#include #include #include @@ -149,6 +150,9 @@ class Symbolic { T value; }; +template +class Symbolic {}; + template class SymbolicLinearContainer { public: @@ -192,39 +196,6 @@ class Symbolic> : DEEPSTATE_INLINE operator tname (void) const { \ return value; \ } \ - DEEPSTATE_INLINE tname operator+(const tname that) const { \ - return value + that; \ - } \ - DEEPSTATE_INLINE tname operator-(const tname that) const { \ - return value - that; \ - } \ - DEEPSTATE_INLINE tname operator*(const tname that) const { \ - return value * that; \ - } \ - DEEPSTATE_INLINE tname operator/(const tname that) const { \ - return value / that; \ - } \ - DEEPSTATE_INLINE tname operator|(const tname that) const { \ - return value | that; \ - } \ - DEEPSTATE_INLINE tname operator&(const tname that) const { \ - return value & that; \ - } \ - DEEPSTATE_INLINE tname operator^(const tname that) const { \ - return value ^ that; \ - } \ - DEEPSTATE_INLINE tname operator~(void) const { \ - return ~value; \ - } \ - DEEPSTATE_INLINE tname operator-(void) const { \ - return -value; \ - } \ - DEEPSTATE_INLINE tname operator>>(const tname that) const { \ - return value >> that; \ - } \ - DEEPSTATE_INLINE tname operator<<(const tname that) const { \ - return value << that; \ - } \ tname value; \ }; @@ -277,13 +248,16 @@ static T Pump(T val, unsigned max=10) { if (!IsSymbolic(val)) { return val; } - for (auto i = 0U; i < max; ++i) { + if (!max) { + DeepState_Abandon("Must have a positie maximum number of values to pump."); + } + for (auto i = 0U; i < max - 1; ++i) { T min_val = Minimize(val); if (val == min_val) { - asm volatile ("" : : "m"(min_val) : "memory"); - return min_val; // Force the concrete `min_val` to be returned, - // as opposed to compiler possibly choosing to - // return `val`. + DEEPSTATE_USED(min_val); // Force the concrete `min_val` to be returned, + // as opposed to compiler possibly choosing to + // return `val`. + return min_val; } } return Minimize(val); @@ -302,9 +276,119 @@ inline static void ForAll(Closure func) { template inline static void OneOf(FuncTys&&... funcs) { std::function func_arr[sizeof...(FuncTys)] = {funcs...}; - func_arr[DeepState_SizeInRange(0, sizeof...(funcs))](); + unsigned index = DeepState_UIntInRange( + 0U, static_cast(sizeof...(funcs))); + func_arr[Pump(index, sizeof...(funcs))](); } + +template +struct ExpandedCompareIntegral { + template + static DEEPSTATE_INLINE bool Compare(T a, T b, C cmp) { + if (cmp((a & 0xFF), (b & 0xFF))) { + return ExpandedCompareIntegral::Compare(a >> 8, b >> 8, cmp); + } + return DeepState_ZeroSink(k); // Also false. + } +}; + +template +struct ExpandedCompareIntegral { + template + static DEEPSTATE_INLINE bool Compare(T a, T b, C cmp) { + if (cmp((a & 0xFF), (b & 0xFF))) { + return DeepState_ZeroSink(0); + } else { + return DeepState_ZeroSink(100); + } + } +}; + +template +struct DeclType { + using Type = T; +}; + +template +struct DeclType : public DeclType {}; + +template +struct DeclType> : public DeclType {}; + +template +struct DeclType &> : public DeclType {}; + +template +struct IsIntegral : public std::is_integral {}; + +template +struct IsIntegral : public IsIntegral {}; + +template +struct IsIntegral> : public IsIntegral {}; + +template +struct IsSigned : public std::is_signed {}; + +template +struct IsSigned : public IsSigned {}; + +template +struct IsSigned> : public IsSigned {}; + +template +struct IsUnsigned : public std::is_unsigned {}; + +template +struct IsUnsigned : public IsUnsigned {}; + +template +struct IsUnsigned> : public std::is_unsigned {}; + +template +struct BestType { + using UA = typename std::conditional< + IsUnsigned::value, + typename std::make_unsigned::type, A>::type; + + using UB = typename std::conditional< + IsUnsigned::value, + typename std::make_unsigned::type, B>::type; + + using Type = typename std::conditional<(sizeof(UA) > sizeof(UB)), + UA, UB>::type; +}; + +template +struct Comparer { + static constexpr bool kIsIntegral = IsIntegral() && IsIntegral(); + struct tag_int {}; + struct tag_not_int {}; + using tag = typename std::conditional::type; + + template + static DEEPSTATE_INLINE bool Do(const A &a, const B &b, C cmp, tag_not_int) { + return cmp(a, b); + } + + template + static DEEPSTATE_INLINE bool Do(A a, B b, C cmp, tag_int) { + using T = typename ::deepstate::BestType::Type; + if (cmp(a, b)) { + return true; + } + DEEPSTATE_USED(a); // These make the compiler forget everything it knew + DEEPSTATE_USED(b); // about `a` and `b`. + return ::deepstate::ExpandedCompareIntegral::Compare(a, b, cmp); + } + + template + static DEEPSTATE_INLINE bool Do(const A &a, const B &b, C cmp) { + return Do(a, b, cmp, tag()); + } +}; + } // namespace deepstate #define ONE_OF ::deepstate::OneOf @@ -341,6 +425,14 @@ inline static void OneOf(FuncTys&&... funcs) { void fixture_name ## _ ## test_name :: DoRunTest(void) +#define _EXPAND_COMPARE(a, b, op) \ + ([] (decltype(a) __a0, decltype(b) __b0) -> bool { \ + using __A = typename ::deepstate::DeclType::Type; \ + using __B = typename ::deepstate::DeclType::Type; \ + auto __cmp = [] (__A __a4, __B __b4) { return __a4 op __b4; }; \ + return ::deepstate::Comparer<__A, __B>::Do(__a0, __b0, __cmp); \ + })((a), (b)) + #define TEST_F(fixture_name, test_name) \ _TEST_F(fixture_name, test_name, __FILE__, __LINE__) @@ -369,19 +461,23 @@ inline static void OneOf(FuncTys&&... funcs) { #define LOG_IF(LEVEL, cond) LOG_ ## LEVEL(cond) +#define DEEPSTATE_LOG_EQNE(a, b, op, level) \ + ::deepstate::Stream( \ + level, !(_EXPAND_COMPARE(a, b, op)), __FILE__, __LINE__) + #define DEEPSTATE_LOG_BINOP(a, b, op, level) \ ::deepstate::Stream( \ - level, !((a) op (b)), __FILE__, __LINE__) + level, !(a op b), __FILE__, __LINE__) -#define ASSERT_EQ(a, b) DEEPSTATE_LOG_BINOP(a, b, ==, DeepState_LogFatal) -#define ASSERT_NE(a, b) DEEPSTATE_LOG_BINOP(a, b, !=, DeepState_LogFatal) +#define ASSERT_EQ(a, b) DEEPSTATE_LOG_EQNE(a, b, ==, DeepState_LogFatal) +#define ASSERT_NE(a, b) DEEPSTATE_LOG_EQNE(a, b, !=, DeepState_LogFatal) #define ASSERT_LT(a, b) DEEPSTATE_LOG_BINOP(a, b, <, DeepState_LogFatal) #define ASSERT_LE(a, b) DEEPSTATE_LOG_BINOP(a, b, <=, DeepState_LogFatal) #define ASSERT_GT(a, b) DEEPSTATE_LOG_BINOP(a, b, >, DeepState_LogFatal) #define ASSERT_GE(a, b) DEEPSTATE_LOG_BINOP(a, b, >=, DeepState_LogFatal) -#define CHECK_EQ(a, b) DEEPSTATE_LOG_BINOP(a, b, ==, DeepState_LogError) -#define CHECK_NE(a, b) DEEPSTATE_LOG_BINOP(a, b, !=, DeepState_LogError) +#define CHECK_EQ(a, b) DEEPSTATE_LOG_EQNE(a, b, ==, DeepState_LogError) +#define CHECK_NE(a, b) DEEPSTATE_LOG_EQNE(a, b, !=, DeepState_LogError) #define CHECK_LT(a, b) DEEPSTATE_LOG_BINOP(a, b, <, DeepState_LogError) #define CHECK_LE(a, b) DEEPSTATE_LOG_BINOP(a, b, <=, DeepState_LogError) #define CHECK_GT(a, b) DEEPSTATE_LOG_BINOP(a, b, >, DeepState_LogError) @@ -406,7 +502,7 @@ inline static void OneOf(FuncTys&&... funcs) { DeepState_LogInfo, true, __FILE__, __LINE__) #define DEEPSTATE_ASSUME_BINOP(a, b, op) \ - DeepState_Assume(((a) op (b))), ::deepstate::Stream( \ + DeepState_Assume((a op b)), ::deepstate::Stream( \ DeepState_LogInfo, true, __FILE__, __LINE__) #define ASSUME_EQ(a, b) DEEPSTATE_ASSUME_BINOP(a, b, ==) diff --git a/src/lib/DeepState.c b/src/lib/DeepState.c index fa47446..3d9762b 100644 --- a/src/lib/DeepState.c +++ b/src/lib/DeepState.c @@ -139,6 +139,12 @@ DEEPSTATE_NOINLINE int DeepState_Zero(void) { return 0; } +/* Always returns `0`. */ +int DeepState_ZeroSink(int sink) { + (void) sink; + 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. */ @@ -222,7 +228,7 @@ int32_t DeepState_MaxInt(int32_t v) { void _DeepState_Assume(int expr, const char *expr_str, const char *file, unsigned line) { if (!expr) { - DeepState_LogFormat(DeepState_LogFatal, "Assumption %s at %s:%u failed", + DeepState_LogFormat(DeepState_LogFatal, "Assumption %s at %s(%u) failed", expr_str, file, line); } } diff --git a/src/lib/Stream.c b/src/lib/Stream.c index 0726ba5..ee57704 100644 --- a/src/lib/Stream.c +++ b/src/lib/Stream.c @@ -277,11 +277,11 @@ void DeepState_StreamResetFormatting(enum DeepState_LogLevel level) { memset(&(stream->options), 0, sizeof(stream->options)); } -static int McTest_NumLsInt64BitFormat = 2; +static int DeepState_NumLsInt64BitFormat = 2; /* `PRId64` will be "ld" or "lld" */ -DEEPSTATE_INITIALIZER(McTest_NumLsFor64BitFormat) { - McTest_NumLsInt64BitFormat = (PRId64)[1] == 'd' ? 1 : 2; +DEEPSTATE_INITIALIZER(DeepState_NumLsFor64BitFormat) { + DeepState_NumLsInt64BitFormat = (PRId64)[1] == 'd' ? 1 : 2; } /* Approximately do string format parsing and convert it into calls into our @@ -419,7 +419,7 @@ get_length_char: if (!length) { length = 1; - } else if (num_ls >= McTest_NumLsInt64BitFormat) { + } else if (num_ls >= DeepState_NumLsInt64BitFormat) { length = 8; }