Added a maximize objective API to DeepState.

bin/deepstate/common.py

@@ -93,6 +93,9 @@ class DeepState(object):
   def concretize_min(self, val, constrain=False):
     raise NotImplementedError("Must be implemented by engine.")
 
+  def concretize_max(self, val, constrain=False):
+    raise NotImplementedError("Must be implemented by engine.")
+
   def concretize_many(self, val, max_num):
     raise NotImplementedError("Must be implemented by engine.")
 
@@ -383,10 +386,10 @@ class DeepState(object):
     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
+  def api_max_uint(self, arg):
+    """Implements the `DeepState_MaxUInt` API function, which returns the
     minimum satisfiable value for `arg`."""
-    return self.concretize_min(arg + 2**31, constrain=False)
+    return self.concretize_max(arg, constrain=False)
 
   def api_is_symbolic_uint(self, arg):
     """Implements the `DeepState_IsSymbolicUInt` API, which returns whether or

bin/deepstate/main_angr.py

@@ -107,6 +107,14 @@ class DeepAngr(DeepState):
       self.add_constraint(val == concrete_val)
     return concrete_val
 
+  def concretize_max(self, val, constrain=False):
+    if isinstance(val, (int, long)):
+      return val
+    concrete_val = self.state.solver.max(val)
+    if constrain:
+      self.add_constraint(val == concrete_val)
+    return concrete_val
+
   def concretize_many(self, val, max_num):
     assert 0 < max_num
     if isinstance(val, (int, long)):
@@ -197,11 +205,11 @@ class MinUInt(angr.SimProcedure):
     return DeepAngr(procedure=self).api_min_uint(val)
 
 
-class MinInt(angr.SimProcedure):
-  """Implements the `Deeptate_MinUInt` API function, which lets the
+class MaxUInt(angr.SimProcedure):
+  """Implements the `Deeptate_MaxUInt` 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)
+    return DeepAngr(procedure=self).api_max_uint(val)
 
 
 class StreamInt(angr.SimProcedure):
@@ -340,7 +348,7 @@ def main():
   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['MaxUInt'], MaxUInt)
   hook_function(project, apis['Assume'], Assume)
   hook_function(project, apis['Pass'], Pass)
   hook_function(project, apis['Fail'], Fail)

bin/deepstate/main_manticore.py

@@ -106,6 +106,14 @@ class DeepManticore(DeepState):
       self.add_constraint(val == concrete_val)
     return concrete_val
 
+  def concretize_max(self, val, constrain=False):
+    if isinstance(val, (int, long)):
+      return val
+    concrete_val = max(self.state.concretize(val, policy='MINMAX'))
+    if constrain:
+      self.add_constraint(val == concrete_val)
+    return concrete_val
+
   def concretize_many(self, val, max_num):
     assert 0 < max_num
     if isinstance(val, (int, long)):
@@ -212,10 +220,10 @@ def hook_MinUInt(self, val):
   return DeepAngr(procedure=self).api_min_uint(val)
 
 
-def hook_MinInt(self, val):
-  """Implements the `Deeptate_MinUInt` API function, which lets the
+def hook_MaxUInt(self, val):
+  """Implements the `Deeptate_MaxUInt` API function, which lets the
   programmer ask for the minimum satisfiable value of a signed integer."""
-  return DeepAngr(procedure=self).api_min_int(val)
+  return DeepAngr(procedure=self).api_max_uint(val)
 
 
 def hook_Log(state, level, ea):
@@ -253,7 +261,7 @@ def do_run_test(state, apis, test):
   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['MaxUInt'], hook(hook_MaxUInt))
   m.add_hook(apis['Assume'], hook(hook_Assume))
   m.add_hook(apis['Pass'], hook(hook_Pass))
   m.add_hook(apis['Fail'], hook(hook_Fail))

src/include/deepstate/DeepState.h

@@ -64,20 +64,39 @@ extern int8_t DeepState_Char(void);
 extern uint32_t DeepState_MinUInt(uint32_t);
 extern int32_t DeepState_MinInt(int32_t);
 
+extern uint32_t DeepState_MaxUInt(uint32_t);
+extern int32_t DeepState_MaxInt(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);
+  return (uint8_t) DeepState_MinUInt(v);
 }
 
 DEEPSTATE_INLINE static int16_t DeepState_MinShort(int16_t v) {
-  return DeepState_MinInt(v);
+  return (int16_t) DeepState_MinInt(v);
 }
 
 DEEPSTATE_INLINE static int8_t DeepState_MinChar(int8_t v) {
-  return DeepState_MinInt(v);
+  return (int8_t) DeepState_MinInt(v);
+}
+
+DEEPSTATE_INLINE static uint16_t DeepState_MaxUShort(uint16_t v) {
+  return (uint16_t) DeepState_MaxUInt(v);
+}
+
+DEEPSTATE_INLINE static uint8_t DeepState_MaxUChar(uint8_t v) {
+  return (uint8_t) DeepState_MaxUInt(v);
+}
+
+DEEPSTATE_INLINE static int16_t DeepState_MaxShort(int16_t v) {
+  return (int16_t) DeepState_MaxInt(v);
+}
+
+DEEPSTATE_INLINE static int8_t DeepState_MaxChar(int8_t v) {
+  return (int8_t) DeepState_MaxInt(v);
 }
 
 /* Returns `1` if `expr` is true, and `0` otherwise. This is kind of an indirect

src/include/deepstate/DeepState.hpp

@@ -258,6 +258,9 @@ using symbolic_uint64_t = Symbolic<uint64_t>;
 #define MAKE_MINIMIZER(Type, type) \
     DEEPSTATE_INLINE static type Minimize(type val) { \
       return DeepState_Min ## Type(val); \
+    } \
+    DEEPSTATE_INLINE static type Maximize(type val) { \
+      return DeepState_Max ## Type(val); \
     }
 
 MAKE_MINIMIZER(UInt, uint32_t)

src/lib/DeepState.c

@@ -204,9 +204,21 @@ uint32_t DeepState_MinUInt(uint32_t v) {
 }
 
 int32_t DeepState_MinInt(int32_t v) {
+  return (int32_t) (DeepState_MinUInt(((uint32_t) v) + 0x80000000U) -
+                    0x80000000U);
+}
+
+/* Returns the maximum satisfiable value for a given symbolic value, given
+ * the constraints present on that value. */
+uint32_t DeepState_MaxUInt(uint32_t v) {
   return v;
 }
 
+int32_t DeepState_MaxInt(int32_t v) {
+  return (int32_t) (DeepState_MaxUInt(((uint32_t) v) + 0x80000000U) -
+                    0x80000000U);
+}
+
 void _DeepState_Assume(int expr, const char *expr_str, const char *file,
                        unsigned line) {
   if (!expr) {
@@ -263,7 +275,7 @@ const struct DeepState_IndexEntry DeepState_API[] = {
   {"ConcretizeData",  (void *) DeepState_ConcretizeData},
   {"ConcretizeCStr",  (void *) DeepState_ConcretizeCStr},
   {"MinUInt",         (void *) DeepState_MinUInt},
-  {"MinInt",          (void *) DeepState_MinInt},
+  {"MaxUInt",         (void *) DeepState_MaxUInt},
 
   /* Logging API. */
   {"Log",             (void *) DeepState_Log},