55 std::string _loop_type,
56 std::string _identifier,
71 assertiont(std::string _identifier, std::string _content)
87 using functionst = std::list<std::pair<std::regex, functiont>>;
95 using objectst = std::list<std::pair<std::regex, objectt>>;
109 auto sources =
config[
"sources"];
111 if(!sources.is_null())
113 if(!sources.is_array())
118 if(!source.is_string())
134 if(!include.is_string())
137 this->
includes.push_back(include.value);
150 if(!define.is_string())
153 this->
defines.push_back(define.value);
170 if(!function.is_object())
175 const auto function_name = function_entry.first;
176 const auto &items = function_entry.second;
178 if(!items.is_array())
188 if(!function_item.is_string())
191 auto item_string = function_item.value;
197 split[0] ==
"ensures" || split[0] ==
"requires" ||
198 split[0] ==
"assigns")
200 std::ostringstream rest;
201 join_strings(rest, split.begin() + 1, split.end(),
' ');
205 else if(split[0] ==
"assert" && split.size() >= 3)
207 std::ostringstream rest;
208 join_strings(rest, split.begin() + 2, split.end(),
' ');
210 function_config.
assertions.emplace_back(split[1], rest.str());
213 (split[0] ==
"for" || split[0] ==
"while" || split[0] ==
"loop") &&
215 (split[2] ==
"invariant" || split[2] ==
"assigns" ||
216 split[2] ==
"decreases"))
218 std::ostringstream rest;
219 join_strings(rest, split.begin() + 3, split.end(),
' ');
222 split[0], split[1], split[2], rest.str());
224 else if(split[0] ==
"stub")
226 std::ostringstream rest;
227 join_strings(rest, split.begin() + 1, split.end(),
' ');
229 function_config.
stub = rest.str();
231 else if(split[0] ==
"remove")
233 if(split.size() == 1)
236 if(split[1] ==
"static")
240 "unexpected remove entry " + split[1]);
244 "unexpected function entry " + split[0]);
262 if(!
object.is_object())
267 const auto &object_name = object_entry.first;
268 const auto &items = object_entry.second;
270 if(!items.is_array())
279 if(!object_item.is_string())
282 auto item_string = object_item.value;
287 if(split[0] ==
"remove")
289 if(split.size() == 1)
292 if(split[1] ==
"static")
296 "unexpected remove entry " + split[1]);
300 "unexpected object entry " + split[0]);
322 std::vector<std::string> argv = {
"cc",
"-E", source_file};
324 for(
const auto &include :
c_wrangler.includes)
326 argv.push_back(
"-I");
327 argv.push_back(include);
331 argv.push_back(std::string(
"-D") + define);
333 std::ostringstream result;
335 auto run_result =
run(
"cc", argv,
"", result,
"");
345 std::vector<std::string> argv = {
"cc",
"-E",
"-dM", source_file};
347 for(
const auto &include :
config.includes)
349 argv.push_back(
"-I");
350 argv.push_back(include);
353 std::ostringstream result;
355 auto run_result =
run(
"cc", argv,
"", result,
"");
360 defines.
parse(result.str());
370 if(function_config.
stub.has_value() && declaration.
has_body())
373 out << function_config.
stub.value();
381 if(t.text ==
"static")
384 out << std::string(6,
' ');
410 << defines(entry.content) <<
')';
412 std::map<std::string, std::string> loop_invariants;
413 std::map<std::string, std::string> loop_assigns;
414 std::map<std::string, std::string> loop_decreases;
418 if(entry.clause ==
"invariant")
419 loop_invariants[entry.loop_type + entry.identifier] = entry.content;
420 if(entry.clause ==
"assigns")
421 loop_assigns[entry.loop_type + entry.identifier] = entry.content;
422 if(entry.clause ==
"decreases")
423 loop_decreases[entry.loop_type + entry.identifier] = entry.content;
427 loop_invariants.empty() && loop_assigns.empty() && loop_decreases.empty())
434 std::size_t for_count = 0, while_count = 0;
439 const auto &token = *(t++);
441 std::string invariant;
443 std::string decreases;
449 loop_invariants.count(
"while" + std::to_string(while_count))
450 ? loop_invariants[
"while" + std::to_string(while_count)]
452 [
"loop" + std::to_string(while_count + for_count)];
455 loop_assigns.count(
"while" + std::to_string(while_count))
456 ? loop_assigns[
"while" + std::to_string(while_count)]
457 : loop_assigns[
"loop" + std::to_string(while_count + for_count)];
460 loop_decreases.count(
"while" + std::to_string(while_count))
461 ? loop_decreases[
"while" + std::to_string(while_count)]
463 [
"loop" + std::to_string(while_count + for_count)];
465 else if(token ==
"for")
468 invariant = loop_invariants.count(
"for" + std::to_string(for_count))
469 ? loop_invariants[
"for" + std::to_string(for_count)]
471 [
"loop" + std::to_string(while_count + for_count)];
473 loop_assigns.count(
"for" + std::to_string(for_count))
474 ? loop_assigns[
"for" + std::to_string(for_count)]
475 : loop_assigns[
"loop" + std::to_string(while_count + for_count)];
477 decreases = loop_decreases.count(
"for" + std::to_string(for_count))
478 ? loop_decreases[
"for" + std::to_string(for_count)]
480 [
"loop" + std::to_string(while_count + for_count)];
484 for(; t != t_end; t++)
489 out <<
' ' <<
CPROVER_PREFIX <<
"assigns(" << defines(assigns) <<
')';
492 if(!invariant.empty())
495 << defines(invariant) <<
')';
498 if(!decreases.empty())
500 out <<
' ' <<
CPROVER_PREFIX <<
"decreases(" << defines(decreases)
518 if(t.text ==
"static")
521 out << std::string(6,
' ');
548 if(declaration.
is_function() && name_opt.has_value())
550 for(
const auto &entry :
config.functions)
552 if(std::regex_match(name_opt->text, entry.first))
561 else if(!declaration.
is_function() && name_opt.has_value())
563 for(
const auto &entry :
config.objects)
565 if(std::regex_match(name_opt->text, entry.first))
580 const std::string &in,
584 std::ostringstream out;
585 std::istringstream in_str(in);
589 for(
const auto &declaration : parsed)
604 for(
auto &source_file :
c_wrangler.source_files)
618 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)
function_contract_clauset(std::string _clause, std::string _content)
std::vector< loop_contract_clauset > loop_contract
std::vector< function_contract_clauset > function_contract
std::vector< assertiont > assertions
optionalt< std::string > stub
loop_contract_clauset(std::string _loop_type, std::string _identifier, std::string _clause, std::string _content)
void configure_output(const jsont &)
void configure_objects(const jsont &)
std::list< std::pair< std::regex, objectt > > objectst
std::vector< std::string > source_files
std::list< std::pair< std::regex, functiont > > functionst
void configure_sources(const jsont &)
std::vector< std::string > includes
std::vector< std::string > defines
void configure_functions(const jsont &)