Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Added function name option into TargetPass #46

Open
wants to merge 2 commits into
base: develop
Choose a base branch
from
Open

Added function name option into TargetPass #46

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3b60f89
added function name option on target pass
rafaelsamenezes Nov 13, 2020
483aabc
removed definition from pass
rafaelsamenezes Nov 13, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions modules/backend/pass/TargetPass.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@
#include "TargetPass.hpp"

bool TargetPass::runOnFunction(Function& F) {
llvm::errs() << "Running TargetPass with: " << this->targetFunctionName;

this->targetFunctionMap2Check = F.getParent()->getOrInsertFunction(
"map2check_target_function", Type::getVoidTy(F.getContext()),
Type::getInt8PtrTy(F.getContext()), Type::getInt32Ty(F.getContext()),
Expand Down
10 changes: 8 additions & 2 deletions modules/backend/pass/TargetPass.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@
#include <llvm/IR/Module.h>
#include <llvm/Pass.h>
#include <llvm/Support/raw_ostream.h>
#include <llvm/Support/CommandLine.h>

#include <iostream>
#include <sstream>
Expand All @@ -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<std::string> 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;
}
Expand All @@ -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_
3 changes: 2 additions & 1 deletion modules/frontend/caller.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
6 changes: 4 additions & 2 deletions modules/frontend/map2check.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -302,7 +302,9 @@ int main(int argc, char **argv) {
z3 (Z3 is default), btor (Boolector), and yices2 (Yices))")
("timeout", po::value<unsigned>(),
"\ttimeout for map2check execution")
("target-function", "\tsearches for __VERIFIER_error is reachable")
("target-function", "\tchecks wether <target-functions> is reachable")
("target-function-name", po::value<std::string>()->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")
Expand Down Expand Up @@ -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<string>();
args.function = function;
args.mode = Map2Check::Map2CheckMode::REACHABILITY_MODE;
args.spectTrue = "target-function";
Expand Down