Skip to content

Commit c3bb5dc

Browse files
sallaigysallaigy
committedDec 12, 2020
Fix translation of incorrect PHI conditions on loop exit blocks (fixes #66)
·
v1.4.3v1.3.0
1 parent 1ef864d commit c3bb5dc

File tree

9 files changed

+397
-36
lines changed

9 files changed

+397
-36
lines changed
 

‎include/gazer/ADT/Graph.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -213,7 +213,7 @@ class Graph
213213
EdgeTy* createEdge(NodeTy* source, NodeTy* target)
214214
{
215215
auto& edge = mEdges.emplace_back(std::make_unique<EdgeTy>(source, target));
216-
216+
217217
static_cast<GraphNode<NodeTy, EdgeTy>*>(source)->mOutgoing.emplace_back(&*edge);
218218
static_cast<GraphNode<NodeTy, EdgeTy>*>(target)->mIncoming.emplace_back(&*edge);
219219

@@ -226,7 +226,7 @@ class Graph
226226
auto& edge = mEdges.emplace_back(std::make_unique<EdgeTy>(
227227
source, target, std::forward<Args...>(args...)
228228
));
229-
229+
230230
source->mOutgoing.emplace_back(&*edge);
231231
target->mIncoming.emplace_back(&*edge);
232232

‎src/Automaton/CfaPrinter.cpp

+2-8
Original file line numberDiff line numberDiff line change
@@ -76,13 +76,7 @@ struct DOTGraphTraits<Cfa> : public DefaultDOTGraphTraits
7676

7777
const Location* target = *edgeIt;
7878

79-
const Transition* edge = nullptr;
80-
for (const Transition* ei : loc->outgoing()) {
81-
if (ei->getTarget() == target) {
82-
edge = ei;
83-
break;
84-
}
85-
}
79+
const Transition* edge = *(edgeIt.getCurrent());
8680

8781
assert(edge != nullptr);
8882

@@ -240,7 +234,7 @@ void Cfa::print(llvm::raw_ostream& os) const
240234
os << ", ";
241235
}
242236
join_print_as(os, call->output_begin(), call->output_end(), ", ", printCallOutput);
243-
os << ");\n";
237+
os << ");\n";
244238
} else {
245239
llvm_unreachable("Unknown transition kind.");
246240
}

‎src/LLVM/Automaton/FunctionToCfa.h

+6-3
Original file line numberDiff line numberDiff line change
@@ -64,9 +64,12 @@ class CfaGenInfo
6464
Cfa* Automaton;
6565
std::variant<llvm::Function*, llvm::Loop*> Source;
6666

67+
using ExitEdge = std::pair<const llvm::BasicBlock*, const llvm::BasicBlock*>;
68+
69+
6770
// For automata with multiple exit paths, this variable tells us which was taken.
6871
Variable* ExitVariable = nullptr;
69-
llvm::SmallDenseMap<const llvm::BasicBlock*, ExprRef<LiteralExpr>, 4> ExitBlocks;
72+
llvm::SmallDenseMap<ExitEdge, ExprRef<LiteralExpr>> ExitEdges;
7073

7174
// For functions with return values
7275
Variable* ReturnVariable = nullptr;
@@ -381,12 +384,12 @@ class BlocksToCfa : public InstToExpr
381384
Location* exit
382385
);
383386

384-
void createExitTransition(const llvm::BasicBlock* target, Location* pred, const ExprPtr& succCondition);
387+
void createExitTransition(const llvm::BasicBlock* source, const llvm::BasicBlock* target, Location* pred, const ExprPtr& succCondition);
385388
void createCallToLoop(
386389
llvm::Loop* loop, const llvm::BasicBlock* source, const llvm::BasicBlock* target,
387390
const ExprPtr& condition, Location* exit);
388391

389-
ExprPtr getExitCondition(const llvm::BasicBlock* target, Variable* exitSelector, CfaGenInfo& nestedInfo);
392+
ExprPtr getExitCondition(const llvm::BasicBlock* source, const llvm::BasicBlock* target, Variable* exitSelector, CfaGenInfo& nestedInfo);
390393
size_t getNumUsesInBlocks(const llvm::Instruction* inst) const;
391394

392395
ExtensionPointImpl createExtensionPoint(

‎src/LLVM/Automaton/ModuleToAutomata.cpp

+16-16
Original file line numberDiff line numberDiff line change
@@ -333,17 +333,17 @@ void ModuleToCfa::createAutomata()
333333
loopGenInfo.addBlockToLocationsMapping(bb, entry, exit);
334334
}
335335

336-
// If the loop has multiple exits, add a selector output to disambiguate between these.
337-
llvm::SmallVector<llvm::BasicBlock*, 4> exitBlocks;
338-
loop->getUniqueExitBlocks(exitBlocks);
336+
// Store which block was the exiting block inside the loop
337+
llvm::SmallVector<llvm::Loop::Edge, 4> exitEdges;
338+
loop->getExitEdges(exitEdges);
339339

340-
if (exitBlocks.size() != 1) {
340+
if (exitEdges.size() != 1) {
341341
Type& selectorTy = getExitSelectorType(mSettings.ints, mContext);
342342
loopGenInfo.ExitVariable = nested->createLocal(LoopOutputSelectorName, selectorTy);
343343
nested->addOutput(loopGenInfo.ExitVariable);
344-
for (size_t i = 0; i < exitBlocks.size(); ++i) {
345-
LLVM_DEBUG(llvm::dbgs() << " Registering exit block " << exitBlocks[i]->getName() << "\n");
346-
loopGenInfo.ExitBlocks[exitBlocks[i]] = selectorTy.isBvType()
344+
for (size_t i = 0; i < exitEdges.size(); ++i) {
345+
LLVM_DEBUG(llvm::dbgs() << " Registering exit edge " << exitEdges[i].first->getName() << " --> " << exitEdges[i].second->getName() << "\n");
346+
loopGenInfo.ExitEdges[exitEdges[i]] = selectorTy.isBvType()
347347
? expr_cast<LiteralExpr>(mExprBuilder->BvLit(i, 8))
348348
: mExprBuilder->IntLit(i);
349349
}
@@ -736,15 +736,15 @@ bool BlocksToCfa::tryToEliminate(ValueOrMemoryObject val, Variable* variable, co
736736
return true;
737737
}
738738

739-
void BlocksToCfa::createExitTransition(const BasicBlock* target, Location* pred, const ExprPtr& succCondition)
739+
void BlocksToCfa::createExitTransition(const BasicBlock* source, const BasicBlock* target, Location* pred, const ExprPtr& succCondition)
740740
{
741741
LLVM_DEBUG(llvm::dbgs() << " Building exit transition for block " << target->getName() << "\n");
742742

743743
// If the target is outside of our region, create a simple edge to the exit.
744744
std::vector<VariableAssignment> exitAssigns;
745745
if (mGenInfo.ExitVariable != nullptr) {
746746
// If there are multiple exits, create an assignment to indicate which one to take.
747-
ExprPtr exitVal = mGenInfo.ExitBlocks[target];
747+
ExprPtr exitVal = mGenInfo.ExitEdges[{source, target}];
748748
assert(exitVal != nullptr && "An exit block must be present in the exit blocks map!");
749749

750750
exitAssigns.emplace_back(mGenInfo.ExitVariable, exitVal);
@@ -759,13 +759,13 @@ void BlocksToCfa::createExitTransition(const BasicBlock* target, Location* pred,
759759
mCfa->createAssignTransition(pred, mCfa->getExit(), succCondition, exitAssigns);
760760
}
761761

762-
ExprPtr BlocksToCfa::getExitCondition(const llvm::BasicBlock* target, Variable* exitSelector, CfaGenInfo& nestedInfo)
762+
ExprPtr BlocksToCfa::getExitCondition(const llvm::BasicBlock* source, const llvm::BasicBlock* target, Variable* exitSelector, CfaGenInfo& nestedInfo)
763763
{
764764
if (nestedInfo.ExitVariable == nullptr) {
765765
return mExprBuilder.True();
766766
}
767767

768-
ExprPtr exitVal = nestedInfo.ExitBlocks[target];
768+
ExprPtr exitVal = nestedInfo.ExitEdges[{source, target}];
769769
assert(exitVal != nullptr && "An exit block must be present in the exit blocks map!");
770770

771771
return mExprBuilder.Eq(exitSelector->getRefExpr(), exitVal);
@@ -776,7 +776,7 @@ void BlocksToCfa::handleSuccessor(const BasicBlock* succ, const ExprPtr& succCon
776776
{
777777
LLVM_DEBUG(llvm::dbgs() << "Translating CFG edge " << parent->getName() << " " << succ->getName() << "\n");
778778
if (succ == mEntryBlock) {
779-
// If the target is the loop header (entry block), create a call to this same automaton.
779+
// If the target is the loop header (entry block), create a call to this same automaton.
780780
auto loc = mCfa->createLocation();
781781
mCfa->createAssignTransition(exit, loc, succCondition);
782782

@@ -821,7 +821,7 @@ void BlocksToCfa::handleSuccessor(const BasicBlock* succ, const ExprPtr& succCon
821821
} else if (auto loop = getNestedLoopOf(mGenCtx, mGenInfo, succ)) {
822822
this->createCallToLoop(loop, parent, succ, succCondition, exit);
823823
} else {
824-
createExitTransition(succ, exit, succCondition);
824+
createExitTransition(parent, succ, exit, succCondition);
825825
}
826826
}
827827

@@ -848,7 +848,7 @@ void BlocksToCfa::createCallToLoop(
848848
}
849849
}
850850

851-
for (auto& [valueOrMemObj, variable] : nestedLoopInfo.Inputs) {
851+
for (auto& [valueOrMemObj, variable] : nestedLoopInfo.Inputs) {
852852
LLVM_DEBUG(llvm::dbgs() << " Translating loop input argument " << *variable << " " << valueOrMemObj << "\n");
853853
ExprPtr argExpr = operand(valueOrMemObj);
854854
loopArgs.emplace_back(variable, argExpr);
@@ -889,11 +889,11 @@ void BlocksToCfa::createCallToLoop(
889889
// simply create an assign transition to represent the exit jump.
890890
mCfa->createAssignTransition(
891891
loc, result->second.first,
892-
getExitCondition(exitBlock, exitSelector, nestedLoopInfo),
892+
getExitCondition(inBlock, exitBlock, exitSelector, nestedLoopInfo),
893893
phiAssignments
894894
);
895895
} else {
896-
createExitTransition(exitBlock, exit, condition);
896+
createExitTransition(inBlock, exitBlock, exit, condition);
897897
}
898898
}
899899
}

‎test/cfa/Expected/LoopMultipleExits.cfa

+8-6
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ procedure main() -> (main/RET_VAL : Bv32)
55
var main/sum : Bv32
66
var main/__output_selector0 : Bv8
77

8-
loc $0 entry
9-
loc $1 final
8+
loc $0 entry
9+
loc $1 final
1010
loc $2
1111
loc $3
1212
loc $4
@@ -41,7 +41,7 @@ procedure main() -> (main/RET_VAL : Bv32)
4141
};
4242

4343
transition $8 -> $4
44-
assume main/__output_selector0 = 0bv8
44+
assume main/__output_selector0 = 2bv8
4545
{
4646
};
4747

@@ -68,6 +68,7 @@ procedure main() -> (main/RET_VAL : Bv32)
6868
};
6969

7070
}
71+
7172
procedure main/loop.header(main/loop.header/i : Bv32, main/loop.header/sum : Bv32, main/loop.header/limit : Bv32) -> (main/loop.header/sum_out : Bv32, main/loop.header/__output_selector : Bv8)
7273
{
7374
var main/loop.header/sum_out : Bv32
@@ -80,8 +81,8 @@ procedure main/loop.header(main/loop.header/i : Bv32, main/loop.header/sum : Bv3
8081
var main/loop.header/c1 : Bool
8182
var main/loop.header/__output_selector : Bv8
8283

83-
loc $0 entry
84-
loc $1 final
84+
loc $0 entry
85+
loc $1 final
8586
loc $2
8687
loc $3
8788
loc $4
@@ -144,7 +145,7 @@ procedure main/loop.header(main/loop.header/i : Bv32, main/loop.header/sum : Bv3
144145
transition $7 -> $1
145146
assume main/loop.header/c1
146147
{
147-
main/loop.header/__output_selector := 0bv8;
148+
main/loop.header/__output_selector := 2bv8;
148149
main/loop.header/sum_out := main/loop.header/sum;
149150
};
150151

@@ -158,3 +159,4 @@ procedure main/loop.header(main/loop.header/i : Bv32, main/loop.header/sum : Bv3
158159
call main/loop.header(main/loop.header/i := main/loop.header/i1, main/loop.header/sum := main/loop.header/s, main/loop.header/limit := main/loop.header/limit, main/loop.header/sum_out <= main/loop.header/sum_out, main/loop.header/__output_selector <= main/loop.header/__output_selector);
159160

160161
}
162+

‎test/cfa/Expected/MultipleExitingBlockBranchingToSame.cfa

+239
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,239 @@
1+
procedure main() -> (main/RET_VAL : Bv32)
2+
{
3+
var main/RET_VAL : Bv32
4+
var main/Memory_0_mem : [Bv64 -> Bv8]
5+
var main/Memory_3_mem : [Bv64 -> Bv8]
6+
var main/Memory_4_mem : [Bv64 -> Bv8]
7+
var main/Memory_5_mem : [Bv64 -> Bv8]
8+
var main/Memory_6_mem : [Bv64 -> Bv8]
9+
var main/tmp6 : Bv32
10+
var main/tmp8 : Bv32
11+
var main/__output_selector0 : Int
12+
13+
loc $0 entry
14+
loc $1 final
15+
loc $2
16+
loc $3
17+
loc $4
18+
loc $5
19+
loc $6
20+
loc $7
21+
loc $8
22+
loc $9 error
23+
loc $10
24+
loc $11
25+
loc $12
26+
27+
transition $0 -> $2
28+
assume true
29+
{
30+
};
31+
32+
transition $2 -> $3
33+
assume true
34+
{
35+
main/Memory_0_mem := undef;
36+
};
37+
38+
transition $3 -> $12
39+
assume true
40+
call main/bb3(main/bb3/Memory_5 := main/Memory_0_mem, main/bb3/b.0 := 16fp32, main/bb3/StackPtr_1 := 1073741824bv64, main/bb3/FramePtr_2 := 1073741824bv64, main/tmp6 <= main/bb3/tmp6_out, main/__output_selector0 <= main/bb3/__output_selector);
41+
42+
transition $12 -> $4
43+
assume main/__output_selector0 = 0
44+
{
45+
main/tmp8 := 12bv32;
46+
};
47+
48+
transition $12 -> $4
49+
assume main/__output_selector0 = 1
50+
{
51+
main/tmp8 := main/tmp6;
52+
};
53+
54+
transition $4 -> $5
55+
assume true
56+
{
57+
};
58+
59+
transition $5 -> $8
60+
assume main/tmp8 = 0bv32
61+
{
62+
};
63+
64+
transition $5 -> $6
65+
assume not (main/tmp8 = 0bv32)
66+
{
67+
};
68+
69+
transition $6 -> $7
70+
assume true
71+
{
72+
};
73+
74+
transition $7 -> $10
75+
assume true
76+
{
77+
};
78+
79+
transition $8 -> $9
80+
assume true
81+
{
82+
};
83+
84+
transition $9 -> $10
85+
assume true
86+
{
87+
};
88+
89+
transition $10 -> $11
90+
assume true
91+
{
92+
};
93+
94+
transition $11 -> $1
95+
assume false
96+
{
97+
};
98+
99+
}
100+
101+
procedure main/bb3(main/bb3/Memory_5 : [Bv64 -> Bv8], main/bb3/StackPtr_1 : Bv64, main/bb3/FramePtr_2 : Bv64, main/bb3/b.0 : Float32) -> (main/bb3/tmp6_out : Bv32, main/bb3/__output_selector : Int)
102+
{
103+
var main/bb3/Memory_3 : [Bv64 -> Bv8]
104+
var main/bb3/Memory_4 : [Bv64 -> Bv8]
105+
var main/bb3/tmp4 : Float32
106+
var main/bb3/tmp5 : Bool
107+
var main/bb3/tmp6 : Bv32
108+
var main/bb3/tmp6_out : Bv32
109+
var main/bb3/tmp7 : Bool
110+
var main/bb3/__output_selector : Int
111+
112+
loc $0 entry
113+
loc $1 final
114+
loc $2
115+
loc $3
116+
loc $4
117+
loc $5
118+
loc $6
119+
loc $7
120+
loc $8
121+
loc $9
122+
loc $10
123+
loc $11
124+
loc $12
125+
126+
transition $0 -> $2
127+
assume true
128+
{
129+
};
130+
131+
transition $2 -> $3
132+
assume true
133+
{
134+
main/bb3/tmp4 := fp.mul(fp.mul(main/bb3/b.0,3fp32),0.25fp32);
135+
main/bb3/tmp5 := undef;
136+
};
137+
138+
transition $3 -> $1
139+
assume main/bb3/tmp5
140+
{
141+
main/bb3/__output_selector := 0;
142+
main/bb3/tmp6_out := main/bb3/tmp6;
143+
};
144+
145+
transition $3 -> $4
146+
assume not main/bb3/tmp5
147+
{
148+
};
149+
150+
transition $4 -> $8
151+
assume true
152+
{
153+
};
154+
155+
transition $8 -> $9
156+
assume true
157+
call a(a/arg := 12bv32, a/Memory_0_mem := main/bb3/Memory_5, a/StackPtr_1_mem := main/bb3/StackPtr_1, a/FramePtr_2_mem := main/bb3/FramePtr_2, main/bb3/Memory_3 <= a/Memory_0_mem);
158+
159+
transition $9 -> $5
160+
assume true
161+
{
162+
main/bb3/tmp6 := fp_to_si.float32.bv32(main/bb3/tmp4);
163+
main/bb3/tmp7 := undef;
164+
};
165+
166+
transition $5 -> $1
167+
assume main/bb3/tmp7
168+
{
169+
main/bb3/__output_selector := 1;
170+
main/bb3/tmp6_out := main/bb3/tmp6;
171+
};
172+
173+
transition $5 -> $6
174+
assume not main/bb3/tmp7
175+
{
176+
};
177+
178+
transition $6 -> $10
179+
assume true
180+
{
181+
};
182+
183+
transition $10 -> $11
184+
assume true
185+
call a(a/arg := main/bb3/tmp6, a/Memory_0_mem := main/bb3/Memory_3, a/StackPtr_1_mem := main/bb3/StackPtr_1, a/FramePtr_2_mem := main/bb3/FramePtr_2, main/bb3/Memory_4 <= a/Memory_0_mem);
186+
187+
transition $11 -> $7
188+
assume true
189+
{
190+
};
191+
192+
transition $7 -> $12
193+
assume true
194+
{
195+
};
196+
197+
transition $12 -> $1
198+
assume true
199+
call main/bb3(main/bb3/Memory_5 := main/bb3/Memory_4, main/bb3/b.0 := main/bb3/tmp4, main/bb3/StackPtr_1 := main/bb3/StackPtr_1, main/bb3/FramePtr_2 := main/bb3/FramePtr_2, main/bb3/tmp6_out <= main/bb3/tmp6_out, main/bb3/__output_selector <= main/bb3/__output_selector);
200+
201+
}
202+
203+
procedure a(a/arg : Bv32, a/Memory_0_mem : [Bv64 -> Bv8], a/StackPtr_1_mem : Bv64, a/FramePtr_2_mem : Bv64) -> (a/Memory_0_mem : [Bv64 -> Bv8])
204+
{
205+
206+
loc $0 entry
207+
loc $1 final
208+
loc $2
209+
loc $3
210+
loc $4
211+
loc $5
212+
213+
transition $0 -> $2
214+
assume true
215+
{
216+
};
217+
218+
transition $2 -> $4
219+
assume true
220+
{
221+
};
222+
223+
transition $4 -> $5
224+
assume not (a/arg = 0bv32)
225+
{
226+
};
227+
228+
transition $5 -> $3
229+
assume true
230+
{
231+
};
232+
233+
transition $3 -> $1
234+
assume true
235+
{
236+
};
237+
238+
}
239+

‎test/cfa/MultipleExitingBlockBranchingToSame.ll

+53
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
; RUN: %cfa -memory=flat "%s" | /usr/bin/diff -B -Z "%p/Expected/MultipleExitingBlockBranchingToSame.cfa" -
2+
3+
define internal void @a(i32 %arg) {
4+
bb:
5+
%tmp = icmp ne i32 %arg, 0
6+
call void @llvm.assume(i1 %tmp)
7+
ret void
8+
}
9+
10+
define i32 @main() {
11+
bb:
12+
br label %bb3
13+
14+
bb3: ; preds = %.split.split, %bb
15+
%b.0 = phi float [ 1.600000e+01, %bb ], [ %tmp4, %.split.split ]
16+
%tmp = fmul float %b.0, 3.000000e+00
17+
%tmp4 = fmul float %tmp, 2.500000e-01
18+
%tmp5 = call i1 @gazer.dummy_nondet.i1()
19+
br i1 %tmp5, label %a_fail, label %.split
20+
21+
.split: ; preds = %bb3
22+
call void @a(i32 12)
23+
%tmp6 = fptosi float %tmp4 to i32
24+
%tmp7 = call i1 @gazer.dummy_nondet.i1()
25+
br i1 %tmp7, label %a_fail, label %.split.split
26+
27+
.split.split: ; preds = %.split
28+
call void @a(i32 %tmp6)
29+
br label %bb3
30+
31+
a_fail: ; preds = %.split, %bb3
32+
%tmp8 = phi i32 [ 12, %bb3 ], [ %tmp6, %.split ]
33+
%tmp9 = icmp eq i32 %tmp8, 0
34+
br i1 %tmp9, label %error1, label %bb10
35+
36+
bb10: ; preds = %a_fail
37+
br label %UnifiedUnreachableBlock
38+
39+
error1: ; preds = %a_fail
40+
call void @gazer.error_code(i16 1)
41+
br label %UnifiedUnreachableBlock
42+
43+
UnifiedUnreachableBlock: ; preds = %error1, %bb10
44+
unreachable
45+
}
46+
47+
declare void @gazer.error_code(i16) local_unnamed_addr
48+
49+
declare void @gazer.dummy.void() local_unnamed_addr
50+
51+
declare i1 @gazer.dummy_nondet.i1() local_unnamed_addr
52+
53+
declare void @llvm.assume(i1)

‎test/verif/regression/floats/fp_if_not_inlined.c

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
// This test failed if gazer-bmc was invoked without the "-inline=all" flag.
2+
// The underlying issue was that the translation process did not handle PHI nodes correctly when jumping out of loops.
3+
4+
// RUN: %bmc -bound 10 -inline=all "%s" | FileCheck "%s"
5+
// RUN: %bmc -bound 10 "%s" | FileCheck "%s"
6+
7+
// CHECK: Verification {{(SUCCESSFUL|BOUND REACHED)}}
8+
9+
float b = 16.f;
10+
void __VERIFIER_error();
11+
void a(c) {
12+
if (!c)
13+
__VERIFIER_error();
14+
}
15+
int main() {
16+
for (;;) {
17+
b = 3.f * b / 4.f;
18+
a(12.f);
19+
a(b);
20+
}
21+
}

‎unittest/Automaton/PathConditionTest.cpp

+50-1
Original file line numberDiff line numberDiff line change
@@ -101,4 +101,53 @@ TEST(PathConditionTest, PredecessorTest)
101101
ASSERT_EQ(expected, actual);
102102
}
103103

104-
}
104+
105+
TEST(PathConditionTest, TestParallelEdges)
106+
{
107+
GazerContext ctx;
108+
AutomataSystem system(ctx);
109+
110+
Cfa* cfa = system.createCfa("main");
111+
auto x = cfa->createLocal("x", IntType::Get(ctx));
112+
113+
// l0, l1 are reserved for entry and exit
114+
auto l2 = cfa->createLocation();
115+
auto le = cfa->createErrorLocation();
116+
117+
// l0 --> l2 { x := 1 }
118+
// l0 --> l2 { x := 1 }
119+
cfa->createAssignTransition(cfa->getEntry(), l2, {
120+
{ x, IntLiteralExpr::Get(ctx, 1) }
121+
});
122+
cfa->createAssignTransition(cfa->getEntry(), l2, {
123+
{ x, IntLiteralExpr::Get(ctx, 1) }
124+
});
125+
126+
// l2 --> le
127+
cfa->createAssignTransition(l2, le);
128+
129+
// le --> exit [False]
130+
cfa->createAssignTransition(le, cfa->getExit(), BoolLiteralExpr::False(ctx));
131+
132+
std::vector<Location*> topo;
133+
llvm::DenseMap<Location*, size_t> indexMap;
134+
createTopologicalSort(*cfa, topo, &indexMap);
135+
auto builder = CreateFoldingExprBuilder(ctx);
136+
137+
PathConditionCalculator pathCond(
138+
topo, *builder,
139+
[&indexMap](auto l) { return indexMap[l]; },
140+
[&ctx](auto t) { return BoolLiteralExpr::True(ctx); },
141+
nullptr
142+
);
143+
144+
auto expected = builder->Or({
145+
builder->Eq(x->getRefExpr(), builder->IntLit(1)),
146+
builder->Eq(x->getRefExpr(), builder->IntLit(1)),
147+
});
148+
149+
auto actual = pathCond.encode(cfa->getEntry(), le);
150+
ASSERT_EQ(expected, actual);
151+
}
152+
153+
}

0 commit comments

Comments
 (0)
Please sign in to comment.