cprover
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_CONTRACTS_CONTRACTS_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
16 
17 #include <map>
18 #include <set>
19 #include <string>
20 #include <unordered_set>
21 
23 
28 
29 #include <util/message.h>
30 #include <util/namespace.h>
31 #include <util/optional.h>
32 #include <util/pointer_expr.h>
33 
34 #define FLAG_LOOP_CONTRACTS "apply-loop-contracts"
35 #define HELP_LOOP_CONTRACTS \
36  " --apply-loop-contracts\n" \
37  " check and use loop contracts when provided\n"
38 
39 #define FLAG_REPLACE_CALL "replace-call-with-contract"
40 #define HELP_REPLACE_CALL \
41  " --replace-call-with-contract <fun>\n" \
42  " replace calls to fun with fun's contract\n"
43 
44 #define FLAG_ENFORCE_CONTRACT "enforce-contract"
45 #define HELP_ENFORCE_CONTRACT \
46  " --enforce-contract <fun> wrap fun with an assertion of its contract\n"
47 
48 class local_may_aliast;
49 class replace_symbolt;
51 class cfg_infot;
52 
54 {
55 public:
57  : ns(goto_model.symbol_table),
58  symbol_table(goto_model.symbol_table),
59  goto_functions(goto_model.goto_functions),
60  log(log),
61  converter(symbol_table, log.get_message_handler())
62  {
63  }
64 
78  bool replace_calls(const std::set<std::string> &);
79 
96  bool enforce_contracts(const std::set<std::string> &functions);
97 
98  void apply_loop_contracts();
99 
101  const irep_idt &function_name,
102  goto_functionst::goto_functiont &goto_function,
103  const local_may_aliast &local_may_alias,
104  goto_programt::targett loop_head,
105  const loopt &loop,
106  const irep_idt &mode);
107 
108  // for "helper" classes to update symbol table.
111 
113 
115  enum class skipt
116  {
117  DontSkip,
118  Skip
119  };
120 
121 protected:
124 
127 
128  std::unordered_set<irep_idt> summarized;
129 
131  bool enforce_contract(const irep_idt &function);
132 
134  bool check_frame_conditions_function(const irep_idt &function);
135 
151  const irep_idt &function,
152  goto_programt &body,
153  goto_programt::targett instruction_it,
154  const goto_programt::targett &instruction_end,
155  instrument_spec_assignst &instrument_spec_assigns,
156  skipt skip_parameter_assigns,
157  optionalt<cfg_infot> &cfg_info_opt);
158 
161  bool check_for_looped_mallocs(const goto_programt &program);
162 
167  goto_programt::targett &instruction_it,
168  goto_programt &program,
169  instrument_spec_assignst &instrument_spec_assigns,
170  optionalt<cfg_infot> &cfg_info_opt);
171 
174  // callee are "included" in the (conditional address ranges in the) write set.
176  goto_programt::targett &instruction_it,
177  const irep_idt &function,
178  goto_programt &body,
179  instrument_spec_assignst &instrument_spec_assigns,
180  optionalt<cfg_infot> &cfg_info_opt);
181 
184  void apply_loop_contract(
185  const irep_idt &function,
186  goto_functionst::goto_functiont &goto_function);
187 
192  const irep_idt &function,
193  const source_locationt &location,
194  goto_programt &function_body,
195  goto_programt::targett &target);
196 
199  void add_contract_check(
200  const irep_idt &wrapper_function,
201  const irep_idt &mangled_function,
202  goto_programt &dest);
203 
209  const exprt &expression,
211  const irep_idt &mode);
212 
216  exprt &expr,
217  std::map<exprt, exprt> &parameter2history,
218  source_locationt location,
219  const irep_idt &mode,
220  goto_programt &history,
221  const irep_idt &id);
222 
226  std::pair<goto_programt, goto_programt> create_ensures_instruction(
227  codet &expression,
228  source_locationt location,
229  const irep_idt &mode);
230 };
231 
232 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
Stores information about a goto function computed from its CFG, together with a target iterator into ...
Definition: utils.h:190
namespacet ns
Definition: contracts.h:112
std::pair< goto_programt, goto_programt > create_ensures_instruction(codet &expression, source_locationt location, const irep_idt &mode)
This function creates and returns an instruction that corresponds to the ensures clause.
Definition: contracts.cpp:639
void replace_history_parameter(exprt &expr, std::map< exprt, exprt > &parameter2history, source_locationt location, const irep_idt &mode, goto_programt &history, const irep_idt &id)
This function recursively identifies the "old" expressions within expr and replaces them with corresp...
Definition: contracts.cpp:565
bool replace_calls(const std::set< std::string > &)
Replace all calls to each function in the list with that function's contract.
Definition: contracts.cpp:1567
bool apply_function_contract(const irep_idt &function, const source_locationt &location, goto_programt &function_body, goto_programt::targett &target)
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for ...
Definition: contracts.cpp:661
void apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function)
Apply loop contracts, whenever available, to all loops in function.
Definition: contracts.cpp:870
messaget & log
Definition: contracts.h:125
goto_functionst & get_goto_functions()
Definition: contracts.cpp:958
void apply_loop_contracts()
Definition: contracts.cpp:1610
symbol_tablet & symbol_table
Definition: contracts.h:122
void instrument_call_statement(goto_programt::targett &instruction_it, const irep_idt &function, goto_programt &body, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
Inserts an assertion into program immediately before the function call at instruction_it,...
Definition: contracts.cpp:977
void add_quantified_variable(const exprt &expression, replace_symbolt &replace, const irep_idt &mode)
This function recursively searches the expression to find nested or non-nested quantified expressions...
Definition: contracts.cpp:499
bool check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
Definition: contracts.cpp:1088
bool enforce_contract(const irep_idt &function)
Enforce contract of a single function.
Definition: contracts.cpp:1351
std::unordered_set< irep_idt > summarized
Definition: contracts.h:128
void check_frame_conditions(const irep_idt &function, goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, instrument_spec_assignst &instrument_spec_assigns, skipt skip_parameter_assigns, optionalt< cfg_infot > &cfg_info_opt)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
Definition: contracts.cpp:1253
code_contractst(goto_modelt &goto_model, messaget &log)
Definition: contracts.h:56
bool check_for_looped_mallocs(const goto_programt &program)
Check if there are any malloc statements which may be repeated because of a goto statement that jumps...
Definition: contracts.cpp:1025
goto_convertt converter
Definition: contracts.h:126
void instrument_assign_statement(goto_programt::targett &instruction_it, goto_programt &program, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
Inserts an assertion into program immediately before the assignment instruction_it,...
Definition: contracts.cpp:963
void check_apply_loop_contracts(const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, const loopt &loop, const irep_idt &mode)
Definition: contracts.cpp:138
goto_functionst & goto_functions
Definition: contracts.h:123
skipt
Tells wether to skip or not skip an action.
Definition: contracts.h:116
bool enforce_contracts(const std::set< std::string > &functions)
Turn requires & ensures into assumptions and assertions for each of the named functions.
Definition: contracts.cpp:1616
void add_contract_check(const irep_idt &wrapper_function, const irep_idt &mangled_function, goto_programt &dest)
Instruments wrapper_function adding assumptions based on requires clauses and assertions based on ens...
Definition: contracts.cpp:1414
symbol_tablet & get_symbol_table()
Definition: contracts.cpp:953
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
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
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:73
instructionst::iterator targett
Definition: goto_program.h:592
A class that generates instrumentation for assigns clause checking.
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Replace expression or type symbols by an expression or type, respectively.
The symbol table.
Definition: symbol_table.h:14
Program Transformation.
Goto Programs with Functions.
Symbol Table + CFG.
Helper functions for k-induction and loop invariants.
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)