CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 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)
405should be necessary. The rest of this file converts expressions containing the
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: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:3117
void set_value(const irep_idt &value)
Definition std_expr.h:3130
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: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: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