Document byte_update_exprt and rename non-const functions

src/solvers/lowering/byte_operators.cpp

@@ -1497,7 +1497,7 @@ static exprt lower_byte_update_struct(
         array_typet{bv_typet{8}, src_size_opt.value()}};
 
       byte_update_exprt bu = src;
-      bu.op() = lower_byte_extract(byte_extract_expr, ns);
+      bu.set_op(lower_byte_extract(byte_extract_expr, ns));
 
       return lower_byte_extract(
         byte_extract_exprt{
@@ -1615,7 +1615,7 @@ static exprt lower_byte_update_union(
     "lower_byte_update of union of unknown size is not supported");
 
   byte_update_exprt bu = src;
-  bu.op() = member_exprt{src.op(), max_comp_name, max_comp_type};
+  bu.set_op(member_exprt{src.op(), max_comp_name, max_comp_type});
   bu.type() = max_comp_type;
 
   return union_exprt{

src/util/byte_operators.h

@@ -20,8 +20,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "invariant.h"
 #include "std_expr.h"
 
-/*! \brief TO_BE_DOCUMENTED
-*/
+/// Expression of type \c type extracted from some object \c op starting at
+/// position \c offset (given in number of bytes).
+/// The object can either be interpreted in big endian or little endian, which
+/// is reflected by the \c id of the expression which is either
+/// \c ID_byte_extract_big_endian or \c ID_byte_extract_little_endian
 class byte_extract_exprt:public binary_exprt
 {
 public:
@@ -69,8 +72,9 @@ inline byte_extract_exprt &to_byte_extract_expr(exprt &expr)
 irep_idt byte_extract_id();
 irep_idt byte_update_id();
 
-/*! \brief TO_BE_DOCUMENTED
-*/
+/// Expression corresponding to \c op() where the bytes starting at
+/// position \c offset (given in number of bytes) have been updated with
+/// \c value.
 class byte_update_exprt : public ternary_exprt
 {
 public:
@@ -83,10 +87,26 @@ class byte_update_exprt : public ternary_exprt
   {
   }
 
+  DEPRECATED(SINCE(2019, 5, 21, "use set_op or as_const instead"))
   exprt &op() { return op0(); }
+  DEPRECATED(SINCE(2019, 5, 21, "use set_offset or as_const instead"))
   exprt &offset() { return op1(); }
+  DEPRECATED(SINCE(2019, 5, 21, "use set_value or as_const instead"))
   exprt &value() { return op2(); }
 
+  void set_op(exprt e)
+  {
+    op0() = std::move(e);
+  }
+  void set_offset(exprt e)
+  {
+    op1() = std::move(e);
+  }
+  void set_value(exprt e)
+  {
+    op2() = std::move(e);
+  }
+
   const exprt &op() const { return op0(); }
   const exprt &offset() const { return op1(); }
   const exprt &value() const { return op2(); }

src/util/simplify_expr.cpp

@@ -1902,7 +1902,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
       expr.op().id() == ID_byte_update_big_endian) ||
      (expr.id() == ID_byte_extract_little_endian &&
       expr.op().id() == ID_byte_update_little_endian)) &&
-    expr.offset() == to_byte_update_expr(expr.op()).offset())
+    expr.offset() == to_byte_update_expr(as_const(expr).op()).offset())
   {
     const auto &op_byte_update = to_byte_update_expr(expr.op());
 
@@ -2057,20 +2057,22 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
 
 bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
 {
+  const byte_update_exprt &expr_const = expr;
   // byte_update(byte_update(root, offset, value), offset, value2) =>
   // byte_update(root, offset, value2)
   if(
-    expr.id() == expr.op().id() &&
-    expr.offset() == to_byte_update_expr(expr.op()).offset() &&
-    expr.value().type() == to_byte_update_expr(expr.op()).value().type())
+    expr_const.id() == expr_const.op().id() &&
+    expr_const.offset() == to_byte_update_expr(expr_const.op()).offset() &&
+    expr_const.value().type() ==
+      to_byte_update_expr(expr_const.op()).value().type())
   {
-    expr.op()=expr.op().op0();
+    expr.set_op(expr_const.op().op0());
     return false;
   }
 
-  const exprt &root=expr.op();
-  const exprt &offset=expr.offset();
-  const exprt &value=expr.value();
+  const exprt &root = expr_const.op();
+  const exprt &offset = expr_const.offset();
+  const exprt &value = expr_const.value();
   const auto val_size = pointer_offset_bits(value.type(), ns);
   const auto root_size = pointer_offset_bits(root.type(), ns);
 
@@ -2140,8 +2142,8 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
             plus_exprt new_offset(offset, compo_offset);
             simplify_node(new_offset);
             exprt new_value(with.new_value());
-            expr.offset().swap(new_offset);
-            expr.value().swap(new_value);
+            expr.set_offset(std::move(new_offset));
+            expr.set_value(std::move(new_value));
             simplify_byte_update(expr); // do this recursively
             return false;
           }
@@ -2167,8 +2169,8 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
           plus_exprt new_offset(offset, index_offset);
           simplify_node(new_offset);
           exprt new_value(with.new_value());
-          expr.offset().swap(new_offset);
-          expr.value().swap(new_value);
+          expr.set_offset(std::move(new_offset));
+          expr.set_value(std::move(new_value));
           simplify_byte_update(expr); // do this recursively
           return false;
         }
@@ -2235,7 +2237,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
       }
 
       if(result_expr.is_nil())
-        result_expr=expr.op();
+        result_expr = as_const(expr).op();
 
       exprt member_name(ID_member_name);
       member_name.set(ID_component_name, component.get_name());