From 6ec7d71188b82f8b282dc8acc92249b79c43e54c Mon Sep 17 00:00:00 2001
From: Peter Goodman <peter.goodman@gmail.com>
Date: Thu, 2 Nov 2017 01:05:15 -0400
Subject: [PATCH] Added error checking.

---
 bin/deepstate/common.py |  8 +++++++-
 src/lib/DeepState.c     | 15 ++++++++++++---
 2 files changed, 19 insertions(+), 4 deletions(-)

diff --git a/bin/deepstate/common.py b/bin/deepstate/common.py
index 6f53cc0..603ae4d 100644
--- a/bin/deepstate/common.py
+++ b/bin/deepstate/common.py
@@ -332,8 +332,14 @@ class DeepState(object):
     apis = self.context['apis']
     input_length, _ = self.read_uint32_t(apis['InputIndex'])
     
-    # Concretize the used symbols.
     symbols = self.context['symbols']
+
+    # Check to see if the test case actually read too many symbols.
+    if input_length > len(symbols):
+      LOGGER.critical("Test overflowed DeepState_Input symbol array")
+      input_length = len(symbols)
+
+    # Concretize the used symbols.
     input_bytes = bytearray()
     for i in xrange(input_length):
       b = self.concretize(symbols[i], constrain=True)
diff --git a/src/lib/DeepState.c b/src/lib/DeepState.c
index c98f34d..317cda4 100644
--- a/src/lib/DeepState.c
+++ b/src/lib/DeepState.c
@@ -27,12 +27,12 @@ DEEPSTATE_BEGIN_EXTERN_C
 struct DeepState_TestInfo *DeepState_LastTestInfo = NULL;
 
 enum {
-  DeepState_InputLength = 8192
+  DeepState_InputSize = 8192
 };
 
 /* Byte buffer that will contain symbolic data that is used to supply requests
  * for symbolic values (e.g. `int`s). */
-static volatile uint8_t DeepState_Input[DeepState_InputLength];
+static volatile uint8_t DeepState_Input[DeepState_InputSize];
 
 /* Index into the `DeepState_Input` array that tracks how many input bytes have
  * been consumed. */
@@ -81,6 +81,9 @@ void DeepState_SymbolizeData(void *begin, void *end) {
   } else {
     uint8_t *bytes = (uint8_t *) begin;
     for (uintptr_t i = 0, max_i = (end_addr - begin_addr); i < max_i; ++i) {
+      if (DeepState_InputIndex >= DeepState_InputSize) {
+        DeepState_Abandon("Read too many symbols");
+      }
       bytes[i] = DeepState_Input[DeepState_InputIndex++];
     }
   }
@@ -138,11 +141,17 @@ int DeepState_IsTrue(int expr) {
 
 /* Return a symbolic value of a given type. */
 int DeepState_Bool(void) {
+  if (DeepState_InputIndex >= DeepState_InputSize) {
+    DeepState_Abandon("Read too many symbols");
+  }
   return DeepState_Input[DeepState_InputIndex++] & 1;
 }
 
 #define MAKE_SYMBOL_FUNC(Type, type) \
     type DeepState_ ## Type(void) { \
+      if ((DeepState_InputIndex + sizeof(type)) > DeepState_InputSize) { \
+        DeepState_Abandon("Read too many symbols"); \
+      } \
       type val = 0; \
       _Pragma("unroll") \
       for (size_t i = 0; i < sizeof(type); ++i) { \
@@ -219,7 +228,7 @@ const struct DeepState_IndexEntry DeepState_API[] = {
 
   /* Source of symbolic bytes. */
   {"InputBegin",      (void *) &(DeepState_Input[0])},
-  {"InputEnd",        (void *) &(DeepState_Input[DeepState_InputLength])},
+  {"InputEnd",        (void *) &(DeepState_Input[DeepState_InputSize])},
   {"InputIndex",      (void *) &DeepState_InputIndex},
 
   /* Solver APIs. */