cprover
Loading...
Searching...
No Matches
analyze_symbol.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbol Analyzer
4
5Author: Malte Mues <mail.mues@gmail.com>
6 Daniel Poetzl
7
8\*******************************************************************/
9
10#include "analyze_symbol.h"
11
12#include <util/c_types.h>
13#include <util/c_types_util.h>
15#include <util/pointer_expr.h>
17#include <util/string2int.h>
19#include <util/string_utils.h>
20
21#include <climits>
22#include <cstdlib>
23
26 const std::vector<std::string> &args)
27 : gdb_api(args),
30 c_converter(ns, expr2c_configurationt::clean_configuration),
32{
33}
34
36 const memory_addresst &begin,
37 const mp_integer &byte_size,
38 const irep_idt &name)
39 : // the address is given in hex, starting with 0x....
41 safe_string2size_t(std::string_view{begin.address_string}.substr(2), 16)),
43 name(name)
44{
45 PRECONDITION(begin.address_string.substr(0, 2) == "0x");
46}
47
49 const memory_addresst &point) const
50{
51 // the address is given in hex, starting with 0x....
52 PRECONDITION(point.address_string.substr(0, 2) == "0x");
53 return safe_string2size_t(
54 std::string_view{point.address_string}.substr(2), 16);
55}
56
57mp_integer gdb_value_extractort::memory_scopet::distance(
58 const memory_addresst &point,
59 mp_integer member_size) const
60{
61 auto point_int = address2size_t(point);
62 CHECK_RETURN(check_containment(point_int));
63 return (point_int - begin_int) / member_size;
64}
65
66std::vector<gdb_value_extractort::memory_scopet>::iterator
68{
69 return std::find_if(
72 [&name](const memory_scopet &scope) { return scope.id() == name; });
73}
74
75std::vector<gdb_value_extractort::memory_scopet>::iterator
77{
78 return std::find_if(
81 [&point](const memory_scopet &memory_scope) {
82 return memory_scope.contains(point);
83 });
84}
85
87{
88 const auto scope_it = find_dynamic_allocation(name);
89 if(scope_it == dynamically_allocated.end())
90 return 1;
91 else
92 return scope_it->size();
93}
94
95std::optional<std::string> gdb_value_extractort::get_malloc_pointee(
96 const memory_addresst &point,
97 mp_integer member_size)
98{
99 const auto scope_it = find_dynamic_allocation(point);
100 if(scope_it == dynamically_allocated.end())
101 return {};
102
103 const auto pointer_distance = scope_it->distance(point, member_size);
104 return id2string(scope_it->id()) +
105 (pointer_distance > 0 ? "+" + integer2string(pointer_distance) : "");
106}
107
109{
110 const auto maybe_size = pointer_offset_bits(type, ns);
111 CHECK_RETURN(maybe_size.has_value());
112 return *maybe_size / CHAR_BIT;
113}
114
116 const std::list<std::string> &symbols)
117{
118 // record addresses of given symbols
119 for(const auto &id : symbols)
120 {
121 const symbolt &symbol = ns.lookup(id);
122 if(
123 symbol.type.id() != ID_pointer ||
125 {
126 const symbol_exprt &symbol_expr = ns.lookup(id).symbol_expr();
127 const address_of_exprt aoe(symbol_expr);
128
129 const std::string c_expr = c_converter.convert(aoe);
130 const pointer_valuet &value = gdb_api.get_memory(c_expr);
131 CHECK_RETURN(value.pointee.empty() || (id == value.pointee));
132
133 memory_map[id] = value;
134 }
135 else
136 {
137 const std::string c_symbol = c_converter.convert(symbol.symbol_expr());
138 const pointer_valuet &symbol_value = gdb_api.get_memory(c_symbol);
139 size_t symbol_size = gdb_api.query_malloc_size(c_symbol);
140
141 if(symbol_size > 1)
142 dynamically_allocated.emplace_back(
143 symbol_value.address, symbol_size, id);
144 memory_map[id] = symbol_value;
145 }
146 }
147
148 for(const auto &id : symbols)
149 {
150 analyze_symbol(id);
151 }
152}
153
155{
156 const symbolt &symbol = ns.lookup(symbol_name);
157 const symbol_exprt symbol_expr = symbol.symbol_expr();
158
159 try
160 {
161 const typet target_type = symbol.type;
162
163 const auto zero_expr = zero_initializer(target_type, symbol.location, ns);
164 CHECK_RETURN(zero_expr);
165
166 const exprt target_expr =
167 get_expr_value(symbol_expr, *zero_expr, symbol.location);
168
169 add_assignment(symbol_expr, target_expr);
170 }
171 catch(const gdb_interaction_exceptiont &e)
172 {
173 throw analysis_exceptiont(e.what());
174 }
175
177}
178
181{
182 code_blockt generated_code;
183
184 allocate_objects.declare_created_symbols(generated_code);
185
186 for(auto const &pair : assignments)
187 {
188 generated_code.add(code_assignt(pair.first, pair.second));
189 }
190
191 return c_converter.convert(generated_code);
192}
193
196{
197 symbol_tablet snapshot;
198
199 for(const auto &pair : assignments)
200 {
201 const symbol_exprt &symbol_expr = to_symbol_expr(pair.first);
202 const irep_idt id = symbol_expr.identifier();
203
204 INVARIANT(symbol_table.has_symbol(id), "symbol must exist in symbol table");
205
206 const symbolt &symbol = symbol_table.lookup_ref(id);
207
208 symbolt snapshot_symbol(symbol);
209 snapshot_symbol.value = pair.second;
210
211 snapshot.insert(snapshot_symbol);
212 }
213
214 // Also add type symbols to the snapshot
215 for(const auto &pair : symbol_table)
216 {
217 const symbolt &symbol = pair.second;
218
219 if(symbol.is_type)
220 {
221 snapshot.insert(symbol);
222 }
223 }
224
225 return snapshot;
226}
227
229{
230 if(assignments.count(lhs) == 0)
231 assignments.emplace(std::make_pair(lhs, value));
232}
233
235 const exprt &expr,
236 const memory_addresst &memory_location,
237 const source_locationt &location)
238{
239 PRECONDITION(expr.type().id() == ID_pointer);
241 PRECONDITION(!memory_location.is_null());
242
243 auto it = values.find(memory_location);
244
245 if(it == values.end())
246 {
247 std::string c_expr = c_converter.convert(expr);
248 pointer_valuet value = gdb_api.get_memory(c_expr);
249 CHECK_RETURN(value.string);
250
251 string_constantt init(*value.string);
253
254 symbol_exprt dummy("tmp", pointer_type(init.type()));
256
257 const symbol_exprt new_symbol =
258 to_symbol_expr(allocate_objects.allocate_automatic_local_object(
259 assignments, dummy, init.type()));
260
261 add_assignment(new_symbol, init);
262
263 values.insert(std::make_pair(memory_location, new_symbol));
264
265 // check that we are returning objects of the right type
267 to_array_type(new_symbol.type()).element_type() ==
268 to_pointer_type(expr.type()).base_type());
269 return new_symbol;
270 }
271 else
272 {
274 to_array_type(it->second.type()).element_type() ==
275 to_pointer_type(expr.type()).base_type());
276 return it->second;
277 }
278}
279
281 const exprt &expr,
282 const pointer_valuet &pointer_value,
283 const source_locationt &location)
284{
285 PRECONDITION(expr.type().id() == ID_pointer);
286 const auto &memory_location = pointer_value.address;
287 std::string memory_location_string = memory_location.string();
288 PRECONDITION(memory_location_string != "0x0");
289 PRECONDITION(!pointer_value.pointee.empty());
290
291 std::string struct_name;
292 size_t member_offset;
293 if(pointer_value.has_known_offset())
294 {
295 std::string member_offset_string;
297 pointer_value.pointee, '+', struct_name, member_offset_string, true);
298 member_offset = safe_string2size_t(member_offset_string);
299 }
300 else
301 {
302 struct_name = pointer_value.pointee;
303 member_offset = 0;
304 }
305
306 const symbolt *struct_symbol = symbol_table.lookup(struct_name);
307 DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
308
309 if(!has_known_memory_location(struct_name))
310 {
311 memory_map[struct_name] = gdb_api.get_memory(struct_name);
312 analyze_symbol(irep_idt{struct_name});
313 }
314
315 const auto &struct_symbol_expr = struct_symbol->symbol_expr();
316 if(struct_symbol->type.id() == ID_array)
317 {
318 return index_exprt{
319 struct_symbol_expr,
322 c_index_type())};
323 }
324 if(struct_symbol->type.id() == ID_pointer)
325 {
326 return dereference_exprt{
327 plus_exprt{struct_symbol_expr,
329 expr.type()}};
330 }
331
332 const auto maybe_member_expr = get_subexpression_at_offset(
333 struct_symbol_expr,
336 ns);
338 maybe_member_expr.has_value(), "structure doesn't have member");
339
340 // check that we return the right type
342 maybe_member_expr->type() == to_pointer_type(expr.type()).base_type());
343 return *maybe_member_expr;
344}
345
347 const exprt &expr,
348 const pointer_valuet &pointer_value,
349 const source_locationt &location)
350{
351 PRECONDITION(expr.type().id() == ID_pointer);
352 PRECONDITION(to_pointer_type(expr.type()).base_type().id() == ID_code);
353 PRECONDITION(!pointer_value.address.is_null());
354
355 const auto &function_name = pointer_value.pointee;
356 CHECK_RETURN(!function_name.empty());
357 const auto function_symbol = symbol_table.lookup(function_name);
358 if(function_symbol == nullptr)
359 {
361 "input source code does not contain function: " + function_name};
362 }
363 CHECK_RETURN(function_symbol->type.id() == ID_code);
364 return function_symbol->symbol_expr();
365}
366
368 const exprt &expr,
369 const pointer_valuet &value,
370 const source_locationt &location)
371{
372 PRECONDITION(expr.type().id() == ID_pointer);
374 const auto &memory_location = value.address;
375 PRECONDITION(!memory_location.is_null());
376
377 auto it = values.find(memory_location);
378
379 if(it == values.end())
380 {
381 if(!value.pointee.empty() && value.pointee != c_converter.convert(expr))
382 {
383 analyze_symbol(value.pointee);
384 const auto pointee_symbol = symbol_table.lookup(value.pointee);
385 CHECK_RETURN(pointee_symbol != nullptr);
386 const auto pointee_symbol_expr = pointee_symbol->symbol_expr();
387 return pointee_symbol_expr;
388 }
389
390 values.insert(std::make_pair(memory_location, nil_exprt()));
391
392 const typet target_type = to_pointer_type(expr.type()).base_type();
393
394 symbol_exprt dummy("tmp", expr.type());
396
397 const auto zero_expr = zero_initializer(target_type, location, ns);
398 CHECK_RETURN(zero_expr);
399
400 // Check if pointer was dynamically allocated (via malloc). If so we will
401 // replace the pointee with a static array filled with values stored at the
402 // expected positions. Since the allocated size is an over-approximation we
403 // may end up querying past the allocated bounds and building a larger array
404 // with meaningless values.
405 mp_integer allocated_size = get_malloc_size(c_converter.convert(expr));
406 // get the sizeof(target_type) and thus the number of elements
407 const auto number_of_elements = allocated_size / get_type_size(target_type);
408 if(allocated_size != 1 && number_of_elements > 1)
409 {
410 array_exprt::operandst elements;
411 // build the operands by querying for an index expression
412 for(size_t i = 0; i < number_of_elements; i++)
413 {
414 const auto sub_expr_value = get_expr_value(
416 *zero_expr,
417 location);
418 elements.push_back(sub_expr_value);
419 }
420 CHECK_RETURN(elements.size() == number_of_elements);
421
422 // knowing the number of elements we can build the type
423 const typet target_array_type =
424 array_typet{target_type, from_integer(elements.size(), c_index_type())};
425
426 array_exprt new_array{elements, to_array_type(target_array_type)};
427
428 // allocate a new symbol for the temporary static array
429 symbol_exprt array_dummy("tmp", pointer_type(target_array_type));
430 const auto array_symbol =
431 allocate_objects.allocate_automatic_local_object(
432 assignments, array_dummy, target_array_type);
433
434 // add assignment of value to newly created symbol
435 add_assignment(array_symbol, new_array);
436 values[memory_location] = array_symbol;
437 CHECK_RETURN(array_symbol.type().id() == ID_array);
438 return array_symbol;
439 }
440
441 const symbol_exprt new_symbol =
442 to_symbol_expr(allocate_objects.allocate_automatic_local_object(
443 assignments, dummy, target_type));
444
445 dereference_exprt dereference_expr(expr);
446
447 const exprt target_expr =
448 get_expr_value(dereference_expr, *zero_expr, location);
449 // add assignment of value to newly created symbol
450 add_assignment(new_symbol, target_expr);
451
452 values[memory_location] = new_symbol;
453
454 return new_symbol;
455 }
456 else
457 {
458 const auto &known_value = it->second;
459 const auto &expected_type = to_pointer_type(expr.type()).base_type();
460 if(find_dynamic_allocation(memory_location) != dynamically_allocated.end())
461 return known_value;
462 if(known_value.is_not_nil() && known_value.type() != expected_type)
463 {
464 return symbol_exprt{
465 to_symbol_expr(known_value).identifier(), expected_type};
466 }
467 return known_value;
468 }
469}
470
472 pointer_valuet &pointer_value,
473 const pointer_typet &expected_type)
474{
475 if(pointer_value.has_known_offset())
476 return true;
477
478 if(pointer_value.pointee.empty())
479 {
480 const auto maybe_pointee = get_malloc_pointee(
481 pointer_value.address, get_type_size(expected_type.base_type()));
482 if(maybe_pointee.has_value())
483 pointer_value.pointee = *maybe_pointee;
484 if(pointer_value.pointee.find("+") != std::string::npos)
485 return true;
486 }
487
488 const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee);
489 if(pointee_symbol == nullptr)
490 return false;
491 const auto &pointee_type = pointee_symbol->type;
492 return pointee_type.id() == ID_struct_tag ||
493 pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array ||
494 pointee_type.id() == ID_struct || pointee_type.id() == ID_union;
495}
496
498 const exprt &expr,
499 const exprt &zero_expr,
500 const source_locationt &location)
501{
502 PRECONDITION(zero_expr.is_constant());
503
504 PRECONDITION(expr.type().id() == ID_pointer);
505 PRECONDITION(expr.type() == zero_expr.type());
506
507 std::string c_expr = c_converter.convert(expr);
508 const auto known_pointer = memory_map.find(c_expr);
509
510 pointer_valuet value = (known_pointer == memory_map.end() ||
511 known_pointer->second.pointee == c_expr)
512 ? gdb_api.get_memory(c_expr)
513 : known_pointer->second;
514 if(!value.valid)
515 return zero_expr;
516
517 const auto memory_location = value.address;
518
519 if(!memory_location.is_null())
520 {
521 // pointers-to-char can point to members as well, e.g. char[]
522 if(points_to_member(value, to_pointer_type(expr.type())))
523 {
524 const auto target_expr =
525 get_pointer_to_member_value(expr, value, location);
526 CHECK_RETURN(target_expr.is_not_nil());
527 const address_of_exprt result_expr{target_expr};
528 CHECK_RETURN(result_expr.type() == zero_expr.type());
529 return std::move(result_expr);
530 }
531
532 // pointer to function
533 if(to_pointer_type(expr.type()).base_type().id() == ID_code)
534 {
535 const auto target_expr =
536 get_pointer_to_function_value(expr, value, location);
537 CHECK_RETURN(target_expr.is_not_nil());
538 const address_of_exprt result_expr{target_expr};
539 CHECK_RETURN(result_expr.type() == zero_expr.type());
540 return std::move(result_expr);
541 }
542
543 // non-member: split for char/non-char
544 const auto target_expr =
546 ? get_char_pointer_value(expr, memory_location, location)
547 : get_non_char_pointer_value(expr, value, location);
548
549 // postpone if we cannot resolve now
550 if(target_expr.is_nil())
551 {
552 outstanding_assignments[expr] = memory_location;
553 return zero_expr;
554 }
555
556 // the pointee was (probably) dynamically allocated (but the allocation
557 // would not be visible in the snapshot) so we pretend it is statically
558 // allocated (we have the value) and return address to the first element
559 // of the array (instead of the array as char*)
560 if(target_expr.type().id() == ID_array)
561 {
562 const auto result_indexed_expr = get_subexpression_at_offset(
563 target_expr, 0, to_pointer_type(zero_expr.type()).base_type(), ns);
564 CHECK_RETURN(result_indexed_expr.has_value());
565 if(result_indexed_expr->type() == zero_expr.type())
566 return *result_indexed_expr;
567 const address_of_exprt result_expr{*result_indexed_expr};
568 CHECK_RETURN(result_expr.type() == zero_expr.type());
569 return std::move(result_expr);
570 }
571
572 // if the types match return right away
573 if(target_expr.type() == zero_expr.type())
574 return target_expr;
575
576 // otherwise the address of target should type-match
577 const address_of_exprt result_expr{target_expr};
578 if(result_expr.type() != zero_expr.type())
579 return typecast_exprt{result_expr, zero_expr.type()};
580 return std::move(result_expr);
581 }
582
583 return zero_expr;
584}
585
587 const exprt &expr,
588 const exprt &array,
589 const source_locationt &location)
590{
591 PRECONDITION(array.id() == ID_array);
592
593 PRECONDITION(expr.type().id() == ID_array);
594 PRECONDITION(expr.type() == array.type());
595
596 exprt new_array(array);
597
598 for(size_t i = 0; i < new_array.operands().size(); ++i)
599 {
600 const index_exprt index_expr(expr, from_integer(i, c_index_type()));
601
602 exprt &operand = new_array.operands()[i];
603
604 operand = get_expr_value(index_expr, operand, location);
605 }
606
607 return new_array;
608}
609
611 const exprt &expr,
612 const exprt &zero_expr,
613 const source_locationt &location)
614{
615 PRECONDITION(expr.type() == zero_expr.type());
616
617 const typet &type = expr.type();
618 PRECONDITION(type.id() != ID_struct);
619
620 if(is_c_integral_type(type))
621 {
622 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
623
624 std::string c_expr = c_converter.convert(expr);
625 const auto maybe_value = gdb_api.get_value(c_expr);
626 if(!maybe_value.has_value())
627 return zero_expr;
628 const std::string value = *maybe_value;
629
630 const mp_integer int_rep = string2integer(value);
631
632 return from_integer(int_rep, type);
633 }
634 else if(is_c_char_type(type))
635 {
636 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
637
638 // check the char-value and return as bitvector-type value
639 std::string c_expr = c_converter.convert(expr);
640 const auto maybe_value = gdb_api.get_value(c_expr);
641 if(!maybe_value.has_value() || maybe_value->empty())
642 return zero_expr;
643 const std::string value = *maybe_value;
644
645 const mp_integer int_rep = value[0];
646 return from_integer(int_rep, type);
647 }
648 else if(type.id() == ID_c_bool)
649 {
650 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
651
652 std::string c_expr = c_converter.convert(expr);
653 const auto maybe_value = gdb_api.get_value(c_expr);
654 if(!maybe_value.has_value())
655 return zero_expr;
656 const std::string value = *maybe_value;
657
658 return from_c_boolean_value(id2boolean(value), type);
659 }
660 else if(type.id() == ID_c_enum)
661 {
662 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
663
664 std::string c_expr = c_converter.convert(expr);
665 const auto maybe_value = gdb_api.get_value(c_expr);
666 if(!maybe_value.has_value())
667 return zero_expr;
668 const std::string value = *maybe_value;
669
671 }
672 else if(type.id() == ID_struct_tag)
673 {
674 return get_struct_value(expr, zero_expr, location);
675 }
676 else if(type.id() == ID_array)
677 {
678 return get_array_value(expr, zero_expr, location);
679 }
680 else if(type.id() == ID_pointer)
681 {
682 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
683
684 return get_pointer_value(expr, zero_expr, location);
685 }
686 else if(type.id() == ID_union_tag)
687 {
688 return get_union_value(expr, zero_expr, location);
689 }
691}
692
694 const exprt &expr,
695 const exprt &zero_expr,
696 const source_locationt &location)
697{
698 PRECONDITION(zero_expr.id() == ID_struct);
699
700 PRECONDITION(expr.type().id() == ID_struct_tag);
701 PRECONDITION(expr.type() == zero_expr.type());
702
703 exprt new_expr(zero_expr);
704
705 const struct_tag_typet &struct_tag_type = to_struct_tag_type(expr.type());
706 const struct_typet &struct_type = ns.follow_tag(struct_tag_type);
707
708 for(size_t i = 0; i < new_expr.operands().size(); ++i)
709 {
710 const struct_typet::componentt &component = struct_type.components()[i];
711
713 component.type().id() != ID_code,
714 "struct member must not be of code type");
715 if(component.get_is_padding())
716 {
717 continue;
718 }
719
720 exprt &operand = new_expr.operands()[i];
721 member_exprt member_expr(expr, component);
722
723 operand = get_expr_value(member_expr, operand, location);
724 }
725
726 return new_expr;
727}
728
730 const exprt &expr,
731 const exprt &zero_expr,
732 const source_locationt &location)
733{
734 PRECONDITION(zero_expr.id() == ID_union);
735
736 PRECONDITION(expr.type().id() == ID_union_tag);
737 PRECONDITION(expr.type() == zero_expr.type());
738
739 exprt new_expr(zero_expr);
740
741 const union_tag_typet &union_tag_type = to_union_tag_type(expr.type());
742 const union_typet &union_type = ns.follow_tag(union_tag_type);
743
744 CHECK_RETURN(new_expr.operands().size() == 1);
745 const union_typet::componentt &component = union_type.components()[0];
746 auto &operand = new_expr.operands()[0];
747 operand = get_expr_value(member_exprt{expr, component}, operand, location);
748 return new_expr;
749}
750
752{
753 for(const auto &pair : outstanding_assignments)
754 {
755 const address_of_exprt aoe(values[pair.second]);
756 add_assignment(pair.first, aoe);
757 }
758}
759
761{
762 std::string c_expr = c_converter.convert(expr);
763 const auto maybe_value = gdb_api.get_value(c_expr);
764 CHECK_RETURN(maybe_value.has_value());
765 return *maybe_value;
766}
High-level interface to gdb.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
unsignedbv_typet size_type()
Definition c_types.cpp:50
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
bitvector_typet c_index_type()
Definition c_types.cpp:16
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
This file contains functions, that should support test for underlying c types, in cases where this is...
bool is_c_integral_type(const typet &type)
This function checks, whether the type has been some kind of integer type in the c program.
bool id2boolean(const std::string &bool_value)
Convert id to a Boolean value.
constant_exprt from_c_boolean_value(bool bool_value, const typet &type)
This function creates a constant representing either 0 or 1 as value of type type.
constant_exprt convert_member_name_to_enum_value(const irep_idt &member_name, const c_enum_typet &c_enum)
This function creates a constant representing the bitvector encoded integer value of a string in the ...
bool is_c_char_type(const typet &type)
This function checks, whether this has been a char type in the c program.
Operator to return the address of an object.
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Array constructor from list of elements.
Definition std_expr.h:1570
Arrays with given size.
Definition std_types.h:806
bool is_complete() const
Definition std_types.h:851
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:826
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition std_code.h:130
void add(const codet &code)
Definition std_code.h:168
virtual std::string what() const
A human readable description of what went wrong.
Operator to dereference a pointer.
Base class for all expressions.
Definition expr.h:57
std::vector< exprt > operandst
Definition expr.h:59
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:213
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
std::string get_gdb_value(const exprt &expr)
Extract a stringified value from and c-converted expr.
exprt get_pointer_to_member_value(const exprt &expr, const pointer_valuet &pointer_value, const source_locationt &location)
Call get_subexpression_at_offset to get the correct member expression.
allocate_objectst allocate_objects
std::map< irep_idt, pointer_valuet > memory_map
Keep track of the memory location for the analyzed symbols.
std::map< exprt, memory_addresst > outstanding_assignments
Mapping pointer expression for which get_non_char_pointer_value returned nil expression to memory loc...
gdb_apit::pointer_valuet pointer_valuet
void analyze_symbol(const irep_idt &symbol_name)
Assign the gdb-extracted value for symbol_name to its symbol expression and then process outstanding ...
bool has_known_memory_location(const irep_idt &id) const
exprt get_char_pointer_value(const exprt &expr, const memory_addresst &memory_location, const source_locationt &location)
If memory_location is found among values then return the symbol expression associated with it.
exprt get_pointer_to_function_value(const exprt &expr, const pointer_valuet &pointer_value, const source_locationt &location)
Extract the function name from pointer_value, check it has a symbol and return the associated symbol ...
void process_outstanding_assignments()
Call add_assignment for each pair in outstanding_assignments.
exprt get_array_value(const exprt &expr, const exprt &array, const source_locationt &location)
Iterate over array and fill its operands with the results of calling get_expr_value on index expressi...
void add_assignment(const exprt &lhs, const exprt &value)
Create assignment lhs := value (see analyze_symbol).
std::vector< memory_scopet > dynamically_allocated
Keep track of the dynamically allocated memory.
std::map< exprt, exprt > assignments
Sequence of assignments collected during analyze_symbols.
std::string get_snapshot_as_c_code()
Get memory snapshot as C code.
std::map< memory_addresst, exprt > values
Storing pairs <address, symbol> such that at address is stored the value of symbol.
gdb_value_extractort(const symbol_table_baset &symbol_table, const std::vector< std::string > &args)
exprt get_expr_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
Case analysis on the typet of expr 1) For integers, booleans, and enums: call gdb_apit::get_value dir...
mp_integer get_type_size(const typet &type) const
Build the pointee string for address point assuming it points to a dynamic allocation of `n' elements...
void analyze_symbols(const std::list< std::string > &symbols)
For each input symbol in symbols: map its value address to its symbol_exprt (via the values map) and ...
bool points_to_member(pointer_valuet &pointer_value, const pointer_typet &expected_type)
Analyzes the pointer_value to decide if it point to a struct or a union (or array).
mp_integer get_malloc_size(irep_idt name)
Search for the size of the allocated memory for name.
exprt get_pointer_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
Call gdb_apit::get_memory on expr then split based on the points-to type being char type or not.
symbol_tablet symbol_table
External symbol table – extracted from read_goto_binary We only expect to analyse symbols located the...
exprt get_struct_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
For each of the members of the struct: call get_expr_value.
std::vector< memory_scopet >::iterator find_dynamic_allocation(irep_idt name)
Search for a memory scope allocated under name.
exprt get_union_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
For each of the members of the struct: call get_expr_value.
symbol_tablet get_snapshot_as_symbol_table()
Get memory snapshot as symbol table Build a new symbol_tablet and for each lhs symbol from collected ...
exprt get_non_char_pointer_value(const exprt &expr, const pointer_valuet &value, const source_locationt &location)
Similar to get_char_pointer_value.
gdb_apit::memory_addresst memory_addresst
const namespacet ns
Array index operator.
Definition std_expr.h:1431
Thrown when user-provided input cannot be processed.
const irep_idt & id() const
Definition irep.h:388
Extract member of struct or union.
Definition std_expr.h:2866
The NIL expression.
Definition std_expr.h:3144
The plus expression Associativity is not specified.
Definition std_expr.h:1006
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
const array_typet & type() const
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:492
Structure type, corresponds to C style structs.
Definition std_types.h:230
const componentst & components() const
Definition std_types.h:146
Expression to hold a symbol (variable).
Definition std_expr.h:132
void identifier(const irep_idt &identifier)
Definition std_expr.h:160
The symbol table base class interface.
The symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition symbol.h:28
bool is_type
Definition symbol.h:61
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:1995
The type of an expression, extends irept.
Definition type.h:29
A union tag type, i.e., union_typet with an identifier.
Definition c_types.h:199
The union type.
Definition c_types.h:147
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.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
STL namespace.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Pointer Logic.
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:291
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:221
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:517
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:887
std::size_t safe_string2size_t(std::string_view str, int base)
void split_string(std::string_view s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Used for configuring the behaviour of expr2c and type2c.
Definition expr2c.h:21
std::string string() const
Definition gdb_api.h:56
std::string address_string
Definition gdb_api.h:39
bool is_null() const
Definition gdb_api.h:48
memory_addresst address
Definition gdb_api.h:92
std::optional< std::string > string
Definition gdb_api.h:95
bool has_known_offset() const
Definition gdb_api.h:97
std::string pointee
Definition gdb_api.h:93
memory_scopet(const memory_addresst &begin, const mp_integer &byte_size, const irep_idt &name)
size_t address2size_t(const memory_addresst &point) const
Convert base-16 memory address to a natural number.
dstringt irep_idt