-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
451eb07
commit 43e8fe5
Showing
11 changed files
with
252 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
#ifndef CINSTRUMENTATION_GOAL_INJECTOR_H | ||
#define CINSTRUMENTATION_GOAL_INJECTOR_H | ||
|
||
#include <string> | ||
#include <fstream> | ||
namespace BoundedLoopUnroller { | ||
std::string RunLoopUnroller(const std::string input, const std::string output); | ||
std::string RunLoopUnroller(const std::ifstream &input, const std::string output); | ||
} | ||
#endif //CINSTRUMENTATION_GOAL_INJECTOR_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
#ifndef CINSTRUMENTATION_FRONTEND_ACTION_H | ||
#define CINSTRUMENTATION_FRONTEND_ACTION_H | ||
|
||
#include <clang/Frontend/CompilerInstance.h> | ||
#include <clang/Frontend/FrontendActions.h> | ||
#include <clang/Lex/Preprocessor.h> | ||
#include <clang/Rewrite/Core/Rewriter.h> | ||
#include <clang/Tooling/Tooling.h> | ||
#include "frontend_consumer.h" | ||
#include "frontend_action.h" | ||
|
||
/* | ||
* This is just the entry point for a Library/Plugin/etc. | ||
* | ||
* If you are looking for the instrumentation, go to frontend_visitor | ||
*/ | ||
namespace BoundedLoopUnroller { | ||
class frontend_action : public clang::ASTFrontendAction { | ||
public: | ||
|
||
explicit frontend_action(const std::string file_output, std::string &rewriter_output) : file_output( | ||
file_output), rewriter_output(rewriter_output) {} | ||
|
||
virtual std::unique_ptr<clang::ASTConsumer> CreateASTConsumer ( | ||
clang::CompilerInstance &CI, llvm::StringRef InFile) { | ||
rewriter.setSourceMgr(CI.getSourceManager(), CI.getLangOpts()); | ||
return std::make_unique<frontend_consumer>(rewriter); | ||
} | ||
|
||
void EndSourceFileAction() override; | ||
|
||
|
||
protected: | ||
clang::Rewriter rewriter; | ||
const std::string file_output; | ||
std::string &rewriter_output; | ||
}; | ||
} | ||
|
||
#endif //CINSTRUMENTATION_FRONTEND_ACTION_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,34 @@ | ||
#ifndef CINSTRUMENTATION_FRONTEND_CONSUMER_H | ||
#define CINSTRUMENTATION_FRONTEND_CONSUMER_H | ||
|
||
#include <clang/Frontend/CompilerInstance.h> | ||
#include <clang/Frontend/FrontendActions.h> | ||
#include <clang/Lex/Preprocessor.h> | ||
#include <clang/Rewrite/Core/Rewriter.h> | ||
#include <clang/Tooling/Tooling.h> | ||
#include <clang/AST/ASTConsumer.h> | ||
#include "frontend_visitor.h" | ||
|
||
/* | ||
* This is just a top-level of how a translation unit should be traversed. | ||
* | ||
* If you are looking for the instrumentation, go to frontend_visitor | ||
*/ | ||
namespace BoundedLoopUnroller { | ||
|
||
class frontend_consumer : public clang::ASTConsumer { | ||
public: | ||
explicit frontend_consumer(clang::Rewriter &rewriter) : rewriter(rewriter), Visitor(rewriter) {} | ||
|
||
virtual void HandleTranslationUnit(clang::ASTContext &Context) { | ||
Visitor.TraverseAST(Context); | ||
} | ||
|
||
private: | ||
clang::Rewriter &rewriter; | ||
// A RecursiveASTVisitor implementation. | ||
frontend_visitor Visitor; | ||
}; | ||
} | ||
|
||
#endif //CINSTRUMENTATION_FRONTEND_CONSUMER_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,59 @@ | ||
#pragma once | ||
|
||
#include <clang/AST/RecursiveASTVisitor.h> | ||
#include <clang/AST/DeclCXX.h> | ||
#include <clang/Rewrite/Core/Rewriter.h> | ||
#include <sstream> | ||
|
||
/** | ||
* This is where the instrumentatoin takes place. | ||
* | ||
* 1. Clang will automatically call for every VisitXXX(XXX *). For this instrumentation, we are mainly interested | ||
* in /IfStmt/, /WhileStmt/ and all other statements that cause branching. | ||
* Check the full statements list here: https://clang.llvm.org/doxygen/classclang_1_1Stmt.html | ||
* | ||
* 2. After we find one of these /branching/ statements, we then instrument its body | ||
* | ||
* 3. We can instrument by: | ||
* a. Using the same approach of FuSeBMC (i.e., GOAL_1:, GOAL_2:, etc.) | ||
* b. Add an assert(0), reach_error (or equivalent). | ||
* | ||
* For now, I will go with the option 3b, as it seems easier to integrate with ESBMC. However, it can cause problems | ||
* during source code rewriting. Specifically, because C allows one-instruction if/while/etc commands. | ||
* This means that if the body of the interesting expressions are not /CompoundStmt/ we will need to manually create a | ||
* scope. | ||
*/ | ||
namespace BoundedLoopUnroller { | ||
class frontend_visitor | ||
: public clang::RecursiveASTVisitor<frontend_visitor> { | ||
public: | ||
explicit frontend_visitor(clang::Rewriter &rewriter) : rewriter(rewriter) {} | ||
|
||
bool VisitWhileStmt(clang::WhileStmt *expr); | ||
|
||
bool VisitIfStmt(clang::IfStmt *expr); | ||
|
||
bool VisitForStmt(clang::ForStmt *expr); | ||
|
||
bool VisitFunctionDecl(clang::FunctionDecl *F); | ||
|
||
/* | ||
* SwitchCase | ||
* dowhile | ||
*/ | ||
|
||
protected: | ||
void InjectOnStmt(clang::Stmt *stmt); | ||
|
||
void InjectOnCompoundStmt(clang::CompoundStmt *stmt); | ||
|
||
void InjectOnNonCompoundStmt(clang::Stmt *stmt); | ||
|
||
private: | ||
int counter = 0; | ||
clang::Rewriter &rewriter; | ||
std::string goal_str(); | ||
std::string goal_block_str(); | ||
|
||
}; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
add_subdirectory(goal-injector) | ||
|
||
add_subdirectory(bounded-loop-unroller) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
add_library(bounded-loop-unroller frontend_action.cpp frontend_consumer.cpp frontend_visitor.cpp) | ||
target_include_directories(bounded-loop-unroller | ||
PRIVATE ${CLANG_INCLUDE_DIRS} | ||
) | ||
set_target_properties(bounded-loop-unroller PROPERTIES COMPILE_FLAGS "-fno-rtti") | ||
target_link_libraries(bounded-loop-unroller clangTooling clangAST clangIndex fmt::fmt) | ||
|
||
add_executable(loop-unroller main.cpp) | ||
target_include_directories(instrumentator | ||
PRIVATE ${CLANG_INCLUDE_DIRS} | ||
) | ||
target_link_libraries(loop-unroller PUBLIC bounded-loop-unroller clangTooling clangAST clangIndex) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,28 @@ | ||
#include <bounded-loop-unroller/frontend_action.h> | ||
#include <bounded-loop-unroller/frontend_consumer.h> | ||
#include <bounded-loop-unroller/bounded-loop-unroller.h> | ||
|
||
namespace BoundedLoopUnroller { | ||
void frontend_action::EndSourceFileAction() { | ||
clang::SourceManager &SM = rewriter.getSourceMgr(); | ||
|
||
// Now emit the rewritten buffer. | ||
llvm::raw_string_ostream ross(rewriter_output); | ||
rewriter.getEditBuffer(SM.getMainFileID()).write(ross); | ||
std::error_code error_code; | ||
llvm::raw_fd_ostream outFile(file_output, error_code, llvm::sys::fs::OF_None); | ||
rewriter.getEditBuffer(SM.getMainFileID()).write(outFile); // --> this will write the result to outFile | ||
outFile.close(); | ||
} | ||
|
||
std::string RunLoopUnroller(const std::string input, const std::string output) { | ||
std::string result; | ||
clang::tooling::runToolOnCode(std::make_unique<frontend_action>(output, result), input); | ||
return result; | ||
} | ||
std::string RunLoopUnroller(const std::ifstream &input, const std::string output) { | ||
std::ostringstream oss; | ||
oss << input.rdbuf(); | ||
return RunLoopUnroller(oss.str(), output); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
#include <bounded-loop-unroller/frontend_consumer.h> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
#include <bounded-loop-unroller/frontend_visitor.h> | ||
#include <fmt/core.h> | ||
|
||
namespace BoundedLoopUnroller { | ||
bool frontend_visitor::VisitWhileStmt(clang::WhileStmt *expr) { | ||
InjectOnStmt(expr->getBody()); | ||
return true; | ||
} | ||
|
||
bool frontend_visitor::VisitIfStmt(clang::IfStmt *expr) { | ||
InjectOnStmt(expr->getThen()); | ||
InjectOnStmt(expr->getElse()); | ||
return true; | ||
} | ||
|
||
bool frontend_visitor::VisitForStmt(clang::ForStmt *expr) { | ||
InjectOnStmt(expr->getBody()); | ||
return true; | ||
} | ||
|
||
bool frontend_visitor::VisitFunctionDecl(clang::FunctionDecl *F) { | ||
InjectOnStmt(F->getBody()); | ||
return true; | ||
} | ||
|
||
|
||
void frontend_visitor::InjectOnStmt(clang::Stmt *stmt) { | ||
if (!stmt) | ||
return; | ||
|
||
if (stmt->getStmtClass() == clang::Stmt::CompoundStmtClass) { | ||
InjectOnCompoundStmt(static_cast<clang::CompoundStmt *>(stmt)); | ||
} else { | ||
InjectOnNonCompoundStmt(stmt); | ||
} | ||
} | ||
|
||
std::string frontend_visitor::goal_str() { | ||
return fmt::format("__ESBMC_assert(0, \"{}\");", counter++); | ||
} | ||
|
||
std::string frontend_visitor::goal_block_str() { | ||
return fmt::format("{}__ESBMC_assert(0, \"{}\");", "{", counter++); | ||
} | ||
void frontend_visitor::InjectOnCompoundStmt(clang::CompoundStmt *stmt) { | ||
// TODO: Not sure whether begin or end location is the best | ||
rewriter.InsertTextAfter(stmt->getBeginLoc().getLocWithOffset(1), goal_str()); | ||
} | ||
|
||
void frontend_visitor::InjectOnNonCompoundStmt(clang::Stmt *stmt) { | ||
// TODO: Not sure whether begin or end location is the best | ||
rewriter.InsertTextAfter(stmt->getBeginLoc(), goal_block_str()); | ||
rewriter.InsertTextAfter(stmt->getEndLoc().getLocWithOffset(1), "}"); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
#include <bounded-loop-unroller/bounded-loop-unroller.h> | ||
#include <fstream> | ||
#include <iostream> | ||
|
||
int main(int argc, char **argv) { | ||
if (argc != 3) | ||
std::cerr << "./loop-unroller <input.c> <output.c>\n"; | ||
const std::ifstream input(argv[1]); | ||
BoundedLoopUnroller::RunLoopUnroller(input, argv[2]); | ||
return 0; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters