Pass location around for nondet initialization

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -812,8 +812,10 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     code_declt declare_cloned(local_symexpr);
     clone_body.move_to_operands(declare_cloned);
 
+    source_locationt location;
+    location.set_function(local_name);
     side_effect_exprt java_new_array(
-      ID_java_new_array, java_reference_type(symbol_type), source_locationt());
+      ID_java_new_array, java_reference_type(symbol_type), location);
     dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
     dereference_exprt new_array(local_symexpr, symbol_type);
     member_exprt old_length(
@@ -859,7 +861,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, typet(), source_locationt());
+    side_effect_exprt inc(ID_assign, typet(), location);
     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_object_factory.cpp

@@ -69,13 +69,15 @@ class java_object_factoryt
     const typet &target_type,
     allocation_typet alloc_type,
     size_t depth,
-    update_in_placet update_in_place);
+    update_in_placet update_in_place,
+    const source_locationt &location);
 
   void allocate_nondet_length_array(
     code_blockt &assignments,
     const exprt &lhs,
     const exprt &max_length_expr,
-    const typet &element_type);
+    const typet &element_type,
+    const source_locationt &location);
 
 public:
   java_object_factoryt(
@@ -102,7 +104,8 @@ class java_object_factoryt
     code_blockt &assignments,
     const exprt &expr,
     size_t depth,
-    update_in_placet);
+    update_in_placet,
+    const source_locationt &location);
 
   void gen_nondet_init(
     code_blockt &assignments,
@@ -114,7 +117,8 @@ class java_object_factoryt
     bool override_,
     const typet &override_type,
     size_t depth,
-    update_in_placet);
+    update_in_placet,
+    const source_locationt &location);
 
 private:
   void gen_nondet_pointer_init(
@@ -123,7 +127,8 @@ class java_object_factoryt
     allocation_typet alloc_type,
     const pointer_typet &pointer_type,
     size_t depth,
-    const update_in_placet &update_in_place);
+    const update_in_placet &update_in_place,
+    const source_locationt &location);
 
   void gen_nondet_struct_init(
     code_blockt &assignments,
@@ -134,13 +139,15 @@ class java_object_factoryt
     allocation_typet alloc_type,
     const struct_typet &struct_type,
     size_t depth,
-    const update_in_placet &update_in_place);
+    const update_in_placet &update_in_place,
+    const source_locationt &location);
 
   symbol_exprt gen_nondet_subtype_pointer_init(
     code_blockt &assignments,
     allocation_typet alloc_type,
     const pointer_typet &substitute_pointer_type,
-    size_t depth);
+    size_t depth,
+    const source_locationt &location);
 };
 
 /// Generates code for allocating a dynamic object. This is used in
@@ -372,7 +379,8 @@ void java_object_factoryt::gen_pointer_target_init(
   const typet &target_type,
   allocation_typet alloc_type,
   size_t depth,
-  update_in_placet update_in_place)
+  update_in_placet update_in_place,
+  const source_locationt &location)
 {
   PRECONDITION(expr.type().id()==ID_pointer);
   PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE);
@@ -383,10 +391,7 @@ void java_object_factoryt::gen_pointer_target_init(
        "java::array["))
   {
     gen_nondet_array_init(
-      assignments,
-      expr,
-      depth+1,
-      update_in_place);
+      assignments, expr, depth + 1, update_in_place, location);
   }
   else
   {
@@ -426,14 +431,15 @@ void java_object_factoryt::gen_pointer_target_init(
     gen_nondet_init(
       assignments,
       init_expr,
-      false,   // is_sub
-      "",      // class_identifier
-      false,   // skip_classid
+      false, // is_sub
+      "",    // class_identifier
+      false, // skip_classid
       alloc_type,
-      false,   // override
-      typet(), // override type immaterial
-      depth+1,
-      update_in_place);
+      false,
+      typet(),
+      depth + 1,
+      update_in_place,
+      location);
   }
 }
 
@@ -688,7 +694,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
   allocation_typet alloc_type,
   const pointer_typet &pointer_type,
   size_t depth,
-  const update_in_placet &update_in_place)
+  const update_in_placet &update_in_place,
+  const source_locationt &location)
 {
   PRECONDITION(expr.type().id()==ID_pointer);
   const pointer_typet &replacement_pointer_type =
@@ -710,7 +717,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
       replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
 
     const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
-      assignments, alloc_type, replacement_pointer_type, depth);
+      assignments, alloc_type, replacement_pointer_type, depth, location);
 
     // Having created a pointer to object of type replacement_pointer_type
     // we now assign it back to the original pointer with a cast
@@ -772,7 +779,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
       subtype,
       alloc_type,
       depth,
-      update_in_placet::MUST_UPDATE_IN_PLACE);
+      update_in_placet::MUST_UPDATE_IN_PLACE,
+      location);
   }
 
   // if we MUST_UPDATE_IN_PLACE, then the job is done, we copy the code emitted
@@ -794,7 +802,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
     subtype,
     alloc_type,
     depth,
-    update_in_placet::NO_UPDATE_IN_PLACE);
+    update_in_placet::NO_UPDATE_IN_PLACE,
+    location);
 
   auto set_null_inst=get_null_assignment(expr, pointer_type);
 
@@ -829,8 +838,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
     //             tmp$<temporary_counter>>
     // }
     code_ifthenelset null_check;
-    null_check.cond() =
-      side_effect_expr_nondett(bool_typet(), expr.source_location());
+    null_check.cond() = side_effect_expr_nondett(bool_typet(), location);
     null_check.then_case()=set_null_inst;
     null_check.else_case()=non_null_inst;
 
@@ -886,7 +894,8 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
   code_blockt &assignments,
   allocation_typet alloc_type,
   const pointer_typet &replacement_pointer,
-  size_t depth)
+  size_t depth,
+  const source_locationt &location)
 {
   symbolt new_symbol = get_fresh_aux_symbol(
     replacement_pointer,
@@ -900,14 +909,15 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
   gen_nondet_init(
     assignments,
     new_symbol.symbol_expr(),
-    false,   // is_sub
-    "",      // class_identifier
-    false,   // skip_classid
+    false, // is_sub
+    "",    // class_identifier
+    false, // skip_classid
     alloc_type,
     false,   // override
     typet(), // override_type
     depth,
-    update_in_placet::NO_UPDATE_IN_PLACE);
+    update_in_placet::NO_UPDATE_IN_PLACE,
+    location);
 
   return new_symbol.symbol_expr();
 }
@@ -950,7 +960,8 @@ void java_object_factoryt::gen_nondet_struct_init(
   allocation_typet alloc_type,
   const struct_typet &struct_type,
   size_t depth,
-  const update_in_placet &update_in_place)
+  const update_in_placet &update_in_place,
+  const source_locationt &location)
 {
   PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
   PRECONDITION(struct_type.id()==ID_struct);
@@ -1052,12 +1063,13 @@ void java_object_factoryt::gen_nondet_struct_init(
         me,
         _is_sub,
         class_identifier,
-        false,   // skip_classid
+        false, // skip_classid
         alloc_type,
         false,   // override
         typet(), // override_type
         depth,
-        substruct_in_place);
+        substruct_in_place,
+        location);
     }
   }
 
@@ -1125,7 +1137,8 @@ void java_object_factoryt::gen_nondet_init(
   bool override_,
   const typet &override_type,
   size_t depth,
-  update_in_placet update_in_place)
+  update_in_placet update_in_place,
+  const source_locationt &location)
 {
   const typet &type=
     override_ ? ns.follow(override_type) : ns.follow(expr.type());
@@ -1150,7 +1163,8 @@ void java_object_factoryt::gen_nondet_init(
       alloc_type,
       pointer_type,
       depth,
-      update_in_place);
+      update_in_place,
+      location);
   }
   else if(type.id()==ID_struct)
   {
@@ -1179,7 +1193,8 @@ void java_object_factoryt::gen_nondet_init(
       alloc_type,
       struct_type,
       depth,
-      update_in_place);
+      update_in_place,
+      location);
   }
   else
   {
@@ -1211,7 +1226,8 @@ void java_object_factoryt::allocate_nondet_length_array(
   code_blockt &assignments,
   const exprt &lhs,
   const exprt &max_length_expr,
-  const typet &element_type)
+  const typet &element_type,
+  const source_locationt &location)
 {
   symbolt &length_sym = get_fresh_aux_symbol(
     java_int_type(),
@@ -1234,7 +1250,8 @@ void java_object_factoryt::allocate_nondet_length_array(
     false,                   // override
     typet(),                 // override type is immaterial
     0,                       // depth is immaterial, always non-null
-    update_in_placet::NO_UPDATE_IN_PLACE);
+    update_in_placet::NO_UPDATE_IN_PLACE,
+    location);
 
   // Insert assumptions to bound its length:
   binary_relation_exprt
@@ -1265,7 +1282,8 @@ void java_object_factoryt::gen_nondet_array_init(
   code_blockt &assignments,
   const exprt &expr,
   size_t depth,
-  update_in_placet update_in_place)
+  update_in_placet update_in_place,
+  const source_locationt &location)
 {
   PRECONDITION(expr.type().id()==ID_pointer);
   PRECONDITION(expr.type().subtype().id()==ID_symbol);
@@ -1284,10 +1302,7 @@ void java_object_factoryt::gen_nondet_array_init(
   if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
   {
     allocate_nondet_length_array(
-      assignments,
-      expr,
-      max_length_expr,
-      element_type);
+      assignments, expr, max_length_expr, element_type, location);
   }
 
   // Otherwise we're updating the array in place, and use the
@@ -1377,15 +1392,16 @@ void java_object_factoryt::gen_nondet_array_init(
   gen_nondet_init(
     assignments,
     arraycellref,
-    false, // is_sub
+    false,      // is_sub
     irep_idt(), // class_identifier
-    false, // skip_classid
+    false,      // skip_classid
     // These are variable in number, so use dynamic allocator:
     allocation_typet::DYNAMIC,
-    true,  // override
+    true, // override
     element_type,
     depth,
-    child_update_in_place);
+    child_update_in_place,
+    location);
 
   exprt java_one=from_integer(1, java_int_type());
   code_assignt incr(counter_expr, plus_exprt(counter_expr, java_one));
@@ -1476,7 +1492,8 @@ exprt object_factory(
     false,   // override
     typet(), // override_type is immaterial
     1,       // initial depth
-    update_in_placet::NO_UPDATE_IN_PLACE);
+    update_in_placet::NO_UPDATE_IN_PLACE,
+    loc);
 
   declare_created_symbols(symbols_created, loc, init_code);
 
@@ -1549,7 +1566,8 @@ void gen_nondet_init(
     false,   // override
     typet(), // override_type is immaterial
     1,       // initial depth
-    update_in_place);
+    update_in_place,
+    loc);
 
   declare_created_symbols(symbols_created, loc, init_code);