Merge pull request #3767 from chrisr-diffblue/validate_goto_programs_symbol_check_fixup

Fix up symbol naming checks so --validate-goto-model can be enabled in regression testing.

Author: chrisr-diffblue

regression/cbmc/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>" -X smt-backend
+    "$<TARGET_FILE:cbmc> --validate-goto-model" -X smt-backend
 )

regression/cbmc/Makefile

@@ -1,13 +1,12 @@
-default: tests.log
+default: test
 
 test:
-	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+	@../test.pl -p -c "../../../src/cbmc/cbmc --validate-goto-model" -X smt-backend
 
 test-cprover-smt2:
 	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
 
-tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+tests.log: ../test.pl test
 
 show:
 	@for dir in *; do \

regression/cbmc/trace-values/trace-values.c

@@ -1,3 +1,5 @@
+#include <stdlib.h>
+
 int global_var;
 
 struct S

regression/cbmc/typedef-return-anon-struct1/test.desc

@@ -5,7 +5,7 @@ main.c
 activate-multi-line-match
 EXIT=0
 SIGNAL=0
-Base name\.+: return\nMode\.+: C\nType\.+: MYSTRUCT
+Base name\.+: return'\nMode\.+: C\nType\.+: MYSTRUCT
 Base name\.+: fun\nMode\.+: C\nType\.+: MYSTRUCT \(\)
 --
 warning: ignoring

regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc

@@ -5,7 +5,7 @@ main.c
 activate-multi-line-match
 EXIT=0
 SIGNAL=0
-Base name\.+: return\nMode\.+: C\nType\.+: MYSTRUCT
+Base name\.+: return'\nMode\.+: C\nType\.+: MYSTRUCT
 Base name\.+: fun\nMode\.+: C\nType\.+: MYSTRUCT \(\)
 --
 warning: ignoring

src/ansi-c/ansi_c_entry_point.cpp

@@ -238,7 +238,7 @@ bool generate_ansi_c_start_function(
     return_symbol.mode=ID_C;
     return_symbol.is_static_lifetime=false;
     return_symbol.name="return'";
-    return_symbol.base_name="return";
+    return_symbol.base_name = "return'";
     return_symbol.type=to_code_type(symbol.type).return_type();
 
     symbol_table.add(return_symbol);
@@ -261,7 +261,7 @@ bool generate_ansi_c_start_function(
       {
         symbolt argc_symbol;
 
-        argc_symbol.base_name = "argc";
+        argc_symbol.base_name = "argc'";
         argc_symbol.name = "argc'";
         argc_symbol.type = signed_int_type();
         argc_symbol.is_static_lifetime = true;

src/ansi-c/c_typecheck_expr.cpp

@@ -538,6 +538,7 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
   symbol.base_name=ID_gcc_builtin_va_arg;
   symbol.name=ID_gcc_builtin_va_arg;
   symbol.type=symbol_type;
+  symbol.mode = ID_C;
 
   symbol_table.insert(std::move(symbol));
 }

src/ansi-c/c_typecheck_type.cpp

@@ -769,7 +769,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
     typecheck_compound_body(to_struct_union_type(compound_symbol.type));
 
     std::string typestr = type2name(compound_symbol.type, *this);
-    compound_symbol.base_name="#anon-"+typestr;
+    compound_symbol.base_name = "#anon#" + typestr;
     compound_symbol.name="tag-#anon#"+typestr;
     identifier=compound_symbol.name;
 

src/goto-programs/goto_convert_class.h

@@ -335,7 +335,7 @@ class goto_convertt:public messaget
 
   typedef std::vector<codet> destructor_stackt;
 
-  symbol_exprt exception_flag();
+  symbol_exprt exception_flag(const irep_idt &mode);
   void unwind_destructor_stack(
     const source_locationt &,
     std::size_t stack_size,

src/goto-programs/goto_convert_exceptions.cpp

@@ -168,7 +168,7 @@ void goto_convertt::convert_CPROVER_try_catch(
   targets.set_throw(tmp.instructions.begin());
 
   // now put 'catch' code onto destructor stack
-  code_ifthenelset catch_code(exception_flag(), to_code(code.op1()));
+  code_ifthenelset catch_code(exception_flag(mode), to_code(code.op1()));
   catch_code.add_source_location()=code.source_location();
 
   targets.destructor_stack.push_back(std::move(catch_code));
@@ -194,7 +194,7 @@ void goto_convertt::convert_CPROVER_throw(
       dest.add_instruction(ASSIGN);
 
     t_set_exception->source_location=code.source_location();
-    t_set_exception->code=code_assignt(exception_flag(), true_exprt());
+    t_set_exception->code = code_assignt(exception_flag(mode), true_exprt());
   }
 
   // do we catch locally?
@@ -244,7 +244,7 @@ void goto_convertt::convert_CPROVER_try_finally(
   convert(to_code(code.op1()), dest, mode);
 }
 
-symbol_exprt goto_convertt::exception_flag()
+symbol_exprt goto_convertt::exception_flag(const irep_idt &mode)
 {
   irep_idt id="$exception_flag";
 
@@ -260,6 +260,7 @@ symbol_exprt goto_convertt::exception_flag()
     new_symbol.is_thread_local=true;
     new_symbol.is_file_local=false;
     new_symbol.type=bool_typet();
+    new_symbol.mode = mode;
     symbol_table.insert(std::move(new_symbol));
   }
 

src/goto-programs/goto_function.cpp

@@ -31,3 +31,36 @@ void get_local_identifiers(
       dest.insert(identifier);
   }
 }
+
+/// Check that the goto function is well-formed
+///
+/// The validation mode indicates whether well-formedness check failures are
+/// reported via DATA_INVARIANT violations or exceptions.
+void goto_functiont::validate(const namespacet &ns, const validation_modet vm)
+  const
+{
+  body.validate(ns, vm);
+
+  find_symbols_sett typetags;
+  find_type_symbols(type, typetags);
+  const symbolt *symbol;
+  for(const auto &identifier : typetags)
+  {
+    DATA_CHECK(
+      vm, !ns.lookup(identifier, symbol), id2string(identifier) + " not found");
+  }
+
+  // Check that a void function does not contain any RETURN instructions
+  if(to_code_type(type).return_type().id() == ID_empty)
+  {
+    forall_goto_program_instructions(instruction, body)
+    {
+      DATA_CHECK(
+        vm,
+        !instruction->is_return(),
+        "void function should not return a value");
+    }
+  }
+
+  validate_full_type(type, ns, vm);
+}

src/goto-programs/goto_function.h

@@ -116,23 +116,7 @@ class goto_functiont
   ///
   /// The validation mode indicates whether well-formedness check failures are
   /// reported via DATA_INVARIANT violations or exceptions.
-  void validate(const namespacet &ns, const validation_modet vm) const
-  {
-    body.validate(ns, vm);
-
-    find_symbols_sett typetags;
-    find_type_symbols(type, typetags);
-    const symbolt *symbol;
-    for(const auto &identifier : typetags)
-    {
-      DATA_CHECK(
-        vm,
-        !ns.lookup(identifier, symbol),
-        id2string(identifier) + " not found");
-    }
-
-    validate_full_type(type, ns, vm);
-  }
+  void validate(const namespacet &ns, const validation_modet vm) const;
 };
 
 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);

src/goto-programs/goto_program.cpp

@@ -22,6 +22,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language_util.h>
 
+#include "remove_returns.h"
+
 /// Writes to \p out a two/three line string representation of a given
 /// \p instruction. The output is of the format:
 /// ```
@@ -709,13 +711,75 @@ void goto_programt::instructiont::validate(
         const auto &goto_id = goto_symbol_expr.get_identifier();
 
         if(!ns.lookup(goto_id, table_symbol))
+        {
+          bool symbol_expr_type_matches_symbol_table =
+            base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns);
+
+          if(
+            !symbol_expr_type_matches_symbol_table &&
+            table_symbol->type.id() == ID_code)
+          {
+            // Return removal sets the return type of a function symbol table
+            // entry to 'void', but some callsites still expect the original
+            // type (e.g. if a function is passed as a parameter)
+            symbol_expr_type_matches_symbol_table = base_type_eq(
+              goto_symbol_expr.type(),
+              original_return_type(ns.get_symbol_table(), goto_id),
+              ns);
+
+            if(
+              !symbol_expr_type_matches_symbol_table &&
+              goto_symbol_expr.type().id() == ID_code)
+            {
+              // If a function declaration and its definition are in different
+              // translation units they may have different return types,
+              // which remove_returns patches up with a typecast. If thats
+              // the case, then the return type in the symbol table may differ
+              // from the return type in the symbol expr
+              if(
+                goto_symbol_expr.type().source_location().get_file() !=
+                table_symbol->type.source_location().get_file())
+              {
+                // temporarily fixup the return types
+                auto goto_symbol_expr_type =
+                  to_code_type(goto_symbol_expr.type());
+                auto table_symbol_type = to_code_type(table_symbol->type);
+
+                goto_symbol_expr_type.return_type() =
+                  table_symbol_type.return_type();
+
+                symbol_expr_type_matches_symbol_table =
+                  base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
+              }
+            }
+          }
+
+          if(
+            !symbol_expr_type_matches_symbol_table &&
+            goto_symbol_expr.type().id() == ID_array &&
+            to_array_type(goto_symbol_expr.type()).is_incomplete())
+          {
+            // If the symbol expr has an incomplete array type, it may not have
+            // a constant size value, whereas the symbol table entry may have
+            // an (assumed) constant size of 1 (which mimics gcc behaviour)
+            if(table_symbol->type.id() == ID_array)
+            {
+              auto symbol_table_array_type = to_array_type(table_symbol->type);
+              symbol_table_array_type.size() = nil_exprt();
+
+              symbol_expr_type_matches_symbol_table = base_type_eq(
+                goto_symbol_expr.type(), symbol_table_array_type, ns);
+            }
+          }
+
           DATA_CHECK_WITH_DIAGNOSTICS(
             vm,
-            base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns),
+            symbol_expr_type_matches_symbol_table,
             id2string(goto_id) + " type inconsistency\n" +
               "goto program type: " + goto_symbol_expr.type().id_string() +
               "\n" + "symbol table type: " + table_symbol->type.id_string(),
             current_source_location);
+        }
       }
     };
 

src/util/std_code.h

@@ -1135,12 +1135,7 @@ class code_function_callt:public codet
   {
     check(code, vm);
 
-    if(code.op0().id() == ID_nil)
-      DATA_CHECK(
-        vm,
-        to_code_type(code.op1().type()).return_type().id() == ID_empty,
-        "void function should not return value");
-    else
+    if(code.op0().id() != ID_nil)
       DATA_CHECK(
         vm,
         base_type_eq(

src/util/symbol.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "source_location.h"
 #include "std_expr.h"
+#include "string_utils.h"
 #include "suffix.h"
 
 /// Dump the state of a symbol object to a given output stream.
@@ -137,11 +138,62 @@ bool symbolt::is_well_formed() const
   // Well-formedness criterion number 2 is for a symbol
   // to have it's base name as a suffix to it's more
   // general name.
+
   // Exception: Java symbols' base names do not have type signatures
   // (for example, they can have name "someclass.method:(II)V" and base name
   // "method")
   if(!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java)
-    return false;
+  {
+    bool criterion_must_hold = true;
+
+    // There are some special cases where this criterion doesn't hold, check
+    // to see if we have one of those cases
+
+    if(is_type)
+    {
+      // Typedefs
+      if(
+        type.find(ID_C_typedef).is_not_nil() &&
+        type.find(ID_C_typedef).id() == base_name)
+      {
+        criterion_must_hold = false;
+      }
+
+      // Tag types
+      if(type.find(ID_tag).is_not_nil() && type.find(ID_tag).id() == base_name)
+      {
+        criterion_must_hold = false;
+      }
+    }
+
+    // Linker renaming may have added $linkN suffixes to the name, and other
+    // suffixes such as #return_value may have then be subsequently added.
+    // Strip out the first $linkN substring and then see if the criterion holds
+    const auto &unstripped_name = id2string(name);
+    const size_t dollar_link_start_pos = unstripped_name.find("$link");
+
+    if(dollar_link_start_pos != std::string::npos)
+    {
+      size_t dollar_link_end_pos = dollar_link_start_pos + 5;
+      while(isdigit(unstripped_name[dollar_link_end_pos]))
+      {
+        ++dollar_link_end_pos;
+      }
+
+      const auto stripped_name =
+        unstripped_name.substr(0, dollar_link_start_pos) +
+        unstripped_name.substr(dollar_link_end_pos, std::string::npos);
+
+      if(has_suffix(stripped_name, id2string(base_name)))
+        criterion_must_hold = false;
+    }
+
+    if(criterion_must_hold)
+    {
+      // For all other cases this criterion should hold
+      return false;
+    }
+  }
 
   return true;
 }