34#include <unordered_map>
60 std::string _loop_type,
61 std::string _identifier,
74 assertiont(std::string _identifier, std::string _content)
90 using functionst = std::list<std::pair<std::regex, functiont>>;
98 using objectst = std::list<std::pair<std::regex, objectt>>;
112 auto sources =
config[
"sources"];
114 if(!sources.is_null())
116 if(!sources.is_array())
121 if(!source.is_string())
137 if(!include.is_string())
140 this->
includes.push_back(include.value);
153 if(!define.is_string())
156 this->
defines.push_back(define.value);
173 if(!function.is_object())
178 const auto function_name = function_entry.first;
179 const auto &items = function_entry.second;
181 if(!items.is_array())
191 if(!function_item.is_string())
194 auto item_string = function_item.value;
200 split[0] ==
"ensures" || split[0] ==
"requires" ||
201 split[0] ==
"assigns")
203 std::ostringstream rest;
204 join_strings(rest, split.begin() + 1, split.end(),
' ');
206 function_config.
contract.emplace_back(split[0], rest.str());
208 else if(split[0] ==
"assert" && split.size() >= 3)
210 std::ostringstream rest;
211 join_strings(rest, split.begin() + 2, split.end(),
' ');
213 function_config.
assertions.emplace_back(split[1], rest.str());
216 (split[0] ==
"for" && split.size() >= 3 && split[2] ==
"invariant") ||
217 (split[0] ==
"while" && split.size() >= 3 && split[2] ==
"invariant"))
219 std::ostringstream rest;
220 join_strings(rest, split.begin() + 3, split.end(),
' ');
223 split[0], split[1], rest.str());
225 else if(split[0] ==
"stub")
227 std::ostringstream rest;
228 join_strings(rest, split.begin() + 1, split.end(),
' ');
230 function_config.
stub = rest.str();
232 else if(split[0] ==
"remove")
234 if(split.size() == 1)
237 if(split[1] ==
"static")
241 "unexpected remove entry " + split[1]);
245 "unexpected function entry " + split[0]);
263 if(!
object.is_object())
268 const auto &object_name = object_entry.first;
269 const auto &items = object_entry.second;
271 if(!items.is_array())
280 if(!object_item.is_string())
283 auto item_string = object_item.value;
288 if(split[0] ==
"remove")
290 if(split.size() == 1)
293 if(split[1] ==
"static")
297 "unexpected remove entry " + split[1]);
301 "unexpected object entry " + split[0]);
323 std::vector<std::string> argv = {
"cc",
"-E", source_file};
325 for(
const auto &include :
c_wrangler.includes)
327 argv.push_back(
"-I");
328 argv.push_back(include);
332 argv.push_back(std::string(
"-D") + define);
334 std::ostringstream result;
336 auto run_result =
run(
"cc", argv,
"", result,
"");
346 std::vector<std::string> argv = {
"cc",
"-E",
"-dM", source_file};
348 for(
const auto &include :
config.includes)
350 argv.push_back(
"-I");
351 argv.push_back(include);
354 std::ostringstream result;
356 auto run_result =
run(
"cc", argv,
"", result,
"");
361 defines.
parse(result.str());
371 if(function_config.
stub.has_value())
374 out << function_config.
stub.value();
382 if(t.text ==
"static")
385 out << std::string(6,
' ');
402 for(
const auto &entry : function_config.
contract)
404 << defines(entry.content) <<
')';
406 std::map<std::string, std::string> loop_invariants;
409 loop_invariants[entry.loop_type + entry.identifier] = entry.content;
411 if(loop_invariants.empty())
418 std::size_t for_count = 0, while_count = 0;
423 const auto &token = *(t++);
429 const auto &invariant =
430 loop_invariants[
"while" + std::to_string(while_count)];
432 if(!invariant.empty())
435 for(; t != t_end; t++)
438 << defines(invariant) <<
')';
441 else if(token ==
"for")
444 const auto &invariant =
445 loop_invariants[
"for" + std::to_string(for_count)];
447 if(!invariant.empty())
450 for(; t != t_end; t++)
452 out <<
' ' <<
CPROVER_PREFIX <<
"invariant(" << defines(invariant)
471 if(t.text ==
"static")
474 out << std::string(6,
' ');
504 for(
const auto &entry :
config.functions)
506 if(std::regex_match(name_opt->text, entry.first))
515 else if(!declaration.
is_function() && name_opt.has_value())
517 for(
const auto &entry :
config.objects)
519 if(std::regex_match(name_opt->text, entry.first))
534 const std::string &in,
538 std::ostringstream out;
539 std::istringstream in_str(in);
543 for(
const auto &declaration : parsed)
558 for(
auto &source_file :
c_wrangler.source_files)
572 std::cout << mangled;
static void mangle_function(const c_declarationt &declaration, const c_definest &defines, const c_wranglert::functiont &function_config, std::ostream &out)
static c_definest get_defines(const std::string &source_file, const c_wranglert &config)
static void mangle_object(const c_declarationt &declaration, const c_definest &defines, const c_wranglert::objectt &object_config, std::ostream &out)
void c_wrangler(const jsont &config)
static std::string preprocess(const std::string &source_file, const c_wranglert &c_wrangler)
static void mangle(const c_declarationt &declaration, const c_definest &defines, const c_wranglert &config, std::ostream &out)
This class maintains a representation of one assignment to the preprocessor macros in a C program.
void parse(const std::string &)
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Thrown when some external system fails unexpectedly.
ctokenitt match_bracket(ctokenitt t, char open, char close)
json_objectt & to_json_object(jsont &json)
json_arrayt & to_json_array(jsont &json)
c_translation_unitt parse_c(std::istream &in)
nonstd::optional< T > optionalt
int run(const std::string &what, const std::vector< std::string > &argv)
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
optionalt< ctokent > declared_identifier() const
assertiont(std::string _identifier, std::string _content)
contract_clauset(std::string _clause, std::string _content)
std::vector< loop_invariantt > loop_invariants
std::vector< assertiont > assertions
std::vector< contract_clauset > contract
optionalt< std::string > stub
loop_invariantt(std::string _loop_type, std::string _identifier, std::string _content)
void configure_output(const jsont &)
void configure_objects(const jsont &)
std::vector< std::string > source_files
std::list< std::pair< std::regex, functiont > > functionst
std::list< std::pair< std::regex, objectt > > objectst
void configure_sources(const jsont &)
std::vector< std::string > includes
std::vector< std::string > defines
void configure_functions(const jsont &)