Merge pull request #5837 from tautschnig/c-no-structured-throws

tautschnig · web-flow · commit d8f3d498e9a4 · 2022-06-30T11:30:15.000+02:00
Add source location to invalid_source_file_exceptiont
diff --git a/regression/ansi-c/character_literals1/unsupported-wide.desc b/regression/ansi-c/character_literals1/unsupported-wide.desc
@@ -0,0 +1,11 @@
+CORE
+unsupported.c
+-DWIDE
+wide literals with 5 characters are not supported$
+^EXIT=70$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed$
+--
+Test to confirm that an actionable error message is provided.
diff --git a/regression/ansi-c/character_literals1/unsupported.c b/regression/ansi-c/character_literals1/unsupported.c
@@ -0,0 +1,8 @@
+int main()
+{
+#ifndef WIDE
+  'abcde';
+#else
+  (void)L'abcde';
+#endif
+}
diff --git a/regression/ansi-c/character_literals1/unsupported.desc b/regression/ansi-c/character_literals1/unsupported.desc
@@ -0,0 +1,11 @@
+CORE
+unsupported.c
+
+literals with 5 characters are not supported$
+^EXIT=70$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed$
+--
+Test to confirm that an actionable error message is provided.
diff --git a/regression/ansi-c/enum_is_in_range/enum_test10.desc b/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$
diff --git a/regression/ansi-c/enum_is_in_range/enum_test12.desc b/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$
diff --git a/regression/cbmc/gcc_builtin_add_overflow/type-conflict.desc b/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$
diff --git a/regression/cbmc/saturating_arithmetric/typeconflict.c b/regression/cbmc/saturating_arithmetric/typeconflict.c
@@ -0,0 +1,4 @@
+int main()
+{
+  __CPROVER_saturating_minus(1);
+}
diff --git a/regression/cbmc/saturating_arithmetric/typeconflict.desc b/regression/cbmc/saturating_arithmetric/typeconflict.desc
@@ -0,0 +1,7 @@
+CORE
+typeconflict.c
+file typeconflict.c line 3 function main: error: __CPROVER_saturating_minus takes exactly two arguments, but 1 were provided
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/ansi_c_typecheck.cpp b/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;
 }
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -3170,21 +3170,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
     {
@@ -3237,9 +3238,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);
@@ -3264,10 +3265,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);
@@ -3283,14 +3284,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)
     {
@@ -3326,10 +3327,11 @@ exprt c_typecheck_baset::typecheck_saturating_arithmetic(
   if(expr.arguments().size() != 2)
   {
     std::ostringstream error_message;
-    error_message << expr.source_location().as_string() << ": " << identifier
+    error_message << "error: " << 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;
diff --git a/src/ansi-c/c_typecheck_type.cpp b/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
diff --git a/src/ansi-c/literals/convert_character_literal.cpp b/src/ansi-c/literals/convert_character_literal.cpp
@@ -20,7 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 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;
 }
diff --git a/src/ansi-c/literals/convert_character_literal.h b/src/ansi-c/literals/convert_character_literal.h
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 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
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
@@ -307,9 +307,9 @@ 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));
+                  loc();
+                  source_locationt l=parser_stack(yyansi_clval).source_location();
+                  parser_stack(yyansi_clval)=convert_character_literal(yytext, true, l);
                   return TOK_CHARACTER;
                 }
 
diff --git a/src/cpp/cpp_typecheck.cpp b/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;
 }
 
diff --git a/src/crangler/mini_c_parser.cpp b/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()
diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp
@@ -114,6 +114,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};
diff --git a/src/goto-programs/string_instrumentation.cpp b/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());
   }
 
diff --git a/src/goto-programs/string_instrumentation.h b/src/goto-programs/string_instrumentation.h
diff --git a/src/symtab2gb/symtab2gb_parse_options.cpp b/src/symtab2gb/symtab2gb_parse_options.cpp
diff --git a/src/util/exception_utils.cpp b/src/util/exception_utils.cpp
diff --git a/src/util/exception_utils.h b/src/util/exception_utils.h
diff --git a/src/util/typecheck.cpp b/src/util/typecheck.cpp

-Original file line number
+Diff line change
@@ @@ -0,0 +1,4 @@ @@
 +int main()
 +{
 +  __CPROVER_saturating_minus(1);
 +}
Original file line number	Diff line number	Diff line change
`@@ -67,5 +67,11 @@ bool ansi_c_typecheck(`
`67`	`67`	`ansi_c_typecheck.error() << e << messaget::eom;`
`68`	`68`	`}`
`69`	`69`
	`70`	`+ catch(const invalid_source_file_exceptiont &e)`
	`71`	`+ {`
	`72`	`+ ansi_c_typecheck.error().source_location = e.get_source_location();`
	`73`	`+ ansi_c_typecheck.error() << e.get_reason() << messaget::eom;`
	`74`	`+ }`
	`75`	`+`
`70`	`76`	`return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;`
`71`	`77`	`}`