cprover
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/deprecate.h>
18#include <util/namespace.h>
19#include <util/std_expr.h>
20
21#include "goto_function.h"
22
23#include <map>
24
25class goto_functionst;
26class goto_modelt;
28
35{
36public:
37 // To be deprecated once the operator() methods have been removed, at which
38 // point a new constructor that only takes a message_handler should be
39 // introduced.
41 symbol_tablet &_symbol_table,
42 message_handlert &_message_handler);
43
44 DEPRECATED(SINCE(2020, 12, 14, "Use apply(goto_modelt &)"))
45 void operator()(goto_programt &dest);
46 DEPRECATED(SINCE(2020, 12, 14, "Use apply(goto_modelt &)"))
47 void operator()(goto_functionst &dest);
48
52 void apply(goto_modelt &goto_model);
53
54protected:
55 std::string sym_suffix;
60
61 typedef ::std::map< typet, typet > abstraction_types_mapt;
63
64 static bool has_string_macros(const exprt &expr);
65
67 exprt &expr,
68 bool lhs,
69 const source_locationt &);
70
71 void move_lhs_arithmetic(exprt &lhs, exprt &rhs);
72
73 bool is_char_type(const typet &type) const
74 {
75 if(type.id()!=ID_signedbv &&
76 type.id()!=ID_unsignedbv)
77 return false;
78
80 }
81
82 bool is_ptr_string_struct(const typet &type) const;
83
84 void make_type(exprt &dest, const typet &type)
85 {
86 if(dest.is_not_nil() &&
87 ns.follow(dest.type())!=ns.follow(type))
88 dest = typecast_exprt(dest, type);
89 }
90
99
101 goto_programt &dest,
103 const exprt &new_lhs,
104 const exprt &lhs,
105 const exprt &rhs);
106
108
111 const exprt &lhs, const exprt &rhs);
112
114 goto_programt &dest,
116 const exprt &lhs, const if_exprt &rhs);
117
119 goto_programt &dest,
121 const exprt &lhs, const exprt &rhs);
122
123 enum class whatt { IS_ZERO, LENGTH, SIZE };
124
125 static typet build_type(whatt what);
126 exprt build(
127 const exprt &pointer,
128 whatt what,
129 bool write,
130 const source_locationt &);
131
132 bool build(const exprt &object, exprt &dest, bool write);
133 bool build_wrap(const exprt &object, exprt &dest, bool write);
134 bool build_if(const if_exprt &o_if, exprt &dest, bool write);
135 bool build_array(const array_exprt &object, exprt &dest, bool write);
136 bool build_symbol(const symbol_exprt &sym, exprt &dest);
137 bool build_symbol_constant(const mp_integer &zero_length,
138 const mp_integer &buf_size, exprt &dest);
139
140 exprt build_unknown(whatt what, bool write);
141 exprt build_unknown(const typet &type, bool write);
142 const typet &build_abstraction_type(const typet &type);
143 const typet &build_abstraction_type_rec(const typet &type,
144 const abstraction_types_mapt &known);
145 bool build_pointer(const exprt &object, exprt &dest, bool write);
146 void build_new_symbol(const symbolt &symbol,
147 const irep_idt &identifier, const typet &type);
148
149 exprt member(const exprt &a, whatt what);
150
153
154 typedef std::unordered_map<irep_idt, irep_idt> localst;
157
158 void abstract(goto_programt &dest);
159
161 symbolt &fct_symbol,
162 goto_functiont::parameter_identifierst &parameter_identifiers);
163
165 const symbolt &fct_symbol,
166 const typet &type,
167 const irep_idt &identifier);
168
170 const irep_idt &identifier, const irep_idt &source_sym);
171
173 goto_programt::targett ref_instr,
174 const symbolt &symbol, const typet &source_type);
175
177 goto_programt &dest,
178 goto_programt::targett ref_instr,
179 const symbolt &symbol,
180 const irep_idt &component_name,
181 const typet &type,
182 const typet &source_type);
183
185};
186
187// keep track of length of strings
188
190 goto_modelt &,
192
194 SINCE(2020, 12, 14, "Use string_abstraction(goto_model, message_handler)"))
199
200#endif // CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H
Pre-defined bitvector types.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Array constructor from list of elements.
Definition: std_expr.h:1476
std::size_t get_width() const
Definition: std_types.h:864
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:37
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
A collection of goto functions.
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:28
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:592
The trinary if-then-else operator.
Definition: std_expr.h:2226
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
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)
string_abstractiont(symbol_tablet &_symbol_table, message_handlert &_message_handler)
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 initialization
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)
void apply(goto_modelt &goto_model)
Apply string abstraction to goto_model.
bool build_symbol(const symbol_exprt &sym, exprt &dest)
void move_lhs_arithmetic(exprt &lhs, exprt &rhs)
void operator()(goto_programt &dest)
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)
void make_type(exprt &dest, const typet &type)
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
symbol_tablet & symbol_table
const typet & build_abstraction_type(const typet &type)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
configt config
Definition: config.cpp:25
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
#define DEPRECATED(msg)
Definition: deprecate.h:23
Goto Function.
BigInt mp_integer
Definition: smt_terms.h:12
API to expression classes.
void string_abstraction(goto_modelt &, message_handlert &)
std::size_t char_width
Definition: config.h:112