From 3b60f898d3cc1f8196e625416a142d4598e2aa85 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Thu, 12 Nov 2020 21:17:46 -0400 Subject: [PATCH 1/2] added function name option on target pass --- modules/backend/pass/TargetPass.cpp | 6 ++++++ modules/backend/pass/TargetPass.hpp | 10 ++++++++-- modules/frontend/caller.cpp | 3 ++- modules/frontend/map2check.cpp | 6 ++++-- 4 files changed, 20 insertions(+), 5 deletions(-) diff --git a/modules/backend/pass/TargetPass.cpp b/modules/backend/pass/TargetPass.cpp index 14d1dd5c..d410c55a 100644 --- a/modules/backend/pass/TargetPass.cpp +++ b/modules/backend/pass/TargetPass.cpp @@ -11,6 +11,12 @@ #include "TargetPass.hpp" bool TargetPass::runOnFunction(Function& F) { + llvm::errs() << "Running TargetPass with: " << this->targetFunctionName; + + // We need to have the definition of the function + F.getParent()->getOrInsertFunction( + this->targetFunctionName, Type::getVoidTy(F.getContext())); + this->targetFunctionMap2Check = F.getParent()->getOrInsertFunction( "map2check_target_function", Type::getVoidTy(F.getContext()), Type::getInt8PtrTy(F.getContext()), Type::getInt32Ty(F.getContext()), diff --git a/modules/backend/pass/TargetPass.hpp b/modules/backend/pass/TargetPass.hpp index 13fca9b9..e146dd2a 100644 --- a/modules/backend/pass/TargetPass.hpp +++ b/modules/backend/pass/TargetPass.hpp @@ -19,6 +19,7 @@ #include #include #include +#include #include #include @@ -38,10 +39,15 @@ using llvm::IRBuilder; using llvm::LLVMContext; using llvm::RegisterPass; using llvm::Value; +//using llvm::cl; +// Target option +static llvm::cl::opt TargetNameOption("function-name", llvm::cl::desc("Specify the target function"), llvm::cl::init("__VERIFIER_error")); struct TargetPass : public FunctionPass { static char ID; - TargetPass() : FunctionPass(ID) {} + TargetPass() : FunctionPass(ID) { + targetFunctionName = TargetNameOption; + } explicit TargetPass(std::string FunctionName) : FunctionPass(ID) { targetFunctionName = FunctionName; } @@ -56,7 +62,7 @@ struct TargetPass : public FunctionPass { BasicBlock::iterator currentInstruction; Constant *targetFunctionMap2Check = NULL; Value *functionName = NULL; - std::string targetFunctionName = "__VERIFIER_error"; + std::string targetFunctionName; }; #endif // MODULES_BACKEND_PASS_TARGETPASS_HPP_ diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index bc553f0d..43da5e39 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -177,9 +177,10 @@ int Caller::callPass(std::string target_function, bool sv_comp) { } case Map2CheckMode::REACHABILITY_MODE: { Map2Check::Log::Info("Running reachability mode"); + Map2Check::Log::Debug("Target function: " + target_function); std::string targetPass = "${MAP2CHECK_PATH}/lib/libTargetPass"; transformCommand << " -load " << targetPass << getLibSuffix() - << " -target_function"; + << " -target_function -function-name " << target_function; break; } diff --git a/modules/frontend/map2check.cpp b/modules/frontend/map2check.cpp index c53d0ee6..e1542177 100644 --- a/modules/frontend/map2check.cpp +++ b/modules/frontend/map2check.cpp @@ -302,7 +302,9 @@ int main(int argc, char **argv) { z3 (Z3 is default), btor (Boolector), and yices2 (Yices))") ("timeout", po::value(), "\ttimeout for map2check execution") - ("target-function", "\tsearches for __VERIFIER_error is reachable") + ("target-function", "\tchecks wether is reachable") + ("target-function-name", po::value()->default_value("__VERIFIER_error"), + R"(define the function name to be searched)") ("generate-testcase", "\tcreates c program with fail testcase (experimental)") ("memtrack", "\tcheck for memory errors") ("print-counter", "\tprint counterexample") @@ -371,7 +373,7 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))") args.timeout = timeout; } if (vm.count("target-function")) { - string function = "__VERIFIER_error"; + string function = vm["target-function-name"].as(); args.function = function; args.mode = Map2Check::Map2CheckMode::REACHABILITY_MODE; args.spectTrue = "target-function"; From 483aabc29a685566ab2c7d078b70f39c6c452c4e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Thu, 12 Nov 2020 21:18:36 -0400 Subject: [PATCH 2/2] removed definition from pass --- modules/backend/pass/TargetPass.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/modules/backend/pass/TargetPass.cpp b/modules/backend/pass/TargetPass.cpp index d410c55a..3048d828 100644 --- a/modules/backend/pass/TargetPass.cpp +++ b/modules/backend/pass/TargetPass.cpp @@ -13,10 +13,6 @@ bool TargetPass::runOnFunction(Function& F) { llvm::errs() << "Running TargetPass with: " << this->targetFunctionName; - // We need to have the definition of the function - F.getParent()->getOrInsertFunction( - this->targetFunctionName, Type::getVoidTy(F.getContext())); - this->targetFunctionMap2Check = F.getParent()->getOrInsertFunction( "map2check_target_function", Type::getVoidTy(F.getContext()), Type::getInt8PtrTy(F.getContext()), Type::getInt32Ty(F.getContext()),