CBMC
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
22
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 {
139 return to_symbol_expr(
140 to_index_expr(to_address_of_expr(expr).object()).array());
141 },
142 [](const exprt &expr)
143 {
144 return expr.id() == ID_address_of &&
145 expr.type().id() == ID_pointer &&
146
147 to_address_of_expr(expr).object().id() == ID_index &&
148 to_address_of_expr(expr).object().type().id() ==
150
151 to_index_expr(to_address_of_expr(expr).object())
152 .array()
153 .id() == ID_symbol &&
154 to_index_expr(to_address_of_expr(expr).object())
155 .array()
156 .type()
157 .id() == ID_array &&
158
159 to_index_expr(to_address_of_expr(expr).object())
160 .index()
161 .is_constant() &&
162 to_index_expr(to_address_of_expr(expr).object())
163 .index()
164 .type()
165 .id() == ID_signedbv;
166 }),
168 "address of array",
169 [](const exprt &expr) -> const symbol_exprt &
170 { return to_symbol_expr(to_address_of_expr(expr).object()); },
171 [](const exprt &expr)
172 {
173 return expr.id() == ID_address_of &&
174 expr.type().id() == ID_pointer &&
175
176 to_address_of_expr(expr).object().id() == ID_symbol &&
177 to_address_of_expr(expr).object().type().id() == ID_array;
178 }),
180 "address of struct",
181 [](const exprt &expr) -> const symbol_exprt &
182 { return to_symbol_expr(to_address_of_expr(expr).object()); },
183 [](const exprt &expr)
184 {
185 return expr.id() == ID_address_of &&
186 expr.type().id() == ID_pointer &&
187
188 to_address_of_expr(expr).object().id() == ID_symbol &&
189 (to_address_of_expr(expr).object().type().id() == ID_struct ||
190 to_address_of_expr(expr).object().type().id() ==
192 }),
194 "array variable",
195 [](const exprt &expr) -> const symbol_exprt &
196 { return to_symbol_expr(expr); },
197 [](const exprt &expr)
198 { return expr.id() == ID_symbol && expr.type().id() == ID_array; }),
200 "pointer (does not need pointerizing)",
201 [](const exprt &expr) -> const symbol_exprt &
202 { return to_symbol_expr(expr); },
203 [](const exprt &expr)
204 { return expr.id() == ID_symbol && expr.type().id() == ID_pointer; })})
205{}
206
208 goto_modelt &goto_model,
210{
211 const namespacet ns(goto_model.symbol_table);
212
213 int ret=0;
214
215 // Next, find all occurrences of linker-defined symbols that are _values_
216 // of some symbol in the symbol table, and pointerize them too
217 for(auto it = goto_model.symbol_table.begin();
218 it != goto_model.symbol_table.end();
219 ++it)
220 {
221 std::list<symbol_exprt> to_pointerize;
223
224 if(to_pointerize.empty())
225 continue;
226 log.debug() << "Pointerizing the symbol-table value of symbol " << it->first
227 << messaget::eom;
229 it.get_writeable_symbol().value, to_pointerize, linker_values);
230 if(to_pointerize.empty() && fail==0)
231 continue;
232 ret=1;
233 for(const auto &sym : to_pointerize)
234 {
235 log.error() << " Could not pointerize '" << sym.get_identifier()
236 << "' in symbol table entry " << it->first << ". Pretty:\n"
237 << sym.pretty() << "\n";
238 }
240 }
241
242 // Finally, pointerize all occurrences of linker-defined symbols in the
243 // goto program
244 for(auto &gf : goto_model.goto_functions.function_map)
245 {
246 goto_programt &program=gf.second.body;
247 for(auto &instruction : program.instructions)
248 {
249 std::list<exprt *> expressions = {&instruction.code_nonconst()};
250 if(instruction.has_condition())
251 expressions.push_back(&instruction.condition_nonconst());
252
253 for(exprt *insts : expressions)
254 {
255 std::list<symbol_exprt> to_pointerize;
257 if(to_pointerize.empty())
258 continue;
259 log.debug() << "Pointerizing a program expression..." << messaget::eom;
261 if(to_pointerize.empty() && fail==0)
262 continue;
263 ret=1;
264 for(const auto &sym : to_pointerize)
265 {
266 log.error() << " Could not pointerize '" << sym.get_identifier()
267 << "' in function " << gf.first << ". Pretty:\n"
268 << sym.pretty() << "\n";
269 log.error().source_location = instruction.source_location();
270 }
272 }
273 }
274 }
275 return ret;
276}
277
281 const symbol_exprt &old_symbol,
282 const irep_idt &ident,
283 const std::string &shape)
284{
285 auto it=linker_values.find(ident);
286 if(it==linker_values.end())
287 {
288 log.error() << "Could not find a new expression for linker script-defined "
289 << "symbol '" << ident << "'" << messaget::eom;
290 return 1;
291 }
292 symbol_exprt new_expr=it->second.first;
293 new_expr.add_source_location()=old_symbol.source_location();
294 log.debug() << "Pointerizing linker-defined symbol '" << ident
295 << "' of shape <" << shape << ">." << messaget::eom;
297 return 0;
298}
299
301 exprt &expr,
302 std::list<symbol_exprt> &to_pointerize,
304{
305 int fail=0, tmp=0;
306 for(auto const &pair : linker_values)
307 for(auto const &pattern : replacement_predicates)
308 {
309 if(!pattern.match(expr))
310 continue;
311 // take a copy, expr will be changed below
312 const symbol_exprt inner_symbol=pattern.inner_symbol(expr);
313 if(pair.first!=inner_symbol.get_identifier())
314 continue;
315 tmp=replace_expr(expr, linker_values, inner_symbol, pair.first,
316 pattern.description());
318 auto result=std::find(to_pointerize.begin(), to_pointerize.end(),
319 inner_symbol);
320 if(result==to_pointerize.end())
321 {
322 fail=1;
323 log.error() << "Too many removals of '" << inner_symbol.get_identifier()
324 << "'" << messaget::eom;
325 }
326 else
327 to_pointerize.erase(result);
328 // If we get here, we've just pointerized this expression. That expression
329 // will be a symbol possibly wrapped in some unary junk, but won't contain
330 // other symbols as subexpressions that might need to be pointerized. So
331 // it's safe to bail out here.
332 return fail;
333 }
334
335 for(auto &op : expr.operands())
336 {
339 }
340 return fail;
341}
342
345 const exprt &expr,
346 std::list<symbol_exprt> &to_pointerize) const
347{
348 for(const auto &op : expr.operands())
349 {
350 if(op.id()!=ID_symbol)
351 continue;
353 const auto &pair=linker_values.find(sym_exp.get_identifier());
354 if(pair!=linker_values.end())
355 to_pointerize.push_back(sym_exp);
356 }
357 for(const auto &op : expr.operands())
359}
360
361#if 0
362The current implementation of this function is less precise than the
365
366Suppose we have a section in the linker script, 100 bytes long, where the
367address of the symbol sec_start is the start of the section (value 4096) and the
368address of sec_end is the end of that section (value 4196).
369
370The current implementation synthesizes the goto-version of the following C:
371
372 char __sec_array[100];
373 char *sec_start=(&__sec_array[0]);
374 char *sec_end=((&__sec_array[0])+100);
375 // Yes, it is 100 not 99. We're pointing to the end of the memory occupied
376 // by __sec_array, not the last element of __sec_array.
377
378This is imprecise for the following reason: the actual address of the array and
379the pointers shall be some random CBMC-internal address, instead of being 4096
381position of the section, and we even know what the actual values of sec_start
382and sec_end are from the object file (these values are in the `addresses` list
383of the `data` argument to this function). If the correctness of the code depends
384on these actual values, then CBMCs model of the code is too imprecise to verify
385this.
386
387The commented-out version of this function below synthesizes the following:
388
389 char *sec_start=4096;
390 char *sec_end=4196;
392
393This code has both the actual addresses of the start and end of the section and
394tells CBMC that the intermediate region is valid. However, the allocated_memory
395macro does not currently allocate an actual object at the address 4096, so
396symbolic execution can fail. In particular, the 'allocated memory' is part of
399do not have know n size. The commented-out implementation should be reinstated
401
402In either case, no other changes to the rest of the code (outside this function)
403should be necessary. The rest of this file converts expressions containing the
404linker-defined symbol into pointer types if they were not already, and this is
406#endif
408 jsont &data,
409 const std::string &linker_script,
410 symbol_tablet &symbol_table,
412#if 1
413{
414 std::map<irep_idt, std::size_t> truncated_symbols;
415 for(auto &d : to_json_array(data["regions"]))
416 {
417 bool has_end=d["has-end-symbol"].is_true();
418
419 std::ostringstream array_name;
420 array_name << CPROVER_PREFIX << "linkerscript-array_"
421 << d["start-symbol"].value;
422 if(has_end)
423 array_name << "-" << d["end-symbol"].value;
424
425
426 // Array symbol_exprt
427 mp_integer array_size = string2integer(d["size"].value);
429 {
430 log.warning() << "Object section '" << d["section"].value << "' of size "
431 << array_size << " is too large to model. Truncating to "
432 << MAX_FLATTENED_ARRAY_SIZE << " bytes" << messaget::eom;
434 if(!has_end)
435 truncated_symbols[d["size-symbol"].value]=MAX_FLATTENED_ARRAY_SIZE;
436 }
437
440
442 array_loc.set_file(linker_script);
443 std::ostringstream array_comment;
444 array_comment << "Object section '" << d["section"].value << "' of size "
445 << array_size << " bytes";
446 array_loc.set_comment(array_comment.str());
447
448 namespacet ns(symbol_table);
449 const auto zi = zero_initializer(array_type, array_loc, ns);
450 CHECK_RETURN(zi.has_value());
451
452 // Add the array to the symbol table.
454 array_sym.is_static_lifetime = true;
455 array_sym.is_lvalue = true;
456 array_sym.is_state_var = true;
457 array_sym.value = *zi;
458 array_sym.location = array_loc;
459
460 bool failed = symbol_table.add(array_sym);
462
463 // Array start address
466
467 // Linker-defined symbol_exprt pointing to start address
468 symbolt start_sym{d["start-symbol"].value, pointer_type(char_type()), ID_C};
469 start_sym.is_static_lifetime = true;
470 start_sym.is_lvalue = true;
471 start_sym.is_state_var = true;
472 start_sym.value = array_start;
473 linker_values.emplace(
474 d["start-symbol"].value,
475 std::make_pair(start_sym.symbol_expr(), array_start));
476
477 // Since the value of the pointer will be a random CBMC address, write a
478 // note about the real address in the object file
479 auto it = std::find_if(
480 to_json_array(data["addresses"]).begin(),
481 to_json_array(data["addresses"]).end(),
482 [&d](const jsont &add) {
483 return add["sym"].value == d["start-symbol"].value;
484 });
485 if(it == to_json_array(data["addresses"]).end())
486 {
487 log.error() << "Start: Could not find address corresponding to symbol '"
488 << d["start-symbol"].value << "' (start of section)"
489 << messaget::eom;
490 return 1;
491 }
493 start_loc.set_file(linker_script);
494 std::ostringstream start_comment;
495 start_comment << "Pointer to beginning of object section '"
496 << d["section"].value << "'. Original address in object file"
497 << " is " << (*it)["val"].value;
498 start_loc.set_comment(start_comment.str());
499 start_sym.location = start_loc;
500
501 auto start_sym_entry = symbol_table.insert(start_sym);
502 if(!start_sym_entry.second)
504
505 if(has_end) // Same for pointer to end of array
506 {
508
509 symbolt end_sym{d["end-symbol"].value, pointer_type(char_type()), ID_C};
510 end_sym.is_static_lifetime = true;
511 end_sym.is_lvalue = true;
512 end_sym.is_state_var = true;
513 end_sym.value = array_end;
514 linker_values.emplace(
515 d["end-symbol"].value,
516 std::make_pair(end_sym.symbol_expr(), array_end));
517
518 auto entry = std::find_if(
519 to_json_array(data["addresses"]).begin(),
520 to_json_array(data["addresses"]).end(),
521 [&d](const jsont &add) {
522 return add["sym"].value == d["end-symbol"].value;
523 });
524 if(entry == to_json_array(data["addresses"]).end())
525 {
526 log.debug() << "Could not find address corresponding to symbol '"
527 << d["end-symbol"].value << "' (end of section)"
528 << messaget::eom;
529 return 1;
530 }
532 end_loc.set_file(linker_script);
533 std::ostringstream end_comment;
534 end_comment << "Pointer to end of object section '" << d["section"].value
535 << "'. Original address in object file"
536 << " is " << (*entry)["val"].value;
537 end_loc.set_comment(end_comment.str());
538 end_sym.location = end_loc;
539
540 auto end_sym_entry = symbol_table.insert(end_sym);
541 if(!end_sym_entry.second)
542 end_sym_entry.first = end_sym;
543 }
544 }
545
546 // We've added every linker-defined symbol that marks the start or end of a
547 // region. But there might be other linker-defined symbols with some random
548 // address. These will have been declared extern too, so we need to give them
549 // a value also. Here, we give them the actual value that they have in the
550 // object file, since we're not assigning any object to them.
551 for(const auto &d : to_json_array(data["addresses"]))
552 {
553 auto it=linker_values.find(irep_idt(d["sym"].value));
554 if(it!=linker_values.end())
555 // sym marks the start or end of a region; already dealt with.
556 continue;
557
558 // Perhaps this is a size symbol for a section whose size we truncated
559 // earlier.
561 const auto &pair=truncated_symbols.find(d["sym"].value);
562 if(pair==truncated_symbols.end())
563 symbol_value=d["val"].value;
564 else
565 {
566 log.debug()
567 << "Truncating the value of symbol " << d["sym"].value << " from "
568 << d["val"].value << " to " << MAX_FLATTENED_ARRAY_SIZE
569 << " because it corresponds to the size of a too-large section."
570 << messaget::eom;
572 }
573
576 loc.set_comment("linker script-defined symbol: char *"+
577 d["sym"].value+"="+"(char *)"+id2string(symbol_value)+"u;");
578
579 constant_exprt rhs(
582 unsigned_int_type().get_width()),
584
586
587 symbolt &symbol = symbol_table.get_writeable_ref(d["sym"].value);
588 symbol.is_extern = false;
589 symbol.is_static_lifetime = true;
590 symbol.location = loc;
591 symbol.type = pointer_type(char_type());
592 symbol.value = rhs_tc;
593
594 linker_values.emplace(
595 irep_idt(d["sym"].value), std::make_pair(symbol.symbol_expr(), rhs_tc));
596 }
597 return 0;
598}
599#else
600{
602 for(const auto &d : to_json_array(data["regions"]))
603 {
604 unsigned start=safe_string2unsigned(d["start"].value);
605 unsigned size=safe_string2unsigned(d["size"].value);
606 constant_exprt first=from_integer(start, size_type());
607 constant_exprt second=from_integer(size, size_type());
608 const code_typet void_t({}, empty_typet());
610 symbol_exprt(CPROVER_PREFIX "allocated_memory", void_t), {first, second});
611
613 loc.set_file(linker_script);
614 loc.set_comment("linker script-defined region:\n"+d["commt"].value+":\n"+
615 d["annot"].value);
616 f.add_source_location()=loc;
617
619 i.make_function_call(f);
620 initialize_instructions.push_front(i);
621 }
622
623 if(!symbol_table.has_symbol(CPROVER_PREFIX "allocated_memory"))
624 {
625 symbolt sym{
626 CPROVER_PREFIX "allocated_memory",
627 code_typet({}, empty_typet()),
628 ID_C} sym.pretty_name = CPROVER_PREFIX "allocated_memory";
629 sym.is_lvalue=sym.is_static_lifetime=true;
630 symbol_table.add(sym);
631 }
632
633 for(const auto &d : to_json_array(data["addresses"]))
634 {
637 loc.set_comment("linker script-defined symbol: char *"+
638 d["sym"].value+"="+"(char *)"+d["val"].value+"u;");
639
640 symbol_exprt lhs(d["sym"].value, pointer_type(char_type()));
641
642 constant_exprt rhs;
644 string2integer(d["val"].value), unsigned_int_type().get_width()));
645 rhs.type()=unsigned_int_type();
646
647 exprt rhs_tc =
649
650 linker_values.emplace(
651 irep_idt(d["sym"].value), std::make_pair(lhs, rhs_tc));
652
653 code_assignt assign(lhs, rhs_tc);
654 assign.add_source_location()=loc;
656 assign_i.make_assignment(assign);
658 }
659 return 0;
660}
661#endif
662
664 std::list<irep_idt> &linker_defined_symbols,
665 const symbol_tablet &symbol_table,
666 const std::string &out_file,
667 const std::string &def_out_file)
668{
669 for(auto const &pair : symbol_table.symbols)
670 {
671 if(
672 pair.second.is_extern && pair.second.value.is_nil() &&
673 pair.second.name != CPROVER_PREFIX "memory")
674 {
675 linker_defined_symbols.push_back(pair.second.name);
676 }
677 }
678
679 std::ostringstream linker_def_str;
680 std::copy(
683 std::ostream_iterator<irep_idt>(linker_def_str, "\n"));
684 log.debug() << "Linker-defined symbols: [" << linker_def_str.str() << "]\n"
685 << messaget::eom;
686
687 temporary_filet linker_def_infile("goto-cc-linker-defs", "");
688 std::ofstream linker_def_file(linker_def_infile());
690 linker_def_file.close();
691
692 std::vector<std::string> argv=
693 {
694 "ls_parse.py",
695 "--script", cmdline.get_value('T'),
696 "--object", out_file,
697 "--sym-file", linker_def_infile(),
698 "--out-file", def_out_file
699 };
700
702 argv.push_back("--very-verbose");
704 argv.push_back("--verbose");
705
706 log.debug() << "RUN:";
707 for(std::size_t i=0; i<argv.size(); i++)
708 log.debug() << " " << argv[i];
710
711 int rc = run(argv[0], argv, linker_def_infile(), def_out_file, "");
712 if(rc!=0)
713 log.warning() << "Problem parsing linker script" << messaget::eom;
714
715 return rc;
716}
717
719 const std::list<irep_idt> &linker_defined_symbols,
721{
722 int fail=0;
723 for(const auto &sym : linker_defined_symbols)
724 if(linker_values.find(sym)==linker_values.end())
725 {
726 log.warning() << "Variable '" << sym
727 << "' was declared extern but never given a value, even in "
728 << "a linker script" << messaget::eom;
729
732 linker_values.emplace(sym, std::make_pair(null_sym, null_pointer));
733 }
734
735 for(const auto &pair : linker_values)
736 {
737 auto it=std::find(linker_defined_symbols.begin(),
738 linker_defined_symbols.end(), pair.first);
739 if(it==linker_defined_symbols.end())
740 {
741 fail=1;
742 log.error()
743 << "Linker script-defined symbol '" << pair.first << "' was "
744 << "either defined in the C source code, not declared extern in "
745 << "the C source code, or does not appear in the C source code"
746 << messaget::eom;
747 }
748 }
749 return fail;
750}
751
753{
754 if(!data.is_object())
755 return true;
756
758 return (
759 !(data_object.find("regions") != data_object.end() &&
760 data_object.find("addresses") != data_object.end() &&
761 data["regions"].is_array() && data["addresses"].is_array() &&
762 std::all_of(
763 to_json_array(data["addresses"]).begin(),
764 to_json_array(data["addresses"]).end(),
765 [](const jsont &j) {
766 if(!j.is_object())
767 return false;
768
769 const json_objectt &address = to_json_object(j);
770 return address.find("val") != address.end() &&
771 address.find("sym") != address.end() &&
772 address["val"].is_number() && address["sym"].is_string();
773 }) &&
774 std::all_of(
775 to_json_array(data["regions"]).begin(),
776 to_json_array(data["regions"]).end(),
777 [](const jsont &j) {
778 if(!j.is_object())
779 return false;
780
782 return region.find("start") != region.end() &&
783 region.find("size") != region.end() &&
784 region.find("annot") != region.end() &&
785 region.find("commt") != region.end() &&
786 region.find("start-symbol") != region.end() &&
787 region.find("has-end-symbol") != region.end() &&
788 region.find("section") != region.end() &&
789 region["start"].is_number() && region["size"].is_number() &&
790 region["annot"].is_string() &&
791 region["start-symbol"].is_string() &&
792 region["section"].is_string() && region["commt"].is_string() &&
793 ((region["has-end-symbol"].is_true() &&
794 region.find("end-symbol") != region.end() &&
795 region["end-symbol"].is_string()) ||
796 (region["has-end-symbol"].is_false() &&
797 region.find("size-symbol") != region.end() &&
798 region.find("end-symbol") == region.end() &&
799 region["size-symbol"].is_string()));
800 })));
801}
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:36
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
bitvector_typet char_type()
Definition c_types.cpp:106
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:562
Arrays with given size.
Definition std_types.h:807
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:583
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:574
A constant literal expression.
Definition std_expr.h:3118
void set_value(const irep_idt &value)
Definition std_expr.h:3131
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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:231
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:1470
const irep_idt & id() const
Definition irep.h:388
arrayt::iterator end()
Definition json.h:251
arrayt::iterator begin()
Definition json.h:236
iterator find(const std::string &key)
Definition json.h:354
iterator end()
Definition json.h:384
Definition json.h:27
bool is_array() const
Definition json.h:61
bool is_number() const
Definition json.h:51
std::string value
Definition json.h:132
void output(std::ostream &out) const
Definition json.h:90
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:53
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:391
mstreamt & debug() const
Definition message.h:421
message_handlert & get_message_handler()
Definition message.h:183
mstreamt & warning() const
Definition message.h:396
@ M_DEBUG
Definition message.h:170
@ M_RESULT
Definition message.h:169
static eomt eom
Definition message.h:289
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:1002
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:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
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:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
Compile and link source and object files.
void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent)
#define CPROVER_PREFIX
std::optional< 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:44
json_objectt & to_json_object(jsont &json)
Definition json.h:442
json_arrayt & to_json_array(jsont &json)
Definition json.h:424
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
double log(double x)
Definition math.c:2449
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:49
#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:1538
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
long random(void)
Definition stdlib.c:630
unsigned safe_string2unsigned(const std::string &str, int base)
void * memset(void *s, int c, size_t n)
Definition string.c:713
void * memcpy(void *dst, const void *src, size_t n)
Definition string.c:613
static bool failed(bool error_indicator)
#define size_type
Definition unistd.c:186
dstringt irep_idt