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$

regression/cbmc/gcc_builtin_add_overflow/type-conflict.desc

@@ -1,6 +1,6 @@
 CORE
 type-conflict.c
 -DCONFLICT1
-line 12 function main: __builtin_add_overflow has signature __builtin_add_overflow\(integral, integral, integral\*\), but argument 3 \(r\) has type `signed int`$
+line 12 function main: error: __builtin_add_overflow has signature __builtin_add_overflow\(integral, integral, integral\*\), but argument 3 \(r\) has type `signed int`$
 ^EXIT=6$
 ^SIGNAL=0$

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

@@ -3171,21 +3171,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
     {
@@ -3238,9 +3239,9 @@ exprt c_typecheck_baset::do_special_functions(
     if(expr.arguments().size() != 1)
     {
       std::ostringstream error_message;
-      error_message << expr.source_location().as_string()
-                    << ": error: " << identifier << " expects one operand";
-      throw invalid_source_file_exceptiont{error_message.str()};
+      error_message << "error: " << identifier << " expects one operand";
+      throw invalid_source_file_exceptiont{
+        error_message.str(), expr.source_location()};
     }
 
     typecheck_function_call_arguments(expr);
@@ -3265,10 +3266,10 @@ exprt c_typecheck_baset::typecheck_builtin_overflow(
   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);
@@ -3284,14 +3285,14 @@ exprt c_typecheck_baset::typecheck_builtin_overflow(
       [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
-                      << "(integral, integral, integral" << (_p ? "" : "*")
-                      << "), "
+        error_message << "error: " << 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)
     {
@@ -3327,10 +3328,10 @@ exprt c_typecheck_baset::typecheck_saturating_arithmetic(
   if(expr.arguments().size() != 2)
   {
     std::ostringstream error_message;
-    error_message << expr.source_location().as_string() << ": " << identifier
-                  << " takes exactly two arguments, but "
+    error_message << identifier << " takes exactly two 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()};
   }
 
   exprt result;

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

@@ -129,6 +129,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

@@ -266,7 +266,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());
   }
@@ -302,7 +302,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());
   }
@@ -339,7 +339,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());
   }
@@ -615,7 +615,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());
   }
 
@@ -639,7 +639,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());
   }
 
@@ -663,7 +663,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());
   }
 
@@ -693,7 +693,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)))
     {
+      source_locationt source_location;
+      source_location.set_file(symtab_filename);
       throw invalid_source_file_exceptiont{
-        "failed to parse symbol table from file '" + symtab_filename + "'"};
+        "failed to parse symbol table", source_location};
     }
     symbol_tablet symtab{};
     if(failed(symtab_language->typecheck(symtab, "<unused>")))
     {
+      source_locationt source_location;
+      source_location.set_file(symtab_filename);
       throw invalid_source_file_exceptiont{
-        "failed to typecheck symbol table from file '" + symtab_filename + "'"};
+        "failed to typecheck symbol table", source_location};
     }
     config.set_from_symbol_table(symtab);