DeforaNetworks/deepstate
3
0
Fork 0
Code Releases Activity

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.

Browse Source
This commit is contained in:
Peter Goodman
2017-12-10 14:39:05 -05:00
parent fcd000dc14
commit 8248bbdcbc
8 changed files with 221 additions and 50 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
bin/deepstate/common.py
View File

@@ -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)

3
examples/CMakeLists.txt
View File

@@ -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)

44
examples/Euler.cpp Normal file
View File

@@ -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 <deepstate/DeepState.hpp>
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();
}

6
src/include/deepstate/Compiler.h
View File

@@ -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_ */

9
src/include/deepstate/DeepState.h
View File

@@ -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);

186
src/include/deepstate/DeepState.hpp
View File

@@ -22,6 +22,7 @@
#include <functional>
#include <string>
#include <type_traits>
#include <utility>
#include <vector>
@@ -149,6 +150,9 @@ class Symbolic {
T value;
};
template <typename T>
class Symbolic<T &> {};
template <typename T>
class SymbolicLinearContainer {
public:
@@ -192,39 +196,6 @@ class Symbolic<std::vector<T>> :
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 <typename... FuncTys>
inline static void OneOf(FuncTys&&... funcs) {
std::function<void(void)> func_arr[sizeof...(FuncTys)] = {funcs...};
func_arr[DeepState_SizeInRange(0, sizeof...(funcs))]();
unsigned index = DeepState_UIntInRange(
0U, static_cast<unsigned>(sizeof...(funcs)));
func_arr[Pump(index, sizeof...(funcs))]();
}
template <typename T, int k=sizeof(T) * 8>
struct ExpandedCompareIntegral {
template <typename C>
static DEEPSTATE_INLINE bool Compare(T a, T b, C cmp) {
if (cmp((a & 0xFF), (b & 0xFF))) {
return ExpandedCompareIntegral<T, k - 8>::Compare(a >> 8, b >> 8, cmp);
}
return DeepState_ZeroSink(k); // Also false.
}
};
template <typename T>
struct ExpandedCompareIntegral<T, 0> {
template <typename C>
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 <typename T>
struct DeclType {
using Type = T;
};
template <typename T>
struct DeclType<T &> : public DeclType<T> {};
template <typename T>
struct DeclType<Symbolic<T>> : public DeclType<T> {};
template <typename T>
struct DeclType<Symbolic<T> &> : public DeclType<T> {};
template <typename T>
struct IsIntegral : public std::is_integral<T> {};
template <typename T>
struct IsIntegral<T &> : public IsIntegral<T> {};
template <typename T>
struct IsIntegral<Symbolic<T>> : public IsIntegral<T> {};
template <typename T>
struct IsSigned : public std::is_signed<T> {};
template <typename T>
struct IsSigned<T &> : public IsSigned<T> {};
template <typename T>
struct IsSigned<Symbolic<T>> : public IsSigned<T> {};
template <typename T>
struct IsUnsigned : public std::is_unsigned<T> {};
template <typename T>
struct IsUnsigned<T &> : public IsUnsigned<T> {};
template <typename T>
struct IsUnsigned<Symbolic<T>> : public std::is_unsigned<T> {};
template <typename A, typename B>
struct BestType {
using UA = typename std::conditional<
IsUnsigned<B>::value,
typename std::make_unsigned<A>::type, A>::type;
using UB = typename std::conditional<
IsUnsigned<A>::value,
typename std::make_unsigned<B>::type, B>::type;
using Type = typename std::conditional<(sizeof(UA) > sizeof(UB)),
UA, UB>::type;
};
template <typename A, typename B>
struct Comparer {
static constexpr bool kIsIntegral = IsIntegral<A>() && IsIntegral<B>();
struct tag_int {};
struct tag_not_int {};
using tag = typename std::conditional<kIsIntegral,tag_int,tag_not_int>::type;
template <typename C>
static DEEPSTATE_INLINE bool Do(const A &a, const B &b, C cmp, tag_not_int) {
return cmp(a, b);
}
template <typename C>
static DEEPSTATE_INLINE bool Do(A a, B b, C cmp, tag_int) {
using T = typename ::deepstate::BestType<A, B>::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<T>::Compare(a, b, cmp);
}
template <typename C>
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<decltype(__a0)>::Type; \
using __B = typename ::deepstate::DeclType<decltype(__b0)>::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, ==)

8
src/lib/DeepState.c
View File

@@ -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);
}
}

8
src/lib/Stream.c
View File

@@ -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;
}