about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--lib/Module/KLEEIRMetaData.h51
1 files changed, 51 insertions, 0 deletions
diff --git a/lib/Module/KLEEIRMetaData.h b/lib/Module/KLEEIRMetaData.h
new file mode 100644
index 00000000..86c24d05
--- /dev/null
+++ b/lib/Module/KLEEIRMetaData.h
@@ -0,0 +1,51 @@
+//===-- KLEEIRMetaData.h ----------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LIB_MODULE_KLEEIRMETADATA_H_
+#define LIB_MODULE_KLEEIRMETADATA_H_
+
+#include "llvm/IR/MDBuilder.h"
+
+namespace klee {
+
+/// Handles KLEE-specific LLVM IR meta-data.
+class KleeIRMetaData : public llvm::MDBuilder {
+
+  llvm::LLVMContext &Context;
+
+public:
+  KleeIRMetaData(llvm::LLVMContext &context)
+      : llvm::MDBuilder(context), Context(context) {}
+
+  /// \brief Return a string node reflecting the value
+  llvm::MDNode *createStringNode(llvm::StringRef value) {
+    return llvm::MDNode::get(Context, createString(value));
+  }
+
+  void addAnnotation(llvm::Instruction &inst, llvm::StringRef key,
+                           llvm::StringRef value) {
+    inst.setMetadata(key, createStringNode(value));
+  }
+
+  /// \brief Check if the instruction has the key/value meta data
+  static bool hasAnnotation(const llvm::Instruction &inst, llvm::StringRef key,
+                             llvm::StringRef value) {
+    auto v = inst.getMetadata(key);
+    if (!v)
+      return false;
+    auto sv = llvm::dyn_cast<llvm::MDString>(v->getOperand(0));
+    if (!sv)
+      return false;
+
+    return sv->getString().equals(value);
+  }
+};
+}
+
+#endif /* LIB_MODULE_KLEEIRMETADATA_H_ */