Add source location to code added by preprocessing

When the String preprocessing adds code to populate some functions, we
should associate a code location to these instructions.
Otherwise this could in particular lead to problem with coverage
instrumentation which would not know what instruction to instrument, and
may not instrument the function at all.

Author: romainbrenguier

src/java_bytecode/java_string_library_preprocess.cpp

@@ -464,7 +464,7 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
     array_data.type(), "char_array", "char_array", loc, ID_java, symbol_table);
   symbol_exprt char_array=sym_char_array.symbol_expr();
   // char_array = array_pointer->data
-  code.add(code_assignt(char_array, array_data));
+  code.add(code_assignt(char_array, array_data), loc);
 
   // string_expr is `{ rhs->length; string_array }`
   refined_string_exprt string_expr(
@@ -524,9 +524,9 @@ refined_string_exprt java_string_library_preprocesst::decl_string_expr(
     ID_java,
     symbol_table);
   symbol_exprt content_field = sym_content.symbol_expr();
-  code.add(code_declt(content_field));
+  code.add(code_declt(content_field), loc);
   refined_string_exprt str(length_field, content_field, refined_string_type);
-  code.add(code_declt(length_field));
+  code.add(code_declt(length_field), loc);
   return str;
 }
 
@@ -545,7 +545,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   const refined_string_exprt str = decl_string_expr(loc, symbol_table, code);
 
   side_effect_expr_nondett nondet_length(str.length().type());
-  code.add(code_assignt(str.length(), nondet_length));
+  code.add(code_assignt(str.length(), nondet_length), loc);
 
   exprt nondet_array_expr =
     make_nondet_infinite_char_array(symbol_table, loc, code);
@@ -559,7 +559,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   add_array_to_length_association(
     nondet_array_expr, str.length(), symbol_table, loc, code);
 
-  code.add(code_assignt(str.content(), array_pointer));
+  code.add(code_assignt(str.content(), array_pointer), loc);
 
   return refined_string_exprt(str.length(), str.content());
 }
@@ -594,7 +594,7 @@ exprt java_string_library_preprocesst::allocate_fresh_array(
   code_blockt &code)
 {
   exprt array=fresh_array(type, loc, symbol_table);
-  code.add(code_declt(array));
+  code.add(code_declt(array), loc);
   allocate_dynamic_object_with_decl(array, symbol_table, loc, code);
   return array;
 }
@@ -659,9 +659,9 @@ exprt make_nondet_infinite_char_array(
     ID_java,
     symbol_table);
   const symbol_exprt data_expr = data_sym.symbol_expr();
-  code.add(code_declt(data_expr));
+  code.add(code_declt(data_expr), loc);
   side_effect_expr_nondett nondet_data(data_expr.type());
-  code.add(code_assignt(data_expr, nondet_data));
+  code.add(code_assignt(data_expr, nondet_data), loc);
   return data_expr;
 }
 
@@ -689,13 +689,14 @@ void add_pointer_to_array_association(
     ID_java,
     symbol_table);
   exprt return_expr = return_sym.symbol_expr();
-  code.add(code_declt(return_expr));
+  code.add(code_declt(return_expr), loc);
   code.add(
     code_assign_function_application(
       return_expr,
       ID_cprover_associate_array_to_pointer_func,
       {array, pointer},
-      symbol_table));
+      symbol_table),
+    loc);
 }
 
 /// Add a call to a primitive of the string solver, letting it know that
@@ -720,13 +721,14 @@ void add_array_to_length_association(
     ID_java,
     symbol_table);
   const exprt return_expr = return_sym.symbol_expr();
-  code.add(code_declt(return_expr));
+  code.add(code_declt(return_expr), loc);
   code.add(
     code_assign_function_application(
       return_expr,
       ID_cprover_associate_length_to_array_func,
       {array, length},
-      symbol_table));
+      symbol_table),
+    loc);
 }
 
 /// Add a call to a primitive of the string solver which ensures all characters
@@ -751,14 +753,15 @@ void add_character_set_constraint(
   symbolt &return_sym = get_fresh_aux_symbol(
     java_int_type(), "cnstr_added", "cnstr_added", loc, ID_java, symbol_table);
   const exprt return_expr = return_sym.symbol_expr();
-  code.add(code_declt(return_expr));
+  code.add(code_declt(return_expr), loc);
   const constant_exprt char_set_expr(char_set, string_typet());
   code.add(
     code_assign_function_application(
       return_expr,
       ID_cprover_string_constrain_characters_func,
       {length, pointer, char_set_expr},
-      symbol_table));
+      symbol_table),
+    loc);
 }
 
 /// Create a refined_string_exprt `str` whose content and length are fresh
@@ -793,7 +796,7 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
     ID_java,
     symbol_table);
   const exprt return_code = return_code_sym.symbol_expr();
-  code.add(code_declt(return_code));
+  code.add(code_declt(return_code), loc);
 
   const refined_string_exprt string_expr =
     make_nondet_string_expr(loc, symbol_table, code);
@@ -807,7 +810,8 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
   // return_code = <function_name>_data(args)
   code.add(
     code_assign_function_application(
-      return_code, function_name, args, symbol_table));
+      return_code, function_name, args, symbol_table),
+    loc);
 
   return string_expr;
 }
@@ -893,9 +897,9 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
   const exprt rhs_length = get_length(deref, symbol_table);
 
   // Assignments
-  code.add(code_assignt(lhs.length(), rhs_length));
+  code.add(code_assignt(lhs.length(), rhs_length), loc);
   const exprt data_as_array = get_data(deref, symbol_table);
-  code.add(code_assignt(lhs.content(), data_as_array));
+  code.add(code_assignt(lhs.content(), data_as_array), loc);
 }
 
 /// Create a string expression whose value is given by a literal
@@ -958,16 +962,21 @@ codet java_string_library_preprocesst::make_equals_function_code(
   const symbolt string_equals_sym = get_fresh_aux_symbol(
     java_boolean_type(), "string_equals", "str_eq", loc, ID_java, symbol_table);
   const symbol_exprt string_equals = string_equals_sym.symbol_expr();
-  code.add(code_declt(string_equals));
-  code.add(code_assignt(
-    string_equals,
-    make_function_application(
-      ID_cprover_string_equal_func, args, type.return_type(), symbol_table)));
-
-  code.add(code_returnt(if_exprt(
-    arg_is_string,
-    string_equals,
-    from_integer(false, java_boolean_type()))));
+  code.add(code_declt(string_equals), loc);
+  code.add(
+    code_assignt(
+      string_equals,
+      make_function_application(
+        ID_cprover_string_equal_func, args, type.return_type(), symbol_table)),
+    loc);
+
+  code.add(
+    code_returnt(
+      if_exprt(
+        arg_is_string,
+        string_equals,
+        from_integer(false, java_boolean_type()))),
+    loc);
   return code;
 }
 
@@ -1094,10 +1103,10 @@ codet java_string_library_preprocesst::make_float_to_string_code(
     ife.else_case()=tmp_code;
     tmp_code=ife;
   }
-  code.add(tmp_code);
+  code.add(tmp_code, loc);
 
   // Return str
-  code.add(code_returnt(str));
+  code.add(code_returnt(str), loc);
   return code;
 }
 
@@ -1144,8 +1153,8 @@ codet java_string_library_preprocesst::make_init_function_from_call(
 
   // arg_this <- string_expr
   code.add(
-    code_assign_string_expr_to_java_string(
-      arg_this, string_expr, symbol_table));
+    code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
+    loc);
 
   return code;
 }
@@ -1168,10 +1177,11 @@ codet java_string_library_preprocesst::
   code_typet::parameterst params=type.parameters();
   PRECONDITION(!params.empty());
   code_blockt code;
-  code.add(make_assign_function_from_call(
-    function_name, type, loc, symbol_table));
+  code.add(
+    make_assign_function_from_call(function_name, type, loc, symbol_table),
+    loc);
   exprt arg_this=symbol_exprt(params[0].get_identifier(), params[0].type());
-  code.add(code_returnt(arg_this));
+  code.add(code_returnt(arg_this), loc);
   return code;
 }
 
@@ -1288,14 +1298,14 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
       dereference_exprt deref(
         typecast_exprt(object, pointer_type), pointer_type.subtype());
       member_exprt deref_value(deref, value_comp.get_name(), value_comp.type());
-      code.add(code_assignt(value, deref_value));
+      code.add(code_assignt(value, deref_value), loc);
       return value;
     }
   }
 
   warning() << object_type.get_identifier()
             << " not available to format function" << eom;
-  code.add(code_declt(value));
+  code.add(code_declt(value), loc);
   return value;
 }
 
@@ -1378,7 +1388,7 @@ exprt java_string_library_preprocesst::make_argument_for_format(
       symbolt field_symbol=get_fresh_aux_symbol(
         type, tmp_name, tmp_name, loc, ID_java, symbol_table);
       field_expr=field_symbol.symbol_expr();
-      code.add(code_declt(field_expr));
+      code.add(code_declt(field_expr), loc);
     }
     else
       field_expr = make_nondet_string_expr(loc, symbol_table, code);
@@ -1393,9 +1403,12 @@ exprt java_string_library_preprocesst::make_argument_for_format(
     obj.type(), "tmp_format_obj", "tmp_format_obj", loc, ID_java, symbol_table);
   symbol_exprt arg_i=object_symbol.symbol_expr();
   allocate_dynamic_object_with_decl(arg_i, symbol_table, loc, code);
-  code.add(code_assignt(arg_i, obj));
-  code.add(code_assumet(not_exprt(equal_exprt(
-    arg_i, null_pointer_exprt(to_pointer_type(arg_i.type()))))));
+  code.add(code_assignt(arg_i, obj), loc);
+  code.add(
+    code_assumet(
+      not_exprt(
+        equal_exprt(arg_i, null_pointer_exprt(to_pointer_type(arg_i.type()))))),
+    loc);
 
   // if arg_i != null then [code_not_null]
   code_ifthenelset code_avoid_null_arg;
@@ -1426,15 +1439,15 @@ exprt java_string_library_preprocesst::make_argument_for_format(
     {
       exprt value=get_primitive_value_of_object(
         arg_i, name, loc, symbol_table, code_not_null);
-      code_not_null.add(code_assignt(field_expr, value));
+      code_not_null.add(code_assignt(field_expr, value), loc);
     }
     else
     {
       // TODO: date_time and hash_code not implemented
     }
   }
 
-  code.add(code_not_null);
+  code.add(code_not_null, loc);
   return arg_i_struct;
 }
 
@@ -1488,8 +1501,9 @@ codet java_string_library_preprocesst::make_string_format_code(
     type.return_type(), loc, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(
-      java_string, string_expr, symbol_table));
-  code.add(code_returnt(java_string));
+      java_string, string_expr, symbol_table),
+    loc);
+  code.add(code_returnt(java_string), loc);
   return code;
 }
 
@@ -1523,7 +1537,7 @@ codet java_string_library_preprocesst::make_object_get_class_code(
   symbolt class1_sym=get_fresh_aux_symbol(
     class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);
   symbol_exprt class1=class1_sym.symbol_expr();
-  code.add(code_declt(class1));
+  code.add(code_declt(class1), loc);
 
   // class_identifier is this->@class_identifier
   member_exprt class_identifier(
@@ -1553,8 +1567,8 @@ codet java_string_library_preprocesst::make_object_get_class_code(
     symbol_table.lookup_ref("java::java.lang.String").type);
   exprt string1=allocate_fresh_string(string_ptr_type, loc, symbol_table, code);
   code.add(
-    code_assign_string_expr_to_java_string(
-      string1, string_expr1, symbol_table));
+    code_assign_string_expr_to_java_string(string1, string_expr1, symbol_table),
+    loc);
 
   // > class1 = Class.forName(string1)
   code_function_callt fun_call;
@@ -1565,10 +1579,10 @@ codet java_string_library_preprocesst::make_object_get_class_code(
   code_typet fun_type;
   fun_type.return_type()=string1.type();
   fun_call.function().type()=fun_type;
-  code.add(fun_call);
+  code.add(fun_call, loc);
 
   // > return class1;
-  code.add(code_returnt(class1));
+  code.add(code_returnt(class1), loc);
   return code;
 }
 
@@ -1591,8 +1605,10 @@ codet java_string_library_preprocesst::make_function_from_call(
   code_blockt code;
   exprt::operandst args=process_parameters(
     type.parameters(), loc, symbol_table, code);
-  code.add(code_return_function_application(
-    function_name, args, type.return_type(), symbol_table));
+  code.add(
+    code_return_function_application(
+      function_name, args, type.return_type(), symbol_table),
+    loc);
   return code;
 }
 
@@ -1629,10 +1645,11 @@ codet java_string_library_preprocesst::make_string_returning_function_from_call(
   // Assign to string
   exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code);
   code.add(
-    code_assign_string_expr_to_java_string(str, string_expr, symbol_table));
+    code_assign_string_expr_to_java_string(str, string_expr, symbol_table),
+    loc);
 
   // Return value
-  code.add(code_returnt(str));
+  code.add(code_returnt(str), loc);
   return code;
 }
 
@@ -1669,10 +1686,11 @@ codet java_string_library_preprocesst::make_copy_string_code(
   // Allocate and assign the string
   exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code);
   code.add(
-    code_assign_string_expr_to_java_string(str, string_expr, symbol_table));
+    code_assign_string_expr_to_java_string(str, string_expr, symbol_table),
+    loc);
 
   // Return value
-  code.add(code_returnt(str));
+  code.add(code_returnt(str), loc);
   return code;
 }
 
@@ -1707,8 +1725,8 @@ codet java_string_library_preprocesst::make_copy_constructor_code(
   // Assign string_expr to `this` object
   symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
   code.add(
-    code_assign_string_expr_to_java_string(
-      arg_this, string_expr, symbol_table));
+    code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
+    loc);
 
   return code;
 }
@@ -1752,8 +1770,8 @@ codet java_string_library_preprocesst::make_init_from_array_code(
   // Assign string_expr to `this` object
   symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
   code.add(
-    code_assign_string_expr_to_java_string(
-      arg_this, string_expr, symbol_table));
+    code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
+    loc);
 
   return code;
 }

src/util/std_code.h

@@ -108,6 +108,12 @@ class code_blockt:public codet
     copy_to_operands(code);
   }
 
+  void add(codet code, const source_locationt &loc)
+  {
+    code.add_source_location() = loc;
+    add(code);
+  }
+
   void append(const code_blockt &extra_block);
 
   // This is the closing '}' or 'END' at the end of a block