Skip to content

Commit a71d19c

Browse files
Avoid uneccessary calls to guardt::as_expr()
We aim at providing other implementations of guardt which may not be encoded using exprt only. In that case, `as_expr` may not be a trivial operation as it is now, so it is better to minimize the number of times it gets called.
1 parent c05fd3e commit a71d19c

File tree

2 files changed

+12
-12
lines changed

2 files changed

+12
-12
lines changed

src/analyses/goto_check.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1407,16 +1407,15 @@ void goto_checkt::add_guarded_claim(
14071407
return;
14081408

14091409
// add the guard
1410-
exprt guard_expr=guard.as_expr();
14111410

14121411
exprt new_expr;
14131412

1414-
if(guard_expr.is_true())
1413+
if(guard.is_true())
14151414
new_expr.swap(expr);
14161415
else
14171416
{
14181417
new_expr=exprt(ID_implies, bool_typet());
1419-
new_expr.move_to_operands(guard_expr, expr);
1418+
new_expr.add_to_operands(guard.as_expr(), std::move(expr));
14201419
}
14211420

14221421
if(assertions.insert(new_expr).second)

src/goto-symex/goto_symex_state.cpp

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -384,6 +384,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
384384
ssa_exprt ssa_l1=expr;
385385
ssa_l1.remove_level_2();
386386
const irep_idt &l1_identifier=ssa_l1.get_identifier();
387+
const exprt guard_as_expr = guard.as_expr();
387388

388389
// see whether we are within an atomic section
389390
if(atomic_section_id!=0)
@@ -430,11 +431,15 @@ bool goto_symex_statet::l2_thread_read_encoding(
430431
read_guard |= a_s_read_guard;
431432
}
432433

433-
exprt cond=read_guard.as_expr();
434+
guardt cond = read_guard;
434435
if(!no_write.op().is_false())
435-
cond=or_exprt(no_write.op(), cond);
436+
{
437+
guardt no_write_guard;
438+
no_write_guard.add(no_write.op());
439+
cond |= no_write_guard;
440+
}
436441

437-
if_exprt tmp(cond, ssa_l1, ssa_l1);
442+
if_exprt tmp(cond.as_expr(), ssa_l1, ssa_l1);
438443
set_l2_indices(to_ssa_expr(tmp.true_case()), ns);
439444

440445
if(a_s_read.second.empty())
@@ -460,7 +465,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
460465
record_events=record_events_bak;
461466

462467
symex_target->assignment(
463-
guard.as_expr(),
468+
guard_as_expr,
464469
ssa_l1,
465470
ssa_l1,
466471
ssa_l1.get_original_expr(),
@@ -498,11 +503,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
498503
// and record that
499504
INVARIANT_STRUCTURED(
500505
symex_target!=nullptr, nullptr_exceptiont, "symex_target is null");
501-
symex_target->shared_read(
502-
guard.as_expr(),
503-
expr,
504-
atomic_section_id,
505-
source);
506+
symex_target->shared_read(guard_as_expr, expr, atomic_section_id, source);
506507

507508
return true;
508509
}

0 commit comments

Comments
 (0)