Path Tracing (#640)

* Add explicit ExplodedSuperGraph and a version of the IDESolver that fills it with content. TODO: Add PathSensitivityManager + unittests

* Add more TODOs

* Add GraphTraits

* Add pathsDagTo (not tested yet)

* Add Z3 submodule

* Set Z3 version

* Add Z3-related stuff (WIP)

* Added now basic functionality for path sensitivity (compiles, but not tested yet)

* Implement LLVMPathConstraints

* Add unittest for PathTracking (C/C++ test files are still missing) and resolve a lot of compilation errors

* Make a lot of the unittests work (still not completed)

* Fix Config propagation

* Finally, fix all unittests

* minor

* redirect z3 submodule

* Checkout the right z3 branch

* bump z3

* add bulk dag-generation (not tested yet)

* Some more fixes

* Add filters to PSM

* Better integrate filter into PSM

* minor

* Improve on reverseDAG

* minor improvements in reverseDAG

* Bump z3

* Fix depdendency issue with utils->config

* Fix bugs indiced by reverse merging from development + bump z3

* Make Z3 optional

* Workaround weird cmake behavior

* Fix seeds in exploded supergraph

* Add forward minimize graph

* Add one Test for forward minimize DAG

* Fix in createEquivalentGraphFrom

* Fix filterOutUnreachableNodes

* Fix: DFAMinimizer edge comparison

* Fix compilation on ubuntu22

* Improve createEquivalentGraphFrom

* Resolve errors due to merging

* Fix z3 dependency

* Fix UAF when copying an ExplicitESG

* Get rid of NodeRef::DSI

* Fix compile error due to merge

* minor

* More const in Table

* Give the PathTracing Filters more power

* Fix null error

* Fix Path Tracing with chaotic edge saving due to new Worklist structure in IDESolver

* Some cleanup

* pre-commit

* Apply some review comments

* Write ESG to temp file instead of hard-coded file

* minor

* pre-commitIDESolver.h

* pre-commit Utilities.h

* trailing whitespace IDESolver.h

* Fix errors due to merge

* Integrate free-functions NToString and DToString into ExplicitESG

* Adapt invariants due to chaotic solving (worklist vs recursion)

* Add LLVMSSA version of pathsDagTo as temporary solution until f-IDESolverStrategy is merged

* minor

* Use system z3

* Find z3 from psr installation

* Assert size overflow

* Enable Z3 in CI

* fix naming issue

---------

Co-authored-by: Fabian Benedikt Schiebel <fabianbs@mail.uni-paderborn.de>
Co-authored-by: Sebastian Böhm <boehmseb@cs.uni-saarland.de>
Co-authored-by: Martin Mory <mmo@mail.upb.de>

Author: 4 people

.clang-tidy

@@ -31,7 +31,7 @@ Checks: '-*,
          modernize-*,
            -modernize-use-trailing-return-type,
          performance-*,
-         clang-analyzer-*,
+         clang-analyzer-*
         '
 
 FormatStyle:  LLVM

.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 .

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)
 

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

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

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

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<l_t> 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<n_t, d_t, EdgeFunction<l_t>>::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<l_t> 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<l_t> 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<n_t, n_t, std::map<d_t, container_type>> &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<l_t> f5 =
                 CachedFlowEdgeFunctions.getReturnEdgeFunction(

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 <typename AnalysisDomainTy,
+          typename Container = std::set<typename AnalysisDomainTy::d_t>>
+class PathAwareIDESolver : public IDESolver<AnalysisDomainTy, Container> {
+  using base_t = IDESolver<AnalysisDomainTy, Container>;
+
+public:
+  using domain_t = AnalysisDomainTy;
+  using n_t = typename base_t::n_t;
+  using d_t = typename base_t::d_t;
+  using i_t = typename base_t::i_t;
+  using container_type = typename base_t::container_type;
+
+  explicit PathAwareIDESolver(
+      IDETabulationProblem<domain_t, container_type> &Problem, const i_t *ICF)
+      : base_t(Problem, ICF), ESG(Problem.getZeroValue()) {
+
+    if (Problem.getIFDSIDESolverConfig().autoAddZero()) {
+      PHASAR_LOG_LEVEL(
+          WARNING,
+          "The PathAwareIDESolver is initialized with the option 'autoAddZero' "
+          "being set. This might degrade the quality of the computed paths!");
+    }
+  }
+
+  [[nodiscard]] const ExplodedSuperGraph<domain_t> &
+  getExplicitESG() const &noexcept {
+    return ESG;
+  }
+
+  [[nodiscard]] ExplodedSuperGraph<domain_t> &&getExplicitESG() &&noexcept {
+    return std::move(ESG);
+  }
+
+private:
+  void saveEdges(n_t Curr, n_t Succ, d_t CurrNode,
+                 const container_type &SuccNodes, ESGEdgeKind Kind) override {
+    ESG.saveEdges(std::move(Curr), std::move(CurrNode), std::move(Succ),
+                  SuccNodes, Kind);
+  }
+
+  ExplodedSuperGraph<domain_t> ESG;
+};
+
+template <typename ProblemTy>
+PathAwareIDESolver(ProblemTy &)
+    -> PathAwareIDESolver<typename ProblemTy::ProblemAnalysisDomain>;
+
+} // namespace psr
+
+#endif // PHASAR_DATAFLOW_IFDSIDE_SOLVER_PATHAWAREIDESOLVER_H

include/phasar/DataFlow/IfdsIde/SolverResults.h

@@ -232,6 +232,7 @@ class OwningSolverResults
   [[nodiscard]] operator SolverResults<N, D, L>() const &noexcept {
     return get();
   }
+
   operator SolverResults<N, D, L>() && = delete;
 
 private: