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 : begin_int(safe_string2size_t(begin.address_string, 0)),
40 byte_size(byte_size),
41 name(name)
42{
43}
44
46 const memory_addresst &point) const
47{
48 return safe_string2size_t(point.address_string, 0);
49}
50
54{
55 auto point_int = address2size_t(point);
56 CHECK_RETURN(check_containment(point_int));
57 return (point_int - begin_int) / member_size;
58}
59
60std::vector<gdb_value_extractort::memory_scopet>::iterator
62{
63 return std::find_if(
66 [&name](const memory_scopet &scope) { return scope.id() == name; });
67}
68
69std::vector<gdb_value_extractort::memory_scopet>::iterator
71{
72 return std::find_if(
76 return memory_scope.contains(point);
77 });
78}
79
81{
82 const auto scope_it = find_dynamic_allocation(name);
84 return 1;
85 else
86 return scope_it->size();
87}
88
92{
95 return {};
96
97 const auto pointer_distance = scope_it->distance(point, member_size);
98 return id2string(scope_it->id()) +
100}
101
103{
104 const auto maybe_size = pointer_offset_bits(type, ns);
105 CHECK_RETURN(maybe_size.has_value());
106 return *maybe_size / CHAR_BIT;
107}
108
110 const std::list<std::string> &symbols)
111{
112 // record addresses of given symbols
113 for(const auto &id : symbols)
114 {
115 const symbolt &symbol = ns.lookup(id);
116 if(
117 symbol.type.id() != ID_pointer ||
118 is_c_char_type(to_pointer_type(symbol.type).base_type()))
119 {
120 const symbol_exprt &symbol_expr = ns.lookup(id).symbol_expr();
121 const address_of_exprt aoe(symbol_expr);
122
123 const std::string c_expr = c_converter.convert(aoe);
124 const pointer_valuet &value = gdb_api.get_memory(c_expr);
125 CHECK_RETURN(value.pointee.empty() || (id == value.pointee));
126
127 memory_map[id] = value;
128 }
129 else
130 {
131 const std::string c_symbol = c_converter.convert(symbol.symbol_expr());
134
135 if(symbol_size > 1)
136 dynamically_allocated.emplace_back(
137 symbol_value.address, symbol_size, id);
139 }
140 }
141
142 for(const auto &id : symbols)
143 {
144 analyze_symbol(id);
145 }
146}
147
149{
150 const symbolt &symbol = ns.lookup(symbol_name);
151 const symbol_exprt symbol_expr = symbol.symbol_expr();
152
153 try
154 {
155 const typet target_type = symbol.type;
156
157 const auto zero_expr = zero_initializer(target_type, symbol.location, ns);
158 CHECK_RETURN(zero_expr);
159
160 const exprt target_expr =
161 get_expr_value(symbol_expr, *zero_expr, symbol.location);
162
163 add_assignment(symbol_expr, target_expr);
164 }
165 catch(const gdb_interaction_exceptiont &e)
166 {
167 throw analysis_exceptiont(e.what());
168 }
169
171}
172
187
190{
192
193 for(const auto &pair : assignments)
194 {
195 const symbol_exprt &symbol_expr = to_symbol_expr(pair.first);
196 const irep_idt id = symbol_expr.get_identifier();
197
198 INVARIANT(symbol_table.has_symbol(id), "symbol must exist in symbol table");
199
200 const symbolt &symbol = symbol_table.lookup_ref(id);
201
202 symbolt snapshot_symbol(symbol);
203 snapshot_symbol.value = pair.second;
204
206 }
207
208 // Also add type symbols to the snapshot
209 for(const auto &pair : symbol_table)
210 {
211 const symbolt &symbol = pair.second;
212
213 if(symbol.is_type)
214 {
215 snapshot.insert(symbol);
216 }
217 }
218
219 return snapshot;
220}
221
223{
224 if(assignments.count(lhs) == 0)
225 assignments.emplace(std::make_pair(lhs, value));
226}
227
229 const exprt &expr,
231 const source_locationt &location)
232{
233 PRECONDITION(expr.type().id() == ID_pointer);
234 PRECONDITION(is_c_char_type(to_pointer_type(expr.type()).base_type()));
235 PRECONDITION(!memory_location.is_null());
236
237 auto it = values.find(memory_location);
238
239 if(it == values.end())
240 {
241 std::string c_expr = c_converter.convert(expr);
243 CHECK_RETURN(value.string);
244
245 string_constantt init(*value.string);
246 CHECK_RETURN(to_array_type(init.type()).is_complete());
247
248 symbol_exprt dummy("tmp", pointer_type(init.type()));
250
251 const symbol_exprt new_symbol =
253 assignments, dummy, init.type()));
254
255 add_assignment(new_symbol, init);
256
257 values.insert(std::make_pair(memory_location, new_symbol));
258
259 // check that we are returning objects of the right type
261 to_array_type(new_symbol.type()).element_type() ==
262 to_pointer_type(expr.type()).base_type());
263 return new_symbol;
264 }
265 else
266 {
268 to_array_type(it->second.type()).element_type() ==
269 to_pointer_type(expr.type()).base_type());
270 return it->second;
271 }
272}
273
275 const exprt &expr,
277 const source_locationt &location)
278{
279 PRECONDITION(expr.type().id() == ID_pointer);
280 const auto &memory_location = pointer_value.address;
281 std::string memory_location_string = memory_location.string();
283 PRECONDITION(!pointer_value.pointee.empty());
284
285 std::string struct_name;
286 size_t member_offset;
287 if(pointer_value.has_known_offset())
288 {
289 std::string member_offset_string;
291 pointer_value.pointee, '+', struct_name, member_offset_string, true);
293 }
294 else
295 {
296 struct_name = pointer_value.pointee;
297 member_offset = 0;
298 }
299
301 DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
302
304 {
307 }
308
309 const auto &struct_symbol_expr = struct_symbol->symbol_expr();
310 if(struct_symbol->type.id() == ID_array)
311 {
312 return index_exprt{
315 member_offset / get_type_size(to_pointer_type(expr.type()).base_type()),
316 c_index_type())};
317 }
318 if(struct_symbol->type.id() == ID_pointer)
319 {
320 return dereference_exprt{
323 expr.type()}};
324 }
325
329 to_pointer_type(expr.type()).base_type(),
330 ns);
332 maybe_member_expr.has_value(), "structure doesn't have member");
333
334 // check that we return the right type
336 maybe_member_expr->type() == to_pointer_type(expr.type()).base_type());
337 return *maybe_member_expr;
338}
339
341 const exprt &expr,
343 const source_locationt &location)
344{
345 PRECONDITION(expr.type().id() == ID_pointer);
346 PRECONDITION(to_pointer_type(expr.type()).base_type().id() == ID_code);
347 PRECONDITION(!pointer_value.address.is_null());
348
349 const auto &function_name = pointer_value.pointee;
350 CHECK_RETURN(!function_name.empty());
351 const auto function_symbol = symbol_table.lookup(function_name);
352 if(function_symbol == nullptr)
353 {
355 "input source code does not contain function: " + function_name};
356 }
357 CHECK_RETURN(function_symbol->type.id() == ID_code);
358 return function_symbol->symbol_expr();
359}
360
362 const exprt &expr,
363 const pointer_valuet &value,
364 const source_locationt &location)
365{
366 PRECONDITION(expr.type().id() == ID_pointer);
367 PRECONDITION(!is_c_char_type(to_pointer_type(expr.type()).base_type()));
368 const auto &memory_location = value.address;
369 PRECONDITION(!memory_location.is_null());
370
371 auto it = values.find(memory_location);
372
373 if(it == values.end())
374 {
375 if(!value.pointee.empty() && value.pointee != c_converter.convert(expr))
376 {
377 analyze_symbol(value.pointee);
378 const auto pointee_symbol = symbol_table.lookup(value.pointee);
379 CHECK_RETURN(pointee_symbol != nullptr);
380 const auto pointee_symbol_expr = pointee_symbol->symbol_expr();
381 return pointee_symbol_expr;
382 }
383
384 values.insert(std::make_pair(memory_location, nil_exprt()));
385
386 const typet target_type = to_pointer_type(expr.type()).base_type();
387
388 symbol_exprt dummy("tmp", expr.type());
390
391 const auto zero_expr = zero_initializer(target_type, location, ns);
392 CHECK_RETURN(zero_expr);
393
394 // Check if pointer was dynamically allocated (via malloc). If so we will
395 // replace the pointee with a static array filled with values stored at the
396 // expected positions. Since the allocated size is an over-approximation we
397 // may end up querying past the allocated bounds and building a larger array
398 // with meaningless values.
400 // get the sizeof(target_type) and thus the number of elements
401 const auto number_of_elements = allocated_size / get_type_size(target_type);
402 if(allocated_size != 1 && number_of_elements > 1)
403 {
404 array_exprt::operandst elements;
405 // build the operands by querying for an index expression
406 for(size_t i = 0; i < number_of_elements; i++)
407 {
408 const auto sub_expr_value = get_expr_value(
410 *zero_expr,
411 location);
412 elements.push_back(sub_expr_value);
413 }
414 CHECK_RETURN(elements.size() == number_of_elements);
415
416 // knowing the number of elements we can build the type
418 array_typet{target_type, from_integer(elements.size(), c_index_type())};
419
421
422 // allocate a new symbol for the temporary static array
424 const auto array_symbol =
427
428 // add assignment of value to newly created symbol
429 add_assignment(array_symbol, new_array);
430 values[memory_location] = array_symbol;
431 CHECK_RETURN(array_symbol.type().id() == ID_array);
432 return array_symbol;
433 }
434
435 const symbol_exprt new_symbol =
437 assignments, dummy, target_type));
438
439 dereference_exprt dereference_expr(expr);
440
441 const exprt target_expr =
442 get_expr_value(dereference_expr, *zero_expr, location);
443 // add assignment of value to newly created symbol
444 add_assignment(new_symbol, target_expr);
445
446 values[memory_location] = new_symbol;
447
448 return new_symbol;
449 }
450 else
451 {
452 const auto &known_value = it->second;
453 const auto &expected_type = to_pointer_type(expr.type()).base_type();
455 return known_value;
456 if(known_value.is_not_nil() && known_value.type() != expected_type)
457 {
458 return symbol_exprt{to_symbol_expr(known_value).get_identifier(),
460 }
461 return known_value;
462 }
463}
464
468{
469 if(pointer_value.has_known_offset())
470 return true;
471
472 if(pointer_value.pointee.empty())
473 {
475 pointer_value.address, get_type_size(expected_type.base_type()));
476 if(maybe_pointee.has_value())
477 pointer_value.pointee = *maybe_pointee;
478 if(pointer_value.pointee.find("+") != std::string::npos)
479 return true;
480 }
481
483 if(pointee_symbol == nullptr)
484 return false;
485 const auto &pointee_type = pointee_symbol->type;
486 return pointee_type.id() == ID_struct_tag ||
487 pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array ||
488 pointee_type.id() == ID_struct || pointee_type.id() == ID_union;
489}
490
492 const exprt &expr,
493 const exprt &zero_expr,
494 const source_locationt &location)
495{
496 PRECONDITION(zero_expr.is_constant());
497
498 PRECONDITION(expr.type().id() == ID_pointer);
499 PRECONDITION(expr.type() == zero_expr.type());
500
501 std::string c_expr = c_converter.convert(expr);
502 const auto known_pointer = memory_map.find(c_expr);
503
504 pointer_valuet value = (known_pointer == memory_map.end() ||
505 known_pointer->second.pointee == c_expr)
507 : known_pointer->second;
508 if(!value.valid)
509 return zero_expr;
510
511 const auto memory_location = value.address;
512
513 if(!memory_location.is_null())
514 {
515 // pointers-to-char can point to members as well, e.g. char[]
516 if(points_to_member(value, to_pointer_type(expr.type())))
517 {
518 const auto target_expr =
519 get_pointer_to_member_value(expr, value, location);
520 CHECK_RETURN(target_expr.is_not_nil());
522 CHECK_RETURN(result_expr.type() == zero_expr.type());
523 return std::move(result_expr);
524 }
525
526 // pointer to function
527 if(to_pointer_type(expr.type()).base_type().id() == ID_code)
528 {
529 const auto target_expr =
530 get_pointer_to_function_value(expr, value, location);
531 CHECK_RETURN(target_expr.is_not_nil());
533 CHECK_RETURN(result_expr.type() == zero_expr.type());
534 return std::move(result_expr);
535 }
536
537 // non-member: split for char/non-char
538 const auto target_expr =
539 is_c_char_type(to_pointer_type(expr.type()).base_type())
540 ? get_char_pointer_value(expr, memory_location, location)
541 : get_non_char_pointer_value(expr, value, location);
542
543 // postpone if we cannot resolve now
544 if(target_expr.is_nil())
545 {
547 return zero_expr;
548 }
549
550 // the pointee was (probably) dynamically allocated (but the allocation
551 // would not be visible in the snapshot) so we pretend it is statically
552 // allocated (we have the value) and return address to the first element
553 // of the array (instead of the array as char*)
554 if(target_expr.type().id() == ID_array)
555 {
557 target_expr, 0, to_pointer_type(zero_expr.type()).base_type(), ns);
559 if(result_indexed_expr->type() == zero_expr.type())
560 return *result_indexed_expr;
562 CHECK_RETURN(result_expr.type() == zero_expr.type());
563 return std::move(result_expr);
564 }
565
566 // if the types match return right away
567 if(target_expr.type() == zero_expr.type())
568 return target_expr;
569
570 // otherwise the address of target should type-match
572 if(result_expr.type() != zero_expr.type())
573 return typecast_exprt{result_expr, zero_expr.type()};
574 return std::move(result_expr);
575 }
576
577 return zero_expr;
578}
579
581 const exprt &expr,
582 const exprt &array,
583 const source_locationt &location)
584{
585 PRECONDITION(array.id() == ID_array);
586
587 PRECONDITION(expr.type().id() == ID_array);
588 PRECONDITION(expr.type() == array.type());
589
590 exprt new_array(array);
591
592 for(size_t i = 0; i < new_array.operands().size(); ++i)
593 {
595
596 exprt &operand = new_array.operands()[i];
597
599 }
600
601 return new_array;
602}
603
605 const exprt &expr,
606 const exprt &zero_expr,
607 const source_locationt &location)
608{
609 PRECONDITION(expr.type() == zero_expr.type());
610
611 const typet &type = expr.type();
612 PRECONDITION(type.id() != ID_struct);
613
614 if(is_c_integral_type(type))
615 {
616 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
617
618 std::string c_expr = c_converter.convert(expr);
619 const auto maybe_value = gdb_api.get_value(c_expr);
620 if(!maybe_value.has_value())
621 return zero_expr;
622 const std::string value = *maybe_value;
623
624 const mp_integer int_rep = string2integer(value);
625
626 return from_integer(int_rep, type);
627 }
628 else if(is_c_char_type(type))
629 {
630 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
631
632 // check the char-value and return as bitvector-type value
633 std::string c_expr = c_converter.convert(expr);
634 const auto maybe_value = gdb_api.get_value(c_expr);
635 if(!maybe_value.has_value() || maybe_value->empty())
636 return zero_expr;
637 const std::string value = *maybe_value;
638
639 const mp_integer int_rep = value[0];
640 return from_integer(int_rep, type);
641 }
642 else if(type.id() == ID_c_bool)
643 {
644 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
645
646 std::string c_expr = c_converter.convert(expr);
647 const auto maybe_value = gdb_api.get_value(c_expr);
648 if(!maybe_value.has_value())
649 return zero_expr;
650 const std::string value = *maybe_value;
651
652 return from_c_boolean_value(id2boolean(value), type);
653 }
654 else if(type.id() == ID_c_enum)
655 {
656 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
657
658 std::string c_expr = c_converter.convert(expr);
659 const auto maybe_value = gdb_api.get_value(c_expr);
660 if(!maybe_value.has_value())
661 return zero_expr;
662 const std::string value = *maybe_value;
663
665 }
666 else if(type.id() == ID_struct_tag)
667 {
668 return get_struct_value(expr, zero_expr, location);
669 }
670 else if(type.id() == ID_array)
671 {
672 return get_array_value(expr, zero_expr, location);
673 }
674 else if(type.id() == ID_pointer)
675 {
676 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
677
678 return get_pointer_value(expr, zero_expr, location);
679 }
680 else if(type.id() == ID_union_tag)
681 {
682 return get_union_value(expr, zero_expr, location);
683 }
685}
686
688 const exprt &expr,
689 const exprt &zero_expr,
690 const source_locationt &location)
691{
692 PRECONDITION(zero_expr.id() == ID_struct);
693
694 PRECONDITION(expr.type().id() == ID_struct_tag);
695 PRECONDITION(expr.type() == zero_expr.type());
696
697 exprt new_expr(zero_expr);
698
700 const struct_typet &struct_type = ns.follow_tag(struct_tag_type);
701
702 for(size_t i = 0; i < new_expr.operands().size(); ++i)
703 {
704 const struct_typet::componentt &component = struct_type.components()[i];
705
707 component.type().id() != ID_code,
708 "struct member must not be of code type");
709 if(component.get_is_padding())
710 {
711 continue;
712 }
713
714 exprt &operand = new_expr.operands()[i];
716
718 }
719
720 return new_expr;
721}
722
724 const exprt &expr,
725 const exprt &zero_expr,
726 const source_locationt &location)
727{
728 PRECONDITION(zero_expr.id() == ID_union);
729
730 PRECONDITION(expr.type().id() == ID_union_tag);
731 PRECONDITION(expr.type() == zero_expr.type());
732
733 exprt new_expr(zero_expr);
734
736 const union_typet &union_type = ns.follow_tag(union_tag_type);
737
738 CHECK_RETURN(new_expr.operands().size() == 1);
739 const union_typet::componentt &component = union_type.components()[0];
740 auto &operand = new_expr.operands()[0];
742 return new_expr;
743}
744
746{
747 for(const auto &pair : outstanding_assignments)
748 {
749 const address_of_exprt aoe(values[pair.second]);
750 add_assignment(pair.first, aoe);
751 }
752}
753
755{
756 std::string c_expr = c_converter.convert(expr);
757 const auto maybe_value = gdb_api.get_value(c_expr);
758 CHECK_RETURN(maybe_value.has_value());
759 return *maybe_value;
760}
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:562
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:1621
Arrays with given size.
Definition std_types.h:807
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:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
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:1470
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:2971
The NIL expression.
Definition std_expr.h:3208
The plus expression Associativity is not specified.
Definition std_expr.h:1002
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:493
Structure type, corresponds to C style structs.
Definition std_types.h:231
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
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:2073
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
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:97
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
std::size_t safe_string2size_t(const std::string &str, int base)
void split_string(const std::string &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
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