diff --git a/include/bounded-loop-unroller/bounded-loop-unroller.h b/include/bounded-loop-unroller/bounded-loop-unroller.h new file mode 100644 index 0000000..1133f2d --- /dev/null +++ b/include/bounded-loop-unroller/bounded-loop-unroller.h @@ -0,0 +1,10 @@ +#ifndef CINSTRUMENTATION_GOAL_INJECTOR_H +#define CINSTRUMENTATION_GOAL_INJECTOR_H + +#include +#include +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 diff --git a/include/bounded-loop-unroller/frontend_action.h b/include/bounded-loop-unroller/frontend_action.h new file mode 100644 index 0000000..3c7b795 --- /dev/null +++ b/include/bounded-loop-unroller/frontend_action.h @@ -0,0 +1,40 @@ +#ifndef CINSTRUMENTATION_FRONTEND_ACTION_H +#define CINSTRUMENTATION_FRONTEND_ACTION_H + +#include +#include +#include +#include +#include +#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 CreateASTConsumer ( + clang::CompilerInstance &CI, llvm::StringRef InFile) { + rewriter.setSourceMgr(CI.getSourceManager(), CI.getLangOpts()); + return std::make_unique(rewriter); + } + + void EndSourceFileAction() override; + + + protected: + clang::Rewriter rewriter; + const std::string file_output; + std::string &rewriter_output; + }; +} + +#endif //CINSTRUMENTATION_FRONTEND_ACTION_H diff --git a/include/bounded-loop-unroller/frontend_consumer.h b/include/bounded-loop-unroller/frontend_consumer.h new file mode 100644 index 0000000..dd8984e --- /dev/null +++ b/include/bounded-loop-unroller/frontend_consumer.h @@ -0,0 +1,34 @@ +#ifndef CINSTRUMENTATION_FRONTEND_CONSUMER_H +#define CINSTRUMENTATION_FRONTEND_CONSUMER_H + +#include +#include +#include +#include +#include +#include +#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 diff --git a/include/bounded-loop-unroller/frontend_visitor.h b/include/bounded-loop-unroller/frontend_visitor.h new file mode 100644 index 0000000..3828ce6 --- /dev/null +++ b/include/bounded-loop-unroller/frontend_visitor.h @@ -0,0 +1,59 @@ +#pragma once + +#include +#include +#include +#include + +/** + * 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 { + 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(); + + }; +} diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9a821fb..c4499f1 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,2 +1,2 @@ add_subdirectory(goal-injector) - +add_subdirectory(bounded-loop-unroller) diff --git a/src/bounded-loop-unroller/CMakeLists.txt b/src/bounded-loop-unroller/CMakeLists.txt new file mode 100644 index 0000000..b300df0 --- /dev/null +++ b/src/bounded-loop-unroller/CMakeLists.txt @@ -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) diff --git a/src/bounded-loop-unroller/frontend_action.cpp b/src/bounded-loop-unroller/frontend_action.cpp new file mode 100644 index 0000000..9888458 --- /dev/null +++ b/src/bounded-loop-unroller/frontend_action.cpp @@ -0,0 +1,28 @@ +#include +#include +#include + +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(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); + } +} diff --git a/src/bounded-loop-unroller/frontend_consumer.cpp b/src/bounded-loop-unroller/frontend_consumer.cpp new file mode 100644 index 0000000..e5106de --- /dev/null +++ b/src/bounded-loop-unroller/frontend_consumer.cpp @@ -0,0 +1 @@ +#include diff --git a/src/bounded-loop-unroller/frontend_visitor.cpp b/src/bounded-loop-unroller/frontend_visitor.cpp new file mode 100644 index 0000000..04ce063 --- /dev/null +++ b/src/bounded-loop-unroller/frontend_visitor.cpp @@ -0,0 +1,55 @@ +#include +#include + +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(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), "}"); + } +} diff --git a/src/bounded-loop-unroller/main.cpp b/src/bounded-loop-unroller/main.cpp new file mode 100644 index 0000000..cd4c6d7 --- /dev/null +++ b/src/bounded-loop-unroller/main.cpp @@ -0,0 +1,11 @@ +#include +#include +#include + +int main(int argc, char **argv) { + if (argc != 3) + std::cerr << "./loop-unroller \n"; + const std::ifstream input(argv[1]); + BoundedLoopUnroller::RunLoopUnroller(input, argv[2]); + return 0; +} diff --git a/src/goal-injector/main.cpp b/src/goal-injector/main.cpp index e3c0e9e..795731f 100644 --- a/src/goal-injector/main.cpp +++ b/src/goal-injector/main.cpp @@ -3,7 +3,7 @@ #include int main(int argc, char **argv) { - if (argc != 2) + if (argc != 3) std::cerr << "./injector \n"; const std::ifstream input(argv[1]); GoalInjector::RunGoalInjectorA(input, argv[2]);