Fix support for with_exprt with more than 3 operands

A `with_exprt` needs to have at least 3 operands, but can encode
multiple updates when using more operands (where any further operands
need to come in pairs of two: an index/member and a new value). We
already support this in several places, but were still missing support
in others. This led to wrong verification results in Kani as recent
changes in CBMC make increasing use of the value set (which is among
those fixed in this commit).

Author: tautschnig

src/goto-programs/interpreter_evaluate.cpp

@@ -948,30 +948,34 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
     const auto &wexpr=to_with_expr(expr);
 
     mp_vectort dest = evaluate(wexpr.old());
-    mp_vectort where = evaluate(wexpr.where());
-    mp_vectort new_value = evaluate(wexpr.new_value());
 
-    const auto &subtype = to_array_type(expr.type()).element_type();
-
-    if(!new_value.empty() && where.size()==1 && !unbounded_size(subtype))
+    for(std::size_t i = 1; i < wexpr.operands().size(); i += 2)
     {
-      // Ignore indices < 0, which the string solver sometimes produces
-      if(where[0]<0)
-        return {};
+      mp_vectort where = evaluate(wexpr.operands()[i]);
+      mp_vectort new_value = evaluate(wexpr.operands()[i + 1]);
+
+      const auto &subtype = to_array_type(expr.type()).element_type();
 
-      mp_integer where_idx=where[0];
-      mp_integer subtype_size=get_size(subtype);
-      mp_integer need_size=(where_idx+1)*subtype_size;
+      if(!new_value.empty() && where.size() == 1 && !unbounded_size(subtype))
+      {
+        // Ignore indices < 0, which the string solver sometimes produces
+        if(where[0] < 0)
+          return {};
 
-      if(dest.size()<need_size)
-        dest.resize(numeric_cast_v<std::size_t>(need_size), 0);
+        mp_integer where_idx = where[0];
+        mp_integer subtype_size = get_size(subtype);
+        mp_integer need_size = (where_idx + 1) * subtype_size;
 
-      for(std::size_t i=0; i<new_value.size(); ++i)
-        dest[numeric_cast_v<std::size_t>((where_idx * subtype_size) + i)] =
-          new_value[i];
+        if(dest.size() < need_size)
+          dest.resize(numeric_cast_v<std::size_t>(need_size), 0);
 
-      return {};
+        for(std::size_t i = 0; i < new_value.size(); ++i)
+          dest[numeric_cast_v<std::size_t>((where_idx * subtype_size) + i)] =
+            new_value[i];
+      }
     }
+
+    return dest;
   }
   else if(expr.id()==ID_nil)
   {

src/pointer-analysis/value_set.cpp

@@ -973,26 +973,38 @@ void value_sett::get_value_set_rec(
       (expr.type().id() == ID_struct_tag || expr.type().id() == ID_struct) &&
       !suffix.empty())
     {
-      irep_idt component_name = with_expr.where().get(ID_component_name);
-      if(suffix_starts_with_field(suffix, id2string(component_name)))
+      bool any_matching_suffix = false;
+      bool all_matching_component_names = true;
+      for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
       {
-        // Looking for the member overwritten by this WITH expression
-        std::string remaining_suffix =
-          strip_first_field_from_suffix(suffix, id2string(component_name));
-        get_value_set_rec(
-          with_expr.new_value(),
-          dest,
-          includes_nondet_pointer,
-          remaining_suffix,
-          original_type,
-          ns);
+        irep_idt component_name =
+          with_expr.operands()[i].get(ID_component_name);
+        if(suffix_starts_with_field(suffix, id2string(component_name)))
+        {
+          // Looking for the member overwritten by this WITH expression
+          any_matching_suffix = true;
+          std::string remaining_suffix =
+            strip_first_field_from_suffix(suffix, id2string(component_name));
+          get_value_set_rec(
+            with_expr.operands()[i + 1],
+            dest,
+            includes_nondet_pointer,
+            remaining_suffix,
+            original_type,
+            ns);
+        }
+        else if(
+          all_matching_component_names &&
+          (expr.type().id() != ID_struct ||
+           !to_struct_type(expr.type()).has_component(component_name)) &&
+          (expr.type().id() != ID_struct_tag ||
+           !ns.follow_tag(to_struct_tag_type(expr.type()))
+              .has_component(component_name)))
+        {
+          all_matching_component_names = false;
+        }
       }
-      else if(
-        (expr.type().id() == ID_struct &&
-         to_struct_type(expr.type()).has_component(component_name)) ||
-        (expr.type().id() == ID_struct_tag &&
-         ns.follow_tag(to_struct_tag_type(expr.type()))
-           .has_component(component_name)))
+      if(!any_matching_suffix && all_matching_component_names)
       {
         // Looking for a non-overwritten member, look through this expression
         get_value_set_rec(
@@ -1003,7 +1015,7 @@ void value_sett::get_value_set_rec(
           original_type,
           ns);
       }
-      else
+      else if(!any_matching_suffix)
       {
         // Member we're looking for is not defined in this struct -- this
         // must be a reinterpret cast of some sort. Default to conservatively
@@ -1015,13 +1027,16 @@ void value_sett::get_value_set_rec(
           suffix,
           original_type,
           ns);
-        get_value_set_rec(
-          with_expr.new_value(),
-          dest,
-          includes_nondet_pointer,
-          "",
-          original_type,
-          ns);
+        for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+        {
+          get_value_set_rec(
+            with_expr.operands()[i + 1],
+            dest,
+            includes_nondet_pointer,
+            "",
+            original_type,
+            ns);
+        }
       }
     }
     else if(expr.type().id() == ID_array && !suffix.empty())
@@ -1040,13 +1055,16 @@ void value_sett::get_value_set_rec(
         suffix,
         original_type,
         ns);
-      get_value_set_rec(
-        with_expr.new_value(),
-        dest,
-        includes_nondet_pointer,
-        new_value_suffix,
-        original_type,
-        ns);
+      for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+      {
+        get_value_set_rec(
+          with_expr.operands()[i + 1],
+          dest,
+          includes_nondet_pointer,
+          new_value_suffix,
+          original_type,
+          ns);
+      }
     }
     else
     {
@@ -1059,13 +1077,16 @@ void value_sett::get_value_set_rec(
         suffix,
         original_type,
         ns);
-      get_value_set_rec(
-        with_expr.new_value(),
-        dest,
-        includes_nondet_pointer,
-        "",
-        original_type,
-        ns);
+      for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+      {
+        get_value_set_rec(
+          with_expr.operands()[i + 1],
+          dest,
+          includes_nondet_pointer,
+          "",
+          original_type,
+          ns);
+      }
     }
   }
   else if(expr.id()==ID_array)
@@ -1624,14 +1645,18 @@ void value_sett::assign(
       }
       else if(rhs.id()==ID_with)
       {
+        const with_exprt &with_expr = to_with_expr(rhs);
         const index_exprt op0_index(
-          to_with_expr(rhs).old(),
+          with_expr.old(),
           exprt(ID_unknown, c_index_type()),
           to_array_type(lhs.type()).element_type());
 
         assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
-        assign(
-          lhs_index, to_with_expr(rhs).new_value(), ns, is_simplified, true);
+        for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+        {
+          assign(
+            lhs_index, with_expr.operands()[i + 1], ns, is_simplified, true);
+        }
       }
       else
       {

src/pointer-analysis/value_set_fi.cpp

@@ -1058,17 +1058,21 @@ void value_set_fit::assign(
         {
           // see if this is the member we want
           const auto &rhs_with = to_with_expr(rhs);
-          const exprt &member_operand = rhs_with.where();
+          bool member_found = false;
+          for(std::size_t i = 1; i < rhs_with.operands().size(); i += 2)
+          {
+            const exprt &member_operand = rhs_with.operands()[i];
 
-          const irep_idt &component_name=
-            member_operand.get(ID_component_name);
+            const irep_idt &component_name =
+              member_operand.get(ID_component_name);
 
-          if(component_name==name)
-          {
-            // yes! just take op2
-            rhs_member = rhs_with.new_value();
+            if(component_name == name)
+            {
+              rhs_member = rhs_with.operands()[i + 1];
+              member_found = true;
+            }
           }
-          else
+          if(!member_found)
           {
             // no! do op0
             rhs_member=exprt(ID_member, subtype);
@@ -1126,13 +1130,17 @@ void value_set_fit::assign(
       }
       else if(rhs.id()==ID_with)
       {
+        const with_exprt &with_expr = to_with_expr(rhs);
         const index_exprt op0_index(
-          to_with_expr(rhs).old(),
+          with_expr.old(),
           exprt(ID_unknown, c_index_type()),
           to_array_type(lhs.type()).element_type());
 
         assign(lhs_index, op0_index, ns);
-        assign(lhs_index, to_with_expr(rhs).new_value(), ns);
+        for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+        {
+          assign(lhs_index, with_expr.operands()[i + 1], ns);
+        }
       }
       else
       {

src/solvers/smt2/smt2_format.cpp

@@ -139,9 +139,14 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
   else if(expr.id() == ID_with && expr.type().id() == ID_array)
   {
     const auto &with_expr = to_with_expr(expr);
-    out << "(store " << smt2_format(with_expr.old()) << ' '
-        << smt2_format(with_expr.where()) << ' '
-        << smt2_format(with_expr.new_value()) << ')';
+    for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+      out << "(store ";
+    out << smt2_format(with_expr.old()) << ' ';
+    for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+    {
+      out << smt2_format(with_expr.operands()[i]) << ' '
+          << smt2_format(with_expr.operands()[i + 1]) << ')';
+    }
   }
   else if(expr.id() == ID_array_list)
   {

src/solvers/strings/string_refinement_util.cpp

@@ -70,9 +70,12 @@ sparse_arrayt::sparse_arrayt(const with_exprt &expr)
   while(can_cast_expr<with_exprt>(ref.get()))
   {
     const auto &with_expr = expr_dynamic_cast<with_exprt>(ref.get());
-    const auto current_index =
-      numeric_cast_v<std::size_t>(to_constant_expr(with_expr.where()));
-    entries[current_index] = with_expr.new_value();
+    for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+    {
+      const auto current_index =
+        numeric_cast_v<std::size_t>(to_constant_expr(with_expr.operands()[i]));
+      entries[current_index] = with_expr.operands()[i + 1];
+    }
     ref = with_expr.old();
   }
 

src/util/simplify_expr.cpp

@@ -2157,7 +2157,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
    *             value)
    */
 
-  if(value.id()==ID_with)
+  if(value.id() == ID_with && value.operands().size() == 3)
   {
     const with_exprt &with=to_with_expr(value);
 
@@ -2297,6 +2297,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
 
         if(
           expr_at_offset_C.id() == ID_with &&
+          expr_at_offset_C.operands().size() == 3 &&
           to_with_expr(expr_at_offset_C).where().is_zero())
         {
           tmp.set_op(to_with_expr(expr_at_offset_C).old());