Restrict with_exprt to exactly three operands

We cannot build a C++ API for the previous >= 3, odd-number operand
variant. Alas, we ended up with various places in the code base silently
ignoring additional operands, which led to wrong verification results in
Kani as recent changes in CBMC made increasing use of the value set
(which is one of the places that silently ignored additional operands).

Resolves: #7272

Author: tautschnig

src/goto-programs/graphml_witness.cpp

@@ -170,26 +170,24 @@ std::string graphml_witnesst::convert_assign_rec(
   else if(assign.rhs().id() == ID_with)
   {
     const with_exprt &with_expr = to_with_expr(assign.rhs());
-    const auto &ops = with_expr.operands();
 
-    for(std::size_t i = 1; i < ops.size(); i += 2)
-    {
-      if(!result.empty())
-        result += ' ';
+    if(!result.empty())
+      result += ' ';
 
-      if(ops[i].id() == ID_member_name)
-      {
-        const member_exprt member{
-          assign.lhs(), ops[i].get(ID_component_name), ops[i + 1].type()};
-        result +=
-          convert_assign_rec(identifier, code_assignt(member, ops[i + 1]));
-      }
-      else
-      {
-        const index_exprt index{assign.lhs(), ops[i]};
-        result +=
-          convert_assign_rec(identifier, code_assignt(index, ops[i + 1]));
-      }
+    if(with_expr.where().id() == ID_member_name)
+    {
+      const member_exprt member{
+        assign.lhs(),
+        with_expr.where().get(ID_component_name),
+        with_expr.new_value().type()};
+      result += convert_assign_rec(
+        identifier, code_assignt(member, with_expr.new_value()));
+    }
+    else
+    {
+      const index_exprt index{assign.lhs(), with_expr.where()};
+      result += convert_assign_rec(
+        identifier, code_assignt(index, with_expr.new_value()));
     }
   }
   else

src/solvers/flattening/arrays.cpp

@@ -145,11 +145,8 @@ void arrayst::collect_arrays(const exprt &a)
     collect_arrays(with_expr.old());
 
     // make sure this shows as an application
-    for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
-    {
-      index_exprt index_expr(with_expr.old(), with_expr.operands()[i]);
-      record_array_index(index_expr);
-    }
+    index_exprt index_expr(with_expr.old(), with_expr.where());
+    record_array_index(index_expr);
   }
   else if(a.id()==ID_update)
   {
@@ -574,31 +571,24 @@ void arrayst::add_array_constraints_with(
   const index_sett &index_set,
   const with_exprt &expr)
 {
-  // We got x=(y with [i:=v, j:=w, ...]).
-  // First add constraints x[i]=v, x[j]=w, ...
+  // We got x=(y with [i:=v]).
+  // First add constraint x[i]=v
   std::unordered_set<exprt, irep_hash> updated_indices;
 
-  const exprt::operandst &operands = expr.operands();
-  for(std::size_t i = 1; i + 1 < operands.size(); i += 2)
-  {
-    const exprt &index = operands[i];
-    const exprt &value = operands[i + 1];
-
-    index_exprt index_expr(
-      expr, index, to_array_type(expr.type()).element_type());
+  index_exprt index_expr(
+    expr, expr.where(), to_array_type(expr.type()).element_type());
 
-    DATA_INVARIANT_WITH_DIAGNOSTICS(
-      index_expr.type() == value.type(),
-      "with-expression operand should match array element type",
-      irep_pretty_diagnosticst{expr});
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    index_expr.type() == expr.new_value().type(),
+    "with-expression operand should match array element type",
+    irep_pretty_diagnosticst{expr});
 
-    lazy_constraintt lazy(
-      lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value));
-    add_array_constraint(lazy, false); // added immediately
-    array_constraint_count[constraint_typet::ARRAY_WITH]++;
+  lazy_constraintt lazy(
+    lazy_typet::ARRAY_WITH, equal_exprt(index_expr, expr.new_value()));
+  add_array_constraint(lazy, false); // added immediately
+  array_constraint_count[constraint_typet::ARRAY_WITH]++;
 
-    updated_indices.insert(index);
-  }
+  updated_indices.insert(expr.where());
 
   // For all other indices use the existing value, i.e., add constraints
   // x[I]=y[I] for I!=i,j,...

src/solvers/flattening/boolbv_with.cpp

@@ -16,28 +16,16 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_with(const with_exprt &expr)
 {
+  DATA_INVARIANT(
+    expr.operands().size() == 3,
+    "with_exprt with more than 3 operands should no longer exist");
+
   auto &type = expr.type();
 
   if(
     type.id() == ID_bv || type.id() == ID_unsignedbv ||
     type.id() == ID_signedbv)
   {
-    if(expr.operands().size() > 3)
-    {
-      std::size_t s = expr.operands().size();
-
-      // strip off the trailing two operands
-      with_exprt tmp = expr;
-      tmp.operands().resize(s - 2);
-
-      with_exprt new_with_expr(
-        tmp, expr.operands()[s - 2], expr.operands().back());
-
-      // recursive call
-      return convert_with(new_with_expr);
-    }
-
-    PRECONDITION(expr.operands().size() == 3);
     if(expr.new_value().type().id() == ID_bool)
     {
       return convert_bv(
@@ -50,7 +38,7 @@ bvt boolbvt::convert_with(const with_exprt &expr)
     }
   }
 
-  bvt bv = convert_bv(expr.old());
+  bvt bv_old = convert_bv(expr.old());
 
   std::size_t width = boolbv_width(type);
 
@@ -61,21 +49,14 @@ bvt boolbvt::convert_with(const with_exprt &expr)
   }
 
   DATA_INVARIANT_WITH_DIAGNOSTICS(
-    bv.size() == width,
+    bv_old.size() == width,
     "unexpected operand 0 width",
     irep_pretty_diagnosticst{expr});
 
-  bvt prev_bv;
-  prev_bv.resize(width);
-
-  const exprt::operandst &ops=expr.operands();
+  bvt bv;
+  bv.resize(width);
 
-  for(std::size_t op_no=1; op_no<ops.size(); op_no+=2)
-  {
-    bv.swap(prev_bv);
-
-    convert_with(expr.old().type(), ops[op_no], ops[op_no + 1], prev_bv, bv);
-  }
+  convert_with(expr.old().type(), expr.where(), expr.new_value(), bv_old, bv);
 
   return bv;
 }

src/solvers/smt2/smt2_conv.cpp

@@ -4308,27 +4308,9 @@ void smt2_convt::convert_floatbv_rem(const binary_exprt &expr)
 
 void smt2_convt::convert_with(const with_exprt &expr)
 {
-  // get rid of "with" that has more than three operands
-
-  if(expr.operands().size()>3)
-  {
-    std::size_t s=expr.operands().size();
-
-    // strip off the trailing two operands
-    with_exprt tmp = expr;
-    tmp.operands().resize(s-2);
-
-    with_exprt new_with_expr(
-      tmp, expr.operands()[s - 2], expr.operands().back());
-
-    // recursive call
-    return convert_with(new_with_expr);
-  }
-
   INVARIANT(
     expr.operands().size() == 3,
-    "with expression should have been converted to a version with three "
-    "operands above");
+    "with expression should have exactly three operands");
 
   const typet &expr_type = expr.type();
 

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1005,12 +1005,9 @@ static smt_termt convert_array_update_to_smt(
   const sub_expression_mapt &converted)
 {
   smt_termt array = converted.at(with.old());
-  for(auto it = ++with.operands().begin(); it != with.operands().end(); it += 2)
-  {
-    const smt_termt &index_term = converted.at(it[0]);
-    const smt_termt &value_term = converted.at(it[1]);
-    array = smt_array_theoryt::store(array, index_term, value_term);
-  }
+  const smt_termt &index_term = converted.at(with.where());
+  const smt_termt &value_term = converted.at(with.new_value());
+  array = smt_array_theoryt::store(array, index_term, value_term);
   return array;
 }
 

src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -71,52 +71,25 @@ typet struct_encodingt::encode(typet type) const
   return type;
 }
 
-/// \brief Extracts the component/field names and new values from a `with_exprt`
-///        which expresses a new struct value where one or more members of a
-///        struct have had their values substituted with new values.
-/// \note  This is implemented using direct access to the operands and other
-///        underlying irept interfaces, because the interface for `with_exprt`
-///        only supports a single `where` / `new_value` pair and does not
-///        support extracting the name from the `where` operand.
-static std::unordered_map<irep_idt, exprt>
-extricate_updates(const with_exprt &struct_expr)
-{
-  std::unordered_map<irep_idt, exprt> pairs;
-  auto current_operand = struct_expr.operands().begin();
-  // Skip the struct being updated in order to begin with the pairs.
-  current_operand++;
-  while(current_operand != struct_expr.operands().end())
-  {
-    INVARIANT(
-      current_operand->id() == ID_member_name,
-      "operand is expected to be the name of a member");
-    auto name = current_operand->find(ID_component_name).id();
-    ++current_operand;
-    INVARIANT(
-      current_operand != struct_expr.operands().end(),
-      "every name is expected to be followed by a paired value");
-    pairs[name] = *current_operand;
-    ++current_operand;
-  }
-  POSTCONDITION(!pairs.empty());
-  return pairs;
-}
-
 static exprt encode(const with_exprt &with, const namespacet &ns)
 {
   const auto tag_type = type_checked_cast<struct_tag_typet>(with.type());
   const auto struct_type = ns.follow_tag(tag_type);
-  const auto updates = extricate_updates(with);
+  INVARIANT(
+    with.where().id() == ID_member_name,
+    "operand is expected to be the name of a member");
+  const auto update_name = with.where().find(ID_component_name).id();
   const auto components =
     make_range(struct_type.components())
-      .map([&](const struct_union_typet::componentt &component) -> exprt {
-        const auto &update = updates.find(component.get_name());
-        if(update != updates.end())
-          return update->second;
-        else
-          return member_exprt{
-            with.old(), component.get_name(), component.type()};
-      })
+      .map(
+        [&](const struct_union_typet::componentt &component) -> exprt
+        {
+          if(component.get_name() == update_name)
+            return with.new_value();
+          else
+            return member_exprt{
+              with.old(), component.get_name(), component.type()};
+        })
       .collect<exprt::operandst>();
   return struct_exprt{components, tag_type};
 }

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -334,16 +334,14 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
 void smt2_incremental_decision_proceduret::define_index_identifiers(
   const exprt &expr)
 {
-  expr.visit_pre([&](const exprt &expr_node) {
-    if(!can_cast_type<array_typet>(expr_node.type()))
-      return;
-    if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
+  expr.visit_post(
+    [&](const exprt &expr_node)
     {
-      for(auto operand_ite = ++with_expr->operands().begin();
-          operand_ite != with_expr->operands().end();
-          operand_ite += 2)
+      if(!can_cast_type<array_typet>(expr_node.type()))
+        return;
+      if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
       {
-        const auto index_expr = *operand_ite;
+        const auto index_expr = with_expr->where();
         const auto index_term = convert_expr_to_smt(index_expr);
         const auto index_identifier =
           "index_" + std::to_string(index_sequence());
@@ -356,8 +354,7 @@ void smt2_incremental_decision_proceduret::define_index_identifiers(
         solver_process->send(
           smt_define_function_commandt{index_identifier, {}, index_term});
       }
-    }
-  });
+    });
 }
 
 exprt smt2_incremental_decision_proceduret::substitute_defined_padding(

src/util/lower_byte_operators.cpp

@@ -1607,10 +1607,7 @@ static exprt lower_byte_update_byte_array_vector(
         index_exprt{src.op(), where}};
     }
 
-    if(result.id() != ID_with)
-      result = with_exprt{result, std::move(where), std::move(update_value)};
-    else
-      result.add_to_operands(std::move(where), std::move(update_value));
+    result = with_exprt{result, std::move(where), std::move(update_value)};
   }
 
   return simplify_expr(std::move(result), ns);
@@ -1892,7 +1889,7 @@ static exprt lower_byte_update_array_vector_non_const(
         src.get_bits_per_byte()},
       ns);
 
-    result.add_to_operands(std::move(where), std::move(element));
+    result = with_exprt{result, std::move(where), std::move(element)};
   };
 
   std::size_t i = 1;