Merge pull request #8674 from tautschnig/three-operand-with

Restrict with_exprt to exactly three operands

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;