cprover
Loading...
Searching...
No Matches
contracts.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Verify and use annotated invariants and pre/post-conditions
4
5Author: Michael Tautschnig
6
7Date: 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
49class replace_symbolt;
51class cfg_infot;
52
54{
55public:
57 : ns(goto_model.symbol_table),
58 symbol_table(goto_model.symbol_table),
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
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
121protected:
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
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
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.
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...
bool replace_calls(const std::set< std::string > &)
Replace all calls to each function in the list with that function's contract.
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 ...
void apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function)
Apply loop contracts, whenever available, to all loops in function.
messaget & log
Definition contracts.h:125
goto_functionst & get_goto_functions()
void apply_loop_contracts()
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,...
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...
bool check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
bool enforce_contract(const irep_idt &function)
Enforce contract of a single function.
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...
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...
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,...
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)
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.
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...
symbol_tablet & get_symbol_table()
Data structure for representing an arbitrary statement in a program.
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.
instructionst::iterator targett
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.
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)