From 4d46147c6e63af8fe90a8bcfcc2502e85c81cf98 Mon Sep 17 00:00:00 2001
From: Simon Schuster <git@rationality.eu>
Date: Sat, 13 May 2017 19:07:14 +0200
Subject: [PATCH] Export "type: lbound" modelfacts to pml
Rational is to be able to bound loopiterations on model level.
Syntax is `#pragma platina lbound <num>` even though this syntax is not
final yet.
---
include/llvm/PML.h | 3 ++-
lib/CodeGen/PMLExport.cpp | 12 ++++++++++++
2 files changed, 14 insertions(+), 1 deletion(-)
diff --git a/include/llvm/PML.h b/include/llvm/PML.h
index 3bbd779790b..d5e9b914f80 100644
--- a/include/llvm/PML.h
+++ b/include/llvm/PML.h
@@ -934,12 +934,13 @@ struct MappingTraits< FlowFact* > {
YAML_IS_PTR_SEQUENCE_VECTOR(FlowFact)
/// Representation Level (source, bitcode, machinecode)
-enum PlatinaType { unknown, guard, callee };
+enum PlatinaType { unknown, guard, callee, lbound };
template <>
struct ScalarEnumerationTraits<PlatinaType> {
static void enumeration(IO &io, PlatinaType& level) {
io.enumCase(level, "guard", guard);
io.enumCase(level, "callee", callee);
+ io.enumCase(level, "lbound", lbound);
io.enumCase(level, "unknown", unknown);
}
};
diff --git a/lib/CodeGen/PMLExport.cpp b/lib/CodeGen/PMLExport.cpp
index 4ab38a773f2..84cee67f758 100644
--- a/lib/CodeGen/PMLExport.cpp
+++ b/lib/CodeGen/PMLExport.cpp
@@ -421,6 +421,18 @@ void PMLBitcodeExport::exportInstruction(yaml::Instruction* I,
MDString *expr = cast<MDString>(nexpr->getOperand(0));
if (type->getString() == "guard") {
YDoc.addPlatinaFact(createPlatinaFact(yaml::guard, &*BB, expr->getString()));
+ } else if(type->getString() == "lbound") {
+ Loop *Loop = LI.getLoopFor(&*BB);
+
+ if (Loop) {
+ const BasicBlock *Header = Loop->getHeader();
+ YDoc.addPlatinaFact(createPlatinaFact(yaml::lbound,
+ Header,
+ expr->getString()));
+ } else {
+ errs() << "Skipping: Cannot find loop for platina annotated loop bound:\n"
+ << *CI << "\n";
+ }
}
}
break;
--
GitLab