-
Notifications
You must be signed in to change notification settings - Fork 143
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'development' into f-ModernizedLLVMTypeHierarchy
Showing
104 changed files
with
9,689 additions
and
640 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel and others | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_DATAFLOW_IFDSIDE_SOLVER_ESGEDGEKIND_H | ||
#define PHASAR_DATAFLOW_IFDSIDE_SOLVER_ESGEDGEKIND_H | ||
|
||
namespace psr { | ||
enum class ESGEdgeKind { Normal, Call, CallToRet, SkipUnknownFn, Ret, Summary }; | ||
|
||
constexpr bool isInterProc(ESGEdgeKind Kind) noexcept { | ||
return Kind == ESGEdgeKind::Call || Kind == ESGEdgeKind::Ret; | ||
} | ||
|
||
} // namespace psr | ||
|
||
#endif // PHASAR_DATAFLOW_IFDSIDE_SOLVER_ESGEDGEKIND_H |
Large diffs are not rendered by default.
Oops, something went wrong.
69 changes: 69 additions & 0 deletions
69
include/phasar/DataFlow/IfdsIde/Solver/PathAwareIDESolver.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,69 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel and others | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_DATAFLOW_IFDSIDE_SOLVER_PATHAWAREIDESOLVER_H | ||
#define PHASAR_DATAFLOW_IFDSIDE_SOLVER_PATHAWAREIDESOLVER_H | ||
|
||
#include "phasar/DataFlow/IfdsIde/IDETabulationProblem.h" | ||
#include "phasar/DataFlow/IfdsIde/Solver/ESGEdgeKind.h" | ||
#include "phasar/DataFlow/IfdsIde/Solver/IDESolver.h" | ||
#include "phasar/DataFlow/PathSensitivity/ExplodedSuperGraph.h" | ||
#include "phasar/Utils/Logger.h" | ||
|
||
namespace psr { | ||
template <typename AnalysisDomainTy, | ||
typename Container = std::set<typename AnalysisDomainTy::d_t>> | ||
class PathAwareIDESolver : public IDESolver<AnalysisDomainTy, Container> { | ||
using base_t = IDESolver<AnalysisDomainTy, Container>; | ||
|
||
public: | ||
using domain_t = AnalysisDomainTy; | ||
using n_t = typename base_t::n_t; | ||
using d_t = typename base_t::d_t; | ||
using i_t = typename base_t::i_t; | ||
using container_type = typename base_t::container_type; | ||
|
||
explicit PathAwareIDESolver( | ||
IDETabulationProblem<domain_t, container_type> &Problem, const i_t *ICF) | ||
: base_t(Problem, ICF), ESG(Problem.getZeroValue()) { | ||
|
||
if (Problem.getIFDSIDESolverConfig().autoAddZero()) { | ||
PHASAR_LOG_LEVEL( | ||
WARNING, | ||
"The PathAwareIDESolver is initialized with the option 'autoAddZero' " | ||
"being set. This might degrade the quality of the computed paths!"); | ||
} | ||
} | ||
|
||
[[nodiscard]] const ExplodedSuperGraph<domain_t> & | ||
getExplicitESG() const &noexcept { | ||
return ESG; | ||
} | ||
|
||
[[nodiscard]] ExplodedSuperGraph<domain_t> &&getExplicitESG() &&noexcept { | ||
return std::move(ESG); | ||
} | ||
|
||
private: | ||
void saveEdges(n_t Curr, n_t Succ, d_t CurrNode, | ||
const container_type &SuccNodes, ESGEdgeKind Kind) override { | ||
ESG.saveEdges(std::move(Curr), std::move(CurrNode), std::move(Succ), | ||
SuccNodes, Kind); | ||
} | ||
|
||
ExplodedSuperGraph<domain_t> ESG; | ||
}; | ||
|
||
template <typename ProblemTy> | ||
PathAwareIDESolver(ProblemTy &) | ||
-> PathAwareIDESolver<typename ProblemTy::ProblemAnalysisDomain>; | ||
|
||
} // namespace psr | ||
|
||
#endif // PHASAR_DATAFLOW_IFDSIDE_SOLVER_PATHAWAREIDESOLVER_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
382 changes: 382 additions & 0 deletions
382
include/phasar/DataFlow/PathSensitivity/ExplodedSuperGraph.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,382 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel and others | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_DATAFLOW_PATHSENSITIVITY_EXPLODEDSUPERGRAPH_H | ||
#define PHASAR_DATAFLOW_PATHSENSITIVITY_EXPLODEDSUPERGRAPH_H | ||
|
||
#include "phasar/DataFlow/IfdsIde/Solver/ESGEdgeKind.h" | ||
#include "phasar/Utils/ByRef.h" | ||
#include "phasar/Utils/Logger.h" | ||
#include "phasar/Utils/Printer.h" | ||
#include "phasar/Utils/StableVector.h" | ||
#include "phasar/Utils/Utilities.h" | ||
|
||
#include "llvm/ADT/DenseMapInfo.h" | ||
#include "llvm/ADT/STLExtras.h" | ||
#include "llvm/ADT/Sequence.h" | ||
#include "llvm/ADT/SmallPtrSet.h" | ||
#include "llvm/ADT/TinyPtrVector.h" | ||
#include "llvm/ADT/iterator_range.h" | ||
#include "llvm/IR/Instructions.h" | ||
#include "llvm/Support/Casting.h" | ||
#include "llvm/Support/Compiler.h" | ||
#include "llvm/Support/ErrorHandling.h" | ||
#include "llvm/Support/raw_os_ostream.h" | ||
#include "llvm/Support/raw_ostream.h" | ||
|
||
#include <cstddef> | ||
#include <cstdio> | ||
#include <numeric> | ||
#include <optional> | ||
#include <set> | ||
#include <string> | ||
#include <type_traits> | ||
#include <unordered_map> | ||
#include <unordered_set> | ||
#include <utility> | ||
|
||
namespace psr { | ||
|
||
/// An explicit representation of the ExplodedSuperGraph (ESG) of an IFDS/IDE | ||
/// analysis. | ||
/// | ||
/// Not all covered instructions of a BasicBlock might be present; however, it | ||
/// is guaranteed that for each BasicBlock covered by the analysis there is at | ||
/// least one node in the ExplicitESG containing an instruction from that BB. | ||
template <typename AnalysisDomainTy> class ExplodedSuperGraph { | ||
public: | ||
using n_t = typename AnalysisDomainTy::n_t; | ||
using d_t = typename AnalysisDomainTy::d_t; | ||
|
||
struct Node { | ||
static constexpr size_t NoPredId = ~size_t(0); | ||
}; | ||
|
||
struct NodeData { | ||
d_t Value{}; | ||
n_t Source{}; | ||
}; | ||
|
||
struct NodeAdj { | ||
size_t PredecessorIdx = Node::NoPredId; | ||
llvm::SmallVector<size_t, 0> Neighbors{}; | ||
}; | ||
|
||
class BuildNodeRef; | ||
class NodeRef { | ||
friend ExplodedSuperGraph; | ||
friend class BuildNodeRef; | ||
|
||
public: | ||
NodeRef() noexcept = default; | ||
NodeRef(std::nullptr_t) noexcept {} | ||
|
||
[[nodiscard]] ByConstRef<d_t> value() const noexcept { | ||
assert(*this); | ||
return Owner->NodeDataOwner[NodeId].Value; | ||
} | ||
|
||
[[nodiscard]] ByConstRef<n_t> source() const noexcept { | ||
assert(*this); | ||
return Owner->NodeDataOwner[NodeId].Source; | ||
} | ||
|
||
[[nodiscard]] NodeRef predecessor() const noexcept { | ||
assert(*this); | ||
auto PredId = Owner->NodeAdjOwner[NodeId].PredecessorIdx; | ||
return PredId == Node::NoPredId ? NodeRef() : NodeRef(PredId, Owner); | ||
} | ||
|
||
[[nodiscard]] bool hasNeighbors() const noexcept { | ||
assert(*this); | ||
return !Owner->NodeAdjOwner[NodeId].Neighbors.empty(); | ||
} | ||
|
||
[[nodiscard]] bool getNumNeighbors() const noexcept { | ||
assert(*this); | ||
return Owner->NodeAdjOwner[NodeId].Neighbors.size(); | ||
} | ||
|
||
[[nodiscard]] auto neighbors() const noexcept { | ||
assert(*this); | ||
|
||
return llvm::map_range(Owner->NodeAdjOwner[NodeId].Neighbors, | ||
[Owner{Owner}](size_t NBIdx) { | ||
assert(NBIdx != Node::NoPredId); | ||
return NodeRef(NBIdx, Owner); | ||
}); | ||
} | ||
|
||
[[nodiscard]] size_t id() const noexcept { return NodeId; } | ||
|
||
explicit operator bool() const noexcept { | ||
return Owner != nullptr && NodeId != Node::NoPredId; | ||
} | ||
|
||
[[nodiscard]] friend bool operator==(NodeRef L, NodeRef R) noexcept { | ||
return L.NodeId == R.NodeId && L.Owner == R.Owner; | ||
} | ||
[[nodiscard]] friend bool operator!=(NodeRef L, NodeRef R) noexcept { | ||
return !(L == R); | ||
} | ||
[[nodiscard]] friend bool operator==(NodeRef L, | ||
std::nullptr_t /*R*/) noexcept { | ||
return L.Owner == nullptr; | ||
} | ||
[[nodiscard]] friend bool operator!=(NodeRef L, std::nullptr_t R) noexcept { | ||
return !(L == R); | ||
} | ||
|
||
friend llvm::hash_code hash_value(NodeRef NR) noexcept { // NOLINT | ||
return llvm::hash_combine(NR.NodeId, NR.Owner); | ||
} | ||
|
||
private: | ||
explicit NodeRef(size_t NodeId, const ExplodedSuperGraph *Owner) noexcept | ||
: NodeId(NodeId), Owner(Owner) {} | ||
|
||
size_t NodeId = Node::NoPredId; | ||
const ExplodedSuperGraph *Owner{}; | ||
}; | ||
|
||
class BuildNodeRef { | ||
public: | ||
[[nodiscard]] NodeRef operator()(size_t NodeId) const noexcept { | ||
return NodeRef(NodeId, Owner); | ||
} | ||
|
||
private: | ||
explicit BuildNodeRef(const ExplodedSuperGraph *Owner) noexcept | ||
: Owner(Owner) {} | ||
|
||
const ExplodedSuperGraph *Owner{}; | ||
}; | ||
|
||
explicit ExplodedSuperGraph(d_t ZeroValue) noexcept( | ||
std::is_nothrow_move_constructible_v<d_t>) | ||
: ZeroValue(std::move(ZeroValue)) {} | ||
|
||
explicit ExplodedSuperGraph(const ExplodedSuperGraph &) = default; | ||
ExplodedSuperGraph &operator=(const ExplodedSuperGraph &) = delete; | ||
|
||
ExplodedSuperGraph(ExplodedSuperGraph &&) noexcept = default; | ||
ExplodedSuperGraph &operator=(ExplodedSuperGraph &&) noexcept = default; | ||
|
||
~ExplodedSuperGraph() = default; | ||
|
||
[[nodiscard]] NodeRef getNodeOrNull(n_t Inst, d_t Fact) const { | ||
auto It = FlowFactVertexMap.find( | ||
std::make_pair(std::move(Inst), std::move(Fact))); | ||
if (It != FlowFactVertexMap.end()) { | ||
return NodeRef(It->second, this); | ||
} | ||
return nullptr; | ||
} | ||
|
||
[[nodiscard]] NodeRef fromNodeId(size_t NodeId) const noexcept { | ||
assert(NodeDataOwner.size() == NodeAdjOwner.size()); | ||
assert(NodeId < NodeDataOwner.size()); | ||
|
||
return NodeRef(NodeId, this); | ||
} | ||
|
||
[[nodiscard]] ByConstRef<d_t> getZeroValue() const noexcept { | ||
return ZeroValue; | ||
} | ||
|
||
template <typename Container> | ||
void saveEdges(n_t Curr, d_t CurrNode, n_t Succ, const Container &SuccNodes, | ||
ESGEdgeKind Kind) { | ||
auto PredId = getNodeIdOrNull(Curr, std::move(CurrNode)); | ||
|
||
/// The Identity CTR-flow on the zero-value has no meaning at all regarding | ||
/// path sensitivity, so skip it | ||
bool MaySkipEdge = Kind == ESGEdgeKind::CallToRet && CurrNode == ZeroValue; | ||
for (const d_t &SuccNode : SuccNodes) { | ||
saveEdge(PredId, Curr, CurrNode, Succ, SuccNode, MaySkipEdge); | ||
} | ||
} | ||
|
||
// NOLINTNEXTLINE(readability-identifier-naming) | ||
[[nodiscard]] auto node_begin() const noexcept { | ||
assert(NodeAdjOwner.size() == NodeDataOwner.size()); | ||
return llvm::map_iterator( | ||
llvm::seq(size_t(0), NodeDataOwner.size()).begin(), BuildNodeRef(this)); | ||
} | ||
// NOLINTNEXTLINE(readability-identifier-naming) | ||
[[nodiscard]] auto node_end() const noexcept { | ||
assert(NodeAdjOwner.size() == NodeDataOwner.size()); | ||
return llvm::map_iterator(llvm::seq(size_t(0), NodeDataOwner.size()).end(), | ||
BuildNodeRef(this)); | ||
} | ||
[[nodiscard]] auto nodes() const noexcept { | ||
assert(NodeAdjOwner.size() == NodeDataOwner.size()); | ||
return llvm::map_range(llvm::seq(size_t(0), NodeDataOwner.size()), | ||
BuildNodeRef(this)); | ||
} | ||
|
||
[[nodiscard]] size_t size() const noexcept { | ||
assert(NodeAdjOwner.size() == NodeDataOwner.size()); | ||
return NodeDataOwner.size(); | ||
} | ||
|
||
/// Printing: | ||
|
||
void printAsDot(llvm::raw_ostream &OS) const { | ||
assert(NodeAdjOwner.size() == NodeDataOwner.size()); | ||
OS << "digraph ESG{\n"; | ||
psr::scope_exit ClosingBrace = [&OS] { OS << '}'; }; | ||
|
||
for (size_t I = 0, End = NodeDataOwner.size(); I != End; ++I) { | ||
auto Nod = NodeRef(I, this); | ||
OS << I << "[label=\""; | ||
OS.write_escaped(DToString(Nod.value())) << "\"];\n"; | ||
|
||
OS << I << "->" << intptr_t(Nod.predecessor().id()) | ||
<< R"([style="bold" label=")"; | ||
OS.write_escaped(NToString(Nod.source())) << "\"];\n"; | ||
for (auto NB : Nod.neighbors()) { | ||
OS << I << "->" << NB.id() << "[color=\"red\"];\n"; | ||
} | ||
} | ||
} | ||
|
||
void printAsDot(std::ostream &OS) const { | ||
llvm::raw_os_ostream ROS(OS); | ||
printAsDot(ROS); | ||
} | ||
|
||
void printESGNodes(llvm::raw_ostream &OS) const { | ||
for (const auto &[Node, _] : FlowFactVertexMap) { | ||
OS << "( " << NToString(Node.first) << "; " << DToString(Node.second) | ||
<< " )\n"; | ||
} | ||
} | ||
|
||
private: | ||
struct PathInfoHash { | ||
size_t operator()(const std::pair<n_t, d_t> &ND) const { | ||
return std::hash<n_t>()(ND.first) * 31 + std::hash<d_t>()(ND.second); | ||
} | ||
}; | ||
|
||
struct PathInfoEq { | ||
bool operator()(const std::pair<n_t, d_t> &Lhs, | ||
const std::pair<n_t, d_t> &Rhs) const { | ||
return Lhs.first == Rhs.first && Lhs.second == Rhs.second; | ||
} | ||
}; | ||
|
||
[[nodiscard]] std::optional<size_t> getNodeIdOrNull(n_t Inst, | ||
d_t Fact) const { | ||
auto It = FlowFactVertexMap.find( | ||
std::make_pair(std::move(Inst), std::move(Fact))); | ||
if (It != FlowFactVertexMap.end()) { | ||
return It->second; | ||
} | ||
return std::nullopt; | ||
} | ||
|
||
void saveEdge(std::optional<size_t> PredId, n_t Curr, d_t CurrNode, n_t Succ, | ||
d_t SuccNode, bool MaySkipEdge) { | ||
auto [SuccVtxIt, Inserted] = FlowFactVertexMap.try_emplace( | ||
std::make_pair(Succ, SuccNode), Node::NoPredId); | ||
|
||
// Save a reference into the FlowFactVertexMap before the SuccVtxIt gets | ||
// invalidated | ||
auto &SuccVtxNode = SuccVtxIt->second; | ||
|
||
// NOLINTNEXTLINE(readability-identifier-naming) | ||
auto makeNode = [this, PredId, Curr, &CurrNode, &SuccNode]() mutable { | ||
assert(NodeAdjOwner.size() == NodeDataOwner.size()); | ||
auto Ret = NodeDataOwner.size(); | ||
|
||
auto &NodData = NodeDataOwner.emplace_back(); | ||
auto &NodAdj = NodeAdjOwner.emplace_back(); | ||
NodData.Value = SuccNode; | ||
|
||
if (!PredId) { | ||
// For the seeds: Just that the FlowFactVertexMap is filled at that | ||
// position... | ||
FlowFactVertexMap[std::make_pair(Curr, CurrNode)] = Ret; | ||
} | ||
|
||
NodAdj.PredecessorIdx = PredId.value_or(Node::NoPredId); | ||
NodData.Source = Curr; | ||
|
||
return Ret; | ||
}; | ||
|
||
if (MaySkipEdge && SuccNode == CurrNode) { | ||
// This CTR edge carries no information, so skip it. | ||
// We still want to create the destination node for the ret-FF later | ||
assert(PredId); | ||
if (Inserted) { | ||
SuccVtxNode = makeNode(); | ||
NodeAdjOwner.back().PredecessorIdx = Node::NoPredId; | ||
} | ||
return; | ||
} | ||
|
||
if (PredId && NodeDataOwner[*PredId].Value == SuccNode && | ||
NodeDataOwner[*PredId].Source->getParent() == Succ->getParent() && | ||
SuccNode != ZeroValue) { | ||
|
||
// Identity edge, we don't need a new node; just assign the Pred here | ||
if (Inserted) { | ||
SuccVtxNode = *PredId; | ||
return; | ||
} | ||
|
||
// This edge has already been here?! | ||
if (*PredId == SuccVtxNode) { | ||
return; | ||
} | ||
} | ||
|
||
if (Inserted) { | ||
SuccVtxNode = makeNode(); | ||
return; | ||
} | ||
|
||
// Node has already been created, but MaySkipEdge above prevented us from | ||
// connecting with the pred. Now, we have a non-skippable edge to connect to | ||
NodeRef SuccVtx(SuccVtxNode, this); | ||
if (!SuccVtx.predecessor()) { | ||
NodeAdjOwner[SuccVtxNode].PredecessorIdx = | ||
PredId.value_or(Node::NoPredId); | ||
NodeDataOwner[SuccVtxNode].Source = Curr; | ||
return; | ||
} | ||
|
||
// This node has more than one predecessor; add a neighbor then | ||
if (SuccVtx.predecessor().id() != PredId.value_or(Node::NoPredId) && | ||
llvm::none_of(SuccVtx.neighbors(), | ||
[Pred = PredId.value_or(Node::NoPredId)](NodeRef Nd) { | ||
return Nd.predecessor().id() == Pred; | ||
})) { | ||
|
||
auto NewNode = makeNode(); | ||
NodeAdjOwner[SuccVtxNode].Neighbors.push_back(NewNode); | ||
return; | ||
} | ||
} | ||
|
||
std::vector<NodeData> NodeDataOwner; | ||
std::vector<NodeAdj> NodeAdjOwner; | ||
std::unordered_map<std::pair<n_t, d_t>, size_t, PathInfoHash, PathInfoEq> | ||
FlowFactVertexMap{}; | ||
|
||
// ZeroValue | ||
d_t ZeroValue; | ||
}; | ||
|
||
} // namespace psr | ||
|
||
#endif // PHASAR_DATAFLOW_PATHSENSITIVITY_EXPLODEDSUPERGRAPH_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,59 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel and others | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_PHASARLLVM_DATAFLOW_PATHSENSITIVITY_FLOWPATH_H | ||
#define PHASAR_PHASARLLVM_DATAFLOW_PATHSENSITIVITY_FLOWPATH_H | ||
|
||
#include "llvm/ADT/ArrayRef.h" | ||
#include "llvm/ADT/SmallVector.h" | ||
|
||
#include "z3++.h" | ||
|
||
namespace psr { | ||
template <typename N> struct FlowPath { | ||
llvm::SmallVector<N, 0> Path; | ||
z3::expr Constraint; | ||
z3::model Model; | ||
|
||
FlowPath(llvm::ArrayRef<N> Path, const z3::expr &Constraint) | ||
: Path(Path.begin(), Path.end()), Constraint(Constraint), | ||
Model(Constraint.ctx()) {} | ||
FlowPath(llvm::ArrayRef<N> Path, const z3::expr &Constraint, | ||
const z3::model &Model) | ||
: Path(Path.begin(), Path.end()), Constraint(Constraint), Model(Model) {} | ||
|
||
[[nodiscard]] auto begin() noexcept { return Path.begin(); } | ||
[[nodiscard]] auto end() noexcept { return Path.end(); } | ||
[[nodiscard]] auto begin() const noexcept { return Path.begin(); } | ||
[[nodiscard]] auto end() const noexcept { return Path.end(); } | ||
[[nodiscard]] auto cbegin() const noexcept { return Path.cbegin(); } | ||
[[nodiscard]] auto cend() const noexcept { return Path.cend(); } | ||
|
||
[[nodiscard]] size_t size() const noexcept { return Path.size(); } | ||
[[nodiscard]] bool empty() const noexcept { return Path.empty(); } | ||
|
||
[[nodiscard]] decltype(auto) operator[](size_t Idx) const { | ||
return Path[Idx]; | ||
} | ||
|
||
[[nodiscard]] operator llvm::ArrayRef<N>() const noexcept { return Path; } | ||
|
||
[[nodiscard]] bool operator==(const FlowPath &Other) const noexcept { | ||
return Other.Path == Path; | ||
} | ||
[[nodiscard]] bool operator!=(const FlowPath &Other) const noexcept { | ||
return !(*this == Other); | ||
} | ||
}; | ||
|
||
template <typename N> using FlowPathSequence = std::vector<FlowPath<N>>; | ||
|
||
} // namespace psr | ||
|
||
#endif // PHASAR_PHASARLLVM_DATAFLOW_PATHSENSITIVITY_FLOWPATH_H |
57 changes: 57 additions & 0 deletions
57
include/phasar/DataFlow/PathSensitivity/PathSensitivityConfig.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,57 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel and others | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYCONFIG_H | ||
#define PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYCONFIG_H | ||
|
||
#include <cstddef> | ||
#include <cstdint> | ||
|
||
namespace psr { | ||
|
||
template <typename DerivedConfig> struct PathSensitivityConfigBase { | ||
size_t DAGSizeThreshold = SIZE_MAX; | ||
size_t DAGDepthThreshold = SIZE_MAX; | ||
size_t NumPathsThreshold = SIZE_MAX; | ||
bool MinimizeDAG = true; | ||
|
||
[[nodiscard]] DerivedConfig | ||
withDAGSizeThreshold(size_t MaxDAGSize) const noexcept { | ||
auto Ret = *static_cast<const DerivedConfig *>(this); | ||
Ret.DAGSizeThreshold = MaxDAGSize; | ||
return Ret; | ||
} | ||
|
||
[[nodiscard]] DerivedConfig | ||
withDAGDepthThreshold(size_t MaxDAGDepth) const noexcept { | ||
auto Ret = *static_cast<const DerivedConfig *>(this); | ||
Ret.DAGDepthThreshold = MaxDAGDepth; | ||
return Ret; | ||
} | ||
|
||
[[nodiscard]] DerivedConfig | ||
withNumPathsThreshold(size_t MaxNumPaths) const noexcept { | ||
auto Ret = *static_cast<const DerivedConfig *>(this); | ||
Ret.NumPathsThreshold = MaxNumPaths; | ||
return Ret; | ||
} | ||
|
||
[[nodiscard]] DerivedConfig withMinimizeDAG(bool DoMinimize) const noexcept { | ||
auto Ret = *static_cast<const DerivedConfig *>(this); | ||
Ret.MinimizeDAG = DoMinimize; | ||
return Ret; | ||
} | ||
}; | ||
|
||
struct PathSensitivityConfig | ||
: PathSensitivityConfigBase<PathSensitivityConfig> {}; | ||
|
||
} // namespace psr | ||
|
||
#endif // PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYCONFIG_H |
54 changes: 54 additions & 0 deletions
54
include/phasar/DataFlow/PathSensitivity/PathSensitivityManager.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,54 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel and others | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYMANAGER_H | ||
#define PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYMANAGER_H | ||
|
||
#include "phasar/DataFlow/PathSensitivity/ExplodedSuperGraph.h" | ||
#include "phasar/DataFlow/PathSensitivity/PathSensitivityConfig.h" | ||
#include "phasar/DataFlow/PathSensitivity/PathSensitivityManagerBase.h" | ||
#include "phasar/DataFlow/PathSensitivity/PathSensitivityManagerMixin.h" | ||
#include "phasar/Utils/AdjacencyList.h" | ||
#include "phasar/Utils/DFAMinimizer.h" | ||
#include "phasar/Utils/GraphTraits.h" | ||
#include "phasar/Utils/Logger.h" | ||
|
||
#include "llvm/ADT/SetVector.h" | ||
#include "llvm/ADT/Twine.h" | ||
#include "llvm/Support/ErrorHandling.h" | ||
|
||
#include <cassert> | ||
#include <type_traits> | ||
|
||
namespace psr { | ||
|
||
template <typename AnalysisDomainTy> | ||
class PathSensitivityManager | ||
: public PathSensitivityManagerBase<typename AnalysisDomainTy::n_t>, | ||
public PathSensitivityManagerMixin< | ||
PathSensitivityManager<AnalysisDomainTy>, AnalysisDomainTy, | ||
typename PathSensitivityManagerBase< | ||
typename AnalysisDomainTy::n_t>::graph_type> { | ||
using base_t = PathSensitivityManagerBase<typename AnalysisDomainTy::n_t>; | ||
using mixin_t = | ||
PathSensitivityManagerMixin<PathSensitivityManager, AnalysisDomainTy, | ||
typename base_t::graph_type>; | ||
|
||
public: | ||
using n_t = typename AnalysisDomainTy::n_t; | ||
using d_t = typename AnalysisDomainTy::d_t; | ||
using typename PathSensitivityManagerBase<n_t>::graph_type; | ||
|
||
PathSensitivityManager( | ||
const ExplodedSuperGraph<AnalysisDomainTy> *ESG) noexcept | ||
: mixin_t(ESG) {} | ||
}; | ||
} // namespace psr | ||
|
||
#endif // PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYMANAGER_H |
191 changes: 191 additions & 0 deletions
191
include/phasar/DataFlow/PathSensitivity/PathSensitivityManagerBase.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,191 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel and others | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYMANAGERBASE_H | ||
#define PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYMANAGERBASE_H | ||
|
||
#include "phasar/Utils/AdjacencyList.h" | ||
#include "phasar/Utils/Logger.h" | ||
#include "phasar/Utils/Utilities.h" | ||
|
||
#include "llvm/ADT/DenseSet.h" | ||
#include "llvm/ADT/IntEqClasses.h" | ||
#include "llvm/ADT/SmallVector.h" | ||
|
||
namespace llvm { | ||
class Instruction; | ||
} // namespace llvm | ||
|
||
namespace psr { | ||
|
||
template <typename Derived, typename AnalysisDomainTy, typename GraphType> | ||
class PathSensitivityManagerMixin; | ||
|
||
template <typename N> class PathSensitivityManagerBase { | ||
public: | ||
using n_t = N; | ||
using graph_type = AdjacencyList<llvm::SmallVector<n_t, 0>>; | ||
|
||
static_assert(std::is_integral_v<typename GraphTraits<graph_type>::vertex_t>); | ||
|
||
template <typename Derived, typename AnalysisDomainTy, typename GraphType> | ||
friend class PathSensitivityManagerMixin; | ||
|
||
protected: | ||
using graph_traits_t = GraphTraits<graph_type>; | ||
using vertex_t = typename graph_traits_t::vertex_t; | ||
|
||
private: | ||
[[nodiscard]] bool assertIsDAG(const graph_type &Dag) const { | ||
llvm::BitVector Visited(graph_traits_t::size(Dag)); | ||
llvm::DenseSet<vertex_t> CurrPath; | ||
CurrPath.reserve(graph_traits_t::size(Dag)); | ||
|
||
// NOLINTNEXTLINE(readability-identifier-naming) | ||
auto doAssertIsDAG = [&CurrPath, &Visited, &Dag](auto &doAssertIsDAG, | ||
vertex_t Vtx) { | ||
if (!CurrPath.insert(Vtx).second) { | ||
PHASAR_LOG_LEVEL(ERROR, "DAG has circle: Vtx: " << uintptr_t(Vtx)); | ||
return false; | ||
} | ||
|
||
scope_exit CurrPathPop = [&CurrPath, Vtx] { CurrPath.erase(Vtx); }; | ||
if (Visited.test(Vtx)) { | ||
/// We have already analyzed this node | ||
/// NOTE: We must check this _after_ doing the circle check. Otherwise, | ||
/// that can never be true | ||
return true; | ||
} | ||
|
||
Visited.set(Vtx); | ||
|
||
for (auto Succ : graph_traits_t::outEdges(Dag, Vtx)) { | ||
if (!doAssertIsDAG(doAssertIsDAG, Succ)) { | ||
return false; | ||
} | ||
} | ||
return true; | ||
}; | ||
|
||
for (auto Rt : graph_traits_t::roots(Dag)) { | ||
if (!doAssertIsDAG(doAssertIsDAG, Rt)) { | ||
return false; | ||
} | ||
} | ||
|
||
return true; | ||
} | ||
|
||
template <typename VertexTransform> | ||
[[nodiscard]] static graph_type | ||
reverseDAG(graph_type &&Dag, const VertexTransform &Equiv, size_t EquivSize, | ||
size_t MaxDepth) { | ||
using graph_traits_t = psr::GraphTraits<graph_type>; | ||
using vertex_t = typename graph_traits_t::vertex_t; | ||
graph_type Ret{}; | ||
if constexpr (psr::is_reservable_graph_trait_v<graph_traits_t>) { | ||
graph_traits_t::reserve(Ret, EquivSize); | ||
} | ||
|
||
// Allocate a buffer for the temporary data needed. | ||
// We need: | ||
// - A cache of vertex_t | ||
// - One worklist WLConsume of pair<vertex_t, vertex_t> where we read from | ||
// - One worklist WLInsert of same type where we insert to | ||
|
||
// We iterate over the graph in levels. Each level corresponds to the | ||
// distance from a root node. We always have all nodes from a level inside a | ||
// worklist | ||
// -- The level we are processing is in WLConsume, the next level in | ||
// WLInsert. This way, we can stop the process, when we have reached the | ||
// MaxDepth | ||
|
||
constexpr auto Factor = | ||
sizeof(vertex_t) + 2 * sizeof(std::pair<vertex_t, vertex_t>); | ||
assert(EquivSize <= SIZE_MAX / Factor && "Overflow on size calculation"); | ||
auto NumBytes = Factor * EquivSize; | ||
|
||
// For performance reasons, we wish to allocate the buffer on the stack, if | ||
// it is small enough | ||
static constexpr size_t MaxNumBytesInStackBuf = 8192; | ||
|
||
auto *Buf = NumBytes <= MaxNumBytesInStackBuf | ||
? reinterpret_cast<char *>(alloca(NumBytes)) | ||
: new char[NumBytes]; | ||
std::unique_ptr<char[]> Owner; // NOLINT | ||
if (NumBytes > MaxNumBytesInStackBuf) { | ||
Owner.reset(Buf); | ||
} | ||
|
||
auto Cache = reinterpret_cast<vertex_t *>(Buf); | ||
std::uninitialized_fill_n(Cache, EquivSize, graph_traits_t::Invalid); | ||
|
||
auto *WLConsumeBegin = | ||
reinterpret_cast<std::pair<vertex_t, vertex_t> *>(Cache + EquivSize); | ||
auto *WLConsumeEnd = WLConsumeBegin; | ||
auto *WLInsertBegin = WLConsumeBegin + EquivSize; | ||
auto *WLInsertEnd = WLInsertBegin; | ||
|
||
for (auto Rt : graph_traits_t::roots(Dag)) { | ||
size_t Eq = std::invoke(Equiv, Rt); | ||
if (Cache[Eq] == graph_traits_t::Invalid) { | ||
Cache[Eq] = graph_traits_t::addNode(Ret, graph_traits_t::node(Dag, Rt)); | ||
*WLConsumeEnd++ = {Rt, Cache[Eq]}; | ||
} | ||
} | ||
|
||
size_t Depth = 0; | ||
|
||
while (WLConsumeBegin != WLConsumeEnd && Depth < MaxDepth) { | ||
for (auto [Vtx, Rev] : llvm::make_range(WLConsumeBegin, WLConsumeEnd)) { | ||
|
||
for (auto Succ : graph_traits_t::outEdges(Dag, Vtx)) { | ||
auto SuccVtx = graph_traits_t::target(Succ); | ||
size_t Eq = std::invoke(Equiv, SuccVtx); | ||
if (Cache[Eq] == graph_traits_t::Invalid) { | ||
Cache[Eq] = graph_traits_t::addNode( | ||
Ret, graph_traits_t::node(Dag, SuccVtx)); | ||
*WLInsertEnd++ = {SuccVtx, Cache[Eq]}; | ||
} | ||
|
||
auto SuccRev = Cache[Eq]; | ||
graph_traits_t::addEdge(Ret, SuccRev, | ||
graph_traits_t::withEdgeTarget(Succ, Rev)); | ||
} | ||
if (graph_traits_t::outDegree(Dag, Vtx) == 0) { | ||
graph_traits_t::addRoot(Ret, Rev); | ||
} | ||
} | ||
|
||
std::swap(WLConsumeBegin, WLInsertBegin); | ||
WLConsumeEnd = std::exchange(WLInsertEnd, WLInsertBegin); | ||
++Depth; | ||
} | ||
|
||
for (auto [Rt, RtRev] : llvm::make_range(WLConsumeBegin, WLConsumeEnd)) { | ||
// All nodes that were cut off because they are at depth MaxDepth must | ||
// become roots | ||
graph_traits_t::addRoot(Ret, RtRev); | ||
} | ||
|
||
return Ret; | ||
} | ||
|
||
[[nodiscard]] static graph_type reverseDAG(graph_type &&Dag, | ||
size_t MaxDepth) { | ||
auto Sz = graph_traits_t::size(Dag); | ||
return reverseDAG(std::move(Dag), identity{}, Sz, MaxDepth); | ||
} | ||
}; | ||
|
||
extern template class PathSensitivityManagerBase<const llvm::Instruction *>; | ||
|
||
} // namespace psr | ||
|
||
#endif // PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYMANAGERBASE_H |
342 changes: 342 additions & 0 deletions
342
include/phasar/DataFlow/PathSensitivity/PathSensitivityManagerMixin.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,342 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel and others | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYMANAGERMIXIN_H | ||
#define PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYMANAGERMIXIN_H | ||
|
||
#include "phasar/DataFlow/IfdsIde/SolverResults.h" | ||
#include "phasar/DataFlow/PathSensitivity/ExplodedSuperGraph.h" | ||
#include "phasar/DataFlow/PathSensitivity/PathSensitivityConfig.h" | ||
#include "phasar/DataFlow/PathSensitivity/PathSensitivityManagerBase.h" | ||
#include "phasar/DataFlow/PathSensitivity/PathTracingFilter.h" | ||
#include "phasar/PhasarLLVM/Utils/LLVMIRToSrc.h" | ||
#include "phasar/PhasarLLVM/Utils/LLVMShorthands.h" | ||
#include "phasar/Utils/DFAMinimizer.h" | ||
#include "phasar/Utils/GraphTraits.h" | ||
#include "phasar/Utils/Printer.h" | ||
|
||
#include "llvm/ADT/ArrayRef.h" | ||
#include "llvm/ADT/STLExtras.h" | ||
#include "llvm/ADT/SetVector.h" | ||
#include "llvm/ADT/SmallPtrSet.h" | ||
#include "llvm/ADT/SmallVector.h" | ||
#include "llvm/Support/raw_ostream.h" | ||
|
||
#include <cstdlib> | ||
#include <filesystem> | ||
#include <system_error> | ||
#include <type_traits> | ||
|
||
namespace llvm { | ||
class DbgInfoIntrinsic; | ||
} // namespace llvm | ||
|
||
namespace psr { | ||
template <typename Derived, typename AnalysisDomainTy, typename GraphType> | ||
class PathSensitivityManagerMixin { | ||
using n_t = typename AnalysisDomainTy::n_t; | ||
using d_t = typename AnalysisDomainTy::d_t; | ||
|
||
using NodeRef = typename ExplodedSuperGraph<AnalysisDomainTy>::NodeRef; | ||
using graph_type = GraphType; | ||
using graph_traits_t = GraphTraits<graph_type>; | ||
using vertex_t = typename graph_traits_t::vertex_t; | ||
|
||
struct PathsToContext { | ||
llvm::DenseMap<size_t, unsigned> Cache; | ||
llvm::SetVector<unsigned, llvm::SmallVector<unsigned, 0>> CurrPath; | ||
}; | ||
|
||
static const ExplodedSuperGraph<AnalysisDomainTy> & | ||
assertNotNull(const ExplodedSuperGraph<AnalysisDomainTy> *ESG) noexcept { | ||
assert(ESG != nullptr && "The exploded supergraph passed to the " | ||
"pathSensitivityManager must not be nullptr!"); | ||
return *ESG; | ||
} | ||
|
||
protected: | ||
PathSensitivityManagerMixin( | ||
const ExplodedSuperGraph<AnalysisDomainTy> *ESG) noexcept | ||
: ESG(assertNotNull(ESG)) { | ||
static_assert(std::is_base_of_v<PathSensitivityManagerBase<n_t>, Derived>, | ||
"Invalid CTRP instantiation: The Derived type must inherit " | ||
"from PathSensitivityManagerBase!"); | ||
} | ||
|
||
public: | ||
template < | ||
typename FactsRangeTy, typename ConfigTy, | ||
typename Filter = DefaultPathTracingFilter, | ||
typename = std::enable_if_t<is_pathtracingfilter_for_v<Filter, NodeRef>>> | ||
[[nodiscard]] GraphType | ||
pathsDagToAll(n_t Inst, FactsRangeTy FactsRange, | ||
const PathSensitivityConfigBase<ConfigTy> &Config, | ||
const Filter &PFilter = {}) const { | ||
graph_type Dag; | ||
PathsToContext Ctx; | ||
|
||
for (const d_t &Fact : FactsRange) { | ||
auto Nod = ESG.getNodeOrNull(Inst, std::move(Fact)); | ||
|
||
if (LLVM_UNLIKELY(!Nod)) { | ||
llvm::errs() << "Invalid Instruction-FlowFact pair. Only use those " | ||
"pairs that are part of the IDE analysis results!\n"; | ||
llvm::errs() << "Fatal error occurred. Writing ESG to temp file...\n"; | ||
llvm::errs().flush(); | ||
|
||
auto FileName = std::string(tmpnam(nullptr)) + "-explicitesg-err.dot"; | ||
|
||
{ | ||
std::error_code EC; | ||
llvm::raw_fd_ostream ROS(FileName, EC); | ||
ESG.printAsDot(ROS); | ||
} | ||
|
||
llvm::errs() << "> ESG written to " << FileName << '\n'; | ||
llvm::errs().flush(); | ||
|
||
abort(); | ||
} | ||
|
||
/// NOTE: We don't need to check that Nod has not been processed yet, | ||
/// because in the ESG construction we only merge nodes with the same flow | ||
/// fact. Here, the flow fact for each node differs (assuming FactsRage | ||
/// does not contain duplicates) | ||
|
||
auto Rt = pathsToImpl(Inst, Nod, Dag, Ctx, PFilter); | ||
if (Rt != GraphTraits<GraphType>::Invalid) { | ||
graph_traits_t::addRoot(Dag, Rt); | ||
} | ||
} | ||
|
||
#ifndef NDEBUG | ||
if (!static_cast<const Derived *>(this)->assertIsDAG(Dag)) { | ||
llvm::report_fatal_error("Invariant violated: DAG has a circle in it!"); | ||
} else { | ||
PHASAR_LOG_LEVEL_CAT(DEBUG, "PathSensitivityManager", | ||
"The DAG indeed has no circles"); | ||
} | ||
|
||
#endif | ||
|
||
if (Config.DAGDepthThreshold != SIZE_MAX) { | ||
Dag = Derived::reverseDAG(std::move(Dag), Config.DAGDepthThreshold); | ||
} else { | ||
Dag = reverseGraph(std::move(Dag)); | ||
} | ||
|
||
if (Config.MinimizeDAG) { | ||
|
||
auto Equiv = minimizeGraph(Dag); | ||
|
||
Dag = createEquivalentGraphFrom(std::move(Dag), Equiv); | ||
|
||
#ifndef NDEBUG | ||
if (!static_cast<const Derived *>(this)->assertIsDAG(Dag)) { | ||
llvm::report_fatal_error("Invariant violated: DAG has a circle in it!"); | ||
} else { | ||
PHASAR_LOG_LEVEL_CAT(DEBUG, "PathSensitivityManager", | ||
"The DAG indeed has no circles"); | ||
} | ||
#endif | ||
} | ||
|
||
return Dag; | ||
} | ||
|
||
template < | ||
typename ConfigTy, typename L, typename Filter = DefaultPathTracingFilter, | ||
typename = std::enable_if_t<is_pathtracingfilter_for_v<Filter, NodeRef>>> | ||
[[nodiscard]] GraphType | ||
pathsDagTo(n_t Inst, const SolverResults<n_t, d_t, L> &SR, | ||
const PathSensitivityConfigBase<ConfigTy> &Config, | ||
const Filter &PFilter = {}) const { | ||
auto Res = SR.resultsAt(Inst); | ||
auto FactsRange = llvm::make_first_range(Res); | ||
return pathsDagToAll(std::move(Inst), FactsRange, Config, PFilter); | ||
} | ||
|
||
template < | ||
typename ConfigTy, typename Filter = DefaultPathTracingFilter, | ||
typename = std::enable_if_t<is_pathtracingfilter_for_v<Filter, NodeRef>>> | ||
[[nodiscard]] GraphType | ||
pathsDagTo(n_t Inst, d_t Fact, | ||
const PathSensitivityConfigBase<ConfigTy> &Config, | ||
const Filter &PFilter = {}) const { | ||
|
||
return pathsDagToAll(std::move(Inst), llvm::ArrayRef(&Fact, 1), Config, | ||
PFilter); | ||
} | ||
|
||
template < | ||
typename ConfigTy, typename Filter = DefaultPathTracingFilter, | ||
typename = std::enable_if_t<is_pathtracingfilter_for_v<Filter, NodeRef>>> | ||
[[nodiscard]] GraphType | ||
pathsDagToInLLVMSSA(n_t Inst, d_t Fact, | ||
const PathSensitivityConfigBase<ConfigTy> &Config, | ||
const Filter &PFilter = {}) const { | ||
// Temporary code to bridge the time until merging f-IDESolverStrategy | ||
// into development | ||
if (Inst->getType()->isVoidTy()) { | ||
return pathsDagToAll(Inst, llvm::ArrayRef(&Fact, 1), Config, PFilter); | ||
} | ||
|
||
if (auto Next = Inst->getNextNonDebugInstruction()) { | ||
return pathsDagToAll(Next, llvm::ArrayRef(&Fact, 1), Config, PFilter); | ||
} | ||
|
||
PHASAR_LOG_LEVEL(WARNING, "[pathsDagToInLLVMSSA]: Cannot precisely " | ||
"determine the ESG node for inst-flowfact-pair (" | ||
<< NToString(Inst) << ", " << DToString(Fact) | ||
<< "). Fall-back to an approximation"); | ||
|
||
for (const auto *BB : llvm::successors(Inst)) { | ||
const auto *First = &BB->front(); | ||
if (llvm::isa<llvm::DbgInfoIntrinsic>(First)) { | ||
First = First->getNextNonDebugInstruction(); | ||
} | ||
if (ESG.getNodeOrNull(First, Fact)) { | ||
return pathsDagToAll(First, llvm::ArrayRef(&Fact, 1), Config, PFilter); | ||
} | ||
} | ||
|
||
llvm::report_fatal_error("Could not determine any ESG node corresponding " | ||
"to the inst-flowfact-pair (" + | ||
llvm::Twine(NToString(Inst)) + ", " + | ||
DToString(Fact) + ")"); | ||
|
||
return {}; | ||
} | ||
|
||
private: | ||
template <typename Filter> | ||
bool pathsToImplLAInvoke(vertex_t Ret, NodeRef Vtx, PathsToContext &Ctx, | ||
graph_type &RetDag, const Filter &PFilter) const { | ||
NodeRef Prev; | ||
bool IsEnd = false; | ||
bool IsError = false; | ||
|
||
do { | ||
Prev = Vtx; | ||
graph_traits_t::node(RetDag, Ret).push_back(Vtx.source()); | ||
|
||
Vtx = Vtx.predecessor(); | ||
|
||
if (PFilter.HasReachedEnd(Prev, Vtx)) { | ||
IsEnd = true; | ||
} else if (PFilter.IsErrorneousTransition(Prev, Vtx)) { | ||
IsError = true; | ||
} | ||
|
||
if (!Vtx) { | ||
return !IsError; | ||
} | ||
|
||
if (IsEnd || IsError) { | ||
break; | ||
} | ||
|
||
} while (!Vtx.hasNeighbors()); | ||
|
||
if (!Ctx.CurrPath.insert(Ret)) { | ||
PHASAR_LOG_LEVEL(ERROR, "Node " << Ret << " already on path"); | ||
return false; | ||
} | ||
scope_exit PopRet = [&Ctx] { Ctx.CurrPath.pop_back(); }; | ||
|
||
// NOLINTNEXTLINE(readability-identifier-naming) | ||
auto traverseNext = [&Ctx, this, Ret, &RetDag, &PFilter](NodeRef Nxt) { | ||
auto Succ = pathsToImplLA(Nxt, Ctx, RetDag, PFilter); | ||
if (Succ != graph_traits_t::Invalid && !Ctx.CurrPath.contains(Succ)) { | ||
graph_traits_t::addEdge(RetDag, Ret, Succ); | ||
} | ||
}; | ||
|
||
if (!IsEnd && !IsError) { | ||
traverseNext(Vtx); | ||
} | ||
|
||
for (auto Nxt : Vtx.neighbors()) { | ||
assert(Nxt != nullptr); | ||
if (PFilter.IsErrorneousTransition(Prev, Nxt)) { | ||
continue; | ||
} | ||
if (PFilter.HasReachedEnd(Prev, Nxt)) { | ||
IsEnd = true; | ||
continue; | ||
} | ||
traverseNext(Nxt); | ||
} | ||
|
||
graph_traits_t::dedupOutEdges(RetDag, Ret); | ||
|
||
return IsEnd || graph_traits_t::outDegree(RetDag, Ret) != 0; | ||
} | ||
|
||
template <typename Filter> | ||
vertex_t pathsToImplLA(NodeRef Vtx, PathsToContext &Ctx, graph_type &RetDag, | ||
const Filter &PFilter) const { | ||
/// Idea: Treat the graph as firstChild-nextSibling notation and always | ||
/// traverse with one predecessor lookAhead | ||
|
||
auto [It, Inserted] = | ||
Ctx.Cache.try_emplace(Vtx.id(), graph_traits_t::Invalid); | ||
if (!Inserted) { | ||
return It->second; | ||
} | ||
|
||
auto Ret = | ||
graph_traits_t::addNode(RetDag, typename graph_traits_t::value_type()); | ||
// auto Ret = RetDag.addNode(); | ||
It->second = Ret; | ||
|
||
if (!pathsToImplLAInvoke(Ret, Vtx, Ctx, RetDag, PFilter)) { | ||
/// NOTE: Don't erase Vtx from Cache to guarantee termination | ||
// NOLINTNEXTLINE(cppcoreguidelines-pro-bounds-pointer-arithmetic) -- fp | ||
Ctx.Cache[Vtx.id()] = graph_traits_t::Invalid; | ||
|
||
if (Ctx.CurrPath.contains(Ret) || !graph_traits_t::pop(RetDag, Ret)) { | ||
PHASAR_LOG_LEVEL(WARNING, "Cannot remove invalid path at: " << Ret); | ||
graph_traits_t::node(RetDag, Ret).clear(); | ||
} | ||
|
||
return graph_traits_t::Invalid; | ||
} | ||
return Ret; | ||
} | ||
|
||
template <typename Filter> | ||
vertex_t pathsToImpl(n_t QueryInst, NodeRef Vtx, graph_type &RetDag, | ||
PathsToContext &Ctx, const Filter &PFilter) const { | ||
|
||
auto Ret = | ||
graph_traits_t::addNode(RetDag, typename graph_traits_t::value_type()); | ||
graph_traits_t::node(RetDag, Ret).push_back(QueryInst); | ||
|
||
for (auto NB : Vtx.neighbors()) { | ||
auto NBNode = pathsToImplLA(NB, Ctx, RetDag, PFilter); | ||
if (NBNode != graph_traits_t::Invalid) { | ||
graph_traits_t::addEdge(RetDag, Ret, NBNode); | ||
} | ||
} | ||
auto VtxNode = pathsToImplLA(Vtx, Ctx, RetDag, PFilter); | ||
if (VtxNode != graph_traits_t::Invalid) { | ||
graph_traits_t::addEdge(RetDag, Ret, VtxNode); | ||
} | ||
|
||
graph_traits_t::dedupOutEdges(RetDag, Ret); | ||
|
||
return Ret; | ||
} | ||
|
||
const ExplodedSuperGraph<AnalysisDomainTy> &ESG; | ||
}; | ||
} // namespace psr | ||
|
||
#endif // PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYMANAGERMIXIN_H |
51 changes: 51 additions & 0 deletions
51
include/phasar/DataFlow/PathSensitivity/PathTracingFilter.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,51 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel and others | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_DATAFLOW_PATHSENSITIVITY_PATHTRACINGFILTER_H | ||
#define PHASAR_DATAFLOW_PATHSENSITIVITY_PATHTRACINGFILTER_H | ||
|
||
#include <type_traits> | ||
|
||
namespace psr { | ||
template <typename EndFilter, typename ErrFilter> struct PathTracingFilter { | ||
using end_filter_t = EndFilter; | ||
using err_filter_t = ErrFilter; | ||
|
||
[[no_unique_address]] end_filter_t HasReachedEnd; | ||
[[no_unique_address]] err_filter_t IsErrorneousTransition; | ||
}; | ||
|
||
namespace detail { | ||
struct False2 { | ||
template <typename T, typename U> | ||
constexpr bool operator()(T && /*First*/, U && /*Second*/) const noexcept { | ||
return false; | ||
} | ||
}; | ||
} // namespace detail | ||
|
||
using DefaultPathTracingFilter = | ||
PathTracingFilter<detail::False2, detail::False2>; | ||
|
||
template <typename F, typename NodeRef, typename = void> | ||
struct is_pathtracingfilter_for : std::false_type {}; | ||
|
||
template <typename EndFilter, typename ErrFilter, typename NodeRef> | ||
struct is_pathtracingfilter_for< | ||
PathTracingFilter<EndFilter, ErrFilter>, NodeRef, | ||
std::enable_if_t<std::is_invocable_r_v<bool, EndFilter, NodeRef, NodeRef> && | ||
std::is_invocable_r_v<bool, ErrFilter, NodeRef, NodeRef>>> | ||
: std::true_type {}; | ||
|
||
template <typename F, typename NodeRef> | ||
constexpr static bool is_pathtracingfilter_for_v = | ||
is_pathtracingfilter_for<F, NodeRef>::value; | ||
} // namespace psr | ||
|
||
#endif // PHASAR_DATAFLOW_PATHSENSITIVITY_PATHTRACINGFILTER_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
97 changes: 97 additions & 0 deletions
97
include/phasar/PhasarLLVM/DataFlow/PathSensitivity/LLVMPathConstraints.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,97 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel and others | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_PHASARLLVM_PATHSENSITIVITY_LLVMPATHCONSTRAINTS_H | ||
#define PHASAR_PHASARLLVM_PATHSENSITIVITY_LLVMPATHCONSTRAINTS_H | ||
|
||
#include "phasar/Utils/MaybeUniquePtr.h" | ||
|
||
#include "llvm/ADT/SmallVector.h" | ||
|
||
#include "z3++.h" | ||
|
||
#include <optional> | ||
|
||
namespace llvm { | ||
class Value; | ||
class Instruction; | ||
class AllocaInst; | ||
class LoadInst; | ||
class GetElementPtrInst; | ||
class PHINode; | ||
class BranchInst; | ||
class CmpInst; | ||
class BinaryOperator; | ||
class CallBase; | ||
} // namespace llvm | ||
|
||
namespace psr { | ||
class LLVMPathConstraints { | ||
public: | ||
struct ConstraintAndVariables { | ||
z3::expr Constraint; | ||
llvm::SmallVector<const llvm::Value *, 4> Variables; | ||
}; | ||
|
||
explicit LLVMPathConstraints(z3::context *Z3Ctx = nullptr, | ||
bool IgnoreDebugInstructions = true); | ||
|
||
z3::context &getContext() noexcept { return *Z3Ctx; } | ||
const z3::context &getContext() const noexcept { return *Z3Ctx; } | ||
|
||
std::optional<z3::expr> getConstraintFromEdge(const llvm::Instruction *Curr, | ||
const llvm::Instruction *Succ); | ||
|
||
std::optional<ConstraintAndVariables> | ||
getConstraintAndVariablesFromEdge(const llvm::Instruction *Curr, | ||
const llvm::Instruction *Succ); | ||
|
||
private: | ||
[[nodiscard]] std::optional<ConstraintAndVariables> | ||
internalGetConstraintAndVariablesFromEdge(const llvm::Instruction *From, | ||
const llvm::Instruction *To); | ||
|
||
/// Allocas are the most basic building blocks and represent a leaf value. | ||
[[nodiscard]] ConstraintAndVariables | ||
getAllocaInstAsZ3(const llvm::AllocaInst *Alloca); | ||
|
||
/// Load instrutions may also represent leafs. | ||
[[nodiscard]] ConstraintAndVariables | ||
getLoadInstAsZ3(const llvm::LoadInst *Load); | ||
|
||
/// GEP instructions may also represent leafs. | ||
[[nodiscard]] ConstraintAndVariables | ||
getGEPInstAsZ3(const llvm::GetElementPtrInst *GEP); | ||
|
||
[[nodiscard]] ConstraintAndVariables | ||
handlePhiInstruction(const llvm::PHINode *Phi); | ||
|
||
[[nodiscard]] ConstraintAndVariables | ||
handleCondBrInst(const llvm::BranchInst *Br, const llvm::Instruction *Succ); | ||
|
||
[[nodiscard]] ConstraintAndVariables handleCmpInst(const llvm::CmpInst *Cmp); | ||
|
||
[[nodiscard]] ConstraintAndVariables | ||
handleBinaryOperator(const llvm::BinaryOperator *BinOp); | ||
|
||
[[nodiscard]] ConstraintAndVariables getLiteralAsZ3(const llvm::Value *V); | ||
|
||
[[nodiscard]] ConstraintAndVariables | ||
getFunctionCallAsZ3(const llvm::CallBase *CallSite); | ||
|
||
friend class SizeGuardCheck; | ||
friend class LoopGuardCheck; | ||
|
||
MaybeUniquePtr<z3::context> Z3Ctx; | ||
std::unordered_map<const llvm::Value *, ConstraintAndVariables> Z3Expr; | ||
bool IgnoreDebugInstructions; | ||
}; | ||
} // namespace psr | ||
|
||
#endif // PHASAR_PHASARLLVM_PATHSENSITIVITY_LLVMPATHCONSTRAINTS_H |
41 changes: 41 additions & 0 deletions
41
include/phasar/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitivityConfig.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,41 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel and others | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_PHASARLLVM_PATHSENSITIVITY_Z3BASEDPATHSENSITIVITYCONFIG_H | ||
#define PHASAR_PHASARLLVM_PATHSENSITIVITY_Z3BASEDPATHSENSITIVITYCONFIG_H | ||
|
||
#include "phasar/DataFlow/PathSensitivity/PathSensitivityConfig.h" | ||
|
||
#include "z3++.h" | ||
|
||
#include <optional> | ||
|
||
namespace psr { | ||
struct Z3BasedPathSensitivityConfig | ||
: PathSensitivityConfigBase<Z3BasedPathSensitivityConfig> { | ||
std::optional<z3::expr> AdditionalConstraint; | ||
|
||
[[nodiscard]] Z3BasedPathSensitivityConfig | ||
withAdditionalConstraint(const z3::expr &Constr) const &noexcept { | ||
auto Ret = *this; | ||
Ret.AdditionalConstraint = | ||
Ret.AdditionalConstraint ? *Ret.AdditionalConstraint && Constr : Constr; | ||
return Ret; | ||
} | ||
|
||
[[nodiscard]] Z3BasedPathSensitivityConfig | ||
withAdditionalConstraint(const z3::expr &Constr) &&noexcept { | ||
AdditionalConstraint = | ||
AdditionalConstraint ? *AdditionalConstraint && Constr : Constr; | ||
return std::move(*this); | ||
} | ||
}; | ||
} // namespace psr | ||
|
||
#endif // PHASAR_PHASARLLVM_PATHSENSITIVITY_Z3BASEDPATHSENSITIVITYCONFIG_H |
186 changes: 186 additions & 0 deletions
186
include/phasar/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitvityManager.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,186 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel and others | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_PHASARLLVM_PATHSENSITIVITY_Z3BASEDPATHSENSITIVITYMANAGER_H | ||
#define PHASAR_PHASARLLVM_PATHSENSITIVITY_Z3BASEDPATHSENSITIVITYMANAGER_H | ||
|
||
#include "phasar/DataFlow/PathSensitivity/FlowPath.h" | ||
#include "phasar/DataFlow/PathSensitivity/PathSensitivityManagerBase.h" | ||
#include "phasar/DataFlow/PathSensitivity/PathSensitivityManagerMixin.h" | ||
#include "phasar/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitivityConfig.h" | ||
#include "phasar/PhasarLLVM/Utils/LLVMIRToSrc.h" | ||
#include "phasar/PhasarLLVM/Utils/LLVMShorthands.h" | ||
#include "phasar/Utils/GraphTraits.h" | ||
#include "phasar/Utils/Logger.h" | ||
#include "phasar/Utils/MaybeUniquePtr.h" | ||
|
||
#include "llvm/ADT/ArrayRef.h" | ||
#include "llvm/ADT/STLExtras.h" | ||
#include "llvm/Support/ErrorHandling.h" | ||
#include "llvm/Support/raw_ostream.h" | ||
|
||
#include "z3++.h" | ||
|
||
#include <cstdint> | ||
#include <filesystem> | ||
#include <memory> | ||
#include <system_error> | ||
#include <type_traits> | ||
|
||
namespace llvm { | ||
class Instruction; | ||
} // namespace llvm | ||
|
||
namespace psr { | ||
class LLVMPathConstraints; | ||
|
||
class Z3BasedPathSensitivityManagerBase | ||
: public PathSensitivityManagerBase<const llvm::Instruction *> { | ||
public: | ||
using n_t = const llvm::Instruction *; | ||
|
||
static_assert(is_removable_graph_trait_v<graph_traits_t>, | ||
"Invalid graph type: Must support edge-removal!"); | ||
|
||
protected: | ||
z3::expr filterOutUnreachableNodes(graph_type &RevDAG, vertex_t Leaf, | ||
const Z3BasedPathSensitivityConfig &Config, | ||
LLVMPathConstraints &LPC) const; | ||
|
||
FlowPathSequence<n_t> | ||
filterAndFlattenRevDag(graph_type &RevDAG, vertex_t Leaf, n_t FinalInst, | ||
const Z3BasedPathSensitivityConfig &Config, | ||
LLVMPathConstraints &LPC) const; | ||
|
||
static void deduplicatePaths(FlowPathSequence<n_t> &Paths); | ||
}; | ||
|
||
template <typename AnalysisDomainTy, | ||
typename = std::enable_if_t<std::is_same_v< | ||
typename AnalysisDomainTy::n_t, const llvm::Instruction *>>> | ||
class Z3BasedPathSensitivityManager | ||
: public Z3BasedPathSensitivityManagerBase, | ||
public PathSensitivityManagerMixin< | ||
Z3BasedPathSensitivityManager<AnalysisDomainTy>, AnalysisDomainTy, | ||
typename Z3BasedPathSensitivityManagerBase::graph_type> { | ||
using base_t = PathSensitivityManagerBase<typename AnalysisDomainTy::n_t>; | ||
using mixin_t = PathSensitivityManagerMixin<Z3BasedPathSensitivityManager, | ||
AnalysisDomainTy, | ||
typename base_t::graph_type>; | ||
|
||
public: | ||
using n_t = typename AnalysisDomainTy::n_t; | ||
using d_t = typename AnalysisDomainTy::d_t; | ||
using typename PathSensitivityManagerBase<n_t>::graph_type; | ||
using MaybeFlowPathSeq = std::variant<FlowPathSequence<n_t>, z3::expr>; | ||
|
||
explicit Z3BasedPathSensitivityManager( | ||
const ExplodedSuperGraph<AnalysisDomainTy> *ESG, | ||
Z3BasedPathSensitivityConfig Config, LLVMPathConstraints *LPC = nullptr) | ||
: mixin_t(ESG), Config(std::move(Config)), LPC(LPC) { | ||
if (!LPC) { | ||
this->LPC = std::make_unique<LLVMPathConstraints>(); | ||
} | ||
} | ||
|
||
FlowPathSequence<n_t> pathsTo(n_t Inst, d_t Fact) const { | ||
if (Config.DAGSizeThreshold != SIZE_MAX) { | ||
PHASAR_LOG_LEVEL( | ||
WARNING, | ||
"Attempting to compute FlowPaths without conditionally " | ||
"falling back to constraint collection, but a DAGSizeThreshold " | ||
"is specified. It will be ignored here. To make use of it, " | ||
"please call the pathsOrConstraintTo function instead!"); | ||
} | ||
|
||
graph_type Dag = this->pathsDagTo(Inst, std::move(Fact), Config); | ||
|
||
PHASAR_LOG_LEVEL_CAT( | ||
DEBUG, "PathSensitivityManager", | ||
"PathsTo with MaxDAGDepth: " << Config.DAGDepthThreshold); | ||
|
||
#ifndef NDEBUG | ||
{ | ||
std::error_code EC; | ||
llvm::raw_fd_stream ROS( | ||
"dag-" + | ||
std::filesystem::path(psr::getFilePathFromIR(Inst)) | ||
.filename() | ||
.string() + | ||
"-" + psr::getMetaDataID(Inst) + ".dot", | ||
EC); | ||
assert(!EC); | ||
printGraph(Dag, ROS, "DAG", [](llvm::ArrayRef<n_t> PartialPath) { | ||
std::string Buf; | ||
llvm::raw_string_ostream ROS(Buf); | ||
ROS << "[ "; | ||
llvm::interleaveComma(PartialPath, ROS, [&ROS](const auto *Inst) { | ||
ROS << psr::getMetaDataID(Inst); | ||
}); | ||
ROS << " ]"; | ||
ROS.flush(); | ||
return Buf; | ||
}); | ||
|
||
llvm::errs() << "Paths DAG has " << Dag.Roots.size() << " roots\n"; | ||
} | ||
#endif | ||
|
||
vertex_t Leaf = [&Dag] { | ||
for (auto Vtx : graph_traits_t::vertices(Dag)) { | ||
if (graph_traits_t::outDegree(Dag, Vtx) == 0) { | ||
return Vtx; | ||
} | ||
} | ||
llvm_unreachable("Expect the DAG to have a leaf node!"); | ||
}(); | ||
|
||
z3::expr Constraint = filterOutUnreachableNodes(Dag, Leaf, Config, *LPC); | ||
|
||
if (Constraint.is_false()) { | ||
PHASAR_LOG_LEVEL_CAT(INFO, "PathSensitivityManager", | ||
"The query position is unreachable"); | ||
return FlowPathSequence<n_t>(); | ||
} | ||
|
||
auto Ret = filterAndFlattenRevDag(Dag, Leaf, Inst, Config, *LPC); | ||
|
||
deduplicatePaths(Ret); | ||
|
||
#ifndef NDEBUG | ||
#ifdef DYNAMIC_LOG | ||
PHASAR_LOG_LEVEL_CAT(DEBUG, "PathSensitivityManager", | ||
"Recorded " << Ret.size() << " valid paths:"); | ||
|
||
std::string Str; | ||
for (const FlowPath<n_t> &Path : Ret) { | ||
Str.clear(); | ||
llvm::raw_string_ostream ROS(Str); | ||
ROS << "> "; | ||
llvm::interleaveComma(Path.Path, ROS, | ||
[&ROS](auto *Inst) { ROS << getMetaDataID(Inst); }); | ||
ROS << ": " << Path.Constraint.to_string(); | ||
ROS.flush(); | ||
PHASAR_LOG_LEVEL_CAT(DEBUG, "PathSensitivityManager", Str); | ||
} | ||
|
||
#endif // DYNAMIC_LOG | ||
#endif // NDEBUG | ||
|
||
return Ret; | ||
} | ||
|
||
private: | ||
Z3BasedPathSensitivityConfig Config{}; | ||
/// FIXME: Not using 'mutable' here | ||
mutable MaybeUniquePtr<LLVMPathConstraints, true> LPC{}; | ||
}; | ||
} // namespace psr | ||
|
||
#endif // PHASAR_PHASARLLVM_PATHSENSITIVITY_Z3BASEDPATHSENSITIVITYMANAGER_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,44 @@ | ||
#ifndef PHASAR_PHASARLLVM_UTILS_ANALYSISPRINTERBASE_H | ||
#define PHASAR_PHASARLLVM_UTILS_ANALYSISPRINTERBASE_H | ||
|
||
#include "llvm/Support/raw_ostream.h" | ||
|
||
namespace psr { | ||
|
||
template <typename AnalysisDomainTy> struct Warning { | ||
using n_t = typename AnalysisDomainTy::n_t; | ||
using d_t = typename AnalysisDomainTy::d_t; | ||
using l_t = typename AnalysisDomainTy::l_t; | ||
|
||
n_t Instr; | ||
d_t Fact; | ||
l_t LatticeElement; | ||
|
||
// Constructor | ||
Warning(n_t Inst, d_t DfFact, l_t Lattice) | ||
: Instr(std::move(Inst)), Fact(std::move(DfFact)), | ||
LatticeElement(std::move(Lattice)) {} | ||
}; | ||
|
||
template <typename AnalysisDomainTy> struct DataflowAnalysisResults { | ||
std::vector<Warning<AnalysisDomainTy>> War; | ||
}; | ||
|
||
template <typename AnalysisDomainTy> class AnalysisPrinterBase { | ||
public: | ||
virtual void onResult(Warning<AnalysisDomainTy> /*War*/) = 0; | ||
virtual void onInitialize() = 0; | ||
virtual void onFinalize(llvm::raw_ostream & /*OS*/) const = 0; | ||
|
||
AnalysisPrinterBase() = default; | ||
virtual ~AnalysisPrinterBase() = default; | ||
AnalysisPrinterBase(const AnalysisPrinterBase &) = delete; | ||
AnalysisPrinterBase &operator=(const AnalysisPrinterBase &) = delete; | ||
|
||
AnalysisPrinterBase(AnalysisPrinterBase &&) = delete; | ||
AnalysisPrinterBase &operator=(AnalysisPrinterBase &&) = delete; | ||
}; | ||
|
||
} // namespace psr | ||
|
||
#endif |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
#ifndef PHASAR_PHASARLLVM_UTILS_DEFAULTANALYSISPRINTER_H | ||
#define PHASAR_PHASARLLVM_UTILS_DEFAULTANALYSISPRINTER_H | ||
|
||
#include "phasar/Domain/BinaryDomain.h" | ||
#include "phasar/PhasarLLVM/Utils/AnalysisPrinterBase.h" | ||
#include "phasar/PhasarLLVM/Utils/LLVMShorthands.h" | ||
#include "phasar/Utils/Printer.h" | ||
|
||
#include <optional> | ||
#include <type_traits> | ||
#include <vector> | ||
|
||
namespace psr { | ||
|
||
template <typename AnalysisDomainTy> | ||
class DefaultAnalysisPrinter : public AnalysisPrinterBase<AnalysisDomainTy> { | ||
using l_t = typename AnalysisDomainTy::l_t; | ||
|
||
public: | ||
~DefaultAnalysisPrinter() override = default; | ||
DefaultAnalysisPrinter() = default; | ||
|
||
void onResult(Warning<AnalysisDomainTy> War) override { | ||
AnalysisResults.War.emplace_back(std::move(War)); | ||
} | ||
|
||
void onInitialize() override{}; | ||
void onFinalize(llvm::raw_ostream &OS = llvm::outs()) const override { | ||
for (const auto &Iter : AnalysisResults.War) { | ||
|
||
OS << "\nAt IR statement: " << NToString(Iter.Instr) << "\n"; | ||
|
||
OS << "\tFact: " << DToString(Iter.Fact) << "\n"; | ||
|
||
if constexpr (std::is_same_v<l_t, BinaryDomain>) { | ||
OS << "Value: " << LToString(Iter.LatticeElement) << "\n"; | ||
} | ||
} | ||
} | ||
|
||
private: | ||
DataflowAnalysisResults<AnalysisDomainTy> AnalysisResults{}; | ||
}; | ||
|
||
} // namespace psr | ||
|
||
#endif |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,25 @@ | ||
#ifndef PHASAR_PHASARLLVM_UTILS_NULLANALYSISPRINTER_H | ||
#define PHASAR_PHASARLLVM_UTILS_NULLANALYSISPRINTER_H | ||
|
||
#include "phasar/PhasarLLVM/Utils/AnalysisPrinterBase.h" | ||
|
||
namespace psr { | ||
|
||
template <typename AnalysisDomainTy> | ||
class NullAnalysisPrinter final : public AnalysisPrinterBase<AnalysisDomainTy> { | ||
public: | ||
static NullAnalysisPrinter *getInstance() { | ||
static auto Instance = NullAnalysisPrinter(); | ||
return &Instance; | ||
} | ||
|
||
void onInitialize() override{}; | ||
void onResult(Warning<AnalysisDomainTy> /*War*/) override{}; | ||
void onFinalize(llvm::raw_ostream & /*OS*/) const override{}; | ||
|
||
private: | ||
NullAnalysisPrinter() = default; | ||
}; | ||
|
||
} // namespace psr | ||
#endif |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,301 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_UTILS_ADJACENCYLIST_H | ||
#define PHASAR_UTILS_ADJACENCYLIST_H | ||
|
||
#include "phasar/Utils/GraphTraits.h" | ||
#include "phasar/Utils/IotaIterator.h" | ||
#include "phasar/Utils/RepeatIterator.h" | ||
#include "phasar/Utils/Utilities.h" | ||
|
||
#include "llvm/ADT/ArrayRef.h" | ||
#include "llvm/ADT/None.h" | ||
#include "llvm/ADT/SmallVector.h" | ||
|
||
#include <iterator> | ||
#include <limits> | ||
#include <type_traits> | ||
|
||
namespace psr { | ||
|
||
template <typename T, typename EdgeTy = unsigned> struct AdjacencyList { | ||
llvm::SmallVector<T, 0> Nodes{}; | ||
llvm::SmallVector<llvm::SmallVector<EdgeTy, 2>, 0> Adj{}; | ||
llvm::SmallVector<unsigned, 1> Roots{}; | ||
}; | ||
|
||
template <typename EdgeTy> struct AdjacencyList<llvm::NoneType, EdgeTy> { | ||
llvm::SmallVector<llvm::SmallVector<EdgeTy, 2>, 0> Adj{}; | ||
llvm::SmallVector<unsigned, 1> Roots{}; | ||
}; | ||
|
||
/// A simple graph implementation based on an adjacency list | ||
template <typename T, typename EdgeTy> | ||
struct GraphTraits<AdjacencyList<T, EdgeTy>> { | ||
using graph_type = AdjacencyList<T, EdgeTy>; | ||
using value_type = T; | ||
using vertex_t = unsigned; | ||
using edge_t = EdgeTy; | ||
using edge_iterator = typename llvm::ArrayRef<edge_t>::const_iterator; | ||
using roots_iterator = typename llvm::ArrayRef<vertex_t>::const_iterator; | ||
|
||
/// A vertex that is not inserted into any graph. Can be used to communicate | ||
/// failure of certain operations | ||
static inline constexpr auto Invalid = std::numeric_limits<vertex_t>::max(); | ||
|
||
/// Adds a new node to the graph G with node-tag Val | ||
/// | ||
/// \returns The vertex-descriptor for the newly created node | ||
template <typename TT, | ||
typename = std::enable_if_t<!std::is_same_v<TT, llvm::NoneType>>> | ||
static vertex_t addNode(graph_type &G, TT &&Val) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
|
||
auto Ret = G.Nodes.size(); | ||
G.Nodes.push_back(std::forward<TT>(Val)); | ||
G.Adj.emplace_back(); | ||
return Ret; | ||
} | ||
|
||
/// Adds a new node to the graph G without node-tag | ||
/// | ||
/// \returns The vertex-descriptor for the newly created node | ||
template <typename TT = value_type, | ||
typename = std::enable_if_t<std::is_same_v<TT, llvm::NoneType>>> | ||
static vertex_t addNode(graph_type &G, llvm::NoneType /*Val*/ = llvm::None) { | ||
auto Ret = G.Adj.size(); | ||
G.Adj.emplace_back(); | ||
return Ret; | ||
} | ||
|
||
/// Makes the node Vtx as root in the graph G. A node should not be registered | ||
/// as root multiple times | ||
static void addRoot(graph_type &G, vertex_t Vtx) { | ||
assert(Vtx < G.Adj.size()); | ||
if constexpr (!std::is_same_v<value_type, llvm::NoneType>) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
} | ||
G.Roots.push_back(Vtx); | ||
} | ||
|
||
/// Gets a range of all root nodes of graph G | ||
static llvm::ArrayRef<vertex_t> roots(const graph_type &G) noexcept { | ||
if constexpr (!std::is_same_v<value_type, llvm::NoneType>) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
} | ||
return G.Roots; | ||
} | ||
|
||
/// Adds a new edge from node From to node To in graph G. From and To should | ||
/// be nodes inside G. Multi-edges are supported, i.e. edges are not | ||
/// deduplicated automatically; to manually deduplicate the edges of one | ||
/// source-node, call dedupOutEdges() | ||
static void addEdge(graph_type &G, vertex_t From, edge_t To) { | ||
assert(From < G.Adj.size()); | ||
if constexpr (!std::is_same_v<value_type, llvm::NoneType>) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
} | ||
G.Adj[From].push_back(std::move(To)); | ||
} | ||
|
||
/// Gets a range of all edges outgoing from node Vtx in graph G | ||
static llvm::ArrayRef<edge_t> outEdges(const graph_type &G, | ||
vertex_t Vtx) noexcept { | ||
assert(Vtx < G.Adj.size()); | ||
if constexpr (!std::is_same_v<value_type, llvm::NoneType>) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
} | ||
return G.Adj[Vtx]; | ||
} | ||
|
||
/// Gets the number of edges outgoing from node Vtx in graph G | ||
static size_t outDegree(const graph_type &G, vertex_t Vtx) noexcept { | ||
assert(Vtx < G.Adj.size()); | ||
if constexpr (!std::is_same_v<value_type, llvm::NoneType>) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
} | ||
return G.Adj[Vtx].size(); | ||
} | ||
|
||
/// Deduplicates the edges outgoing from node Vtx in graph G. Deduplication is | ||
/// based on operator< and operator== of the edge_t type | ||
static void dedupOutEdges(graph_type &G, vertex_t Vtx) noexcept { | ||
assert(Vtx < G.Adj.size()); | ||
if constexpr (!std::is_same_v<value_type, llvm::NoneType>) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
} | ||
auto &OutEdges = G.Adj[Vtx]; | ||
std::sort(OutEdges.begin(), OutEdges.end()); | ||
OutEdges.erase(std::unique(OutEdges.begin(), OutEdges.end()), | ||
OutEdges.end()); | ||
} | ||
|
||
/// Gets a const range of all nodes in graph G | ||
template <typename TT = value_type, | ||
typename = std::enable_if_t<!std::is_same_v<TT, llvm::NoneType>>> | ||
static llvm::ArrayRef<value_type> nodes(const graph_type &G) noexcept { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
return G.Nodes; | ||
} | ||
/// Gets a mutable range of all nodes in graph G | ||
template <typename TT = value_type, | ||
typename = std::enable_if_t<!std::is_same_v<TT, llvm::NoneType>>> | ||
static llvm::MutableArrayRef<value_type> nodes(graph_type &G) noexcept { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
return G.Nodes; | ||
} | ||
/// Gets a range of all nodes in graph G | ||
template <typename TT = value_type, | ||
typename = std::enable_if_t<std::is_same_v<TT, llvm::NoneType>>> | ||
static RepeatRangeType<value_type> nodes(const graph_type &G) noexcept { | ||
return repeat(llvm::None, G.Adj.size()); | ||
} | ||
|
||
/// Gets a range of vertex-descriptors for all nodes in graph G | ||
static auto vertices(const graph_type &G) noexcept { | ||
if constexpr (!std::is_same_v<value_type, llvm::NoneType>) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
} | ||
return psr::iota(size_t(0), G.Adj.size()); | ||
} | ||
|
||
/// Gets the node-tag for node Vtx in graph G. Vtx must be part of G | ||
template <typename TT = value_type, | ||
typename = std::enable_if_t<!std::is_same_v<TT, llvm::NoneType>>> | ||
static const value_type &node(const graph_type &G, vertex_t Vtx) noexcept { | ||
assert(Vtx < G.Nodes.size()); | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
return G.Nodes[Vtx]; | ||
} | ||
/// Gets the node-tag for node Vtx in graph G. Vtx must be part of G | ||
template <typename TT = value_type, | ||
typename = std::enable_if_t<!std::is_same_v<TT, llvm::NoneType>>> | ||
static value_type &node(graph_type &G, vertex_t Vtx) noexcept { | ||
assert(Vtx < G.Nodes.size()); | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
return G.Nodes[Vtx]; | ||
} | ||
|
||
/// Gets the node-tag for node Vtx in graph G. Vtx must be part of G | ||
template <typename TT = value_type, | ||
typename = std::enable_if_t<std::is_same_v<TT, llvm::NoneType>>> | ||
static llvm::NoneType node([[maybe_unused]] const graph_type &G, | ||
[[maybe_unused]] vertex_t Vtx) noexcept { | ||
assert(Vtx < G.Adj.size()); | ||
return llvm::None; | ||
} | ||
|
||
/// Gets the number of nodes in graph G | ||
static size_t size(const graph_type &G) noexcept { | ||
if constexpr (!std::is_same_v<value_type, llvm::NoneType>) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
} | ||
return G.Adj.size(); | ||
} | ||
|
||
/// Gets the number of nodes in graph G that are marked as root | ||
static size_t roots_size(const graph_type &G) noexcept { // NOLINT | ||
if constexpr (!std::is_same_v<value_type, llvm::NoneType>) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
} | ||
return G.Roots.size(); | ||
} | ||
|
||
/// Pre-allocates space to hold up to Capacity nodes | ||
static void reserve(graph_type &G, size_t Capacity) { | ||
if constexpr (!std::is_same_v<value_type, llvm::NoneType>) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
G.Nodes.reserve(Capacity); | ||
} | ||
|
||
G.Adj.reserve(Capacity); | ||
} | ||
|
||
/// Tries to remove the last inserted node Vtx fro graph G. Fails, if there | ||
/// was another not-popped node inserted in between. | ||
/// | ||
/// \returns True, iff the removal was successful | ||
static bool pop(graph_type &G, vertex_t Vtx) { | ||
if (Vtx == G.Adj.size() - 1) { | ||
G.Adj.pop_back(); | ||
if constexpr (!std::is_same_v<llvm::NoneType, value_type>) { | ||
G.Nodes.pop_back(); | ||
} | ||
return true; | ||
} | ||
return false; | ||
} | ||
|
||
/// Gets the vertex-descriptor of the target-node of the given Edge | ||
template <typename E = edge_t> | ||
static std::enable_if_t<std::is_same_v<E, vertex_t>, vertex_t> | ||
target(edge_t Edge) noexcept { | ||
return Edge; | ||
} | ||
|
||
/// Copies the given edge, but replaces the target node by Tar; i.e. the | ||
/// weight of the returned edge and the parameter edge is same, but the target | ||
/// nodes may differ. | ||
template <typename E = edge_t> | ||
static std::enable_if_t<std::is_same_v<E, vertex_t>, edge_t> | ||
withEdgeTarget(edge_t /*edge*/, vertex_t Tar) noexcept { | ||
return Tar; | ||
} | ||
|
||
/// Gets the weight associated with the given edge | ||
static llvm::NoneType weight(edge_t /*unused*/) noexcept { | ||
return llvm::None; | ||
} | ||
|
||
/// Removes the edge denoted by It outgoing from source-vertex Vtx from the | ||
/// graph G. This function is not required by the is_graph_trait concept. | ||
/// | ||
/// \returns An edge_iterator directly following It that should be used to | ||
/// continue iteration instead of std::next(It) | ||
static edge_iterator removeEdge(graph_type &G, vertex_t Vtx, | ||
edge_iterator It) noexcept { | ||
assert(Vtx < G.Adj.size()); | ||
if constexpr (!std::is_same_v<value_type, llvm::NoneType>) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
} | ||
assert(G.Adj[Vtx].begin() <= It && It < G.Adj[Vtx].end()); | ||
auto Idx = std::distance(std::cbegin(G.Adj[Vtx]), It); | ||
|
||
std::swap(G.Adj[Vtx][Idx], G.Adj[Vtx].back()); | ||
G.Adj[Vtx].pop_back(); | ||
return It; | ||
} | ||
|
||
/// Removes the root denoted by It from the graph G. This function is not | ||
/// required by the is_graph_trait concept. | ||
/// | ||
/// \returns A roots_iterator directly following It that should be used to | ||
/// continue iteration instead of std::next(It) | ||
static roots_iterator removeRoot(graph_type &G, roots_iterator It) noexcept { | ||
if constexpr (!std::is_same_v<value_type, llvm::NoneType>) { | ||
assert(G.Adj.size() == G.Nodes.size()); | ||
} | ||
assert(G.Roots.begin() <= It && It < G.Roots.end()); | ||
|
||
auto Idx = std::distance(std::cbegin(G.Roots), It); | ||
std::swap(G.Roots[Idx], G.Roots.back()); | ||
G.Roots.pop_back(); | ||
return It; | ||
} | ||
|
||
#if __cplusplus >= 202002L | ||
static_assert(is_graph<AdjacencyList<T>>); | ||
static_assert(is_reservable_graph_trait<GraphTraits<AdjacencyList<T>>>); | ||
#endif | ||
}; | ||
|
||
} // namespace psr | ||
|
||
#endif // PHASAR_UTILS_ADJACENCYLIST_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,194 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_UTILS_DFAMINIMIZER_H | ||
#define PHASAR_UTILS_DFAMINIMIZER_H | ||
|
||
#include "phasar/Utils/GraphTraits.h" | ||
#include "phasar/Utils/Logger.h" | ||
#include "phasar/Utils/Utilities.h" | ||
|
||
#include "llvm/ADT/IntEqClasses.h" | ||
#include "llvm/ADT/SmallBitVector.h" | ||
#include "llvm/ADT/SmallVector.h" | ||
|
||
namespace psr { | ||
|
||
template <typename GraphTy> | ||
[[nodiscard]] std::decay_t<GraphTy> | ||
createEquivalentGraphFrom(GraphTy &&G, const llvm::IntEqClasses &Eq) | ||
#if __cplusplus >= 202002L | ||
requires is_graph<GraphTy> | ||
#endif | ||
{ | ||
using traits_t = GraphTraits<GraphTy>; | ||
using vertex_t = typename traits_t::vertex_t; | ||
|
||
std::decay_t<GraphTy> Ret; | ||
|
||
llvm::SmallBitVector Handled(traits_t::size(G)); | ||
llvm::SmallVector<vertex_t> Eq2Vtx(Eq.getNumClasses(), traits_t::Invalid); | ||
llvm::SmallVector<vertex_t> WorkList; | ||
|
||
if constexpr (is_reservable_graph_trait_v<traits_t>) { | ||
traits_t::reserve(Ret, Eq.getNumClasses()); | ||
} | ||
|
||
for (auto Rt : traits_t::roots(G)) { | ||
auto EqRt = Eq[Rt]; | ||
|
||
if (Eq2Vtx[EqRt] == traits_t::Invalid) { | ||
auto NwRt = | ||
traits_t::addNode(Ret, forward_like<GraphTy>(traits_t::node(G, Rt))); | ||
Eq2Vtx[EqRt] = NwRt; | ||
traits_t::addRoot(Ret, NwRt); | ||
} | ||
WorkList.push_back(Rt); | ||
} | ||
|
||
while (!WorkList.empty()) { | ||
auto Vtx = WorkList.pop_back_val(); | ||
auto EqVtx = Eq[Vtx]; | ||
|
||
auto NwVtx = Eq2Vtx[EqVtx]; | ||
assert(NwVtx != traits_t::Invalid); | ||
|
||
Handled.set(Vtx); | ||
|
||
for (const auto &Edge : traits_t::outEdges(G, Vtx)) { | ||
auto Target = traits_t::target(Edge); | ||
auto EqTarget = Eq[Target]; | ||
if (Eq2Vtx[EqTarget] == traits_t::Invalid) { | ||
Eq2Vtx[EqTarget] = traits_t::addNode( | ||
Ret, forward_like<GraphTy>(traits_t::node(G, Target))); | ||
} | ||
if (!Handled.test(Target)) { | ||
WorkList.push_back(Target); | ||
} | ||
auto NwTarget = Eq2Vtx[EqTarget]; | ||
traits_t::addEdge(Ret, NwVtx, traits_t::withEdgeTarget(Edge, NwTarget)); | ||
} | ||
} | ||
|
||
for (auto Vtx : traits_t::vertices(Ret)) { | ||
traits_t::dedupOutEdges(Ret, Vtx); | ||
} | ||
|
||
return Ret; | ||
} | ||
|
||
template <typename GraphTy> | ||
[[nodiscard]] llvm::IntEqClasses minimizeGraph(const GraphTy &G) | ||
#if __cplusplus >= 202002L | ||
requires is_graph<GraphTy> | ||
#endif | ||
{ | ||
|
||
using traits_t = GraphTraits<GraphTy>; | ||
using vertex_t = typename traits_t::vertex_t; | ||
using edge_t = typename traits_t::edge_t; | ||
|
||
auto DagSize = traits_t::size(G); | ||
llvm::SmallVector<std::pair<vertex_t, vertex_t>> WorkList; | ||
WorkList.reserve(DagSize); | ||
|
||
const auto &Vertices = traits_t::vertices(G); | ||
|
||
for (auto VtxBegin = Vertices.begin(), VtxEnd = Vertices.end(); | ||
VtxBegin != VtxEnd; ++VtxBegin) { | ||
for (auto Inner = std::next(VtxBegin); Inner != VtxEnd; ++Inner) { | ||
if (traits_t::node(G, *VtxBegin) == traits_t::node(G, *Inner) && | ||
traits_t::outDegree(G, *VtxBegin) == traits_t::outDegree(G, *Inner)) { | ||
WorkList.emplace_back(*VtxBegin, *Inner); | ||
} | ||
} | ||
} | ||
|
||
llvm::IntEqClasses Equiv(traits_t::size(G)); | ||
|
||
auto isEquivalent = [&Equiv](edge_t LHS, edge_t RHS) { | ||
if (traits_t::weight(LHS) != traits_t::weight(RHS)) { | ||
return false; | ||
} | ||
|
||
if (traits_t::target(LHS) == traits_t::target(RHS)) { | ||
return true; | ||
} | ||
|
||
return Equiv.findLeader(traits_t::target(LHS)) == | ||
Equiv.findLeader(traits_t::target(RHS)); | ||
}; | ||
|
||
auto makeEquivalent = [&Equiv](vertex_t LHS, vertex_t RHS) { | ||
if (LHS == RHS) { | ||
return; | ||
} | ||
|
||
Equiv.join(LHS, RHS); | ||
}; | ||
|
||
auto removeAt = [&WorkList](size_t I) { | ||
std::swap(WorkList[I], WorkList.back()); | ||
WorkList.pop_back(); | ||
return I - 1; | ||
}; | ||
|
||
/// NOTE: This algorithm can be further optimized, but for now it is fast | ||
/// enough | ||
|
||
bool Changed = true; | ||
while (Changed) { | ||
Changed = false; | ||
for (size_t I = 0; I < WorkList.size(); ++I) { | ||
auto [LHS, RHS] = WorkList[I]; | ||
bool Eq = true; | ||
for (auto [LSucc, RSucc] : | ||
llvm::zip(traits_t::outEdges(G, LHS), traits_t::outEdges(G, RHS))) { | ||
if (!isEquivalent(LSucc, RSucc)) { | ||
Eq = false; | ||
break; | ||
} | ||
} | ||
|
||
if (Eq) { | ||
makeEquivalent(LHS, RHS); | ||
I = removeAt(I); | ||
Changed = true; | ||
continue; | ||
} | ||
|
||
if (traits_t::outDegree(G, LHS) == 2) { | ||
auto LFirst = *traits_t::outEdges(G, LHS).begin(); | ||
auto LSecond = *std::next(traits_t::outEdges(G, LHS).begin()); | ||
auto RFirst = *traits_t::outEdges(G, RHS).begin(); | ||
auto RSecond = *std::next(traits_t::outEdges(G, RHS).begin()); | ||
|
||
if (isEquivalent(LFirst, RSecond) && isEquivalent(LSecond, RFirst)) { | ||
makeEquivalent(LHS, RHS); | ||
I = removeAt(I); | ||
Changed = true; | ||
continue; | ||
} | ||
} | ||
} | ||
} | ||
|
||
Equiv.compress(); | ||
|
||
PHASAR_LOG_LEVEL_CAT(DEBUG, "GraphTraits", | ||
"> Computed " << Equiv.getNumClasses() | ||
<< " Equivalence classes for " << DagSize | ||
<< " nodes"); | ||
|
||
return Equiv; | ||
} | ||
|
||
} // namespace psr | ||
|
||
#endif // PHASAR_UTILS_DFAMINIMIZER_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,213 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_UTILS_GRAPHTRAITS_H | ||
#define PHASAR_UTILS_GRAPHTRAITS_H | ||
|
||
#include "phasar/Utils/TypeTraits.h" | ||
#include "phasar/Utils/Utilities.h" | ||
|
||
#include "llvm/ADT/ArrayRef.h" | ||
#include "llvm/ADT/None.h" | ||
#include "llvm/ADT/STLExtras.h" | ||
#include "llvm/ADT/StringRef.h" | ||
#include "llvm/ADT/identity.h" | ||
#include "llvm/Support/raw_ostream.h" | ||
|
||
#include <concepts> | ||
#include <functional> | ||
#include <string> | ||
#include <type_traits> | ||
|
||
namespace psr { | ||
|
||
/// We aim to get rid of boost, so introduce a new GraphTraits class to replace | ||
/// it. | ||
/// This GraphTraits type should be specialized for each type that implements a | ||
/// "graph". All the functionality should be reflected by the GraphTraits class. | ||
/// Once moving to C++20, we have nice type-checking using concepts | ||
template <typename Graph> struct GraphTraits; | ||
|
||
#if __cplusplus >= 202002L | ||
|
||
template <typename Edge> | ||
concept is_graph_edge = requires(const Edge e1, Edge e2) { | ||
{ e1 == e2 } -> std::convertible_to<bool>; | ||
{ e1 != e2 } -> std::convertible_to<bool>; | ||
{ e1 < e2 } -> std::convertible_to<bool>; | ||
}; | ||
|
||
template <typename GraphTrait> | ||
concept is_graph_trait = requires(typename GraphTrait::graph_type &graph, | ||
const typename GraphTrait::graph_type &cgraph, | ||
typename GraphTrait::value_type val, | ||
typename GraphTrait::vertex_t vtx, | ||
typename GraphTrait::edge_t edge) { | ||
typename GraphTrait::graph_type; | ||
typename GraphTrait::value_type; | ||
typename GraphTrait::vertex_t; | ||
typename GraphTrait::edge_t; | ||
requires is_graph_edge<typename GraphTrait::edge_t>; | ||
{ GraphTrait::Invalid } -> std::convertible_to<typename GraphTrait::vertex_t>; | ||
{ | ||
GraphTrait::addNode(graph, val) | ||
} -> std::convertible_to<typename GraphTrait::vertex_t>; | ||
{GraphTrait::addEdge(graph, vtx, edge)}; | ||
{ | ||
GraphTrait::outEdges(cgraph, vtx) | ||
} -> psr::is_iterable_over_v<typename GraphTrait::edge_t>; | ||
{ GraphTrait::outDegree(cgraph, vtx) } -> std::convertible_to<size_t>; | ||
{GraphTrait::dedupOutEdges(graph, vtx)}; | ||
{ | ||
GraphTrait::nodes(cgraph) | ||
} -> psr::is_iterable_over_v<typename GraphTrait::value_type>; | ||
{ | ||
GraphTrait::vertices(cgraph) | ||
} -> psr::is_iterable_over_v<typename GraphTrait::value_type>; | ||
{ | ||
GraphTrait::node(cgraph, vtx) | ||
} -> std::convertible_to<typename GraphTrait::value_type>; | ||
{ GraphTrait::size(cgraph) } -> std::convertible_to<size_t>; | ||
{GraphTrait::addRoot(graph, vtx)}; | ||
{ | ||
GraphTrait::roots(cgraph) | ||
} -> psr::is_iterable_over_v<typename GraphTrait::vertex_t>; | ||
{ GraphTrait::pop(graph, vtx) } -> std::same_as<bool>; | ||
{ GraphTrait::roots_size(cgraph) } -> std::convertible_to<size_t>; | ||
{ | ||
GraphTrait::target(edge) | ||
} -> std::convertible_to<typename GraphTrait::vertex_t>; | ||
{ | ||
GraphTrait::withEdgeTarget(edge, vtx) | ||
} -> std::convertible_to<typename GraphTrait::edge_t>; | ||
{GraphTrait::weight(edge)}; | ||
}; | ||
|
||
template <typename Graph> | ||
concept is_graph = requires(Graph g) { | ||
typename GraphTraits<std::decay_t<Graph>>; | ||
requires is_graph_trait<GraphTraits<std::decay_t<Graph>>>; | ||
}; | ||
|
||
template <typename GraphTrait> | ||
concept is_reservable_graph_trait_v = is_graph_trait<GraphTrait> && | ||
requires(typename GraphTrait::graph_type &g) { | ||
{GraphTrait::reserve(g, size_t(0))}; | ||
}; | ||
|
||
#else | ||
namespace detail { | ||
template <typename GraphTrait, typename = void> | ||
// NOLINTNEXTLINE(readability-identifier-naming) | ||
struct is_reservable_graph_trait : std::false_type {}; | ||
template <typename GraphTrait> | ||
struct is_reservable_graph_trait< | ||
GraphTrait, | ||
std::void_t<decltype(GraphTrait::reserve( | ||
std::declval<typename GraphTrait::graph_type &>(), size_t()))>> | ||
: std::true_type {}; | ||
|
||
template <typename GraphTrait, typename = void> | ||
// NOLINTNEXTLINE(readability-identifier-naming) | ||
struct is_removable_graph_trait : std::false_type {}; | ||
template <typename GraphTrait> | ||
struct is_removable_graph_trait< | ||
GraphTrait, | ||
std::void_t<typename GraphTrait::edge_iterator, | ||
typename GraphTrait::roots_iterator, | ||
decltype(GraphTrait::removeEdge( | ||
std::declval<typename GraphTrait::graph_type &>(), | ||
std::declval<typename GraphTrait::vertex_t>(), | ||
std::declval<typename GraphTrait::edge_iterator>())), | ||
decltype(GraphTrait::removeRoot( | ||
std::declval<typename GraphTrait::graph_type &>(), | ||
std::declval<typename GraphTrait::roots_iterator>()))>> | ||
: std::true_type {}; | ||
} // namespace detail | ||
|
||
template <typename GraphTrait> | ||
// NOLINTNEXTLINE(readability-identifier-naming) | ||
static constexpr bool is_reservable_graph_trait_v = | ||
detail::is_reservable_graph_trait<GraphTrait>::value; | ||
|
||
template <typename GraphTrait> | ||
// NOLINTNEXTLINE(readability-identifier-naming) | ||
static constexpr bool is_removable_graph_trait_v = | ||
detail::is_removable_graph_trait<GraphTrait>::value; | ||
#endif | ||
|
||
template <typename GraphTy> | ||
std::decay_t<GraphTy> reverseGraph(GraphTy &&G) | ||
#if __cplusplus >= 202002L | ||
requires is_graph<GraphTy> | ||
#endif | ||
{ | ||
std::decay_t<GraphTy> Ret; | ||
using traits_t = GraphTraits<std::decay_t<GraphTy>>; | ||
if constexpr (is_reservable_graph_trait_v<traits_t>) { | ||
traits_t::reserve(Ret, traits_t::size(G)); | ||
} | ||
|
||
for (auto &Nod : traits_t::nodes(G)) { | ||
traits_t::addNode(Ret, forward_like<GraphTy>(Nod)); | ||
} | ||
for (auto I : traits_t::vertices(G)) { | ||
for (auto Child : traits_t::outEdges(G, I)) { | ||
traits_t::addEdge(Ret, traits_t::target(Child), | ||
traits_t::withEdgeTarget(Child, I)); | ||
} | ||
if (traits_t::outDegree(G, I) == 0) { | ||
traits_t::addRoot(Ret, I); | ||
} | ||
} | ||
return Ret; | ||
} | ||
|
||
struct DefaultNodeTransform { | ||
template <typename N> std::string operator()(const N &Nod) const { | ||
std::string Buf; | ||
llvm::raw_string_ostream ROS(Buf); | ||
ROS << Nod; | ||
ROS.flush(); | ||
return Buf; | ||
} | ||
}; | ||
|
||
template <typename GraphTy, typename NodeTransform = DefaultNodeTransform> | ||
void printGraph(const GraphTy &G, llvm::raw_ostream &OS, | ||
llvm::StringRef Name = "", NodeTransform NodeToString = {}) | ||
#if __cplusplus >= 202002L | ||
requires is_graph<GraphTy> | ||
#endif | ||
{ | ||
using traits_t = GraphTraits<GraphTy>; | ||
|
||
OS << "digraph " << Name << " {\n"; | ||
psr::scope_exit CloseBrace = [&OS] { OS << "}\n"; }; | ||
|
||
auto Sz = traits_t::size(G); | ||
|
||
for (size_t I = 0; I < Sz; ++I) { | ||
OS << I; | ||
if constexpr (!std::is_same_v<llvm::NoneType, | ||
typename traits_t::value_type>) { | ||
OS << "[label=\""; | ||
OS.write_escaped(std::invoke(NodeToString, traits_t::node(G, I))); | ||
OS << "\"]"; | ||
} | ||
OS << ";\n"; | ||
for (const auto &Edge : traits_t::outEdges(G, I)) { | ||
OS << I << "->" << Edge << ";\n"; | ||
} | ||
} | ||
} | ||
|
||
} // namespace psr | ||
|
||
#endif // PHASAR_UTILS_GRAPHTRAITS_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,73 @@ | ||
/****************************************************************************** | ||
* Copyright (c) 2022 Philipp Schubert. | ||
* All rights reserved. This program and the accompanying materials are made | ||
* available under the terms of LICENSE.txt. | ||
* | ||
* Contributors: | ||
* Fabian Schiebel | ||
*****************************************************************************/ | ||
|
||
#ifndef PHASAR_UTILS_IOTAITERATOR_H | ||
#define PHASAR_UTILS_IOTAITERATOR_H | ||
|
||
#include "phasar/Utils/TypeTraits.h" | ||
|
||
#include "llvm/ADT/iterator_range.h" | ||
|
||
#include <cstddef> | ||
#include <iterator> | ||
#include <optional> | ||
#include <type_traits> | ||
|
||
namespace psr { | ||
/// An iterator that iterates over the same value a specified number of times | ||
template <typename T> class IotaIterator { | ||
public: | ||
using value_type = T; | ||
using reference = T; | ||
using pointer = const T *; | ||
using difference_type = ptrdiff_t; | ||
using iterator_category = std::forward_iterator_tag; | ||
|
||
constexpr reference operator*() const noexcept { return Elem; } | ||
constexpr pointer operator->() const noexcept { return &Elem; } | ||
|
||
constexpr IotaIterator &operator++() noexcept { | ||
++Elem; | ||
return *this; | ||
} | ||
constexpr IotaIterator operator++(int) noexcept { | ||
auto Ret = *this; | ||
++*this; | ||
return Ret; | ||
} | ||
|
||
constexpr bool operator==(const IotaIterator &Other) const noexcept { | ||
return Other.Elem == Elem; | ||
} | ||
constexpr bool operator!=(const IotaIterator &Other) const noexcept { | ||
return !(*this == Other); | ||
} | ||
|
||
constexpr explicit IotaIterator(T Elem) noexcept : Elem(Elem) {} | ||
|
||
constexpr IotaIterator() noexcept = default; | ||
|
||
private: | ||
T Elem{}; | ||
}; | ||
|
||
template <typename T> | ||
using IotaRangeType = llvm::iterator_range<IotaIterator<T>>; | ||
template <typename T> constexpr auto iota(T From, T To) noexcept { | ||
static_assert(std::is_integral_v<T>, "Iota only works on integers"); | ||
using iterator_type = IotaIterator<std::decay_t<T>>; | ||
auto Ret = llvm::make_range(iterator_type(From), iterator_type(To)); | ||
return Ret; | ||
} | ||
|
||
static_assert(is_iterable_over_v<IotaRangeType<int>, int>); | ||
|
||
} // namespace psr | ||
|
||
#endif // PHASAR_UTILS_IOTAITERATOR_H |
Oops, something went wrong.