From 862aa15009841e7221720040460e612245d8bf24 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 29 May 2019 17:27:15 +0100 Subject: [PATCH] Do not assign a non-ssa expr to an object that is accessed via an ssa_exprt ref Previously a variable `expr` of type `exprt &` was cast to `ssa_exprt &` and assigned to variable `ssa`. Later the object was modified via assigning a non-ssa expression to `expr`, violating the invariants of `ssa_exprt`. --- src/goto-symex/goto_symex_state.cpp | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 7c6360134ef..61165b1551d 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -285,13 +285,10 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) rename(expr.type(), ssa.get_identifier(), ns); ssa.update_type(); - if(l2_thread_read_encoding(ssa, ns)) + // renaming taken care of by l2_thread_encoding, or already at L2 + if(l2_thread_read_encoding(ssa, ns) || !ssa.get_level_2().empty()) { - // renaming taken care of by l2_thread_encoding - } - else if(!ssa.get_level_2().empty()) - { - // already at L2 + return renamedt(std::move(ssa)); } else { @@ -300,11 +297,15 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) auto p_it = propagation.find(ssa.get_identifier()); if(p_it.has_value()) - expr = *p_it; // already L2 + { + return renamedt(*p_it); // already L2 + } else + { ssa = set_indices(std::move(ssa), ns).get(); + return renamedt(std::move(ssa)); + } } - return renamedt(std::move(ssa)); } } else if(expr.id()==ID_symbol)