Skip to content

Commit 37a2317

Browse files
Factor out language_infot from languaget
Previously, using language-specific methods such as from_expr() required creating a new languaget instance which could be potentially costly. This commit introduces a language_infot class that offers language-specific methods that don't require parsing functionality. language_infot is now used for language registration (instead of language_entryt). The immutable registered *_language_infot instances are shared among the corresponding *_languaget instances that are requested by the get_language_from_* functions.
1 parent 88db26f commit 37a2317

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

56 files changed

+829
-571
lines changed

src/analyses/goto_check.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -1275,7 +1275,8 @@ void goto_checkt::add_guarded_claim(
12751275
goto_programt::targett t=new_code.add_instruction(type);
12761276

12771277
std::string source_expr_string;
1278-
get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
1278+
get_language_from_mode(mode)->info.from_expr(
1279+
src_expr, source_expr_string, ns);
12791280

12801281
t->guard.swap(new_expr);
12811282
t->source_location=source_location;

src/ansi-c/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ SRC = anonymous_member.cpp \
44
ansi_c_entry_point.cpp \
55
ansi_c_internal_additions.cpp \
66
ansi_c_language.cpp \
7+
ansi_c_language_info.cpp \
78
ansi_c_lex.yy.cpp \
89
ansi_c_parse_tree.cpp \
910
ansi_c_parser.cpp \

src/ansi-c/ansi_c_language.cpp

+2-36
Original file line numberDiff line numberDiff line change
@@ -21,15 +21,8 @@ Author: Daniel Kroening, [email protected]
2121
#include "ansi_c_entry_point.h"
2222
#include "ansi_c_typecheck.h"
2323
#include "ansi_c_parser.h"
24-
#include "expr2c.h"
2524
#include "c_preprocess.h"
2625
#include "ansi_c_internal_additions.h"
27-
#include "type2name.h"
28-
29-
std::set<std::string> ansi_c_languaget::extensions() const
30-
{
31-
return { "c", "i" };
32-
}
3326

3427
void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
3528
{
@@ -144,36 +137,9 @@ void ansi_c_languaget::show_parse(std::ostream &out)
144137
parse_tree.output(out);
145138
}
146139

147-
std::unique_ptr<languaget> new_ansi_c_language()
148-
{
149-
return util_make_unique<ansi_c_languaget>();
150-
}
151-
152-
bool ansi_c_languaget::from_expr(
153-
const exprt &expr,
154-
std::string &code,
155-
const namespacet &ns)
156-
{
157-
code=expr2c(expr, ns);
158-
return false;
159-
}
160-
161-
bool ansi_c_languaget::from_type(
162-
const typet &type,
163-
std::string &code,
164-
const namespacet &ns)
140+
std::unique_ptr<languaget> new_ansi_c_language(const language_infot &info)
165141
{
166-
code=type2c(type, ns);
167-
return false;
168-
}
169-
170-
bool ansi_c_languaget::type_to_name(
171-
const typet &type,
172-
std::string &name,
173-
const namespacet &ns)
174-
{
175-
name=type2name(type, ns);
176-
return false;
142+
return std::unique_ptr<ansi_c_languaget>(new ansi_c_languaget(info));
177143
}
178144

179145
bool ansi_c_languaget::to_expr(

src/ansi-c/ansi_c_language.h

+4-24
Original file line numberDiff line numberDiff line change
@@ -39,44 +39,24 @@ class ansi_c_languaget:public languaget
3939

4040
void show_parse(std::ostream &out) override;
4141

42+
explicit ansi_c_languaget(const language_infot &info) : languaget(info)
43+
{
44+
}
4245
~ansi_c_languaget() override;
43-
ansi_c_languaget() { }
44-
45-
bool from_expr(
46-
const exprt &expr,
47-
std::string &code,
48-
const namespacet &ns) override;
49-
50-
bool from_type(
51-
const typet &type,
52-
std::string &code,
53-
const namespacet &ns) override;
54-
55-
bool type_to_name(
56-
const typet &type,
57-
std::string &name,
58-
const namespacet &ns) override;
5946

6047
bool to_expr(
6148
const std::string &code,
6249
const std::string &module,
6350
exprt &expr,
6451
const namespacet &ns) override;
6552

66-
std::unique_ptr<languaget> new_language() override
67-
{ return util_make_unique<ansi_c_languaget>(); }
68-
69-
std::string id() const override { return "C"; }
70-
std::string description() const override { return "ANSI-C 99"; }
71-
std::set<std::string> extensions() const override;
72-
7353
void modules_provided(std::set<std::string> &modules) override;
7454

7555
protected:
7656
ansi_c_parse_treet parse_tree;
7757
std::string parse_path;
7858
};
7959

80-
std::unique_ptr<languaget> new_ansi_c_language();
60+
std::unique_ptr<languaget> new_ansi_c_language(const language_infot &info);
8161

8262
#endif // CPROVER_ANSI_C_ANSI_C_LANGUAGE_H

src/ansi-c/ansi_c_language_info.cpp

+52
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "ansi_c_language_info.h"
10+
11+
#include "expr2c.h"
12+
#include "type2name.h"
13+
14+
#include "ansi_c_language.h"
15+
16+
std::set<std::string> ansi_c_language_infot::extensions() const
17+
{
18+
return {"c", "i"};
19+
}
20+
21+
bool ansi_c_language_infot::from_expr(
22+
const exprt &expr,
23+
std::string &code,
24+
const namespacet &ns) const
25+
{
26+
code = expr2c(expr, ns);
27+
return false;
28+
}
29+
30+
bool ansi_c_language_infot::from_type(
31+
const typet &type,
32+
std::string &code,
33+
const namespacet &ns) const
34+
{
35+
code = type2c(type, ns);
36+
return false;
37+
}
38+
39+
bool ansi_c_language_infot::type_to_name(
40+
const typet &type,
41+
std::string &name,
42+
const namespacet &ns) const
43+
{
44+
name = type2name(type, ns);
45+
return false;
46+
}
47+
48+
std::unique_ptr<language_infot> new_ansi_c_language_info()
49+
{
50+
return std::unique_ptr<language_infot>(
51+
new ansi_c_language_infot(new_ansi_c_language));
52+
}

src/ansi-c/ansi_c_language_info.h

+48
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_ANSI_C_ANSI_C_LANGUAGE_INFO_H
10+
#define CPROVER_ANSI_C_ANSI_C_LANGUAGE_INFO_H
11+
12+
#include <memory>
13+
14+
#include <langapi/language_info.h>
15+
16+
class ansi_c_language_infot : public language_infot
17+
{
18+
public:
19+
explicit ansi_c_language_infot(language_factoryt _factory)
20+
: language_infot(_factory)
21+
{
22+
}
23+
24+
irep_idt id() const override
25+
{
26+
return ID_C;
27+
}
28+
29+
std::string description() const override
30+
{
31+
return "C";
32+
}
33+
34+
std::set<std::string> extensions() const override;
35+
36+
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
37+
const override;
38+
39+
bool from_type(const typet &type, std::string &code, const namespacet &ns)
40+
const override;
41+
42+
bool type_to_name(const typet &type, std::string &name, const namespacet &ns)
43+
const override;
44+
};
45+
46+
std::unique_ptr<language_infot> new_ansi_c_language_info();
47+
48+
#endif // CPROVER_ANSI_C_ANSI_C_LANGUAGE_INFO_H

src/ansi-c/cprover_library.cpp

+6-4
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include <sstream>
1212

13+
#include <langapi/mode.h>
14+
1315
#include <util/config.h>
1416

1517
#include "ansi_c_language.h"
@@ -88,9 +90,9 @@ void add_library(
8890

8991
std::istringstream in(src);
9092

91-
ansi_c_languaget ansi_c_language;
92-
ansi_c_language.set_message_handler(message_handler);
93-
ansi_c_language.parse(in, "");
93+
auto ansi_c_language = get_language_from_mode(ID_C);
94+
ansi_c_language->set_message_handler(message_handler);
95+
ansi_c_language->parse(in, "");
9496

95-
ansi_c_language.typecheck(symbol_table, "<built-in-library>");
97+
ansi_c_language->typecheck(symbol_table, "<built-in-library>");
9698
}

src/cbmc/cbmc_languages.cpp

+6-6
Original file line numberDiff line numberDiff line change
@@ -13,19 +13,19 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <langapi/mode.h>
1515

16-
#include <ansi-c/ansi_c_language.h>
17-
#include <cpp/cpp_language.h>
16+
#include <ansi-c/ansi_c_language_info.h>
17+
#include <cpp/cpp_language_info.h>
1818

1919
#ifdef HAVE_JSIL
20-
#include <jsil/jsil_language.h>
20+
#include <jsil/jsil_language_info.h>
2121
#endif
2222

2323
void cbmc_parse_optionst::register_languages()
2424
{
25-
register_language(new_ansi_c_language);
26-
register_language(new_cpp_language);
25+
register_language(new_ansi_c_language_info);
26+
register_language(new_cpp_language_info);
2727

2828
#ifdef HAVE_JSIL
29-
register_language(new_jsil_language);
29+
register_language(new_jsil_language_info);
3030
#endif
3131
}

src/clobber/clobber_parse_options.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,8 @@ Author: Daniel Kroening, [email protected]
2020
#include <util/options.h>
2121
#include <util/memory_info.h>
2222

23-
#include <ansi-c/ansi_c_language.h>
24-
#include <cpp/cpp_language.h>
23+
#include <ansi-c/ansi_c_language_info.h>
24+
#include <cpp/cpp_language_info.h>
2525

2626
#include <goto-programs/initialize_goto_model.h>
2727
#include <goto-programs/show_properties.h>
@@ -107,8 +107,8 @@ int clobber_parse_optionst::doit()
107107
return 0;
108108
}
109109

110-
register_language(new_ansi_c_language);
111-
register_language(new_cpp_language);
110+
register_language(new_ansi_c_language_info);
111+
register_language(new_cpp_language_info);
112112

113113
//
114114
// command line options

src/cpp/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ SRC = cpp_constructor.cpp \
1111
cpp_internal_additions.cpp \
1212
cpp_is_pod.cpp \
1313
cpp_language.cpp \
14+
cpp_language_info.cpp \
1415
cpp_name.cpp \
1516
cpp_namespace_spec.cpp \
1617
cpp_parse_tree.cpp \

src/cpp/cpp_language.cpp

+2-47
Original file line numberDiff line numberDiff line change
@@ -30,24 +30,6 @@ Author: Daniel Kroening, [email protected]
3030
#include "cpp_typecheck.h"
3131
#include "cpp_type2name.h"
3232

33-
std::set<std::string> cpp_languaget::extensions() const
34-
{
35-
std::set<std::string> s;
36-
37-
s.insert("cpp");
38-
s.insert("CPP");
39-
s.insert("cc");
40-
s.insert("c++");
41-
s.insert("ii");
42-
s.insert("cxx");
43-
44-
#ifndef _WIN32
45-
s.insert("C");
46-
#endif
47-
48-
return s;
49-
}
50-
5133
void cpp_languaget::modules_provided(std::set<std::string> &modules)
5234
{
5335
modules.insert(get_base_name(parse_path, true));
@@ -203,36 +185,9 @@ void cpp_languaget::show_parse(
203185
out << "UNKNOWN: " << item.pretty() << '\n';
204186
}
205187

206-
std::unique_ptr<languaget> new_cpp_language()
207-
{
208-
return util_make_unique<cpp_languaget>();
209-
}
210-
211-
bool cpp_languaget::from_expr(
212-
const exprt &expr,
213-
std::string &code,
214-
const namespacet &ns)
215-
{
216-
code=expr2cpp(expr, ns);
217-
return false;
218-
}
219-
220-
bool cpp_languaget::from_type(
221-
const typet &type,
222-
std::string &code,
223-
const namespacet &ns)
224-
{
225-
code=type2cpp(type, ns);
226-
return false;
227-
}
228-
229-
bool cpp_languaget::type_to_name(
230-
const typet &type,
231-
std::string &name,
232-
const namespacet &ns)
188+
std::unique_ptr<languaget> new_cpp_language(const language_infot &info)
233189
{
234-
name=cpp_type2name(type);
235-
return false;
190+
return std::unique_ptr<cpp_languaget>(new cpp_languaget(info));
236191
}
237192

238193
bool cpp_languaget::to_expr(

0 commit comments

Comments
 (0)