From 1077ce8dd15fb9e5018a9505556a29cb6889582b Mon Sep 17 00:00:00 2001 From: Fabian Schiebel Date: Fri, 12 May 2023 10:42:11 +0200 Subject: [PATCH 1/5] Fix resultsAtInLLVMSSA in case the statement is an invoke inst --- .../phasar/DataFlow/IfdsIde/SolverResults.h | 22 +-- .../DataFlow/IfdsIde/LLVMSolverResults.h | 155 ++++++++++++++++++ .../Problems/IDEInstInteractionAnalysis.h | 1 + 3 files changed, 158 insertions(+), 20 deletions(-) create mode 100644 include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h diff --git a/include/phasar/DataFlow/IfdsIde/SolverResults.h b/include/phasar/DataFlow/IfdsIde/SolverResults.h index 0e760878cb..6d59713e21 100644 --- a/include/phasar/DataFlow/IfdsIde/SolverResults.h +++ b/include/phasar/DataFlow/IfdsIde/SolverResults.h @@ -94,19 +94,7 @@ class SolverResultsBase { std::is_same_v>, llvm::Instruction>, std::unordered_map> - resultsAtInLLVMSSA(ByConstRef Stmt, bool StripZero = false) { - std::unordered_map Result = [this, Stmt]() { - if (Stmt->getType()->isVoidTy()) { - return self().Results.row(Stmt); - } - assert(Stmt->getNextNode() && "Expected to find a valid successor node!"); - return self().Results.row(Stmt->getNextNode()); - }(); - if (StripZero) { - Result.erase(self().ZV); - } - return Result; - } + resultsAtInLLVMSSA(ByConstRef Stmt, bool StripZero = false); /// Returns the L-type result at the given statement for the given data-flow /// fact while respecting LLVM's SSA semantics. @@ -128,13 +116,7 @@ class SolverResultsBase { std::is_same_v>, llvm::Instruction>, l_t> - resultAtInLLVMSSA(ByConstRef Stmt, d_t Value) { - if (Stmt->getType()->isVoidTy()) { - return self().Results.get(Stmt, Value); - } - assert(Stmt->getNextNode() && "Expected to find a valid successor node!"); - return self().Results.get(Stmt->getNextNode(), Value); - } + resultAtInLLVMSSA(ByConstRef Stmt, d_t Value); [[nodiscard]] std::vector::Cell> getAllResultEntries() const { diff --git a/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h b/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h new file mode 100644 index 0000000000..a30b155f6c --- /dev/null +++ b/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h @@ -0,0 +1,155 @@ +/****************************************************************************** + * Copyright (c) 2017 Philipp Schubert. + * All rights reserved. This program and the accompanying materials are made + * available under the terms of LICENSE.txt. + * + * Contributors: + * Philipp Schubert, Fabian Schiebel and others + *****************************************************************************/ + +#ifndef PHASAR_PHASARLLVM_DATAFLOW_IFDSIDE_LLVMSOLVERRESULTS_H +#define PHASAR_PHASARLLVM_DATAFLOW_IFDSIDE_LLVMSOLVERRESULTS_H + +#include "phasar/DataFlow/IfdsIde/SolverResults.h" +#include "phasar/Utils/JoinLattice.h" +#include "phasar/Utils/Logger.h" + +#include "llvm/IR/BasicBlock.h" +#include "llvm/IR/CFG.h" +#include "llvm/IR/IntrinsicInst.h" + +namespace psr::detail { + +template +template +auto SolverResultsBase::resultsAtInLLVMSSA( + ByConstRef Stmt, bool StripZero) -> + typename std::enable_if_t< + std::is_same_v>, + llvm::Instruction>, + std::unordered_map> { + std::unordered_map Result = [this, Stmt]() { + if (Stmt->getType()->isVoidTy()) { + return self().Results.row(Stmt); + } + if (!Stmt->getNextNode()) { + auto GetStartRow = [this](const llvm::BasicBlock *BB) -> decltype(auto) { + const auto *First = &BB->front(); + if (llvm::isa(First)) { + First = First->getNextNonDebugInstruction(); + } + return self().Results.row(First); + }; + + // We have reached the end of a BasicBlock. If there is a successor BB + // that only has one predecessor, we are lucky and can just take results + // from there + for (const llvm::BasicBlock *Succ : llvm::successors(Stmt)) { + if (Succ->hasNPredecessors(1)) { + return GetStartRow(Succ); + } + } + + // There is no successor with only one predecessor. + // All we can do is merge the results from all successors to get a sound + // overapproximation. This is not optimal and may be replaced in the + // future. + PHASAR_LOG_LEVEL(WARNING, "[resultsAtInLLVMSSA]: Cannot precisely " + "collect the results at instruction " + << llvmIRToString(Stmt) + << ". Use a sound, but potentially " + "imprecise overapproximation"); + std::unordered_map Ret; + for (const llvm::BasicBlock *Succ : llvm::successors(Stmt)) { + const auto &Row = GetStartRow(Succ); + for (const auto &[Fact, Value] : Row) { + auto [It, Inserted] = Ret.try_emplace(Fact, Value); + if (!Inserted && Value != It->second) { + if constexpr (HasJoinLatticeTraits) { + It->second = JoinLatticeTraits::join(It->second, Value); + } else { + // We have no way of correctly merging, so set the value to the + // default constructed l_t hoping it marks BOTTOM. + It->second = l_t(); + } + } + } + } + return Ret; + } + assert(Stmt->getNextNode() && "Expected to find a valid successor node!"); + return self().Results.row(Stmt->getNextNode()); + }(); + if (StripZero) { + Result.erase(self().ZV); + } + return Result; +} + +template +template +auto SolverResultsBase::resultAtInLLVMSSA( + ByConstRef Stmt, d_t Value) -> + typename std::enable_if_t< + std::is_same_v>, + llvm::Instruction>, + l_t> { + if (Stmt->getType()->isVoidTy()) { + return self().Results.get(Stmt, Value); + } + if (!Stmt->getNextNode()) { + auto GetStartVal = [this, + &Value](const llvm::BasicBlock *BB) -> decltype(auto) { + const auto *First = &BB->front(); + if (llvm::isa(First)) { + First = First->getNextNonDebugInstruction(); + } + return self().Results.get(First, Value); + }; + + // We have reached the end of a BasicBlock. If there is a successor BB + // that only has one predecessor, we are lucky and can just take results + // from there + for (const llvm::BasicBlock *Succ : llvm::successors(Stmt)) { + if (Succ->hasNPredecessors(1)) { + return GetStartVal(Succ); + } + } + + // There is no successor with only one predecessor. + // All we can do is merge the results from all successors to get a sound + // overapproximation. This is not optimal and may be replaced in the + // future. + PHASAR_LOG_LEVEL(WARNING, "[resultAtInLLVMSSA]: Cannot precisely " + "collect the results at instruction " + << *Stmt + << ". Use a sound, but potentially " + "imprecise overapproximation"); + auto It = llvm::succ_begin(Stmt); + auto End = llvm::succ_end(Stmt); + l_t Ret{}; + if (It != End) { + Ret = GetStartVal(*It); + for (++It; It != End; ++It) { + const auto &Val = GetStartVal(*It); + if constexpr (HasJoinLatticeTraits) { + Ret = JoinLatticeTraits::join(Ret, Value); + if (Ret == JoinLatticeTraits::bottom()) { + break; + } + } else { + // We have no way of correctly merging, so set the value to the + // default constructed l_t hoping it marks BOTTOM. + Ret = l_t(); + break; + } + } + } + return Ret; + } + assert(Stmt->getNextNode() && "Expected to find a valid successor node!"); + return self().Results.get(Stmt->getNextNode(), Value); +} +} // namespace psr::detail + +#endif // PHASAR_PHASARLLVM_DATAFLOW_IFDSIDE_LLVMSOLVERRESULTS_H diff --git a/include/phasar/PhasarLLVM/DataFlow/IfdsIde/Problems/IDEInstInteractionAnalysis.h b/include/phasar/PhasarLLVM/DataFlow/IfdsIde/Problems/IDEInstInteractionAnalysis.h index c39808640e..c0824c7a5c 100644 --- a/include/phasar/PhasarLLVM/DataFlow/IfdsIde/Problems/IDEInstInteractionAnalysis.h +++ b/include/phasar/PhasarLLVM/DataFlow/IfdsIde/Problems/IDEInstInteractionAnalysis.h @@ -18,6 +18,7 @@ #include "phasar/Domain/LatticeDomain.h" #include "phasar/PhasarLLVM/DB/LLVMProjectIRDB.h" #include "phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMFlowFunctions.h" +#include "phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h" #include "phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMZeroValue.h" #include "phasar/PhasarLLVM/Domain/LLVMAnalysisDomain.h" #include "phasar/PhasarLLVM/Pointer/LLVMAliasInfo.h" From 073e06aadaf4b9d6e3ae5076feacbe6e1c0a43f1 Mon Sep 17 00:00:00 2001 From: Fabian Schiebel Date: Fri, 12 May 2023 12:32:35 +0200 Subject: [PATCH 2/5] minor --- include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h | 2 +- lib/AnalysisStrategy/Strategies.cpp | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h b/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h index a30b155f6c..cc713f3240 100644 --- a/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h +++ b/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h @@ -133,7 +133,7 @@ auto SolverResultsBase::resultAtInLLVMSSA( for (++It; It != End; ++It) { const auto &Val = GetStartVal(*It); if constexpr (HasJoinLatticeTraits) { - Ret = JoinLatticeTraits::join(Ret, Value); + Ret = JoinLatticeTraits::join(Ret, Val); if (Ret == JoinLatticeTraits::bottom()) { break; } diff --git a/lib/AnalysisStrategy/Strategies.cpp b/lib/AnalysisStrategy/Strategies.cpp index a05ba58488..844b4e650c 100644 --- a/lib/AnalysisStrategy/Strategies.cpp +++ b/lib/AnalysisStrategy/Strategies.cpp @@ -16,7 +16,6 @@ namespace psr { std::string toString(const AnalysisStrategy &S) { switch (S) { - default: #define ANALYSIS_STRATEGY_TYPES(NAME, CMDFLAG, DESC) \ case AnalysisStrategy::NAME: \ return #NAME; \ From e372831fc22580e29b38901394d909d4dbba2c90 Mon Sep 17 00:00:00 2001 From: Fabian Schiebel Date: Mon, 15 May 2023 17:47:23 +0200 Subject: [PATCH 3/5] small fix --- .../PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h b/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h index cc713f3240..d6c5f7c85a 100644 --- a/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h +++ b/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h @@ -138,10 +138,11 @@ auto SolverResultsBase::resultAtInLLVMSSA( break; } } else { - // We have no way of correctly merging, so set the value to the - // default constructed l_t hoping it marks BOTTOM. - Ret = l_t(); - break; + if (Ret != Val) { + // We have no way of correctly merging, so set the value to the + // default constructed l_t hoping it marks BOTTOM. + return {}; + } } } } From bc91b4164455c9759069c34b5bb99479e25076fb Mon Sep 17 00:00:00 2001 From: Fabian Schiebel Date: Tue, 16 May 2023 10:45:41 +0200 Subject: [PATCH 4/5] Assert overapproximation (optionally) --- .../phasar/DataFlow/IfdsIde/SolverResults.h | 6 +++-- .../DataFlow/IfdsIde/LLVMSolverResults.h | 23 ++++++++++++++++--- 2 files changed, 24 insertions(+), 5 deletions(-) diff --git a/include/phasar/DataFlow/IfdsIde/SolverResults.h b/include/phasar/DataFlow/IfdsIde/SolverResults.h index 6d59713e21..6a5671a50e 100644 --- a/include/phasar/DataFlow/IfdsIde/SolverResults.h +++ b/include/phasar/DataFlow/IfdsIde/SolverResults.h @@ -94,7 +94,8 @@ class SolverResultsBase { std::is_same_v>, llvm::Instruction>, std::unordered_map> - resultsAtInLLVMSSA(ByConstRef Stmt, bool StripZero = false); + resultsAtInLLVMSSA(ByConstRef Stmt, bool AllowOverapproximation = false, + bool StripZero = false); /// Returns the L-type result at the given statement for the given data-flow /// fact while respecting LLVM's SSA semantics. @@ -116,7 +117,8 @@ class SolverResultsBase { std::is_same_v>, llvm::Instruction>, l_t> - resultAtInLLVMSSA(ByConstRef Stmt, d_t Value); + resultAtInLLVMSSA(ByConstRef Stmt, d_t Value, + bool AllowOverapproximation = false); [[nodiscard]] std::vector::Cell> getAllResultEntries() const { diff --git a/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h b/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h index d6c5f7c85a..de74f22d21 100644 --- a/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h +++ b/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h @@ -17,18 +17,19 @@ #include "llvm/IR/BasicBlock.h" #include "llvm/IR/CFG.h" #include "llvm/IR/IntrinsicInst.h" +#include "llvm/Support/ErrorHandling.h" namespace psr::detail { template template auto SolverResultsBase::resultsAtInLLVMSSA( - ByConstRef Stmt, bool StripZero) -> + ByConstRef Stmt, bool AllowOverapproximation, bool StripZero) -> typename std::enable_if_t< std::is_same_v>, llvm::Instruction>, std::unordered_map> { - std::unordered_map Result = [this, Stmt]() { + std::unordered_map Result = [this, Stmt, AllowOverapproximation]() { if (Stmt->getType()->isVoidTy()) { return self().Results.row(Stmt); } @@ -50,6 +51,14 @@ auto SolverResultsBase::resultsAtInLLVMSSA( } } + if (!AllowOverapproximation) { + llvm::report_fatal_error("[resultsAtInLLVMSSA]: Cannot precisely " + "collect the results at instruction " + + llvm::Twine(llvmIRToString(Stmt)) + + ". Use a sound, but potentially " + "imprecise overapproximation"); + } + // There is no successor with only one predecessor. // All we can do is merge the results from all successors to get a sound // overapproximation. This is not optimal and may be replaced in the @@ -89,7 +98,7 @@ auto SolverResultsBase::resultsAtInLLVMSSA( template template auto SolverResultsBase::resultAtInLLVMSSA( - ByConstRef Stmt, d_t Value) -> + ByConstRef Stmt, d_t Value, bool AllowOverapproximation) -> typename std::enable_if_t< std::is_same_v>, llvm::Instruction>, @@ -116,6 +125,14 @@ auto SolverResultsBase::resultAtInLLVMSSA( } } + if (!AllowOverapproximation) { + llvm::report_fatal_error("[resultsAtInLLVMSSA]: Cannot precisely " + "collect the results at instruction " + + llvm::Twine(llvmIRToString(Stmt)) + + ". Use a sound, but potentially " + "imprecise overapproximation"); + } + // There is no successor with only one predecessor. // All we can do is merge the results from all successors to get a sound // overapproximation. This is not optimal and may be replaced in the From ed8aea0fa2dfacd6184629f21d03d1b8e59713ea Mon Sep 17 00:00:00 2001 From: Fabian Schiebel Date: Tue, 16 May 2023 11:08:55 +0200 Subject: [PATCH 5/5] minor --- .../PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h b/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h index de74f22d21..0e334cb336 100644 --- a/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h +++ b/include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h @@ -54,9 +54,7 @@ auto SolverResultsBase::resultsAtInLLVMSSA( if (!AllowOverapproximation) { llvm::report_fatal_error("[resultsAtInLLVMSSA]: Cannot precisely " "collect the results at instruction " + - llvm::Twine(llvmIRToString(Stmt)) + - ". Use a sound, but potentially " - "imprecise overapproximation"); + llvm::Twine(llvmIRToString(Stmt))); } // There is no successor with only one predecessor. @@ -128,9 +126,7 @@ auto SolverResultsBase::resultAtInLLVMSSA( if (!AllowOverapproximation) { llvm::report_fatal_error("[resultsAtInLLVMSSA]: Cannot precisely " "collect the results at instruction " + - llvm::Twine(llvmIRToString(Stmt)) + - ". Use a sound, but potentially " - "imprecise overapproximation"); + llvm::Twine(llvmIRToString(Stmt))); } // There is no successor with only one predecessor.