Skip to content

Commit 56aaf0c

Browse files
committed
Avoid repeated computation of guardt::operator-=
Each iteration of the loop yields the same expression. Avoiding repeated construction enables trivial sharing rather than relying on merge_irepst for a reduced memory footprint, and reduces the computational cost as guardt::operator-= is non-trivial.
1 parent 320722f commit 56aaf0c

File tree

1 file changed

+11
-6
lines changed

1 file changed

+11
-6
lines changed

src/goto-symex/symex_goto.cpp

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -350,6 +350,16 @@ void goto_symext::phi_function(
350350
goto_state.level2_get_variables(variables);
351351
dest_state.level2.get_variables(variables);
352352

353+
guardt diff_guard;
354+
355+
if(!variables.empty())
356+
{
357+
diff_guard=goto_state.guard;
358+
359+
// this gets the diff between the guards
360+
diff_guard-=dest_state.guard;
361+
}
362+
353363
for(std::unordered_set<ssa_exprt, irep_hash>::const_iterator
354364
it=variables.begin();
355365
it!=variables.end();
@@ -417,12 +427,7 @@ void goto_symext::phi_function(
417427
rhs=dest_state_rhs;
418428
else
419429
{
420-
guardt tmp_guard(goto_state.guard);
421-
422-
// this gets the diff between the guards
423-
tmp_guard-=dest_state.guard;
424-
425-
rhs=if_exprt(tmp_guard.as_expr(), goto_state_rhs, dest_state_rhs);
430+
rhs=if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);
426431
do_simplify(rhs);
427432
}
428433

0 commit comments

Comments
 (0)