Skip to content

Commit d7cb8ea

Browse files
fabianbs96fabianbs96
authored
Fix result[s]AtInLLVMSSA() (#620)
* Fix resultsAtInLLVMSSA in case the statement is an invoke inst * minor * small fix * Assert overapproximation (optionally) * minor
1 parent 285f03e commit d7cb8ea

File tree

4 files changed

+174
-21
lines changed

4 files changed

+174
-21
lines changed

‎include/phasar/DataFlow/IfdsIde/SolverResults.h‎

Lines changed: 4 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -94,19 +94,8 @@ class SolverResultsBase {
9494
std::is_same_v<std::decay_t<std::remove_pointer_t<NTy>>,
9595
llvm::Instruction>,
9696
std::unordered_map<d_t, l_t>>
97-
resultsAtInLLVMSSA(ByConstRef<n_t> Stmt, bool StripZero = false) {
98-
std::unordered_map<d_t, l_t> Result = [this, Stmt]() {
99-
if (Stmt->getType()->isVoidTy()) {
100-
return self().Results.row(Stmt);
101-
}
102-
assert(Stmt->getNextNode() && "Expected to find a valid successor node!");
103-
return self().Results.row(Stmt->getNextNode());
104-
}();
105-
if (StripZero) {
106-
Result.erase(self().ZV);
107-
}
108-
return Result;
109-
}
97+
resultsAtInLLVMSSA(ByConstRef<n_t> Stmt, bool AllowOverapproximation = false,
98+
bool StripZero = false);
11099

111100
/// Returns the L-type result at the given statement for the given data-flow
112101
/// fact while respecting LLVM's SSA semantics.
@@ -128,13 +117,8 @@ class SolverResultsBase {
128117
std::is_same_v<std::decay_t<std::remove_pointer_t<NTy>>,
129118
llvm::Instruction>,
130119
l_t>
131-
resultAtInLLVMSSA(ByConstRef<n_t> Stmt, d_t Value) {
132-
if (Stmt->getType()->isVoidTy()) {
133-
return self().Results.get(Stmt, Value);
134-
}
135-
assert(Stmt->getNextNode() && "Expected to find a valid successor node!");
136-
return self().Results.get(Stmt->getNextNode(), Value);
137-
}
120+
resultAtInLLVMSSA(ByConstRef<n_t> Stmt, d_t Value,
121+
bool AllowOverapproximation = false);
138122

139123
[[nodiscard]] std::vector<typename Table<n_t, d_t, l_t>::Cell>
140124
getAllResultEntries() const {

‎include/phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h‎

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,169 @@
1+
/******************************************************************************
2+
* Copyright (c) 2017 Philipp Schubert.
3+
* All rights reserved. This program and the accompanying materials are made
4+
* available under the terms of LICENSE.txt.
5+
*
6+
* Contributors:
7+
* Philipp Schubert, Fabian Schiebel and others
8+
*****************************************************************************/
9+
10+
#ifndef PHASAR_PHASARLLVM_DATAFLOW_IFDSIDE_LLVMSOLVERRESULTS_H
11+
#define PHASAR_PHASARLLVM_DATAFLOW_IFDSIDE_LLVMSOLVERRESULTS_H
12+
13+
#include "phasar/DataFlow/IfdsIde/SolverResults.h"
14+
#include "phasar/Utils/JoinLattice.h"
15+
#include "phasar/Utils/Logger.h"
16+
17+
#include "llvm/IR/BasicBlock.h"
18+
#include "llvm/IR/CFG.h"
19+
#include "llvm/IR/IntrinsicInst.h"
20+
#include "llvm/Support/ErrorHandling.h"
21+
22+
namespace psr::detail {
23+
24+
template <typename Derived, typename N, typename D, typename L>
25+
template <typename NTy>
26+
auto SolverResultsBase<Derived, N, D, L>::resultsAtInLLVMSSA(
27+
ByConstRef<n_t> Stmt, bool AllowOverapproximation, bool StripZero) ->
28+
typename std::enable_if_t<
29+
std::is_same_v<std::decay_t<std::remove_pointer_t<NTy>>,
30+
llvm::Instruction>,
31+
std::unordered_map<d_t, l_t>> {
32+
std::unordered_map<d_t, l_t> Result = [this, Stmt, AllowOverapproximation]() {
33+
if (Stmt->getType()->isVoidTy()) {
34+
return self().Results.row(Stmt);
35+
}
36+
if (!Stmt->getNextNode()) {
37+
auto GetStartRow = [this](const llvm::BasicBlock *BB) -> decltype(auto) {
38+
const auto *First = &BB->front();
39+
if (llvm::isa<llvm::DbgInfoIntrinsic>(First)) {
40+
First = First->getNextNonDebugInstruction();
41+
}
42+
return self().Results.row(First);
43+
};
44+
45+
// We have reached the end of a BasicBlock. If there is a successor BB
46+
// that only has one predecessor, we are lucky and can just take results
47+
// from there
48+
for (const llvm::BasicBlock *Succ : llvm::successors(Stmt)) {
49+
if (Succ->hasNPredecessors(1)) {
50+
return GetStartRow(Succ);
51+
}
52+
}
53+
54+
if (!AllowOverapproximation) {
55+
llvm::report_fatal_error("[resultsAtInLLVMSSA]: Cannot precisely "
56+
"collect the results at instruction " +
57+
llvm::Twine(llvmIRToString(Stmt)));
58+
}
59+
60+
// There is no successor with only one predecessor.
61+
// All we can do is merge the results from all successors to get a sound
62+
// overapproximation. This is not optimal and may be replaced in the
63+
// future.
64+
PHASAR_LOG_LEVEL(WARNING, "[resultsAtInLLVMSSA]: Cannot precisely "
65+
"collect the results at instruction "
66+
<< llvmIRToString(Stmt)
67+
<< ". Use a sound, but potentially "
68+
"imprecise overapproximation");
69+
std::unordered_map<d_t, l_t> Ret;
70+
for (const llvm::BasicBlock *Succ : llvm::successors(Stmt)) {
71+
const auto &Row = GetStartRow(Succ);
72+
for (const auto &[Fact, Value] : Row) {
73+
auto [It, Inserted] = Ret.try_emplace(Fact, Value);
74+
if (!Inserted && Value != It->second) {
75+
if constexpr (HasJoinLatticeTraits<l_t>) {
76+
It->second = JoinLatticeTraits<l_t>::join(It->second, Value);
77+
} else {
78+
// We have no way of correctly merging, so set the value to the
79+
// default constructed l_t hoping it marks BOTTOM.
80+
It->second = l_t();
81+
}
82+
}
83+
}
84+
}
85+
return Ret;
86+
}
87+
assert(Stmt->getNextNode() && "Expected to find a valid successor node!");
88+
return self().Results.row(Stmt->getNextNode());
89+
}();
90+
if (StripZero) {
91+
Result.erase(self().ZV);
92+
}
93+
return Result;
94+
}
95+
96+
template <typename Derived, typename N, typename D, typename L>
97+
template <typename NTy>
98+
auto SolverResultsBase<Derived, N, D, L>::resultAtInLLVMSSA(
99+
ByConstRef<n_t> Stmt, d_t Value, bool AllowOverapproximation) ->
100+
typename std::enable_if_t<
101+
std::is_same_v<std::decay_t<std::remove_pointer_t<NTy>>,
102+
llvm::Instruction>,
103+
l_t> {
104+
if (Stmt->getType()->isVoidTy()) {
105+
return self().Results.get(Stmt, Value);
106+
}
107+
if (!Stmt->getNextNode()) {
108+
auto GetStartVal = [this,
109+
&Value](const llvm::BasicBlock *BB) -> decltype(auto) {
110+
const auto *First = &BB->front();
111+
if (llvm::isa<llvm::DbgInfoIntrinsic>(First)) {
112+
First = First->getNextNonDebugInstruction();
113+
}
114+
return self().Results.get(First, Value);
115+
};
116+
117+
// We have reached the end of a BasicBlock. If there is a successor BB
118+
// that only has one predecessor, we are lucky and can just take results
119+
// from there
120+
for (const llvm::BasicBlock *Succ : llvm::successors(Stmt)) {
121+
if (Succ->hasNPredecessors(1)) {
122+
return GetStartVal(Succ);
123+
}
124+
}
125+
126+
if (!AllowOverapproximation) {
127+
llvm::report_fatal_error("[resultsAtInLLVMSSA]: Cannot precisely "
128+
"collect the results at instruction " +
129+
llvm::Twine(llvmIRToString(Stmt)));
130+
}
131+
132+
// There is no successor with only one predecessor.
133+
// All we can do is merge the results from all successors to get a sound
134+
// overapproximation. This is not optimal and may be replaced in the
135+
// future.
136+
PHASAR_LOG_LEVEL(WARNING, "[resultAtInLLVMSSA]: Cannot precisely "
137+
"collect the results at instruction "
138+
<< *Stmt
139+
<< ". Use a sound, but potentially "
140+
"imprecise overapproximation");
141+
auto It = llvm::succ_begin(Stmt);
142+
auto End = llvm::succ_end(Stmt);
143+
l_t Ret{};
144+
if (It != End) {
145+
Ret = GetStartVal(*It);
146+
for (++It; It != End; ++It) {
147+
const auto &Val = GetStartVal(*It);
148+
if constexpr (HasJoinLatticeTraits<l_t>) {
149+
Ret = JoinLatticeTraits<l_t>::join(Ret, Val);
150+
if (Ret == JoinLatticeTraits<l_t>::bottom()) {
151+
break;
152+
}
153+
} else {
154+
if (Ret != Val) {
155+
// We have no way of correctly merging, so set the value to the
156+
// default constructed l_t hoping it marks BOTTOM.
157+
return {};
158+
}
159+
}
160+
}
161+
}
162+
return Ret;
163+
}
164+
assert(Stmt->getNextNode() && "Expected to find a valid successor node!");
165+
return self().Results.get(Stmt->getNextNode(), Value);
166+
}
167+
} // namespace psr::detail
168+
169+
#endif // PHASAR_PHASARLLVM_DATAFLOW_IFDSIDE_LLVMSOLVERRESULTS_H

‎include/phasar/PhasarLLVM/DataFlow/IfdsIde/Problems/IDEInstInteractionAnalysis.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@
1818
#include "phasar/Domain/LatticeDomain.h"
1919
#include "phasar/PhasarLLVM/DB/LLVMProjectIRDB.h"
2020
#include "phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMFlowFunctions.h"
21+
#include "phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMSolverResults.h"
2122
#include "phasar/PhasarLLVM/DataFlow/IfdsIde/LLVMZeroValue.h"
2223
#include "phasar/PhasarLLVM/Domain/LLVMAnalysisDomain.h"
2324
#include "phasar/PhasarLLVM/Pointer/LLVMAliasInfo.h"

‎lib/AnalysisStrategy/Strategies.cpp‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ namespace psr {
1616

1717
std::string toString(const AnalysisStrategy &S) {
1818
switch (S) {
19-
default:
2019
#define ANALYSIS_STRATEGY_TYPES(NAME, CMDFLAG, DESC) \
2120
case AnalysisStrategy::NAME: \
2221
return #NAME; \

0 commit comments

Comments
 (0)