33
44#include " phasar/DataFlow/IfdsIde/Solver/IterativeIDESolverResults.h"
55#include " phasar/Utils/ByRef.h"
6+ #include " phasar/Utils/Printer.h"
7+ #include " phasar/Utils/Utilities.h"
68
79#include " llvm/ADT/STLExtras.h"
10+ #include " llvm/ADT/SmallVector.h"
811
912#include < cassert>
1013#include < cstddef>
1114#include < set>
1215#include < unordered_map>
1316#include < utility>
1417
18+ namespace llvm {
19+ class Instruction ;
20+ class Value ;
21+ } // namespace llvm
22+
1523namespace psr {
1624
1725namespace detail {
@@ -31,7 +39,7 @@ class IdBasedSolverResultsBase {
3139
3240 // --v Needed for llvm::mapped_iterator
3341 // NOLINTNEXTLINE(readability-const-return-type)
34- const std::pair<const d_t &, const l_t & >
42+ const std::pair<ByConstRef< d_t >, ByConstRef< l_t > >
3543 operator ()(ByConstRef<typename row_map_t ::value_type> Entry) const {
3644 return {Results->FactCompressor [Entry.first ],
3745 Results->ValCompressor [Entry.second ]};
@@ -81,6 +89,7 @@ class IdBasedSolverResultsBase {
8189 }
8290
8391 [[nodiscard]] size_t size () const noexcept { return Row->size (); }
92+ [[nodiscard]] bool empty () const noexcept { return Row->empty (); }
8493
8594 private:
8695 const detail::IterativeIDESolverResults<n_t , d_t , l_t > *Results{};
@@ -174,6 +183,49 @@ class IdBasedSolverResultsBase {
174183 }
175184 }
176185
186+ // / Returns the data-flow results at the given statement while respecting
187+ // / LLVM's SSA semantics.
188+ // /
189+ // / An example: when a value is loaded and the location loaded from, here
190+ // / variable 'i', is a data-flow fact that holds, then the loaded value '%0'
191+ // / will usually be generated and also holds. However, due to the underlying
192+ // / theory (and respective implementation) this load instruction causes the
193+ // / loaded value to be generated and thus, it will be valid only AFTER the
194+ // / load instruction, i.e., at the successor instruction.
195+ // /
196+ // / %0 = load i32, i32* %i, align 4
197+ // /
198+ // / This result accessor function returns the results at the successor
199+ // / instruction(s) reflecting that the expression on the left-hand side holds
200+ // / if the expression on the right-hand side holds.
201+ [[nodiscard]] std::unordered_map<d_t , l_t >
202+ resultsAtInLLVMSSA (ByConstRef<n_t > Stmt,
203+ bool AllowOverapproximation = false ) const
204+ requires same_as_decay<std::remove_pointer_t <n_t >, llvm::Instruction>;
205+
206+ // / Returns the L-type result at the given statement for the given data-flow
207+ // / fact while respecting LLVM's SSA semantics.
208+ // /
209+ // / An example: when a value is loaded and the location loaded from, here
210+ // / variable 'i', is a data-flow fact that holds, then the loaded value '%0'
211+ // / will usually be generated and also holds. However, due to the underlying
212+ // / theory (and respective implementation) this load instruction causes the
213+ // / loaded value to be generated and thus, it will be valid only AFTER the
214+ // / load instruction, i.e., at the successor instruction.
215+ // /
216+ // / %0 = load i32, i32* %i, align 4
217+ // /
218+ // / This result accessor function returns the results at the successor
219+ // / instruction(s) reflecting that the expression on the left-hand side holds
220+ // / if the expression on the right-hand side holds.
221+ [[nodiscard]] l_t resultAtInLLVMSSA (ByConstRef<n_t > Stmt, d_t Value,
222+ bool AllowOverapproximation = false ) const
223+ requires same_as_decay<std::remove_pointer_t<n_t>, llvm::Instruction>;
224+
225+ template <typename ICFGTy>
226+ void dumpResults (const ICFGTy &ICF ,
227+ llvm::raw_ostream &OS = llvm::outs()) const ;
228+
177229private:
178230 [[nodiscard]] constexpr const auto &results () const noexcept {
179231 return static_cast <const Derived *>(this )->resultsImpl ();
@@ -219,6 +271,17 @@ class OwningIdBasedSolverResults
219271 assert (this ->Results != nullptr );
220272 }
221273
274+ [[nodiscard]] IdBasedSolverResults<N, D, L> get () const & noexcept {
275+ return IdBasedSolverResults<N, D, L>{Results.get ()};
276+ }
277+ IdBasedSolverResults<N, D, L> get () && = delete;
278+
279+ [[nodiscard]] operator IdBasedSolverResults<N, D, L>() const & noexcept {
280+ return get ();
281+ }
282+
283+ operator IdBasedSolverResults<N, D, L>() && = delete ;
284+
222285private:
223286 [[nodiscard]] constexpr const auto &resultsImpl () const noexcept {
224287 assert (Results != nullptr );
@@ -227,6 +290,57 @@ class OwningIdBasedSolverResults
227290
228291 std::unique_ptr<const detail::IterativeIDESolverResults<N, D, L>> Results{};
229292};
293+
294+ // For sorting the results in dumpResults()
295+ std::string getMetaDataID (const llvm::Value *V);
296+
297+ template <typename Derived, typename N, typename D, typename L>
298+ template <typename ICFGTy>
299+ void detail::IdBasedSolverResultsBase<Derived, N, D, L>::dumpResults(
300+ const ICFGTy &ICF , llvm::raw_ostream &OS ) const {
301+ using f_t = typename ICFGTy::f_t ;
302+
303+ auto ResultEntries = llvm::to_vector (getAllResultEntries ());
304+
305+ std::ranges::sort (ResultEntries, [](const auto &Lhs, const auto &Rhs) {
306+ const auto &LRow = std::get<0 >(Lhs);
307+ const auto &RRow = std::get<0 >(Rhs);
308+ if constexpr (std::is_same_v<n_t , const llvm::Instruction *>) {
309+ return StringIDLess{}(getMetaDataID (LRow), getMetaDataID (RRow));
310+ } else {
311+ // If non-LLVM IR is used
312+ return LRow < RRow;
313+ }
314+ });
315+
316+ OS << " \n ***************************************************************\n "
317+ << " * Raw IterativeIDESolver results *\n "
318+ << " ***************************************************************\n " ;
319+
320+ f_t PrevFn = f_t {};
321+ f_t CurrFn = f_t {};
322+
323+ for (const auto &[Row, Column] : ResultEntries) {
324+ if (Column.empty ()) {
325+ continue ;
326+ }
327+ CurrFn = ICF .getFunctionOf (Row);
328+ if (PrevFn != CurrFn) {
329+ PrevFn = CurrFn;
330+ OS << " \n\n ============ Results for function '" +
331+ ICF .getFunctionName (CurrFn) + " ' ============\n " ;
332+ }
333+
334+ std::string NString = NToString (Row);
335+ std::string Line (NString.size (), ' -' );
336+ OS << " \n\n N: " << NString << " \n ---" << Line << ' \n ' ;
337+
338+ for (const auto &[Col, Val] : Column) {
339+ OS << " \t D: " << DToString (Col) << " | V: " << LToString (Val) << ' \n ' ;
340+ }
341+ }
342+ OS << ' \n ' ;
343+ }
230344} // namespace psr
231345
232346#endif // PHASAR_PHASARLLVM_DATAFLOWSOLVER_IFDSIDE_SOLVER_IDBASEDSOLVERRESULTS_H
0 commit comments