Specify source location for nondet expressions

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -253,7 +253,7 @@ static void instrument_synchronized_code(
   catch_block.add(monitorexit);
 
   // Re-throw exception
-  side_effect_expr_throwt throw_expr;
+  side_effect_expr_throwt throw_expr(irept(), typet(), code.source_location());
   throw_expr.copy_to_operands(catch_var);
   catch_block.add(code_expressiont(throw_expr));
 

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -813,8 +813,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     clone_body.move_to_operands(declare_cloned);
 
     side_effect_exprt java_new_array(
-      ID_java_new_array,
-      java_reference_type(symbol_type));
+      ID_java_new_array, java_reference_type(symbol_type), source_locationt());
     dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
     dereference_exprt new_array(local_symexpr, symbol_type);
     member_exprt old_length(
@@ -860,7 +859,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     copy_loop.cond()=
       binary_relation_exprt(index_symexpr, ID_lt, old_length);
 
-    side_effect_exprt inc(ID_assign);
+    side_effect_exprt inc(ID_assign, typet(), source_locationt());
     inc.operands().resize(2);
     inc.op0()=index_symexpr;
     inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type()));

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2328,8 +2328,7 @@ void java_bytecode_convert_methodt::convert_athrow(
   }
   else
   {
-    side_effect_expr_throwt throw_expr;
-    throw_expr.add_source_location() = location;
+    side_effect_expr_throwt throw_expr(irept(), typet(), location);
     throw_expr.copy_to_operands(op[0]);
     c = code_expressiont(throw_expr);
   }
@@ -2454,14 +2453,11 @@ void java_bytecode_convert_methodt::convert_multianewarray(
   codet &c,
   exprt::operandst &results)
 {
+  PRECONDITION(!location.get_line().empty());
   const reference_typet ref_type = java_reference_type(arg0.type());
-
-  side_effect_exprt java_new_array(ID_java_new_array, ref_type);
+  side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
   java_new_array.operands() = op;
 
-  if(!location.get_line().empty())
-    java_new_array.add_source_location() = location;
-
   code_blockt create;
 
   if(max_array_length != 0)
@@ -2516,12 +2512,9 @@ void java_bytecode_convert_methodt::convert_newarray(
 
   const reference_typet ref_type = java_array_type(element_type);
 
-  side_effect_exprt java_new_array(ID_java_new_array, ref_type);
+  side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
   java_new_array.copy_to_operands(op[0]);
 
-  if(!location.get_line().empty())
-    java_new_array.add_source_location() = location;
-
   c = code_blockt();
 
   if(max_array_length != 0)
@@ -2543,7 +2536,7 @@ void java_bytecode_convert_methodt::convert_new(
   exprt::operandst &results)
 {
   const reference_typet ref_type = java_reference_type(arg0.type());
-  side_effect_exprt java_new_expr(ID_java_new, ref_type);
+  side_effect_exprt java_new_expr(ID_java_new, ref_type, location);
 
   if(!location.get_line().empty())
     java_new_expr.add_source_location() = location;

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -122,10 +122,10 @@ codet java_bytecode_instrumentt::throw_exception(
       ID_java,
       symbol_table);
 
-  side_effect_exprt new_instance(ID_java_new, exc_ptr_type);
+  side_effect_exprt new_instance(ID_java_new, exc_ptr_type, original_loc);
   code_assignt assign_new(new_symbol.symbol_expr(), new_instance);
 
-  side_effect_expr_throwt throw_expr;
+  side_effect_expr_throwt throw_expr(irept(), typet(), original_loc);
   throw_expr.copy_to_operands(new_symbol.symbol_expr());
 
   code_blockt throw_code;

jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -160,6 +160,6 @@ void java_bytecode_typecheckt::typecheck_expr_member(member_exprt &expr)
             << component_name << "` in class hierarchy" << eom;
 
   // We replace by a non-det of same type
-  side_effect_expr_nondett nondet(expr.type());
+  side_effect_expr_nondett nondet(expr.type(), expr.source_location());
   expr.swap(nondet);
 }

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -162,7 +162,7 @@ static void java_static_lifetime_init(
         // Call the literal initializer method instead of a nondet initializer:
 
         // For arguments we can't parse yet:
-        side_effect_expr_nondett nondet_bool(java_boolean_type());
+        side_effect_expr_nondett nondet_bool(java_boolean_type(), sym.location);
 
         // Argument order is: name, isAnnotation, isArray, isInterface,
         // isSynthetic, isLocalClass, isMemberClass, isEnum

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -173,7 +173,8 @@ exprt allocate_dynamic_object(
   {
     INVARIANT(!object_size.is_nil(), "Size of Java objects should be known");
     // malloc expression
-    side_effect_exprt malloc_expr(ID_allocate, pointer_type(allocate_type));
+    side_effect_exprt malloc_expr(
+      ID_allocate, pointer_type(allocate_type), loc);
     malloc_expr.copy_to_operands(object_size);
     malloc_expr.copy_to_operands(false_exprt());
     // create a symbol for the malloc expression so we can initialize
@@ -503,7 +504,7 @@ static mp_integer max_value(const typet &type)
 /// \return code allocation object and assigning `lhs`
 static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
 {
-  side_effect_exprt alloc(ID_allocate, lhs.type());
+  side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location());
   alloc.copy_to_operands(size);
   alloc.copy_to_operands(false_exprt());
   return code_assignt(lhs, alloc);
@@ -599,7 +600,7 @@ bool initialize_nondet_string_fields(
     ID_java,
     symbol_table);
   const symbol_exprt length_expr = length_sym.symbol_expr();
-  const side_effect_expr_nondett nondet_length(length_expr.type());
+  const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
   code.add(code_declt(length_expr));
   code.add(code_assignt(length_expr, nondet_length));
 
@@ -828,7 +829,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
     //             tmp$<temporary_counter>>
     // }
     code_ifthenelset null_check;
-    null_check.cond()=side_effect_expr_nondett(bool_typet());
+    null_check.cond() =
+      side_effect_expr_nondett(bool_typet(), expr.source_location());
     null_check.then_case()=set_null_inst;
     null_check.else_case()=non_null_inst;
 
@@ -847,7 +849,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
       "No-update and must-update should have already been resolved");
 
     code_ifthenelset update_check;
-    update_check.cond()=side_effect_expr_nondett(bool_typet());
+    update_check.cond() =
+      side_effect_expr_nondett(bool_typet(), expr.source_location());
     update_check.then_case()=update_in_place_assignments;
     update_check.else_case()=new_object_assignments;
 
@@ -1182,9 +1185,8 @@ void java_object_factoryt::gen_nondet_init(
   {
     // types different from pointer or structure:
     // bool, int, float, byte, char, ...
-    exprt rhs=type.id()==ID_c_bool?
-      get_nondet_bool(type):
-      side_effect_expr_nondett(type);
+    exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type)
+                                       : side_effect_expr_nondett(type, loc);
     code_assignt assign(expr, rhs);
     assign.add_source_location()=loc;
 
@@ -1244,7 +1246,7 @@ void java_object_factoryt::allocate_nondet_length_array(
   assignments.move_to_operands(assume_inst1);
   assignments.move_to_operands(assume_inst2);
 
-  side_effect_exprt java_new_array(ID_java_new_array, lhs.type());
+  side_effect_exprt java_new_array(ID_java_new_array, lhs.type(), loc);
   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);

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -788,11 +788,13 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body(
         ? object_factory_parameters.max_nonnull_tree_depth + 1
         : object_factory_parameters.max_nonnull_tree_depth;
 
+    source_locationt location;
+    location.set_function(function_id);
     gen_nondet_init(
       new_global_symbol,
       static_init_body,
       symbol_table,
-      source_locationt(),
+      location,
       false,
       allocation_typet::DYNAMIC,
       parameters,

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -547,7 +547,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   /// \todo refactor with initialize_nonddet_string_struct
   const refined_string_exprt str = decl_string_expr(loc, symbol_table, code);
 
-  side_effect_expr_nondett nondet_length(str.length().type());
+  const side_effect_expr_nondett nondet_length(str.length().type(), loc);
   code.add(code_assignt(str.length(), nondet_length), loc);
 
   exprt nondet_array_expr =
@@ -667,7 +667,7 @@ exprt make_nondet_infinite_char_array(
     symbol_table);
   const symbol_exprt data_expr = data_sym.symbol_expr();
   code.add(code_declt(data_expr), loc);
-  side_effect_expr_nondett nondet_data(data_expr.type());
+  const side_effect_expr_nondett nondet_data(data_expr.type(), loc);
   code.add(code_assignt(data_expr, nondet_data), loc);
   return data_expr;
 }

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -84,7 +84,7 @@ goto_programt::targett remove_java_newt::lower_java_new(
   CHECK_RETURN(object_size.is_not_nil());
 
   // we produce a malloc side-effect, which stays
-  side_effect_exprt malloc_expr(ID_allocate, rhs.type());
+  side_effect_exprt malloc_expr(ID_allocate, rhs.type(), location);
   malloc_expr.copy_to_operands(object_size);
   // could use true and get rid of the code below
   malloc_expr.copy_to_operands(false_exprt());
@@ -135,7 +135,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   CHECK_RETURN(!object_size.is_nil());
 
   // we produce a malloc side-effect, which stays
-  side_effect_exprt malloc_expr(ID_allocate, rhs.type());
+  side_effect_exprt malloc_expr(ID_allocate, rhs.type(), location);
   malloc_expr.copy_to_operands(object_size);
   // code use true and get rid of the code below
   malloc_expr.copy_to_operands(false_exprt());
@@ -188,7 +188,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     allocate_data_type = data.type();
 
   side_effect_exprt data_java_new_expr(
-    ID_java_new_array_data, allocate_data_type);
+    ID_java_new_array_data, allocate_data_type, location);
 
   // The instruction may specify a (hopefully small) upper bound on the
   // array size, in which case we allocate a fixed-length array that may
@@ -276,7 +276,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     CHECK_RETURN(sub_type.id() == ID_pointer);
     sub_java_new.type() = sub_type;
 
-    side_effect_exprt inc(ID_assign);
+    side_effect_exprt inc(ID_assign, typet(), location);
     inc.operands().resize(2);
     inc.op0() = tmp_i;
     inc.op1() = plus_exprt(tmp_i, from_integer(1, tmp_i.type()));