cprover
Loading...
Searching...
No Matches
c_wrangler.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C Wrangler
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#include "c_wrangler.h"
13
14#include <util/cprover_prefix.h>
16#include <util/json.h>
17#include <util/run.h>
18#include <util/string_utils.h>
19
20#include "c_defines.h"
21#include "ctokenit.h"
22#include "mini_c_parser.h"
23
24#include <fstream> // IWYU pragma: keep
25#include <iostream>
26#include <map>
27#include <regex>
28#include <sstream>
29
31{
32 // sources and preprocessing
33 std::vector<std::string> source_files;
34 std::vector<std::string> includes;
35 std::vector<std::string> defines;
36
37 // transformations
39 {
40 std::string clause;
41 std::string content;
42 function_contract_clauset(std::string _clause, std::string _content)
43 : clause(std::move(_clause)), content(std::move(_content))
44 {
45 }
46 };
47
49 {
50 std::string loop_type;
51 std::string identifier;
52 std::string clause;
53 std::string content;
55 std::string _loop_type,
56 std::string _identifier,
57 std::string _clause,
58 std::string _content)
59 : loop_type(std::move(_loop_type)),
60 identifier(std::move(_identifier)),
61 clause(std::move(_clause)),
62 content(std::move(_content))
63 {
64 }
65 };
66
68 {
69 std::string identifier;
70 std::string content;
71 assertiont(std::string _identifier, std::string _content)
72 : identifier(std::move(_identifier)), content(std::move(_content))
73 {
74 }
75 };
76
77 struct functiont
78 {
79 // should be variant to preserve ordering
80 std::vector<function_contract_clauset> function_contract;
81 std::vector<loop_contract_clauset> loop_contract;
82 std::vector<assertiont> assertions;
84 bool remove_static = false;
85 };
86
87 using functionst = std::list<std::pair<std::regex, functiont>>;
89
90 struct objectt
91 {
92 bool remove_static = false;
93 };
94
95 using objectst = std::list<std::pair<std::regex, objectt>>;
97
98 // output
99 std::string output;
100
101 void configure_sources(const jsont &);
102 void configure_functions(const jsont &);
103 void configure_objects(const jsont &);
104 void configure_output(const jsont &);
105};
106
108{
109 auto sources = config["sources"];
110
111 if(!sources.is_null())
112 {
113 if(!sources.is_array())
114 throw deserialization_exceptiont("sources entry must be sequence");
115
116 for(const auto &source : to_json_array(sources))
117 {
118 if(!source.is_string())
119 throw deserialization_exceptiont("source must be string");
120
121 this->source_files.push_back(source.value);
122 }
123 }
124
125 auto includes = config["includes"];
126
127 if(!includes.is_null())
128 {
129 if(!includes.is_array())
130 throw deserialization_exceptiont("includes entry must be sequence");
131
132 for(const auto &include : to_json_array(includes))
133 {
134 if(!include.is_string())
135 throw deserialization_exceptiont("include must be string");
136
137 this->includes.push_back(include.value);
138 }
139 }
140
141 auto defines = config["defines"];
142
143 if(!defines.is_null())
144 {
145 if(!defines.is_array())
146 throw deserialization_exceptiont("defines entry must be sequence");
147
148 for(const auto &define : to_json_array(defines))
149 {
150 if(!define.is_string())
151 throw deserialization_exceptiont("define must be string");
152
153 this->defines.push_back(define.value);
154 }
155 }
156}
157
159{
160 auto functions = config["functions"];
161
162 if(functions.is_null())
163 return;
164
165 if(!functions.is_array())
166 throw deserialization_exceptiont("functions entry must be sequence");
167
168 for(const auto &function : to_json_array(functions))
169 {
170 if(!function.is_object())
171 throw deserialization_exceptiont("function entry must be object");
172
173 for(const auto &function_entry : to_json_object(function))
174 {
175 const auto function_name = function_entry.first;
176 const auto &items = function_entry.second;
177
178 if(!items.is_array())
179 throw deserialization_exceptiont("function entry must be sequence");
180
181 this->functions.emplace_back(function_name, functiont{});
182 functiont &function_config = this->functions.back().second;
183
184 for(const auto &function_item : to_json_array(items))
185 {
186 // These need to start with "ensures", "requires", "assigns",
187 // "invariant", "assert", "stub", "remove"
188 if(!function_item.is_string())
189 throw deserialization_exceptiont("function entry must be string");
190
191 auto item_string = function_item.value;
192 auto split = split_string(item_string, ' ');
193 if(split.empty())
194 continue;
195
196 if(
197 split[0] == "ensures" || split[0] == "requires" ||
198 split[0] == "assigns")
199 {
200 std::ostringstream rest;
201 join_strings(rest, split.begin() + 1, split.end(), ' ');
202
203 function_config.function_contract.emplace_back(split[0], rest.str());
204 }
205 else if(split[0] == "assert" && split.size() >= 3)
206 {
207 std::ostringstream rest;
208 join_strings(rest, split.begin() + 2, split.end(), ' ');
209
210 function_config.assertions.emplace_back(split[1], rest.str());
211 }
212 else if(
213 (split[0] == "for" || split[0] == "while" || split[0] == "loop") &&
214 split.size() >= 3 &&
215 (split[2] == "invariant" || split[2] == "assigns" ||
216 split[2] == "decreases"))
217 {
218 std::ostringstream rest;
219 join_strings(rest, split.begin() + 3, split.end(), ' ');
220
221 function_config.loop_contract.emplace_back(
222 split[0], split[1], split[2], rest.str());
223 }
224 else if(split[0] == "stub")
225 {
226 std::ostringstream rest;
227 join_strings(rest, split.begin() + 1, split.end(), ' ');
228
229 function_config.stub = rest.str();
230 }
231 else if(split[0] == "remove")
232 {
233 if(split.size() == 1)
234 throw deserialization_exceptiont("unexpected remove entry");
235
236 if(split[1] == "static")
237 function_config.remove_static = true;
238 else
240 "unexpected remove entry " + split[1]);
241 }
242 else
244 "unexpected function entry " + split[0]);
245 }
246 }
247 }
248}
249
251{
252 auto objects = config["objects"];
253
254 if(objects.is_null())
255 return;
256
257 if(!objects.is_array())
258 throw deserialization_exceptiont("objects entry must be sequence");
259
260 for(const auto &object : to_json_array(objects))
261 {
262 if(!object.is_object())
263 throw deserialization_exceptiont("object entry must be object");
264
265 for(const auto &object_entry : to_json_object(object))
266 {
267 const auto &object_name = object_entry.first;
268 const auto &items = object_entry.second;
269
270 if(!items.is_array())
271 throw deserialization_exceptiont("object entry must be sequence");
272
273 this->objects.emplace_back(object_name, objectt{});
274 objectt &object_config = this->objects.back().second;
275
276 for(const auto &object_item : to_json_array(items))
277 {
278 // Needs to start with "remove"
279 if(!object_item.is_string())
280 throw deserialization_exceptiont("object entry must be string");
281
282 auto item_string = object_item.value;
283 auto split = split_string(item_string, ' ');
284 if(split.empty())
285 continue;
286
287 if(split[0] == "remove")
288 {
289 if(split.size() == 1)
290 throw deserialization_exceptiont("unexpected remove entry");
291
292 if(split[1] == "static")
293 object_config.remove_static = true;
294 else
296 "unexpected remove entry " + split[1]);
297 }
298 else
300 "unexpected object entry " + split[0]);
301 }
302 }
303 }
304}
305
307{
308 auto output = config["output"];
309
310 if(output.is_null())
311 return;
312
313 if(!output.is_string())
314 throw deserialization_exceptiont("output entry must be string");
315
316 this->output = output.value;
317}
318
319static std::string
320preprocess(const std::string &source_file, const c_wranglert &c_wrangler)
321{
322 std::vector<std::string> argv = {"cc", "-E", source_file};
323
324 for(const auto &include : c_wrangler.includes)
325 {
326 argv.push_back("-I");
327 argv.push_back(include);
328 }
329
330 for(const auto &define : c_wrangler.defines)
331 argv.push_back(std::string("-D") + define);
332
333 std::ostringstream result;
334
335 auto run_result = run("cc", argv, "", result, "");
336 if(run_result != 0)
337 throw system_exceptiont("preprocessing " + source_file + " has failed");
338
339 return result.str();
340}
341
342static c_definest
343get_defines(const std::string &source_file, const c_wranglert &config)
344{
345 std::vector<std::string> argv = {"cc", "-E", "-dM", source_file};
346
347 for(const auto &include : config.includes)
348 {
349 argv.push_back("-I");
350 argv.push_back(include);
351 }
352
353 std::ostringstream result;
354
355 auto run_result = run("cc", argv, "", result, "");
356 if(run_result != 0)
357 throw system_exceptiont("preprocessing " + source_file + " has failed");
358
359 c_definest defines;
360 defines.parse(result.str());
361 return defines;
362}
363
364static void mangle_function(
365 const c_declarationt &declaration,
366 const c_definest &defines,
367 const c_wranglert::functiont &function_config,
368 std::ostream &out)
369{
370 if(function_config.stub.has_value() && declaration.has_body())
371 {
372 // replace by stub
373 out << function_config.stub.value();
374 }
375 else
376 {
377 if(function_config.remove_static)
378 {
379 for(auto &t : declaration.pre_declarator)
380 {
381 if(t.text == "static")
382 {
383 // we replace by white space
384 out << std::string(6, ' ');
385 }
386 else
387 out << t.text;
388 }
389 }
390 else
391 {
392 for(auto &t : declaration.pre_declarator)
393 out << t.text;
394 }
395
396 for(auto &t : declaration.declarator)
397 out << t.text;
398 for(auto &t : declaration.post_declarator)
399 out << t.text;
400
401 if(!declaration.has_body())
402 {
403 for(auto &t : declaration.initializer)
404 out << t.text;
405 return;
406 }
407
408 for(const auto &entry : function_config.function_contract)
409 out << ' ' << CPROVER_PREFIX << entry.clause << '('
410 << defines(entry.content) << ')';
411
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;
415
416 for(const auto &entry : function_config.loop_contract)
417 {
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;
424 }
425
426 if(
427 loop_invariants.empty() && loop_assigns.empty() && loop_decreases.empty())
428 {
429 for(auto &t : declaration.initializer)
430 out << t.text;
431 }
432 else
433 {
434 std::size_t for_count = 0, while_count = 0;
435 ctokenitt t(declaration.initializer);
436
437 while(t)
438 {
439 const auto &token = *(t++);
440 out << token.text;
441 std::string invariant;
442 std::string assigns;
443 std::string decreases;
444
445 if(token == "while")
446 {
447 while_count++;
448 invariant =
449 loop_invariants.count("while" + std::to_string(while_count))
450 ? loop_invariants["while" + std::to_string(while_count)]
451 : loop_invariants
452 ["loop" + std::to_string(while_count + for_count)];
453
454 assigns =
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)];
458
459 decreases =
460 loop_decreases.count("while" + std::to_string(while_count))
461 ? loop_decreases["while" + std::to_string(while_count)]
462 : loop_decreases
463 ["loop" + std::to_string(while_count + for_count)];
464 }
465 else if(token == "for")
466 {
467 for_count++;
468 invariant = loop_invariants.count("for" + std::to_string(for_count))
469 ? loop_invariants["for" + std::to_string(for_count)]
470 : loop_invariants
471 ["loop" + std::to_string(while_count + for_count)];
472 assigns =
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)];
476
477 decreases = loop_decreases.count("for" + std::to_string(for_count))
478 ? loop_decreases["for" + std::to_string(for_count)]
479 : loop_decreases
480 ["loop" + std::to_string(while_count + for_count)];
481 }
482
483 auto t_end = match_bracket(t, '(', ')');
484 for(; t != t_end; t++)
485 out << t->text;
486
487 if(!assigns.empty())
488 {
489 out << ' ' << CPROVER_PREFIX << "assigns(" << defines(assigns) << ')';
490 }
491
492 if(!invariant.empty())
493 {
494 out << ' ' << CPROVER_PREFIX << "loop_invariant("
495 << defines(invariant) << ')';
496 }
497
498 if(!decreases.empty())
499 {
500 out << ' ' << CPROVER_PREFIX << "decreases(" << defines(decreases)
501 << ')';
502 }
503 }
504 }
505 }
506}
507
508static void mangle_object(
509 const c_declarationt &declaration,
510 const c_definest &defines,
511 const c_wranglert::objectt &object_config,
512 std::ostream &out)
513{
514 if(object_config.remove_static)
515 {
516 for(auto &t : declaration.pre_declarator)
517 {
518 if(t.text == "static")
519 {
520 // we replace by white space
521 out << std::string(6, ' ');
522 }
523 else
524 out << t.text;
525 }
526 }
527 else
528 {
529 for(auto &t : declaration.pre_declarator)
530 out << t.text;
531 }
532
533 for(auto &t : declaration.declarator)
534 out << t.text;
535 for(auto &t : declaration.post_declarator)
536 out << t.text;
537 for(auto &t : declaration.initializer)
538 out << t.text;
539}
540
541static void mangle(
542 const c_declarationt &declaration,
543 const c_definest &defines,
544 const c_wranglert &config,
545 std::ostream &out)
546{
547 auto name_opt = declaration.declared_identifier();
548 if(declaration.is_function() && name_opt.has_value())
549 {
550 for(const auto &entry : config.functions)
551 {
552 if(std::regex_match(name_opt->text, entry.first))
553 {
554 // we are to modify this function
555 mangle_function(declaration, defines, entry.second, out);
556
557 return;
558 }
559 }
560 }
561 else if(!declaration.is_function() && name_opt.has_value())
562 {
563 for(const auto &entry : config.objects)
564 {
565 if(std::regex_match(name_opt->text, entry.first))
566 {
567 // we are to modify this function
568 mangle_object(declaration, defines, entry.second, out);
569
570 return;
571 }
572 }
573 }
574
575 // output
576 out << declaration;
577}
578
579static std::string mangle(
580 const std::string &in,
581 const c_definest &defines,
582 const c_wranglert &config)
583{
584 std::ostringstream out;
585 std::istringstream in_str(in);
586
587 auto parsed = parse_c(in_str);
588
589 for(const auto &declaration : parsed)
590 mangle(declaration, defines, config, out);
591
592 return out.str();
593}
594
596{
598
600 c_wrangler.configure_functions(config);
601 c_wrangler.configure_objects(config);
602 c_wrangler.configure_output(config);
603
604 for(auto &source_file : c_wrangler.source_files)
605 {
606 // first preprocess
607 auto preprocessed = preprocess(source_file, c_wrangler);
608
609 // get the defines
610 auto defines = get_defines(source_file, c_wrangler);
611
612 // now mangle
613 auto mangled = mangle(preprocessed, defines, c_wrangler);
614
615 // now output
616 if(c_wrangler.output == "stdout" || c_wrangler.output.empty())
617 {
618 std::cout << mangled;
619 }
620 else
621 {
622 std::ofstream out(c_wrangler.output);
623 out << mangled;
624 }
625 }
626}
configt config
Definition config.cpp:25
c_defines
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)
C Wrangler.
This class maintains a representation of one assignment to the preprocessor macros in a C program.
Definition c_defines.h:24
void parse(const std::string &)
Definition c_defines.cpp:21
std::string text
Definition ctoken.h:40
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition json.h:27
Thrown when some external system fails unexpectedly.
#define CPROVER_PREFIX
ctokenitt match_bracket(ctokenitt t, char open, char close)
Definition ctokenit.cpp:33
ctokenit
json_objectt & to_json_object(jsont &json)
Definition json.h:444
json_arrayt & to_json_array(jsont &json)
Definition json.h:426
c_translation_unitt parse_c(std::istream &in)
Mini C Parser.
STL namespace.
nonstd::optional< T > optionalt
Definition optional.h:35
int run(const std::string &what, const std::vector< std::string > &argv)
Definition run.cpp:48
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.
bool has_body() const
bool is_function() const
tokenst post_declarator
tokenst initializer
optionalt< ctokent > declared_identifier() const
tokenst pre_declarator
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 &)
objectst objects
std::list< std::pair< std::regex, objectt > > objectst
std::vector< std::string > source_files
std::string output
std::list< std::pair< std::regex, functiont > > functionst
functionst functions
void configure_sources(const jsont &)
std::vector< std::string > includes
std::vector< std::string > defines
void configure_functions(const jsont &)