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()));

jbmc/src/java_bytecode/replace_java_nondet.cpp

@@ -279,7 +279,8 @@ static goto_programt::targett check_and_replace_target(
     const auto &nondet_var =
       to_code_return(target_instruction->code).return_value();
 
-    side_effect_expr_nondett inserted_expr(nondet_var.type());
+    side_effect_expr_nondett inserted_expr(
+      nondet_var.type(), target_instruction->source_location);
     inserted_expr.set_nullable(
       instr_info.get_nullable_type() ==
       nondet_instruction_infot::is_nullablet::TRUE);
@@ -292,7 +293,8 @@ static goto_programt::targett check_and_replace_target(
     // Assume that the LHS of *this* assignment is the actual nondet variable
     const auto &nondet_var = to_code_assign(target_instruction->code).lhs();
 
-    side_effect_expr_nondett inserted_expr(nondet_var.type());
+    side_effect_expr_nondett inserted_expr(
+      nondet_var.type(), target_instruction->source_location);
     inserted_expr.set_nullable(
       instr_info.get_nullable_type() ==
       nondet_instruction_infot::is_nullablet::TRUE);

src/analyses/flow_insensitive_analysis.cpp

@@ -210,7 +210,8 @@ bool flow_insensitive_analysis_baset::do_function_call(
 
     goto_programt temp;
 
-    exprt rhs=side_effect_expr_nondett(code.lhs().type());
+    exprt rhs =
+      side_effect_expr_nondett(code.lhs().type(), l_call->source_location);
 
     goto_programt::targett r=temp.add_instruction();
     r->make_return();

src/analyses/goto_check.cpp

@@ -1703,7 +1703,7 @@ void goto_checkt::goto_check(
           if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
             address_of_expr.make_typecast(lhs.type());
           const if_exprt rhs(
-            side_effect_expr_nondett(bool_typet()),
+            side_effect_expr_nondett(bool_typet(), i.source_location),
             address_of_expr,
             lhs,
             lhs.type());

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -43,11 +43,12 @@ static const symbolt &c_new_tmp_symbol(
 }
 
 /// \param type: Desired type (C_bool or plain bool)
+/// \param loc: source location
 /// \return nondet expr of that type
-static exprt c_get_nondet_bool(const typet &type)
+static exprt c_get_nondet_bool(const typet &type, const source_locationt &loc)
 {
   // We force this to 0 and 1 and won't consider other values
-  return typecast_exprt(side_effect_expr_nondett(bool_typet()), type);
+  return typecast_exprt(side_effect_expr_nondett(bool_typet(), loc), type);
 }
 
 class symbol_factoryt
@@ -173,7 +174,7 @@ void symbol_factoryt::gen_nondet_init(
       set_null_inst.add_source_location()=loc;
 
       code_ifthenelset null_check;
-      null_check.cond()=side_effect_expr_nondett(bool_typet());
+      null_check.cond() = side_effect_expr_nondett(bool_typet(), loc);
       null_check.then_case()=set_null_inst;
       null_check.else_case()=non_null_inst;
 
@@ -187,9 +188,8 @@ void symbol_factoryt::gen_nondet_init(
     //   <expr> = NONDET(_BOOL);
     // Else add the following code to assignments:
     //   <expr> = NONDET(type);
-    exprt rhs=type.id()==ID_c_bool?
-      c_get_nondet_bool(type):
-      side_effect_expr_nondett(type);
+    exprt rhs = type.id() == ID_c_bool ? c_get_nondet_bool(type, loc)
+                                       : side_effect_expr_nondett(type, loc);
     code_assignt assign(expr, rhs);
     assign.add_source_location()=loc;
 

src/ansi-c/c_typecheck_code.cpp

@@ -675,7 +675,8 @@ void c_typecheck_baset::typecheck_return(codet &code)
       warning().source_location = code.source_location();
       warning() << "non-void function should return a value" << eom;
 
-      code.copy_to_operands(side_effect_expr_nondett(return_type));
+      code.copy_to_operands(
+        side_effect_expr_nondett(return_type, code.source_location()));
     }
   }
   else if(code.operands().size()==1)

src/ansi-c/c_typecheck_expr.cpp

@@ -466,9 +466,7 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
 
   // turn into function call
   side_effect_expr_function_callt result(
-    function, {arg}, new_type.return_type());
-
-  result.add_source_location()=expr.source_location();
+    function, {arg}, new_type.return_type(), expr.source_location());
 
   expr.swap(result);
 
@@ -884,8 +882,7 @@ void c_typecheck_baset::typecheck_side_effect_statement_expression(
       static_cast<const typet &>(fc.function().type().find(ID_return_type));
 
     side_effect_expr_function_callt sideeffect(
-      fc.function(), fc.arguments(), return_type);
-    sideeffect.add_source_location()=fc.source_location();
+      fc.function(), fc.arguments(), return_type, fc.source_location());
 
     expr.type()=sideeffect.type();
 
@@ -897,8 +894,8 @@ void c_typecheck_baset::typecheck_side_effect_statement_expression(
     }
     else
     {
-      side_effect_exprt assign(ID_assign, sideeffect.type());
-      assign.add_source_location()=fc.source_location();
+      side_effect_exprt assign(
+        ID_assign, sideeffect.type(), fc.source_location());
       assign.move_to_operands(fc.lhs(), sideeffect);
 
       code_expressiont code_expr(assign);
@@ -965,7 +962,8 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
   // The type may contain side-effects.
   if(!clean_code.empty())
   {
-    side_effect_exprt side_effect_expr(ID_statement_expression, void_type());
+    side_effect_exprt side_effect_expr(
+      ID_statement_expression, void_type(), expr.source_location());
     code_blockt decl_block(clean_code);
     decl_block.set_statement(ID_decl_block);
     side_effect_expr.copy_to_operands(decl_block);
@@ -1021,7 +1019,8 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
   // The type may contain side-effects.
   if(!clean_code.empty())
   {
-    side_effect_exprt side_effect_expr(ID_statement_expression, void_type());
+    side_effect_exprt side_effect_expr(
+      ID_statement_expression, void_type(), expr.source_location());
     code_blockt decl_block(clean_code);
     decl_block.set_statement(ID_decl_block);
     side_effect_expr.copy_to_operands(decl_block);
@@ -2327,8 +2326,7 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    side_effect_exprt malloc_expr(ID_allocate, expr.type());
-    malloc_expr.add_source_location()=source_location;
+    side_effect_exprt malloc_expr(ID_allocate, expr.type(), source_location);
     malloc_expr.operands()=expr.arguments();
 
     return malloc_expr;