Adding readable names for CAR instrumentation variables.

Author: Remi Delmas

regression/contracts/assigns_enforce_free_dead/test.desc

@@ -29,7 +29,9 @@ main.c
 ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$
-^.*tmp_cc\$\d+.*: FAILURE$
+^.*__car_valid.*: FAILURE$
+^.*__car_lb.*: FAILURE$
+^.*__car_ub.*: FAILURE$
 --
 Checks that invalidated CARs are correctly tracked on `free` and `DEAD`.
 
@@ -40,4 +42,4 @@ We also check (using positive regex matches above) that
 `**p` should be assignable in one case and should not be assignable in the other.
 
 Finally, we check that there should be no "internal" assertion failures
-on `tmp_cc` variables used to track CARs.
+on `__car_valid`, `__car_ub`, `__car_lb` variables used to track CARs.

src/goto-instrument/contracts/assigns.cpp

@@ -52,14 +52,16 @@ static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns)
 }
 
 const symbolt assigns_clauset::conditional_address_ranget::generate_new_symbol(
+  const std::string &prefix,
   const typet &type,
   const source_locationt &location) const
 {
   return new_tmp_symbol(
     type,
     location,
     parent.symbol_table.lookup_ref(parent.function_name).mode,
-    parent.symbol_table);
+    parent.symbol_table,
+    prefix);
 }
 
 assigns_clauset::conditional_address_ranget::conditional_address_ranget(
@@ -70,11 +72,13 @@ assigns_clauset::conditional_address_ranget::conditional_address_ranget(
     parent(parent),
     slice(normalize_to_slice(expr, parent.ns)),
     validity_condition_var(
-      generate_new_symbol(bool_typet(), location).symbol_expr()),
+      generate_new_symbol("__car_valid", bool_typet(), location).symbol_expr()),
     lower_bound_address_var(
-      generate_new_symbol(slice.first.type(), location).symbol_expr()),
+      generate_new_symbol("__car_lb", slice.first.type(), location)
+        .symbol_expr()),
     upper_bound_address_var(
-      generate_new_symbol(slice.first.type(), location).symbol_expr())
+      generate_new_symbol("__car_ub", slice.first.type(), location)
+        .symbol_expr())
 {
 }
 

src/goto-instrument/contracts/assigns.h

@@ -60,8 +60,10 @@ class assigns_clauset
     const exprt
     generate_unsafe_inclusion_check(const conditional_address_ranget &) const;
 
-    const symbolt
-    generate_new_symbol(const typet &, const source_locationt &) const;
+    const symbolt generate_new_symbol(
+      const std::string &prefix,
+      const typet &,
+      const source_locationt &) const;
 
     friend class assigns_clauset;
   };

src/goto-instrument/contracts/contracts.cpp

@@ -936,9 +936,10 @@ void code_contractst::instrument_call_statement(
       const auto object_validity_var_addr =
         new_tmp_symbol(
           pointer_type(bool_typet{}),
-          instruction_it->source_location(),
+          location_no_checks,
           symbol_table.lookup_ref(function).mode,
-          symbol_table)
+          symbol_table,
+          "__car_valid")
           .symbol_expr();
       write_set_validity_addrs.insert(object_validity_var_addr);
 

src/goto-instrument/contracts/utils.cpp

@@ -142,13 +142,18 @@ const symbolt &new_tmp_symbol(
   const typet &type,
   const source_locationt &location,
   const irep_idt &mode,
-  symbol_table_baset &symtab)
+  symbol_table_baset &symtab,
+  std::string suffix,
+  bool is_auxiliary)
 {
-  return get_fresh_aux_symbol(
+  symbolt &new_symbol = get_fresh_aux_symbol(
     type,
-    id2string(location.get_function()) + "::tmp_cc",
-    "tmp_cc",
+    id2string(location.get_function()) + "::",
+    suffix,
     location,
     mode,
     symtab);
+    new_symbol.is_auxiliary = is_auxiliary;
+    return new_symbol;
+}
 }

src/goto-instrument/contracts/utils.h

@@ -105,17 +105,21 @@ void insert_before_swap_and_advance(
   goto_programt::targett &target,
   goto_programt &payload);
 
-/// \brief Adds a new temporary symbol to the symbol table.
+/// \brief Adds a fresh and uniquely named symbol to the symbol table.
 ///
 /// \param type: The type of the new symbol.
 /// \param location: The source location for the new symbol.
 /// \param mode: The mode for the new symbol, e.g. ID_C, ID_java.
 /// \param symtab: The symbol table to which the new symbol is to be added.
+/// \param suffix: Suffix to use to generate the unique name
+/// \param is_auxiliary: Do not print symbol in traces if true (default = false) 
 /// \return The new symbolt object.
 const symbolt &new_tmp_symbol(
   const typet &type,
   const source_locationt &location,
   const irep_idt &mode,
-  symbol_table_baset &symtab);
+  symbol_table_baset &symtab,
+  std::string suffix = "tmp_cc",
+  bool is_auxiliary = false);
 
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H