27
27
28
28
static void get_l1_name (exprt &expr);
29
29
30
+ static void set_l2_indices (
31
+ symex_level0t level0,
32
+ symex_level1t level1,
33
+ symex_level2t level2,
34
+ ssa_exprt &ssa_expr,
35
+ unsigned int thread_nr,
36
+ const namespacet &ns);
37
+
30
38
goto_symex_statet::goto_symex_statet ()
31
39
: depth(0 ),
32
40
symex_target(nullptr ),
@@ -190,7 +198,7 @@ void goto_symex_statet::assignment(
190
198
const auto level2_it =
191
199
level2.current_names .emplace (l1_identifier, std::make_pair (lhs, 0 )).first ;
192
200
symex_renaming_levelt::increase_counter (level2_it);
193
- set_l2_indices (lhs, ns);
201
+ set_l2_indices (level0, level1, level2, lhs, source. thread_nr , ns);
194
202
195
203
// in case we happen to be multi-threaded, record the memory access
196
204
bool is_shared=l2_thread_write_encoding (lhs, ns);
@@ -261,13 +269,17 @@ static void set_l1_indices(
261
269
level1 (ssa_expr);
262
270
}
263
271
264
- void goto_symex_statet::set_l2_indices (
272
+ static void set_l2_indices (
273
+ symex_level0t level0,
274
+ symex_level1t level1,
275
+ symex_level2t level2,
265
276
ssa_exprt &ssa_expr,
277
+ unsigned int thread_nr,
266
278
const namespacet &ns)
267
279
{
268
280
if (!ssa_expr.get_level_2 ().empty ())
269
281
return ;
270
- level0 (ssa_expr, ns, source. thread_nr );
282
+ level0 (ssa_expr, ns, thread_nr);
271
283
level1 (ssa_expr);
272
284
ssa_expr.set_level_2 (level2.current_count (ssa_expr.get_identifier ()));
273
285
}
@@ -319,7 +331,7 @@ void goto_symex_statet::rename(
319
331
if (p_it != propagation.end ())
320
332
expr=p_it->second ; // already L2
321
333
else
322
- set_l2_indices (ssa, ns);
334
+ set_l2_indices (level0, level1, level2, ssa, source. thread_nr , ns);
323
335
}
324
336
}
325
337
}
@@ -439,7 +451,8 @@ bool goto_symex_statet::l2_thread_read_encoding(
439
451
cond |= guardt{no_write.op ()};
440
452
441
453
if_exprt tmp (cond.as_expr (), ssa_l1, ssa_l1);
442
- set_l2_indices (to_ssa_expr (tmp.true_case ()), ns);
454
+ auto &ssa_true = to_ssa_expr (tmp.true_case ());
455
+ set_l2_indices (level0, level1, level2, ssa_true, source.thread_nr , ns);
443
456
444
457
if (a_s_read.second .empty ())
445
458
{
@@ -472,7 +485,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
472
485
source,
473
486
symex_targett::assignment_typet::PHI);
474
487
475
- set_l2_indices (ssa_l1, ns);
488
+ set_l2_indices (level0, level1, level2, ssa_l1, source. thread_nr , ns);
476
489
expr=ssa_l1;
477
490
478
491
a_s_read.second .push_back (guard);
@@ -489,14 +502,14 @@ bool goto_symex_statet::l2_thread_read_encoding(
489
502
// No event and no fresh index, but avoid constant propagation
490
503
if (!record_events)
491
504
{
492
- set_l2_indices (ssa_l1, ns);
505
+ set_l2_indices (level0, level1, level2, ssa_l1, source. thread_nr , ns);
493
506
expr=ssa_l1;
494
507
return true ;
495
508
}
496
509
497
510
// produce a fresh L2 name
498
511
symex_renaming_levelt::increase_counter (level2_it);
499
- set_l2_indices (ssa_l1, ns);
512
+ set_l2_indices (level0, level1, level2, ssa_l1, source. thread_nr , ns);
500
513
expr=ssa_l1;
501
514
502
515
// and record that
0 commit comments