CBMC
Loading...
Searching...
No Matches
string_abstraction.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: String Abstraction
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H
13#define CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H
14
16#include <util/config.h>
17#include <util/namespace.h>
18#include <util/std_expr.h>
19
20#include "goto_function.h"
21
22#include <map>
23
24class goto_modelt;
26
33{
34public:
41
42 void apply();
43
44protected:
45 std::string sym_suffix;
50
51 typedef ::std::map< typet, typet > abstraction_types_mapt;
53
54 void apply(goto_programt &dest);
55
56 static bool has_string_macros(const exprt &expr);
57
59 exprt &expr,
60 bool lhs,
61 const source_locationt &);
62
63 void move_lhs_arithmetic(exprt &lhs, exprt &rhs);
64
65 bool is_char_type(const typet &type) const
66 {
67 if(type.id()!=ID_signedbv &&
68 type.id()!=ID_unsignedbv)
69 return false;
70
71 return to_bitvector_type(type).get_width()==config.ansi_c.char_width;
72 }
73
74 bool is_ptr_string_struct(const typet &type) const;
75
84
86 goto_programt &dest,
88 const exprt &new_lhs,
89 const exprt &lhs,
90 const exprt &rhs);
91
93
96 const exprt &lhs, const exprt &rhs);
97
99 goto_programt &dest,
101 const exprt &lhs, const if_exprt &rhs);
102
104 goto_programt &dest,
106 const exprt &lhs, const exprt &rhs);
107
108 enum class whatt { IS_ZERO, LENGTH, SIZE };
109
110 static typet build_type(whatt what);
111 exprt build(
112 const exprt &pointer,
113 whatt what,
114 bool write,
115 const source_locationt &);
116
117 bool build(const exprt &object, exprt &dest, bool write);
118 bool build_wrap(const exprt &object, exprt &dest, bool write);
119 bool build_if(const if_exprt &o_if, exprt &dest, bool write);
120 bool build_array(const array_exprt &object, exprt &dest, bool write);
121 bool build_symbol(const symbol_exprt &sym, exprt &dest);
123 const mp_integer &buf_size, exprt &dest);
124
125 exprt build_unknown(whatt what, bool write);
126 exprt build_unknown(const typet &type, bool write);
127 const typet &build_abstraction_type(const typet &type);
128 const typet &build_abstraction_type_rec(const typet &type,
130 bool build_pointer(const exprt &object, exprt &dest, bool write);
131 void build_new_symbol(const symbolt &symbol,
132 const irep_idt &identifier, const typet &type);
133
134 exprt member(const exprt &a, whatt what);
135
138
139 typedef std::unordered_map<irep_idt, irep_idt> localst;
142
143 void abstract(goto_programt &dest);
144
147 goto_functiont::parameter_identifierst &parameter_identifiers);
148
150 const symbolt &fct_symbol,
151 const typet &type,
152 const irep_idt &identifier);
153
155 const irep_idt &identifier, const irep_idt &source_sym);
156
159 const symbolt &symbol, const typet &source_type);
160
162 goto_programt &dest,
164 const symbolt &symbol,
165 const irep_idt &component_name,
166 const typet &type,
167 const typet &source_type);
168
170};
171
172// keep track of length of strings
173
175 goto_modelt &,
177
178#endif // CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H
configt config
Definition config.cpp:25
Pre-defined bitvector types.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Array constructor from list of elements.
Definition std_expr.h:1621
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
std::vector< irep_idt > parameter_identifierst
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
The trinary if-then-else operator.
Definition std_expr.h:2497
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Replace all uses of char * by a struct that carries that string, and also the underlying allocation a...
goto_programt::targett abstract(goto_programt &dest, goto_programt::targett it)
goto_programt::targett value_assignments_if(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const if_exprt &rhs)
goto_programt::targett value_assignments_string_struct(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt &rhs)
void declare_define_locals(goto_programt &dest)
exprt make_val_or_dummy_rec(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const typet &source_type)
bool build_symbol_constant(const mp_integer &zero_length, const mp_integer &buf_size, exprt &dest)
goto_programt::targett abstract_assign(goto_programt &dest, goto_programt::targett it)
static typet build_type(whatt what)
goto_programt::targett abstract_pointer_assign(goto_programt &dest, goto_programt::targett it)
bool build_if(const if_exprt &o_if, exprt &dest, bool write)
const typet & build_abstraction_type_rec(const typet &type, const abstraction_types_mapt &known)
void replace_string_macros(exprt &expr, bool lhs, const source_locationt &)
exprt build_unknown(whatt what, bool write)
void build_new_symbol(const symbolt &symbol, const irep_idt &identifier, const typet &type)
bool is_ptr_string_struct(const typet &type) const
message_handlert & message_handler
::std::map< typet, typet > abstraction_types_mapt
std::unordered_map< irep_idt, irep_idt > localst
goto_programt::targett value_assignments(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt &rhs)
symbol_exprt add_dummy_symbol_and_value(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const irep_idt &component_name, const typet &type, const typet &source_type)
bool build_wrap(const exprt &object, exprt &dest, bool write)
goto_programt::targett abstract_char_assign(goto_programt &dest, goto_programt::targett it)
bool build_array(const array_exprt &object, exprt &dest, bool write)
bool build_symbol(const symbol_exprt &sym, exprt &dest)
void move_lhs_arithmetic(exprt &lhs, exprt &rhs)
abstraction_types_mapt abstraction_types_map
goto_programt::targett char_assign(goto_programt &dest, goto_programt::targett target, const exprt &new_lhs, const exprt &lhs, const exprt &rhs)
code_typet::parametert add_parameter(const symbolt &fct_symbol, const typet &type, const irep_idt &identifier)
bool build_pointer(const exprt &object, exprt &dest, bool write)
void abstract_function_call(goto_programt::targett it)
exprt member(const exprt &a, whatt what)
static bool has_string_macros(const exprt &expr)
exprt build(const exprt &pointer, whatt what, bool write, const source_locationt &)
void make_decl_and_def(goto_programt &dest, goto_programt::targett ref_instr, const irep_idt &identifier, const irep_idt &source_sym)
void add_str_parameters(symbolt &fct_symbol, goto_functiont::parameter_identifierst &parameter_identifiers)
bool is_char_type(const typet &type) const
const typet & build_abstraction_type(const typet &type)
Expression to hold a symbol (variable)
Definition std_expr.h:131
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
Goto Function.
BigInt mp_integer
Definition smt_terms.h:17
API to expression classes.
void string_abstraction(goto_modelt &, message_handlert &)
ssize_t write(int fildes, const void *buf, size_t nbyte)
Definition unistd.c:195