Added prime polynomial example, new Pumping function to address scalability challenges with primality testing, and some improvements to the streaming interface, where if you don't stream in values, then the python side doesn't end up printing out some 'empty' stream infos.

bin/deepstate/common.py

@@ -377,6 +377,16 @@ class DeepState(object):
     """Notify the symbolic executor that this test has been abandoned due to
     some critical error and stop executing the current state."""
     self.context['abandoned'] = True
+  
+  def api_min_uint(self, arg):
+    """Implements the `DeepState_MinUInt` API function, which returns the
+    minimum satisfiable value for `arg`."""
+    return self.concretize_min(arg, constrain=False)
+
+  def api_min_int(self, arg):
+    """Implements the `DeepState_MinInt` API function, which returns the
+    minimum satisfiable value for `arg`."""
+    return self.concretize_min(arg + 2**31, constrain=False)
 
   def api_is_symbolic_uint(self, arg):
     """Implements the `DeepState_IsSymbolicUInt` API, which returns whether or
@@ -391,13 +401,17 @@ class DeepState(object):
     else:
       return 1
 
-  def api_assume(self, arg):
+  def api_assume(self, arg, expr_ea, file_ea, line):
     """Implements the `DeepState_Assume` API function, which injects a
     constraint into the solver."""
     constraint = arg != 0
     if not self.add_constraint(constraint):
-      self.log_message(LOG_LEVEL_FATAL,
-                       "Failed to add assumption {}".format(constraint))
+      expr, _ = self.read_c_string(expr_ea, concretize=False)
+      file, _ = self.read_c_string(file_ea, concretize=False)
+      line = self.concretize(line, constrain=True)
+      self.log_message(
+        LOG_LEVEL_FATAL, "Failed to add assumption {} in {}:{}".format(
+            expr, file, line))
       self.abandon_test()
 
   def api_concretize_data(self, begin_ea, end_ea):
@@ -529,6 +543,14 @@ class DeepState(object):
     stream.append((str, format_str, None, print_str))
     self.context[stream_id] = stream
 
+  def api_clear_stream(self, level):
+    """Implements DeepState_ClearStream, which clears the contents of a stream
+    for level `level`."""
+    level = self.concretize(level, constrain=True)
+    assert level in LOG_LEVEL_TO_LOGGER
+    stream_id = 'stream_{}'.format(level)
+    self.context[stream_id] = []
+
   def api_log_stream(self, level):
     """Implements DeepState_LogStream, which converts the contents of a stream
     for level `level` into a log for level `level`."""

bin/deepstate/main_angr.py

@@ -147,8 +147,8 @@ class IsSymbolicUInt(angr.SimProcedure):
 
 class Assume(angr.SimProcedure):
   """Implements _DeepState_Assume, which tries to inject a constraint."""
-  def run(self, arg):
-    DeepAngr(procedure=self).api_assume(arg)
+  def run(self, arg, expr_ea, file_ea, line):
+    DeepAngr(procedure=self).api_assume(arg, expr_ea, file_ea, line)
 
 
 class Pass(angr.SimProcedure):
@@ -190,6 +190,20 @@ class ConcretizeCStr(angr.SimProcedure):
     return DeepAngr(procedure=self).api_concretize_cstr(begin_ea)
 
 
+class MinUInt(angr.SimProcedure):
+  """Implements the `Deeptate_MinUInt` API function, which lets the
+    programmer ask for the minimum satisfiable value of an unsigned integer."""
+  def run(self, val):
+    return DeepAngr(procedure=self).api_min_uint(val)
+
+
+class MinInt(angr.SimProcedure):
+  """Implements the `Deeptate_MinUInt` API function, which lets the
+    programmer ask for the minimum satisfiable value of a signed integer."""
+  def run(self, val):
+    return DeepAngr(procedure=self).api_min_int(val)
+
+
 class StreamInt(angr.SimProcedure):
   """Implements _DeepState_StreamInt, which gives us an integer to stream, and
   the format to use for streaming."""
@@ -212,6 +226,13 @@ class StreamString(angr.SimProcedure):
     DeepAngr(procedure=self).api_stream_string(level, format_ea, str_ea)
 
 
+class ClearStream(angr.SimProcedure):
+  """Implements DeepState_ClearStream, which clears the contents of a stream for
+  level `level`."""
+  def run(self, level):
+    DeepAngr(procedure=self).api_clear_stream(level)
+
+
 class LogStream(angr.SimProcedure):
   """Implements DeepState_LogStream, which converts the contents of a stream for
   level `level` into a log for level `level`."""
@@ -318,6 +339,8 @@ def main():
   hook_function(project, apis['IsSymbolicUInt'], IsSymbolicUInt)
   hook_function(project, apis['ConcretizeData'], ConcretizeData)
   hook_function(project, apis['ConcretizeCStr'], ConcretizeCStr)
+  hook_function(project, apis['MinUInt'], MinUInt)
+  hook_function(project, apis['MinInt'], MinInt)
   hook_function(project, apis['Assume'], Assume)
   hook_function(project, apis['Pass'], Pass)
   hook_function(project, apis['Fail'], Fail)
@@ -327,6 +350,7 @@ def main():
   hook_function(project, apis['StreamInt'], StreamInt)
   hook_function(project, apis['StreamFloat'], StreamFloat)
   hook_function(project, apis['StreamString'], StreamString)
+  hook_function(project, apis['ClearStream'], ClearStream)
   hook_function(project, apis['LogStream'], LogStream)
 
   # Find the test cases that we want to run.

bin/deepstate/main_manticore.py

@@ -137,9 +137,9 @@ def hook_IsSymbolicUInt(state, arg):
   return DeepManticore(state).api_is_symbolic_uint(arg)
 
 
-def hook_Assume(state, arg):
+def hook_Assume(state, arg, expr_ea, file_ea, line):
   """Implements _DeepState_Assume, which tries to inject a constraint."""
-  DeepManticore(state).api_assume(arg)
+  DeepManticore(state).api_assume(arg, expr_ea, file_ea, line)
 
 
 def hook_StreamInt(state, level, format_ea, unpack_ea, uint64_ea):
@@ -160,6 +160,12 @@ def hook_StreamString(state, level, format_ea, str_ea):
   DeepManticore(state).api_stream_string(level, format_ea, str_ea)
 
 
+def hook_ClearStream(state, level):
+  """Implements DeepState_ClearStream, which clears the contents of a stream
+  for level `level`."""
+  DeepManticore(state).api_clear_stream(level)
+
+
 def hook_LogStream(state, level):
   """Implements DeepState_LogStream, which converts the contents of a stream for
   level `level` into a log for level `level`."""
@@ -200,6 +206,18 @@ def hook_ConcretizeCStr(state, begin_ea):
   return DeepManticore(state).api_concretize_cstr(begin_ea)
 
 
+def hook_MinUInt(self, val):
+  """Implements the `Deeptate_MinUInt` API function, which lets the
+  programmer ask for the minimum satisfiable value of an unsigned integer."""
+  return DeepAngr(procedure=self).api_min_uint(val)
+
+
+def hook_MinInt(self, val):
+  """Implements the `Deeptate_MinUInt` API function, which lets the
+  programmer ask for the minimum satisfiable value of a signed integer."""
+  return DeepAngr(procedure=self).api_min_int(val)
+
+
 def hook_Log(state, level, ea):
   """Implements DeepState_Log, which lets Manticore intercept and handle the
   printing of log messages from the simulated tests."""
@@ -234,6 +252,8 @@ def do_run_test(state, apis, test):
   m.add_hook(apis['IsSymbolicUInt'], hook(hook_IsSymbolicUInt))
   m.add_hook(apis['ConcretizeData'], hook(hook_ConcretizeData))
   m.add_hook(apis['ConcretizeCStr'], hook(hook_ConcretizeCStr))
+  m.add_hook(apis['MinUInt'], hook(hook_MinUInt))
+  m.add_hook(apis['MinInt'], hook(hook_MinInt))
   m.add_hook(apis['Assume'], hook(hook_Assume))
   m.add_hook(apis['Pass'], hook(hook_Pass))
   m.add_hook(apis['Fail'], hook(hook_Fail))
@@ -243,6 +263,7 @@ def do_run_test(state, apis, test):
   m.add_hook(apis['StreamInt'], hook(hook_StreamInt))
   m.add_hook(apis['StreamFloat'], hook(hook_StreamFloat))
   m.add_hook(apis['StreamString'], hook(hook_StreamString))
+  m.add_hook(apis['ClearStream'], hook(hook_ClearStream))
   m.add_hook(apis['LogStream'], hook(hook_LogStream))
 
   m.subscribe('will_terminate_state', done_test)

examples/CMakeLists.txt

@@ -16,6 +16,9 @@
 add_executable(Fixture Fixture.cpp)
 target_link_libraries(Fixture deepstate)
 
+add_executable(Primes Primes.cpp)
+target_link_libraries(Primes deepstate)
+
 add_executable(IntegerOverflow IntegerOverflow.cpp)
 target_link_libraries(IntegerOverflow deepstate)
 

examples/Primes.cpp

@@ -0,0 +1,46 @@
+/*
+ * 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;
+
+bool IsPrime(const unsigned p) {
+  for (unsigned i = 2; i <= (p/2); ++i) {
+    if (!(p % i)) {
+      return i;
+    }
+  }
+  return true;
+}
+
+TEST(PrimePolynomial, OnlyGeneratesPrimes) {
+  symbolic_unsigned x, y, z;
+  ASSUME_GT(x, 0);
+  unsigned poly = (x * x) + x + 41;
+  ASSUME_GT(y, 1);
+  ASSUME_GT(z, 1);
+  ASSUME_LT(y, poly);
+  ASSUME_LT(z, poly);
+  ASSERT_NE(poly, y * z)
+      << x << "^2 + " << x << " + 41 is not prime";
+  ASSERT(IsPrime(Pump(poly)))
+      << x << "^2 + " << x << " + 41 is not prime";
+}
+
+int main(int argc, char *argv[]) {
+  return DeepState_Run();
+}

src/include/deepstate/DeepState.h

@@ -59,6 +59,27 @@ extern int16_t DeepState_Short(void);
 extern uint8_t DeepState_UChar(void);
 extern int8_t DeepState_Char(void);
 
+/* Returns the minimum satisfiable value for a given symbolic value, given
+ * the constraints present on that value. */
+extern uint32_t DeepState_MinUInt(uint32_t);
+extern int32_t DeepState_MinInt(int32_t);
+
+DEEPSTATE_INLINE static uint16_t DeepState_MinUShort(uint16_t v) {
+  return DeepState_MinUInt(v);
+}
+
+DEEPSTATE_INLINE static uint8_t DeepState_MinUChar(uint8_t v) {
+  return DeepState_MinUInt(v);
+}
+
+DEEPSTATE_INLINE static int16_t DeepState_MinShort(int16_t v) {
+  return DeepState_MinInt(v);
+}
+
+DEEPSTATE_INLINE static int8_t DeepState_MinChar(int8_t v) {
+  return DeepState_MinInt(v);
+}
+
 /* 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. */
@@ -105,9 +126,10 @@ DEEPSTATE_MAKE_SYMBOLIC_ARRAY(UChar, unsigned char)
 
 /* Creates an assumption about a symbolic value. Returns `1` if the assumption
  * can hold and was asserted. */
-extern void _DeepState_Assume(int expr);
+extern void _DeepState_Assume(int expr, const char *expr_str, const char *file,
+                              unsigned line);
 
-#define DeepState_Assume(x) _DeepState_Assume(!!(x))
+#define DeepState_Assume(x) _DeepState_Assume(!!(x), #x, __FILE__, __LINE__)
 
 /* Abandon this test. We've hit some kind of internal problem. */
 DEEPSTATE_NORETURN

src/include/deepstate/DeepState.hpp

@@ -192,6 +192,39 @@ 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; \
     };
 
@@ -204,8 +237,55 @@ MAKE_SYMBOL_SPECIALIZATION(Short, int16_t)
 MAKE_SYMBOL_SPECIALIZATION(UChar, uint8_t)
 MAKE_SYMBOL_SPECIALIZATION(Char, int8_t)
 
+
+using symbolic_char = Symbolic<char>;
+using symbolic_short = Symbolic<short>;
+using symbolic_int = Symbolic<int>;
+using symbolic_unsigned = Symbolic<unsigned>;
+using symbolic_long = Symbolic<long>;
+
+using symbolic_int8_t = Symbolic<int8_t>;
+using symbolic_uint8_t = Symbolic<uint8_t>;
+using symbolic_int16_t = Symbolic<int16_t>;
+using symbolic_uint16_t = Symbolic<uint16_t>;
+using symbolic_int32_t = Symbolic<int32_t>;
+using symbolic_uint32_t = Symbolic<uint32_t>;
+using symbolic_int64_t = Symbolic<int64_t>;
+using symbolic_uint64_t = Symbolic<uint64_t>;
+
 #undef MAKE_SYMBOL_SPECIALIZATION
 
+#define MAKE_MINIMIZER(Type, type) \
+    DEEPSTATE_INLINE static type Minimize(type val) { \
+      return DeepState_Min ## Type(val); \
+    }
+
+MAKE_MINIMIZER(UInt, uint32_t)
+MAKE_MINIMIZER(Int, int32_t)
+MAKE_MINIMIZER(UShort, uint16_t)
+MAKE_MINIMIZER(Short, int16_t)
+MAKE_MINIMIZER(UChar, uint8_t)
+MAKE_MINIMIZER(Char, int8_t)
+
+#undef MAKE_MINIMIZER
+
+template <typename T>
+static T Pump(T val, unsigned max=10) {
+  if (!IsSymbolic(val)) {
+    return val;
+  }
+  for (auto i = 0U; i < max; ++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`.
+    }
+  }
+  return Minimize(val);
+}
+
 template <typename... Args>
 inline static void ForAll(void (*func)(Args...)) {
   func(Symbolic<Args>()...);

src/include/deepstate/Stream.h

@@ -25,6 +25,9 @@
 
 DEEPSTATE_BEGIN_EXTERN_C
 
+/* Clear the contents of the stream and don't log it. */
+extern void DeepState_ClearStream(enum DeepState_LogLevel level);
+
 /* Flush the contents of the stream to a log. */
 extern void DeepState_LogStream(enum DeepState_LogLevel level);
 

src/include/deepstate/Stream.hpp

@@ -28,9 +28,10 @@ namespace deepstate {
 class Stream {
  public:
   DEEPSTATE_INLINE Stream(DeepState_LogLevel level_, bool do_log_,
-                       const char *file, unsigned line)
+                          const char *file, unsigned line)
       : level(level_),
-        do_log(DeepState_IsTrue(do_log_)) {
+        do_log(!!DeepState_IsTrue(do_log_)),
+        has_something_to_log(false) {
     DeepState_LogStream(level);
     if (do_log) {
       DeepState_StreamFormat(level, "%s(%u): ", file, line);
@@ -39,7 +40,11 @@ class Stream {
 
   DEEPSTATE_INLINE ~Stream(void) {
     if (do_log) {
-      DeepState_LogStream(level);
+      if (has_something_to_log) {
+        DeepState_LogStream(level);
+      } else {
+        DeepState_ClearStream(level);
+      }
     }
   }
 
@@ -47,6 +52,7 @@ class Stream {
   DEEPSTATE_INLINE const Stream &operator<<(type val) const { \
     if (do_log) { \
       DeepState_Stream ## Type(level, expr); \
+      has_something_to_log = true; \
     } \
     return *this; \
   }
@@ -82,6 +88,7 @@ class Stream {
   DEEPSTATE_INLINE const Stream &operator<<(const std::string &str) const {
     if (do_log && !str.empty()) {
       DeepState_StreamCStr(level, str.c_str());
+      has_something_to_log = true;
     }
     return *this;
   }
@@ -94,7 +101,8 @@ class Stream {
   Stream &operator=(const Stream &) = delete;
 
   const DeepState_LogLevel level;
-  const int do_log;
+  const bool do_log;
+  mutable bool has_something_to_log;
 };
 
 }  // namespace deepstate

src/lib/DeepState.c

@@ -15,6 +15,7 @@
  */
 
 #include "deepstate/DeepState.h"
+#include "deepstate/Log.h"
 
 #include <assert.h>
 #include <limits.h>
@@ -195,9 +196,22 @@ int8_t DeepState_Char(void) {
 
 #undef MAKE_SYMBOL_FUNC
 
-void _DeepState_Assume(int expr) {
+
+/* Returns the minimum satisfiable value for a given symbolic value, given
+ * the constraints present on that value. */
+uint32_t DeepState_MinUInt(uint32_t v) {
+  return v;
+}
+
+int32_t DeepState_MinInt(int32_t v) {
+  return v;
+}
+
+void _DeepState_Assume(int expr, const char *expr_str, const char *file,
+                       unsigned line) {
   if (!expr) {
-    DeepState_Abandon("");
+    DeepState_LogFormat(DeepState_LogFatal, "Assumption %s at %s:%u failed",
+                        expr_str, file, line);
   }
 }
 
@@ -248,11 +262,14 @@ const struct DeepState_IndexEntry DeepState_API[] = {
   {"IsSymbolicUInt",  (void *) DeepState_IsSymbolicUInt},
   {"ConcretizeData",  (void *) DeepState_ConcretizeData},
   {"ConcretizeCStr",  (void *) DeepState_ConcretizeCStr},
+  {"MinUInt",         (void *) DeepState_MinUInt},
+  {"MinInt",          (void *) DeepState_MinInt},
 
   /* Logging API. */
   {"Log",             (void *) DeepState_Log},
 
   /* Streaming API for deferred logging. */
+  {"ClearStream",     (void *) DeepState_ClearStream},
   {"LogStream",       (void *) DeepState_LogStream},
   {"StreamInt",       (void *) _DeepState_StreamInt},
   {"StreamFloat",     (void *) _DeepState_StreamFloat},

src/lib/Stream.c

@@ -251,6 +251,15 @@ void DeepState_StreamDouble(enum DeepState_LogLevel level, double val) {
   _DeepState_StreamFloat(level, format, stream->unpack, &(stream->value.as_fp64));
 }
 
+/* Clear the contents of the stream and don't log it. */
+void DeepState_ClearStream(enum DeepState_LogLevel level) {
+  struct DeepState_Stream *stream = &(DeepState_Streams[level]);
+  if (stream->size) {
+    memset(stream->message, 0, DeepState_StreamSize);
+    stream->size = 0;
+  }
+}
+
 /* Flush the contents of the stream to a log. */
 void DeepState_LogStream(enum DeepState_LogLevel level) {
   struct DeepState_Stream *stream = &(DeepState_Streams[level]);
@@ -258,8 +267,7 @@ void DeepState_LogStream(enum DeepState_LogLevel level) {
     stream->message[stream->size] = '\0';
     stream->message[DeepState_StreamSize] = '\0';
     DeepState_Log(level, stream->message);
-    memset(stream->message, 0, DeepState_StreamSize);
-    stream->size = 0;
+    DeepState_ClearStream(level);
   }
 }