add annotation redefinitions

Author: ladisgin

lib/Core/Executor.cpp

@@ -577,10 +577,10 @@ llvm::Module *Executor::setModule(
     kmodule->instrument(opts);
   }
 
-  if (interpreterOpts.MockStrategy != MockStrategy::None) {
-    MockBuilder mockBuilder(kmodule->module.get(), opts,
-                            ignoredExternals, redefinitions,
-                            interpreterHandler);
+  if (interpreterOpts.MockStrategy != MockStrategy::None ||
+      !opts.AnnotationsFile.empty()) {
+    MockBuilder mockBuilder(kmodule->module.get(), opts, ignoredExternals,
+                            redefinitions, interpreterHandler);
     std::unique_ptr<llvm::Module> mockModule = mockBuilder.build();
 
     std::vector<std::unique_ptr<llvm::Module>> mockModules;

lib/Core/MockBuilder.cpp

@@ -29,7 +29,7 @@ MockBuilder::getExternalFunctions() {
   std::map<std::string, llvm::FunctionType *> externals;
   for (const auto &f : userModule->functions()) {
     if (f.isDeclaration() && !f.use_empty() &&
-            !ignoredExternals.count(f.getName().str())) {
+        !ignoredExternals.count(f.getName().str())) {
       // NOTE: here we detect all the externals, even linked.
       externals.insert(std::make_pair(f.getName(), f.getFunctionType()));
     }
@@ -202,6 +202,14 @@ void MockBuilder::buildExternalFunctionsDefinitions() {
     if (nameToAnnotations != annotations.end()) {
       const auto &annotation = nameToAnnotations->second;
 
+      if (llvm::Function *f = userModule->getFunction(extName)) {
+        std::string replacedName = extName + "_replaced_by_mock";
+        klee_message("Renamed symbol %s to %s", f->getName().str().c_str(),
+                     replacedName.c_str());
+        redefinitions.emplace_back(f->getName(), extName);
+        f->setName(replacedName);
+      }
+
       buildAnnotationForExternalFunctionArgs(func, annotation.argsStatements);
       buildAnnotationForExternalFunctionReturn(func,
                                                annotation.returnStatements);