cprover
code_contracts.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Verify and use annotated invariants and pre/post-conditions
4 
5 Author: Michael Tautschnig
6 
7 Date: February 2016
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
15 #define CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
16 
17 #include <set>
18 #include <string>
19 #include <unordered_set>
20 
23 
24 #include <util/c_types.h>
25 #include <util/message.h>
26 #include <util/namespace.h>
27 #include <util/pointer_expr.h>
28 #include <util/replace_symbol.h>
29 
30 class messaget;
31 class assigns_clauset;
32 
34 {
35 public:
37  : ns(goto_model.symbol_table),
38  symbol_table(goto_model.symbol_table),
39  goto_functions(goto_model.goto_functions),
41  log(log)
42  {
43  }
44 
58  bool replace_calls(const std::set<std::string> &);
59 
76  bool enforce_contracts(const std::set<std::string> &);
77 
80  bool enforce_contracts();
81 
85  bool replace_calls();
86 
87  const symbolt &new_tmp_symbol(
88  const typet &type,
89  const source_locationt &source_location,
90  const irep_idt &function_id,
91  const irep_idt &mode);
92 
94 
95 protected:
98 
101 
102  std::unordered_set<irep_idt> summarized;
103 
105  bool enforce_contract(const std::string &);
106 
108  void convert_to_goto(
109  const codet &code,
110  const irep_idt &mode,
111  goto_programt &program);
112 
115  bool add_pointer_checks(const std::string &);
116 
120 
126  goto_programt::instructionst::iterator &instruction_it,
127  goto_programt &program,
128  exprt &assigns,
129  std::set<irep_idt> &freely_assignable_symbols,
130  assigns_clauset &assigns_clause);
131 
137  goto_programt::instructionst::iterator &ins_it,
138  goto_programt &program,
139  exprt &assigns,
140  const irep_idt &function_id,
141  std::set<irep_idt> &freely_assignable_symbols,
142  assigns_clauset &assigns_clause);
143 
150  std::vector<exprt> operands,
151  const symbolt &function_symbol,
152  const irep_idt &function_id,
153  goto_programt &created_declarations,
154  std::vector<exprt> &created_references);
155 
160  const exprt &lhs,
161  std::vector<exprt> &aliasable_references);
162 
164 
166  bool has_contract(const irep_idt);
167 
169  const irep_idt &function_id,
170  goto_programt &goto_program,
171  goto_programt::targett target);
172 
173  void
174  add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest);
175 
181  exprt expression,
183  irep_idt mode);
184 };
185 
186 #define FLAG_REPLACE_CALL "replace-call-with-contract"
187 #define HELP_REPLACE_CALL \
188  " --replace-call-with-contract <fun>\n" \
189  " replace calls to fun with fun's contract\n"
190 
191 #define FLAG_REPLACE_ALL_CALLS "replace-all-calls-with-contracts"
192 #define HELP_REPLACE_ALL_CALLS \
193  " --replace-all-calls-with-contracts\n" \
194  " as above for all functions with a contract\n"
195 
196 #define FLAG_ENFORCE_CONTRACT "enforce-contract"
197 #define HELP_ENFORCE_CONTRACT \
198  " --enforce-contract <fun> wrap fun with an assertion of its contract\n"
199 
200 #define FLAG_ENFORCE_ALL_CONTRACTS "enforce-all-contracts"
201 #define HELP_ENFORCE_ALL_CONTRACTS \
202  " --enforce-all-contracts as above for all functions with a contract\n"
203 
206 {
207 public:
209  {
212  Array
213  };
214 
216  target_type type,
217  const exprt object_ptr,
218  const code_contractst &contract,
219  messaget &log_parameter)
220  : target_type(type),
221  pointer_object(object_ptr),
223  init_block(),
224  log(log_parameter)
225  {
226  INVARIANT(
227  pointer_object.type().id() == ID_pointer,
228  "Assigns clause targets should be stored as pointer expressions.");
229  }
230 
232  {
233  }
234 
235  virtual std::vector<symbol_exprt> temporary_declarations() const = 0;
236  virtual exprt alias_expression(const exprt &lhs) = 0;
237  virtual exprt
239  virtual goto_programt havoc_code(source_locationt location) const = 0;
240 
241  const exprt &get_direct_pointer() const
242  {
243  return pointer_object;
244  }
245 
247  {
248  return init_block;
249  }
250 
251  static exprt pointer_for(const exprt &exp)
252  {
253  return address_of_exprt(exp);
254  }
255 
257 
258 protected:
263 };
264 
266 {
267 public:
269  const exprt &object_ptr,
271  messaget &log_parameter,
272  const irep_idt &function_id);
273 
274  std::vector<symbol_exprt> temporary_declarations() const;
275  exprt alias_expression(const exprt &lhs);
276  exprt compatible_expression(const assigns_clause_targett &called_target);
277  goto_programt havoc_code(source_locationt location) const;
278 
279 protected:
281 };
282 
284 {
285 public:
287  const exprt &object_ptr,
289  messaget &log_parameter,
290  const irep_idt &function_id);
291 
292  std::vector<symbol_exprt> temporary_declarations() const;
293  exprt alias_expression(const exprt &lhs);
294  exprt compatible_expression(const assigns_clause_targett &called_target);
295  goto_programt havoc_code(source_locationt location) const;
296 
297 protected:
299  std::vector<symbol_exprt> local_standin_variables;
300 };
301 
303 {
304 public:
306  const exprt &object_ptr,
308  messaget &log_parameter,
309  const irep_idt &function_id);
310 
311  std::vector<symbol_exprt> temporary_declarations() const;
312  exprt alias_expression(const exprt &lhs);
313  exprt compatible_expression(const assigns_clause_targett &called_target);
314  goto_programt havoc_code(source_locationt location) const;
315 
316 protected:
319 
322 
326 };
327 
329 {
330 public:
332  const exprt &assigns,
333  code_contractst &contract,
334  const irep_idt function_id,
335  messaget log_parameter);
337 
338  assigns_clause_targett *add_target(exprt current_operation);
339  assigns_clause_targett *add_pointer_target(exprt current_operation);
342  source_locationt location,
343  irep_idt function_name,
344  irep_idt language_mode);
346  source_locationt location,
347  irep_idt function_name,
348  irep_idt language_mode);
350  source_locationt location,
351  irep_idt function_name,
352  irep_idt language_mode);
353  exprt alias_expression(const exprt &lhs);
354 
355  exprt compatible_expression(const assigns_clauset &called_assigns);
356 
357 protected:
359 
360  std::vector<assigns_clause_targett *> targets;
362 
366 };
367 
368 #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
assigns_clause_targett::alias_expression
virtual exprt alias_expression(const exprt &lhs)=0
assigns_clause_array_targett::temporary_declarations
std::vector< symbol_exprt > temporary_declarations() const
Definition: code_contracts.cpp:1342
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
assigns_clause_targett::temporary_declarations
virtual std::vector< symbol_exprt > temporary_declarations() const =0
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
assigns_clause_array_targett::compatible_expression
exprt compatible_expression(const assigns_clause_targett &called_target)
Definition: code_contracts.cpp:1404
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
assigns_clauset::function_id
const irep_idt function_id
Definition: code_contracts.h:364
assigns_clause_scalar_targett::havoc_code
goto_programt havoc_code(source_locationt location) const
Definition: code_contracts.cpp:1078
assigns_clause_struct_targett::compatible_expression
exprt compatible_expression(const assigns_clause_targett &called_target)
Definition: code_contracts.cpp:1206
assigns_clause_targett::target_type
target_type
Definition: code_contracts.h:209
code_contractst::populate_assigns_reference
void populate_assigns_reference(std::vector< exprt > operands, const symbolt &function_symbol, const irep_idt &function_id, goto_programt &created_declarations, std::vector< exprt > &created_references)
Creates a local variable declaration for each expression in operands, and stores them in created_decl...
code_contractst::add_contract_check
void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest)
Definition: code_contracts.cpp:783
assigns_clause_array_targett::upper_offset_object
exprt upper_offset_object
Definition: code_contracts.h:321
assigns_clauset::dead_stmts
goto_programt dead_stmts(source_locationt location, irep_idt function_name, irep_idt language_mode)
Definition: code_contracts.cpp:1520
typet
The type of an expression, extends irept.
Definition: type.h:28
assigns_clauset::targets
std::vector< assigns_clause_targett * > targets
Definition: code_contracts.h:360
assigns_clause_targett::log
messaget & log
Definition: code_contracts.h:262
assigns_clauset::assigns_expr
const exprt & assigns_expr
Definition: code_contracts.h:358
code_contractst::add_quantified_variable
void add_quantified_variable(exprt expression, replace_symbolt &replace, irep_idt mode)
This function recursively searches the expression to find nested or non-nested quantified expressions...
Definition: code_contracts.cpp:177
assigns_clause_struct_targett::temporary_declarations
std::vector< symbol_exprt > temporary_declarations() const
Definition: code_contracts.cpp:1174
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
assigns_clause_targett::pointer_for
static exprt pointer_for(const exprt &exp)
Definition: code_contracts.h:251
replace_symbol.h
assigns_clause_array_targett::assigns_clause_array_targett
assigns_clause_array_targett(const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
Definition: code_contracts.cpp:1263
assigns_clause_array_targett::lower_offset_variable
symbol_exprt lower_offset_variable
Definition: code_contracts.h:324
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
assigns_clause_scalar_targett::compatible_expression
exprt compatible_expression(const assigns_clause_targett &called_target)
Definition: code_contracts.cpp:1064
code_contractst::apply_function_contract
bool apply_function_contract(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target)
Definition: code_contracts.cpp:247
assigns_clause_targett::assigns_clause_targett
assigns_clause_targett(target_type type, const exprt object_ptr, const code_contractst &contract, messaget &log_parameter)
Definition: code_contracts.h:215
assigns_clause_array_targett::upper_bound
mp_integer upper_bound
Definition: code_contracts.h:318
goto_model.h
Symbol Table + CFG.
assigns_clauset::alias_expression
exprt alias_expression(const exprt &lhs)
Definition: code_contracts.cpp:1554
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
code_contractst::log
messaget & log
Definition: code_contracts.h:100
assigns_clause_targett::contract
const code_contractst & contract
Definition: code_contracts.h:260
assigns_clauset::add_pointer_target
assigns_clause_targett * add_pointer_target(exprt current_operation)
Definition: code_contracts.cpp:1482
assigns_clauset::add_target
assigns_clause_targett * add_target(exprt current_operation)
Definition: code_contracts.cpp:1453
assigns_clauset::assigns_clauset
assigns_clauset(const exprt &assigns, code_contractst &contract, const irep_idt function_id, messaget log_parameter)
Definition: code_contracts.cpp:1430
assigns_clause_targett::pointer_object
const exprt pointer_object
Definition: code_contracts.h:259
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
assigns_clauset::log
messaget log
Definition: code_contracts.h:365
namespace.h
assigns_clause_targett::havoc_code
virtual goto_programt havoc_code(source_locationt location) const =0
assigns_clause_targett::Array
@ Array
Definition: code_contracts.h:212
code_contractst::instrument_call_statement
void instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, const irep_idt &function_id, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)
Inserts an assertion statement into program before the function call at ins_it, to ensure that any me...
Definition: code_contracts.cpp:449
code_contractst::instrument_assign_statement
void instrument_assign_statement(goto_programt::instructionst::iterator &instruction_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)
Inserts an assertion statement into program before the assignment instruction_it, to ensure that the ...
Definition: code_contracts.cpp:425
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
assigns_clause_targett::target_type
const target_type target_type
Definition: code_contracts.h:256
assigns_clause_struct_targett::local_standin_variables
std::vector< symbol_exprt > local_standin_variables
Definition: code_contracts.h:299
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
assigns_clause_scalar_targett::temporary_declarations
std::vector< symbol_exprt > temporary_declarations() const
Definition: code_contracts.cpp:1052
assigns_clauset::parent
code_contractst & parent
Definition: code_contracts.h:363
code_contractst::code_contractst
code_contractst(goto_modelt &goto_model, messaget &log)
Definition: code_contracts.h:36
assigns_clause_array_targett::lower_bound
mp_integer lower_bound
Definition: code_contracts.h:317
assigns_clauset::init_block
goto_programt init_block(source_locationt location)
Definition: code_contracts.cpp:1487
assigns_clause_targett::get_init_block
goto_programt & get_init_block()
Definition: code_contracts.h:246
assigns_clause_targett::Scalar
@ Scalar
Definition: code_contracts.h:210
code_contractst::temporary_counter
unsigned temporary_counter
Definition: code_contracts.h:99
code_contractst::has_contract
bool has_contract(const irep_idt)
Does the named function have a contract?
Definition: code_contracts.cpp:170
assigns_clause_scalar_targett::alias_expression
exprt alias_expression(const exprt &lhs)
Definition: code_contracts.cpp:1059
pointer_expr.h
API to expression classes for Pointers.
code_contractst::create_alias_expression
exprt create_alias_expression(const exprt &lhs, std::vector< exprt > &aliasable_references)
Creates a boolean expression which is true when there exists an expression in aliasable_references wi...
Definition: code_contracts.cpp:412
assigns_clause_struct_targett::main_struct_standin
symbol_exprt main_struct_standin
Definition: code_contracts.h:298
code_contractst::check_for_looped_mallocs
bool check_for_looped_mallocs(const goto_programt &)
Check if there are any malloc statements which may be repeated because of a goto statement that jumps...
Definition: code_contracts.cpp:562
code_contractst::add_pointer_checks
bool add_pointer_checks(const std::string &)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
Definition: code_contracts.cpp:615
code_contractst
Definition: code_contracts.h:34
assigns_clause_array_targett::alias_expression
exprt alias_expression(const exprt &lhs)
Definition: code_contracts.cpp:1386
assigns_clauset
Definition: code_contracts.h:329
assigns_clauset::temporary_declarations
goto_programt & temporary_declarations(source_locationt location, irep_idt function_name, irep_idt language_mode)
Definition: code_contracts.cpp:1501
assigns_clause_scalar_targett
Definition: code_contracts.h:266
irept::id
const irep_idt & id() const
Definition: irep.h:407
assigns_clauset::compatible_expression
exprt compatible_expression(const assigns_clauset &called_assigns)
Definition: code_contracts.cpp:1580
code_contractst::ns
namespacet ns
Definition: code_contracts.h:93
code_contractst::convert_to_goto
void convert_to_goto(const codet &code, const irep_idt &mode, goto_programt &program)
Create goto instructions based on code and add them to program.
Definition: code_contracts.cpp:161
assigns_clause_array_targett::array_standin_variable
symbol_exprt array_standin_variable
Definition: code_contracts.h:323
assigns_clause_struct_targett::alias_expression
exprt alias_expression(const exprt &lhs)
Definition: code_contracts.cpp:1179
code_contractst::apply_loop_contract
void apply_loop_contract(goto_functionst::goto_functiont &goto_function)
Definition: code_contracts.cpp:385
assigns_clauset::havoc_code
goto_programt havoc_code(source_locationt location, irep_idt function_name, irep_idt language_mode)
Definition: code_contracts.cpp:1537
source_locationt
Definition: source_location.h:20
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
code_contractst::new_tmp_symbol
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)
Definition: code_contracts.cpp:397
assigns_clause_targett::Struct
@ Struct
Definition: code_contracts.h:211
assigns_clause_array_targett::havoc_code
goto_programt havoc_code(source_locationt location) const
Definition: code_contracts.cpp:1353
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
assigns_clause_scalar_targett::local_standin_variable
symbol_exprt local_standin_variable
Definition: code_contracts.h:280
assigns_clause_struct_targett
Definition: code_contracts.h:284
code_contractst::enforce_contracts
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
Definition: code_contracts.cpp:976
assigns_clause_array_targett::upper_offset_variable
symbol_exprt upper_offset_variable
Definition: code_contracts.h:325
code_contractst::goto_functions
goto_functionst & goto_functions
Definition: code_contracts.h:97
symbolt
Symbol table entry.
Definition: symbol.h:28
assigns_clause_array_targett
Definition: code_contracts.h:303
assigns_clause_array_targett::lower_offset_object
exprt lower_offset_object
Definition: code_contracts.h:320
assigns_clause_struct_targett::havoc_code
goto_programt havoc_code(source_locationt location) const
Definition: code_contracts.cpp:1248
goto_functions.h
Goto Programs with Functions.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
code_contractst::replace_calls
bool replace_calls()
Call replace_calls() on all calls to any function that has a contract.
Definition: code_contracts.cpp:965
code_contractst::summarized
std::unordered_set< irep_idt > summarized
Definition: code_contracts.h:102
assigns_clauset::standin_declarations
goto_programt standin_declarations
Definition: code_contracts.h:361
code_contractst::enforce_contract
bool enforce_contract(const std::string &)
Enforce contract of a single function.
Definition: code_contracts.cpp:721
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
message.h
assigns_clause_targett::compatible_expression
virtual exprt compatible_expression(const assigns_clause_targett &called_target)=0
assigns_clause_scalar_targett::assigns_clause_scalar_targett
assigns_clause_scalar_targett(const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
Definition: code_contracts.cpp:1020
assigns_clause_targett::init_block
goto_programt init_block
Definition: code_contracts.h:261
assigns_clauset::~assigns_clauset
~assigns_clauset()
Definition: code_contracts.cpp:1445
assigns_clause_targett
A base class for assigns clause targets.
Definition: code_contracts.h:206
assigns_clause_targett::get_direct_pointer
const exprt & get_direct_pointer() const
Definition: code_contracts.h:241
c_types.h
assigns_clause_struct_targett::assigns_clause_struct_targett
assigns_clause_struct_targett(const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
Definition: code_contracts.cpp:1093
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563
code_contractst::symbol_table
symbol_tablet & symbol_table
Definition: code_contracts.h:96
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
assigns_clause_targett::~assigns_clause_targett
virtual ~assigns_clause_targett()
Definition: code_contracts.h:231