cpp_parsert: construct with message handler

src/ansi-c/ansi_c_internal_additions.cpp

@@ -158,7 +158,9 @@ max_malloc_size(std::size_t pointer_width, std::size_t object_bits)
   return ((mp_integer)1) << (mp_integer)bits_for_positive_offset;
 }
 
-void ansi_c_internal_additions(std::string &code)
+void ansi_c_internal_additions(
+  std::string &code,
+  bool support_ts_18661_3_Floatn_types)
 {
   // clang-format off
   // do the built-in types and variables
@@ -247,9 +249,7 @@ void ansi_c_internal_additions(std::string &code)
     config.ansi_c.mode == configt::ansi_ct::flavourt::ARM)
   {
     code+=gcc_builtin_headers_types;
-    // check the parser and not config.ansi_c.ts_18661_3_Floatn_types to adjust
-    // behaviour depending on C or C++ context
-    if(ansi_c_parser.ts_18661_3_Floatn_types)
+    if(support_ts_18661_3_Floatn_types)
       code += gcc_builtin_headers_types_gcc7plus;
 
     // there are many more, e.g., look at

src/ansi-c/ansi_c_internal_additions.h

@@ -12,7 +12,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <string>
 
-void ansi_c_internal_additions(std::string &code);
+void ansi_c_internal_additions(
+  std::string &code,
+  bool support_ts_18661_3_Floatn_types);
 void ansi_c_architecture_strings(std::string &code);
 
 extern const char clang_builtin_headers[];

src/ansi-c/ansi_c_language.cpp

@@ -68,20 +68,19 @@ bool ansi_c_languaget::parse(
   // parsing
 
   std::string code;
-  ansi_c_internal_additions(code);
+  ansi_c_internal_additions(code, config.ansi_c.ts_18661_3_Floatn_types);
   std::istringstream codestr(code);
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=&codestr;
-  ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   ansi_c_parser.cpp98=false; // it's not C++
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
 
-  ansi_c_scanner_init();
+  ansi_c_scanner_init(ansi_c_parser);
 
   bool result=ansi_c_parser.parse();
 
@@ -90,7 +89,7 @@ bool ansi_c_languaget::parse(
     ansi_c_parser.set_line_no(0);
     ansi_c_parser.set_file(path);
     ansi_c_parser.in=&i_preprocessed;
-    ansi_c_scanner_init();
+    ansi_c_scanner_init(ansi_c_parser);
     result=ansi_c_parser.parse();
   }
 
@@ -197,13 +196,12 @@ bool ansi_c_languaget::to_expr(
 
   // parsing
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_file(irep_idt());
   ansi_c_parser.in=&i_preprocessed;
-  ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.mode=config.ansi_c.mode;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
-  ansi_c_scanner_init();
+  ansi_c_scanner_init(ansi_c_parser);
 
   bool result=ansi_c_parser.parse();
 

src/ansi-c/ansi_c_parser.cpp

@@ -10,8 +10,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_storage_spec.h"
 
-ansi_c_parsert ansi_c_parser;
-
 ansi_c_id_classt ansi_c_parsert::lookup(
   const irep_idt &base_name,
   irep_idt &identifier, // output
@@ -73,14 +71,6 @@ void ansi_c_parsert::add_tag_with_body(irept &tag)
   }
 }
 
-extern char *yyansi_ctext;
-
-int yyansi_cerror(const std::string &error)
-{
-  ansi_c_parser.parse_error(error, yyansi_ctext);
-  return 0;
-}
-
 void ansi_c_parsert::add_declarator(
   exprt &declaration,
   irept &declarator)

src/ansi-c/ansi_c_parser.h

@@ -18,15 +18,17 @@ Author: Daniel Kroening, [email protected]
 #include "ansi_c_parse_tree.h"
 #include "ansi_c_scope.h"
 
-int yyansi_cparse();
+class ansi_c_parsert;
+int yyansi_cparse(ansi_c_parsert &);
 
 class ansi_c_parsert:public parsert
 {
 public:
   ansi_c_parse_treet parse_tree;
 
-  ansi_c_parsert()
-    : tag_following(false),
+  explicit ansi_c_parsert(message_handlert &message_handler)
+    : parsert(message_handler),
+      tag_following(false),
       asm_block_following(false),
       parenthesis_counter(0),
       mode(modet::NONE),
@@ -35,11 +37,14 @@ class ansi_c_parsert:public parsert
       for_has_scope(false),
       ts_18661_3_Floatn_types(false)
   {
+    // set up global scope
+    scopes.clear();
+    scopes.push_back(scopet());
   }
 
   virtual bool parse() override
   {
-    return yyansi_cparse()!=0;
+    return yyansi_cparse(*this) != 0;
   }
 
   virtual void clear() override
@@ -166,9 +171,6 @@ class ansi_c_parsert:public parsert
   std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
 };
 
-extern ansi_c_parsert ansi_c_parser;
-
-int yyansi_cerror(const std::string &error);
-void ansi_c_scanner_init();
+void ansi_c_scanner_init(ansi_c_parsert &);
 
 #endif // CPROVER_ANSI_C_ANSI_C_PARSER_H

src/ansi-c/builtin_factory.cpp

@@ -47,16 +47,15 @@ static bool convert(
 {
   std::istringstream in(s.str());
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=∈
-  ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.cpp98=false; // it's not C++
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
 
-  ansi_c_scanner_init();
+  ansi_c_scanner_init(ansi_c_parser);
 
   if(ansi_c_parser.parse())
     return true;
@@ -97,6 +96,7 @@ static bool convert(
 //! \return 'true' on error
 bool builtin_factory(
   const irep_idt &identifier,
+  bool support_ts_18661_3_Floatn_types,
   symbol_table_baset &symbol_table,
   message_handlert &mh)
 {
@@ -106,7 +106,7 @@ bool builtin_factory(
   std::ostringstream s;
 
   std::string code;
-  ansi_c_internal_additions(code);
+  ansi_c_internal_additions(code, support_ts_18661_3_Floatn_types);
   s << code;
 
   // our own extensions

src/ansi-c/builtin_factory.h

@@ -17,6 +17,7 @@ class symbol_table_baset;
 //! \return 'true' in case of error
 bool builtin_factory(
   const irep_idt &identifier,
+  bool support_ts_18661_3_Floatn_types,
   symbol_table_baset &,
   message_handlert &);
 

src/ansi-c/c_typecheck_base.h

@@ -250,6 +250,8 @@ class c_typecheck_baset:
 
   virtual bool gcc_types_compatible_p(const typet &, const typet &);
 
+  virtual bool builtin_factory(const irep_idt &);
+
   // types
   virtual void typecheck_type(typet &type);
   virtual void typecheck_compound_type(struct_union_typet &type);

src/ansi-c/c_typecheck_expr.cpp

@@ -2072,6 +2072,15 @@ void c_typecheck_baset::typecheck_obeys_contract_call(
   expr.type() = bool_typet();
 }
 
+bool c_typecheck_baset::builtin_factory(const irep_idt &identifier)
+{
+  return ::builtin_factory(
+    identifier,
+    config.ansi_c.ts_18661_3_Floatn_types,
+    symbol_table,
+    get_message_handler());
+}
+
 void c_typecheck_baset::typecheck_side_effect_function_call(
   side_effect_expr_function_callt &expr)
 {
@@ -2106,7 +2115,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
         typecheck_typed_target_call(expr);
       }
       // Is this a builtin?
-      else if(!builtin_factory(identifier, symbol_table, get_message_handler()))
+      else if(!builtin_factory(identifier))
       {
         // yes, it's a builtin
       }

src/ansi-c/parser.y

@@ -13,13 +13,27 @@
 #ifdef ANSI_C_DEBUG
 #define YYDEBUG 1
 #endif
-#define PARSER ansi_c_parser
+#define PARSER (*ansi_c_parser)
 
 #include "ansi_c_parser.h"
 
 int yyansi_clex();
 extern char *yyansi_ctext;
 
+static ansi_c_parsert *ansi_c_parser;
+int yyansi_cparse(void);
+int yyansi_cparse(ansi_c_parsert &_ansi_c_parser)
+{
+  ansi_c_parser = &_ansi_c_parser;
+  return yyansi_cparse();
+}
+
+int yyansi_cerror(const std::string &error)
+{
+  ansi_c_parser->parse_error(error, yyansi_ctext);
+  return 0;
+}
+
 #include "parser_static.inc"
 
 #include "literals/convert_integer_literal.h"

src/ansi-c/scanner.l

@@ -38,7 +38,7 @@ static int isatty(int) { return 0; }
 #include "literals/convert_string_literal.h"
 #include "literals/unescape_string.h"
 
-#define PARSER ansi_c_parser
+#define PARSER (*ansi_c_parser)
 #define YYSTYPE unsigned
 #undef  ECHO
 #define ECHO
@@ -49,6 +49,19 @@ static int isatty(int) { return 0; }
 extern int yyansi_cdebug;
 #endif
 
+static ansi_c_parsert *ansi_c_parser;
+void ansi_c_scanner_init(ansi_c_parsert &_ansi_c_parser)
+{
+#ifdef ANSI_C_DEBUG
+  yyansi_cdebug=1;
+#endif
+  ansi_c_parser = &_ansi_c_parser;
+  YY_FLUSH_BUFFER;
+  BEGIN(0);
+}
+
+int yyansi_cerror(const std::string &error);
+
 #define loc() \
   { newstack(yyansi_clval); PARSER.set_source_location(parser_stack(yyansi_clval)); }
 
@@ -264,17 +277,6 @@ enable_or_disable ("enable"|"disable")
 %x CPROVER_PRAGMA
 %x OTHER_PRAGMA
 
-%{
-void ansi_c_scanner_init()
-{
-#ifdef ANSI_C_DEBUG
-  yyansi_cdebug=1;
-#endif
-  YY_FLUSH_BUFFER;
-  BEGIN(0);
-}
-%}
-
 %%
 
 <INITIAL>.|\n   { BEGIN(GRAMMAR);

src/cpp/cpp_language.cpp

@@ -102,11 +102,9 @@ bool cpp_languaget::parse(
   std::istringstream i_preprocessed(o_preprocessed.str());
 
   // parsing
-
-  cpp_parser.clear();
+  cpp_parsert cpp_parser{message_handler};
   cpp_parser.set_file(path);
   cpp_parser.in=&i_preprocessed;
-  cpp_parser.log.set_message_handler(message_handler);
   cpp_parser.mode=config.ansi_c.mode;
 
   bool result=cpp_parser.parse();
@@ -245,11 +243,9 @@ bool cpp_languaget::to_expr(
   std::istringstream i_preprocessed(code);
 
   // parsing
-
-  cpp_parser.clear();
+  cpp_parsert cpp_parser{message_handler};
   cpp_parser.set_file(irep_idt());
   cpp_parser.in=&i_preprocessed;
-  cpp_parser.log.set_message_handler(message_handler);
 
   bool result=cpp_parser.parse();
 

src/cpp/cpp_parser.cpp

@@ -11,25 +11,12 @@ Author: Daniel Kroening, [email protected]
 
 #include "cpp_parser.h"
 
-#include <util/config.h>
-
-cpp_parsert cpp_parser;
-
-bool cpp_parse();
+bool cpp_parse(cpp_parsert &, message_handlert &);
 
 bool cpp_parsert::parse()
 {
-  // We use the ANSI-C scanner
-  ansi_c_parser.cpp98=true;
-  ansi_c_parser.cpp11 =
-    config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP11 ||
-    config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP14 ||
-    config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17;
-  ansi_c_parser.ts_18661_3_Floatn_types=false;
-  ansi_c_parser.in=in;
-  ansi_c_parser.mode=mode;
-  ansi_c_parser.set_file(get_file());
-  ansi_c_parser.log.set_message_handler(log.get_message_handler());
-
-  return cpp_parse();
+  token_buffer.ansi_c_parser.in = in;
+  token_buffer.ansi_c_parser.mode = mode;
+  token_buffer.ansi_c_parser.set_file(get_file());
+  return cpp_parse(*this, log.get_message_handler());
 }

src/cpp/cpp_parser.h

@@ -34,10 +34,12 @@ class cpp_parsert:public parsert
     asm_block_following=false;
   }
 
-  cpp_parsert():
-    mode(configt::ansi_ct::flavourt::ANSI),
-    recognize_wchar_t(true),
-    asm_block_following(false)
+  explicit cpp_parsert(message_handlert &message_handler)
+    : parsert(message_handler),
+      mode(configt::ansi_ct::flavourt::ANSI),
+      recognize_wchar_t(true),
+      token_buffer(message_handler),
+      asm_block_following(false)
   {
   }
 
@@ -67,6 +69,4 @@ class cpp_parsert:public parsert
   bool asm_block_following;
 };
 
-extern cpp_parsert cpp_parser;
-
 #endif // CPROVER_CPP_CPP_PARSER_H

src/cpp/cpp_token_buffer.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "cpp_token_buffer.h"
 
-#include <ansi-c/ansi_c_parser.h>
-
 int cpp_token_buffert::LookAhead(unsigned offset)
 {
   PRECONDITION(current_pos <= token_vector.size());