Commit 3d2b9eab authored by Daniel Liew's avatar Daniel Liew
Browse files

A symbolic Thread ID is now stored in the Thread Class (to be used

for race checking later).
parent e2113452
......@@ -88,6 +88,8 @@ private:
wlist_id_t waitingList;
thread_uid_t tuid;
ref<Expr> symbolicThreadID;
public:
Thread(thread_id_t tid, process_id_t pid, KFunction *start_function,
unsigned moduleId);
......@@ -96,6 +98,7 @@ public:
process_id_t getPid() const { return tuid.second; }
unsigned getWorkgroupId() const { return workgroupId; }
void setWorkgroupId(unsigned wgid) { workgroupId = wgid; }
void setSymbolicThreadID(ref<Expr> symbolicID);
StackTrace getStackTrace() const;
void dumpStackTrace() const;
......
......@@ -219,6 +219,8 @@ extern "C" {
/* Set the work group id for this thread to the given id. */
void klee_set_work_group_id(unsigned wgid);
void klee_set_work_item_id(size_t* ids, size_t byteSzie, size_t nDim);
//////////////////////////////////////////////////////////////////////////////
// Thread Scheduling Management
//////////////////////////////////////////////////////////////////////////////
......
/*******************************************************************************
* ref<Expr> dim = arguments[2];
* Copyright (C) 2010 Dependable Systems Laboratory, EPFL
*
* This file is part of the Cloud9-specific extensions to the KLEE symbolic
......@@ -55,6 +56,7 @@
#include "llvm/Support/Path.h"
#endif
#include "llvm/Support/raw_os_ostream.h"
#include "llvm/Support/Debug.h"
#ifdef HAVE_OPENCL
#include "clang/Basic/Version.h"
......@@ -216,6 +218,7 @@ HandlerInfo handlerInfo[] = {
add("lrintf", handleFPToSIRound, true),
add("llrint", handleFPToSIRound, true),
add("llrintf", handleFPToSIRound, true),
add("klee_set_work_item_id", handleSetWorkItemID, false)
#undef addDNR
#undef add
......@@ -1642,3 +1645,72 @@ void SpecialFunctionHandler::handleFPToSIRound(ExecutionState &state,
/*fromIsIEEE=*/false,
/*roundNearest=*/true));
}
void SpecialFunctionHandler::handleSetWorkItemID(ExecutionState &state,
KInstruction *target,
std::vector<ref<Expr> > &arguments) {
// This is a hack so we can get access to the symbolic thread IDs
// and store them in the Thread class for later use for race checking.
assert( arguments.size() == 3 && "Incorrect number of args");
for(std::vector<ref<Expr> >::const_iterator i = arguments.begin(),
end = arguments.end();
i != end;
++i)
{
assert( (*i)->getKind() == Expr::Constant && "Non constant argument passed");
}
ref<ConstantExpr> threadIdPtr = cast<ConstantExpr>(arguments[0]);
Expr::Width dataSize = 8*( cast<ConstantExpr>(arguments[1])->getZExtValue() );
assert( (dataSize == Expr::Int64) && "Passed in data size is incorrect");
size_t num_dim = cast<ConstantExpr>(arguments[2])->getZExtValue();
assert( num_dim > 0 && "Cannot have negative number of dimensions");
assert(num_dim < 64 && "Cannot support that many dimensions");
// FIXME: Use dbgs() with ref<Expr>
std::cerr << "threadid pointer:" << threadIdPtr << "\n";
std::cerr << "Size:" << dataSize << "\n";
std::cerr << "Number of Dimensions: " << num_dim << "\n";
//executor.resolveExact(state, threadIdPtr, rl, "work-item-ids-pointer");
// Get the memory object for the symbolic IDs.
ObjectPair result;
bool success = state.addressSpace().resolveOne(threadIdPtr,
result);
assert(success && "Could not find MO");
const MemoryObject* MO = result.first;
const ObjectState* OS = result.second;
/* It is not guaranteed we'll get the Memory object with the address we
* asked for (e.g we might of asked for an address into a struct but
* we'll get a MemoryObject representing the whole struct). So compute
* the offset in the Object state that we want.
*/
uint64_t reqAddr = threadIdPtr->getZExtValue();
uint64_t givenAddr = MO->address;
if ( givenAddr > reqAddr)
assert(false && "Invalid MO");
dbgs() << "Have object:" << MO->name << "\n";
dbgs() << "With size:" << OS->size << "\n";
uint64_t offset = reqAddr - givenAddr;
ref<Expr> ids;
dbgs() << "Reading offset:" << offset << "\n";
ids = OS->read(offset, dataSize*num_dim, &state, executor.solver);
std::cerr << "Found :" << ids << "\n";
assert( !isa<ConstantExpr>(ids) && "Error: Found non symbolic.");
// Save the symbolic threadID
Thread& t = state.crtThread();
assert(t.getTid() != 0 && "Cannot use this function from main thread!");
t.setSymbolicThreadID(ids);
}
......@@ -157,6 +157,7 @@ namespace klee {
HANDLER(handleCos);
HANDLER(handleSin);
HANDLER(handleFPToSIRound);
HANDLER(handleSetWorkItemID);
#undef HANDLER
};
} // End klee namespace
......
......@@ -115,6 +115,14 @@ StackTrace Thread::getStackTrace() const {
return result;
}
void Thread::setSymbolicThreadID(ref<Expr> symbolicID)
{
assert( (this->symbolicThreadID.isNull()) &&
"Cannot set symbolic ID again");
this->symbolicThreadID = symbolicID;
}
void Thread::dumpStackTrace() const {
getStackTrace().dump(std::cerr);
}
......
......@@ -141,6 +141,10 @@ static void *work_item_thread(void *arg) {
memcpy40(prog->ids, params->ids, sizeof(size_t)*params->work_dim);
}
klee_assert( klee_is_symbolic(*(params->ids)) );
klee_set_work_item_id(params->ids, sizeof(size_t), params->work_dim);
klee_set_work_group_id(params->wgid);
if (prog->wgBarrierWlist)
*prog->wgBarrierWlist = wg_wlist;
......@@ -167,7 +171,11 @@ static int invoke_work_item(cl_kernel kern, uintptr_t args, cl_uint work_dim,
params->wg_wlist = wg_wlist;
params->global_wlist = global_wlist;
params->global_size = global_size;
klee_assert( klee_is_symbolic(*ids));
memcpy(params->ids, ids, sizeof(size_t)*work_dim);
klee_assert( klee_is_symbolic(*(params->ids)));
return pthread_create(pt, NULL, work_item_thread, params);
}
......@@ -400,6 +408,7 @@ cl_int clEnqueueNDRangeKernel(cl_command_queue command_queue,
/* Hack symbolic thread IDs */
klee_make_symbolic(ids, sizeof(size_t)*work_dim, threadString);
klee_assert( klee_is_symbolic(*ids) );
invoke_work_item(kernel,
argList,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment