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
18
19#include <util/message.h>
20#include <util/namespace.h>
21
24
26
27#include <map>
28#include <set>
29#include <string>
30#include <unordered_set>
31
32#define FLAG_LOOP_CONTRACTS "apply-loop-contracts"
33#define HELP_LOOP_CONTRACTS \
34 " {y--apply-loop-contracts} \t check and use loop contracts when provided\n"
35
36#define FLAG_LOOP_CONTRACTS_NO_UNWIND "loop-contracts-no-unwind"
37#define HELP_LOOP_CONTRACTS_NO_UNWIND \
38 " {y--loop-contracts-no-unwind} \t do not unwind transformed loops\n"
39
40#define FLAG_LOOP_CONTRACTS_FILE "loop-contracts-file"
41#define HELP_LOOP_CONTRACTS_FILE \
42 " {y--loop-contracts-file} {ufile} \t " \
43 "parse and annotate loop contracts from files\n"
44
45#define FLAG_REPLACE_CALL "replace-call-with-contract"
46#define HELP_REPLACE_CALL \
47 " {y--replace-call-with-contract} {ufunction}[/{ucontract}] \t " \
48 "replace calls to {ufunction} with {ucontract}\n"
49
50#define FLAG_ENFORCE_CONTRACT "enforce-contract"
51#define HELP_ENFORCE_CONTRACT \
52 " {y--enforce-contract} {ufunction}[/{ucontract}] \t " \
53 "wrap function with an assertion of contract\n"
54
56
58{
59public:
69
71 void check_all_functions_found(const std::set<std::string> &functions) const;
72
86 void replace_calls(const std::set<std::string> &to_replace);
87
109 const std::set<std::string> &to_enforce,
110 const std::set<std::string> &to_exclude_from_nondet_init = {});
111
116 const std::set<std::string> &to_exclude_from_nondet_init = {});
117
119 const irep_idt &function_name,
120 goto_functionst::goto_functiont &goto_function,
121 const local_may_aliast &local_may_alias,
124 const loopt &loop,
126 exprt invariant,
128 const irep_idt &mode);
129
130 std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
135
136 std::unordered_set<goto_programt::const_targett, const_target_hash>
138 {
139 return loop_havoc_set;
140 }
141
143
144 // Unwind transformed loops after applying loop contracts or not.
146
147protected:
151
154
155 std::unordered_set<irep_idt> summarized;
156
158 std::list<std::string> loop_names;
159
164 std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
166
168 std::unordered_set<goto_programt::const_targett, const_target_hash>
170
171public:
173 void enforce_contract(const irep_idt &function);
174
176 void check_frame_conditions_function(const irep_idt &function);
177
181 const irep_idt &function,
182 goto_functionst::goto_functiont &goto_function);
183
188 const irep_idt &function,
189 const source_locationt &location,
191 goto_programt::targett &target);
192
198 goto_programt &dest);
199};
200
201#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
namespacet ns
Definition contracts.h:142
void 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 enforce_contract(const irep_idt &function)
Enforce contract of a single function.
goto_modelt & goto_model
Definition contracts.h:148
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, goto_programt::targett loop_end, const loopt &loop, exprt assigns_clause, exprt invariant, exprt decreases_clause, const irep_idt &mode)
Definition contracts.cpp:49
void apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function)
Apply loop contracts, whenever available, to all loops in function.
void check_all_functions_found(const std::set< std::string > &functions) const
Throws an exception if some function functions is found in the program.
void check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
messaget & log
Definition contracts.h:152
void apply_loop_contracts(const std::set< std::string > &to_exclude_from_nondet_init={})
Applies loop contract transformations.
symbol_tablet & symbol_table
Definition contracts.h:149
void enforce_contracts(const std::set< std::string > &to_enforce, const std::set< std::string > &to_exclude_from_nondet_init={})
Turn requires & ensures into assumptions and assertions for each of the named functions.
void replace_calls(const std::set< std::string > &to_replace)
Replace all calls to each function in the to_replace set with that function's contract.
std::unordered_set< irep_idt > summarized
Definition contracts.h:155
code_contractst(goto_modelt &goto_model, messaget &log)
Definition contracts.h:60
goto_convertt converter
Definition contracts.h:153
std::unordered_set< goto_programt::const_targett, const_target_hash > loop_havoc_set
Loop havoc instructions instrumented during applying loop contracts.
Definition contracts.h:169
std::list< std::string > loop_names
Name of loops we are going to unwind.
Definition contracts.h:158
goto_functionst & goto_functions
Definition contracts.h:150
std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > get_original_loop_number_map() const
Definition contracts.h:131
std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > original_loop_number_map
Store the map from instrumented instructions for loop contracts to their original loop numbers.
Definition contracts.h:165
std::unordered_set< goto_programt::const_targett, const_target_hash > get_loop_havoc_set() const
Definition contracts.h:137
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...
bool unwind_transformed_loops
Definition contracts.h:145
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
A collection of goto functions.
::goto_functiont goto_functiont
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
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
The symbol table.
Program Transformation.
Goto Programs with Functions.
Symbol Table + CFG.
Helper functions for k-induction and loop invariants.