diff --git a/.clang-tidy b/.clang-tidy index 5d40d294db..8447efed92 100644 --- a/.clang-tidy +++ b/.clang-tidy @@ -31,7 +31,7 @@ Checks: '-*, modernize-*, -modernize-use-trailing-return-type, performance-*, - clang-analyzer-*, + clang-analyzer-* ' FormatStyle: LLVM diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d109a180f3..67a32f1a53 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -65,6 +65,7 @@ jobs: -DCMAKE_BUILD_TYPE=${{ matrix.build }} \ -DBUILD_SWIFT_TESTS=ON \ -DPHASAR_DEBUG_LIBDEPS=ON \ + -DPHASAR_USE_Z3=ON \ ${{ matrix.flags }} \ -G Ninja cmake --build . diff --git a/CMakeLists.txt b/CMakeLists.txt index a32ac2bc24..ab524715d9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,4 +1,4 @@ -cmake_minimum_required (VERSION 3.9) +cmake_minimum_required (VERSION 3.14) # Avoid IPO/LTO Warnings: cmake_policy(SET CMP0069 NEW) @@ -150,6 +150,8 @@ option(PHASAR_BUILD_UNITTESTS "Build all tests (default is ON)" ON) option(PHASAR_BUILD_OPENSSL_TS_UNITTESTS "Build OPENSSL typestate tests (require OpenSSL, default is OFF)" OFF) +option(PHASAR_USE_Z3 "Build the phasar_llvm_pathsensitivity library with Z3 support for constraint solving (default is OFF)" OFF) + option(PHASAR_BUILD_IR "Build IR test code (default is ON)" ON) option(PHASAR_ENABLE_CLANG_TIDY_DURING_BUILD "Run clang-tidy during build (default is OFF)" OFF) @@ -259,11 +261,13 @@ add_subdirectory(external/json) # The following workaround may collapse or become unnecessary once the issue is # changed or fixed in nlohmann_json_schema_validator. -#Override option of nlohmann_json_schema_validator to not build its tests +# Override option of nlohmann_json_schema_validator to not build its tests set(BUILD_TESTS OFF CACHE BOOL "Build json-schema-validator-tests") if (PHASAR_IN_TREE) set_property(GLOBAL APPEND PROPERTY LLVM_EXPORTS nlohmann_json_schema_validator) + + set (PHASAR_USE_Z3 OFF) endif() # Json Schema Validator @@ -337,6 +341,21 @@ if(NOT LLVM_ENABLE_RTTI AND NOT PHASAR_IN_TREE) message(FATAL_ERROR "PhASAR requires a LLVM version that is built with RTTI") endif() +# Z3 Solver +if(PHASAR_USE_Z3) + # This z3-version is the same version LLVM requires; however, we cannot just use Z3 via the LLVM interface + # as it lacks some functionality (such as z3::expr::simplify()) that we require + find_package(Z3 4.7.1 REQUIRED) + + if(NOT TARGET z3) + add_library(z3 IMPORTED SHARED) + set_property(TARGET z3 PROPERTY + IMPORTED_LOCATION ${Z3_LIBRARIES}) + set_property(TARGET z3 PROPERTY + INTERFACE_INCLUDE_DIRECTORIES ${Z3_INCLUDE_DIR}) + endif() +endif(PHASAR_USE_Z3) + # Clang option(BUILD_PHASAR_CLANG "Build the phasar_clang library (default is ON)" ON) diff --git a/Config.cmake.in b/Config.cmake.in index 5828af35ee..8093b5f782 100644 --- a/Config.cmake.in +++ b/Config.cmake.in @@ -13,6 +13,11 @@ find_package(LLVM 14 REQUIRED CONFIG) set(PHASAR_USE_LLVM_FAT_LIB @USE_LLVM_FAT_LIB@) set(PHASAR_BUILD_DYNLIB @PHASAR_BUILD_DYNLIB@) +set(PHASAR_USE_Z3 @PHASAR_USE_Z3@) + +if (PHASAR_USE_Z3) + find_dependency(Z3) +endif() set(PHASAR_COMPONENTS utils diff --git a/include/phasar/DataFlow.h b/include/phasar/DataFlow.h index a642ae4847..88453a251d 100644 --- a/include/phasar/DataFlow.h +++ b/include/phasar/DataFlow.h @@ -24,6 +24,7 @@ #include "phasar/DataFlow/IfdsIde/Solver/IDESolver.h" #include "phasar/DataFlow/IfdsIde/Solver/IFDSSolver.h" #include "phasar/DataFlow/IfdsIde/Solver/JumpFunctions.h" +#include "phasar/DataFlow/IfdsIde/Solver/PathAwareIDESolver.h" #include "phasar/DataFlow/IfdsIde/Solver/PathEdge.h" #include "phasar/DataFlow/IfdsIde/SolverResults.h" #include "phasar/DataFlow/IfdsIde/SpecialSummaries.h" @@ -32,5 +33,7 @@ #include "phasar/DataFlow/Mono/IntraMonoProblem.h" #include "phasar/DataFlow/Mono/Solver/InterMonoSolver.h" #include "phasar/DataFlow/Mono/Solver/IntraMonoSolver.h" +#include "phasar/DataFlow/PathSensitivity/PathSensitivityConfig.h" +#include "phasar/DataFlow/PathSensitivity/PathSensitivityManager.h" #endif // PHASAR_DATAFLOW_H diff --git a/include/phasar/DataFlow/IfdsIde/Solver/ESGEdgeKind.h b/include/phasar/DataFlow/IfdsIde/Solver/ESGEdgeKind.h new file mode 100644 index 0000000000..94b98ed893 --- /dev/null +++ b/include/phasar/DataFlow/IfdsIde/Solver/ESGEdgeKind.h @@ -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 diff --git a/include/phasar/DataFlow/IfdsIde/Solver/IDESolver.h b/include/phasar/DataFlow/IfdsIde/Solver/IDESolver.h index cfe82bacfa..36b782b4cf 100644 --- a/include/phasar/DataFlow/IfdsIde/Solver/IDESolver.h +++ b/include/phasar/DataFlow/IfdsIde/Solver/IDESolver.h @@ -26,6 +26,7 @@ #include "phasar/DataFlow/IfdsIde/IDETabulationProblem.h" #include "phasar/DataFlow/IfdsIde/IFDSTabulationProblem.h" #include "phasar/DataFlow/IfdsIde/InitialSeeds.h" +#include "phasar/DataFlow/IfdsIde/Solver/ESGEdgeKind.h" #include "phasar/DataFlow/IfdsIde/Solver/FlowEdgeFunctionCache.h" #include "phasar/DataFlow/IfdsIde/Solver/IDESolverAPIMixin.h" #include "phasar/DataFlow/IfdsIde/Solver/JumpFunctions.h" @@ -297,20 +298,25 @@ class IDESolver } }); + bool HasNoCalleeInformation = true; + // for each possible callee for (f_t SCalledProcN : Callees) { // still line 14 // check if a special summary for the called procedure exists FlowFunctionPtrType SpecialSum = CachedFlowEdgeFunctions.getSummaryFlowFunction(n, SCalledProcN); + // if a special summary is available, treat this as a normal flow // and use the summary flow and edge functions + if (SpecialSum) { + HasNoCalleeInformation = false; PHASAR_LOG_LEVEL(DEBUG, "Found and process special summary"); for (n_t ReturnSiteN : ReturnSiteNs) { container_type Res = computeSummaryFlowFunction(SpecialSum, d1, d2); INC_COUNTER("SpecialSummary-FF Application", 1, Full); ADD_TO_HISTOGRAM("Data-flow facts", Res.size(), 1, Full); - saveEdges(n, ReturnSiteN, d2, Res, false); + saveEdges(n, ReturnSiteN, d2, Res, ESGEdgeKind::Summary); for (d_t d3 : Res) { EdgeFunction SumEdgFnE = CachedFlowEdgeFunctions.getSummaryEdgeFunction(n, d2, @@ -341,7 +347,8 @@ class IDESolver } // if startPointsOf is empty, the called function is a declaration for (n_t SP : StartPointsOf) { - saveEdges(n, SP, d2, Res, true); + HasNoCalleeInformation = false; + saveEdges(n, SP, d2, Res, ESGEdgeKind::Call); // for each result node of the call-flow function for (d_t d3 : Res) { using TableCell = typename Table>::Cell; @@ -382,7 +389,7 @@ class IDESolver RetFunction, d3, d4, n, Container{d2}); ADD_TO_HISTOGRAM("Data-flow facts", ReturnedFacts.size(), 1, Full); - saveEdges(eP, RetSiteN, d4, ReturnedFacts, true); + saveEdges(eP, RetSiteN, d4, ReturnedFacts, ESGEdgeKind::Ret); // for each target value of the function for (d_t d5 : ReturnedFacts) { // update the caller-side summary function @@ -439,7 +446,9 @@ class IDESolver container_type ReturnFacts = computeCallToReturnFlowFunction(CallToReturnFF, d1, d2); ADD_TO_HISTOGRAM("Data-flow facts", ReturnFacts.size(), 1, Full); - saveEdges(n, ReturnSiteN, d2, ReturnFacts, false); + saveEdges(n, ReturnSiteN, d2, ReturnFacts, + HasNoCalleeInformation ? ESGEdgeKind::SkipUnknownFn + : ESGEdgeKind::CallToRet); for (d_t d3 : ReturnFacts) { EdgeFunction EdgeFnE = CachedFlowEdgeFunctions.getCallToRetEdgeFunction(n, d2, ReturnSiteN, @@ -478,7 +487,7 @@ class IDESolver INC_COUNTER("FF Queries", 1, Full); const container_type Res = computeNormalFlowFunction(FlowFunc, d1, d2); ADD_TO_HISTOGRAM("Data-flow facts", Res.size(), 1, Full); - saveEdges(n, nPrime, d2, Res, false); + saveEdges(n, nPrime, d2, Res, ESGEdgeKind::Normal); for (d_t d3 : Res) { EdgeFunction g = CachedFlowEdgeFunctions.getNormalEdgeFunction(n, d2, nPrime, d3); @@ -690,12 +699,12 @@ class IDESolver } virtual void saveEdges(n_t SourceNode, n_t SinkStmt, d_t SourceVal, - const container_type &DestVals, bool InterP) { + const container_type &DestVals, ESGEdgeKind Kind) { if (!SolverConfig.recordEdges()) { return; } Table> &TgtMap = - (InterP) ? ComputedInterPathEdges : ComputedIntraPathEdges; + (isInterProc(Kind)) ? ComputedInterPathEdges : ComputedIntraPathEdges; TgtMap.get(SourceNode, SinkStmt)[SourceVal].insert(DestVals.begin(), DestVals.end()); } @@ -833,7 +842,7 @@ class IDESolver const container_type Targets = computeReturnFlowFunction(RetFunction, d1, d2, c, Entry.second); ADD_TO_HISTOGRAM("Data-flow facts", Targets.size(), 1, Full); - saveEdges(n, RetSiteC, d2, Targets, true); + saveEdges(n, RetSiteC, d2, Targets, ESGEdgeKind::Ret); // for each target value at the return site // line 23 for (d_t d5 : Targets) { @@ -902,7 +911,7 @@ class IDESolver const container_type Targets = computeReturnFlowFunction( RetFunction, d1, d2, Caller, Container{ZeroValue}); ADD_TO_HISTOGRAM("Data-flow facts", Targets.size(), 1, Full); - saveEdges(n, RetSiteC, d2, Targets, true); + saveEdges(n, RetSiteC, d2, Targets, ESGEdgeKind::Ret); for (d_t d5 : Targets) { EdgeFunction f5 = CachedFlowEdgeFunctions.getReturnEdgeFunction( diff --git a/include/phasar/DataFlow/IfdsIde/Solver/PathAwareIDESolver.h b/include/phasar/DataFlow/IfdsIde/Solver/PathAwareIDESolver.h new file mode 100644 index 0000000000..711932c878 --- /dev/null +++ b/include/phasar/DataFlow/IfdsIde/Solver/PathAwareIDESolver.h @@ -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 > +class PathAwareIDESolver : public IDESolver { + using base_t = IDESolver; + +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 &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 & + getExplicitESG() const &noexcept { + return ESG; + } + + [[nodiscard]] ExplodedSuperGraph &&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 ESG; +}; + +template +PathAwareIDESolver(ProblemTy &) + -> PathAwareIDESolver; + +} // namespace psr + +#endif // PHASAR_DATAFLOW_IFDSIDE_SOLVER_PATHAWAREIDESOLVER_H diff --git a/include/phasar/DataFlow/IfdsIde/SolverResults.h b/include/phasar/DataFlow/IfdsIde/SolverResults.h index 512d80063f..65da6d5e8f 100644 --- a/include/phasar/DataFlow/IfdsIde/SolverResults.h +++ b/include/phasar/DataFlow/IfdsIde/SolverResults.h @@ -232,6 +232,7 @@ class OwningSolverResults [[nodiscard]] operator SolverResults() const &noexcept { return get(); } + operator SolverResults() && = delete; private: diff --git a/include/phasar/DataFlow/PathSensitivity/ExplodedSuperGraph.h b/include/phasar/DataFlow/PathSensitivity/ExplodedSuperGraph.h new file mode 100644 index 0000000000..df9d1ec3cc --- /dev/null +++ b/include/phasar/DataFlow/PathSensitivity/ExplodedSuperGraph.h @@ -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 +#include +#include +#include +#include +#include +#include +#include +#include +#include + +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 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 Neighbors{}; + }; + + class BuildNodeRef; + class NodeRef { + friend ExplodedSuperGraph; + friend class BuildNodeRef; + + public: + NodeRef() noexcept = default; + NodeRef(std::nullptr_t) noexcept {} + + [[nodiscard]] ByConstRef value() const noexcept { + assert(*this); + return Owner->NodeDataOwner[NodeId].Value; + } + + [[nodiscard]] ByConstRef 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) + : 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 getZeroValue() const noexcept { + return ZeroValue; + } + + template + 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 &ND) const { + return std::hash()(ND.first) * 31 + std::hash()(ND.second); + } + }; + + struct PathInfoEq { + bool operator()(const std::pair &Lhs, + const std::pair &Rhs) const { + return Lhs.first == Rhs.first && Lhs.second == Rhs.second; + } + }; + + [[nodiscard]] std::optional 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 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 NodeDataOwner; + std::vector NodeAdjOwner; + std::unordered_map, size_t, PathInfoHash, PathInfoEq> + FlowFactVertexMap{}; + + // ZeroValue + d_t ZeroValue; +}; + +} // namespace psr + +#endif // PHASAR_DATAFLOW_PATHSENSITIVITY_EXPLODEDSUPERGRAPH_H diff --git a/include/phasar/DataFlow/PathSensitivity/FlowPath.h b/include/phasar/DataFlow/PathSensitivity/FlowPath.h new file mode 100644 index 0000000000..532852ab0e --- /dev/null +++ b/include/phasar/DataFlow/PathSensitivity/FlowPath.h @@ -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 struct FlowPath { + llvm::SmallVector Path; + z3::expr Constraint; + z3::model Model; + + FlowPath(llvm::ArrayRef Path, const z3::expr &Constraint) + : Path(Path.begin(), Path.end()), Constraint(Constraint), + Model(Constraint.ctx()) {} + FlowPath(llvm::ArrayRef 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() 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 using FlowPathSequence = std::vector>; + +} // namespace psr + +#endif // PHASAR_PHASARLLVM_DATAFLOW_PATHSENSITIVITY_FLOWPATH_H diff --git a/include/phasar/DataFlow/PathSensitivity/PathSensitivityConfig.h b/include/phasar/DataFlow/PathSensitivity/PathSensitivityConfig.h new file mode 100644 index 0000000000..582dd02b17 --- /dev/null +++ b/include/phasar/DataFlow/PathSensitivity/PathSensitivityConfig.h @@ -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 +#include + +namespace psr { + +template 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(this); + Ret.DAGSizeThreshold = MaxDAGSize; + return Ret; + } + + [[nodiscard]] DerivedConfig + withDAGDepthThreshold(size_t MaxDAGDepth) const noexcept { + auto Ret = *static_cast(this); + Ret.DAGDepthThreshold = MaxDAGDepth; + return Ret; + } + + [[nodiscard]] DerivedConfig + withNumPathsThreshold(size_t MaxNumPaths) const noexcept { + auto Ret = *static_cast(this); + Ret.NumPathsThreshold = MaxNumPaths; + return Ret; + } + + [[nodiscard]] DerivedConfig withMinimizeDAG(bool DoMinimize) const noexcept { + auto Ret = *static_cast(this); + Ret.MinimizeDAG = DoMinimize; + return Ret; + } +}; + +struct PathSensitivityConfig + : PathSensitivityConfigBase {}; + +} // namespace psr + +#endif // PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYCONFIG_H diff --git a/include/phasar/DataFlow/PathSensitivity/PathSensitivityManager.h b/include/phasar/DataFlow/PathSensitivity/PathSensitivityManager.h new file mode 100644 index 0000000000..d781d127f5 --- /dev/null +++ b/include/phasar/DataFlow/PathSensitivity/PathSensitivityManager.h @@ -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 +#include + +namespace psr { + +template +class PathSensitivityManager + : public PathSensitivityManagerBase, + public PathSensitivityManagerMixin< + PathSensitivityManager, AnalysisDomainTy, + typename PathSensitivityManagerBase< + typename AnalysisDomainTy::n_t>::graph_type> { + using base_t = PathSensitivityManagerBase; + using mixin_t = + PathSensitivityManagerMixin; + +public: + using n_t = typename AnalysisDomainTy::n_t; + using d_t = typename AnalysisDomainTy::d_t; + using typename PathSensitivityManagerBase::graph_type; + + PathSensitivityManager( + const ExplodedSuperGraph *ESG) noexcept + : mixin_t(ESG) {} +}; +} // namespace psr + +#endif // PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYMANAGER_H diff --git a/include/phasar/DataFlow/PathSensitivity/PathSensitivityManagerBase.h b/include/phasar/DataFlow/PathSensitivity/PathSensitivityManagerBase.h new file mode 100644 index 0000000000..e1195bb573 --- /dev/null +++ b/include/phasar/DataFlow/PathSensitivity/PathSensitivityManagerBase.h @@ -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 +class PathSensitivityManagerMixin; + +template class PathSensitivityManagerBase { +public: + using n_t = N; + using graph_type = AdjacencyList>; + + static_assert(std::is_integral_v::vertex_t>); + + template + friend class PathSensitivityManagerMixin; + +protected: + using graph_traits_t = GraphTraits; + 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 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 + [[nodiscard]] static graph_type + reverseDAG(graph_type &&Dag, const VertexTransform &Equiv, size_t EquivSize, + size_t MaxDepth) { + using graph_traits_t = psr::GraphTraits; + using vertex_t = typename graph_traits_t::vertex_t; + graph_type Ret{}; + if constexpr (psr::is_reservable_graph_trait_v) { + 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 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); + 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(alloca(NumBytes)) + : new char[NumBytes]; + std::unique_ptr Owner; // NOLINT + if (NumBytes > MaxNumBytesInStackBuf) { + Owner.reset(Buf); + } + + auto Cache = reinterpret_cast(Buf); + std::uninitialized_fill_n(Cache, EquivSize, graph_traits_t::Invalid); + + auto *WLConsumeBegin = + reinterpret_cast *>(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; + +} // namespace psr + +#endif // PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYMANAGERBASE_H diff --git a/include/phasar/DataFlow/PathSensitivity/PathSensitivityManagerMixin.h b/include/phasar/DataFlow/PathSensitivity/PathSensitivityManagerMixin.h new file mode 100644 index 0000000000..6a986d99c7 --- /dev/null +++ b/include/phasar/DataFlow/PathSensitivity/PathSensitivityManagerMixin.h @@ -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 +#include +#include +#include + +namespace llvm { +class DbgInfoIntrinsic; +} // namespace llvm + +namespace psr { +template +class PathSensitivityManagerMixin { + using n_t = typename AnalysisDomainTy::n_t; + using d_t = typename AnalysisDomainTy::d_t; + + using NodeRef = typename ExplodedSuperGraph::NodeRef; + using graph_type = GraphType; + using graph_traits_t = GraphTraits; + using vertex_t = typename graph_traits_t::vertex_t; + + struct PathsToContext { + llvm::DenseMap Cache; + llvm::SetVector> CurrPath; + }; + + static const ExplodedSuperGraph & + assertNotNull(const ExplodedSuperGraph *ESG) noexcept { + assert(ESG != nullptr && "The exploded supergraph passed to the " + "pathSensitivityManager must not be nullptr!"); + return *ESG; + } + +protected: + PathSensitivityManagerMixin( + const ExplodedSuperGraph *ESG) noexcept + : ESG(assertNotNull(ESG)) { + static_assert(std::is_base_of_v, 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>> + [[nodiscard]] GraphType + pathsDagToAll(n_t Inst, FactsRangeTy FactsRange, + const PathSensitivityConfigBase &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::Invalid) { + graph_traits_t::addRoot(Dag, Rt); + } + } + +#ifndef NDEBUG + if (!static_cast(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(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>> + [[nodiscard]] GraphType + pathsDagTo(n_t Inst, const SolverResults &SR, + const PathSensitivityConfigBase &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>> + [[nodiscard]] GraphType + pathsDagTo(n_t Inst, d_t Fact, + const PathSensitivityConfigBase &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>> + [[nodiscard]] GraphType + pathsDagToInLLVMSSA(n_t Inst, d_t Fact, + const PathSensitivityConfigBase &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(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 + 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 + 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 + 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 &ESG; +}; +} // namespace psr + +#endif // PHASAR_DATAFLOW_PATHSENSITIVITY_PATHSENSITIVITYMANAGERMIXIN_H diff --git a/include/phasar/DataFlow/PathSensitivity/PathTracingFilter.h b/include/phasar/DataFlow/PathSensitivity/PathTracingFilter.h new file mode 100644 index 0000000000..8baaa10961 --- /dev/null +++ b/include/phasar/DataFlow/PathSensitivity/PathTracingFilter.h @@ -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 + +namespace psr { +template 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 + constexpr bool operator()(T && /*First*/, U && /*Second*/) const noexcept { + return false; + } +}; +} // namespace detail + +using DefaultPathTracingFilter = + PathTracingFilter; + +template +struct is_pathtracingfilter_for : std::false_type {}; + +template +struct is_pathtracingfilter_for< + PathTracingFilter, NodeRef, + std::enable_if_t && + std::is_invocable_r_v>> + : std::true_type {}; + +template +constexpr static bool is_pathtracingfilter_for_v = + is_pathtracingfilter_for::value; +} // namespace psr + +#endif // PHASAR_DATAFLOW_PATHSENSITIVITY_PATHTRACINGFILTER_H diff --git a/include/phasar/PhasarLLVM/DataFlow/PathSensitivity/LLVMPathConstraints.h b/include/phasar/PhasarLLVM/DataFlow/PathSensitivity/LLVMPathConstraints.h new file mode 100644 index 0000000000..887f4f54bc --- /dev/null +++ b/include/phasar/PhasarLLVM/DataFlow/PathSensitivity/LLVMPathConstraints.h @@ -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 + +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 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 getConstraintFromEdge(const llvm::Instruction *Curr, + const llvm::Instruction *Succ); + + std::optional + getConstraintAndVariablesFromEdge(const llvm::Instruction *Curr, + const llvm::Instruction *Succ); + +private: + [[nodiscard]] std::optional + 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 Z3Ctx; + std::unordered_map Z3Expr; + bool IgnoreDebugInstructions; +}; +} // namespace psr + +#endif // PHASAR_PHASARLLVM_PATHSENSITIVITY_LLVMPATHCONSTRAINTS_H diff --git a/include/phasar/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitivityConfig.h b/include/phasar/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitivityConfig.h new file mode 100644 index 0000000000..3d219f5fcd --- /dev/null +++ b/include/phasar/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitivityConfig.h @@ -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 + +namespace psr { +struct Z3BasedPathSensitivityConfig + : PathSensitivityConfigBase { + std::optional 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 diff --git a/include/phasar/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitvityManager.h b/include/phasar/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitvityManager.h new file mode 100644 index 0000000000..988a977c4a --- /dev/null +++ b/include/phasar/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitvityManager.h @@ -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 +#include +#include +#include +#include + +namespace llvm { +class Instruction; +} // namespace llvm + +namespace psr { +class LLVMPathConstraints; + +class Z3BasedPathSensitivityManagerBase + : public PathSensitivityManagerBase { +public: + using n_t = const llvm::Instruction *; + + static_assert(is_removable_graph_trait_v, + "Invalid graph type: Must support edge-removal!"); + +protected: + z3::expr filterOutUnreachableNodes(graph_type &RevDAG, vertex_t Leaf, + const Z3BasedPathSensitivityConfig &Config, + LLVMPathConstraints &LPC) const; + + FlowPathSequence + filterAndFlattenRevDag(graph_type &RevDAG, vertex_t Leaf, n_t FinalInst, + const Z3BasedPathSensitivityConfig &Config, + LLVMPathConstraints &LPC) const; + + static void deduplicatePaths(FlowPathSequence &Paths); +}; + +template >> +class Z3BasedPathSensitivityManager + : public Z3BasedPathSensitivityManagerBase, + public PathSensitivityManagerMixin< + Z3BasedPathSensitivityManager, AnalysisDomainTy, + typename Z3BasedPathSensitivityManagerBase::graph_type> { + using base_t = PathSensitivityManagerBase; + using mixin_t = PathSensitivityManagerMixin; + +public: + using n_t = typename AnalysisDomainTy::n_t; + using d_t = typename AnalysisDomainTy::d_t; + using typename PathSensitivityManagerBase::graph_type; + using MaybeFlowPathSeq = std::variant, z3::expr>; + + explicit Z3BasedPathSensitivityManager( + const ExplodedSuperGraph *ESG, + Z3BasedPathSensitivityConfig Config, LLVMPathConstraints *LPC = nullptr) + : mixin_t(ESG), Config(std::move(Config)), LPC(LPC) { + if (!LPC) { + this->LPC = std::make_unique(); + } + } + + FlowPathSequence 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 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(); + } + + 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 &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 LPC{}; +}; +} // namespace psr + +#endif // PHASAR_PHASARLLVM_PATHSENSITIVITY_Z3BASEDPATHSENSITIVITYMANAGER_H diff --git a/include/phasar/Utils/AdjacencyList.h b/include/phasar/Utils/AdjacencyList.h new file mode 100644 index 0000000000..e09bb99fa5 --- /dev/null +++ b/include/phasar/Utils/AdjacencyList.h @@ -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 +#include +#include + +namespace psr { + +template struct AdjacencyList { + llvm::SmallVector Nodes{}; + llvm::SmallVector, 0> Adj{}; + llvm::SmallVector Roots{}; +}; + +template struct AdjacencyList { + llvm::SmallVector, 0> Adj{}; + llvm::SmallVector Roots{}; +}; + +/// A simple graph implementation based on an adjacency list +template +struct GraphTraits> { + using graph_type = AdjacencyList; + using value_type = T; + using vertex_t = unsigned; + using edge_t = EdgeTy; + using edge_iterator = typename llvm::ArrayRef::const_iterator; + using roots_iterator = typename llvm::ArrayRef::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::max(); + + /// Adds a new node to the graph G with node-tag Val + /// + /// \returns The vertex-descriptor for the newly created node + template >> + 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(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 >> + 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) { + 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 roots(const graph_type &G) noexcept { + if constexpr (!std::is_same_v) { + 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) { + 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 outEdges(const graph_type &G, + vertex_t Vtx) noexcept { + assert(Vtx < G.Adj.size()); + if constexpr (!std::is_same_v) { + 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) { + 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) { + 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 >> + static llvm::ArrayRef 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 >> + static llvm::MutableArrayRef 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 >> + static RepeatRangeType 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) { + 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 >> + 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 >> + 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 >> + 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) { + 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) { + 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) { + 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) { + G.Nodes.pop_back(); + } + return true; + } + return false; + } + + /// Gets the vertex-descriptor of the target-node of the given Edge + template + static std::enable_if_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 + static std::enable_if_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) { + 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) { + 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>); + static_assert(is_reservable_graph_trait>>); +#endif +}; + +} // namespace psr + +#endif // PHASAR_UTILS_ADJACENCYLIST_H diff --git a/include/phasar/Utils/DFAMinimizer.h b/include/phasar/Utils/DFAMinimizer.h new file mode 100644 index 0000000000..00a20f0db9 --- /dev/null +++ b/include/phasar/Utils/DFAMinimizer.h @@ -0,0 +1,196 @@ +/****************************************************************************** + * 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 +[[nodiscard]] std::decay_t +createEquivalentGraphFrom(GraphTy &&G, const llvm::IntEqClasses &Eq) +#if __cplusplus >= 202002L + requires is_graph +#endif +{ + using traits_t = GraphTraits; + using vertex_t = typename traits_t::vertex_t; + + std::decay_t Ret; + + llvm::SmallBitVector Handled(traits_t::size(G)); + llvm::SmallVector Eq2Vtx(Eq.getNumClasses(), traits_t::Invalid); + llvm::SmallVector WorkList; + + if constexpr (is_reservable_graph_trait_v) { + 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(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(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 +[[nodiscard]] llvm::IntEqClasses minimizeGraph(const GraphTy &G) +#if __cplusplus >= 202002L + requires is_graph +#endif +{ + + using traits_t = GraphTraits; + using vertex_t = typename traits_t::vertex_t; + using edge_t = typename traits_t::edge_t; + + auto DagSize = traits_t::size(G); + llvm::SmallVector> 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); + } + } + } + + size_t Idx = 0; + + 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 diff --git a/include/phasar/Utils/GraphTraits.h b/include/phasar/Utils/GraphTraits.h new file mode 100644 index 0000000000..be00b4b84f --- /dev/null +++ b/include/phasar/Utils/GraphTraits.h @@ -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 +#include +#include +#include + +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 struct GraphTraits; + +#if __cplusplus >= 202002L + +template +concept is_graph_edge = requires(const Edge e1, Edge e2) { + { e1 == e2 } -> std::convertible_to; + { e1 != e2 } -> std::convertible_to; + { e1 < e2 } -> std::convertible_to; +}; + +template +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; + { GraphTrait::Invalid } -> std::convertible_to; + { + GraphTrait::addNode(graph, val) + } -> std::convertible_to; + {GraphTrait::addEdge(graph, vtx, edge)}; + { + GraphTrait::outEdges(cgraph, vtx) + } -> psr::is_iterable_over_v; + { GraphTrait::outDegree(cgraph, vtx) } -> std::convertible_to; + {GraphTrait::dedupOutEdges(graph, vtx)}; + { + GraphTrait::nodes(cgraph) + } -> psr::is_iterable_over_v; + { + GraphTrait::vertices(cgraph) + } -> psr::is_iterable_over_v; + { + GraphTrait::node(cgraph, vtx) + } -> std::convertible_to; + { GraphTrait::size(cgraph) } -> std::convertible_to; + {GraphTrait::addRoot(graph, vtx)}; + { + GraphTrait::roots(cgraph) + } -> psr::is_iterable_over_v; + { GraphTrait::pop(graph, vtx) } -> std::same_as; + { GraphTrait::roots_size(cgraph) } -> std::convertible_to; + { + GraphTrait::target(edge) + } -> std::convertible_to; + { + GraphTrait::withEdgeTarget(edge, vtx) + } -> std::convertible_to; + {GraphTrait::weight(edge)}; +}; + +template +concept is_graph = requires(Graph g) { + typename GraphTraits>; + requires is_graph_trait>>; +}; + +template +concept is_reservable_graph_trait_v = is_graph_trait && + requires(typename GraphTrait::graph_type &g) { + {GraphTrait::reserve(g, size_t(0))}; +}; + +#else +namespace detail { +template +// NOLINTNEXTLINE(readability-identifier-naming) +struct is_reservable_graph_trait : std::false_type {}; +template +struct is_reservable_graph_trait< + GraphTrait, + std::void_t(), size_t()))>> + : std::true_type {}; + +template +// NOLINTNEXTLINE(readability-identifier-naming) +struct is_removable_graph_trait : std::false_type {}; +template +struct is_removable_graph_trait< + GraphTrait, + std::void_t(), + std::declval(), + std::declval())), + decltype(GraphTrait::removeRoot( + std::declval(), + std::declval()))>> + : std::true_type {}; +} // namespace detail + +template +// NOLINTNEXTLINE(readability-identifier-naming) +static constexpr bool is_reservable_graph_trait_v = + detail::is_reservable_graph_trait::value; + +template +// NOLINTNEXTLINE(readability-identifier-naming) +static constexpr bool is_removable_graph_trait_v = + detail::is_removable_graph_trait::value; +#endif + +template +std::decay_t reverseGraph(GraphTy &&G) +#if __cplusplus >= 202002L + requires is_graph +#endif +{ + std::decay_t Ret; + using traits_t = GraphTraits>; + if constexpr (is_reservable_graph_trait_v) { + traits_t::reserve(Ret, traits_t::size(G)); + } + + for (auto &Nod : traits_t::nodes(G)) { + traits_t::addNode(Ret, forward_like(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 std::string operator()(const N &Nod) const { + std::string Buf; + llvm::raw_string_ostream ROS(Buf); + ROS << Nod; + ROS.flush(); + return Buf; + } +}; + +template +void printGraph(const GraphTy &G, llvm::raw_ostream &OS, + llvm::StringRef Name = "", NodeTransform NodeToString = {}) +#if __cplusplus >= 202002L + requires is_graph +#endif +{ + using traits_t = GraphTraits; + + 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) { + 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 diff --git a/include/phasar/Utils/IotaIterator.h b/include/phasar/Utils/IotaIterator.h new file mode 100644 index 0000000000..9eab786b61 --- /dev/null +++ b/include/phasar/Utils/IotaIterator.h @@ -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 +#include +#include +#include + +namespace psr { +/// An iterator that iterates over the same value a specified number of times +template 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 +using IotaRangeType = llvm::iterator_range>; +template constexpr auto iota(T From, T To) noexcept { + static_assert(std::is_integral_v, "Iota only works on integers"); + using iterator_type = IotaIterator>; + auto Ret = llvm::make_range(iterator_type(From), iterator_type(To)); + return Ret; +} + +static_assert(is_iterable_over_v, int>); + +} // namespace psr + +#endif // PHASAR_UTILS_IOTAITERATOR_H diff --git a/include/phasar/Utils/MaybeUniquePtr.h b/include/phasar/Utils/MaybeUniquePtr.h index d5d0dd1aaf..d7cc7db022 100644 --- a/include/phasar/Utils/MaybeUniquePtr.h +++ b/include/phasar/Utils/MaybeUniquePtr.h @@ -14,7 +14,6 @@ #include #include -#include namespace psr { @@ -26,71 +25,70 @@ template class MaybeUniquePtrBase { bool Flag = false; /// Compatibility with llvm::PointerIntPair: - [[nodiscard]] T *getPointer() const noexcept { return Pointer; } - [[nodiscard]] bool getInt() const noexcept { return Flag; } - void setInt(bool Flag) noexcept { this->Flag = Flag; } + [[nodiscard]] constexpr T *getPointer() const noexcept { return Pointer; } + [[nodiscard]] constexpr bool getInt() const noexcept { return Flag; } + constexpr void setInt(bool Flag) noexcept { this->Flag = Flag; } }; std::conditional_t<(alignof(T) > 1), llvm::PointerIntPair, PointerBoolPairFallback> Data{}; - MaybeUniquePtrBase(T *Ptr, bool Owns) noexcept : Data{Ptr, Owns} {} - MaybeUniquePtrBase() noexcept = default; + constexpr MaybeUniquePtrBase(T *Ptr, bool Owns) noexcept : Data{Ptr, Owns} {} + constexpr MaybeUniquePtrBase() noexcept = default; }; template class MaybeUniquePtrBase { protected: llvm::PointerIntPair Data{}; - MaybeUniquePtrBase(T *Ptr, bool Owns) noexcept : Data{Ptr, Owns} { - static_assert(alignof(T) > 1, - "Using MaybeUniquePtr requires alignment > 1!"); - } - MaybeUniquePtrBase() noexcept = default; + constexpr MaybeUniquePtrBase(T *Ptr, bool Owns) noexcept : Data{Ptr, Owns} {} + constexpr MaybeUniquePtrBase() noexcept = default; }; } // namespace detail -/// A smart-pointer, similar to std::unique_ptr that can be used as both, -/// owning and non-owning pointer. +/// A smart-pointer, similar to std::unique_ptr, that can optionally own an +/// object. /// /// \tparam T The pointee type -/// \tparam RequireAlignment If true, the datastructure only works if alignof(T) -/// > 1 holds. Enables incomplete T types +/// \tparam RequireAlignment If true, the datastructure only works if +/// alignof(T) > 1 holds. Enables incomplete T types template class MaybeUniquePtr : detail::MaybeUniquePtrBase { using detail::MaybeUniquePtrBase::Data; public: - MaybeUniquePtr() noexcept = default; + constexpr MaybeUniquePtr() noexcept = default; - MaybeUniquePtr(T *Pointer, bool Owns = false) noexcept - : detail::MaybeUniquePtrBase( - Pointer, Owns && Pointer != nullptr) {} + constexpr MaybeUniquePtr(T *Pointer, bool Owns = false) noexcept + : detail::MaybeUniquePtrBase(Pointer, Owns) {} - MaybeUniquePtr(std::unique_ptr &&Owner) noexcept + constexpr MaybeUniquePtr(std::unique_ptr &&Owner) noexcept : MaybeUniquePtr(Owner.release(), true) {} template - MaybeUniquePtr(std::unique_ptr &&Owner) noexcept + constexpr MaybeUniquePtr(std::unique_ptr &&Owner) noexcept : MaybeUniquePtr(Owner.release(), true) {} - MaybeUniquePtr(MaybeUniquePtr &&Other) noexcept + constexpr MaybeUniquePtr(MaybeUniquePtr &&Other) noexcept : detail::MaybeUniquePtrBase( std::exchange(Other.Data, {})) {} - void swap(MaybeUniquePtr &Other) noexcept { std::swap(Data, Other.Data); } + constexpr void swap(MaybeUniquePtr &Other) noexcept { + std::swap(Data, Other.Data); + } - friend void swap(MaybeUniquePtr &LHS, MaybeUniquePtr &RHS) noexcept { + constexpr friend void swap(MaybeUniquePtr &LHS, + MaybeUniquePtr &RHS) noexcept { LHS.swap(RHS); } - MaybeUniquePtr &operator=(MaybeUniquePtr &&Other) noexcept { + constexpr MaybeUniquePtr &operator=(MaybeUniquePtr &&Other) noexcept { swap(Other); return *this; } - MaybeUniquePtr &operator=(std::unique_ptr &&Owner) noexcept { + constexpr MaybeUniquePtr &operator=(std::unique_ptr &&Owner) noexcept { if (owns()) { delete Data.getPointer(); } @@ -99,7 +97,7 @@ class MaybeUniquePtr : detail::MaybeUniquePtrBase { } template - MaybeUniquePtr &operator=(std::unique_ptr &&Owner) noexcept { + constexpr MaybeUniquePtr &operator=(std::unique_ptr &&Owner) noexcept { if (owns()) { delete Data.getPointer(); } @@ -110,24 +108,29 @@ class MaybeUniquePtr : detail::MaybeUniquePtrBase { MaybeUniquePtr(const MaybeUniquePtr &) = delete; MaybeUniquePtr &operator=(const MaybeUniquePtr &) = delete; - ~MaybeUniquePtr() { +#if __cplusplus >= 202002L + constexpr +#endif + ~MaybeUniquePtr() { if (owns()) { delete Data.getPointer(); Data = {}; } } - [[nodiscard]] T *get() noexcept { return Data.getPointer(); } - [[nodiscard]] const T *get() const noexcept { return Data.getPointer(); } + [[nodiscard]] constexpr T *get() noexcept { return Data.getPointer(); } + [[nodiscard]] constexpr const T *get() const noexcept { + return Data.getPointer(); + } - [[nodiscard]] T *operator->() noexcept { return get(); } - [[nodiscard]] const T *operator->() const noexcept { return get(); } + [[nodiscard]] constexpr T *operator->() noexcept { return get(); } + [[nodiscard]] constexpr const T *operator->() const noexcept { return get(); } - [[nodiscard]] T &operator*() noexcept { + [[nodiscard]] constexpr T &operator*() noexcept { assert(get() != nullptr); return *get(); } - [[nodiscard]] const T &operator*() const noexcept { + [[nodiscard]] constexpr const T &operator*() const noexcept { assert(get() != nullptr); return *get(); } @@ -137,45 +140,48 @@ class MaybeUniquePtr : detail::MaybeUniquePtrBase { return Data.getPointer(); } - void reset() noexcept { + constexpr void reset() noexcept { if (owns()) { delete Data.getPointer(); } Data = {}; } - [[nodiscard]] bool owns() const noexcept { + [[nodiscard]] constexpr bool owns() const noexcept { return Data.getInt() && Data.getPointer(); } - friend bool operator==(const MaybeUniquePtr &LHS, - const MaybeUniquePtr &RHS) noexcept { + constexpr friend bool operator==(const MaybeUniquePtr &LHS, + const MaybeUniquePtr &RHS) noexcept { return LHS.Data.getPointer() == RHS.Data.getPointer(); } - friend bool operator!=(const MaybeUniquePtr &LHS, - const MaybeUniquePtr &RHS) noexcept { + constexpr friend bool operator!=(const MaybeUniquePtr &LHS, + const MaybeUniquePtr &RHS) noexcept { return !(LHS == RHS); } - friend bool operator==(const MaybeUniquePtr &LHS, const T *RHS) noexcept { + constexpr friend bool operator==(const MaybeUniquePtr &LHS, + const T *RHS) noexcept { return LHS.Data.getPointer() == RHS; } - friend bool operator!=(const MaybeUniquePtr &LHS, const T *RHS) noexcept { + constexpr friend bool operator!=(const MaybeUniquePtr &LHS, + const T *RHS) noexcept { return !(LHS == RHS); } - friend bool operator==(const T *LHS, const MaybeUniquePtr &RHS) noexcept { + constexpr friend bool operator==(const T *LHS, + const MaybeUniquePtr &RHS) noexcept { return LHS == RHS.Data.getPointer(); } - friend bool operator!=(const T *LHS, const MaybeUniquePtr &RHS) noexcept { + constexpr friend bool operator!=(const T *LHS, + const MaybeUniquePtr &RHS) noexcept { return !(LHS == RHS); } - explicit operator bool() const noexcept { + constexpr explicit operator bool() const noexcept { return Data.getPointer() != nullptr; } }; - } // namespace psr #endif // PHASAR_UTILS_MAYBEUNIQUEPTR_H_ diff --git a/include/phasar/Utils/RepeatIterator.h b/include/phasar/Utils/RepeatIterator.h new file mode 100644 index 0000000000..94245930a1 --- /dev/null +++ b/include/phasar/Utils/RepeatIterator.h @@ -0,0 +1,84 @@ +/****************************************************************************** + * 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_REPEATITERATOR_H +#define PHASAR_UTILS_REPEATITERATOR_H + +#include "phasar/Utils/TypeTraits.h" + +#include "llvm/ADT/iterator_range.h" + +#include +#include +#include +#include + +namespace psr { +/// An iterator that iterates over the same value a specified number of times +template class RepeatIterator { +public: + using value_type = T; + using reference = const T &; + using pointer = const T *; + using difference_type = ptrdiff_t; + using iterator_category = std::forward_iterator_tag; + + reference operator*() const noexcept { + assert(Elem.has_value() && "Dereferencing end()-iterator"); + return *Elem; + } + pointer operator->() const noexcept { + assert(Elem.has_value() && "Dereferencing end()-iterator"); + return &*Elem; + } + + RepeatIterator &operator++() noexcept { + ++Index; + return *this; + } + RepeatIterator operator++(int) noexcept { + auto Ret = *this; + ++*this; + return Ret; + } + + bool operator==(const RepeatIterator &Other) const noexcept { + return Other.Index == Index; + } + bool operator!=(const RepeatIterator &Other) const noexcept { + return !(*this == Other); + } + + template >>> + explicit RepeatIterator(TT &&Elem) : Elem(std::forward(Elem)) {} + explicit RepeatIterator(size_t Index, std::true_type /*AsEndIterator*/) + : Index(Index), Elem(std::nullopt) {} + + RepeatIterator() noexcept = default; + +private: + size_t Index{}; + std::optional Elem{}; +}; + +template +using RepeatRangeType = llvm::iterator_range>; +template auto repeat(T &&Elem, size_t Num) { + using iterator_type = RepeatIterator>; + auto Ret = llvm::make_range(iterator_type(std::forward(Elem)), + iterator_type(Num, std::true_type{})); + return Ret; +} + +static_assert(is_iterable_over_v, int>); + +} // namespace psr + +#endif // PHASAR_UTILS_REPEATITERATOR_H diff --git a/include/phasar/Utils/StableVector.h b/include/phasar/Utils/StableVector.h index 68102efd37..12c18853ec 100644 --- a/include/phasar/Utils/StableVector.h +++ b/include/phasar/Utils/StableVector.h @@ -21,6 +21,7 @@ #include #include #include +#include namespace psr { @@ -153,20 +154,21 @@ class StableVector { using allocator_type = typename std::allocator_traits::template rebind_alloc; - StableVector(const allocator_type &Alloc = allocator_type()) noexcept( + StableVector() noexcept( + std::is_nothrow_default_constructible_v) = default; + + StableVector(const allocator_type &Alloc) noexcept( std::is_nothrow_copy_constructible_v) : Alloc(Alloc) {} StableVector(StableVector &&Other) noexcept - : Blocks(std::move(Other.Blocks)), Start(Other.Start), Pos(Other.Pos), - End(Other.End), Size(Other.Size), BlockIdx(Other.BlockIdx), - Alloc(std::move(Other.Alloc)) { - Other.Start = nullptr; - Other.Pos = nullptr; - Other.End = nullptr; - Other.Size = 0; - Other.BlockIdx = 0; - } + : Blocks(std::move(Other.Blocks)), + Start(std::exchange(Other.Start, nullptr)), + Pos(std::exchange(Other.Pos, nullptr)), + End(std::exchange(Other.End, nullptr)), + Size(std::exchange(Other.Size, 0)), + BlockIdx(std::exchange(Other.BlockIdx, 0)), + Alloc(std::move(Other.Alloc)) {} explicit StableVector(const StableVector &Other) : Size(Other.Size), BlockIdx(Other.BlockIdx), @@ -470,24 +472,16 @@ class StableVector { size_t Total = InitialCapacity; for (size_t I = 0; I < LHS.BlockIdx; ++I) { - for (T *LIt = LHS.Blocks[I], *RIt = RHS.Blocks[I], *LEnd = LIt + Cap; - LIt != LEnd; ++LIt, ++RIt) { - if (*LIt != *RIt) { - return false; - } + auto LIt = LHS.Blocks[I]; + if (!std::equal(LIt, LIt + Cap, RHS.Blocks[I])) { + return false; } Cap = Total; Total <<= 1; } - for (T *LIt = LHS.Start, *RIt = RHS.Start, *LEnd = LHS.Pos; LIt != LEnd; - ++LIt, ++RIt) { - if (*LIt != *RIt) { - return false; - } - } - return true; + return std::equal(LHS.Start, LHS.Pos, RHS.Start); } [[nodiscard]] friend bool operator!=(const StableVector &LHS, @@ -553,13 +547,13 @@ class StableVector { // return Blocks[LogIdx][Offset]; } - llvm::SmallVector Blocks; + llvm::SmallVector Blocks{}; T *Start = nullptr; T *Pos = nullptr; T *End = nullptr; size_t Size = 0; size_t BlockIdx = 0; - [[no_unique_address]] allocator_type Alloc; + [[no_unique_address]] allocator_type Alloc{}; }; // NOLINTEND(readability-identifier-naming) diff --git a/include/phasar/Utils/TypeTraits.h b/include/phasar/Utils/TypeTraits.h index d3022d72c6..e954dd14e6 100644 --- a/include/phasar/Utils/TypeTraits.h +++ b/include/phasar/Utils/TypeTraits.h @@ -10,6 +10,7 @@ #ifndef PHASAR_UTILS_TYPETRAITS_H #define PHASAR_UTILS_TYPETRAITS_H +#include "llvm/ADT/STLExtras.h" #include "llvm/Support/raw_ostream.h" #include @@ -33,19 +34,19 @@ namespace detail { template struct is_iterable : std::false_type {}; // NOLINT template -struct is_iterable().begin()), - decltype(std::declval().end())>> : std::true_type { -}; +struct is_iterable())), + decltype(llvm::adl_end(std::declval()))>> + : public std::true_type {}; + template struct is_iterable_over : std::false_type {}; // NOLINT template struct is_iterable_over< T, U, - std::enable_if_t< - is_iterable::value && - std::is_convertible_v().begin()), U>>> - : std::true_type {}; + std::enable_if_t::value && + std::is_same_v()))>>>> + : public std::true_type {}; template struct is_pair : std::false_type {}; // NOLINT template diff --git a/include/phasar/Utils/Utilities.h b/include/phasar/Utils/Utilities.h index 5bc01ecd21..ec4f26cd06 100644 --- a/include/phasar/Utils/Utilities.h +++ b/include/phasar/Utils/Utilities.h @@ -257,6 +257,32 @@ auto remove_by_index(Container &Cont, const Indices &Idx) { return remove_by_index(begin(Cont), end(Cont), begin(Idx), end(Idx)); } +/// See https://en.cppreference.com/w/cpp/utility/forward_like +template +[[nodiscard]] constexpr auto &&forward_like(U &&X) noexcept { // NOLINT + // NOLINTNEXTLINE + constexpr bool is_adding_const = std::is_const_v>; + if constexpr (std::is_lvalue_reference_v) { + if constexpr (is_adding_const) { + return std::as_const(X); + } else { + return static_cast(X); + } + } else { + if constexpr (is_adding_const) { + return std::move(std::as_const(X)); + } else { + return std::move(X); // NOLINT + } + } +} + +struct identity { + template decltype(auto) operator()(T &&Val) const noexcept { + return std::forward(Val); + } +}; + template >> llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const std::optional &Opt) { diff --git a/lib/PhasarLLVM/DataFlow/CMakeLists.txt b/lib/PhasarLLVM/DataFlow/CMakeLists.txt index 509a22b31b..3af5da4864 100644 --- a/lib/PhasarLLVM/DataFlow/CMakeLists.txt +++ b/lib/PhasarLLVM/DataFlow/CMakeLists.txt @@ -1,2 +1,3 @@ add_subdirectory(IfdsIde) add_subdirectory(Mono) +add_subdirectory(PathSensitivity) diff --git a/lib/PhasarLLVM/DataFlow/PathSensitivity/CMakeLists.txt b/lib/PhasarLLVM/DataFlow/PathSensitivity/CMakeLists.txt new file mode 100644 index 0000000000..1cbe6a3f6f --- /dev/null +++ b/lib/PhasarLLVM/DataFlow/PathSensitivity/CMakeLists.txt @@ -0,0 +1,44 @@ +file(GLOB_RECURSE PATHSENSITIVITY_SRC *.h *.cpp) + +if(NOT PHASAR_USE_Z3) + message("Not compiling LLVMPathConstraints.cpp since Z3 is disabled.") + # get_filename_component(LLVMPathConstraints_src LLVMPathConstraints.cpp ABSOLUTE) + # list(REMOVE_ITEM PATHSENSITIVITY_SRC ${LLVMPathConstraints_src}) + + + get_filename_component(Z3BasedPathSensitvityManager_src Z3BasedPathSensitvityManager.cpp ABSOLUTE) + # message("Not compiling ${Z3BasedPathSensitvityManager_src} since Z3 is disabled.") + # list(REMOVE_ITEM PATHSENSITIVITY_SRC ${Z3BasedPathSensitvityManager_src}) + + set(PATHSENSITIVITY_SRC + PathSensitivityManagerBase.cpp + ) + + message("Remaining PathSensitivity targets to build: ${PATHSENSITIVITY_SRC}") +endif() + + +if(PHASAR_USE_Z3) + set(ADDITIONAL_LINK_LIBS z3) +endif() + +add_phasar_library(phasar_llvm_pathsensitivity + ${PATHSENSITIVITY_SRC} + + LINKS + phasar_config + phasar_controlflow + phasar_llvm_controlflow + phasar_utils + phasar_llvm_utils + phasar_pointer + phasar_llvm_pointer + + LLVM_LINK_COMPONENTS + Core + Support + + LINK_PUBLIC + nlohmann_json::nlohmann_json + ${ADDITIONAL_LINK_LIBS} +) diff --git a/lib/PhasarLLVM/DataFlow/PathSensitivity/LLVMPathConstraints.cpp b/lib/PhasarLLVM/DataFlow/PathSensitivity/LLVMPathConstraints.cpp new file mode 100644 index 0000000000..9ea5c94fcc --- /dev/null +++ b/lib/PhasarLLVM/DataFlow/PathSensitivity/LLVMPathConstraints.cpp @@ -0,0 +1,659 @@ +#include "phasar/PhasarLLVM/DataFlow/PathSensitivity/LLVMPathConstraints.h" + +#include "phasar/PhasarLLVM/ControlFlow/LLVMBasedCFG.h" +#include "phasar/PhasarLLVM/Utils/LLVMShorthands.h" + +#include "llvm/Demangle/Demangle.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" + +namespace psr { +LLVMPathConstraints::LLVMPathConstraints(z3::context *Z3Ctx, + bool IgnoreDebugInstructions) + : Z3Ctx(Z3Ctx), IgnoreDebugInstructions(IgnoreDebugInstructions) { + if (!Z3Ctx) { + this->Z3Ctx = std::make_unique(); + } + Z3_set_ast_print_mode(getContext(), + Z3_ast_print_mode::Z3_PRINT_SMTLIB2_COMPLIANT); +} + +auto LLVMPathConstraints::internalGetConstraintAndVariablesFromEdge( + const llvm::Instruction *From, const llvm::Instruction *To) + -> std::optional { + LLVMBasedCFG CF(IgnoreDebugInstructions); + const auto *BI = llvm::dyn_cast(From); + if (!BI || !BI->isConditional()) { + return std::nullopt; + } + + if (IgnoreDebugInstructions) { + while (const auto *Prev = To->getPrevNonDebugInstruction(false)) { + To = Prev; + } + } else { + while (const auto *Prev = To->getPrevNode()) { + To = Prev; + } + } + + if (CF.isBranchTarget(From, To)) { + return handleCondBrInst(BI, To); + } + + return std::nullopt; +} + +std::optional +LLVMPathConstraints::getConstraintFromEdge(const llvm::Instruction *Curr, + const llvm::Instruction *Succ) { + if (auto CV = internalGetConstraintAndVariablesFromEdge(Curr, Succ)) { + return CV->Constraint; + } + + return std::nullopt; +} + +auto LLVMPathConstraints::getConstraintAndVariablesFromEdge( + const llvm::Instruction *Curr, const llvm::Instruction *Succ) + -> std::optional { + auto CV = internalGetConstraintAndVariablesFromEdge(Curr, Succ); + if (CV) { + /// Deduplicate the Variables vector + std::sort(CV->Variables.begin(), CV->Variables.end()); + CV->Variables.erase(std::unique(CV->Variables.begin(), CV->Variables.end()), + CV->Variables.end()); + } + + return CV; +} + +// void LLVMPathConstraints::getConstraintsInPath( +// llvm::ArrayRef Path, +// llvm::SmallVectorImpl &Dest) { +// LLVMBasedCFG CF(IgnoreDebugInstructions); +// for (size_t Idx = 0; Idx < Path.size(); ++Idx) { +// const llvm::Instruction *I = Path[Idx]; +// // handle non-loop flows and collect branch conditions +// const auto *BI = llvm::dyn_cast(I); +// if (!BI || !BI->isConditional()) { +// continue; +// } + +// // llvm::errs() << "Conditional branch on path: " << *BI << '\n'; +// if (Idx + 1 == Path.size()) { +// // llvm::errs() << "> skip: last\n"; +// continue; +// } + +// if (CF.isBranchTarget(I, Path[Idx + 1])) { +// // llvm::errs() << "> add to solver\n"; +// Dest.push_back(handleCondBrInst(BI, Path[Idx + 1]).Constraint); +// } +// // else { +// // llvm::errs() << "> skip: no target: " << *Path[Idx + 1] << '\n'; +// // } +// } +// } + +auto LLVMPathConstraints::handlePhiInstruction(const llvm::PHINode *Phi) + -> ConstraintAndVariables { + auto Search = Z3Expr.find(Phi); + if (Search != Z3Expr.end()) { + return Search->second; + } + const auto *Ty = Phi->getType(); + auto TyConstraints = [&]() { + std::string Name = "PHI"; + if (const auto *IntTy = llvm::dyn_cast(Ty)) { + auto NumBits = IntTy->getBitWidth(); + // case of bool + if (NumBits == 1) { + return Z3Ctx->bool_const(Name.c_str()); + } + // other integers + return Z3Ctx->int_const(Name.c_str()); + } + // case of float types + if (Ty->isFloatTy() || Ty->isDoubleTy()) { + return Z3Ctx->real_const(Name.c_str()); + } + if (Ty->isPointerTy()) { + /// Treat pointers as integers... + return Z3Ctx->bv_const(Name.c_str(), 64); + } + llvm::report_fatal_error("unhandled type of PHI node!"); + }(); + ConstraintAndVariables CAV{Z3Ctx->bool_val(true), {}}; + for (const auto &Incoming : Phi->incoming_values()) { + if (const auto *ConstInt = llvm::dyn_cast(Incoming)) { + if (ConstInt->isOne()) { + CAV.Constraint = CAV.Constraint || Z3Ctx->bool_val(true); + } else if (ConstInt->isZero()) { + CAV.Constraint = CAV.Constraint || Z3Ctx->bool_val(false); + } else { + CAV.Constraint = CAV.Constraint || TyConstraints; + } + } else if (const auto *Load = llvm::dyn_cast(Incoming)) { + auto Ret = getLoadInstAsZ3(Load); + CAV.Constraint = CAV.Constraint || Ret.Constraint; + CAV.Variables.append(Ret.Variables.begin(), Ret.Variables.end()); + } else if (const auto *Call = llvm::dyn_cast(Incoming)) { + auto Ret = getFunctionCallAsZ3(Call); + CAV.Constraint = CAV.Constraint || Ret.Constraint; + CAV.Variables.append(Ret.Variables.begin(), Ret.Variables.end()); + } else if (const auto *Cmp = llvm::dyn_cast(Incoming)) { + auto Ret = handleCmpInst(Cmp); + CAV.Constraint = CAV.Constraint || Ret.Constraint; + CAV.Variables.append(Ret.Variables.begin(), Ret.Variables.end()); + } else { + llvm::outs() << "unhanled phi value: " << *Incoming << '\n'; + llvm::outs().flush(); + llvm::report_fatal_error("unhanled incoming value in PHI node!"); + } + } + return Z3Expr.try_emplace(Phi, CAV).first->second; +} + +auto LLVMPathConstraints::handleCondBrInst(const llvm::BranchInst *Br, + const llvm::Instruction *Succ) + -> ConstraintAndVariables { + // llvm::outs() << "handleCondBrInst\n"; + auto Search = Z3Expr.find(Br); + if (Search != Z3Expr.end()) { + return Search->second; + } + const auto *Cond = Br->getCondition(); + // yes, the true label is indeed operand 2 + const auto *IfTrue = llvm::dyn_cast(Br->getOperand(2)); + const auto *IfFalse = llvm::dyn_cast(Br->getOperand(1)); + + auto GetFirstInst = [IgnoreDebugInstructions{IgnoreDebugInstructions}]( + const llvm::BasicBlock *BB) { + const auto *Ret = &BB->front(); + if (IgnoreDebugInstructions && llvm::isa(Ret)) { + Ret = Ret->getNextNonDebugInstruction(false); + } + return Ret; + }; + + if (const auto *Cmp = llvm::dyn_cast(Cond)) { + if (IfTrue && GetFirstInst(IfTrue) == Succ) { + return handleCmpInst(Cmp); + } + if (IfFalse && GetFirstInst(IfFalse) == Succ) { + auto Ret = handleCmpInst(Cmp); + Ret.Constraint = !Ret.Constraint; + return Ret; + } + } + if (const auto *BinOp = llvm::dyn_cast(Cond)) { + if (IfTrue && GetFirstInst(IfTrue) == Succ) { + return handleBinaryOperator(BinOp); + } + if (IfFalse && GetFirstInst(IfFalse) == Succ) { + auto Ret = handleBinaryOperator(BinOp); + Ret.Constraint = !Ret.Constraint; + return Ret; + } + } + if (const auto *CallSite = llvm::dyn_cast(Cond)) { + if (IfTrue && GetFirstInst(IfTrue) == Succ) { + return getFunctionCallAsZ3(CallSite); + } + if (IfFalse && GetFirstInst(IfFalse) == Succ) { + auto Ret = getFunctionCallAsZ3(CallSite); + Ret.Constraint = !Ret.Constraint; + return Ret; + } + } + // Dirty HACK + if (const auto *Trunc = llvm::dyn_cast(Cond)) { + if (Trunc->getDestTy()->isIntegerTy(1)) { + if (const auto *FromLoad = + llvm::dyn_cast(Trunc->getOperand(0))) { + auto Ret = getLoadInstAsZ3(FromLoad); + Ret.Constraint = (Ret.Constraint % 2 == 1); + return Ret; + } + } + } + if (const auto *Phi = llvm::dyn_cast(Cond)) { + return handlePhiInstruction(Phi); + } + llvm::report_fatal_error( + llvm::StringRef("unhandled conditional branch instruction: '") + + llvmIRToString(Br) + "'!\n"); +} + +auto LLVMPathConstraints::handleCmpInst(const llvm::CmpInst *Cmp) + -> ConstraintAndVariables { + // llvm::outs() << "handleCmpInst\n"; + auto Search = Z3Expr.find(Cmp); + if (Search != Z3Expr.end()) { + return Search->second; + } + const auto *Lhs = Cmp->getOperand(0); + const auto *Rhs = Cmp->getOperand(1); + + auto HandleOperand = [this](const llvm::Value *Op) { + if (const auto *Cast = llvm::dyn_cast(Op)) { + Op = Cast->getOperand(0); + } + + if (const auto *ConstData = llvm::dyn_cast(Op)) { + return getLiteralAsZ3(ConstData); + } + if (const auto *Load = llvm::dyn_cast(Op)) { + if (const auto *Alloca = + llvm::dyn_cast(Load->getPointerOperand())) { + return getAllocaInstAsZ3(Alloca); + } + return getLoadInstAsZ3(Load); + } + if (const auto *BinOpLhs = llvm::dyn_cast(Op)) { + return handleBinaryOperator(BinOpLhs); + } + if (const auto *CallSite = llvm::dyn_cast(Op)) { + return getFunctionCallAsZ3(CallSite); + } + if (const auto *Gep = llvm::dyn_cast(Op)) { + return getGEPInstAsZ3(Gep); + } + llvm::report_fatal_error("unhandled operand: " + + llvm::Twine(llvmIRToString(Op))); + }; + + auto LhsZ3Expr = HandleOperand(Lhs); + auto RhsZ3Expr = HandleOperand(Rhs); + LhsZ3Expr.Variables.append(RhsZ3Expr.Variables); + + switch (Cmp->getPredicate()) { + // Opcode U L G E Intuitive operation + case llvm::CmpInst::Predicate::FCMP_FALSE: ///< 0 0 0 0 Always false + ///< (always folded) + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_OEQ: ///< 0 0 0 1 True if ordered and + ///< equal + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_OGT: ///< 0 0 1 0 True if ordered and + ///< greater than + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_OGE: ///< 0 0 1 1 True if ordered and + ///< greater than or equal + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_OLT: ///< 0 1 0 0 True if ordered and + ///< less than + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_OLE: ///< 0 1 0 1 True if ordered and + ///< less than or equal + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_ONE: ///< 0 1 1 0 True if ordered and + ///< operands are unequal + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_ORD: ///< 0 1 1 1 True if ordered (no + ///< nans) + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_UNO: ///< 1 0 0 0 True if unordered: + ///< isnan(X) | isnan(Y) + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_UEQ: ///< 1 0 0 1 True if unordered or + ///< equal + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_UGT: ///< 1 0 1 0 True if unordered or + ///< greater than + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_UGE: ///< 1 0 1 1 True if unordered, + ///< greater than, or equal + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_ULT: ///< 1 1 0 0 True if unordered or + ///< less than + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_ULE: ///< 1 1 0 1 True if unordered, + ///< less than, or equal + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_UNE: ///< 1 1 1 0 True if unordered or + ///< not equal + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::FCMP_TRUE: ///< 1 1 1 1 Always true (always + ///< folded) + llvm::report_fatal_error("unhandled predicate!"); + break; + case llvm::CmpInst::Predicate::ICMP_EQ: ///< equal + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint == RhsZ3Expr.Constraint; + break; + case llvm::CmpInst::Predicate::ICMP_NE: ///< not equal + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint != RhsZ3Expr.Constraint; + break; + case llvm::CmpInst::Predicate::ICMP_UGT: ///< unsigned greater than + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint > RhsZ3Expr.Constraint; + break; + case llvm::CmpInst::Predicate::ICMP_UGE: ///< unsigned greater or equal + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint >= RhsZ3Expr.Constraint; + break; + case llvm::CmpInst::Predicate::ICMP_ULT: ///< unsigned less than + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint < RhsZ3Expr.Constraint; + break; + case llvm::CmpInst::Predicate::ICMP_ULE: ///< unsigned less or equal + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint <= RhsZ3Expr.Constraint; + break; + case llvm::CmpInst::Predicate::ICMP_SGT: ///< signed greater than + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint > RhsZ3Expr.Constraint; + break; + case llvm::CmpInst::Predicate::ICMP_SGE: ///< signed greater or equal + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint >= RhsZ3Expr.Constraint; + break; + case llvm::CmpInst::Predicate::ICMP_SLT: ///< signed less than + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint < RhsZ3Expr.Constraint; + break; + case llvm::CmpInst::Predicate::ICMP_SLE: ///< signed less or equal + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint <= RhsZ3Expr.Constraint; + break; + default: + llvm::report_fatal_error("unhandled predicate!"); + break; + } + + return LhsZ3Expr; +} + +auto LLVMPathConstraints::handleBinaryOperator( + const llvm::BinaryOperator *BinOp) -> ConstraintAndVariables { + auto Search = Z3Expr.find(BinOp); + if (Search != Z3Expr.end()) { + return Search->second; + } + const auto *Lhs = BinOp->getOperand(0); + const auto *Rhs = BinOp->getOperand(1); + + auto HandleOperand = [this](const llvm::Value *Op) { + if (const auto *Cast = llvm::dyn_cast(Op)) { + Op = Cast->getOperand(0); + } + + if (const auto *ConstData = llvm::dyn_cast(Op)) { + return getLiteralAsZ3(ConstData); + } + if (const auto *Load = llvm::dyn_cast(Op)) { + if (const auto *Alloca = + llvm::dyn_cast(Load->getPointerOperand())) { + return getAllocaInstAsZ3(Alloca); + } + return getLoadInstAsZ3(Load); + } + if (const auto *BinOpLhs = llvm::dyn_cast(Op)) { + return handleBinaryOperator(BinOpLhs); + } + if (const auto *CallSite = llvm::dyn_cast(Op)) { + return getFunctionCallAsZ3(CallSite); + } + llvm::report_fatal_error("unhandled operand: " + + llvm::Twine(llvmIRToString(Op))); + }; + + auto LhsZ3Expr = HandleOperand(Lhs); + auto RhsZ3Expr = HandleOperand(Rhs); + LhsZ3Expr.Variables.append(RhsZ3Expr.Variables); + + /// TODO: Once we have bitvectors, we must distinguish between signed and + /// unsigned div/rem operations! + + switch (BinOp->getOpcode()) { + case llvm::Instruction::BinaryOps::Add: + case llvm::Instruction::BinaryOps::FAdd: + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint + RhsZ3Expr.Constraint; + break; + case llvm::Instruction::BinaryOps::Sub: + case llvm::Instruction::BinaryOps::FSub: + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint - RhsZ3Expr.Constraint; + break; + case llvm::Instruction::BinaryOps::Mul: + case llvm::Instruction::BinaryOps::FMul: + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint * RhsZ3Expr.Constraint; + break; + case llvm::Instruction::BinaryOps::UDiv: + case llvm::Instruction::BinaryOps::SDiv: + case llvm::Instruction::BinaryOps::FDiv: + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint / RhsZ3Expr.Constraint; + break; + case llvm::Instruction::BinaryOps::URem: + case llvm::Instruction::BinaryOps::SRem: + case llvm::Instruction::BinaryOps::FRem: + LhsZ3Expr.Constraint = z3::rem(LhsZ3Expr.Constraint, RhsZ3Expr.Constraint); + break; + case llvm::Instruction::BinaryOps::Shl: // Shift left (logical) + LhsZ3Expr.Constraint = z3::shl(LhsZ3Expr.Constraint, RhsZ3Expr.Constraint); + break; + case llvm::Instruction::BinaryOps::LShr: // Shift right (logical) + LhsZ3Expr.Constraint = z3::lshr(LhsZ3Expr.Constraint, RhsZ3Expr.Constraint); + break; + case llvm::Instruction::BinaryOps::AShr: // Shift right (arithmetic) + LhsZ3Expr.Constraint = z3::ashr(LhsZ3Expr.Constraint, RhsZ3Expr.Constraint); + break; + case llvm::Instruction::BinaryOps::And: + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint & RhsZ3Expr.Constraint; + break; + case llvm::Instruction::BinaryOps::Or: + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint | RhsZ3Expr.Constraint; + break; + case llvm::Instruction::BinaryOps::Xor: + LhsZ3Expr.Constraint = LhsZ3Expr.Constraint ^ RhsZ3Expr.Constraint; + break; + default: + llvm::report_fatal_error("unhandled binary opcode!"); + break; + } + + return Z3Expr.try_emplace(BinOp, LhsZ3Expr).first->second; +} + +static llvm::DILocalVariable *getDILocalVariable(const llvm::AllocaInst *A) { + const llvm::Function *Fun = A->getParent()->getParent(); + // Search for llvm.dbg.declare + for (const auto &BB : *Fun) { + for (const auto &I : BB) { + if (const auto *Dbg = llvm::dyn_cast(&I)) { + // found. is it for an AllocaInst? + if (auto *DbgAI = llvm::dyn_cast(Dbg->getAddress())) { + // is it for our AllocaInst? + if (DbgAI == A) { + if (llvm::DILocalVariable *VarMD = Dbg->getVariable()) { + return VarMD; + } + } + } + } + } + } + return nullptr; +} + +static llvm::StringRef getVarName(const llvm::AllocaInst *A) { + auto *VarMD = getDILocalVariable(A); + if (VarMD) { + return VarMD->getName(); + } + if (A->hasName()) { + return A->getName(); + } + return ""; +} + +auto LLVMPathConstraints::getAllocaInstAsZ3(const llvm::AllocaInst *Alloca) + -> ConstraintAndVariables { + auto Search = Z3Expr.find(Alloca); + if (Search != Z3Expr.end()) { + return Search->second; + } + std::string Name = getVarName(Alloca).str(); + const auto *Ty = Alloca->getAllocatedType(); + + if (const auto *IntTy = llvm::dyn_cast(Ty)) { + auto NumBits = IntTy->getBitWidth(); + // case of bool + if (NumBits == 1) { + auto BoolConst = Z3Ctx->bool_const(Name.c_str()); + return Z3Expr + .try_emplace(Alloca, ConstraintAndVariables{BoolConst, {Alloca}}) + .first->second; + } + // other integers + auto IntConst = Z3Ctx->int_const(Name.c_str()); + return Z3Expr + .try_emplace(Alloca, ConstraintAndVariables{IntConst, {Alloca}}) + .first->second; + } + // case of float types + if (Ty->isFloatTy() || Ty->isDoubleTy()) { + auto RealConst = Z3Ctx->real_const(Name.c_str()); + return Z3Expr + .try_emplace(Alloca, ConstraintAndVariables{RealConst, {Alloca}}) + .first->second; + } + if (Ty->isPointerTy()) { + /// Treat pointers as integers... + return Z3Expr + .try_emplace( + Alloca, + ConstraintAndVariables{Z3Ctx->bv_const(Name.c_str(), 64), {Alloca}}) + .first->second; + } + llvm::report_fatal_error( + "unsupported type: " + llvm::Twine(llvmTypeToString(Ty)) + " at " + + llvmIRToString(Alloca) + " in function " + + Alloca->getFunction()->getName().str()); +} + +auto LLVMPathConstraints::getLoadInstAsZ3(const llvm::LoadInst *Load) + -> ConstraintAndVariables { + auto Search = Z3Expr.find(Load); + if (Search != Z3Expr.end()) { + return Search->second; + } + if (const auto *Alloca = + llvm::dyn_cast(Load->getPointerOperand())) { + return getAllocaInstAsZ3(Alloca); + } + // do not follow GEP instructions + if (const auto *GEP = + llvm::dyn_cast(Load->getPointerOperand())) { + return getGEPInstAsZ3(GEP); + } + // track down alloca or GEP + llvm::SmallVector Worklist = {Load}; + while (!Worklist.empty()) { + const auto *WorkV = Worklist.pop_back_val(); + // llvm::outs() << "Load-Val: " << *WorkV << '\n'; + if (const auto *Alloca = llvm::dyn_cast(WorkV)) { + return getAllocaInstAsZ3(Alloca); + } + if (const auto *GEP = llvm::dyn_cast(WorkV)) { + return getGEPInstAsZ3(GEP); + } + if (const auto *Inst = llvm::dyn_cast(WorkV)) { + Worklist.append(Inst->op_begin(), Inst->op_end()); + } + } + llvm::report_fatal_error("unsupported load!"); +} + +auto LLVMPathConstraints::getGEPInstAsZ3(const llvm::GetElementPtrInst *GEP) + -> ConstraintAndVariables { + std::string Name = + (GEP->hasName()) ? GEP->getName().str() : "gep" + psr::getMetaDataID(GEP); + + /// TODO: Unify different GEPs of same memory locations + const auto *Ty = GEP->getResultElementType(); + if (const auto *IntTy = llvm::dyn_cast(Ty)) { + auto NumBits = IntTy->getBitWidth(); + // case of bool + if (NumBits == 1) { + auto BoolConst = Z3Ctx->bool_const(Name.c_str()); + return Z3Expr.try_emplace(GEP, ConstraintAndVariables{BoolConst, {GEP}}) + .first->second; + } + // other integers + auto IntConst = Z3Ctx->int_const(Name.c_str()); + // also add value constraints to the solver + // FIXME + // if (isSignedInteger(GEP)) { + // auto Range = IntConst >= std::numeric_limits::min() && + // IntConst <= std::numeric_limits::max(); + // Z3Solver.add(Range); + // } else if (isUnsignedInteger(GEP)) { + // Z3 only supports plain 'int' + // Z3Solver.add(Range); + // } + return Z3Expr.try_emplace(GEP, ConstraintAndVariables{IntConst, {GEP}}) + .first->second; + } + // case of float types + if (Ty->isFloatTy() || Ty->isDoubleTy()) { + auto RealConst = Z3Ctx->real_const(Name.c_str()); + return Z3Expr.try_emplace(GEP, ConstraintAndVariables{RealConst, {GEP}}) + .first->second; + } + // some other pointer, we can treat those as integers + if (const auto *PointerTy = + llvm::dyn_cast(GEP->getPointerOperandType())) { + auto PointerConst = Z3Ctx->bv_const(Name.c_str(), 64); + return Z3Expr.try_emplace(GEP, ConstraintAndVariables{PointerConst, {GEP}}) + .first->second; + } + llvm::report_fatal_error("unsupported GEP type!"); +} + +auto LLVMPathConstraints::getLiteralAsZ3(const llvm::Value *V) + -> ConstraintAndVariables { + if (const auto *CI = llvm::dyn_cast(V)) { + return {Z3Ctx->int_val(CI->getSExtValue()), {}}; + } + if (const auto *CF = llvm::dyn_cast(V)) { + return {Z3Ctx->fpa_val(CF->getValue().convertToDouble()), {}}; + } + if (llvm::isa(V)) { + return {Z3Ctx->bv_val(0, 64), {}}; + } + llvm::report_fatal_error("unhandled literal!"); +} + +auto LLVMPathConstraints::getFunctionCallAsZ3(const llvm::CallBase *CallSite) + -> ConstraintAndVariables { + if (const auto *Callee = CallSite->getCalledFunction()) { + if (Callee->hasName()) { + auto DemangledName = llvm::demangle(Callee->getName().str()); + const auto *ReturnTy = Callee->getReturnType(); + if (ReturnTy->isFloatingPointTy()) { + return {Z3Ctx->real_const(DemangledName.c_str()), {Callee}}; + } + if (ReturnTy->isIntegerTy()) { + // case of bool + if (ReturnTy->getIntegerBitWidth() == 1) { + return {Z3Ctx->bool_const(DemangledName.c_str()), {Callee}}; + } + return {Z3Ctx->int_const(DemangledName.c_str()), {Callee}}; + } + if (ReturnTy->isPointerTy()) { + return {Z3Ctx->bv_const(DemangledName.c_str(), 64), {Callee}}; + } + } + } + llvm::report_fatal_error("unhandled function call!"); +} + +} // namespace psr diff --git a/lib/PhasarLLVM/DataFlow/PathSensitivity/PathSensitivityManagerBase.cpp b/lib/PhasarLLVM/DataFlow/PathSensitivity/PathSensitivityManagerBase.cpp new file mode 100644 index 0000000000..413e95f2da --- /dev/null +++ b/lib/PhasarLLVM/DataFlow/PathSensitivity/PathSensitivityManagerBase.cpp @@ -0,0 +1,5 @@ +#include "phasar/DataFlow/PathSensitivity/PathSensitivityManagerBase.h" + +namespace psr { +template class PathSensitivityManagerBase; +} // namespace psr diff --git a/lib/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitivityManager.cpp b/lib/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitivityManager.cpp new file mode 100644 index 0000000000..801a8e10f1 --- /dev/null +++ b/lib/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitivityManager.cpp @@ -0,0 +1,580 @@ +#include "phasar/PhasarLLVM/DataFlow/PathSensitivity/LLVMPathConstraints.h" +#include "phasar/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitvityManager.h" +#include "phasar/PhasarLLVM/Utils/LLVMShorthands.h" +#include "phasar/Utils/Logger.h" + +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/Support/Casting.h" + +namespace psr { +z3::expr Z3BasedPathSensitivityManagerBase::filterOutUnreachableNodes( + graph_type &RevDAG, vertex_t Leaf, + const Z3BasedPathSensitivityConfig &Config, + LLVMPathConstraints &LPC) const { + + struct FilterContext { + llvm::BitVector Visited{}; + z3::expr True; + z3::expr False; + llvm::SmallVector NodeConstraints{}; + size_t Ctr = 0; + z3::solver Solver; + + explicit FilterContext(z3::context &Z3Ctx) + : True(Z3Ctx.bool_val(true)), False(Z3Ctx.bool_val(false)), + Solver(Z3Ctx) {} + } Ctx(LPC.getContext()); + + Ctx.Visited.resize(graph_traits_t::size(RevDAG)); + Ctx.NodeConstraints.resize(graph_traits_t::size(RevDAG), Ctx.True); + + size_t TotalNumEdges = 0; + for (auto I : graph_traits_t::vertices(RevDAG)) { + TotalNumEdges += graph_traits_t::outDegree(RevDAG, I); + } + + if (Config.AdditionalConstraint) { + Ctx.Solver.add(*Config.AdditionalConstraint); + } + + // NOLINTNEXTLINE(readability-identifier-naming) + auto doFilter = [&Ctx, &RevDAG, &LPC, Leaf](auto &doFilter, + vertex_t Vtx) -> z3::expr { + Ctx.Visited.set(Vtx); + z3::expr X = Ctx.True; + llvm::ArrayRef PartialPath = graph_traits_t::node(RevDAG, Vtx); + assert(!PartialPath.empty()); + + for (size_t I = PartialPath.size() - 1; I; --I) { + if (auto Constr = + LPC.getConstraintFromEdge(PartialPath[I], PartialPath[I - 1])) { + X = X && *Constr; + } + } + + llvm::SmallVector Ys; + + for (auto Iter = graph_traits_t::outEdges(RevDAG, Vtx).begin(); + Iter != graph_traits_t::outEdges(RevDAG, Vtx).end();) { + // NOLINTNEXTLINE(readability-qualified-auto, llvm-qualified-auto) + auto It = Iter++; + auto Edge = *It; + auto Adj = graph_traits_t::target(Edge); + if (!Ctx.Visited.test(Adj)) { + doFilter(doFilter, Adj); + } + Ctx.Solver.push(); + Ctx.Solver.add(X); + auto Y = Ctx.NodeConstraints[Adj]; + const auto &AdjPP = graph_traits_t::node(RevDAG, Adj); + assert(!AdjPP.empty()); + if (auto Constr = + LPC.getConstraintFromEdge(PartialPath.front(), AdjPP.back())) { + Y = Y && *Constr; + } + + Ctx.Solver.add(Y); + + auto Sat = Ctx.Solver.check(); + if (Sat == z3::check_result::unsat) { + Iter = graph_traits_t::removeEdge(RevDAG, Vtx, It); + Ctx.Ctr++; + } else { + Ys.push_back(std::move(Y)); + } + + Ctx.Solver.pop(); + // Idx++; + } + + if (graph_traits_t::outDegree(RevDAG, Vtx) == 0) { + return Ctx.NodeConstraints[Vtx] = Vtx == Leaf ? X : Ctx.False; + } + if (Ys.empty()) { + llvm_unreachable("Adj nonempty and Ys empty is unexpected"); + } + auto Y = Ys[0]; + for (const auto &Constr : llvm::makeArrayRef(Ys).drop_front()) { + Y = Y || Constr; + } + return Ctx.NodeConstraints[Vtx] = (X && Y).simplify(); + }; + + z3::expr Ret = LPC.getContext().bool_val(false); + + for (auto Iter = graph_traits_t::roots(RevDAG).begin(); + Iter != graph_traits_t::roots(RevDAG).end();) { + // NOLINTNEXTLINE(readability-qualified-auto, llvm-qualified-auto) + auto It = Iter++; + auto Rt = *It; + auto Res = doFilter(doFilter, Rt); + Ret = Ret || Res; + if (Rt != Leaf && RevDAG.Adj[Rt].empty()) { + // llvm::errs() << "> Remove root " << Rt << "\n"; + Iter = graph_traits_t::removeRoot(RevDAG, It); + } + } + + PHASAR_LOG_LEVEL_CAT(DEBUG, "PathSensitivityManager", + "> Filtered out " << Ctx.Ctr << " edges from the DAG"); + PHASAR_LOG_LEVEL_CAT(DEBUG, "PathSensitivityManager", + ">> " << (TotalNumEdges - Ctx.Ctr) + << " edges remaining"); + + return Ret.simplify(); +} + +/// This could be a C++20 concept! +struct PathFilter { + // void saveState(); + // void restoreState(); + // void saveEdge(n_t Prev, n_t Inst); + // bool isValid() const; + // bool saveFinalEdge(n_t Prev, n_t FinalInst); +}; + +template class PathFilterList : public std::tuple { +public: + using n_t = const llvm::Instruction *; + using std::tuple::tuple; + + void saveState() { saveStateImpl(std::make_index_sequence()); } + + void restoreState() { + restoreStateImpl(std::make_index_sequence()); + } + + void saveEdge(n_t Prev, n_t Inst) { + saveEdgeImpl(Prev, Inst, std::make_index_sequence()); + } + + [[nodiscard]] bool isValid() { + return isValidImpl(std::make_index_sequence()); + } + + bool saveFinalEdge(n_t Prev, n_t Inst) { + return saveFinalEdgeImpl(Prev, Inst, + std::make_index_sequence()); + } + +private: + template + void saveStateImpl(std::index_sequence /*unused*/) { + (std::get(*this).saveState(), ...); + } + template + void restoreStateImpl(std::index_sequence /*unused*/) { + (std::get(*this).restoreState(), ...); + } + template + void saveEdgeImpl(n_t Prev, n_t Inst, std::index_sequence /*unused*/) { + (std::get(*this).saveEdge(Prev, Inst), ...); + } + template + bool saveFinalEdgeImpl(n_t Prev, n_t Inst, + std::index_sequence /*unused*/) { + return (std::get(*this).saveFinalEdge(Prev, Inst) && ...); + } + template + bool isValidImpl(std::index_sequence /*unused*/) { + return (std::get(*this).isValid() && ...); + } +}; + +template +static PathFilterList makePathFilterList(T &&...Filters) { + return PathFilterList(std::forward(Filters)...); +} + +class CallStackPathFilter { +public: + using n_t = const llvm::Instruction *; + void saveState() { CallStackSafe.emplace_back(CallStackOwner.size(), TOS); } + + void restoreState() { + auto [SaveCallStackSize, CSSave] = CallStackSafe.pop_back_val(); + assert(CallStackOwner.size() >= SaveCallStackSize); + CallStackOwner.pop_back_n(CallStackOwner.size() - SaveCallStackSize); + TOS = CSSave; + Valid = true; + } + + void saveEdge(n_t Prev, n_t Inst) { + if (!Valid) { + return; + } + if (const auto *CS = llvm::dyn_cast(Prev); + CS && !isDirectSuccessorOf(Inst, CS)) { + PHASAR_LOG_LEVEL_CAT(DEBUG, "CallStackPathFilter", + "Push CS: " << llvmIRToString(CS)); + pushCS(CS); + + } else if (llvm::isa(Prev) || + llvm::isa(Prev)) { + /// Allow unbalanced returns + if (!emptyCS()) { + const auto *CS = popCS(); + + PHASAR_LOG_LEVEL_CAT(DEBUG, "CallStackPathFilter", + "Pop CS: " << llvmIRToString(CS) << " at exit " + << llvmIRToString(Prev) + << " and ret-site " + << llvmIRToString(Inst)); + + if (!isDirectSuccessorOf(Inst, CS)) { + /// Invalid return + Valid = false; + + PHASAR_LOG_LEVEL_CAT(DEBUG, "CallStackPathFilter", + "> Invalid return"); + } else { + PHASAR_LOG_LEVEL_CAT(DEBUG, "CallStackPathFilter", "> Valid return"); + } + } else { + PHASAR_LOG_LEVEL_CAT(DEBUG, "CallStackPathFilter", + "> Unbalanced return at exit " + << llvmIRToString(Prev)); + } + /// else: unbalanced return + } + } + + bool saveFinalEdge(n_t Prev, n_t FinalInst) { + if (!Valid) { + return false; + } + + if (Prev && (llvm::isa(Prev) || + llvm::isa(Prev))) { + if (!emptyCS() && !isDirectSuccessorOf(FinalInst, popCS())) { + /// Invalid return + return false; + } + } + return true; + } + + [[nodiscard]] bool isValid() const noexcept { return Valid; } + +private: + bool isDirectSuccessorOf(const llvm::Instruction *Succ, + const llvm::Instruction *Of) { + + while (const auto *Nxt = Of->getNextNode()) { + if (Nxt == Succ) { + return true; + } + Of = Nxt; + + if (Nxt->isTerminator()) { + break; + } + if (const auto *Call = llvm::dyn_cast(Nxt); + Call && Call->getCalledFunction() && + !Call->getCalledFunction()->isDeclaration()) { + /// Don't skip function calls. We might call the same fun twice in the + /// same BB, so we recognize invalid paths there as well! + return false; + } + } + + assert(Of->isTerminator()); + + return std::find_if(llvm::succ_begin(Of), llvm::succ_end(Of), + [&Succ](const llvm::BasicBlock *BB) { + return &BB->front() == Succ; + }) != llvm::succ_end(Of); + } + + void pushCS(const llvm::CallBase *CS) { + auto *NewNode = &CallStackOwner.emplace_back(); + NewNode->Prev = TOS; + NewNode->CS = CS; + TOS = NewNode; + } + + const llvm::CallBase *popCS() noexcept { + assert(TOS && "We should already have checked for nullness..."); + const auto *Ret = TOS->CS; + TOS = TOS->Prev; + /// Defer the deallocation, such that we still can rollback + return Ret; + } + + [[nodiscard]] bool emptyCS() const noexcept { return TOS == nullptr; } + + struct CallStackNode { + CallStackNode *Prev = nullptr; + const llvm::CallBase *CS = nullptr; + }; + /// Now, filter directly on the reversed DAG + + StableVector CallStackOwner; + llvm::SmallVector> CallStackSafe; + CallStackNode *TOS = nullptr; + bool Valid = true; +}; + +class ConstraintPathFilter { +public: + using n_t = const llvm::Instruction *; + + ConstraintPathFilter(LLVMPathConstraints &LPC, + const z3::expr &AdditionalConstraint, + size_t *CompletedCtr) noexcept + : LPC(LPC), Solver(LPC.getContext()), CompletedCtr(*CompletedCtr) { + Solver.add(AdditionalConstraint); + Solver.push(); + NumAtomsStack.push_back(0); + } + + void saveState() { + NumAtomsStack.push_back(NumAtomsStack.back()); + Solver.push(); + } + + void restoreState() { + Solver.pop(); + auto NumAtoms = NumAtomsStack.pop_back_val(); + assert(!NumAtomsStack.empty()); + auto Diff = NumAtoms - NumAtomsStack.back(); + for (size_t I = 0; I < Diff; ++I) { + SymbolicAtoms.pop_back(); + } + NeedSolverInvocation = false; + LocalAtoms.clear(); + Model = std::nullopt; + } + + void saveEdge(n_t Prev, n_t Inst) { + + if (auto ConstrAndVariables = + LPC.getConstraintAndVariablesFromEdge(Prev, Inst)) { + + Solver.add(ConstrAndVariables->Constraint); + + LocalAtoms.append(ConstrAndVariables->Variables); + } + } + + [[nodiscard]] bool isValid() { + ++IsValidCalls; + if (LocalAtoms.empty() && !NeedSolverInvocation) { + /// Nothing (new) to check + return true; + } + + if (!checkLocalAtomsOverlap()) { + return true; + } + + NeedSolverInvocation = false; + + auto Res = Solver.check(); + ++Ctr; +#ifdef DYNAMIC_LOG + if (Ctr % 10000 == 0) { + PHASAR_LOG_LEVEL_CAT(DEBUG, "PathSensitivityManager", + Ctr << " solver invocations so far..."); + PHASAR_LOG_LEVEL_CAT(DEBUG, "PathSensitivityManager", + ">> " << IsValidCalls << " calls to isValid()"); + PHASAR_LOG_LEVEL_CAT(DEBUG, "PathSensitivityManager", + ">> " << RejectedCtr << " paths rejected"); + PHASAR_LOG_LEVEL_CAT(DEBUG, "PathSensitivityManager", + ">> " << CompletedCtr << " paths completed"); + } +#endif + + auto Ret = Res != z3::check_result::unsat; + if (!Ret) { + ++RejectedCtr; + } else { + Model = Solver.get_model(); + } + + return Ret; + } + + bool saveFinalEdge(n_t Prev, n_t FinalInst) { + saveEdge(Prev, FinalInst); + NeedSolverInvocation = true; + return isValid(); + } + + z3::expr getPathConstraints() { + auto Vec = Solver.assertions(); + if (Vec.empty()) { + return LPC.getContext().bool_val(true); + } + + auto Ret = Vec[0]; + for (int I = 1, End = int(Vec.size()); I != End; ++I) { + Ret = Ret && Vec[I]; + } + return Ret.simplify(); + } + + z3::model getModel() { return Model.value(); } + + [[nodiscard]] size_t getNumSolverInvocations() const noexcept { return Ctr; } + +private: + [[nodiscard]] bool checkLocalAtomsOverlap() { + if (NeedSolverInvocation) { + return true; + } + + std::sort(LocalAtoms.begin(), LocalAtoms.end()); + LocalAtoms.erase(std::unique(LocalAtoms.begin(), LocalAtoms.end()), + LocalAtoms.end()); + size_t NumLocalAtoms = LocalAtoms.size(); + size_t OldSize = SymbolicAtoms.size(); + SymbolicAtoms.insert(LocalAtoms.begin(), LocalAtoms.end()); + size_t NewSize = SymbolicAtoms.size(); + LocalAtoms.clear(); + /// The newly added atoms don't overlap with the atoms from the + /// already seen constraints. So, there can be no contradicion (would + /// have already been filtered out in the previous step) + return NewSize - OldSize != NumLocalAtoms; + } + + LLVMPathConstraints &LPC; + z3::solver Solver; + llvm::SmallSetVector SymbolicAtoms; + llvm::SmallVector NumAtomsStack; + llvm::SmallVector LocalAtoms; + std::optional Model; + bool NeedSolverInvocation = false; + + size_t Ctr = 0; + size_t RejectedCtr = 0; + size_t IsValidCalls = 0; + size_t &CompletedCtr; +}; + +auto Z3BasedPathSensitivityManagerBase::filterAndFlattenRevDag( + graph_type &RevDAG, vertex_t Leaf, n_t FinalInst, + const Z3BasedPathSensitivityConfig &Config, LLVMPathConstraints &LPC) const + -> FlowPathSequence { + /// Here, we do the following: + /// - Traversing the ReverseDAG in a simple DFS order and maintaining the + /// exact path reaching the current node. + /// - On the fly constructing and updating a call-stack to regain + /// context-sensitivity by filtering out paths with invalid returns + /// - Similarly on the fly constructing and solving Z3 Path Constraints and + /// filtering out all paths with unsatisfiable constraints + /// - Saving all "surviving" paths that end at a leaf to the overall vector + /// that gets returned at the end + + /// Problem: We still have way too many Z3 solver invocations (> 900000 for + /// some small test programs) + /// Solution idea: In contrast to the context sensitivity check, the Path + /// constraints are context-independent. So, it might be beneficial to + /// compute the end-reachability constraints of each _node_ in a bottom-up + /// fashion leading to PathNodeOwner.size() solver invocations. We then + /// still need a subsequent DFS order traversal to collect all remaining + /// satisfiable paths, so there we can still apply the context-sensitivity + /// check OTF. + /// NOTE: This is implemented now in filterOutUnreachableNodes() + + FlowPathSequence Ret; + size_t CompletedCtr = 0; + auto Filters = makePathFilterList( + CallStackPathFilter{}, + ConstraintPathFilter{ + LPC, + Config.AdditionalConstraint.value_or(LPC.getContext().bool_val(true)), + &CompletedCtr}); + + llvm::SmallVector CurrPath; + + n_t Prev = nullptr; + + auto doFilter = [FinalInst, &Prev, &Filters, &RevDAG, &CurrPath, &Ret, + &CompletedCtr, MaxNumPaths{Config.NumPathsThreshold}, + Leaf](auto &doFilter, vertex_t Vtx) { + auto CurrPathSave = CurrPath.size(); + scope_exit RestoreCurrPath = [&CurrPath, CurrPathSave] { + assert(CurrPathSave <= CurrPath.size()); + CurrPath.resize(CurrPathSave); + }; + + const auto *PrevSave = Prev; + scope_exit RestorePrev = [PrevSave, &Prev] { Prev = PrevSave; }; + + Filters.saveState(); + scope_exit RestoreFilters = [&Filters] { Filters.restoreState(); }; + + for (const auto *Inst : llvm::reverse(graph_traits_t::node(RevDAG, Vtx))) { + CurrPath.push_back(Inst); + if (!Prev) { + Prev = Inst; + continue; + } + + Filters.saveEdge(Prev, Inst); + + Prev = Inst; + } + + if (Vtx == Leaf) { + // llvm::errs() << "> Reached Leaf!\n"; + + assert(!CurrPath.empty() && "Reported paths must not be empty!"); + + /// Reached the end + /// TODO: No need to add the final inst separately anymore. Now, it + /// has its own PathNode and is handled implicitly + if (Filters.saveFinalEdge(Prev, FinalInst)) { + auto Model = std::get<1>(Filters).getModel(); + Ret.emplace_back(CurrPath, std::get<1>(Filters).getPathConstraints(), + Model); + ++CompletedCtr; + } + + return; + } + if (graph_traits_t::outDegree(RevDAG, Vtx) == 0) { + llvm::report_fatal_error("Non-leaf node has no successors!"); + } + + if (CompletedCtr >= MaxNumPaths) { + return; + } + if (!Filters.isValid()) { + return; + } + /// TODO: Verify that we have no concurrent modification here and the + /// iterator is never dangling! + for (auto Edge : graph_traits_t::outEdges(RevDAG, Vtx)) { + doFilter(doFilter, graph_traits_t::target(Edge)); + } + }; + + for (auto Rt : graph_traits_t::roots(RevDAG)) { + doFilter(doFilter, Rt); + } + + PHASAR_LOG_LEVEL_CAT(DEBUG, "PathSensitivityManager", + "Num Solver invocations: " + << std::get<1>(Filters).getNumSolverInvocations()); + + return Ret; +} + +void Z3BasedPathSensitivityManagerBase::deduplicatePaths( + FlowPathSequence &Paths) { + /// Some kind of lexical sort for being able to deduplicate the paths easily + std::sort(Paths.begin(), Paths.end(), + [](const FlowPath &LHS, const FlowPath &RHS) { + return LHS.size() < RHS.size() || + (LHS.size() == RHS.size() && + std::lexicographical_compare(LHS.begin(), LHS.end(), + RHS.begin(), RHS.end())); + }); + + Paths.erase(std::unique(Paths.begin(), Paths.end()), Paths.end()); +} + +} // namespace psr diff --git a/lib/PhasarLLVM/Utils/LLVMShorthands.cpp b/lib/PhasarLLVM/Utils/LLVMShorthands.cpp index 62672afabd..1525668be3 100644 --- a/lib/PhasarLLVM/Utils/LLVMShorthands.cpp +++ b/lib/PhasarLLVM/Utils/LLVMShorthands.cpp @@ -177,6 +177,19 @@ std::string llvmIRToString(const llvm::Value *V) { return llvm::StringRef(IRBuffer).ltrim().str(); } +std::string llvmTypeToString(const llvm::Type *T) { + // WARNING: Expensive function, cause is the T->print(RSO) + // (20ms on a medium size code (phasar without debug) + // 80ms on a huge size code (clang without debug), + // can be multiplied by times 3 to 5 if passes are enabled) + std::string IRBuffer; + llvm::raw_string_ostream RSO(IRBuffer); + T->print(RSO); + RSO.flush(); + boost::trim_left(IRBuffer); + return IRBuffer; +} + std::string llvmIRToStableString(const llvm::Value *V) { if (!V) { return ""; diff --git a/test/llvm_test_code/path_tracing/CMakeLists.txt b/test/llvm_test_code/path_tracing/CMakeLists.txt new file mode 100644 index 0000000000..3a701b4770 --- /dev/null +++ b/test/llvm_test_code/path_tracing/CMakeLists.txt @@ -0,0 +1,32 @@ +set(PATH_TRACING_FILES + inter_01.cpp + inter_02.cpp + inter_03.cpp + inter_04.cpp + inter_05.cpp + inter_06.cpp + inter_07.cpp + inter_08.cpp + inter_09.cpp + inter_10.cpp + inter_11.cpp + inter_12.cpp + intra_01.cpp + intra_02.cpp + intra_03.cpp + intra_04.cpp + intra_05.cpp + intra_06.cpp + intra_07.cpp + intra_08.cpp + intra_09.cpp + other_01.cpp +) + +foreach(TEST_SRC ${PATH_TRACING_FILES}) + generate_ll_file(FILE ${TEST_SRC}) +endforeach(TEST_SRC) + +foreach(TEST_SRC ${PATH_TRACING_FILES}) + generate_ll_file(FILE ${TEST_SRC} DEBUG) +endforeach(TEST_SRC) diff --git a/test/llvm_test_code/path_tracing/inter_01.cpp b/test/llvm_test_code/path_tracing/inter_01.cpp new file mode 100644 index 0000000000..71b0801f97 --- /dev/null +++ b/test/llvm_test_code/path_tracing/inter_01.cpp @@ -0,0 +1,8 @@ +int increment(int I) { return ++I; } + +int main() { + int I = 42; + int J = I; + int K = increment(J); + return K; +} diff --git a/test/llvm_test_code/path_tracing/inter_02.cpp b/test/llvm_test_code/path_tracing/inter_02.cpp new file mode 100644 index 0000000000..2b5eedbbe5 --- /dev/null +++ b/test/llvm_test_code/path_tracing/inter_02.cpp @@ -0,0 +1,11 @@ +int increment(int I) { return ++I; } + +int compute(int I) { return (I + 42) * 2; } + +int main() { + int I = 42; + int J = I; + int K = compute(J); + K = increment(K); + return K; +} diff --git a/test/llvm_test_code/path_tracing/inter_03.cpp b/test/llvm_test_code/path_tracing/inter_03.cpp new file mode 100644 index 0000000000..1208186b3f --- /dev/null +++ b/test/llvm_test_code/path_tracing/inter_03.cpp @@ -0,0 +1,9 @@ +int increment(int I) { return ++I; } + +int main() { + int I = 42; + int J = I; + int K = increment(J); + int L = increment(K); + return L; +} diff --git a/test/llvm_test_code/path_tracing/inter_04.cpp b/test/llvm_test_code/path_tracing/inter_04.cpp new file mode 100644 index 0000000000..8402d65d05 --- /dev/null +++ b/test/llvm_test_code/path_tracing/inter_04.cpp @@ -0,0 +1,20 @@ +extern int someFunc(int L); + +int increment(int I) { return ++I; } + +int modify(int I) { + if (I < 90) { + return someFunc(I); + } else { + return increment(I); + } + return --I; +} + +int main() { + int I = 42; + int J = I; + int K = increment(J); + int L = modify(K); + return L; +} diff --git a/test/llvm_test_code/path_tracing/inter_05.cpp b/test/llvm_test_code/path_tracing/inter_05.cpp new file mode 100644 index 0000000000..d2ec590662 --- /dev/null +++ b/test/llvm_test_code/path_tracing/inter_05.cpp @@ -0,0 +1,29 @@ +#include +#include + +int *bar(int *Foo, int I) { + if (I > 10) { + return Foo; + } + return 0; +} + +void lorem(int I) { + if (I > 10) { + } +} + +int main(int Argc, char **Argv) { + int K = 0, J = 10; + int Z = Argc; + lorem(Z); + if (K == 0) { + J = 20; + } + int *Foo = &Z; + int M = *bar(Foo, Z); + if (M < 0) { + J = 42; + } + return J; +} diff --git a/test/llvm_test_code/path_tracing/inter_06.cpp b/test/llvm_test_code/path_tracing/inter_06.cpp new file mode 100644 index 0000000000..99e8c4ecd6 --- /dev/null +++ b/test/llvm_test_code/path_tracing/inter_06.cpp @@ -0,0 +1,9 @@ +int add(int A, int B) { return A + B; } + +int main(int Argc, char **Argv) { + int A = 42; + int B = A++; + int (*F)(int, int) = &add; + int C = F(A, B); + return C; +} diff --git a/test/llvm_test_code/path_tracing/inter_07.cpp b/test/llvm_test_code/path_tracing/inter_07.cpp new file mode 100644 index 0000000000..c7245ea57d --- /dev/null +++ b/test/llvm_test_code/path_tracing/inter_07.cpp @@ -0,0 +1,18 @@ +int add(int A, int B) { return A + B; } + +int sub(int A, int B) { return A - B; } + +int main(int Argc, char **Argv) { + int A = 42; + int B = A++; + int C; + if (Argc > 0) { + int (*F)(int, int) = &add; + C = F(A, B); + } else { + int (*F)(int, int) = ⊂ + C = F(A, B); + } + + return C; +} diff --git a/test/llvm_test_code/path_tracing/inter_08.cpp b/test/llvm_test_code/path_tracing/inter_08.cpp new file mode 100644 index 0000000000..cf3797a41d --- /dev/null +++ b/test/llvm_test_code/path_tracing/inter_08.cpp @@ -0,0 +1,31 @@ +int add(int A, int B) { + int C; + for (int I = 0; I < 12; I++) { + C = A + B; + } + return C; +} + +int sub(int A, int B) { + int C; + int I = 5; + while (I < 12) { + C = A + B; + I++; + } + return C; +} + +int main(int Argc, char **Argv) { + int A = 42; + int B = A++; + int C; + if (Argc > 0) { + int (*F)(int, int) = &add; + C = F(A, B); + } else { + int (*F)(int, int) = ⊂ + C = F(A, B); + } + return C; +} diff --git a/test/llvm_test_code/path_tracing/inter_09.cpp b/test/llvm_test_code/path_tracing/inter_09.cpp new file mode 100644 index 0000000000..710a21ae48 --- /dev/null +++ b/test/llvm_test_code/path_tracing/inter_09.cpp @@ -0,0 +1,11 @@ +unsigned recursion(unsigned i) { + if (i > 0) { + return recursion(i - 1); + } + return i; +} + +int main(int Argc, char **Argv) { + Argc = recursion(5); + return 0; +} diff --git a/test/llvm_test_code/path_tracing/inter_10.cpp b/test/llvm_test_code/path_tracing/inter_10.cpp new file mode 100644 index 0000000000..8b8e4a33a9 --- /dev/null +++ b/test/llvm_test_code/path_tracing/inter_10.cpp @@ -0,0 +1,15 @@ +#include + +int createInitialValue() { return 42; } + +int foo = createInitialValue(); + +int bar; + +__attribute__((constructor)) void myGlobalCtor() { bar = 45; } + +int main(int Argc, char **Argv) { + Argc = foo + 1; + int y = bar - 1; + return 0; +} diff --git a/test/llvm_test_code/path_tracing/inter_11.cpp b/test/llvm_test_code/path_tracing/inter_11.cpp new file mode 100644 index 0000000000..9628566c64 --- /dev/null +++ b/test/llvm_test_code/path_tracing/inter_11.cpp @@ -0,0 +1,16 @@ +struct One { + virtual int assignValue(int J) = 0; +}; + +struct Two : public One { + int assignValue(int J) override { return J + 1; } +}; + +struct Three : public One { + int assignValue(int J) override { return J + 2; } +}; + +int main(int Argc, char **Argv) { + One *O = new Two; + return O->assignValue(42); +} diff --git a/test/llvm_test_code/path_tracing/inter_12.cpp b/test/llvm_test_code/path_tracing/inter_12.cpp new file mode 100644 index 0000000000..b9fe519b0e --- /dev/null +++ b/test/llvm_test_code/path_tracing/inter_12.cpp @@ -0,0 +1,20 @@ +struct One { + virtual ~One() = default; + virtual int assignValue(int J) = 0; +}; + +struct Two : public One { + int assignValue(int J) override { return J + 1; } +}; + +struct Three : public One { + int assignValue(int J) override { return J + 2; } +}; + +int main(int Argc, char **Argv) { + One *O = new Two; + delete O; + O = new Three; + + return O->assignValue(42); +} diff --git a/test/llvm_test_code/path_tracing/intra_01.cpp b/test/llvm_test_code/path_tracing/intra_01.cpp new file mode 100644 index 0000000000..b275d50e4f --- /dev/null +++ b/test/llvm_test_code/path_tracing/intra_01.cpp @@ -0,0 +1,6 @@ +int main() { + int I = 13; + int J = 42; + int K = J + 9001; + return K; +} diff --git a/test/llvm_test_code/path_tracing/intra_02.cpp b/test/llvm_test_code/path_tracing/intra_02.cpp new file mode 100644 index 0000000000..b4411b86d3 --- /dev/null +++ b/test/llvm_test_code/path_tracing/intra_02.cpp @@ -0,0 +1,9 @@ +int main(int Argc, char **Argv) { + int I; + if (Argc > 24) { + I = 42; + } else { + I = 13; + } + return I; +} diff --git a/test/llvm_test_code/path_tracing/intra_03.cpp b/test/llvm_test_code/path_tracing/intra_03.cpp new file mode 100644 index 0000000000..c89956da1b --- /dev/null +++ b/test/llvm_test_code/path_tracing/intra_03.cpp @@ -0,0 +1,10 @@ +int main(int Argc, char **Argv) { + int I = Argc; + int J = I; + if (Argc > 1) { + J = 100; + } else { + I = 13; + } + return J; +} diff --git a/test/llvm_test_code/path_tracing/intra_04.cpp b/test/llvm_test_code/path_tracing/intra_04.cpp new file mode 100644 index 0000000000..f4cdbc7dff --- /dev/null +++ b/test/llvm_test_code/path_tracing/intra_04.cpp @@ -0,0 +1,13 @@ +int main(int Argc, char **Argv) { + int I = Argc; + int J = I; + if (Argc > 1) { + J = 100; + for (int Idx = 0; Idx < 1000; ++Idx) { + ++J; + } + } else { + I = 13; + } + return J; +} diff --git a/test/llvm_test_code/path_tracing/intra_05.cpp b/test/llvm_test_code/path_tracing/intra_05.cpp new file mode 100644 index 0000000000..a3eab5f04c --- /dev/null +++ b/test/llvm_test_code/path_tracing/intra_05.cpp @@ -0,0 +1,12 @@ +int main(int Argc, char **Argv) { + int I = 2000; + int J = 4000; + if (Argc > 1) { + I = 1; + J = 4; + } else { + I = 2; + J = 4; + } + return J; +} diff --git a/test/llvm_test_code/path_tracing/intra_06.cpp b/test/llvm_test_code/path_tracing/intra_06.cpp new file mode 100644 index 0000000000..0547c6bf28 --- /dev/null +++ b/test/llvm_test_code/path_tracing/intra_06.cpp @@ -0,0 +1,9 @@ +int main(int Argc, [[maybe_unused]] char **Argv) { + int I = 2000; + if (Argc > 1) { // NOLINT + I = 9001; + } else { + I = 9001; + } + return I; +} diff --git a/test/llvm_test_code/path_tracing/intra_07.cpp b/test/llvm_test_code/path_tracing/intra_07.cpp new file mode 100644 index 0000000000..fc69a9f550 --- /dev/null +++ b/test/llvm_test_code/path_tracing/intra_07.cpp @@ -0,0 +1,15 @@ +int main(int Argc, char **Argv) { + int I = Argc; + int J = I; + if (Argc > 1) { + J = 100; + do { + for (int Idx = 0; Idx < 1000; ++Idx) { + ++J; + } + } while (J > 150); + } else { + I = 13; + } + return J; +} diff --git a/test/llvm_test_code/path_tracing/intra_08.cpp b/test/llvm_test_code/path_tracing/intra_08.cpp new file mode 100644 index 0000000000..26e77a673b --- /dev/null +++ b/test/llvm_test_code/path_tracing/intra_08.cpp @@ -0,0 +1,17 @@ +int main(int Argc, char **Argv) { + int i; + switch (Argc) { + case 1: + i = 10; + break; + case 2: + case 3: + i = 20; + break; + case 4: + i = 30; + default: + i = -1; + } + return i; +} diff --git a/test/llvm_test_code/path_tracing/intra_09.cpp b/test/llvm_test_code/path_tracing/intra_09.cpp new file mode 100644 index 0000000000..784712af18 --- /dev/null +++ b/test/llvm_test_code/path_tracing/intra_09.cpp @@ -0,0 +1,9 @@ +int main(int Argc, char **Argv) { + int C, A, B; + int I = 5; + while (I < 12) { + C = A + B; + I++; + } + return C; +} diff --git a/test/llvm_test_code/path_tracing/other_01.cpp b/test/llvm_test_code/path_tracing/other_01.cpp new file mode 100644 index 0000000000..98f19aabe2 --- /dev/null +++ b/test/llvm_test_code/path_tracing/other_01.cpp @@ -0,0 +1,7 @@ +int main() { + int I; + int J = I; + int K = J + 13; + int L = 9001; + return K; +} diff --git a/tools/example-tool/myphasartool.cpp b/tools/example-tool/myphasartool.cpp index f95f34ce2d..8080dabbe1 100644 --- a/tools/example-tool/myphasartool.cpp +++ b/tools/example-tool/myphasartool.cpp @@ -28,6 +28,9 @@ int main(int Argc, const char **Argv) { std::vector EntryPoints = {"main"s}; HelperAnalyses HA(Argv[1], EntryPoints); + if (!HA.getProjectIRDB().isValid()) { + return 1; + } if (const auto *F = HA.getProjectIRDB().getFunctionDefinition("main")) { // print type hierarchy diff --git a/tools/phasar-cli/phasar-cli.cpp b/tools/phasar-cli/phasar-cli.cpp index c9c20f6296..6781e8e4ba 100644 --- a/tools/phasar-cli/phasar-cli.cpp +++ b/tools/phasar-cli/phasar-cli.cpp @@ -260,7 +260,7 @@ void validateParamModule() { if (!(std::filesystem::exists(ModulePath) && !std::filesystem::is_directory(ModulePath) && (ModulePath.extension() == ".ll" || ModulePath.extension() == ".bc"))) { - llvm::errs() << "LLVM module '" << std::filesystem::absolute(ModulePath) + llvm::errs() << "LLVM module '" << std::filesystem::canonical(ModulePath) << "' does not exist!\n"; exit(1); } @@ -453,6 +453,10 @@ int main(int Argc, const char **Argv) { !AnalysisController::needsToEmitPTA(EmitterOptions), EntryOpt, std::move(PrecomputedCallGraph), CGTypeOpt, SoundnessOpt, AutoGlobalsOpt); + if (!HA.getProjectIRDB().isValid()) { + // Note: Error message has already been printed + return 1; + } AnalysisController Controller( HA, DataFlowAnalysisOpt, {AnalysisConfigOpt.getValue()}, EntryOpt, diff --git a/unittests/PhasarLLVM/DataFlow/CMakeLists.txt b/unittests/PhasarLLVM/DataFlow/CMakeLists.txt index 509a22b31b..3af5da4864 100644 --- a/unittests/PhasarLLVM/DataFlow/CMakeLists.txt +++ b/unittests/PhasarLLVM/DataFlow/CMakeLists.txt @@ -1,2 +1,3 @@ add_subdirectory(IfdsIde) add_subdirectory(Mono) +add_subdirectory(PathSensitivity) diff --git a/unittests/PhasarLLVM/DataFlow/PathSensitivity/CMakeLists.txt b/unittests/PhasarLLVM/DataFlow/PathSensitivity/CMakeLists.txt new file mode 100644 index 0000000000..ac70e1b3ea --- /dev/null +++ b/unittests/PhasarLLVM/DataFlow/PathSensitivity/CMakeLists.txt @@ -0,0 +1,9 @@ +if(PHASAR_USE_Z3) + add_phasar_unittest(PathTracingTest.cpp) + + target_link_libraries(PathTracingTest + LINK_PUBLIC + phasar_llvm_pathsensitivity + z3 + ) +endif() diff --git a/unittests/PhasarLLVM/DataFlow/PathSensitivity/PathTracingTest.cpp b/unittests/PhasarLLVM/DataFlow/PathSensitivity/PathTracingTest.cpp new file mode 100644 index 0000000000..0194d0eead --- /dev/null +++ b/unittests/PhasarLLVM/DataFlow/PathSensitivity/PathTracingTest.cpp @@ -0,0 +1,861 @@ +#include "phasar/DataFlow/IfdsIde/Solver/PathAwareIDESolver.h" +#include "phasar/DataFlow/PathSensitivity/FlowPath.h" +#include "phasar/DataFlow/PathSensitivity/PathSensitivityManager.h" +#include "phasar/PhasarLLVM/ControlFlow/LLVMBasedICFG.h" +#include "phasar/PhasarLLVM/DB/LLVMProjectIRDB.h" +#include "phasar/PhasarLLVM/DataFlow/IfdsIde/Problems/IDEExtendedTaintAnalysis.h" +#include "phasar/PhasarLLVM/DataFlow/IfdsIde/Problems/IDELinearConstantAnalysis.h" +#include "phasar/PhasarLLVM/DataFlow/PathSensitivity/LLVMPathConstraints.h" +#include "phasar/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitivityConfig.h" +#include "phasar/PhasarLLVM/DataFlow/PathSensitivity/Z3BasedPathSensitvityManager.h" +#include "phasar/PhasarLLVM/Passes/ValueAnnotationPass.h" +#include "phasar/PhasarLLVM/Pointer/LLVMAliasSet.h" +#include "phasar/PhasarLLVM/TaintConfig/LLVMTaintConfig.h" +#include "phasar/PhasarLLVM/TypeHierarchy/LLVMTypeHierarchy.h" +#include "phasar/PhasarLLVM/Utils/LLVMShorthands.h" +#include "phasar/Utils/AdjacencyList.h" +#include "phasar/Utils/DFAMinimizer.h" +#include "phasar/Utils/DebugOutput.h" +#include "phasar/Utils/GraphTraits.h" +#include "phasar/Utils/Logger.h" +#include "phasar/Utils/Utilities.h" + +#include "llvm/ADT/STLExtras.h" +#include "llvm/IR/Constants.h" +#include "llvm/IR/Instruction.h" +#include "llvm/IR/Instructions.h" +#include "llvm/Support/Casting.h" +#include "llvm/Support/raw_ostream.h" + +#include "TestConfig.h" +#include "gtest/gtest.h" + +#include +#include +#include +#include +#include +#include + +namespace { +// ============== TEST FIXTURE ============== // +class PathTracingTest : public ::testing::Test { +public: + static constexpr auto PathToLlFiles = PHASAR_BUILD_SUBFOLDER("path_tracing/"); + + static std::pair + getInterestingInstFact(psr::LLVMProjectIRDB &IRDB) { + auto *Main = IRDB.getFunctionDefinition("main"); + assert(Main); + auto *LastInst = &Main->back().back(); + auto *InterestingFact = [&] { + if (auto *RetInst = llvm::dyn_cast(LastInst); + RetInst && RetInst->getReturnValue() && + !llvm::isa(RetInst->getReturnValue())) { + return RetInst->getReturnValue(); + } + + auto *Inst = LastInst->getPrevNode(); + while (Inst && !Inst->getType()->isIntegerTy()) { + Inst = Inst->getPrevNode(); + } + assert(Inst != nullptr); + return static_cast(Inst); + }(); + + return {LastInst, InterestingFact}; + } + +protected: + std::unique_ptr IRDB; + psr::LLVMPathConstraints LPC; + + void SetUp() override { psr::ValueAnnotationPass::resetValueID(); } + void TearDown() override { psr::Logger::disable(); } + + std::pair + getInterestingInstFact() { + return getInterestingInstFact(*IRDB); + } + + psr::FlowPathSequence + doAnalysis(const std::string &LlvmFilePath, bool PrintDump = false) { + IRDB = std::make_unique(PathToLlFiles + LlvmFilePath); + psr::LLVMTypeHierarchy TH(*IRDB); + psr::LLVMAliasSet PT(IRDB.get()); + psr::LLVMBasedICFG ICFG(IRDB.get(), psr::CallGraphAnalysisType::OTF, + {"main"}, &TH, &PT, psr::Soundness::Soundy, + /*IncludeGlobals*/ false); + psr::IDELinearConstantAnalysis LCAProblem(IRDB.get(), &ICFG, {"main"}); + psr::PathAwareIDESolver LCASolver(LCAProblem, &ICFG); + LCASolver.solve(); + if (PrintDump) { + // IRDB->print(); + // ICFG.print(); + // LCASolver.dumpResults(); + std::error_code EC; + llvm::raw_fd_ostream ROS(LlvmFilePath + "_explicit_esg.dot", EC); + assert(!EC); + LCASolver.getExplicitESG().printAsDot(ROS); + } + auto [LastInst, InterestingFact] = getInterestingInstFact(); + llvm::outs() << "Target instruction: " << psr::llvmIRToString(LastInst); + llvm::outs() << "\nTarget data-flow fact: " + << psr::llvmIRToString(InterestingFact) << '\n'; + + psr::Z3BasedPathSensitivityManager + PSM(&LCASolver.getExplicitESG(), {}, &LPC); + + return PSM.pathsTo(LastInst, InterestingFact); + } + + psr::FlowPathSequence + doLambdaAnalysis(const std::string &LlvmFilePath, + size_t MaxDAGDepth = SIZE_MAX) { + IRDB = std::make_unique(PathToLlFiles + LlvmFilePath); + psr::LLVMTypeHierarchy TH(*IRDB); + psr::LLVMAliasSet PT(IRDB.get()); + psr::LLVMBasedICFG ICFG(IRDB.get(), psr::CallGraphAnalysisType::OTF, + {"main"}, &TH, &PT, psr::Soundness::Soundy, + /*IncludeGlobals*/ false); + + psr::LLVMTaintConfig Config(*IRDB); + psr::IDEExtendedTaintAnalysis<3, false> Analysis(IRDB.get(), &ICFG, &PT, + Config, {"main"}); + psr::PathAwareIDESolver Solver(Analysis, &ICFG); + Solver.solve(); + + auto *Main = IRDB->getFunctionDefinition("main"); + assert(Main); + auto *LastInst = &Main->back().back(); + llvm::outs() << "Target instruction: " << psr::llvmIRToString(LastInst) + << '\n'; + + // std::error_code EC; + // llvm::raw_fd_ostream ROS(LlvmFilePath + "_explicit_esg.dot", EC); + // assert(!EC); + // Solver.getExplicitESG().printAsDot(ROS); + + psr::Z3BasedPathSensitivityManager PSM( + &Solver.getExplicitESG(), + psr::Z3BasedPathSensitivityConfig().withDAGDepthThreshold(MaxDAGDepth), + &LPC); + + return PSM.pathsTo(LastInst, Analysis.getZeroValue()); + } + + void comparePaths( + const psr::FlowPathSequence &AnalyzedPaths, + const std::vector> &GroundTruth) { + std::set MatchingIndices; + auto Matches = [&AnalyzedPaths, + &MatchingIndices](const std::vector >) { + size_t Idx = 0; + for (const auto &Path : AnalyzedPaths) { + psr::scope_exit IncIdx = [&Idx] { ++Idx; }; + if (Path.size() != GT.size()) { + continue; + } + bool Match = true; + for (size_t I = 0; I < Path.size(); ++I) { + if (std::stoul(psr::getMetaDataID(Path[I])) != GT[I]) { + Match = false; + break; + } + } + if (Match) { + MatchingIndices.insert(Idx); + return true; + } + } + + return false; + }; + + for (const auto > : GroundTruth) { + EXPECT_TRUE(Matches(GT)) + << "No match found for " << psr::PrettyPrinter{GT} + << "; MatchingIndices.size() = " << MatchingIndices.size() + << "; AnalyzedPaths.size() = " << AnalyzedPaths.size(); + } + + EXPECT_EQ(MatchingIndices.size(), AnalyzedPaths.size()); + + if (MatchingIndices.size() != AnalyzedPaths.size()) { + for (size_t I = 0; I < AnalyzedPaths.size(); ++I) { + if (MatchingIndices.count(I)) { + continue; + } + + llvm::errs() << "> PATH NOT IN GT: " + << psr::PrettyPrinter{llvm::map_range( + AnalyzedPaths[I], + [](const auto *Inst) { + return psr::getMetaDataID(Inst); + })} + << '\n'; + } + } + } +}; // Test Fixture + +TEST_F(PathTracingTest, Handle_Inter_01) { + auto PathsVec = doAnalysis("inter_01_cpp.ll"); + comparePaths(PathsVec, {{6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 0, 1, 2, 3, 5, + 16, 17, 18}}); +} + +TEST_F(PathTracingTest, Lambda_Inter_01) { + auto PathsVec = doLambdaAnalysis("inter_01_cpp.ll"); + comparePaths(PathsVec, {{6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 0, 1, 2, 3, 4, 5, + 16, 17, 18}}); +} + +TEST_F(PathTracingTest, Handle_Inter_02) { + auto PathsVec = doAnalysis("inter_02_cpp.ll"); + comparePaths(PathsVec, + {{12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 6, 7, 8, 9, + 10, 11, 22, 23, 24, 0, 1, 2, 3, 5, 25, 26, 27}}); +} + +TEST_F(PathTracingTest, Lambda_Inter_02) { + auto PathsVec = doLambdaAnalysis("inter_02_cpp.ll"); + comparePaths(PathsVec, + {{12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 6, 7, 8, 9, + 10, 11, 22, 23, 24, 0, 1, 2, 3, 4, 5, 25, 26, 27}}); +} + +TEST_F(PathTracingTest, Handle_Inter_03) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "CallStackPathFilter"); + auto PathsVec = doAnalysis("inter_03_cpp.ll", false); + comparePaths(PathsVec, {{6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 0, 1, 2, + 3, 5, 17, 18, 19, 0, 1, 2, 3, 5, 20, 21, 22}}); +} + +TEST_F(PathTracingTest, Lambda_Inter_03) { + auto PathsVec = doLambdaAnalysis("inter_03_cpp.ll"); + comparePaths(PathsVec, + {{6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 0, 1, 2, 3, + 4, 5, 17, 18, 19, 0, 1, 2, 3, 4, 5, 20, 21, 22}}); +} + +TEST_F(PathTracingTest, Handle_Inter_04) { + auto PathsVec = doAnalysis("inter_04_cpp.ll"); + comparePaths(PathsVec, {{22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 0, + 1, 2, 3, 5, 33, 34, 35, 6, 8, 11, 16, 17, + 0, 1, 2, 3, 5, 18, 19, 20, 21, 36, 37, 38}}); +} + +TEST_F(PathTracingTest, Lambda_Inter_04) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + auto PathsVec = doLambdaAnalysis("inter_04_cpp.ll"); + comparePaths(PathsVec, + { + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 0, 1, 2, + 3, 4, 5, 33, 34, 35, 6, 7, 8, 9, 10, 11, 16, 17, + 0, 1, 2, 3, 4, 5, 18, 19, 20, 21, 36, 37, 38}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 0, + 1, 2, 3, 4, 5, 33, 34, 35, 6, 7, 8, 9, + 10, 11, 12, 13, 14, 15, 20, 21, 36, 37, 38}, + }); +} + +TEST_F(PathTracingTest, Handle_Inter_05) { + /// NOTE: We are generating from zero a few times, so without AutoSkipZero we + /// get a lot of paths here + auto PathsVec = doAnalysis("inter_05_cpp.ll", false); + comparePaths( + PathsVec, + {{22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, + 15, 16, 17, 18, 19, 21, 39, 40, 41, 44, 45, 46, 47, 0, 1, 2, 3, + 4, 5, 6, 7, 11, 12, 13, 14, 48, 49, 50, 51, 52, 53, 54, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 15, + 16, 17, 18, 19, 21, 39, 40, 41, 42, 43, 44, 45, 46, 47, 0, 1, 2, 3, + 4, 5, 6, 7, 11, 12, 13, 14, 48, 49, 50, 51, 52, 53, 54, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 15, + 16, 17, 18, 19, 20, 21, 39, 40, 41, 44, 45, 46, 47, 0, 1, 2, 3, 4, + 5, 6, 7, 8, 9, 10, 13, 14, 48, 49, 50, 51, 52, 53, 54, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, + 36, 37, 38, 15, 16, 17, 18, 19, 20, 21, 39, 40, 41, 42, + 43, 44, 45, 46, 47, 0, 1, 2, 3, 4, 5, 6, 7, 8, + 9, 10, 13, 14, 48, 49, 50, 51, 52, 53, 54, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 41, 44, 52, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, + 38, 15, 16, 17, 18, 19, 21, 39, 40, 41, 42, 43, 44, 52, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, + 15, 16, 17, 18, 19, 20, 21, 39, 40, 41, 42, 43, 44, 52, 55, 56}}); +} + +TEST_F(PathTracingTest, Lambda_Inter_05) { + /// We have 4 branches ==> 16 paths + auto PathsVec = doLambdaAnalysis("inter_05_cpp.ll"); + comparePaths( + PathsVec, + { + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, + 15, 16, 17, 18, 19, 21, 39, 40, 41, 44, 45, 46, 47, 0, 1, 2, 3, + 4, 5, 6, 7, 11, 12, 13, 14, 48, 49, 50, 51, 52, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, + 15, 16, 17, 18, 19, 21, 39, 40, 41, 42, 43, 44, 45, 46, 47, 0, 1, + 2, 3, 4, 5, 6, 7, 11, 12, 13, 14, 48, 49, 50, 51, 52, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, + 15, 16, 17, 18, 19, 21, 39, 40, 41, 44, 45, 46, 47, 0, 1, 2, 3, + 4, 5, 6, 7, 11, 12, 13, 14, 48, 49, 50, 51, 52, 53, 54, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, + 15, 16, 17, 18, 19, 20, 21, 39, 40, 41, 44, 45, 46, 47, 0, 1, 2, + 3, 4, 5, 6, 7, 8, 9, 10, 13, 14, 48, 49, 50, 51, 52, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, + 36, 37, 38, 15, 16, 17, 18, 19, 21, 39, 40, 41, 42, 43, + 44, 45, 46, 47, 0, 1, 2, 3, 4, 5, 6, 7, 11, 12, + 13, 14, 48, 49, 50, 51, 52, 53, 54, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, + 36, 37, 38, 15, 16, 17, 18, 19, 20, 21, 39, 40, 41, 42, + 43, 44, 45, 46, 47, 0, 1, 2, 3, 4, 5, 6, 7, 8, + 9, 10, 13, 14, 48, 49, 50, 51, 52, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, + 36, 37, 38, 15, 16, 17, 18, 19, 20, 21, 39, 40, 41, 44, + 45, 46, 47, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, + 13, 14, 48, 49, 50, 51, 52, 53, 54, 55, 56}, + {22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, + 36, 37, 38, 15, 16, 17, 18, 19, 20, 21, 39, 40, 41, 42, + 43, 44, 45, 46, 47, 0, 1, 2, 3, 4, 5, 6, 7, 8, + 9, 10, 13, 14, 48, 49, 50, 51, 52, 53, 54, 55, 56}, + }); +} + +TEST_F(PathTracingTest, Lambda_Inter_Depth3_05) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + /// We have 4 branches ==> 16 paths + auto PathsVec = doLambdaAnalysis("inter_05_cpp.ll", /*MaxDAGDepth*/ 3); + comparePaths(PathsVec, + { + {44, 45, 46, 47, 0, 1, 2, 3, 4, 5, 6, 7, + 8, 9, 10, 13, 14, 48, 49, 50, 51, 52, 55, 56}, + {44, 45, 46, 47, 0, 1, 2, 3, 4, 5, 6, 7, 8, + 9, 10, 13, 14, 48, 49, 50, 51, 52, 53, 54, 55, 56}, + {44, 45, 46, 47, 0, 1, 2, 3, 4, 5, 6, 7, + 11, 12, 13, 14, 48, 49, 50, 51, 52, 55, 56}, + {44, 45, 46, 47, 0, 1, 2, 3, 4, 5, 6, 7, 11, + 12, 13, 14, 48, 49, 50, 51, 52, 53, 54, 55, 56}, + }); +} + +TEST_F(PathTracingTest, Handle_Inter_06) { + auto PathsVec = doAnalysis("inter_06_cpp.ll"); + comparePaths(PathsVec, {{8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, + 20, 21, 25, 27, 0, 2, 4, 6, 7, 28, 29, 30}, + {8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, + 22, 26, 27, 0, 3, 5, 6, 7, 28, 29, 30}}); +} + +TEST_F(PathTracingTest, Lambda_Inter_06) { + auto PathsVec = doLambdaAnalysis("inter_06_cpp.ll"); + comparePaths(PathsVec, + {{8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, + 24, 25, 26, 27, 0, 1, 2, 3, 4, 5, 6, 7, 28, 29, 30}}); +} + +TEST_F(PathTracingTest, Handle_Inter_07) { + auto PathsVec = doAnalysis("inter_07_cpp.ll"); + comparePaths(PathsVec, + { + {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, + 30, 34, 42, 44, 46, 8, 10, 12, 14, 15, 47, 48, 49, 50}, + {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 31, + 34, 42, 45, 46, 8, 11, 13, 14, 15, 47, 48, 49, 50}, + {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, + 30, 34, 42, 44, 46, 0, 2, 4, 6, 7, 47, 48, 49, 50}, + {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 31, + 34, 42, 45, 46, 0, 3, 5, 6, 7, 47, 48, 49, 50}, + {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, + 30, 34, 35, 37, 39, 8, 10, 12, 14, 15, 40, 41, 49, 50}, + {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 31, + 34, 35, 38, 39, 8, 11, 13, 14, 15, 40, 41, 49, 50}, + {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, + 30, 34, 35, 37, 39, 0, 2, 4, 6, 7, 40, 41, 49, 50}, + {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 31, + 34, 35, 38, 39, 0, 3, 5, 6, 7, 40, 41, 49, 50}, + }); +} + +TEST_F(PathTracingTest, Lambda_Inter_07) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + auto PathsVec = doLambdaAnalysis("inter_07_cpp.ll"); + comparePaths(PathsVec, { + {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, + 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, + 0, 1, 2, 3, 4, 5, 6, 7, 40, 41, 49, 50}, + {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, + 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, + 8, 9, 10, 11, 12, 13, 14, 15, 40, 41, 49, 50}, + {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, + 28, 29, 30, 31, 32, 33, 34, 42, 43, 44, 45, 46, + 0, 1, 2, 3, 4, 5, 6, 7, 47, 48, 49, 50}, + {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, + 28, 29, 30, 31, 32, 33, 34, 42, 43, 44, 45, 46, + 8, 9, 10, 11, 12, 13, 14, 15, 47, 48, 49, 50}, + }); +} + +TEST_F(PathTracingTest, Lambda_Inter_Depth3_07) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + auto PathsVec = doLambdaAnalysis("inter_07_cpp.ll", /*MaxDAGDepth*/ 3); + comparePaths(PathsVec, { + {0, 1, 2, 3, 4, 5, 6, 7, 40, 41, 49, 50}, + {0, 1, 2, 3, 4, 5, 6, 7, 47, 48, 49, 50}, + {8, 9, 10, 11, 12, 13, 14, 15, 40, 41, 49, 50}, + {8, 9, 10, 11, 12, 13, 14, 15, 47, 48, 49, 50}, + }); +} + +TEST_F(PathTracingTest, Handle_Inter_08) { + auto PathsVec = doAnalysis("inter_08_cpp.ll", false); + /// FIXME: Handle mutable z3::exprs; As of now, we reject all paths that go + /// into a loop, because this requires the loop condiiton to hold, whereas + /// leaving the loop requires the loop condition not to hold which is + /// contradictory + comparePaths( + PathsVec, + { + {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, + 55, 56, 57, 58, 59, 60, 61, 69, 70, 71, 72, 73, + 0, 1, 2, 7, 8, 10, 20, 21, 74, 75, 76, 77}, + // {54, 55, 56, 57, 61, 71, 73, 26, 29, 32, + // 33, 35, 36, 40, 32, 41, 42, 74, 75, 76}, + // {54, 55, 58, 61, 72, 73, 27, 29, 32, 34, 35, 36, 40, + // 32, 41, 42, 74, 75, 76, 77}, + {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, + 55, 56, 57, 58, 59, 60, 61, 69, 70, 71, 72, 73, + 22, 23, 24, 29, 30, 32, 41, 42, 74, 75, 76, 77}, + // {54, 55, 56, 57, 61, 71, 73, 4, 7, 10, 11, + // 13, 14, 15, 19, 10, 20, 21, 74, 75, 76, 77}, + // {54, 55, 58, 61, 72, 73, 5, 7, 10, 12, + // 13, 14, 15, 19, 10, 20, 21, 74, 75, 76, 77}, + {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, + 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, + 22, 23, 24, 29, 30, 32, 41, 42, 67, 68, 76, 77}, + // {54, 55, 56, 57, 61, 64, 66, 26, 29, 32, + // 33, 35, 36, 40, 32, 41, 42, 67, 68, 76, 77}, + // {54, 55, 58, 61, 65, 66, 27, 29, 32, 34, 35, 36, 40, 32, 41, 42, + // 67, 68, 76, 77}, + {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, + 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, + 0, 1, 2, 7, 8, 10, 20, 21, 67, 68, 76, 77}, + // {54, 55, 56, 57, 61, 64, 66, 4, 7, 10, 11, + // 13, 14, 15, 19, 10, 20, 21, 67, 68, 76, 77}, + // {54, 55, 58, 61, 65, 66, 5, 7, 10, 12, + // 13, 14, 15, 19, 10, 20, 21, 67, 68, 76, 77}, + }); +} + +TEST_F(PathTracingTest, Lambda_Inter_08) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + auto PathsVec = doLambdaAnalysis("inter_08_cpp.ll"); + /// FIXME: Handle mutable z3::exprs; As of now, we reject all paths that go + /// into a loop, because this requires the loop condiiton to hold, whereas + /// leaving the loop requires the loop condition not to hold which is + /// contradictory + comparePaths(PathsVec, + { + {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, + 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 0, 1, 2, 3, + 4, 5, 6, 7, 8, 9, 10, 20, 21, 67, 68, 76, 77}, + {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, + 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 22, 23, 24, 25, + 26, 27, 28, 29, 30, 31, 32, 41, 42, 67, 68, 76, 77}, + {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, + 57, 58, 59, 60, 61, 69, 70, 71, 72, 73, 0, 1, 2, 3, + 4, 5, 6, 7, 8, 9, 10, 20, 21, 74, 75, 76, 77}, + {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, + 57, 58, 59, 60, 61, 69, 70, 71, 72, 73, 22, 23, 24, 25, + 26, 27, 28, 29, 30, 31, 32, 41, 42, 74, 75, 76, 77}, + // {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, + // 57, 58, 59, + // 60, 61, 62, 63, 64, 65, 66, 22, 23, 24, 25, 26, 27, 28, + // 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 30, 31, + // 32, 41, 42, 67, 68, 76, 77}, + // {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, + // 57, 58, 59, + // 60, 61, 69, 70, 71, 72, 73, 22, 23, 24, 25, 26, 27, 28, + // 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 30, 31, + // 32, 41, 42, 74, 75, 76, 77}, + // {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, + // 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 0, 1, + // 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, + // 15, 16, 17, 18, 19, 8, 9, 10, 20, 21, 67, 68, 76, 77}, + // {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, + // 56, 57, 58, 59, 60, 61, 69, 70, 71, 72, 73, 0, 1, + // 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, + // 15, 16, 17, 18, 19, 8, 9, 10, 20, 21, 74, 75, 76, 77}, + + }); +} + +TEST_F(PathTracingTest, Handle_Inter_09) { + auto PathsVec = doAnalysis("inter_09_cpp.ll", false); + /// FIXME: Same reason as Handle_Inter_08 + comparePaths( + PathsVec, + { + // {22, 2, 5, 6, 7, 8, 2, 5, 11, 12, 13, 14, 15, 9, 10, 14, 15}, + {16, 17, 18, 19, 20, 21, 22, 0, 2, 5, 11, 12, 13, 14, 15, 23, 24}, + }); +} + +TEST_F(PathTracingTest, Lambda_Inter_09) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + auto PathsVec = doLambdaAnalysis("inter_09_cpp.ll"); + /// FIXME: Same reason as Lambda_Inter_08 + comparePaths(PathsVec, { + {16, 17, 18, 19, 20, 21, 22, 0, 1, 2, + 3, 4, 5, 11, 12, 13, 14, 15, 23, 24}, + // {16, 17, 18, 19, 20, 21, 22, 0, 1, 2, 3, + // 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, + // 11, 12, 13, 14, 15, 9, 10, 14, 15, 23, 24}, + }); +} + +TEST_F(PathTracingTest, Handle_Inter_10) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + GTEST_SKIP() << "Need globals support"; + auto PathsVec = doAnalysis("inter_10_cpp.ll", false); + /// TODO: GT +} + +TEST_F(PathTracingTest, Handle_Inter_11) { + auto PathsVec = doAnalysis("inter_11_cpp.ll"); + // Note: The alias analysis is strong enough to see that Three::assignValue + // can never be called + comparePaths(PathsVec, {{8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 27, 28, 29, + 30, 31, 35, 36, 37, 38, 39, 40, 32, 33, 34, 18, 19, + 20, 21, 22, 23, 24, 25, 41, 44, 46, 47, 48, 26}}); +} + +TEST_F(PathTracingTest, Lambda_Inter_11) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + auto PathsVec = doLambdaAnalysis("inter_11_cpp.ll"); + // Note: The alias analysis is strong enough to see that Three::assignValue + // can never be called + comparePaths(PathsVec, + {{8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 27, 28, 29, 30, + 31, 35, 36, 37, 38, 39, 40, 32, 33, 34, 18, 19, 20, 21, + 22, 23, 24, 25, 41, 42, 43, 44, 45, 46, 47, 48, 26}}); +} + +TEST_F(PathTracingTest, Handle_Inter_12) { + auto PathsVec = doAnalysis("inter_12_cpp.ll"); + comparePaths( + PathsVec, + {{11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 44, 45, 46, 47, 48, + 60, 61, 62, 63, 64, 65, 49, 50, 51, 21, 22, 23, 24, 25, 32, + 33, 34, 52, 53, 54, 55, 56, 60, 61, 62, 63, 64, 65, 57, 58, + 59, 35, 36, 37, 38, 39, 40, 41, 42, 79, 82, 84, 85, 86, 43}, + {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 44, 45, 46, 47, 48, + 60, 61, 62, 63, 64, 65, 49, 50, 51, 21, 22, 23, 24, 25, 32, + 33, 34, 52, 53, 54, 55, 56, 60, 61, 62, 63, 64, 65, 57, 58, + 59, 35, 36, 37, 38, 39, 40, 41, 42, 109, 112, 114, 115, 116, 43}, + {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 44, 45, 46, 47, 48, 60, 61, + 62, 63, 64, 65, 49, 50, 51, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, + 72, 73, 74, 75, 66, 67, 68, 69, 70, 87, 88, 89, 90, 71, 76, 77, 78, + 31, 32, 33, 34, 52, 53, 54, 55, 56, 60, 61, 62, 63, 64, 65, 57, 58, + 59, 35, 36, 37, 38, 39, 40, 41, 42, 79, 82, 84, 85, 86, 43}, + {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 44, 45, 46, 47, 48, 60, 61, + 62, 63, 64, 65, 49, 50, 51, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, + 72, 73, 74, 75, 66, 67, 68, 69, 70, 87, 88, 89, 90, 71, 76, 77, 78, + 31, 32, 33, 34, 52, 53, 54, 55, 56, 60, 61, 62, 63, 64, 65, 57, 58, + 59, 35, 36, 37, 38, 39, 40, 41, 42, 109, 112, 114, 115, 116, 43}, + {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 44, 45, 46, 47, + 48, 60, 61, 62, 63, 64, 65, 49, 50, 51, 21, 22, 23, 24, + 25, 26, 27, 28, 29, 30, 102, 103, 104, 105, 96, 97, 98, 99, + 100, 87, 88, 89, 90, 101, 106, 107, 108, 31, 32, 33, 34, 52, + 53, 54, 55, 56, 60, 61, 62, 63, 64, 65, 57, 58, 59, 35, + 36, 37, 38, 39, 40, 41, 42, 79, 82, 84, 85, 86, 43}, + {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 44, 45, 46, 47, + 48, 60, 61, 62, 63, 64, 65, 49, 50, 51, 21, 22, 23, 24, + 25, 26, 27, 28, 29, 30, 102, 103, 104, 105, 96, 97, 98, 99, + 100, 87, 88, 89, 90, 101, 106, 107, 108, 31, 32, 33, 34, 52, + 53, 54, 55, 56, 60, 61, 62, 63, 64, 65, 57, 58, 59, 35, + 36, 37, 38, 39, 40, 41, 42, 109, 112, 114, 115, 116, 43}}); +} + +TEST_F(PathTracingTest, Lambda_Inter_12) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + auto PathsVec = doLambdaAnalysis("inter_12_cpp.ll"); + comparePaths( + PathsVec, + { + {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 44, 45, 46, + 47, 48, 60, 61, 62, 63, 64, 65, 49, 50, 51, 21, 22, + 23, 24, 25, 32, 33, 34, 52, 53, 54, 55, 56, 60, 61, + 62, 63, 64, 65, 57, 58, 59, 35, 36, 37, 38, 39, 40, + 41, 42, 109, 110, 111, 112, 113, 114, 115, 116, 43}, + {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 44, 45, 46, 47, 48, + 60, 61, 62, 63, 64, 65, 49, 50, 51, 21, 22, 23, 24, 25, 26, + 27, 28, 29, 30, 72, 73, 74, 75, 66, 67, 68, 69, 70, 87, 88, + 89, 90, 71, 76, 77, 78, 31, 32, 33, 34, 52, 53, 54, 55, 56, + 60, 61, 62, 63, 64, 65, 57, 58, 59, 35, 36, 37, 38, 39, 40, + 41, 42, 79, 80, 81, 82, 83, 84, 85, 86, 43}, + {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 44, 45, 46, 47, 48, + 60, 61, 62, 63, 64, 65, 49, 50, 51, 21, 22, 23, 24, 25, 26, + 27, 28, 29, 30, 72, 73, 74, 75, 66, 67, 68, 69, 70, 87, 88, + 89, 90, 71, 76, 77, 78, 31, 32, 33, 34, 52, 53, 54, 55, 56, + 60, 61, 62, 63, 64, 65, 57, 58, 59, 35, 36, 37, 38, 39, 40, + 41, 42, 109, 110, 111, 112, 113, 114, 115, 116, 43}, + {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 44, 45, 46, 47, 48, + 60, 61, 62, 63, 64, 65, 49, 50, 51, 21, 22, 23, 24, 25, 26, + 27, 28, 29, 30, 102, 103, 104, 105, 96, 97, 98, 99, 100, 87, 88, + 89, 90, 101, 106, 107, 108, 31, 32, 33, 34, 52, 53, 54, 55, 56, + 60, 61, 62, 63, 64, 65, 57, 58, 59, 35, 36, 37, 38, 39, 40, + 41, 42, 79, 80, 81, 82, 83, 84, 85, 86, 43}, + {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 44, 45, 46, 47, 48, + 60, 61, 62, 63, 64, 65, 49, 50, 51, 21, 22, 23, 24, 25, 26, + 27, 28, 29, 30, 102, 103, 104, 105, 96, 97, 98, 99, 100, 87, 88, + 89, 90, 101, 106, 107, 108, 31, 32, 33, 34, 52, 53, 54, 55, 56, + 60, 61, 62, 63, 64, 65, 57, 58, 59, 35, 36, 37, 38, 39, 40, + 41, 42, 109, 110, 111, 112, 113, 114, 115, 116, 43}, + {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 44, 45, 46, 47, 48, 60, + 61, 62, 63, 64, 65, 49, 50, 51, 21, 22, 23, 24, 25, 32, 33, 34, + 52, 53, 54, 55, 56, 60, 61, 62, 63, 64, 65, 57, 58, 59, 35, 36, + 37, 38, 39, 40, 41, 42, 79, 80, 81, 82, 83, 84, 85, 86, 43}, + }); +} + +TEST_F(PathTracingTest, Handle_Intra_01) { + auto PathsVec = doAnalysis("intra_01_cpp.ll"); + comparePaths(PathsVec, {{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11}}); +} + +TEST_F(PathTracingTest, Handle_Intra_02) { + auto PathsVec = doAnalysis("intra_02_cpp.ll"); + comparePaths(PathsVec, {{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 14, 15}, + {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 12, 13, 14, 15}}); +} + +TEST_F(PathTracingTest, Handle_Intra_03) { + auto PathsVec = doAnalysis("intra_03_cpp.ll"); + comparePaths(PathsVec, {{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, + 16, 19, 20}}); +} + +TEST_F(PathTracingTest, Handle_Intra_04) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + auto PathsVec = doAnalysis("intra_04_cpp.ll"); + /// FIXME: Same reason as Handle_Inter_08 + comparePaths(PathsVec, + { + // {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, + // 18, 21, 22, 23, 24, 25, 29, 21, 30, 33, 34}, + {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, + 12, 13, 14, 15, 16, 18, 19, 21, 30, 33, 34}, + }); +} + +TEST_F(PathTracingTest, Handle_Intra_05) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + auto PathsVec = doAnalysis("intra_05_cpp.ll"); + comparePaths( + PathsVec, + {{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 19, 20}, + {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 16, 17, 18, 19, 20}}); +} + +TEST_F(PathTracingTest, Handle_Intra_06) { + auto PathsVec = doAnalysis("intra_06_cpp.ll"); + comparePaths(PathsVec, {{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 15, 16}, + {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 13, 14, 15, 16}}); +} + +TEST_F(PathTracingTest, Handle_Intra_07) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + auto PathsVec = doAnalysis("intra_07_cpp.ll"); + /// FIXME: Same reason as Handle_Inter_08 + comparePaths( + PathsVec, + { + // {16, 17, 19, 22, 31, 34, 19, 22, 23, 24, 25, 26, 30, 22, 31, + // 34, 35, 38, 39}, + // {16, 17, 18, 19, 20, 21, 22, 31, 32, 33, 34, + // 18, 19, 20, 21, 22, 31, 32, 33, 34, 35, 38, 39}, + // {16, 17, 19, 22, 23, 24, 25, 26, 30, 22, 31, 34, 35, 38, 39}, + // {16, 17, 19, 22, 31, 34, 19, 22, 31, 34, 35, 38, 39}, + {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, + 14, 15, 16, 17, 18, 19, 20, 22, 31, 32, 34, 35, 38, 39}, + }); +} + +TEST_F(PathTracingTest, Handle_Intra_08) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + auto PathsVec = doAnalysis("intra_08_cpp.ll", false); + // for (const auto &Path : PathsVec) { + // for (const auto *Inst : Path) { + // llvm::errs() << " " << psr::getMetaDataID(Inst); + // } + // llvm::errs() << '\n'; + // } + + /// NOTE: we have a fallthrough from case 4 to default; Therefore, we only + /// have 3 paths + /// UPDATE: Despite the fallthrough, clang-14 now generates 4 distinct + /// switch-cases, where the ID13 one just branches into the default case. So, + /// we now have 4 cases! + comparePaths(PathsVec, {{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 17, 18}, + {0, 1, 2, 3, 4, 5, 6, 7, 8, 11, 12, 17, 18}, + {0, 1, 2, 3, 4, 5, 6, 7, 8, 15, 16, 17, 18}, + {0, 1, 2, 3, 4, 5, 6, 7, 8, 13, 14, 15, 16, 17, 18}}); +} + +TEST_F(PathTracingTest, Handle_Intra_09) { + // psr::Logger::initializeStderrLogger(psr::SeverityLevel::DEBUG, + // "PathSensitivityManager"); + auto PathsVec = doAnalysis("intra_09_cpp.ll"); + /// FIXME: Same reason as Handle_Inter_08 + comparePaths(PathsVec, + { + // {0, 1, 2, 5, 11, 14, 16, 17, 18, 22, 14, 23, 24}, + // {0, 1, 2, 4, 11, 14, 15, 17, 18, 22, 14, 23, 24}, + {0, 1, 2, 3, 11, 12, 14, 23, 24}, + }); +} + +TEST_F(PathTracingTest, Handle_Other_01) { + auto PathsVec = doAnalysis("other_01_cpp.ll"); + comparePaths(PathsVec, {{0, 1, 6, 7, 8, 9, 10, 12, 13}}); +} + +TEST(PathsDAGTest, ForwardMinimizeDAGTest) { + psr::AdjacencyList Graph; + using traits_t = psr::GraphTraits; + auto One = traits_t::addNode(Graph, 1); + auto Two = traits_t::addNode(Graph, 2); + auto Three = traits_t::addNode(Graph, 2); + auto Four = traits_t::addNode(Graph, 2); + + traits_t::addRoot(Graph, One); + traits_t::addEdge(Graph, One, Two); + traits_t::addEdge(Graph, One, Three); + traits_t::addEdge(Graph, One, Four); + + auto Eq = psr::minimizeGraph(Graph); + Graph = psr::createEquivalentGraphFrom(std::move(Graph), Eq); + // psr::printGraph(Graph, llvm::outs()); + // llvm::outs() << '\n'; + + EXPECT_EQ(traits_t::size(Graph), 2); + ASSERT_EQ(traits_t::roots_size(Graph), 1); + auto Rt = traits_t::roots(Graph)[0]; + EXPECT_EQ(traits_t::outDegree(Graph, Rt), 1); + EXPECT_NE(traits_t::target(traits_t::outEdges(Graph, Rt)[0]), Rt); + EXPECT_EQ(traits_t::outDegree( + Graph, traits_t::target(traits_t::outEdges(Graph, Rt)[0])), + 0); +} + +template +std::vector> getPaths(const GraphTy &G) { + std::vector> Ret; + std::vector Curr; + using traits_t = psr::GraphTraits; + auto doGetPaths = [&G, &Curr, &Ret](const auto &doGetPaths, + auto Vtx) -> void { + size_t Sz = Curr.size(); + for (const auto *N : traits_t::node(G, Vtx)) { + Curr.push_back(psr::getMetaDataID(N)); + } + bool HasSucc = false; + for (auto Edge : traits_t::outEdges(G, Vtx)) { + HasSucc = true; + doGetPaths(doGetPaths, traits_t::target(Edge)); + } + if (!HasSucc) { + Ret.push_back(Curr); + } + Curr.resize(Sz); + }; + + for (auto Rt : traits_t::roots(G)) { + doGetPaths(doGetPaths, Rt); + } + + return Ret; +} + +TEST(PathsDAGTest, InLLVMSSA) { + psr::LLVMProjectIRDB IRDB(PathTracingTest::PathToLlFiles + "inter_01_cpp.ll"); + psr::LLVMTypeHierarchy TH(IRDB); + psr::LLVMAliasSet PT(&IRDB); + psr::LLVMBasedICFG ICFG(&IRDB, psr::CallGraphAnalysisType::OTF, {"main"}, &TH, + &PT, psr::Soundness::Soundy, + /*IncludeGlobals*/ false); + psr::IDELinearConstantAnalysis LCAProblem(&IRDB, &ICFG, {"main"}); + psr::PathAwareIDESolver LCASolver(LCAProblem, &ICFG); + LCASolver.solve(); + // if (PrintDump) { + // // IRDB->print(); + // // ICFG.print(); + // // LCASolver.dumpResults(); + // std::error_code EC; + // llvm::raw_fd_ostream ROS(LlvmFilePath + "_explicit_esg.dot", EC); + // assert(!EC); + // LCASolver.getExplicitESG().printAsDot(ROS); + // } + auto [LastInst, InterestingFact] = + PathTracingTest::getInterestingInstFact(IRDB); + // llvm::outs() << "Target instruction: " << psr::llvmIRToString(LastInst); + // llvm::outs() << "\nTarget data-flow fact: " + // << psr::llvmIRToString(InterestingFact) << '\n'; + + const auto *InterestingFactInst = + llvm::dyn_cast(InterestingFact); + ASSERT_FALSE(InterestingFact->getType()->isVoidTy()); + ASSERT_NE(nullptr, InterestingFactInst); + + psr::PathSensitivityManager PSM( + &LCASolver.getExplicitESG()); + + auto Dag = PSM.pathsDagToInLLVMSSA(InterestingFactInst, InterestingFact, + psr::PathSensitivityConfig{}); + + // psr::printGraph(Dag, llvm::outs(), "", [](const auto &Node) { + // std::string Str; + // llvm::raw_string_ostream ROS(Str); + // ROS << '['; + // llvm::interleaveComma(Node, ROS, [&ROS](const auto *Inst) { + // ROS << psr::getMetaDataID(Inst); + // }); + // ROS << ']'; + + // return Str; + // }); + auto Paths = getPaths(Dag); + ASSERT_EQ(1, Paths.size()); + + // TODO: Should the "18" be removed? + std::vector Gt = {"17", "16", "5", "3", "2", "1", + "0", "15", "14", "13", "12", "11", + "10", "9", "8", "7", "6", "18"}; + EXPECT_EQ(Gt, Paths[0]); +} + +} // namespace + +// main function for the test case +int main(int Argc, char **Argv) { + ::testing::InitGoogleTest(&Argc, Argv); + return RUN_ALL_TESTS(); +}