cprover
Loading...
Searching...
No Matches
linker_script_merge.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Linker Script Merging
4
5Author: Kareem Khazem <karkhaz@karkhaz.com>, 2017
6
7\*******************************************************************/
8
10
11#include <util/arith_tools.h>
12#include <util/c_types.h>
13#include <util/cmdline.h>
15#include <util/magic.h>
16#include <util/pointer_expr.h>
17#include <util/run.h>
18#include <util/tempfile.h>
19
23
24#include <json/json_parser.h>
26
27#include "compile.h"
28
29#include <algorithm>
30#include <fstream> // IWYU pragma: keep
31#include <iterator>
32
34{
35 if(!cmdline.isset('T'))
36 return 0;
37
40
41 if(!original_goto_model.has_value())
42 {
43 log.error() << "Unable to read goto binary for linker script merging"
45 return 1;
46 }
47
48 temporary_filet linker_def_outfile("goto-cc-linker-info", ".json");
49 std::list<irep_idt> linker_defined_symbols;
52 original_goto_model->symbol_table,
55 // ignore linker script parsing failures until the code is tested more widely
56 if(fail!=0)
57 return 0;
58
59 jsont data;
61 if(fail!=0)
62 {
63 log.error() << "Problem parsing linker script JSON data" << messaget::eom;
64 return fail;
65 }
66
68 if(fail!=0)
69 {
70 log.error() << "Malformed linker-script JSON document" << messaget::eom;
71 data.output(log.error());
72 return fail;
73 }
74
77 data,
78 cmdline.get_value('T'),
79 original_goto_model->symbol_table,
81 if(fail!=0)
82 {
83 log.error() << "Could not add linkerscript defs to symbol table"
85 return fail;
86 }
87
88 if(original_goto_model->can_produce_function(INITIALIZE_FUNCTION))
89 {
92 }
93
95 if(fail!=0)
96 return fail;
97
98 // The keys of linker_values are exactly the elements of
99 // linker_defined_symbols, so iterate over linker_values from now on.
100
102
103 if(fail!=0)
104 {
105 log.error() << "Could not pointerize all linker-defined expressions"
106 << messaget::eom;
107 return fail;
108 }
109
113 cmdline.isset("validate-goto-model"),
115
116 if(fail!=0)
117 {
118 log.error() << "Could not write linkerscript-augmented binary"
119 << messaget::eom;
120 }
121
122 return fail;
123}
124
126 const std::string &elf_binary,
127 const std::string &goto_binary,
128 const cmdlinet &cmdline,
129 message_handlert &message_handler)
130 : elf_binary(elf_binary),
131 goto_binary(goto_binary),
132 cmdline(cmdline),
133 log(message_handler),
134 replacement_predicates(
136 "address of array's first member",
137 [](const exprt &expr) -> const symbol_exprt & {
138 return to_symbol_expr(
139 to_index_expr(to_address_of_expr(expr).object()).index());
140 },
141 [](const exprt &expr) {
142 return expr.id() == ID_address_of &&
143 expr.type().id() == ID_pointer &&
144
145 to_address_of_expr(expr).object().id() == ID_index &&
146 to_address_of_expr(expr).object().type().id() ==
148
149 to_index_expr(to_address_of_expr(expr).object())
150 .array()
151 .id() == ID_symbol &&
152 to_index_expr(to_address_of_expr(expr).object())
153 .array()
154 .type()
155 .id() == ID_array &&
156
157 to_index_expr(to_address_of_expr(expr).object())
158 .index()
159 .is_constant() &&
160 to_index_expr(to_address_of_expr(expr).object())
161 .index()
162 .type()
163 .id() == ID_signedbv;
164 }),
166 "address of array",
167 [](const exprt &expr) -> const symbol_exprt & {
168 return to_symbol_expr(to_address_of_expr(expr).object());
169 },
170 [](const exprt &expr) {
171 return expr.id() == ID_address_of &&
172 expr.type().id() == ID_pointer &&
173
174 to_address_of_expr(expr).object().id() == ID_symbol &&
175 to_address_of_expr(expr).object().type().id() == ID_array;
176 }),
178 "address of struct",
179 [](const exprt &expr) -> const symbol_exprt & {
180 return to_symbol_expr(to_address_of_expr(expr).object());
181 },
182 [](const exprt &expr) {
183 return expr.id() == ID_address_of &&
184 expr.type().id() == ID_pointer &&
185
186 to_address_of_expr(expr).object().id() == ID_symbol &&
187 (to_address_of_expr(expr).object().type().id() == ID_struct ||
188 to_address_of_expr(expr).object().type().id() ==
190 }),
192 "array variable",
193 [](const exprt &expr) -> const symbol_exprt & {
194 return to_symbol_expr(expr);
195 },
196 [](const exprt &expr) {
197 return expr.id() == ID_symbol && expr.type().id() == ID_array;
198 }),
200 "pointer (does not need pointerizing)",
201 [](const exprt &expr) -> const symbol_exprt & {
202 return to_symbol_expr(expr);
203 },
204 [](const exprt &expr) {
205 return expr.id() == ID_symbol && expr.type().id() == ID_pointer;
206 })})
207{}
208
210 goto_modelt &goto_model,
212{
213 const namespacet ns(goto_model.symbol_table);
214
215 int ret=0;
216
217 // Next, find all occurrences of linker-defined symbols that are _values_
218 // of some symbol in the symbol table, and pointerize them too
219 for(auto it = goto_model.symbol_table.begin();
220 it != goto_model.symbol_table.end();
221 ++it)
222 {
223 std::list<symbol_exprt> to_pointerize;
225
226 if(to_pointerize.empty())
227 continue;
228 log.debug() << "Pointerizing the symbol-table value of symbol " << it->first
229 << messaget::eom;
231 it.get_writeable_symbol().value, to_pointerize, linker_values);
232 if(to_pointerize.empty() && fail==0)
233 continue;
234 ret=1;
235 for(const auto &sym : to_pointerize)
236 {
237 log.error() << " Could not pointerize '" << sym.get_identifier()
238 << "' in symbol table entry " << it->first << ". Pretty:\n"
239 << sym.pretty() << "\n";
240 }
242 }
243
244 // Finally, pointerize all occurrences of linker-defined symbols in the
245 // goto program
246 for(auto &gf : goto_model.goto_functions.function_map)
247 {
248 goto_programt &program=gf.second.body;
249 for(auto &instruction : program.instructions)
250 {
251 std::list<exprt *> expressions = {&instruction.code_nonconst()};
252 if(instruction.has_condition())
253 expressions.push_back(&instruction.condition_nonconst());
254
255 for(exprt *insts : expressions)
256 {
257 std::list<symbol_exprt> to_pointerize;
259 if(to_pointerize.empty())
260 continue;
261 log.debug() << "Pointerizing a program expression..." << messaget::eom;
263 if(to_pointerize.empty() && fail==0)
264 continue;
265 ret=1;
266 for(const auto &sym : to_pointerize)
267 {
268 log.error() << " Could not pointerize '" << sym.get_identifier()
269 << "' in function " << gf.first << ". Pretty:\n"
270 << sym.pretty() << "\n";
271 log.error().source_location = instruction.source_location();
272 }
274 }
275 }
276 }
277 return ret;
278}
279
283 const symbol_exprt &old_symbol,
284 const irep_idt &ident,
285 const std::string &shape)
286{
287 auto it=linker_values.find(ident);
288 if(it==linker_values.end())
289 {
290 log.error() << "Could not find a new expression for linker script-defined "
291 << "symbol '" << ident << "'" << messaget::eom;
292 return 1;
293 }
294 symbol_exprt new_expr=it->second.first;
295 new_expr.add_source_location()=old_symbol.source_location();
296 log.debug() << "Pointerizing linker-defined symbol '" << ident
297 << "' of shape <" << shape << ">." << messaget::eom;
299 return 0;
300}
301
303 exprt &expr,
304 std::list<symbol_exprt> &to_pointerize,
306{
307 int fail=0, tmp=0;
308 for(auto const &pair : linker_values)
309 for(auto const &pattern : replacement_predicates)
310 {
311 if(!pattern.match(expr))
312 continue;
313 // take a copy, expr will be changed below
314 const symbol_exprt inner_symbol=pattern.inner_symbol(expr);
315 if(pair.first!=inner_symbol.get_identifier())
316 continue;
317 tmp=replace_expr(expr, linker_values, inner_symbol, pair.first,
318 pattern.description());
320 auto result=std::find(to_pointerize.begin(), to_pointerize.end(),
321 inner_symbol);
322 if(result==to_pointerize.end())
323 {
324 fail=1;
325 log.error() << "Too many removals of '" << inner_symbol.get_identifier()
326 << "'" << messaget::eom;
327 }
328 else
329 to_pointerize.erase(result);
330 // If we get here, we've just pointerized this expression. That expression
331 // will be a symbol possibly wrapped in some unary junk, but won't contain
332 // other symbols as subexpressions that might need to be pointerized. So
333 // it's safe to bail out here.
334 return fail;
335 }
336
337 for(auto &op : expr.operands())
338 {
341 }
342 return fail;
343}
344
347 const exprt &expr,
348 std::list<symbol_exprt> &to_pointerize) const
349{
350 for(const auto &op : expr.operands())
351 {
352 if(op.id()!=ID_symbol)
353 continue;
355 const auto &pair=linker_values.find(sym_exp.get_identifier());
356 if(pair!=linker_values.end())
357 to_pointerize.push_back(sym_exp);
358 }
359 for(const auto &op : expr.operands())
361}
362
363#if 0
364The current implementation of this function is less precise than the
367
368Suppose we have a section in the linker script, 100 bytes long, where the
369address of the symbol sec_start is the start of the section (value 4096) and the
370address of sec_end is the end of that section (value 4196).
371
372The current implementation synthesizes the goto-version of the following C:
373
374 char __sec_array[100];
375 char *sec_start=(&__sec_array[0]);
376 char *sec_end=((&__sec_array[0])+100);
377 // Yes, it is 100 not 99. We're pointing to the end of the memory occupied
378 // by __sec_array, not the last element of __sec_array.
379
380This is imprecise for the following reason: the actual address of the array and
381the pointers shall be some random CBMC-internal address, instead of being 4096
383position of the section, and we even know what the actual values of sec_start
384and sec_end are from the object file (these values are in the `addresses` list
385of the `data` argument to this function). If the correctness of the code depends
386on these actual values, then CBMCs model of the code is too imprecise to verify
387this.
388
389The commented-out version of this function below synthesizes the following:
390
391 char *sec_start=4096;
392 char *sec_end=4196;
394
395This code has both the actual addresses of the start and end of the section and
396tells CBMC that the intermediate region is valid. However, the allocated_memory
397macro does not currently allocate an actual object at the address 4096, so
398symbolic execution can fail. In particular, the 'allocated memory' is part of
401do not have know n size. The commented-out implementation should be reinstated
403
404In either case, no other changes to the rest of the code (outside this function)
406linker-defined symbol into pointer types if they were not already, and this is
408#endif
410 jsont &data,
411 const std::string &linker_script,
412 symbol_tablet &symbol_table,
414#if 1
415{
416 std::map<irep_idt, std::size_t> truncated_symbols;
417 for(auto &d : to_json_array(data["regions"]))
418 {
419 bool has_end=d["has-end-symbol"].is_true();
420
421 std::ostringstream array_name;
422 array_name << CPROVER_PREFIX << "linkerscript-array_"
423 << d["start-symbol"].value;
424 if(has_end)
425 array_name << "-" << d["end-symbol"].value;
426
427
428 // Array symbol_exprt
429 mp_integer array_size = string2integer(d["size"].value);
431 {
432 log.warning() << "Object section '" << d["section"].value << "' of size "
433 << array_size << " is too large to model. Truncating to "
434 << MAX_FLATTENED_ARRAY_SIZE << " bytes" << messaget::eom;
436 if(!has_end)
437 truncated_symbols[d["size-symbol"].value]=MAX_FLATTENED_ARRAY_SIZE;
438 }
439
442
444 array_loc.set_file(linker_script);
445 std::ostringstream array_comment;
446 array_comment << "Object section '" << d["section"].value << "' of size "
447 << array_size << " bytes";
448 array_loc.set_comment(array_comment.str());
449
450 namespacet ns(symbol_table);
451 const auto zi = zero_initializer(array_type, array_loc, ns);
452 CHECK_RETURN(zi.has_value());
453
454 // Add the array to the symbol table.
456 array_sym.is_static_lifetime = true;
457 array_sym.is_lvalue = true;
458 array_sym.is_state_var = true;
459 array_sym.value = *zi;
460 array_sym.location = array_loc;
461
462 bool failed = symbol_table.add(array_sym);
464
465 // Array start address
468
469 // Linker-defined symbol_exprt pointing to start address
470 symbolt start_sym{d["start-symbol"].value, pointer_type(char_type()), ID_C};
471 start_sym.is_static_lifetime = true;
472 start_sym.is_lvalue = true;
473 start_sym.is_state_var = true;
474 start_sym.value = array_start;
475 linker_values.emplace(
476 d["start-symbol"].value,
477 std::make_pair(start_sym.symbol_expr(), array_start));
478
479 // Since the value of the pointer will be a random CBMC address, write a
480 // note about the real address in the object file
481 auto it = std::find_if(
482 to_json_array(data["addresses"]).begin(),
483 to_json_array(data["addresses"]).end(),
484 [&d](const jsont &add) {
485 return add["sym"].value == d["start-symbol"].value;
486 });
487 if(it == to_json_array(data["addresses"]).end())
488 {
489 log.error() << "Start: Could not find address corresponding to symbol '"
490 << d["start-symbol"].value << "' (start of section)"
491 << messaget::eom;
492 return 1;
493 }
495 start_loc.set_file(linker_script);
496 std::ostringstream start_comment;
497 start_comment << "Pointer to beginning of object section '"
498 << d["section"].value << "'. Original address in object file"
499 << " is " << (*it)["val"].value;
500 start_loc.set_comment(start_comment.str());
501 start_sym.location = start_loc;
502
503 auto start_sym_entry = symbol_table.insert(start_sym);
504 if(!start_sym_entry.second)
506
507 if(has_end) // Same for pointer to end of array
508 {
510
511 symbolt end_sym{d["end-symbol"].value, pointer_type(char_type()), ID_C};
512 end_sym.is_static_lifetime = true;
513 end_sym.is_lvalue = true;
514 end_sym.is_state_var = true;
515 end_sym.value = array_end;
516 linker_values.emplace(
517 d["end-symbol"].value,
518 std::make_pair(end_sym.symbol_expr(), array_end));
519
520 auto entry = std::find_if(
521 to_json_array(data["addresses"]).begin(),
522 to_json_array(data["addresses"]).end(),
523 [&d](const jsont &add) {
524 return add["sym"].value == d["end-symbol"].value;
525 });
526 if(entry == to_json_array(data["addresses"]).end())
527 {
528 log.debug() << "Could not find address corresponding to symbol '"
529 << d["end-symbol"].value << "' (end of section)"
530 << messaget::eom;
531 return 1;
532 }
534 end_loc.set_file(linker_script);
535 std::ostringstream end_comment;
536 end_comment << "Pointer to end of object section '" << d["section"].value
537 << "'. Original address in object file"
538 << " is " << (*entry)["val"].value;
539 end_loc.set_comment(end_comment.str());
540 end_sym.location = end_loc;
541
542 auto end_sym_entry = symbol_table.insert(end_sym);
543 if(!end_sym_entry.second)
544 end_sym_entry.first = end_sym;
545 }
546 }
547
548 // We've added every linker-defined symbol that marks the start or end of a
549 // region. But there might be other linker-defined symbols with some random
550 // address. These will have been declared extern too, so we need to give them
551 // a value also. Here, we give them the actual value that they have in the
552 // object file, since we're not assigning any object to them.
553 for(const auto &d : to_json_array(data["addresses"]))
554 {
555 auto it=linker_values.find(irep_idt(d["sym"].value));
556 if(it!=linker_values.end())
557 // sym marks the start or end of a region; already dealt with.
558 continue;
559
560 // Perhaps this is a size symbol for a section whose size we truncated
561 // earlier.
563 const auto &pair=truncated_symbols.find(d["sym"].value);
564 if(pair==truncated_symbols.end())
565 symbol_value=d["val"].value;
566 else
567 {
568 log.debug()
569 << "Truncating the value of symbol " << d["sym"].value << " from "
570 << d["val"].value << " to " << MAX_FLATTENED_ARRAY_SIZE
571 << " because it corresponds to the size of a too-large section."
572 << messaget::eom;
574 }
575
578 loc.set_comment("linker script-defined symbol: char *"+
579 d["sym"].value+"="+"(char *)"+id2string(symbol_value)+"u;");
580
581 constant_exprt rhs(
584 unsigned_int_type().get_width()),
586
588
589 symbolt &symbol = symbol_table.get_writeable_ref(d["sym"].value);
590 symbol.is_extern = false;
591 symbol.is_static_lifetime = true;
592 symbol.location = loc;
593 symbol.type = pointer_type(char_type());
594 symbol.value = rhs_tc;
595
596 linker_values.emplace(
597 irep_idt(d["sym"].value), std::make_pair(symbol.symbol_expr(), rhs_tc));
598 }
599 return 0;
600}
601#else
602{
604 for(const auto &d : to_json_array(data["regions"]))
605 {
606 unsigned start=safe_string2unsigned(d["start"].value);
607 unsigned size=safe_string2unsigned(d["size"].value);
608 constant_exprt first=from_integer(start, size_type());
609 constant_exprt second=from_integer(size, size_type());
610 const code_typet void_t({}, empty_typet());
612 symbol_exprt(CPROVER_PREFIX "allocated_memory", void_t), {first, second});
613
615 loc.set_file(linker_script);
616 loc.set_comment("linker script-defined region:\n"+d["commt"].value+":\n"+
617 d["annot"].value);
618 f.add_source_location()=loc;
619
621 i.make_function_call(f);
622 initialize_instructions.push_front(i);
623 }
624
625 if(!symbol_table.has_symbol(CPROVER_PREFIX "allocated_memory"))
626 {
627 symbolt sym{
628 CPROVER_PREFIX "allocated_memory",
629 code_typet({}, empty_typet()),
630 ID_C} sym.pretty_name = CPROVER_PREFIX "allocated_memory";
631 sym.is_lvalue=sym.is_static_lifetime=true;
632 symbol_table.add(sym);
633 }
634
635 for(const auto &d : to_json_array(data["addresses"]))
636 {
639 loc.set_comment("linker script-defined symbol: char *"+
640 d["sym"].value+"="+"(char *)"+d["val"].value+"u;");
641
642 symbol_exprt lhs(d["sym"].value, pointer_type(char_type()));
643
644 constant_exprt rhs;
646 string2integer(d["val"].value), unsigned_int_type().get_width()));
647 rhs.type()=unsigned_int_type();
648
649 exprt rhs_tc =
651
652 linker_values.emplace(
653 irep_idt(d["sym"].value), std::make_pair(lhs, rhs_tc));
654
655 code_assignt assign(lhs, rhs_tc);
656 assign.add_source_location()=loc;
658 assign_i.make_assignment(assign);
660 }
661 return 0;
662}
663#endif
664
666 std::list<irep_idt> &linker_defined_symbols,
667 const symbol_tablet &symbol_table,
668 const std::string &out_file,
669 const std::string &def_out_file)
670{
671 for(auto const &pair : symbol_table.symbols)
672 {
673 if(
674 pair.second.is_extern && pair.second.value.is_nil() &&
675 pair.second.name != CPROVER_PREFIX "memory")
676 {
677 linker_defined_symbols.push_back(pair.second.name);
678 }
679 }
680
681 std::ostringstream linker_def_str;
682 std::copy(
685 std::ostream_iterator<irep_idt>(linker_def_str, "\n"));
686 log.debug() << "Linker-defined symbols: [" << linker_def_str.str() << "]\n"
687 << messaget::eom;
688
689 temporary_filet linker_def_infile("goto-cc-linker-defs", "");
690 std::ofstream linker_def_file(linker_def_infile());
692 linker_def_file.close();
693
694 std::vector<std::string> argv=
695 {
696 "ls_parse.py",
697 "--script", cmdline.get_value('T'),
698 "--object", out_file,
699 "--sym-file", linker_def_infile(),
700 "--out-file", def_out_file
701 };
702
704 argv.push_back("--very-verbose");
706 argv.push_back("--verbose");
707
708 log.debug() << "RUN:";
709 for(std::size_t i=0; i<argv.size(); i++)
710 log.debug() << " " << argv[i];
712
713 int rc = run(argv[0], argv, linker_def_infile(), def_out_file, "");
714 if(rc!=0)
715 log.warning() << "Problem parsing linker script" << messaget::eom;
716
717 return rc;
718}
719
721 const std::list<irep_idt> &linker_defined_symbols,
723{
724 int fail=0;
725 for(const auto &sym : linker_defined_symbols)
726 if(linker_values.find(sym)==linker_values.end())
727 {
728 log.warning() << "Variable '" << sym
729 << "' was declared extern but never given a value, even in "
730 << "a linker script" << messaget::eom;
731
734 linker_values.emplace(sym, std::make_pair(null_sym, null_pointer));
735 }
736
737 for(const auto &pair : linker_values)
738 {
739 auto it=std::find(linker_defined_symbols.begin(),
740 linker_defined_symbols.end(), pair.first);
741 if(it==linker_defined_symbols.end())
742 {
743 fail=1;
744 log.error()
745 << "Linker script-defined symbol '" << pair.first << "' was "
746 << "either defined in the C source code, not declared extern in "
747 << "the C source code, or does not appear in the C source code"
748 << messaget::eom;
749 }
750 }
751 return fail;
752}
753
755{
756 if(!data.is_object())
757 return true;
758
760 return (
761 !(data_object.find("regions") != data_object.end() &&
762 data_object.find("addresses") != data_object.end() &&
763 data["regions"].is_array() && data["addresses"].is_array() &&
764 std::all_of(
765 to_json_array(data["addresses"]).begin(),
766 to_json_array(data["addresses"]).end(),
767 [](const jsont &j) {
768 if(!j.is_object())
769 return false;
770
771 const json_objectt &address = to_json_object(j);
772 return address.find("val") != address.end() &&
773 address.find("sym") != address.end() &&
774 address["val"].is_number() && address["sym"].is_string();
775 }) &&
776 std::all_of(
777 to_json_array(data["regions"]).begin(),
778 to_json_array(data["regions"]).end(),
779 [](const jsont &j) {
780 if(!j.is_object())
781 return false;
782
784 return region.find("start") != region.end() &&
785 region.find("size") != region.end() &&
786 region.find("annot") != region.end() &&
787 region.find("commt") != region.end() &&
788 region.find("start-symbol") != region.end() &&
789 region.find("has-end-symbol") != region.end() &&
790 region.find("section") != region.end() &&
791 region["start"].is_number() && region["size"].is_number() &&
792 region["annot"].is_string() &&
793 region["start-symbol"].is_string() &&
794 region["section"].is_string() && region["commt"].is_string() &&
795 ((region["has-end-symbol"].is_true() &&
796 region.find("end-symbol") != region.end() &&
797 region["end-symbol"].is_string()) ||
798 (region["has-end-symbol"].is_false() &&
799 region.find("size-symbol") != region.end() &&
800 region.find("end-symbol") == region.end() &&
801 region["size-symbol"].is_string()));
802 })));
803}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
std::string array_name(const namespacet &ns, const exprt &expr)
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:41
unsignedbv_typet size_type()
Definition c_types.cpp:55
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
bitvector_typet char_type()
Definition c_types.cpp:111
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Arrays with given size.
Definition std_types.h:763
A goto_instruction_codet representing an assignment in the program.
goto_instruction_codet representation of a function call statement.
Base type of functions.
Definition std_types.h:539
static bool write_bin_object_file(const std::string &file_name, const goto_modelt &src_goto_model, bool validate_goto_model, message_handlert &message_handler)
Writes the goto functions of src_goto_model to a binary format object file.
Definition compile.cpp:565
A constant literal expression.
Definition std_expr.h:2942
void set_value(const irep_idt &value)
Definition std_expr.h:2955
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:223
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
std::list< instructiont > instructionst
Array index operator.
Definition std_expr.h:1410
const irep_idt & id() const
Definition irep.h:396
arrayt::iterator end()
Definition json.h:251
arrayt::iterator begin()
Definition json.h:236
iterator find(const std::string &key)
Definition json.h:356
iterator end()
Definition json.h:386
Definition json.h:27
bool is_number() const
Definition json.h:51
std::string value
Definition json.h:132
bool is_string() const
Definition json.h:46
bool is_object() const
Definition json.h:56
linker_script_merget(const std::string &elf_binary, const std::string &goto_binary, const cmdlinet &, message_handlert &)
int pointerize_linker_defined_symbols(goto_modelt &, const linker_valuest &)
convert the type of linker script-defined symbols to char*
void symbols_to_pointerize(const linker_valuest &linker_values, const exprt &expr, std::list< symbol_exprt > &to_pointerize) const
fill to_pointerize with names of linker symbols appearing in expr
int add_linker_script_definitions()
Add values of linkerscript-defined symbols to the goto-binary.
const std::string & elf_binary
int get_linker_script_data(std::list< irep_idt > &linker_defined_symbols, const symbol_tablet &symbol_table, const std::string &out_file, const std::string &def_out_file)
Write linker script definitions to linker_data.
std::map< irep_idt, std::pair< symbol_exprt, exprt > > linker_valuest
int goto_and_object_mismatch(const std::list< irep_idt > &linker_defined_symbols, linker_valuest &linker_values)
one-to-one correspondence between extern & linker symbols
int ls_data2instructions(jsont &data, const std::string &linker_script, symbol_tablet &symbol_table, linker_valuest &linker_values)
Write a list of definitions derived from data into the symbol_table.
int pointerize_subexprs_of(exprt &expr, std::list< symbol_exprt > &to_pointerize, const linker_valuest &linker_values)
std::list< replacement_predicatet > replacement_predicates
The "shapes" of expressions to be replaced by a pointer.
int replace_expr(exprt &old_expr, const linker_valuest &linker_values, const symbol_exprt &old_symbol, const irep_idt &ident, const std::string &shape)
do the actual replacement of an expr with a new pointer expr
int linker_data_is_malformed(const jsont &data) const
Validate output of the scripts/ls_parse.py tool.
const std::string & goto_binary
unsigned get_verbosity() const
Definition message.h:54
source_locationt source_location
Definition message.h:247
mstreamt & error() const
Definition message.h:399
mstreamt & debug() const
Definition message.h:429
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
@ M_DEBUG
Definition message.h:171
@ M_RESULT
Definition message.h:170
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The null pointer constant.
The plus expression Associativity is not specified.
Definition std_expr.h:947
Patterns of expressions that should be replaced.
void set_comment(const irep_idt &comment)
void set_file(const irep_idt &file)
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The symbol table.
virtual iteratort begin() override
virtual iteratort end() override
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition symbol.h:28
bool is_extern
Definition symbol.h:74
bool is_static_lifetime
Definition symbol.h:70
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
exprt value
Initial value of symbol.
Definition symbol.h:34
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
Compile and link source and object files.
void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent)
#define CPROVER_PREFIX
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
Goto Programs with Functions.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
json_objectt & to_json_object(jsont &json)
Definition json.h:444
json_arrayt & to_json_array(jsont &json)
Definition json.h:426
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
Merge linker script-defined symbols into a goto-program.
bool is_false(const literalt &l)
Definition literal.h:197
Magic numbers used throughout the codebase.
const std::size_t MAX_FLATTENED_ARRAY_SIZE
Definition magic.h:11
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
Read Goto Programs.
int run(const std::string &what, const std::vector< std::string > &argv)
Definition run.cpp:48
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
void recreate_initialize_function(goto_modelt &goto_model, message_handlert &message_handler)
Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto m...
#define INITIALIZE_FUNCTION
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
unsigned safe_string2unsigned(const std::string &str, int base)
Definition kdev_t.h:24
Definition kdev_t.h:19
static bool failed(bool error_indicator)
typename detail::make_voidt< typest... >::type void_t
Definition type_traits.h:35
dstringt irep_idt