void SpecialFunctionHandler::handleRealloc(ExecutionState &state,
		KInstruction *target, std::vector<ref<Expr> > &arguments) {
	// XXX should type check args
	assert(arguments.size() == 2 && "invalid number of arguments to realloc");
	ref<Expr> address = arguments[0];
	ref<Expr> size = arguments[1];

	Executor::StatePair zeroSize = executor.fork(state,
			Expr::createIsZero(size), true);

	if (zeroSize.first) { // size == 0
		executor.executeFree(*zeroSize.first, address, target);
	}
	if (zeroSize.second) { // size != 0
		Executor::StatePair zeroPointer = executor.fork(*zeroSize.second,
				Expr::createIsZero(address), true);

		if (zeroPointer.first) { // address == 0
			executor.executeAlloc(*zeroPointer.first, size, false, target);
		}
		if (zeroPointer.second) { // address != 0
			Executor::ExactResolutionList rl;
			executor.resolveExact(*zeroPointer.second, address, rl, "realloc");

			for (Executor::ExactResolutionList::iterator it = rl.begin(), ie =
					rl.end(); it != ie; ++it) {
				executor.executeAlloc(*it->second, size, false, target, false,
						it->first.second);
			}
		}
	}
}

void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
                                                KInstruction *target,
                                                std::vector<ref<Expr> > &arguments) {
  std::string name;

  // FIXME: For backwards compatibility, we should eventually enforce the
  // correct arguments.
  if (arguments.size() == 2) {
    name = "unnamed";
  } else {
    // FIXME: Should be a user.err, not an assert.
    assert(arguments.size()==3 &&
           "invalid number of arguments to klee_make_symbolic");  
    name = readStringAtAddress(state, arguments[2]);
  }

  Executor::ExactResolutionList rl;
  executor.resolveExact(state, arguments[0], rl, "make_symbolic");
  
  for (Executor::ExactResolutionList::iterator it = rl.begin(), 
         ie = rl.end(); it != ie; ++it) {
    const MemoryObject *mo = it->first.first;
    mo->setName(name);
    
    const ObjectState *old = it->first.second;
    ExecutionState *s = it->second;
    
    if (old->readOnly) {
      executor.terminateStateOnError(*s, 
                                     "cannot make readonly object symbolic", 
                                     "user.err");
      return;
    } 

    // FIXME: Type coercion should be done consistently somewhere.
    bool res;
    bool success __attribute__ ((unused)) =
      executor.solver->mustBeTrue(*s, 
                                  EqExpr::create(ZExtExpr::create(arguments[1],
                                                                  Context::get().getPointerWidth()),
                                                 mo->getSizeExpr()),
                                  res);
    assert(success && "FIXME: Unhandled solver failure");
    
    if (res) {
      executor.executeMakeSymbolic(*s, mo, name);
    } else {      
      executor.terminateStateOnError(*s, 
                                     "wrong size given to klee_make_symbolic[_name]", 
                                     "user.err");
    }
  }
}

void SpecialFunctionHandler::handleGetObjSize(ExecutionState &state,
		KInstruction *target, std::vector<ref<Expr> > &arguments) {
	// XXX should type check args
	assert(
			arguments.size() == 1
					&& "invalid number of arguments to klee_get_obj_size");
	Executor::ExactResolutionList rl;
	executor.resolveExact(state, arguments[0], rl, "klee_get_obj_size");
	for (Executor::ExactResolutionList::iterator it = rl.begin(), ie = rl.end();
			it != ie; ++it) {
		executor.bindLocal(target, it->second->currentThread,
				ConstantExpr::create(it->first.first->size, Expr::Int32));
	}
}

void SpecialFunctionHandler::handleMakeLengthSymbolic(ExecutionState &state,
                                                KInstruction *target,
                                                std::vector<ref<Expr> > &arguments) {
  std::string name;
  assert(arguments.size()==3 && "invalid number of arguments to klee_make_symbolic");  
  name = readStringAtAddress(state, arguments[2]);
  
  //std::cerr << "make_length_symbolic called len_rl.size=" << len_rl.size() << " \n";
    
  Executor::ExactResolutionList rl;
  executor.resolveExact(state, arguments[0], rl, "make_symbolic");
  
  for (Executor::ExactResolutionList::iterator it = rl.begin(), 
         ie = rl.end(); it != ie; ++it) {
    
    const ObjectState *old = it->first.second;
    ExecutionState *s = it->second;
    
    //allocate space for len_mo
    MemoryObject *len_mo = executor.executeNoBindAlloc(*s, 4);  //4-byte int
    len_mo->setName(name + "_len");
    len_mo->onlyTrackLength = 0;
    len_mo->isALength = 1;  
    executor.executeMakeSymbolic(*s, len_mo);    

    MemoryObject *mo = (MemoryObject*) it->first.first;
    mo->setName(name);
    mo->onlyTrackLength = 1;
    mo->isALength = 0;
    
    mo->length = len_mo;  //important! makes len_mo track mo->length
    
    if (old->readOnly) { 
      executor.terminateStateOnError(*s, "cannot make readonly object symbolic", "user.err");
      return;
    } 

    // FIXME: Type coercion should be done consistently somewhere.
    bool res;
    bool success = executor.solver->mustBeTrue(*s,EqExpr::create(ZExtExpr::create(arguments[1], Context::get().getPointerWidth()), mo->getSizeExpr()), res);
    assert(success && "FIXME: Unhandled solver failure");
    
    if (res) {
      executor.executeMakeSymbolic(*s, mo);
    } else {      
      executor.terminateStateOnError(*s, "wrong size given to klee_make_symbolic[_name]", "user.err");
    }
  }
}

void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state,
		KInstruction *target, std::vector<ref<Expr> > &arguments) {
	assert(
			arguments.size() == 1
					&& "invalid number of arguments to klee_mark_global");

	Executor::ExactResolutionList rl;
	executor.resolveExact(state, arguments[0], rl, "mark_global");

	for (Executor::ExactResolutionList::iterator it = rl.begin(), ie = rl.end();
			it != ie; ++it) {
		const MemoryObject *mo = it->first.first;
		assert(!mo->isLocal);
		mo->isGlobal = true;
	}
}

void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
                                             KInstruction *target,
                                             std::vector<ref<Expr> > &arguments) {
  assert(arguments.size()==2 &&
         "invalid number of arguments to klee_prefex_cex");

  ref<Expr> cond = arguments[1];
  if (cond->getWidth() != Expr::Bool)
    cond = NeExpr::create(cond, ConstantExpr::alloc(0, cond->getWidth()));

  Executor::ExactResolutionList rl;
  executor.resolveExact(state, arguments[0], rl, "prefex_cex");
  
  assert(rl.size() == 1 &&
         "prefer_cex target must resolve to precisely one object");

  rl[0].first.first->cexPreferences.push_back(cond);
}