From 940779dc449885c87d13e48405360298a6591d33 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 8 May 2019 10:48:47 +0100
Subject: [PATCH 01/13] Rename guarded_rhs and use move instead of swap

The name better reflects what the variable represent and using move is
clearer than swap.
---
 src/goto-symex/symex_assign.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 879827a3f1d..57c3ea0587b 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -426,16 +426,16 @@ void goto_symext::symex_assign_symbol(
     return;
   }
 
-  exprt ssa_rhs=rhs;
+  exprt guarded_rhs = rhs;
 
   // put assignment guard into the rhs
   if(!guard.empty())
   {
-    if_exprt tmp_ssa_rhs(conjunction(guard), ssa_rhs, lhs, ssa_rhs.type());
-    tmp_ssa_rhs.swap(ssa_rhs);
+    guarded_rhs =
+      if_exprt{conjunction(guard), std::move(guarded_rhs), lhs, rhs.type()};
   }
 
-  exprt l2_rhs = state.rename(std::move(ssa_rhs), ns).get();
+  exprt l2_rhs = state.rename(std::move(guarded_rhs), ns).get();
 
   ssa_exprt lhs_mod = lhs;
 

From 5111b4d0b6a3be159787cd6826a0ba86939b9f86 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 8 May 2019 10:52:04 +0100
Subject: [PATCH 02/13] Better scope guarded_rhs

guarded_rhs is only used to define l2_rhs, we make this explicit in the code.
---
 src/goto-symex/symex_assign.cpp | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 57c3ea0587b..7da757984b6 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -426,16 +426,16 @@ void goto_symext::symex_assign_symbol(
     return;
   }
 
-  exprt guarded_rhs = rhs;
-
-  // put assignment guard into the rhs
-  if(!guard.empty())
-  {
-    guarded_rhs =
-      if_exprt{conjunction(guard), std::move(guarded_rhs), lhs, rhs.type()};
-  }
-
-  exprt l2_rhs = state.rename(std::move(guarded_rhs), ns).get();
+  exprt l2_rhs = [&]() {
+    exprt guarded_rhs = rhs;
+    // put assignment guard into the rhs
+    if(!guard.empty())
+    {
+      guarded_rhs =
+        if_exprt{conjunction(guard), std::move(guarded_rhs), lhs, rhs.type()};
+    }
+    return state.rename(std::move(guarded_rhs), ns).get();
+  }();
 
   ssa_exprt lhs_mod = lhs;
 

From cf576fc563231e59aba8f60911701c4e1258b17a Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 10 May 2019 07:30:58 +0100
Subject: [PATCH 03/13] Make shift_indexed_access_to_lhs return an exprt

This makes it a bit clearer what the shift_indexed_access_to_lhs
function produced.
It also avoids errors where the argument as a specific type but the
identifier is overwritten, for instance:
```
symbol_exprt s1 = ...;
shift_indexed_access_to_lhs(state, s1, lhs, ns, true);
assert(s1 == ID_symbol); // may fail though s1 has type symbol_exprt
```
---
 src/goto-symex/symex_assign.cpp | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 7da757984b6..8d7b3ca54c9 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -288,13 +288,14 @@ static void rewrite_with_to_field_symbols(
 /// "update") expressions, which \ref rewrite_with_to_field_symbols will then
 /// take care of.
 /// \param [in, out] state: symbolic execution state to perform renaming
-/// \param [in,out] ssa_rhs: right-hand side
+/// \param ssa_rhs: right-hand side
 /// \param [in,out] lhs_mod: left-hand side
 /// \param ns: namespace
 /// \param do_simplify: set to true if, and only if, simplification is enabled
-static void shift_indexed_access_to_lhs(
+/// \return updated right-hand side
+static exprt shift_indexed_access_to_lhs(
   goto_symext::statet &state,
-  exprt &ssa_rhs,
+  exprt ssa_rhs,
   ssa_exprt &lhs_mod,
   const namespacet &ns,
   bool do_simplify)
@@ -303,7 +304,7 @@ static void shift_indexed_access_to_lhs(
     ssa_rhs.id() == ID_byte_update_little_endian ||
     ssa_rhs.id() == ID_byte_update_big_endian)
   {
-    byte_update_exprt &byte_update = to_byte_update_expr(ssa_rhs);
+    const byte_update_exprt &byte_update = to_byte_update_expr(ssa_rhs);
     exprt byte_extract = byte_extract_exprt(
       byte_update.id() == ID_byte_update_big_endian
         ? ID_byte_extract_big_endian
@@ -316,8 +317,8 @@ static void shift_indexed_access_to_lhs(
 
     if(byte_extract.id() == ID_symbol)
     {
-      ssa_rhs = byte_update.value();
       lhs_mod = to_ssa_expr(byte_extract);
+      return byte_update.value();
     }
     else if(byte_extract.id() == ID_index || byte_extract.id() == ID_member)
     {
@@ -359,10 +360,11 @@ static void shift_indexed_access_to_lhs(
 
       // We may have shifted the previous lhs into the rhs; as the lhs is only
       // L1-renamed, we need to rename again.
-      ssa_rhs = state.rename(ssa_rhs, ns).get();
       lhs_mod = to_ssa_expr(byte_extract);
+      return state.rename(std::move(ssa_rhs), ns).get();
     }
   }
+  return ssa_rhs;
 }
 
 /// Assign a struct expression to a symbol. If \ref symex_assign_symbol was used
@@ -444,8 +446,8 @@ void goto_symext::symex_assign_symbol(
   // introduced by symex_assign_struct_member, are transformed into member
   // expressions on the LHS. If we add an option to disable field-sensitivity
   // in the future these should be omitted.
-  shift_indexed_access_to_lhs(
-    state, l2_rhs, lhs_mod, ns, symex_config.simplify_opt);
+  l2_rhs = shift_indexed_access_to_lhs(
+    state, std::move(l2_rhs), lhs_mod, ns, symex_config.simplify_opt);
   rewrite_with_to_field_symbols(state, l2_rhs, lhs_mod, ns);
 
   do_simplify(l2_rhs);

From ab30a67343e24a71ee33a4f355a20b1aedf4095f Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 10 May 2019 07:45:14 +0100
Subject: [PATCH 04/13] Return modified lhs in shift_indexed_access_to_lhs

This avoids having an input that is also an output and makes what is
modified by the call clearer.
The argument was copied before the call anyway.
---
 src/goto-symex/symex_assign.cpp | 40 ++++++++++++++++++---------------
 1 file changed, 22 insertions(+), 18 deletions(-)

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 8d7b3ca54c9..0cba3e1a75f 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -283,20 +283,27 @@ static void rewrite_with_to_field_symbols(
 #endif
 }
 
+/// Structure to hold the result of shift_indexed_access_to_lhs
+struct assignmentt final
+{
+  ssa_exprt lhs;
+  exprt rhs;
+};
+
 /// Replace byte-update operations that only affect individual fields of an
 /// expression by assignments to just those fields. May generate "with" (or
 /// "update") expressions, which \ref rewrite_with_to_field_symbols will then
 /// take care of.
 /// \param [in, out] state: symbolic execution state to perform renaming
 /// \param ssa_rhs: right-hand side
-/// \param [in,out] lhs_mod: left-hand side
+/// \param lhs_mod: left-hand side
 /// \param ns: namespace
 /// \param do_simplify: set to true if, and only if, simplification is enabled
-/// \return updated right-hand side
-static exprt shift_indexed_access_to_lhs(
+/// \return updated assignment
+static assignmentt shift_indexed_access_to_lhs(
   goto_symext::statet &state,
   exprt ssa_rhs,
-  ssa_exprt &lhs_mod,
+  ssa_exprt lhs_mod,
   const namespacet &ns,
   bool do_simplify)
 {
@@ -317,8 +324,7 @@ static exprt shift_indexed_access_to_lhs(
 
     if(byte_extract.id() == ID_symbol)
     {
-      lhs_mod = to_ssa_expr(byte_extract);
-      return byte_update.value();
+      return assignmentt{to_ssa_expr(byte_extract), byte_update.value()};
     }
     else if(byte_extract.id() == ID_index || byte_extract.id() == ID_member)
     {
@@ -360,11 +366,11 @@ static exprt shift_indexed_access_to_lhs(
 
       // We may have shifted the previous lhs into the rhs; as the lhs is only
       // L1-renamed, we need to rename again.
-      lhs_mod = to_ssa_expr(byte_extract);
-      return state.rename(std::move(ssa_rhs), ns).get();
+      return assignmentt{to_ssa_expr(byte_extract),
+                         state.rename(std::move(ssa_rhs), ns).get()};
     }
   }
-  return ssa_rhs;
+  return assignmentt{std::move(lhs_mod), std::move(ssa_rhs)};
 }
 
 /// Assign a struct expression to a symbol. If \ref symex_assign_symbol was used
@@ -439,24 +445,22 @@ void goto_symext::symex_assign_symbol(
     return state.rename(std::move(guarded_rhs), ns).get();
   }();
 
-  ssa_exprt lhs_mod = lhs;
-
   // Note the following two calls are specifically required for
   // field-sensitivity. For example, with-expressions, which may have just been
   // introduced by symex_assign_struct_member, are transformed into member
   // expressions on the LHS. If we add an option to disable field-sensitivity
   // in the future these should be omitted.
-  l2_rhs = shift_indexed_access_to_lhs(
-    state, std::move(l2_rhs), lhs_mod, ns, symex_config.simplify_opt);
-  rewrite_with_to_field_symbols(state, l2_rhs, lhs_mod, ns);
+  auto assignment = shift_indexed_access_to_lhs(
+    state, std::move(l2_rhs), lhs, ns, symex_config.simplify_opt);
+  rewrite_with_to_field_symbols(state, assignment.rhs, assignment.lhs, ns);
 
-  do_simplify(l2_rhs);
+  do_simplify(assignment.rhs);
 
-  ssa_exprt l2_lhs = lhs_mod;
+  ssa_exprt l2_lhs = std::move(assignment.lhs);
   ssa_exprt l1_lhs = l2_lhs; // l2_lhs will be renamed to L2 by the following:
   state.assignment(
     l2_lhs,
-    l2_rhs,
+    assignment.rhs,
     ns,
     symex_config.simplify_opt,
     symex_config.constant_propagation,
@@ -492,7 +496,7 @@ void goto_symext::symex_assign_symbol(
     l2_lhs,
     l2_full_lhs,
     original_lhs,
-    l2_rhs,
+    assignment.rhs,
     state.source,
     assignment_type);
 

From 9221e0ec71a9c1f09e81937174f7c05ba2a755c1 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 10 May 2019 08:12:17 +0100
Subject: [PATCH 05/13] Make rewrite_with_to_field_symbols return an
 assignmentt

This avoids having parameters that are also output value, which is not
clear from the calling site, and could cause some type mistakes when the
exprt parameters is from a subtype of exprt.
---
 src/goto-symex/symex_assign.cpp | 29 ++++++++++++++++-------------
 1 file changed, 16 insertions(+), 13 deletions(-)

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 0cba3e1a75f..643b04f3162 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -202,6 +202,13 @@ void goto_symext::symex_assign_rec(
       "assignment to `" + lhs.id_string() + "' not handled");
 }
 
+/// Assignment from the rhs value to the lhs variable
+struct assignmentt final
+{
+  ssa_exprt lhs;
+  exprt rhs;
+};
+
 /// Replace "with" (or "update") expressions in \p ssa_rhs by their update
 /// values and move the index or member to the left-hand side \p lhs_mod. This
 /// effectively undoes the work that \ref goto_symext::symex_assign_array and
@@ -209,13 +216,14 @@ void goto_symext::symex_assign_rec(
 /// of the index/member that may only be known after renaming to L2 has taken
 /// place.
 /// \param [in, out] state: symbolic execution state to perform renaming
-/// \param [in,out] ssa_rhs: right-hand side
-/// \param [in,out] lhs_mod: left-hand side
+/// \param ssa_rhs: right-hand side
+/// \param lhs_mod: left-hand side
 /// \param ns: namespace
-static void rewrite_with_to_field_symbols(
+/// \return the updated assignment
+static assignmentt rewrite_with_to_field_symbols(
   goto_symext::statet &state,
-  exprt &ssa_rhs,
-  ssa_exprt &lhs_mod,
+  exprt ssa_rhs,
+  ssa_exprt lhs_mod,
   const namespacet &ns)
 {
 #ifdef USE_UPDATE
@@ -281,15 +289,9 @@ static void rewrite_with_to_field_symbols(
     lhs_mod = to_ssa_expr(field_sensitive_lhs);
   }
 #endif
+  return assignmentt{std::move(lhs_mod), std::move(ssa_rhs)};
 }
 
-/// Structure to hold the result of shift_indexed_access_to_lhs
-struct assignmentt final
-{
-  ssa_exprt lhs;
-  exprt rhs;
-};
-
 /// Replace byte-update operations that only affect individual fields of an
 /// expression by assignments to just those fields. May generate "with" (or
 /// "update") expressions, which \ref rewrite_with_to_field_symbols will then
@@ -452,7 +454,8 @@ void goto_symext::symex_assign_symbol(
   // in the future these should be omitted.
   auto assignment = shift_indexed_access_to_lhs(
     state, std::move(l2_rhs), lhs, ns, symex_config.simplify_opt);
-  rewrite_with_to_field_symbols(state, assignment.rhs, assignment.lhs, ns);
+  assignment = rewrite_with_to_field_symbols(
+    state, std::move(assignment.rhs), std::move(assignment.lhs), ns);
 
   do_simplify(assignment.rhs);
 

From 892aacdfc14ddc792c2dac8fde9866f2ba11d173 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 10 May 2019 08:17:10 +0100
Subject: [PATCH 06/13] Make rewrite_to_field_symbols take assignmentt argument

This simplifies the call to this function and is clearer about the
semantical relation between the lhs and rhs arguments.
---
 src/goto-symex/symex_assign.cpp | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 643b04f3162..16f760e0a73 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -209,23 +209,24 @@ struct assignmentt final
   exprt rhs;
 };
 
-/// Replace "with" (or "update") expressions in \p ssa_rhs by their update
-/// values and move the index or member to the left-hand side \p lhs_mod. This
-/// effectively undoes the work that \ref goto_symext::symex_assign_array and
+/// Replace "with" (or "update") expressions in the right-hand side of
+/// \p assignment by their update values and move the index or member to the
+/// left-hand side of \p assignment. This effectively undoes the work that
+/// \ref goto_symext::symex_assign_array and
 /// \ref goto_symext::symex_assign_struct_member have done, but now making use
 /// of the index/member that may only be known after renaming to L2 has taken
 /// place.
 /// \param [in, out] state: symbolic execution state to perform renaming
-/// \param ssa_rhs: right-hand side
-/// \param lhs_mod: left-hand side
+/// \param assignment: an assignment to rewrite
 /// \param ns: namespace
 /// \return the updated assignment
 static assignmentt rewrite_with_to_field_symbols(
   goto_symext::statet &state,
-  exprt ssa_rhs,
-  ssa_exprt lhs_mod,
+  assignmentt assignment,
   const namespacet &ns)
 {
+  exprt &ssa_rhs = assignment.rhs;
+  ssa_exprt &lhs_mod = assignment.lhs;
 #ifdef USE_UPDATE
   while(ssa_rhs.id() == ID_update &&
         to_update_expr(ssa_rhs).designator().size() == 1 &&
@@ -289,7 +290,7 @@ static assignmentt rewrite_with_to_field_symbols(
     lhs_mod = to_ssa_expr(field_sensitive_lhs);
   }
 #endif
-  return assignmentt{std::move(lhs_mod), std::move(ssa_rhs)};
+  return assignment;
 }
 
 /// Replace byte-update operations that only affect individual fields of an
@@ -454,8 +455,7 @@ void goto_symext::symex_assign_symbol(
   // in the future these should be omitted.
   auto assignment = shift_indexed_access_to_lhs(
     state, std::move(l2_rhs), lhs, ns, symex_config.simplify_opt);
-  assignment = rewrite_with_to_field_symbols(
-    state, std::move(assignment.rhs), std::move(assignment.lhs), ns);
+  assignment = rewrite_with_to_field_symbols(state, std::move(assignment), ns);
 
   do_simplify(assignment.rhs);
 

From d51c192a6611f4e0a5d6fda04f17723ccd213a61 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 10 May 2019 08:20:43 +0100
Subject: [PATCH 07/13] Make shift_indexed_access_to_lhs take assignment
 argument

This makes the relation between lhs and rhs clearer.
---
 src/goto-symex/symex_assign.cpp | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 16f760e0a73..a791f0679b1 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -298,18 +298,18 @@ static assignmentt rewrite_with_to_field_symbols(
 /// "update") expressions, which \ref rewrite_with_to_field_symbols will then
 /// take care of.
 /// \param [in, out] state: symbolic execution state to perform renaming
-/// \param ssa_rhs: right-hand side
-/// \param lhs_mod: left-hand side
+/// \param assignment: assignment to transform
 /// \param ns: namespace
 /// \param do_simplify: set to true if, and only if, simplification is enabled
 /// \return updated assignment
 static assignmentt shift_indexed_access_to_lhs(
   goto_symext::statet &state,
-  exprt ssa_rhs,
-  ssa_exprt lhs_mod,
+  assignmentt assignment,
   const namespacet &ns,
   bool do_simplify)
 {
+  exprt &ssa_rhs = assignment.rhs;
+  ssa_exprt &lhs_mod = assignment.lhs;
   if(
     ssa_rhs.id() == ID_byte_update_little_endian ||
     ssa_rhs.id() == ID_byte_update_big_endian)
@@ -373,7 +373,7 @@ static assignmentt shift_indexed_access_to_lhs(
                          state.rename(std::move(ssa_rhs), ns).get()};
     }
   }
-  return assignmentt{std::move(lhs_mod), std::move(ssa_rhs)};
+  return assignment;
 }
 
 /// Assign a struct expression to a symbol. If \ref symex_assign_symbol was used
@@ -454,7 +454,7 @@ void goto_symext::symex_assign_symbol(
   // expressions on the LHS. If we add an option to disable field-sensitivity
   // in the future these should be omitted.
   auto assignment = shift_indexed_access_to_lhs(
-    state, std::move(l2_rhs), lhs, ns, symex_config.simplify_opt);
+    state, assignmentt{lhs, std::move(l2_rhs)}, ns, symex_config.simplify_opt);
   assignment = rewrite_with_to_field_symbols(state, std::move(assignment), ns);
 
   do_simplify(assignment.rhs);

From faeb70cee85de2a012f250e1d93e971f2d21328a Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 10 May 2019 08:49:33 +0100
Subject: [PATCH 08/13] Make assignment return rename lhs

This avoids having an input that is also an output and clarifies how lhs
is changed.
---
 src/goto-symex/field_sensitivity.cpp | 12 +++++++++---
 src/goto-symex/goto_symex_state.cpp  | 22 +++++++++++++---------
 src/goto-symex/goto_symex_state.h    |  9 +++++----
 src/goto-symex/symex_assign.cpp      | 19 ++++++++++---------
 src/goto-symex/symex_goto.cpp        |  7 ++++---
 5 files changed, 41 insertions(+), 28 deletions(-)

diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
index f6dbc409471..fc05ad82213 100644
--- a/src/goto-symex/field_sensitivity.cpp
+++ b/src/goto-symex/field_sensitivity.cpp
@@ -222,9 +222,15 @@ void field_sensitivityt::field_assignments_rec(
     exprt ssa_rhs = state.rename(lhs, ns).get();
     simplify(ssa_rhs, ns);
 
-    ssa_exprt ssa_lhs = to_ssa_expr(lhs_fs);
-    state.assignment(
-      ssa_lhs, ssa_rhs, ns, true, true, allow_pointer_unsoundness);
+    const ssa_exprt ssa_lhs = state
+                                .assignment(
+                                  to_ssa_expr(lhs_fs),
+                                  ssa_rhs,
+                                  ns,
+                                  true,
+                                  true,
+                                  allow_pointer_unsoundness)
+                                .get();
 
     // do the assignment
     target.assignment(
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index c7b31662373..3e5dba24070 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -151,9 +151,9 @@ goto_symex_statet::set_indices<L2>(ssa_exprt ssa_expr, const namespacet &ns)
   return level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
 }
 
-void goto_symex_statet::assignment(
-  ssa_exprt &lhs, // L0/L1
-  const exprt &rhs,  // L2
+renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
+  ssa_exprt lhs,    // L0/L1
+  const exprt &rhs, // L2
   const namespacet &ns,
   bool rhs_is_simplified,
   bool record_value,
@@ -182,7 +182,8 @@ void goto_symex_statet::assignment(
 
   // do the l2 renaming
   increase_generation(l1_identifier, lhs);
-  lhs = set_indices<L2>(std::move(lhs), ns).get();
+  renamedt<ssa_exprt, L2> l2_lhs = set_indices<L2>(std::move(lhs), ns);
+  lhs = l2_lhs.get();
 
   // in case we happen to be multi-threaded, record the memory access
   bool is_shared=l2_thread_write_encoding(lhs, ns);
@@ -233,6 +234,8 @@ void goto_symex_statet::assignment(
   value_set.output(ns, std::cout);
   std::cout << "**********************\n";
 #endif
+
+  return l2_lhs;
 }
 
 template <levelt level>
@@ -444,19 +447,20 @@ bool goto_symex_statet::l2_thread_read_encoding(
 
     const bool record_events_bak=record_events;
     record_events=false;
-    assignment(ssa_l1, tmp, ns, true, true);
+    ssa_exprt ssa_l2 = assignment(std::move(ssa_l1), tmp, ns, true, true).get();
     record_events=record_events_bak;
 
     symex_target->assignment(
       guard_as_expr,
-      ssa_l1,
-      ssa_l1,
-      ssa_l1.get_original_expr(),
+      ssa_l2,
+      ssa_l2,
+      ssa_l2.get_original_expr(),
       tmp,
       source,
       symex_targett::assignment_typet::PHI);
 
-    expr = set_indices<L2>(std::move(ssa_l1), ns).get();
+    // TODO: are we setting l2 indices of something that is already l2?
+    expr = set_indices<L2>(std::move(ssa_l2), ns).get();
 
     a_s_read.second.push_back(guard);
     if(!no_write.op().is_false())
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index e568a5ee04b..c7ae6fab70a 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -108,13 +108,14 @@ class goto_symex_statet final : public goto_statet
   template <levelt level = L2>
   void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
 
-  void assignment(
-    ssa_exprt &lhs, // L0/L1
-    const exprt &rhs,  // L2
+  /// \return lhs renamed to level 2
+  renamedt<ssa_exprt, L2> assignment(
+    ssa_exprt lhs,    // L0/L1
+    const exprt &rhs, // L2
     const namespacet &ns,
     bool rhs_is_simplified,
     bool record_value,
-    bool allow_pointer_unsoundness=false);
+    bool allow_pointer_unsoundness = false);
 
   field_sensitivityt field_sensitivity;
 
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index a791f0679b1..ba1b1014031 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -459,15 +459,16 @@ void goto_symext::symex_assign_symbol(
 
   do_simplify(assignment.rhs);
 
-  ssa_exprt l2_lhs = std::move(assignment.lhs);
-  ssa_exprt l1_lhs = l2_lhs; // l2_lhs will be renamed to L2 by the following:
-  state.assignment(
-    l2_lhs,
-    assignment.rhs,
-    ns,
-    symex_config.simplify_opt,
-    symex_config.constant_propagation,
-    symex_config.allow_pointer_unsoundness);
+  ssa_exprt &l1_lhs = assignment.lhs;
+  ssa_exprt l2_lhs = state
+                       .assignment(
+                         assignment.lhs,
+                         assignment.rhs,
+                         ns,
+                         symex_config.simplify_opt,
+                         symex_config.constant_propagation,
+                         symex_config.allow_pointer_unsoundness)
+                       .get();
 
   exprt ssa_full_lhs=full_lhs;
   ssa_full_lhs = add_to_lhs(ssa_full_lhs, l2_lhs);
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index baa61bc7647..c6b820c00ca 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -310,7 +310,8 @@ void goto_symext::symex_goto(statet &state)
 
       ssa_exprt new_lhs =
         state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns).get();
-      state.assignment(new_lhs, new_rhs, ns, true, false);
+      new_lhs =
+        state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get();
 
       guardt guard{true_exprt{}, guard_manager};
 
@@ -527,10 +528,10 @@ static void merge_names(
       simplify(rhs, ns);
   }
 
-  ssa_exprt new_lhs = ssa;
   const bool record_events = dest_state.record_events;
   dest_state.record_events = false;
-  dest_state.assignment(new_lhs, rhs, ns, true, true);
+  const ssa_exprt new_lhs =
+    dest_state.assignment(ssa, rhs, ns, true, true).get();
   dest_state.record_events = record_events;
 
   log.conditional_output(

From 822c49357222834cce5c28787bbe87b7bca7756a Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 10 May 2019 08:59:35 +0100
Subject: [PATCH 09/13] Replace record_events by a stack

In practice there was an implicit stack of record events backup through
the recursive calls, this makes the stack explicit.
---
 src/goto-symex/goto_symex_state.cpp   | 11 +++++------
 src/goto-symex/goto_symex_state.h     |  2 +-
 src/goto-symex/symex_assign.cpp       |  5 ++---
 src/goto-symex/symex_decl.cpp         |  5 ++---
 src/goto-symex/symex_goto.cpp         |  5 ++---
 src/goto-symex/symex_main.cpp         |  5 ++---
 src/goto-symex/symex_start_thread.cpp |  5 ++---
 7 files changed, 16 insertions(+), 22 deletions(-)

diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 3e5dba24070..a5267813b2c 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -38,7 +38,7 @@ goto_symex_statet::goto_symex_statet(
     source(_source),
     guard_manager(manager),
     symex_target(nullptr),
-    record_events(true),
+    record_events({true}),
     fresh_l2_name_provider(fresh_l2_name_provider)
 {
   threads.emplace_back(guard_manager);
@@ -445,10 +445,9 @@ bool goto_symex_statet::l2_thread_read_encoding(
     else
       tmp = if_exprt{cond.as_expr(), l2_true_case.get(), l2_false_case.get()};
 
-    const bool record_events_bak=record_events;
-    record_events=false;
+    record_events.push(false);
     ssa_exprt ssa_l2 = assignment(std::move(ssa_l1), tmp, ns, true, true).get();
-    record_events=record_events_bak;
+    record_events.pop();
 
     symex_target->assignment(
       guard_as_expr,
@@ -470,7 +469,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
   }
 
   // No event and no fresh index, but avoid constant propagation
-  if(!record_events)
+  if(!record_events.top())
   {
     expr = set_indices<L2>(std::move(ssa_l1), ns).get();
     return true;
@@ -492,7 +491,7 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(
   const ssa_exprt &expr,
   const namespacet &ns) const
 {
-  if(!record_events)
+  if(!record_events.top())
     return write_is_shared_resultt::NOT_SHARED;
 
   PRECONDITION(dirty != nullptr);
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index c7ae6fab70a..3751037956f 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -198,7 +198,7 @@ class goto_symex_statet final : public goto_statet
   write_is_shared_resultt
   write_is_shared(const ssa_exprt &expr, const namespacet &ns) const;
 
-  bool record_events;
+  std::stack<bool> record_events;
 
   const incremental_dirtyt *dirty = nullptr;
 
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index ba1b1014031..cd543f7f7bd 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -472,10 +472,9 @@ void goto_symext::symex_assign_symbol(
 
   exprt ssa_full_lhs=full_lhs;
   ssa_full_lhs = add_to_lhs(ssa_full_lhs, l2_lhs);
-  const bool record_events=state.record_events;
-  state.record_events=false;
+  state.record_events.push(false);
   exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns).get();
-  state.record_events=record_events;
+  state.record_events.pop();
 
   // do the assignment
   const symbolt &symbol = ns.lookup(l2_lhs.get_object_name());
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index 660bd640d04..55f3e7cc1d8 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -76,14 +76,13 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     CHECK_RETURN(field_generation == 1);
   }
 
-  const bool record_events=state.record_events;
-  state.record_events=false;
+  state.record_events.push(false);
   exprt expr_l2 = state.rename(std::move(ssa), ns).get();
   INVARIANT(
     expr_l2.id() == ID_symbol && expr_l2.get_bool(ID_C_SSA_symbol),
     "symbol to declare should not be replaced by constant propagation");
   ssa = to_ssa_expr(expr_l2);
-  state.record_events=record_events;
+  state.record_events.pop();
 
   // we hide the declaration of auxiliary variables
   // and if the statement itself is hidden
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index c6b820c00ca..0fdfcbbe938 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -528,11 +528,10 @@ static void merge_names(
       simplify(rhs, ns);
   }
 
-  const bool record_events = dest_state.record_events;
-  dest_state.record_events = false;
+  dest_state.record_events.push(false);
   const ssa_exprt new_lhs =
     dest_state.assignment(ssa, rhs, ns, true, true).get();
-  dest_state.record_events = record_events;
+  dest_state.record_events.pop();
 
   log.conditional_output(
     log.debug(), [ns, &new_lhs](messaget::mstreamt &mstream) {
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 2a3fb8b92b2..a1eccab9bf4 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -747,10 +747,9 @@ void goto_symext::try_filter_value_sets(
     // something that just replaces `*&x` with `x` whenever it finds it.
     do_simplify(modified_condition);
 
-    const bool record_events = state.record_events;
-    state.record_events = false;
+    state.record_events.push(false);
     modified_condition = state.rename(std::move(modified_condition), ns).get();
-    state.record_events = record_events;
+    state.record_events.pop();
 
     do_simplify(modified_condition);
 
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index cdd483f6e32..66921875c32 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -85,8 +85,7 @@ void goto_symext::symex_start_thread(statet &state)
     ssa_exprt rhs = pair.second.first;
 
     exprt::operandst lhs_conditions;
-    const bool record_events=state.record_events;
-    state.record_events=false;
+    state.record_events.push(false);
     symex_assign_symbol(
       state,
       lhs_l1,
@@ -94,7 +93,7 @@ void goto_symext::symex_start_thread(statet &state)
       rhs,
       lhs_conditions,
       symex_targett::assignment_typet::HIDDEN);
-    state.record_events=record_events;
+    state.record_events.pop();
   }
 
   // initialize all variables marked thread-local

From 5d0ac3ab02bd24a821c097a581fa8bd7d18d7cdf Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 10 May 2019 09:02:02 +0100
Subject: [PATCH 10/13] Avoid unneccessary copy

The argument of add_to_lhs are const anyway.
---
 src/goto-symex/symex_assign.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index cd543f7f7bd..3a3aadd087a 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -470,8 +470,7 @@ void goto_symext::symex_assign_symbol(
                          symex_config.allow_pointer_unsoundness)
                        .get();
 
-  exprt ssa_full_lhs=full_lhs;
-  ssa_full_lhs = add_to_lhs(ssa_full_lhs, l2_lhs);
+  exprt ssa_full_lhs = add_to_lhs(full_lhs, l2_lhs);
   state.record_events.push(false);
   exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns).get();
   state.record_events.pop();

From ae52ed3f83a21767fbf22ff5e447090b542bfd8d Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 10 May 2019 09:03:14 +0100
Subject: [PATCH 11/13] Mark l2_full_lhs const

It is not modified after assignment.
---
 src/goto-symex/symex_assign.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 3a3aadd087a..c4a87c45da1 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -472,7 +472,7 @@ void goto_symext::symex_assign_symbol(
 
   exprt ssa_full_lhs = add_to_lhs(full_lhs, l2_lhs);
   state.record_events.push(false);
-  exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns).get();
+  const exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns).get();
   state.record_events.pop();
 
   // do the assignment

From d6418ff65296ee7697ce22da1ba67ff5350dbfb3 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 10 May 2019 09:16:07 +0100
Subject: [PATCH 12/13] Make get_original_name return the expression

This avoids having an input that is also an output and make the calls to
get_original_name clearer.
---
 src/goto-symex/postcondition.cpp     |  7 +++----
 src/goto-symex/precondition.cpp      |  3 +--
 src/goto-symex/renaming_level.cpp    | 23 ++++++++++++++---------
 src/goto-symex/renaming_level.h      |  4 ++--
 src/goto-symex/symex_assign.cpp      |  3 +--
 src/goto-symex/symex_dereference.cpp |  4 ++--
 6 files changed, 23 insertions(+), 21 deletions(-)

diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index d6c7eb69d32..317297c6c7e 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -130,8 +130,8 @@ void postconditiont::strengthen(exprt &dest)
        SSA_step.ssa_lhs.type().id()==ID_struct)
       return;
 
-    equal_exprt equality(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
-    get_original_name(equality);
+    exprt equality =
+      get_original_name(equal_exprt{SSA_step.ssa_lhs, SSA_step.ssa_rhs});
 
     if(dest.is_true())
       dest.swap(equality);
@@ -169,8 +169,7 @@ bool postconditiont::is_used(
         it!=expr_set.end();
         it++)
     {
-      exprt tmp(*it);
-      get_original_name(tmp);
+      const exprt tmp = get_original_name(*it);
       find_symbols(tmp, symbols);
     }
 
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index abd9d8983be..dd0ccb50296 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -140,8 +140,7 @@ void preconditiont::compute_rec(exprt &dest)
   }
   else if(dest==SSA_step.ssa_lhs.get_original_expr())
   {
-    dest=SSA_step.ssa_rhs;
-    get_original_name(dest);
+    dest = get_original_name(SSA_step.ssa_rhs);
   }
   else
     Forall_operands(it, dest)
diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp
index d187c11a776..949b47ceea3 100644
--- a/src/goto-symex/renaming_level.cpp
+++ b/src/goto-symex/renaming_level.cpp
@@ -97,26 +97,29 @@ void symex_level1t::restore_from(const current_namest &other)
   }
 }
 
-void get_original_name(exprt &expr)
+exprt get_original_name(exprt expr)
 {
-  get_original_name(expr.type());
+  expr.type() = get_original_name(std::move(expr.type()));
 
   if(expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol))
-    expr = to_ssa_expr(expr).get_original_expr();
+    return to_ssa_expr(expr).get_original_expr();
   else
+  {
     Forall_operands(it, expr)
-      get_original_name(*it);
+      *it = get_original_name(std::move(*it));
+    return expr;
+  }
 }
 
-void get_original_name(typet &type)
+typet get_original_name(typet type)
 {
   // rename all the symbols with their last known value
 
   if(type.id() == ID_array)
   {
     auto &array_type = to_array_type(type);
-    get_original_name(array_type.subtype());
-    get_original_name(array_type.size());
+    array_type.subtype() = get_original_name(std::move(array_type.subtype()));
+    array_type.size() = get_original_name(std::move(array_type.size()));
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
   {
@@ -124,10 +127,12 @@ void get_original_name(typet &type)
     struct_union_typet::componentst &components = s_u_type.components();
 
     for(auto &component : components)
-      get_original_name(component.type());
+      component.type() = get_original_name(std::move(component.type()));
   }
   else if(type.id() == ID_pointer)
   {
-    get_original_name(to_pointer_type(type).subtype());
+    type.subtype() =
+      get_original_name(std::move(to_pointer_type(type).subtype()));
   }
+  return type;
 }
diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h
index c2a631619a7..8096ca37cf0 100644
--- a/src/goto-symex/renaming_level.h
+++ b/src/goto-symex/renaming_level.h
@@ -148,9 +148,9 @@ struct symex_level2t : public symex_renaming_levelt
 };
 
 /// Undo all levels of renaming
-void get_original_name(exprt &expr);
+exprt get_original_name(exprt expr);
 
 /// Undo all levels of renaming
-void get_original_name(typet &type);
+typet get_original_name(typet type);
 
 #endif // CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index c4a87c45da1..c1117be4ed1 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -491,8 +491,7 @@ void goto_symext::symex_assign_symbol(
   // Temporarily add the state guard
   guard.emplace_back(state.guard.as_expr());
 
-  exprt original_lhs = l2_full_lhs;
-  get_original_name(original_lhs);
+  const exprt original_lhs = get_original_name(l2_full_lhs);
   target.assignment(
     conjunction(guard),
     l2_lhs,
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 1e6d54747f5..5489a8df717 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -202,7 +202,6 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
 {
   if(expr.id()==ID_dereference)
   {
-    dereference_exprt to_check = to_dereference_expr(expr);
     bool expr_is_not_null = false;
 
     if(state.threads.size() == 1)
@@ -210,7 +209,8 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
       const irep_idt &expr_function = state.source.function_id;
       if(!expr_function.empty())
       {
-        get_original_name(to_check);
+        const dereference_exprt to_check =
+          to_dereference_expr(get_original_name(expr));
 
         expr_is_not_null = path_storage.safe_pointers.at(expr_function)
                              .is_safe_dereference(to_check, state.source.pc);

From fdc03e0ac87d45be70296b902aafc091b0e8f319 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 10 May 2019 09:31:20 +0100
Subject: [PATCH 13/13] Replace set_indices by an invariant

ssa_l2 is already an L2 expression, its indices doesn't need to be reset.
We just check that the renaming was correct instead.
---
 src/goto-symex/goto_symex_state.cpp | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index a5267813b2c..7c6360134ef 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -47,7 +47,8 @@ goto_symex_statet::goto_symex_statet(
 
 goto_symex_statet::~goto_symex_statet()=default;
 
-/// write to a variable
+/// Check that \p expr is correctly renamed to level 2 and return true in case
+/// an error is detected.
 static bool check_renaming(const exprt &expr);
 
 static bool check_renaming(const typet &type)
@@ -458,8 +459,8 @@ bool goto_symex_statet::l2_thread_read_encoding(
       source,
       symex_targett::assignment_typet::PHI);
 
-    // TODO: are we setting l2 indices of something that is already l2?
-    expr = set_indices<L2>(std::move(ssa_l2), ns).get();
+    INVARIANT(!check_renaming(ssa_l2), "expr should be renamed to L2");
+    expr = std::move(ssa_l2);
 
     a_s_read.second.push_back(guard);
     if(!no_write.op().is_false())