Skip to content

Commit a750238

Browse files
pdschubertpdschubert
committed
Merge branch 'development' into master_github
2 parents 94769fd + 1ca069a commit a750238

7 files changed

Lines changed: 54 additions & 30 deletions

File tree

‎include/phasar/PhasarLLVM/IfdsIde/Problems/TypeStateDescriptions/CSTDFILEIOTypeStateDescription.h‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ class CSTDFILEIOTypeStateDescription : public TypeStateDescription {
3939
OPENED = 1,
4040
CLOSED = 2,
4141
ERROR = 3,
42-
BOT = 13
42+
BOT = 4
4343
};
4444

4545
/**
@@ -51,7 +51,7 @@ class CSTDFILEIOTypeStateDescription : public TypeStateDescription {
5151

5252
static const std::map<std::string, std::set<int>> StdFileIOFuncs;
5353
// delta matrix to implement the state machine's delta function
54-
static const CSTDFILEIOState delta[3][4];
54+
static const CSTDFILEIOState delta[3][5];
5555
CSTDFILEIOToken funcNameToToken(const std::string &F) const;
5656

5757
public:

‎include/phasar/PhasarLLVM/IfdsIde/Solver/IDESolver.h‎

Lines changed: 20 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -695,13 +695,31 @@ class IDESolver {
695695
}
696696

697697
std::shared_ptr<EdgeFunction<V>> jumpFunction(PathEdge<N, D> edge) {
698+
auto &lg = lg::get();
699+
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, DEBUG) << " ");
700+
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, DEBUG) << "JumpFunctions Forward-Lookup:");
701+
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, DEBUG)
702+
<< " Source D: "
703+
<< ideTabulationProblem.DtoString(edge.factAtSource()));
704+
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, DEBUG)
705+
<< " Target N: "
706+
<< ideTabulationProblem.NtoString(edge.getTarget()));
707+
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, DEBUG)
708+
<< " Target D: "
709+
<< ideTabulationProblem.DtoString(edge.factAtTarget()));
698710
if (!jumpFn->forwardLookup(edge.factAtSource(), edge.getTarget())
699711
.count(edge.factAtTarget())) {
712+
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, DEBUG)
713+
<< " => EdgeFn: " << allTop->str());
714+
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, DEBUG) << " ");
700715
// JumpFn initialized to all-top, see line [2] in SRH96 paper
701716
return allTop;
702717
}
703-
return jumpFn->forwardLookup(edge.factAtSource(),
704-
edge.getTarget())[edge.factAtTarget()];
718+
auto res = jumpFn->forwardLookup(edge.factAtSource(),
719+
edge.getTarget())[edge.factAtTarget()];
720+
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, DEBUG) << " => EdgeFn: " << res->str());
721+
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, DEBUG) << " ");
722+
return res;
705723
}
706724

707725
void addEndSummary(N sP, D d1, N eP, D d2,

‎include/phasar/PhasarLLVM/IfdsIde/Solver/JumpFunctions.h‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -83,18 +83,19 @@ class JumpFunctions {
8383
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, DEBUG)
8484
<< "Edge Function : " << function->str());
8585
// we do not store the default function (all-top)
86-
if (function->equal_to(allTop))
86+
if (function->equal_to(allTop)) {
8787
return;
88+
}
89+
// it is important that existing values in JumpFunctions are overwritten
90+
// (use operator[] instead of insert)
8891
std::unordered_map<D, std::shared_ptr<EdgeFunction<L>>> &sourceValToFunc =
8992
nonEmptyReverseLookup.get(target, targetVal);
90-
sourceValToFunc.insert({sourceVal, function});
91-
// printNonEmptyReverseLookup();
93+
sourceValToFunc[sourceVal] = function;
9294
std::unordered_map<D, std::shared_ptr<EdgeFunction<L>>> &targetValToFunc =
9395
nonEmptyForwardLookup.get(sourceVal, target);
94-
targetValToFunc.insert({targetVal, function});
95-
// printNonEmptyForwardLookup();
96+
targetValToFunc[targetVal] = function;
97+
// V Table::insert(R r, C c, V v) always overrides (see comments above)
9698
nonEmptyLookupByTargetNode[target].insert(sourceVal, targetVal, function);
97-
// printNonEmptyLookupByTargetNode();
9899
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, DEBUG) << "End adding new jump function");
99100
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, DEBUG) << ' ');
100101
}

‎lib/PhasarLLVM/IfdsIde/Problems/IDETypeStateAnalysis.cpp‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -590,6 +590,10 @@ IDETypeStateAnalysis::TSEdgeFunction::joinWith(
590590
otherFunction->equal_to(this->shared_from_this())) {
591591
return this->shared_from_this();
592592
}
593+
// if (auto *EI = dynamic_cast<EdgeIdentity<IDETypeStateAnalysis::v_t> *>(
594+
// otherFunction.get())) {
595+
// return this->shared_from_this();
596+
// }
593597
if (auto *AT = dynamic_cast<AllTop<IDETypeStateAnalysis::v_t> *>(
594598
otherFunction.get())) {
595599
return this->shared_from_this();

‎lib/PhasarLLVM/IfdsIde/Problems/TypeStateDescriptions/CSTDFILEIOTypeStateDescription.cpp‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -34,18 +34,18 @@ const std::map<std::string, std::set<int>>
3434

3535
// delta[Token][State] = next State
3636
// Token: FOPEN = 0, FCLOSE = 1, STAR = 2
37-
// States: UNINIT = 0, OPENED = 1, CLOSED = 2, ERROR = 3
37+
// States: UNINIT = 0, OPENED = 1, CLOSED = 2, ERROR = 3, BOT = 4
3838
const CSTDFILEIOTypeStateDescription::CSTDFILEIOState
39-
CSTDFILEIOTypeStateDescription::delta[3][4] = {
39+
CSTDFILEIOTypeStateDescription::delta[3][5] = {
4040
/* FOPEN */
4141
{CSTDFILEIOState::OPENED, CSTDFILEIOState::OPENED,
42-
CSTDFILEIOState::ERROR, CSTDFILEIOState::ERROR},
42+
CSTDFILEIOState::ERROR, CSTDFILEIOState::ERROR, CSTDFILEIOState::BOT},
4343
/* FCLOSE */
4444
{CSTDFILEIOState::ERROR, CSTDFILEIOState::CLOSED,
45-
CSTDFILEIOState::ERROR, CSTDFILEIOState::ERROR},
45+
CSTDFILEIOState::ERROR, CSTDFILEIOState::ERROR, CSTDFILEIOState::BOT},
4646
/* STAR */
4747
{CSTDFILEIOState::ERROR, CSTDFILEIOState::OPENED,
48-
CSTDFILEIOState::ERROR, CSTDFILEIOState::ERROR},
48+
CSTDFILEIOState::ERROR, CSTDFILEIOState::ERROR, CSTDFILEIOState::BOT},
4949
};
5050

5151
bool CSTDFILEIOTypeStateDescription::isFactoryFunction(

‎tools/phasar/phasar.cpp‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -265,7 +265,6 @@ int main(int argc, const char **argv) {
265265
initializeLogger(VariablesMap["log"].as<bool>());
266266
LOG_IF_ENABLE(BOOST_LOG_SEV(lg, INFO)
267267
<< "Program options have been successfully parsed.");
268-
bl::core::get()->flush();
269268
}
270269
ifstream ifs(ConfigFile.c_str());
271270
if (!ifs) {

‎unittests/PhasarLLVM/IfdsIde/Problems/IDETypeStateAnalysisTest.cpp‎

Lines changed: 16 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ class IDETypeStateAnalysisTest : public ::testing::Test {
2828
OPENED = 1,
2929
CLOSED = 2,
3030
ERROR = 3,
31-
BOT = 13
31+
BOT = 4
3232
};
3333

3434
IDETypeStateAnalysisTest() = default;
@@ -422,6 +422,7 @@ TEST_F(IDETypeStateAnalysisTest, HandleTypeState_16) {
422422
compareResults(gt, llvmtssolver);
423423
}
424424

425+
// TODO: Check this case again!
425426
TEST_F(IDETypeStateAnalysisTest, HandleTypeState_17) {
426427
Initialize({pathToLLFiles + "typestate_17_c.ll"});
427428
LLVMIDESolver<const llvm::Value *, int, LLVMBasedICFG &> llvmtssolver(
@@ -431,22 +432,22 @@ TEST_F(IDETypeStateAnalysisTest, HandleTypeState_17) {
431432
const std::map<std::size_t, std::map<std::string, int>> gt = {
432433
// Before fgetc()
433434
{17,
434-
{{"2", IOSTATE::CLOSED},
435-
{"9", IOSTATE::CLOSED},
436-
{"13", IOSTATE::CLOSED},
437-
{"16", IOSTATE::CLOSED}}},
435+
{{"2", IOSTATE::BOT},
436+
{"9", IOSTATE::BOT},
437+
{"13", IOSTATE::BOT},
438+
{"16", IOSTATE::BOT}}},
438439
// After fgetc()
439440
{18,
440-
{{"2", IOSTATE::ERROR},
441-
{"9", IOSTATE::ERROR},
442-
{"13", IOSTATE::ERROR},
443-
{"16", IOSTATE::ERROR}}},
441+
{{"2", IOSTATE::BOT},
442+
{"9", IOSTATE::BOT},
443+
{"13", IOSTATE::BOT},
444+
{"16", IOSTATE::BOT}}},
444445
// At exit in main()
445446
{22,
446-
{{"2", IOSTATE::ERROR},
447-
{"9", IOSTATE::ERROR},
448-
{"13", IOSTATE::ERROR},
449-
{"16", IOSTATE::ERROR}}}};
447+
{{"2", IOSTATE::BOT},
448+
{"9", IOSTATE::BOT},
449+
{"13", IOSTATE::BOT},
450+
{"16", IOSTATE::BOT}}}};
450451
compareResults(gt, llvmtssolver);
451452
}
452453

@@ -464,6 +465,7 @@ TEST_F(IDETypeStateAnalysisTest, HandleTypeState_18) {
464465
compareResults(gt, llvmtssolver);
465466
}
466467

468+
// TODO: Check this case again!
467469
TEST_F(IDETypeStateAnalysisTest, HandleTypeState_19) {
468470
Initialize({pathToLLFiles + "typestate_19_c.ll"});
469471
LLVMIDESolver<const llvm::Value *, int, LLVMBasedICFG &> llvmtssolver(
@@ -472,7 +474,7 @@ TEST_F(IDETypeStateAnalysisTest, HandleTypeState_19) {
472474
llvmtssolver.solve();
473475
const std::map<std::size_t, std::map<std::string, int>> gt = {
474476
{11, {{"8", IOSTATE::UNINIT}}},
475-
{14, {{"8", IOSTATE::ERROR}}},
477+
{14, {{"8", IOSTATE::BOT}}},
476478
// At exit in main()
477479
{25, {{"2", IOSTATE::CLOSED}, {"8", IOSTATE::CLOSED}}}};
478480
compareResults(gt, llvmtssolver);

0 commit comments

Comments
 (0)