Add source location to invalid_source_file_exceptiont

This enables proper use in the C front-end in a way that is compatible
with the compiler-specific message handlers in goto-cc: those message
handlers generate source-location output that mimics that of the
compiler being emulated.

As future work it is thus possible to remove all "throw 0" instances
from the C front-end.

Author: tautschnig

regression/ansi-c/enum_is_in_range/enum_test10.desc

@@ -1,9 +1,9 @@
 CORE
 enum_test10.c
 
-^EXIT=(6|70)$
+^EXIT=(1|64)$
 ^SIGNAL=0$
-^file enum_test10.c line \d+ function main: __CPROVER_enum_is_in_range expects enum, but \(i\) has type `signed int`$
+__CPROVER_enum_is_in_range expects enum, but \(i\) has type `signed int`$
 --
 ^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): SUCCESS$
 ^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): FAILURE$

regression/ansi-c/enum_is_in_range/enum_test12.desc

@@ -1,9 +1,9 @@
 CORE
 enum_test12.c
 
-^EXIT=(6|70)$
+^EXIT=(1|64)$
 ^SIGNAL=0$
-^file enum_test12.c line \d+ function main: __CPROVER_enum_is_in_range takes exactly 1 argument, but 2 were provided$
+__CPROVER_enum_is_in_range takes exactly 1 argument, but 2 were provided$
 --
 ^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): SUCCESS$
 ^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): FAILURE$

src/ansi-c/ansi_c_typecheck.cpp

@@ -67,5 +67,11 @@ bool ansi_c_typecheck(
     ansi_c_typecheck.error() << e << messaget::eom;
   }
 
+  catch(const invalid_source_file_exceptiont &e)
+  {
+    ansi_c_typecheck.error().source_location = e.get_source_location();
+    ansi_c_typecheck.error() << e.get_reason() << messaget::eom;
+  }
+
   return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
 }

src/ansi-c/c_typecheck_expr.cpp

@@ -3147,21 +3147,22 @@ exprt c_typecheck_baset::do_special_functions(
     if(expr.arguments().size() != 1)
     {
       std::ostringstream error_message;
-      error_message << expr.source_location().as_string() << ": " << identifier
-                    << " takes exactly 1 argument, but "
+      error_message << identifier << " takes exactly 1 argument, but "
                     << expr.arguments().size() << " were provided";
-      throw invalid_source_file_exceptiont{error_message.str()};
+      throw invalid_source_file_exceptiont{error_message.str(),
+                                           expr.source_location()};
     }
     auto arg1 = expr.arguments()[0];
     typecheck_expr(arg1);
     if(!can_cast_type<c_enum_tag_typet>(arg1.type()))
     {
       // Can't enum range check a non-enum
       std::ostringstream error_message;
-      error_message << expr.source_location().as_string() << ": " << identifier
-                    << " expects enum, but (" << expr2c(arg1, *this)
-                    << ") has type `" << type2c(arg1.type(), *this) << '`';
-      throw invalid_source_file_exceptiont{error_message.str()};
+      error_message << identifier << " expects enum, but ("
+                    << expr2c(arg1, *this) << ") has type `"
+                    << type2c(arg1.type(), *this) << '`';
+      throw invalid_source_file_exceptiont{error_message.str(),
+                                           expr.source_location()};
     }
     else
     {
@@ -3180,10 +3181,10 @@ exprt c_typecheck_baset::do_special_functions(
     if(expr.arguments().size() != 3)
     {
       std::ostringstream error_message;
-      error_message << expr.source_location().as_string() << ": " << identifier
-                    << " takes exactly 3 arguments, but "
+      error_message << identifier << " takes exactly 3 arguments, but "
                     << expr.arguments().size() << " were provided";
-      throw invalid_source_file_exceptiont{error_message.str()};
+      throw invalid_source_file_exceptiont{error_message.str(),
+                                           expr.source_location()};
     }
 
     typecheck_function_call_arguments(expr);
@@ -3199,14 +3200,14 @@ exprt c_typecheck_baset::do_special_functions(
         [this, identifier](
           const exprt &wrong_argument, std::size_t argument_number, bool _p) {
           std::ostringstream error_message;
-          error_message << wrong_argument.source_location().as_string() << ": "
-                        << identifier << " has signature " << identifier
+          error_message << identifier << " has signature " << identifier
                         << "(integral, integral, integral" << (_p ? "" : "*")
                         << "), "
                         << "but argument " << argument_number << " ("
                         << expr2c(wrong_argument, *this) << ") has type `"
                         << type2c(wrong_argument.type(), *this) << '`';
-          throw invalid_source_file_exceptiont{error_message.str()};
+          throw invalid_source_file_exceptiont{
+            error_message.str(), wrong_argument.source_location()};
         };
       for(int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
       {

src/ansi-c/c_typecheck_type.cpp

@@ -1198,10 +1198,9 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
     if(!is_signed_or_unsigned_bitvector(underlying_type))
     {
       std::ostringstream msg;
-      msg << source_location << ": non-integral type '"
-          << underlying_type.get(ID_C_c_type)
+      msg << "non-integral type '" << underlying_type.get(ID_C_c_type)
           << "' is an invalid underlying type";
-      throw invalid_source_file_exceptiont{msg.str()};
+      throw invalid_source_file_exceptiont{msg.str(), source_location};
     }
   }
 
@@ -1260,11 +1259,9 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
       if(value < tmp.smallest() || value > tmp.largest())
       {
         std::ostringstream msg;
-        msg
-          << v.source_location()
-          << ": enumerator value is not representable in the underlying type '"
-          << constant_type.get(ID_C_c_type) << "'";
-        throw invalid_source_file_exceptiont{msg.str()};
+        msg << "enumerator value is not representable in the underlying type '"
+            << constant_type.get(ID_C_c_type) << "'";
+        throw invalid_source_file_exceptiont{msg.str(), v.source_location()};
       }
     }
     else

src/ansi-c/literals/convert_character_literal.cpp

@@ -20,7 +20,8 @@ Author: Daniel Kroening, [email protected]
 
 exprt convert_character_literal(
   const std::string &src,
-  bool force_integer_type)
+  bool force_integer_type,
+  const source_locationt &source_location)
 {
   assert(src.size()>=2);
 
@@ -60,8 +61,10 @@ exprt convert_character_literal(
       result=from_integer(x, type);
     }
     else
-      throw "wide literals with "+std::to_string(value.size())+
-            " characters are not supported";
+      throw invalid_source_file_exceptiont{"wide literals with " +
+                                             std::to_string(value.size()) +
+                                             " characters are not supported",
+                                           source_location};
   }
   else
   {
@@ -93,9 +96,12 @@ exprt convert_character_literal(
       result=from_integer(x, signed_int_type());
     }
     else
-      throw "literals with "+std::to_string(value.size())+
-            " characters are not supported";
+      throw invalid_source_file_exceptiont{"literals with " +
+                                             std::to_string(value.size()) +
+                                             " characters are not supported",
+                                           source_location};
   }
 
+  result.add_source_location() = source_location;
   return result;
 }

src/ansi-c/literals/convert_character_literal.h

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 
 exprt convert_character_literal(
   const std::string &src,
-  bool force_integer_type);
+  bool force_integer_type,
+  const source_locationt &source_location);
 
 #endif // CPROVER_ANSI_C_LITERALS_CONVERT_CHARACTER_LITERAL_H

src/ansi-c/scanner.l

@@ -308,8 +308,8 @@ void ansi_c_scanner_init()
 
 <GRAMMAR>{char_lit} {
                   newstack(yyansi_clval);
-                  parser_stack(yyansi_clval)=convert_character_literal(yytext, true);
-                  PARSER.set_source_location(parser_stack(yyansi_clval));
+                  source_locationt l=parser_stack(yyansi_clval).source_location();
+                  parser_stack(yyansi_clval)=convert_character_literal(yytext, true, l);
                   return TOK_CHARACTER;
                 }
 

src/cpp/cpp_typecheck.cpp

@@ -128,6 +128,12 @@ bool cpp_typecheck(
     cpp_typecheck.error() << e << messaget::eom;
   }
 
+  catch(const invalid_source_file_exceptiont &e)
+  {
+    cpp_typecheck.error().source_location = e.get_source_location();
+    cpp_typecheck.error() << e.get_reason() << messaget::eom;
+  }
+
   return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
 }
 

src/crangler/mini_c_parser.cpp

@@ -236,8 +236,12 @@ mini_c_parsert::tokenst mini_c_parsert::parse_pre_declarator()
     else if(token == '(') // function type, part of declarator
       return result;
     else
+    {
+      source_locationt loc;
+      loc.set_line(token.line_number);
       throw invalid_source_file_exceptiont(
-        "expected a declaration but got '" + token.text + "'");
+        "expected a declaration but got '" + token.text + "'", loc);
+    }
   }
 }
 
@@ -263,7 +267,11 @@ mini_c_parsert::tokenst mini_c_parsert::parse_declarator()
     return {consume_token()};
   }
   else
-    throw invalid_source_file_exceptiont("expected an identifier");
+  {
+    source_locationt loc;
+    loc.set_line(peek().line_number);
+    throw invalid_source_file_exceptiont("expected an identifier", loc);
+  }
 }
 
 mini_c_parsert::tokenst mini_c_parsert::parse_post_declarator()

src/goto-cc/goto_cc_mode.cpp

@@ -111,6 +111,15 @@ int goto_cc_modet::main(int argc, const char **argv)
     log.error() << "Out of memory" << messaget::eom;
     return EX_SOFTWARE;
   }
+
+  catch(const invalid_source_file_exceptiont &e)
+  {
+    messaget log{message_handler};
+    log.error().source_location = e.get_source_location();
+    log.error() << e.get_reason() << messaget::eom;
+    return EX_SOFTWARE;
+  }
+
   catch(const cprover_exception_baset &e)
   {
     messaget log{message_handler};

src/goto-programs/string_instrumentation.cpp

@@ -265,7 +265,7 @@ void string_instrumentationt::do_sprintf(
 {
   if(arguments.size()<2)
   {
-    throw incorrect_source_program_exceptiont(
+    throw invalid_source_file_exceptiont(
       "sprintf expected to have two or more arguments",
       target->source_location());
   }
@@ -301,7 +301,7 @@ void string_instrumentationt::do_snprintf(
 {
   if(arguments.size()<3)
   {
-    throw incorrect_source_program_exceptiont(
+    throw invalid_source_file_exceptiont(
       "snprintf expected to have three or more arguments",
       target->source_location());
   }
@@ -338,7 +338,7 @@ void string_instrumentationt::do_fscanf(
 {
   if(arguments.size()<2)
   {
-    throw incorrect_source_program_exceptiont(
+    throw invalid_source_file_exceptiont(
       "fscanf expected to have two or more arguments",
       target->source_location());
   }
@@ -614,7 +614,7 @@ void string_instrumentationt::do_strchr(
 {
   if(arguments.size()!=2)
   {
-    throw incorrect_source_program_exceptiont(
+    throw invalid_source_file_exceptiont(
       "strchr expected to have two arguments", target->source_location());
   }
 
@@ -638,7 +638,7 @@ void string_instrumentationt::do_strrchr(
 {
   if(arguments.size()!=2)
   {
-    throw incorrect_source_program_exceptiont(
+    throw invalid_source_file_exceptiont(
       "strrchr expected to have two arguments", target->source_location());
   }
 
@@ -662,7 +662,7 @@ void string_instrumentationt::do_strstr(
 {
   if(arguments.size()!=2)
   {
-    throw incorrect_source_program_exceptiont(
+    throw invalid_source_file_exceptiont(
       "strstr expected to have two arguments", target->source_location());
   }
 
@@ -692,7 +692,7 @@ void string_instrumentationt::do_strtok(
 {
   if(arguments.size()!=2)
   {
-    throw incorrect_source_program_exceptiont(
+    throw invalid_source_file_exceptiont(
       "strtok expected to have two arguments", target->source_location());
   }
 

src/goto-programs/string_instrumentation.h

@@ -12,33 +12,12 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
 #define CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
 
-#include <util/exception_utils.h>
-
 class exprt;
 class goto_functionst;
 class goto_modelt;
 class goto_programt;
 class symbol_tablet;
 
-class incorrect_source_program_exceptiont : public cprover_exception_baset
-{
-public:
-  incorrect_source_program_exceptiont(
-    std::string message,
-    source_locationt source_location)
-    : cprover_exception_baset(std::move(message)),
-      source_location(std::move(source_location))
-  {
-  }
-  std::string what() const override
-  {
-    return reason + " (at: " + source_location.as_string() + ")";
-  }
-
-private:
-  source_locationt source_location;
-};
-
 void string_instrumentation(
   symbol_tablet &,
   goto_programt &);

src/symtab2gb/symtab2gb_parse_options.cpp

@@ -77,14 +77,18 @@ static void run_symtab2gb(
     auto &symtab_file = symtab_files[ix];
     if(failed(symtab_language->parse(symtab_file, symtab_filename)))
     {
-      throw invalid_source_file_exceptiont{
-        "failed to parse symbol table from file '" + symtab_filename + "'"};
+      source_locationt source_location;
+      source_location.set_file(symtab_filename);
+      throw invalid_source_file_exceptiont{"failed to parse symbol table",
+                                           source_location};
     }
     symbol_tablet symtab{};
     if(failed(symtab_language->typecheck(symtab, "<unused>")))
     {
-      throw invalid_source_file_exceptiont{
-        "failed to typecheck symbol table from file '" + symtab_filename + "'"};
+      source_locationt source_location;
+      source_location.set_file(symtab_filename);
+      throw invalid_source_file_exceptiont{"failed to typecheck symbol table",
+                                           source_location};
     }
     config.set_from_symbol_table(symtab);
 

src/util/exception_utils.cpp

@@ -86,7 +86,14 @@ invalid_input_exceptiont::invalid_input_exceptiont(std::string reason)
 }
 
 invalid_source_file_exceptiont::invalid_source_file_exceptiont(
-  std::string reason)
-  : cprover_exception_baset(std::move(reason))
+  std::string reason,
+  source_locationt source_location)
+  : invalid_input_exceptiont(std::move(reason)),
+    source_location(std::move(source_location))
+{
+}
+
+std::string invalid_source_file_exceptiont::what() const
 {
+  return source_location.as_string() + ": " + reason;
 }