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.

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

Add Edge-Function-Composer #10

Merged
merged 1 commit into from
Sep 3, 2018
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
5 changes: 3 additions & 2 deletions include/phasar/PhasarLLVM/IfdsIde/EdgeFunction.h
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,9 @@
#ifndef PHASAR_PHASARLLVM_IFDSIDE_EDGEFUNCTION_H_
#define PHASAR_PHASARLLVM_IFDSIDE_EDGEFUNCTION_H_

#include <iostream> // std::cout in dump, better replace it with a ostream
#include <memory>
#include <ostream>
#include <sstream>
#include <string>

namespace psr {
Expand All @@ -38,7 +39,7 @@ template <typename V> class EdgeFunction {
virtual bool equal_to(std::shared_ptr<EdgeFunction<V>> other) const = 0;

virtual void print(std::ostream &OS, bool isForDebug = false) const {
OS << "edge_function";
OS << "EdgeFunction";
}

std::string str() {
Expand Down
98 changes: 98 additions & 0 deletions include/phasar/PhasarLLVM/IfdsIde/EdgeFunctionComposer.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,98 @@
/******************************************************************************
* Copyright (c) 2017 Philipp Schubert.
* All rights reserved. This program and the accompanying materials are made
* available under the terms of LICENSE.txt.
*
* Contributors:
* Philipp Schubert and others
*****************************************************************************/

#ifndef PHASAR_PHASARLLVM_IFDSIDE_EDGEFUNCTIONCOMPOSER_H
#define PHASAR_PHASARLLVM_IFDSIDE_EDGEFUNCTIONCOMPOSER_H

#include <gtest/gtest_prod.h>
#include <memory>
#include <phasar/PhasarLLVM/IfdsIde/EdgeFunction.h>
#include <phasar/PhasarLLVM/IfdsIde/EdgeFunctions/AllBottom.h>
#include <phasar/PhasarLLVM/IfdsIde/EdgeFunctions/EdgeIdentity.h>

namespace psr {

/**
* This abstract class models edge function composition. It holds two edge
* functions. The edge function computation order is implemented as
* F -> G -> otherFunction
* i.e. F is computed before G, G is computed before otherFunction.
*
* Note that an own implementation for the join function is required, since
* this varies between different analyses, and is not implemented by this
* class.
* It is also advised to provide a more precise compose function, which is able
* to reduce the result of the composition, rather than using the default
* implementation. By default, an explicit composition is used. Such a function
* definition can grow unduly large.
*/
template <typename V>
class EdgeFunctionComposer
: public EdgeFunction<V>,
public std::enable_shared_from_this<EdgeFunctionComposer<V>> {
private:
// For debug purpose only
const unsigned EFComposer_Id;
static unsigned CurrEFComposer_Id;

protected:
/// First edge function
std::shared_ptr<EdgeFunction<V>> F;
/// Second edge function
std::shared_ptr<EdgeFunction<V>> G;

public:
EdgeFunctionComposer(std::shared_ptr<EdgeFunction<V>> F,
std::shared_ptr<EdgeFunction<V>> G)
: EFComposer_Id(++CurrEFComposer_Id), F(F), G(G) {}

/**
* Target value computation is implemented as
* G(F(source))
*/
virtual V computeTarget(V source) override {
return G->computeTarget(F->computeTarget(source));
}

/**
* Function composition is implemented as an explicit composition, i.e.
* (secondFunction * G) * F = EFC(F, EFC(G , otherFunction))
*
* However, it is advised to immediately reduce the resulting edge function
* by providing an own implementation of this function.
*/
virtual std::shared_ptr<EdgeFunction<V>>
composeWith(std::shared_ptr<EdgeFunction<V>> secondFunction) override {
if (auto *EI = dynamic_cast<EdgeIdentity<V> *>(secondFunction.get())) {
return this->shared_from_this();
}
return F->composeWith(G->composeWith(secondFunction));
}

// virtual std::shared_ptr<EdgeFunction<V>>
// joinWith(std::shared_ptr<EdgeFunction<V>> otherFunction) = 0;

virtual bool equal_to(std::shared_ptr<EdgeFunction<V>> other) const override {
if (auto EFC = dynamic_cast<EdgeFunctionComposer<V> *>(other.get())) {
return F->equal_to(EFC->F) && G->equal_to(EFC->G);
}
return false;
}

virtual void print(std::ostream &OS, bool isForDebug = false) const override {
OS << "EFComposer_" << EFComposer_Id << "[ " << F.get()->str() << " , "
<< G.get()->str() << " ]";
}
};

template <typename V> unsigned EdgeFunctionComposer<V>::CurrEFComposer_Id = 0;

} // namespace psr

#endif
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ class AllBottom : public EdgeFunction<V>,
}

virtual void print(std::ostream &OS, bool isForDebug = false) const override {
OS << "all_bottom";
OS << "AllBottom";
}
};

Expand Down
2 changes: 1 addition & 1 deletion include/phasar/PhasarLLVM/IfdsIde/EdgeFunctions/AllTop.h
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ class AllTop : public EdgeFunction<V>,
}

virtual void print(std::ostream &OS, bool isForDebug = false) const override {
OS << "all_top";
OS << "AllTop";
}
};

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ class EdgeIdentity : public EdgeFunction<V>,
}

virtual void print(std::ostream &OS, bool isForDebug = false) const override {
OS << "edge_identity";
OS << "EdgeIdentity";
}
};

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
#include <vector>

#include <phasar/PhasarLLVM/IfdsIde/DefaultIDETabulationProblem.h>
#include <phasar/PhasarLLVM/IfdsIde/EdgeFunctionComposer.h>

namespace llvm {
class Instruction;
Expand All @@ -34,6 +35,11 @@ class IDELinearConstantAnalysis
private:
std::vector<std::string> EntryPoints;

// For debug purpose only
static unsigned CurrStoreConst_Id;
static unsigned CurrLoadStoreV_Id;
static unsigned CurrBinary_Id;

public:
typedef const llvm::Value *d_t;
typedef const llvm::Instruction *n_t;
Expand All @@ -42,12 +48,6 @@ class IDELinearConstantAnalysis
typedef int64_t v_t;
typedef LLVMBasedICFG &i_t;

// For debug purpose only
static unsigned StoreConstCount;
static unsigned LoadStoreValueCount;
static unsigned BinaryCount;
static unsigned EdgeComposerCount;

static const v_t TOP;
static const v_t BOTTOM;

Expand Down Expand Up @@ -113,46 +113,26 @@ class IDELinearConstantAnalysis

std::shared_ptr<EdgeFunction<v_t>> allTopFunction() override;

/**
* secondFunction o G o F
*
* compose with: EFC(F, EFC(G,secondFunction))
* compute target: G(F(source))
*
* java solution:
* compose: G -> F -> secondFunction
* compute target: F(G(source))
*/
class EdgeFunctionComposer
: public EdgeFunction<v_t>,
public std::enable_shared_from_this<EdgeFunctionComposer> {
private:
const unsigned EdgeFunctionID;
std::shared_ptr<EdgeFunction<v_t>> F;
std::shared_ptr<EdgeFunction<v_t>> G;
// Custom EdgeFunction declarations

class LCAEdgeFunctionComposer : public EdgeFunctionComposer<v_t> {
public:
EdgeFunctionComposer(std::shared_ptr<EdgeFunction<v_t>> F,
std::shared_ptr<EdgeFunction<v_t>> G);

v_t computeTarget(v_t source) override;
LCAEdgeFunctionComposer(std::shared_ptr<EdgeFunction<v_t>> F,
std::shared_ptr<EdgeFunction<v_t>> G)
: EdgeFunctionComposer<v_t>(F, G){};

std::shared_ptr<EdgeFunction<v_t>>
composeWith(std::shared_ptr<EdgeFunction<v_t>> secondFunction) override;

std::shared_ptr<EdgeFunction<v_t>>
joinWith(std::shared_ptr<EdgeFunction<v_t>> otherFunction) override;

bool equal_to(std::shared_ptr<EdgeFunction<v_t>> other) const override;

void print(std::ostream &OS, bool isForDebug = false) const override;
};

class StoreConstant : public EdgeFunction<v_t>,
public std::enable_shared_from_this<StoreConstant> {
private:
const unsigned EdgeFunctionID;
const IDELinearConstantAnalysis::v_t IntConst;
const unsigned StoreConst_Id;
const v_t IntConst;

public:
explicit StoreConstant(v_t IntConst);
Expand All @@ -174,7 +154,7 @@ class IDELinearConstantAnalysis
: public EdgeFunction<v_t>,
public std::enable_shared_from_this<LoadStoreValueIdentity> {
private:
const unsigned EdgeFunctionID;
const unsigned LoadStoreV_Id;

public:
explicit LoadStoreValueIdentity();
Expand All @@ -192,6 +172,22 @@ class IDELinearConstantAnalysis
void print(std::ostream &OS, bool isForDebug = false) const override;
};

// Helper functions

/**
* The following binary operations are computed:
* - addition
* - subtraction
* - multiplication
* - division (signed/unsinged)
* - remainder (signed/unsinged)
*
* @brief Computes the result of a binary operation.
* @param op operator
* @param lop left operand
* @param rop right operand
* @return Result of binary operation
*/
static v_t executeBinOperation(const unsigned op, v_t lop, v_t rop);

std::string DtoString(d_t d) const override;
Expand Down
5 changes: 1 addition & 4 deletions lib/Controller/AnalysisController.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -275,10 +275,7 @@ AnalysisController::AnalysisController(
for (auto exit : ICFG.getExitPointsOf(f)) {
cout << "Exit : " << lcaproblem.NtoString(exit) << endl;
for (auto res : llvmlcasolver.resultsAt(exit, true)) {
cout << "Value: "
<< (res.second == lcaproblem.bottomElement()
? "BOT"
: lcaproblem.VtoString(res.second))
cout << "Value: " << lcaproblem.VtoString(res.second)
<< "\tat " << lcaproblem.DtoString(res.first) << endl;
}
}
Expand Down
Loading