cprover
string_abstraction.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String Abstraction
4 
5 Author: 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 
15 #include <util/bitvector_types.h>
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 
25 class goto_functionst;
26 class goto_modelt;
27 class message_handlert;
28 
35 {
36 public:
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 
54 protected:
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 
91  goto_programt::targett abstract(
99 
101  goto_programt &dest,
102  goto_programt::targett target,
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,
115  goto_programt::targett target,
116  const exprt &lhs, const if_exprt &rhs);
117 
119  goto_programt &dest,
120  goto_programt::targett target,
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 
160  void add_str_parameters(
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 
189 void string_abstraction(
190  goto_modelt &,
191  message_handlert &);
192 
193 DEPRECATED(
194  SINCE(2020, 12, 14, "Use string_abstraction(goto_model, message_handler)"))
195 void string_abstraction(
196  symbol_tablet &,
198  goto_functionst &);
199 
200 #endif // CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
string_abstractiont::string_abstractiont
string_abstractiont(symbol_tablet &_symbol_table, message_handlert &_message_handler)
Definition: string_abstraction.cpp:86
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
string_abstractiont::member
exprt member(const exprt &a, whatt what)
Definition: string_abstraction.cpp:1356
string_abstractiont::build_type
static typet build_type(whatt what)
Definition: string_abstraction.cpp:105
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
string_abstractiont::build
exprt build(const exprt &pointer, whatt what, bool write, const source_locationt &)
Definition: string_abstraction.cpp:637
string_abstractiont::abstract_assign
goto_programt::targett abstract_assign(goto_programt &dest, goto_programt::targett it)
Definition: string_abstraction.cpp:515
string_abstraction
void string_abstraction(goto_modelt &, message_handlert &)
Definition: string_abstraction.cpp:78
typet
The type of an expression, extends irept.
Definition: type.h:28
string_abstractiont::build_pointer
bool build_pointer(const exprt &object, exprt &dest, bool write)
Definition: string_abstraction.cpp:879
string_abstractiont::abstraction_types_map
abstraction_types_mapt abstraction_types_map
Definition: string_abstraction.h:62
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
string_abstractiont::string_struct
typet string_struct
Definition: string_abstraction.h:151
string_abstractiont::whatt::LENGTH
@ LENGTH
string_abstractiont::locals
localst locals
Definition: string_abstraction.h:155
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
string_abstractiont::build_abstraction_type_rec
const typet & build_abstraction_type_rec(const typet &type, const abstraction_types_mapt &known)
Definition: string_abstraction.cpp:693
configt::ansi_c
struct configt::ansi_ct ansi_c
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
string_abstractiont::is_ptr_string_struct
bool is_ptr_string_struct(const typet &type) const
Definition: string_abstraction.cpp:59
namespace.h
string_abstractiont::add_parameter
code_typet::parametert add_parameter(const symbolt &fct_symbol, const typet &type, const irep_idt &identifier)
Definition: string_abstraction.cpp:213
string_abstractiont::abstract_function_call
void abstract_function_call(goto_programt::targett it)
Definition: string_abstraction.cpp:543
string_abstractiont::abstract_char_assign
goto_programt::targett abstract_char_assign(goto_programt &dest, goto_programt::targett it)
Definition: string_abstraction.cpp:1143
string_abstractiont::value_assignments
goto_programt::targett value_assignments(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt &rhs)
Definition: string_abstraction.cpp:1238
string_abstractiont::make_type
void make_type(exprt &dest, const typet &type)
Definition: string_abstraction.h:84
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:113
string_abstractiont::is_char_type
bool is_char_type(const typet &type) const
Definition: string_abstraction.h:73
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
string_abstractiont::whatt
whatt
Definition: string_abstraction.h:123
string_abstractiont::sym_suffix
std::string sym_suffix
Definition: string_abstraction.h:55
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
string_abstractiont::abstraction_types_mapt
::std::map< typet, typet > abstraction_types_mapt
Definition: string_abstraction.h:61
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
string_abstractiont::has_string_macros
static bool has_string_macros(const exprt &expr)
Definition: string_abstraction.cpp:592
string_abstractiont::symbol_table
symbol_tablet & symbol_table
Definition: string_abstraction.h:56
string_abstractiont
Replace all uses of char * by a struct that carries that string, and also the underlying allocation a...
Definition: string_abstraction.h:35
string_abstractiont::build_unknown
exprt build_unknown(whatt what, bool write)
Definition: string_abstraction.cpp:911
string_abstractiont::whatt::SIZE
@ SIZE
deprecate.h
string_abstractiont::declare_define_locals
void declare_define_locals(goto_programt &dest)
Definition: string_abstraction.cpp:260
bitvector_types.h
Pre-defined bitvector types.
string_abstractiont::make_val_or_dummy_rec
exprt make_val_or_dummy_rec(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const typet &source_type)
Definition: string_abstraction.cpp:326
string_abstractiont::add_dummy_symbol_and_value
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)
Definition: string_abstraction.cpp:397
string_abstractiont::parameter_map
localst parameter_map
Definition: string_abstraction.h:156
string_abstractiont::ns
namespacet ns
Definition: string_abstraction.h:57
string_abstractiont::build_new_symbol
void build_new_symbol(const symbolt &symbol, const irep_idt &identifier, const typet &type)
Definition: string_abstraction.cpp:1002
string_abstractiont::build_abstraction_type
const typet & build_abstraction_type(const typet &type)
Definition: string_abstraction.cpp:674
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
string_abstractiont::char_assign
goto_programt::targett char_assign(goto_programt &dest, goto_programt::targett target, const exprt &new_lhs, const exprt &lhs, const exprt &rhs)
Definition: string_abstraction.cpp:1206
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
string_abstractiont::value_assignments_if
goto_programt::targett value_assignments_if(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const if_exprt &rhs)
Definition: string_abstraction.cpp:1285
string_abstractiont::initialization
goto_programt initialization
Definition: string_abstraction.h:152
string_abstractiont::build_wrap
bool build_wrap(const exprt &object, exprt &dest, bool write)
Definition: string_abstraction.cpp:28
string_abstractiont::replace_string_macros
void replace_string_macros(exprt &expr, bool lhs, const source_locationt &)
Definition: string_abstraction.cpp:606
config
configt config
Definition: config.cpp:25
source_locationt
Definition: source_location.h:19
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:843
string_abstractiont::add_str_parameters
void add_str_parameters(symbolt &fct_symbol, goto_functiont::parameter_identifierst &parameter_identifiers)
Definition: string_abstraction.cpp:186
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
string_abstractiont::abstract_pointer_assign
goto_programt::targett abstract_pointer_assign(goto_programt &dest, goto_programt::targett it)
Definition: string_abstraction.cpp:1103
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
string_abstractiont::temporary_counter
unsigned temporary_counter
Definition: string_abstraction.h:58
symbolt
Symbol table entry.
Definition: symbol.h:28
string_abstractiont::build_symbol_constant
bool build_symbol_constant(const mp_integer &zero_length, const mp_integer &buf_size, exprt &dest)
Definition: string_abstraction.cpp:1034
string_abstractiont::make_decl_and_def
void make_decl_and_def(goto_programt &dest, goto_programt::targett ref_instr, const irep_idt &identifier, const irep_idt &source_sym)
Definition: string_abstraction.cpp:295
code_typet::parametert
Definition: std_types.h:556
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
string_abstractiont::whatt::IS_ZERO
@ IS_ZERO
config.h
goto_functiont::parameter_identifierst
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:28
string_abstractiont::build_array
bool build_array(const array_exprt &object, exprt &dest, bool write)
Definition: string_abstraction.cpp:853
string_abstractiont::move_lhs_arithmetic
void move_lhs_arithmetic(exprt &lhs, exprt &rhs)
Definition: string_abstraction.cpp:1077
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
string_abstractiont::build_if
bool build_if(const if_exprt &o_if, exprt &dest, bool write)
Definition: string_abstraction.cpp:825
string_abstractiont::localst
std::unordered_map< irep_idt, irep_idt > localst
Definition: string_abstraction.h:154
std_expr.h
API to expression classes.
string_abstractiont::message_handler
message_handlert & message_handler
Definition: string_abstraction.h:59
string_abstractiont::operator()
void operator()(goto_programt &dest)
Definition: string_abstraction.cpp:176
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1467
goto_function.h
Goto Function.
string_abstractiont::build_symbol
bool build_symbol(const symbol_exprt &sym, exprt &dest)
Definition: string_abstraction.cpp:962
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646
string_abstractiont::value_assignments_string_struct
goto_programt::targett value_assignments_string_struct(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt &rhs)
Definition: string_abstraction.cpp:1316
string_abstractiont::apply
void apply(goto_modelt &goto_model)
Apply string abstraction to goto_model.
Definition: string_abstraction.cpp:121