Merge pull request #6389 from diffblue/code_frontend_assign

introduce code_frontend_assignt

Author: tautschnig

jbmc/src/java_bytecode/code_with_references.cpp

@@ -23,7 +23,7 @@ codet allocate_array(
   pointer_type.subtype().set(ID_element_type, element_type);
   side_effect_exprt java_new_array{
     ID_java_new_array, {array_length_expr}, pointer_type, loc};
-  return code_assignt{expr, java_new_array, loc};
+  return code_frontend_assignt{expr, java_new_array, loc};
 }
 
 code_blockt
@@ -41,8 +41,8 @@ reference_allocationt::to_code(reference_substitutiont &references) const
   // or the "@id" json field corresponding to `reference_id` doesn't appear in
   // the file.
   code_blockt code;
-  code.add(code_assignt{*reference.array_length,
-                        side_effect_expr_nondett{java_int_type(), loc}});
+  code.add(code_frontend_assignt{
+    *reference.array_length, side_effect_expr_nondett{java_int_type(), loc}});
   code.add(code_assumet{binary_predicate_exprt{
     *reference.array_length, ID_ge, from_integer(0, java_int_type())}});
   code.add(allocate_array(reference.expr, *reference.array_length, loc));

jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp

@@ -14,9 +14,9 @@ Author: Diffblue Ltd.
 #include <java_bytecode/java_types.h>
 
 #include <util/fresh_symbol.h>
-#include <util/goto_instruction_code.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
+#include <util/std_code.h>
 #include <util/symbol_table_base.h>
 
 /// Returns the symbol name for `org.cprover.CProver.createArrayWithType`
@@ -81,7 +81,7 @@ codet create_array_with_type_body(
   side_effect_exprt new_array_expr{
     ID_java_new_array, new_array_symbol.type, source_locationt{}};
   new_array_expr.copy_to_operands(length_argument_symbol_expr);
-  code_block.add(code_assignt(new_array_symbol_expr, new_array_expr));
+  code_block.add(code_frontend_assignt(new_array_symbol_expr, new_array_expr));
 
   dereference_exprt existing_array(existing_array_argument_symbol_expr);
   dereference_exprt new_array(new_array_symbol_expr);
@@ -99,9 +99,10 @@ codet create_array_with_type_body(
   member_exprt new_array_element_classid(
     new_array, JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME, string_typet());
 
-  code_block.add(code_assignt(new_array_dimension, old_array_dimension));
   code_block.add(
-    code_assignt(new_array_element_classid, old_array_element_classid));
+    code_frontend_assignt(new_array_dimension, old_array_dimension));
+  code_block.add(code_frontend_assignt(
+    new_array_element_classid, old_array_element_classid));
 
   // return new_array
   code_block.add(code_returnt(new_array_symbol_expr));

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -909,7 +909,7 @@ void add_java_array_types(symbol_tablet &symbol_table)
     member_exprt old_length(
       old_array, length_component.get_name(), length_component.type());
     java_new_array.copy_to_operands(old_length);
-    code_assignt create_blank(local_symexpr, java_new_array);
+    code_frontend_assignt create_blank(local_symexpr, java_new_array);
 
     codet copy_type_information = code_skipt();
     if(l == 'a')
@@ -930,8 +930,9 @@ void add_java_array_types(symbol_tablet &symbol_table)
         new_array, array_element_classid_component);
 
       copy_type_information = code_blockt{
-        {code_assignt(new_array_dimension, old_array_dimension),
-         code_assignt(new_array_element_classid, old_array_element_classid)}};
+        {code_frontend_assignt(new_array_dimension, old_array_dimension),
+         code_frontend_assignt(
+           new_array_element_classid, old_array_element_classid)}};
     }
 
     member_exprt old_data(
@@ -971,7 +972,7 @@ void add_java_array_types(symbol_tablet &symbol_table)
       from_integer(0, index_symexpr.type()),
       old_length,
       index_symexpr,
-      code_assignt(std::move(new_cell), std::move(old_cell)),
+      code_frontend_assignt(std::move(new_cell), std::move(old_cell)),
       location);
 
     member_exprt new_base_class(

jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp

@@ -19,7 +19,7 @@ void java_bytecode_typecheckt::typecheck_code(codet &code)
 
   if(statement==ID_assign)
   {
-    code_assignt &code_assign=to_code_assign(code);
+    code_frontend_assignt &code_assign = to_code_frontend_assign(code);
     typecheck_expr(code_assign.lhs());
     typecheck_expr(code_assign.rhs());
 

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -122,8 +122,8 @@ void java_static_lifetime_init(
 
   const symbol_exprt rounding_mode =
     symbol_table.lookup_ref(rounding_mode_identifier()).symbol_expr();
-  code_block.add(
-    code_assignt{rounding_mode, from_integer(0, rounding_mode.type())});
+  code_block.add(code_frontend_assignt{rounding_mode,
+                                       from_integer(0, rounding_mode.type())});
 
   object_factory_parameters.function_id = initialize_symbol.name;
 
@@ -226,7 +226,7 @@ void java_static_lifetime_init(
           to_struct_expr(*zero_object), ns, to_struct_tag_type(sym.type));
 
         code_block.add(
-          std::move(code_assignt(sym.symbol_expr(), *zero_object)));
+          std::move(code_frontend_assignt(sym.symbol_expr(), *zero_object)));
 
         // Then call the init function:
         code_block.add(std::move(initializer_call));
@@ -257,7 +257,7 @@ void java_static_lifetime_init(
       }
       else if(sym.value.is_not_nil())
       {
-        code_assignt assignment(sym.symbol_expr(), sym.value);
+        code_frontend_assignt assignment(sym.symbol_expr(), sym.value);
         assignment.add_source_location()=source_location;
         code_block.add(assignment);
       }
@@ -333,7 +333,7 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
                                     .symbol_expr();
       main_arguments[param_number] = result;
       init_code.add(code_declt{result});
-      init_code.add(code_assignt{
+      init_code.add(code_frontend_assignt{
         result,
         side_effect_exprt{ID_java_new, {}, p.type(), function.location}});
       continue;
@@ -417,10 +417,9 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
           function.location,
           pointer_type_selector,
           message_handler);
-        init_code_for_type.add(
-          code_assignt(
-            result_symbol.symbol_expr(),
-            typecast_exprt(init_expr_for_parameter, p.type())));
+        init_code_for_type.add(code_frontend_assignt(
+          result_symbol.symbol_expr(),
+          typecast_exprt(init_expr_for_parameter, p.type())));
         cases.push_back(init_code_for_type);
       }
 
@@ -672,7 +671,7 @@ bool generate_java_start_function(
   symbol_table.add(exc_symbol);
 
   // Zero-initialise the top-level exception catch variable:
-  init_code.add(code_assignt(
+  init_code.add(code_frontend_assignt(
     exc_symbol.symbol_expr(),
     null_pointer_exprt(to_pointer_type(exc_symbol.type))));
 

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -399,7 +399,7 @@ void initialize_nondet_string_fields(
     allocate_objects.allocate_automatic_local_object(
       java_int_type(), "tmp_object_factory");
   const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
-  code.add(code_assignt(length_expr, nondet_length));
+  code.add(code_frontend_assignt(length_expr, nondet_length));
 
   // assume (length_expr >= min_nondet_string_length);
   const exprt min_length =
@@ -508,8 +508,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
     // Having created a pointer to object of type replacement_pointer_type
     // we now assign it back to the original pointer with a cast
     // from pointer_type to replacement_pointer_type
-    assignments.add(
-      code_assignt(expr, typecast_exprt(real_pointer_symbol, pointer_type)));
+    assignments.add(code_frontend_assignt(
+      expr, typecast_exprt(real_pointer_symbol, pointer_type)));
     return;
   }
 
@@ -539,8 +539,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
   {
     if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
     {
-      assignments.add(
-        code_assignt{expr, null_pointer_exprt{pointer_type}, location});
+      assignments.add(code_frontend_assignt{
+        expr, null_pointer_exprt{pointer_type}, location});
     }
     // Otherwise leave it as it is.
     return;
@@ -615,7 +615,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
     update_in_placet::NO_UPDATE_IN_PLACE,
     location);
 
-  const code_assignt set_null_inst{
+  const code_frontend_assignt set_null_inst{
     expr, null_pointer_exprt{pointer_type}, location};
 
   const bool allow_null = depth > object_factory_parameters.min_null_tree_depth;
@@ -734,7 +734,7 @@ alternate_casest get_string_input_values_code(
   {
     const symbol_exprt s =
       get_or_create_string_literal_symbol(val, symbol_table, true);
-    cases.push_back(code_assignt(expr, s));
+    cases.push_back(code_frontend_assignt(expr, s));
   }
   return cases;
 }
@@ -843,7 +843,7 @@ void java_object_factoryt::gen_nondet_struct_init(
         allocate_objects);
     }
 
-    assignments.add(code_assignt(expr, *initial_object));
+    assignments.add(code_frontend_assignt(expr, *initial_object));
   }
 
   for(const auto &component : components)
@@ -865,7 +865,7 @@ void java_object_factoryt::gen_nondet_struct_init(
       // which is necessary to support concurrency.
       if(update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE)
         continue;
-      code_assignt code(me, from_integer(0, me.type()));
+      code_frontend_assignt code(me, from_integer(0, me.type()));
       code.add_source_location() = location;
       assignments.add(code);
     }
@@ -950,7 +950,7 @@ static code_blockt assume_expr_integral(
     allocate_local_symbol(java_int_type(), "assume_integral_tmp");
   assignments.add(code_declt(aux_int), location);
   exprt nondet_rhs = side_effect_expr_nondett(java_int_type(), location);
-  code_assignt aux_assign(aux_int, nondet_rhs);
+  code_frontend_assignt aux_assign(aux_int, nondet_rhs);
   aux_assign.add_source_location() = location;
   assignments.add(aux_assign);
   assignments.add(
@@ -1068,7 +1068,7 @@ void java_object_factoryt::gen_nondet_init(
     exprt rhs = type.id() == ID_c_bool
                   ? get_nondet_bool(type, location)
                   : side_effect_expr_nondett(type, location);
-    code_assignt assign(expr, rhs);
+    code_frontend_assignt assign(expr, rhs);
     assign.add_source_location() = location;
 
     assignments.add(assign);
@@ -1084,7 +1084,7 @@ void java_object_factoryt::gen_nondet_init(
       if(auto singleton = interval.as_singleton())
       {
         assignments.add(
-          code_assignt{expr, from_integer(*singleton, expr.type())});
+          code_frontend_assignt{expr, from_integer(*singleton, expr.type())});
       }
       else
       {
@@ -1158,7 +1158,7 @@ static void allocate_nondet_length_array(
   java_new_array.copy_to_operands(length_sym_expr);
   java_new_array.set(ID_length_upper_bound, max_length_expr);
   java_new_array.type().subtype().set(ID_element_type, element_type);
-  code_assignt assign(lhs, java_new_array);
+  code_frontend_assignt assign(lhs, java_new_array);
   assign.add_source_location() = location;
   assignments.add(assign);
 }
@@ -1204,13 +1204,15 @@ static void array_primitive_init_code(
   // *array_data_init = NONDET(TYPE [max_length_expr]);
   side_effect_expr_nondett nondet_data(array_type, location);
   const dereference_exprt data_pointer_deref{tmp_finite_array_pointer};
-  assignments.add(code_assignt(data_pointer_deref, std::move(nondet_data)));
+  assignments.add(
+    code_frontend_assignt(data_pointer_deref, std::move(nondet_data)));
   assignments.statements().back().add_source_location() = location;
 
   // init_array_expr = *array_data_init;
   address_of_exprt tmp_nondet_pointer(
     index_exprt(data_pointer_deref, from_integer(0, java_int_type())));
-  assignments.add(code_assignt(init_array_expr, std::move(tmp_nondet_pointer)));
+  assignments.add(
+    code_frontend_assignt(init_array_expr, std::move(tmp_nondet_pointer)));
   assignments.statements().back().add_source_location() = location;
 }
 
@@ -1251,7 +1253,7 @@ code_blockt java_object_factoryt::assign_element(
     // If we're updating an existing array item, read the existing object that
     // we (may) alter:
     if(update_in_place != update_in_placet::NO_UPDATE_IN_PLACE)
-      assignments.add(code_assignt(init_expr, element));
+      assignments.add(code_frontend_assignt(init_expr, element));
   }
 
   // MUST_UPDATE_IN_PLACE only applies to this object.
@@ -1277,7 +1279,7 @@ code_blockt java_object_factoryt::assign_element(
   {
     // We used a temporary variable to update or initialise an array item;
     // now write it into the array:
-    assignments.add(code_assignt(element, init_expr));
+    assignments.add(code_frontend_assignt(element, init_expr));
   }
   return assignments;
 }
@@ -1337,7 +1339,7 @@ static void array_loop_init_code(
   const symbol_exprt &array_init_symexpr =
     allocate_local_symbol(init_array_expr.type(), "array_data_init");
 
-  code_assignt data_assign(array_init_symexpr, init_array_expr);
+  code_frontend_assignt data_assign(array_init_symexpr, init_array_expr);
   data_assign.add_source_location() = location;
   assignments.add(data_assign);
 
@@ -1505,7 +1507,8 @@ bool java_object_factoryt::gen_nondet_enum_init(
 
   const dereference_exprt element_at_index =
     array_element_from_pointer(enum_array_expr, index_expr);
-  code_assignt enum_assign(expr, typecast_exprt(element_at_index, expr.type()));
+  code_frontend_assignt enum_assign(
+    expr, typecast_exprt(element_at_index, expr.type()));
   assignments.add(enum_assign);
 
   return true;
@@ -1520,7 +1523,7 @@ static void assert_type_consistency(const code_blockt &assignments)
   {
     if(code.get_statement() != ID_assign)
       continue;
-    const auto &assignment = to_code_assign(code);
+    const auto &assignment = to_code_frontend_assign(code);
     INVARIANT(
       assignment.lhs().type() == assignment.rhs().type(),
       "object factory should produce type-consistent assignments");

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -179,20 +179,20 @@ static irep_idt clinit_local_init_complete_var_name(const irep_idt &class_name)
   return id2string(class_name) + CPROVER_PREFIX "clinit_wrapper::init_complete";
 }
 
-/// Generates a code_assignt for clinit_statest
+/// Generates a code_frontend_assignt for clinit_statest
 /// /param expr:
 ///   expression to be used as the LHS of generated assignment.
 /// /param state:
 ///   execution state of the clint_wrapper, used as the RHS of the generated
 ///   assignment.
-/// /return returns a code_assignt, assigning \p expr to the integer
+/// /return returns a code_frontend_assignt, assigning \p expr to the integer
 ///   representation of \p state
-static code_assignt
+static code_frontend_assignt
 gen_clinit_assign(const exprt &expr, const clinit_statest state)
 {
   mp_integer initv(static_cast<int>(state));
   constant_exprt init_s = from_integer(initv, clinit_states_type());
-  return code_assignt(expr, init_s);
+  return code_frontend_assignt(expr, init_s);
 }
 
 /// Generates an equal_exprt for clinit_statest
@@ -596,7 +596,7 @@ code_blockt get_thread_safe_clinit_wrapper_body(
 
   // C::__CPROVER_PREFIX_clinit_thread_local_state = INIT_COMPLETE;
   {
-    code_assignt assign = gen_clinit_assign(
+    code_frontend_assignt assign = gen_clinit_assign(
       clinit_thread_local_state_sym.symbol_expr(),
       clinit_statest::INIT_COMPLETE);
     function_body.add(assign);
@@ -629,15 +629,16 @@ code_blockt get_thread_safe_clinit_wrapper_body(
     code_ifthenelset init_conditional(
       gen_clinit_eqexpr(
         clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE),
-      code_blockt({code_assignt(init_complete.symbol_expr(), true_exprt())}));
+      code_blockt(
+        {code_frontend_assignt(init_complete.symbol_expr(), true_exprt())}));
 
     code_ifthenelset not_init_conditional(
       gen_clinit_eqexpr(
         clinit_state_sym.symbol_expr(), clinit_statest::NOT_INIT),
       code_blockt(
         {gen_clinit_assign(
            clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS),
-         code_assignt(init_complete.symbol_expr(), false_exprt())}),
+         code_frontend_assignt(init_complete.symbol_expr(), false_exprt())}),
       std::move(init_conditional));
 
     function_body.add(std::move(not_init_conditional));
@@ -757,7 +758,8 @@ code_ifthenelset get_clinit_wrapper_body(
     false_exprt());
 
   // add the "already-run = false" statement
-  code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
+  code_frontend_assignt set_already_run(
+    already_run_symbol.symbol_expr(), true_exprt());
   code_blockt init_body({set_already_run});
 
   clinit_wrapper_do_recursive_calls(