Skip to content

Commit 764550e

Browse files
authored
Update phasar's SVF bindings to support SVF-3.1 and SVF-3.2 (#812)
1 parent dbeeb6f commit 764550e

7 files changed

Lines changed: 103 additions & 122 deletions

File tree

CMakeLists.txt

Lines changed: 21 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -356,22 +356,27 @@ if(PHASAR_IN_TREE)
356356
set (PHASAR_USE_Z3 OFF)
357357
else()
358358
if(PHASAR_USE_Z3)
359-
# This z3-version is the same version LLVM requires; however, we cannot just use Z3 via the LLVM interface
360-
# as it lacks some functionality (such as z3::expr::simplify()) that we require
361-
362-
# FindZ3.cmake by llvm tries to compile a snippet with Z3 which crashes on arm with sanitizers enabled
363-
set(SAFE_CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS}")
364-
set(CMAKE_CXX_FLAGS "")
365-
find_package(Z3 4.7.1 REQUIRED)
366-
set(CMAKE_CXX_FLAGS "${SAFE_CMAKE_CXX_FLAGS}")
367-
368-
if(Z3_FOUND)
369-
if (NOT TARGET z3)
370-
add_library(z3 IMPORTED SHARED)
371-
set_property(TARGET z3 PROPERTY
372-
IMPORTED_LOCATION ${Z3_LIBRARIES})
373-
set_property(TARGET z3 PROPERTY
374-
INTERFACE_INCLUDE_DIRECTORIES ${Z3_INCLUDE_DIR})
359+
if (TARGET z3::libz3)
360+
# When including SVF, it also tries to find z3, but in addition to LLVM's search it already creates a target: z3::libz3.
361+
# Reuse it here:
362+
if(NOT TARGET z3)
363+
add_library(z3 ALIAS z3::libz3)
364+
endif()
365+
else()
366+
# FindZ3.cmake by llvm tries to compile a snippet with Z3 which crashes on arm with sanitizers enabled
367+
set(SAFE_CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS}")
368+
set(CMAKE_CXX_FLAGS "")
369+
find_package(Z3 REQUIRED)
370+
set(CMAKE_CXX_FLAGS "${SAFE_CMAKE_CXX_FLAGS}")
371+
372+
if(Z3_FOUND)
373+
if (NOT TARGET z3)
374+
add_library(z3 IMPORTED SHARED)
375+
set_target_properties(z3 PROPERTIES
376+
IMPORTED_LOCATION ${Z3_LIBRARIES}
377+
INTERFACE_INCLUDE_DIRECTORIES ${Z3_INCLUDE_DIR}
378+
)
379+
endif()
375380
endif()
376381
endif()
377382
endif()

lib/PhasarLLVM/Pointer/SVF/CMakeLists.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,3 +22,5 @@ add_phasar_library(phasar_llvm_pointer_svf
2222

2323
target_include_directories(phasar_llvm_pointer_svf SYSTEM PRIVATE ${SVF_INSTALL_INCLUDE_DIR})
2424
target_link_directories(phasar_llvm_pointer_svf PUBLIC ${SVF_INSTALL_LIB_DIR})
25+
# Such that SVF finds its extapi.bc without system-wide installation:
26+
target_compile_options(phasar_llvm_pointer_svf PRIVATE -DPHASAR_SVF_INSTALL_LIBDIR="${SVF_INSTALL_LIBDIR}")

lib/PhasarLLVM/Pointer/SVF/InitSVF.cpp

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,12 @@ static psr::EmptyType initializeSVFImpl() {
1212
char EmptyStr[] = "";
1313
char NoAliasCheck[] = "-alias-check=false";
1414
char NoStat[] = "-stat=false";
15+
char Extapi[] = "-extapi=" PHASAR_SVF_INSTALL_LIBDIR "/extapi.bc";
1516
char *MockArgv[] = {
1617
EmptyStr,
1718
NoAliasCheck,
1819
NoStat,
20+
Extapi,
1921
};
2022
OptionBase::parseOptions(std::size(MockArgv), MockArgv, "", "");
2123

@@ -33,14 +35,8 @@ void psr::initializeSVF() {
3335
(void)SVFInitialized;
3436
}
3537

36-
SVF::SVFModule *psr::initSVFModule(psr::LLVMProjectIRDB &IRDB) {
38+
void psr::initSVFModule(psr::LLVMProjectIRDB &IRDB) {
3739
psr::initializeSVF();
3840

39-
auto *Mod = SVF::LLVMModuleSet::buildSVFModule(*IRDB.getModule());
40-
if (!Mod) {
41-
throw std::runtime_error(
42-
"SVF failed to create an SVFModule from an llvm::Module!");
43-
}
44-
45-
return Mod;
41+
SVF::LLVMModuleSet::buildSVFModule(*IRDB.getModule());
4642
}

lib/PhasarLLVM/Pointer/SVF/InitSVF.h

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,9 @@
22

33
#include "llvm/Support/Compiler.h"
44

5-
namespace SVF {
6-
class SVFModule;
7-
} // namespace SVF
8-
95
namespace psr {
106
class LLVMProjectIRDB;
117

128
LLVM_LIBRARY_VISIBILITY void initializeSVF();
13-
LLVM_LIBRARY_VISIBILITY SVF::SVFModule *
14-
initSVFModule(psr::LLVMProjectIRDB &IRDB);
9+
LLVM_LIBRARY_VISIBILITY void initSVFModule(psr::LLVMProjectIRDB &IRDB);
1510
} // namespace psr

lib/PhasarLLVM/Pointer/SVF/PhasarSVFUtils.h

Lines changed: 16 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -6,44 +6,39 @@
66
#include "Util/GeneralType.h"
77

88
namespace psr {
9+
10+
[[nodiscard]] inline const llvm::Value *
11+
svfVarToLLVMOrNull(const SVF::SVFVar *Var, SVF::LLVMModuleSet &ModSet) {
12+
if (ModSet.hasLLVMValue(Var)) {
13+
return ModSet.getLLVMValue(Var);
14+
}
15+
16+
return nullptr;
17+
}
18+
919
[[nodiscard]] inline const llvm::Value *
1020
pointerNodeToLLVMOrNull(SVF::NodeID Nod, SVF::LLVMModuleSet &ModSet,
1121
SVF::SVFIR &PAG) {
1222

1323
if (const SVF::SVFVar *Var = PAG.getGNode(Nod)) {
14-
if (const auto *Val = Var->getValue()) {
15-
if (const auto *LLVMVal = ModSet.getLLVMValue(Val)) {
16-
return LLVMVal;
17-
}
18-
}
24+
return svfVarToLLVMOrNull(Var, ModSet);
1925
}
2026
return nullptr;
2127
}
2228

2329
[[nodiscard]] inline const llvm::Value *
2430
objectNodeToLLVMOrNull(SVF::NodeID Nod, SVF::LLVMModuleSet &ModSet,
2531
SVF::SVFIR &PAG) {
26-
if (const SVF::MemObj *Mem = PAG.getObject(Nod)) {
27-
if (const auto *Val = Mem->getValue()) {
28-
if (const auto *LLVMVal = ModSet.getLLVMValue(Val)) {
29-
return LLVMVal;
30-
}
31-
}
32-
}
33-
return nullptr;
32+
return pointerNodeToLLVMOrNull(Nod, ModSet, PAG);
3433
}
3534

3635
[[nodiscard]] inline SVF::NodeID getNodeId(const llvm::Value *Pointer,
37-
SVF::LLVMModuleSet &ModSet,
38-
SVF::SVFIR &PAG) {
39-
auto *Nod = ModSet.getSVFValue(Pointer);
40-
return PAG.getValueNode(Nod);
36+
SVF::LLVMModuleSet &ModSet) {
37+
return ModSet.getValueNode(Pointer);
4138
}
4239
[[nodiscard]] inline SVF::NodeID getObjNodeId(const llvm::Value *Obj,
43-
SVF::LLVMModuleSet &ModSet,
44-
SVF::SVFIR &PAG) {
45-
auto *Nod = ModSet.getSVFValue(Obj);
46-
return PAG.getObjectNode(Nod);
40+
SVF::LLVMModuleSet &ModSet) {
41+
return ModSet.getObjectNode(Obj);
4742
}
4843

4944
} // namespace psr

lib/PhasarLLVM/Pointer/SVF/SVFBasedAliasAnalysis.cpp

Lines changed: 40 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,6 @@
2727
#include "SVF-LLVM/LLVMModule.h"
2828
#include "SVF-LLVM/SVFIRBuilder.h"
2929
#include "SVFIR/SVFIR.h"
30-
#include "SVFIR/SVFModule.h"
3130
#include "SVFIR/SVFType.h"
3231
#include "Util/GeneralType.h"
3332
#include "WPA/Andersen.h"
@@ -36,7 +35,10 @@
3635
#include <memory>
3736
#include <optional>
3837

39-
namespace psr {
38+
using namespace psr;
39+
40+
namespace {
41+
4042
static constexpr psr::AliasResult
4143
translateSVFAliasResult(SVF::AliasResult AR) noexcept {
4244
switch (AR) {
@@ -55,13 +57,14 @@ static psr::AliasResult doAliasImpl(SVF::PointerAnalysis *AA,
5557
const llvm::Value *V,
5658
const llvm::Value *Rep) {
5759
auto *ModSet = SVF::LLVMModuleSet::getLLVMModuleSet();
58-
auto *Nod1 = ModSet->getSVFValue(V);
59-
auto *Nod2 = ModSet->getSVFValue(Rep);
6060

61-
if (!Nod1 || !Nod2) {
61+
if (!ModSet->hasValueNode(V) || !ModSet->hasValueNode(Rep)) {
6262
return AliasResult::MayAlias;
6363
}
6464

65+
auto Nod1 = getNodeId(V, *ModSet);
66+
auto Nod2 = getNodeId(Rep, *ModSet);
67+
6568
return translateSVFAliasResult(AA->alias(Nod1, Nod2));
6669
}
6770

@@ -74,13 +77,12 @@ static psr::AliasResult aliasImpl(SVF::PointerAnalysis *AA,
7477
// NOLINTNEXTLINE(cppcoreguidelines-special-member-functions)
7578
class SVFAliasAnalysisBase : public AliasAnalysisView {
7679
public:
77-
SVFAliasAnalysisBase(SVF::SVFModule *Mod, AliasAnalysisType PATy)
78-
: AliasAnalysisView(PATy), IRBuilder(Mod), PAG(IRBuilder.build()) {}
80+
SVFAliasAnalysisBase(AliasAnalysisType PATy)
81+
: AliasAnalysisView(PATy), PAG(IRBuilder.build()) {}
7982

8083
~SVFAliasAnalysisBase() override {
8184
SVF::SVFIR::releaseSVFIR();
8285
SVF::AndersenWaveDiff::releaseAndersenWaveDiff();
83-
SVF::SymbolTableInfo::releaseSymbolInfo();
8486
SVF::LLVMModuleSet::releaseLLVMModuleSet();
8587
}
8688

@@ -95,8 +97,8 @@ class SVFAliasAnalysisBase : public AliasAnalysisView {
9597

9698
class SVFVFSAnalysis : public SVFAliasAnalysisBase {
9799
public:
98-
SVFVFSAnalysis(SVF::SVFModule *Mod)
99-
: SVFAliasAnalysisBase(Mod, AliasAnalysisType::SVFVFS),
100+
SVFVFSAnalysis()
101+
: SVFAliasAnalysisBase(AliasAnalysisType::SVFVFS),
100102
// Note: We must use the static createVFSWPA() function, otherwise SVF
101103
// will leak memory
102104
VFS(SVF::VersionedFlowSensitive::createVFSWPA(PAG)) {}
@@ -121,9 +123,8 @@ class SVFVFSAnalysis : public SVFAliasAnalysisBase {
121123

122124
class SVFDDAAnalysis : public SVFAliasAnalysisBase {
123125
public:
124-
SVFDDAAnalysis(SVF::SVFModule *Mod)
125-
: SVFAliasAnalysisBase(Mod, AliasAnalysisType::SVFVFS), Client(Mod) {
126-
Client.initialise(Mod);
126+
SVFDDAAnalysis() : SVFAliasAnalysisBase(AliasAnalysisType::SVFVFS) {
127+
Client.initialise();
127128
DDA.emplace(PAG, &Client);
128129
DDA->initialize();
129130
Client.answerQueries(&*DDA);
@@ -149,28 +150,6 @@ class SVFDDAAnalysis : public SVFAliasAnalysisBase {
149150
mutable std::optional<SVF::ContextDDA> DDA;
150151
};
151152

152-
} // namespace psr
153-
154-
auto psr::createSVFVFSAnalysis(LLVMProjectIRDB &IRDB)
155-
-> std::unique_ptr<AliasAnalysisView> {
156-
157-
return std::make_unique<SVFVFSAnalysis>(psr::initSVFModule(IRDB));
158-
}
159-
160-
auto psr::createSVFDDAAnalysis(LLVMProjectIRDB &IRDB)
161-
-> std::unique_ptr<AliasAnalysisView> {
162-
163-
return std::make_unique<SVFDDAAnalysis>(psr::initSVFModule(IRDB));
164-
}
165-
166-
namespace psr {
167-
168-
class SVFAliasInfoImpl;
169-
170-
template <>
171-
struct AliasInfoTraits<SVFAliasInfoImpl>
172-
: DefaultAATraits<const llvm::Value *, const llvm::Instruction *> {};
173-
174153
class SVFAliasInfoImpl
175154
: public SVFDDAAnalysis,
176155
public AnalysisPropertiesMixin<SVFAliasInfoImpl>,
@@ -217,9 +196,7 @@ class SVFAliasInfoImpl
217196
Ret = Set;
218197

219198
auto *ModSet = SVF::LLVMModuleSet::getLLVMModuleSet();
220-
auto *Nod = ModSet->getSVFValue(Ptr);
221-
222-
auto PointerNod = PAG->getValueNode(Nod);
199+
auto PointerNod = getNodeId(Ptr, *ModSet);
223200

224201
createAliasSet(PointerNod, *Set, *ModSet);
225202

@@ -235,7 +212,7 @@ class SVFAliasInfoImpl
235212
}
236213

237214
auto &ModSet = *SVF::LLVMModuleSet::getLLVMModuleSet();
238-
auto Nod = getNodeId(Ptr, ModSet, *PAG);
215+
auto Nod = getNodeId(Ptr, ModSet);
239216
const auto &Pts = getPTA().getPts(Nod);
240217

241218
const auto *VFun = AliasInfoBaseUtils::retrieveFunction(Ptr);
@@ -267,14 +244,14 @@ class SVFAliasInfoImpl
267244
}
268245

269246
auto &ModSet = *SVF::LLVMModuleSet::getLLVMModuleSet();
270-
auto Nod = getNodeId(Ptr, ModSet, *PAG);
247+
auto Nod = getNodeId(Ptr, ModSet);
271248

272249
if (IntraProcOnly && llvm::isa<llvm::Argument>(AllocSite)) {
273-
auto AllocSiteNod = getNodeId(AllocSite, ModSet, *PAG);
250+
auto AllocSiteNod = getNodeId(AllocSite, ModSet);
274251
return getPTA().alias(Nod, AllocSiteNod) != SVF::NoAlias;
275252
}
276253

277-
auto AllocSiteNod = getObjNodeId(AllocSite, ModSet, *PAG);
254+
auto AllocSiteNod = getObjNodeId(AllocSite, ModSet);
278255
const auto &Pts = getPTA().getPts(Nod);
279256

280257
return Pts.test(AllocSiteNod);
@@ -285,11 +262,7 @@ class SVFAliasInfoImpl
285262

286263
auto &ModSet = *SVF::LLVMModuleSet::getLLVMModuleSet();
287264
for (const auto &[Nod, Var] : *PAG) {
288-
if (!Var->hasValue()) {
289-
continue;
290-
}
291-
292-
const auto *PointerVal = ModSet.getLLVMValue(Var->getValue());
265+
const auto *PointerVal = svfVarToLLVMOrNull(Var, ModSet);
293266
if (!PointerVal) {
294267
continue;
295268
}
@@ -352,8 +325,27 @@ class SVFAliasInfoImpl
352325
AliasSetOwner<AliasSetTy>::memory_resource_type MRes;
353326
AliasSetOwner<AliasSetTy> Owner{&MRes};
354327
};
328+
} // namespace
329+
330+
namespace psr {
331+
template <>
332+
struct AliasInfoTraits<SVFAliasInfoImpl>
333+
: DefaultAATraits<const llvm::Value *, const llvm::Instruction *> {};
355334
} // namespace psr
356335

336+
auto psr::createSVFVFSAnalysis(LLVMProjectIRDB &IRDB)
337+
-> std::unique_ptr<AliasAnalysisView> {
338+
psr::initSVFModule(IRDB);
339+
return std::make_unique<SVFVFSAnalysis>();
340+
}
341+
342+
auto psr::createSVFDDAAnalysis(LLVMProjectIRDB &IRDB)
343+
-> std::unique_ptr<AliasAnalysisView> {
344+
psr::initSVFModule(IRDB);
345+
return std::make_unique<SVFDDAAnalysis>();
346+
}
347+
357348
auto psr::createLLVMSVFDDAAliasInfo(LLVMProjectIRDB &IRDB) -> LLVMAliasInfo {
358-
return std::make_unique<SVFAliasInfoImpl>(psr::initSVFModule(IRDB));
349+
psr::initSVFModule(IRDB);
350+
return std::make_unique<SVFAliasInfoImpl>();
359351
}

0 commit comments

Comments
 (0)