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/message.h>
17 #include <util/config.h>
18 #include <util/std_expr.h>
19 
20 #include "goto_functions.h"
21 
23 {
24 public:
26  symbol_tablet &_symbol_table,
27  message_handlert &_message_handler);
28 
29  void operator()(goto_programt &dest);
30  void operator()(goto_functionst &dest);
31 
32 protected:
33  const std::string arg_suffix;
34  std::string sym_suffix;
38 
39  typedef ::std::map< typet, typet > abstraction_types_mapt;
41 
42  ::std::set< irep_idt > current_args;
43 
44  static bool has_string_macros(const exprt &expr);
45 
47  exprt &expr,
48  bool lhs,
49  const source_locationt &);
50 
51  void move_lhs_arithmetic(exprt &lhs, exprt &rhs);
52 
53  bool is_char_type(const typet &type) const
54  {
55  if(type.id()==ID_symbol)
56  return is_char_type(ns.follow(type));
57 
58  if(type.id()!=ID_signedbv &&
59  type.id()!=ID_unsignedbv)
60  return false;
61 
63  }
64 
65  bool is_ptr_string_struct(const typet &type) const;
66 
67  void make_type(exprt &dest, const typet &type)
68  {
69  if(dest.is_not_nil() &&
70  ns.follow(dest.type())!=ns.follow(type))
71  dest.make_typecast(type);
72  }
73 
74  goto_programt::targett abstract(
82 
84  goto_programt &dest,
86  const exprt &new_lhs,
87  const exprt &lhs,
88  const exprt &rhs);
89 
91 
94  const exprt &lhs, const exprt &rhs);
95 
97  goto_programt &dest,
99  const exprt &lhs, const if_exprt &rhs);
100 
102  goto_programt &dest,
103  goto_programt::targett target,
104  const exprt &lhs, const exprt &rhs);
105 
106  enum class whatt { IS_ZERO, LENGTH, SIZE };
107 
108  static typet build_type(whatt what);
109  exprt build(
110  const exprt &pointer,
111  whatt what,
112  bool write,
113  const source_locationt &);
114 
115  bool build(const exprt &object, exprt &dest, bool write);
116  bool build_wrap(const exprt &object, exprt &dest, bool write);
117  bool build_if(const if_exprt &o_if, exprt &dest, bool write);
118  bool build_array(const array_exprt &object, exprt &dest, bool write);
119  bool build_symbol(const symbol_exprt &sym, exprt &dest);
120  bool build_symbol_constant(const mp_integer &zero_length,
121  const mp_integer &buf_size, exprt &dest);
122 
123  exprt build_unknown(whatt what, bool write);
124  exprt build_unknown(const typet &type, bool write);
125  const typet &build_abstraction_type(const typet &type);
126  const typet &build_abstraction_type_rec(const typet &type,
127  const abstraction_types_mapt &known);
128  bool build_pointer(const exprt &object, exprt &dest, bool write);
129  void build_new_symbol(const symbolt &symbol,
130  const irep_idt &identifier, const typet &type);
131 
132  exprt member(const exprt &a, whatt what);
133 
136 
137  typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash> localst;
139 
140  void abstract(goto_programt &dest);
141 
142  void add_str_arguments(
143  const irep_idt &name,
145 
146  void add_argument(
147  code_typet::parameterst &str_args,
148  const symbolt &fct_symbol,
149  const typet &type,
150  const irep_idt &base_name,
151  const irep_idt &identifier);
152 
154  const irep_idt &identifier, const irep_idt &source_sym);
155 
157  goto_programt::targett ref_instr,
158  const symbolt &symbol, const typet &source_type);
159 
161  goto_programt &dest,
162  goto_programt::targett ref_instr,
163  const symbolt &symbol,
164  const irep_idt &component_name,
165  const typet &type,
166  const typet &source_type);
167 
169 };
170 
171 // keep track of length of strings
172 
173 void string_abstraction(
174  symbol_tablet &symbol_table,
175  message_handlert &message_handler,
176  goto_programt &dest);
177 
178 void string_abstraction(
179  symbol_tablet &symbol_table,
180  message_handlert &message_handler,
181  goto_functionst &dest);
182 
183 #endif // CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H
goto_programt::targett abstract_pointer_assign(goto_programt &dest, goto_programt::targett it)
The type of an expression.
Definition: type.h:20
bool build_array(const array_exprt &object, exprt &dest, bool write)
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
const std::string arg_suffix
const typet & build_abstraction_type_rec(const typet &type, const abstraction_types_mapt &known)
BigInt mp_integer
Definition: mp_arith.h:19
bool is_not_nil() const
Definition: irep.h:104
void make_type(exprt &dest, const typet &type)
exprt build_unknown(whatt what, bool write)
goto_programt::targett char_assign(goto_programt &dest, goto_programt::targett target, const exprt &new_lhs, const exprt &lhs, const exprt &rhs)
goto_programt initialization
goto_programt::targett abstract_char_assign(goto_programt &dest, goto_programt::targett it)
void declare_define_locals(goto_programt &dest)
void move_lhs_arithmetic(exprt &lhs, exprt &rhs)
Goto Programs with Functions.
std::vector< parametert > parameterst
Definition: std_types.h:829
bool build_wrap(const exprt &object, exprt &dest, bool write)
void build_new_symbol(const symbolt &symbol, const irep_idt &identifier, const typet &type)
The trinary if-then-else operator.
Definition: std_expr.h:2771
static typet build_type(whatt what)
typet & type()
Definition: expr.h:60
void add_str_arguments(const irep_idt &name, goto_functionst::goto_functiont &fct)
unsigned char_width
Definition: config.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
configt config
Definition: config.cpp:21
void add_argument(code_typet::parameterst &str_args, const symbolt &fct_symbol, const typet &type, const irep_idt &base_name, const irep_idt &identifier)
void make_decl_and_def(goto_programt &dest, goto_programt::targett ref_instr, const irep_idt &identifier, const irep_idt &source_sym)
const irep_idt & id() const
Definition: irep.h:189
::std::set< irep_idt > current_args
void replace_string_macros(exprt &expr, bool lhs, const source_locationt &)
bool build_symbol(const symbol_exprt &sym, exprt &dest)
bool build_symbol_constant(const mp_integer &zero_length, const mp_integer &buf_size, exprt &dest)
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
bool is_char_type(const typet &type) const
::std::map< typet, typet > abstraction_types_mapt
goto_programt::targett abstract_assign(goto_programt &dest, goto_programt::targett it)
API to expression classes.
exprt make_val_or_dummy_rec(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const typet &source_type)
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
symbol_tablet & symbol_table
std::unordered_map< irep_idt, irep_idt, irep_id_hash > localst
exprt build(const exprt &pointer, whatt what, bool write, const source_locationt &)
goto_function_templatet< goto_programt > goto_functiont
Symbol table.
goto_programt::targett value_assignments(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt &rhs)
goto_programt::targett value_assignments_string_struct(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt &rhs)
const typet & build_abstraction_type(const typet &type)
std::size_t get_width() const
Definition: std_types.h:1030
void abstract_function_call(goto_programt &dest, goto_programt::targett it)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void operator()(goto_programt &dest)
string_abstractiont(symbol_tablet &_symbol_table, message_handlert &_message_handler)
Base class for all expressions.
Definition: expr.h:46
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_pointer(const exprt &object, exprt &dest, bool write)
bool build_if(const if_exprt &o_if, exprt &dest, bool write)
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bool is_ptr_string_struct(const typet &type) const
goto_programt::targett value_assignments_if(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const if_exprt &rhs)
static bool has_string_macros(const exprt &expr)
exprt member(const exprt &a, whatt what)
abstraction_types_mapt abstraction_types_map
void make_typecast(const typet &_type)
Definition: expr.cpp:90
array constructor from list of elements
Definition: std_expr.h:1309
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1051