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/symbol_table.h>
16 #include <util/config.h>
17 #include <util/std_expr.h>
18 
19 #include "goto_model.h"
20 
21 class message_handlert;
22 
29 {
30 public:
32  symbol_tablet &_symbol_table,
33  message_handlert &_message_handler);
34 
35  void operator()(goto_programt &dest);
36  void operator()(goto_functionst &dest);
37 
38 protected:
39  const std::string arg_suffix;
40  std::string sym_suffix;
45 
46  typedef ::std::map< typet, typet > abstraction_types_mapt;
48 
49  ::std::set< irep_idt > current_args;
50 
51  static bool has_string_macros(const exprt &expr);
52 
54  exprt &expr,
55  bool lhs,
56  const source_locationt &);
57 
58  void move_lhs_arithmetic(exprt &lhs, exprt &rhs);
59 
60  bool is_char_type(const typet &type) const
61  {
62  if(type.id()!=ID_signedbv &&
63  type.id()!=ID_unsignedbv)
64  return false;
65 
67  }
68 
69  bool is_ptr_string_struct(const typet &type) const;
70 
71  void make_type(exprt &dest, const typet &type)
72  {
73  if(dest.is_not_nil() &&
74  ns.follow(dest.type())!=ns.follow(type))
75  dest = typecast_exprt(dest, type);
76  }
77 
78  goto_programt::targett abstract(
86 
88  goto_programt &dest,
90  const exprt &new_lhs,
91  const exprt &lhs,
92  const exprt &rhs);
93 
95 
98  const exprt &lhs, const exprt &rhs);
99 
101  goto_programt &dest,
102  goto_programt::targett target,
103  const exprt &lhs, const if_exprt &rhs);
104 
106  goto_programt &dest,
107  goto_programt::targett target,
108  const exprt &lhs, const exprt &rhs);
109 
110  enum class whatt { IS_ZERO, LENGTH, SIZE };
111 
112  static typet build_type(whatt what);
113  exprt build(
114  const exprt &pointer,
115  whatt what,
116  bool write,
117  const source_locationt &);
118 
119  bool build(const exprt &object, exprt &dest, bool write);
120  bool build_wrap(const exprt &object, exprt &dest, bool write);
121  bool build_if(const if_exprt &o_if, exprt &dest, bool write);
122  bool build_array(const array_exprt &object, exprt &dest, bool write);
123  bool build_symbol(const symbol_exprt &sym, exprt &dest);
124  bool build_symbol_constant(const mp_integer &zero_length,
125  const mp_integer &buf_size, exprt &dest);
126 
127  exprt build_unknown(whatt what, bool write);
128  exprt build_unknown(const typet &type, bool write);
129  const typet &build_abstraction_type(const typet &type);
130  const typet &build_abstraction_type_rec(const typet &type,
131  const abstraction_types_mapt &known);
132  bool build_pointer(const exprt &object, exprt &dest, bool write);
133  void build_new_symbol(const symbolt &symbol,
134  const irep_idt &identifier, const typet &type);
135 
136  exprt member(const exprt &a, whatt what);
137 
140 
141  typedef std::unordered_map<irep_idt, irep_idt> localst;
143 
144  void abstract(goto_programt &dest);
145 
146  void add_str_arguments(
147  const irep_idt &name,
149 
150  void add_argument(
151  code_typet::parameterst &str_args,
152  const symbolt &fct_symbol,
153  const typet &type,
154  const irep_idt &base_name,
155  const irep_idt &identifier);
156 
158  const irep_idt &identifier, const irep_idt &source_sym);
159 
161  goto_programt::targett ref_instr,
162  const symbolt &symbol, const typet &source_type);
163 
165  goto_programt &dest,
166  goto_programt::targett ref_instr,
167  const symbolt &symbol,
168  const irep_idt &component_name,
169  const typet &type,
170  const typet &source_type);
171 
173 };
174 
175 // keep track of length of strings
176 
177 void string_abstraction(
178  goto_modelt &,
179  message_handlert &);
180 
181 void string_abstraction(
182  symbol_tablet &,
184  goto_functionst &);
185 
186 #endif // CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H
Array constructor from list of elements.
Definition: std_expr.h:1382
std::size_t get_width() const
Definition: std_types.h:1048
std::vector< parametert > parameterst
Definition: std_types.h:746
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.
::goto_functiont goto_functiont
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
instructionst::iterator targett
Definition: goto_program.h:550
The trinary if-then-else operator.
Definition: std_expr.h:2087
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Replace all uses of char * by a struct that carries that string, and also the underlying allocation a...
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)
const std::string arg_suffix
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::set< irep_idt > current_args
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)
void add_str_arguments(const irep_idt &name, goto_functionst::goto_functiont &fct)
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)
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)
void add_argument(code_typet::parameterst &str_args, const symbolt &fct_symbol, const typet &type, const irep_idt &base_name, 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)
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:81
The symbol table.
Definition: symbol_table.h:20
Symbol table entry.
Definition: symbol.h:28
Semantic type conversion.
Definition: std_expr.h:1781
The type of an expression, extends irept.
Definition: type.h:28
configt config
Definition: config.cpp:24
Symbol Table + CFG.
BigInt mp_integer
Definition: mp_arith.h:19
API to expression classes.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1096
void string_abstraction(goto_modelt &, message_handlert &)
std::size_t char_width
Definition: config.h:114
Author: Diffblue Ltd.