Skip to content

Commit e25524e

Browse files
committed
Language files: add support for a generic fallback provider
This adds a mechanism for asking languaget instances to produce functions they have not advertised. DeepTest currently uses it to supply stub function bodies (jbmc replaces the calls, but this results in a less-useful trace, as it lacks FUNCTION_CALL steps for stubbed functions).
1 parent 10d0042 commit e25524e

File tree

2 files changed

+38
-1
lines changed

2 files changed

+38
-1
lines changed

src/langapi/language.h

+16
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,22 @@ class languaget:public messaget
8686
const irep_idt &function_id, symbol_table_baset &symbol_table)
8787
{ }
8888

89+
/// Can this languaget instance provide a body for `function_id`, which no
90+
/// languaget instance has claimed to be able to provide?
91+
virtual bool can_convert_fallback_method(const irep_idt &function_id) const
92+
{
93+
return false;
94+
}
95+
96+
/// Populate the body of `function_id`, which no languaget instance has
97+
/// claimed to be able to provide.
98+
virtual bool convert_fallback_method(
99+
const irep_idt &function_id, symbol_table_baset &symbol_table)
100+
{
101+
PRECONDITION(can_convert_fallback_method(function_id));
102+
return false;
103+
}
104+
89105
/// Final adjustments, e.g. initializing stub functions and globals that
90106
/// were discovered during function loading
91107
virtual bool final(symbol_table_baset &symbol_table);

src/langapi/language_file.h

+22-1
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,9 @@ class language_filest:public messaget
7272
typedef std::map<irep_idt, language_filet *> lazy_method_mapt;
7373
lazy_method_mapt lazy_method_map;
7474

75+
typedef std::vector<language_filet *> fallback_method_providerst;
76+
fallback_method_providerst fallback_method_providers;
77+
7578
public:
7679
language_filet &add_file(const std::string &filename)
7780
{
@@ -126,11 +129,29 @@ class language_filest:public messaget
126129
lazy_method_mapt::iterator it=lazy_method_map.find(id);
127130
if(it!=lazy_method_map.end())
128131
it->second->convert_lazy_method(id, symbol_table);
132+
133+
for(const auto &file : file_map)
134+
{
135+
if(file.second.language->can_convert_fallback_method(id) &&
136+
file.second.language->convert_fallback_method(id, symbol_table))
137+
{
138+
return;
139+
}
140+
}
129141
}
130142

131143
bool can_convert_lazy_method(const irep_idt &id) const
132144
{
133-
return lazy_method_map.count(id) != 0;
145+
if(lazy_method_map.count(id) != 0)
146+
return true;
147+
148+
for(const auto &file : file_map)
149+
{
150+
if(file.second.language->can_convert_fallback_method(id))
151+
return true;
152+
}
153+
154+
return false;
134155
}
135156

136157
void clear()

0 commit comments

Comments
 (0)