Commit 8e9e5cfa authored by Dr. Michael Petter's avatar Dr. Michael Petter
Browse files

patched support for vizualization into fixpoint.cpp

parent c03aa190
...@@ -56,6 +56,8 @@ After successfull compilation, you can run your particular analysis on some exam ...@@ -56,6 +56,8 @@ After successfull compilation, you can run your particular analysis on some exam
There is a plugin for [Visual Studio Code](https://code.visualstudio.com/), that can be obtained from https://versioncontrolseidl.in.tum.de/schwarz/llvm-abstractinterpretation-vscode-plugin . This expects your inferred abstract domain values in a JSON file with extension `$target.out` next to `$target.ll`, which is used to present a CFG representation of your analysis target. There is a plugin for [Visual Studio Code](https://code.visualstudio.com/), that can be obtained from https://versioncontrolseidl.in.tum.de/schwarz/llvm-abstractinterpretation-vscode-plugin . This expects your inferred abstract domain values in a JSON file with extension `$target.out` next to `$target.ll`, which is used to present a CFG representation of your analysis target.
This is done semi-automatically by specifying the analysis pass parameter `-vo <filename>`. This automatically evaluates the abstract states `printOutgoing(BasicBlock const&,raw_ostream&,indentation)` function on all basic blocks, giving the programmer a way of providing Information about their abstract domain values as key/value pairs.
# Authors # Authors
## Author during Bachelor Thesis 2019/20 ## Author during Bachelor Thesis 2019/20
......
...@@ -18,9 +18,20 @@ ...@@ -18,9 +18,20 @@
#include "llvm/ADT/PostOrderIterator.h" #include "llvm/ADT/PostOrderIterator.h"
#include "llvm/Support/raw_os_ostream.h"
#include <fstream>
#include "llvm/Support/CommandLine.h"
static llvm::cl::opt<std::string>
OutputFilename("vo",
llvm::cl::desc("Specify the filename for the vizualization output"),
llvm::cl::value_desc("filename"));
namespace pcpo { namespace pcpo {
using namespace llvm; using namespace llvm;
using std::ostream;
using std::vector; using std::vector;
using std::pair; using std::pair;
using std::unordered_map; using std::unordered_map;
...@@ -336,7 +347,29 @@ void executeFixpointAlgorithm(Module const& M) { ...@@ -336,7 +347,29 @@ void executeFixpointAlgorithm(Module const& M) {
if (!worklist.empty()) { if (!worklist.empty()) {
dbgs(0) << "Iteration terminated due to exceeding loop count.\n"; dbgs(0) << "Iteration terminated due to exceeding loop count.\n";
} }
std::ofstream Res(OutputFilename.c_str());
unsigned int y=0;
if (Res.good()) {
dbgs(0) << "Output filename: " << OutputFilename.c_str();
std::error_code ErrInfo;
llvm::raw_fd_ostream Result(OutputFilename.c_str(),ErrInfo,llvm::sys::fs::F_None);
Result << "{\n";
for (auto const& [key, node]:nodes){
Result << " \"" << *node.basic_block << "\"" << ":{\n";
node.state.printOutgoing(*node.basic_block,Result,4);
Result << " }" ;
if (y++ != nodes.size()-1)
Result <<",";
Result<<"\n";
}
Result << "}\n";
Result.flush();
}
// Output the final result // Output the final result
dbgs(0) << "\nFinal result:\n"; dbgs(0) << "\nFinal result:\n";
for (auto const& [key, node]: nodes) { for (auto const& [key, node]: nodes) {
...@@ -348,11 +381,10 @@ void executeFixpointAlgorithm(Module const& M) { ...@@ -348,11 +381,10 @@ void executeFixpointAlgorithm(Module const& M) {
bool AbstractInterpretationPass::runOnModule(llvm::Module& M) { bool AbstractInterpretationPass::runOnModule(llvm::Module& M) {
using AbstractState = AbstractStateValueSet<SimpleInterval>; using AbstractState = AbstractStateValueSet<SimpleInterval>;
// Use either the standard fixpoint algorithm or the version with widening // Use either the standard fixpoint algorithm or the version with widening
// executeFixpointAlgorithm<AbstractState>(M); executeFixpointAlgorithm<AbstractState>(M);
// executeFixpointAlgorithm<NormalizedConjunction>(M); // executeFixpointAlgorithm<NormalizedConjunction>(M);
executeFixpointAlgorithm<LinearSubspace>(M); // executeFixpointAlgorithm<LinearSubspace>(M);
// executeFixpointAlgorithmWidening<AbstractState>(M); // executeFixpointAlgorithmWidening<AbstractState>(M);
// We never change anything // We never change anything
......
...@@ -386,17 +386,20 @@ public: ...@@ -386,17 +386,20 @@ public:
} }
} }
void printOutgoing(llvm::BasicBlock const& bb, llvm::raw_ostream& out, int indentation = 0) const { void printOutgoing(llvm::BasicBlock const& bb, llvm::raw_ostream& out, int indentation = 0) const {
unsigned int j=0;
for (auto const& i: values) { for (auto const& i: values) {
if (llvm::ReturnInst::classof(i.first)) { if (llvm::ReturnInst::classof(i.first)) {
out.indent(indentation) << "<ret> = " << i.second << '\n'; out.indent(indentation) << "\"<ret>\" : \"" << i.second<<"\"";
} else { } else {
out.indent(indentation) << '%' << i.first->getName() << " = " << i.second << '\n'; out.indent(indentation) << "\"%" << i.first->getName() << "\" : \"" << i.second << "\"";
} }
if(j++ != values.size() -1) out << ",";
out <<"\n";
} }
if (isBottom) { if (isBottom) {
out.indent(indentation) << "bottom\n"; out.indent(indentation) << "bottom\n";
} else if (values.size() == 0) { } else if (values.size() == 0) {
out.indent(indentation) << "<nothing>\n"; //out.indent(indentation) << "<nothing>\n";
} }
}; };
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment