Add constraints to symbolic threads.

lib/Core/Memory.cpp

@@ -17,6 +17,7 @@
 #include "klee/Expr.h"
 #include "klee/Solver.h"
 #include "klee/util/BitArray.h"
+#include "klee/KleeDebug.h"
 
 #include "ObjectHolder.h"
 
@@ -229,6 +230,7 @@ bool MemoryLog::logRead(ExecutionState *state, TimingSolver *solver, ref<Expr> o
                                     AndExpr::create(threadIdMismatch, wgidMismatch) // BUG: probably should be OR
                                    );
 
+  KLEE_DEBUG( dbgs() << "Log Read Query: **START**\n" << query << "\n**END**\n");
   bool result;
   bool success = solver->mayBeTrue(*state, query, result);
   assert(success && "FIXME: Unhandled solver failure");

runtime/CLHost/kernel.c

@@ -385,7 +385,7 @@ cl_int clEnqueueNDRangeKernel(cl_command_queue command_queue,
     memcpy(kernel->program->numGroups, num_groups, work_dim*sizeof(size_t));
   }
 
-  char threadString[] = "threadX"; // Hacky way of setting a symbolic value's name.
+  char threadString[] = "symbolic_threadX"; // Hacky way of setting a symbolic value's name.
   size_t threadNum=0;
   do {
     /* Build up a one-dimensional work-group id for the work item.
@@ -410,6 +410,27 @@ cl_int clEnqueueNDRangeKernel(cl_command_queue command_queue,
     klee_make_symbolic(ids, sizeof(size_t)*work_dim, threadString);
     klee_assert( klee_is_symbolic(*ids) );
 
+    /* Constrain symbolic thread IDs */
+    unsigned int dim=0;
+    for (; dim < work_dim; ++dim )
+    {
+        // work item ids should be in a sensible range
+        klee_assume( ids[dim] < global_work_size[dim] );
+        klee_assume( ids[dim] >= 0); // Is this needed?
+
+        // Make sure previously created symbolic threads are distinct from the one
+        // we are going to create.
+        // Is the multi-dimensional restriction correct???
+        signed int prevThread = threadNum;
+        prevThread--;
+        while (prevThread >= 0)
+        {
+            klee_assume( symbolicIDs[prevThread][dim] < ids[dim] );
+            prevThread--;
+        }
+
+    }
+
     invoke_work_item(kernel,
                      argList,
                      work_dim,