CBMC
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
25 const symbol_table_baset &symbol_table,
26 const std::vector<std::string> &args)
27 : gdb_api(args),
28 symbol_table(symbol_table),
29 ns(symbol_table),
30 c_converter(ns, expr2c_configurationt::clean_configuration),
31 allocate_objects(ID_C, source_locationt(), irep_idt{}, this->symbol_table)
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....
40 begin_int(
41 safe_string2size_t(std::string_view{begin.address_string}.substr(2), 16)),
42 byte_size(byte_size),
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
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(
82 return memory_scope.contains(point);
83 });
84}
85
87{
88 const auto scope_it = find_dynamic_allocation(name);
90 return 1;
91 else
92 return scope_it->size();
93}
94
98{
101 return {};
102
103 const auto pointer_distance = scope_it->distance(point, member_size);
104 return id2string(scope_it->id()) +
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 ||
124 is_c_char_type(to_pointer_type(symbol.type).base_type()))
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());
140
141 if(symbol_size > 1)
142 dynamically_allocated.emplace_back(
143 symbol_value.address, symbol_size, id);
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
193
196{
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
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,
237 const source_locationt &location)
238{
239 PRECONDITION(expr.type().id() == ID_pointer);
240 PRECONDITION(is_c_char_type(to_pointer_type(expr.type()).base_type()));
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);
249 CHECK_RETURN(value.string);
250
251 string_constantt init(*value.string);
252 CHECK_RETURN(to_array_type(init.type()).is_complete());
253
254 symbol_exprt dummy("tmp", pointer_type(init.type()));
256
257 const symbol_exprt new_symbol =
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,
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();
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);
299 }
300 else
301 {
302 struct_name = pointer_value.pointee;
303 member_offset = 0;
304 }
305
307 DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
308
310 {
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{
321 member_offset / get_type_size(to_pointer_type(expr.type()).base_type()),
322 c_index_type())};
323 }
324 if(struct_symbol->type.id() == ID_pointer)
325 {
326 return dereference_exprt{
329 expr.type()}};
330 }
331
335 to_pointer_type(expr.type()).base_type(),
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,
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);
373 PRECONDITION(!is_c_char_type(to_pointer_type(expr.type()).base_type()));
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.
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
424 array_typet{target_type, from_integer(elements.size(), c_index_type())};
425
427
428 // allocate a new symbol for the temporary static array
430 const auto array_symbol =
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 =
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();
461 return known_value;
462 if(known_value.is_not_nil() && known_value.type() != expected_type)
463 {
464 return symbol_exprt{
466 }
467 return known_value;
468 }
469}
470
474{
475 if(pointer_value.has_known_offset())
476 return true;
477
478 if(pointer_value.pointee.empty())
479 {
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
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)
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());
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());
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 =
545 is_c_char_type(to_pointer_type(expr.type()).base_type())
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 {
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 {
563 target_expr, 0, to_pointer_type(zero_expr.type()).base_type(), ns);
565 if(result_indexed_expr->type() == zero_expr.type())
566 return *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
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 {
601
602 exprt &operand = new_array.operands()[i];
603
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
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];
722
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
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];
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)
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
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
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition std_code.h:130
virtual std::string what() const
A human readable description of what went wrong.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
virtual std::string convert(const typet &src)
Definition expr2c.cpp:213
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
std::optional< std::string > get_value(const std::string &expr)
Get the memory address pointed to by the given pointer expression.
pointer_valuet get_memory(const std::string &expr)
Get the value of a pointer associated with expr.
size_t query_malloc_size(const std::string &pointer_expr)
Get the exact allocated size for a pointer pointer_expr.
Definition gdb_api.cpp:56
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...
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
Wrapper for call get_offset_pointer_bits.
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.
std::optional< std::string > get_malloc_pointee(const memory_addresst &point, mp_integer member_size)
Build the pointee string for address point assuming it points to a dynamic allocation of ā€˜n’ elements...
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.
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 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
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.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
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
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
Memory address imbued with the explicit boolean data indicating if the address is null or not.
Definition gdb_api.h:37
std::string address_string
Definition gdb_api.h:39
Data associated with the value of a pointer, i.e.
Definition gdb_api.h:77
memory_addresst address
Definition gdb_api.h:92
std::optional< std::string > string
Definition gdb_api.h:95
std::string pointee
Definition gdb_api.h:93
mp_integer distance(const memory_addresst &point, mp_integer member_size) const
Compute the distance of point from the beginning of this scope.
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.
#define size_type
Definition unistd.c:186