CBMC
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 <util/message.h>
18 #include <util/namespace.h>
19 
22 
24 
25 #include "loop_contract_config.h"
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_DISABLE_SIDE_EFFECT_CHECK \
37  "disable-loop-contracts-side-effect-check"
38 #define HELP_DISABLE_SIDE_EFFECT_CHECK \
39  " {y--disable-loop-contracts-side-effect-check} \t UNSOUND OPTION.\t " \
40  " disable the check of side-effect of loop contracts\n"
41 #define FLAG_LOOP_CONTRACTS_NO_UNWIND "loop-contracts-no-unwind"
42 #define HELP_LOOP_CONTRACTS_NO_UNWIND \
43  " {y--loop-contracts-no-unwind} \t do not unwind transformed loops\n"
44 
45 #define FLAG_LOOP_CONTRACTS_FILE "loop-contracts-file"
46 #define HELP_LOOP_CONTRACTS_FILE \
47  " {y--loop-contracts-file} {ufile} \t " \
48  "parse and annotate loop contracts from files\n"
49 
50 #define FLAG_REPLACE_CALL "replace-call-with-contract"
51 #define HELP_REPLACE_CALL \
52  " {y--replace-call-with-contract} {ufunction}[/{ucontract}] \t " \
53  "replace calls to {ufunction} with {ucontract}\n"
54 
55 #define FLAG_ENFORCE_CONTRACT "enforce-contract"
56 #define HELP_ENFORCE_CONTRACT \
57  " {y--enforce-contract} {ufunction}[/{ucontract}] \t " \
58  "wrap function with an assertion of contract\n"
59 
60 class local_may_aliast;
61 
63 {
64 public:
67  messaget &log,
73  log(log),
75  {
76  }
77 
79  void check_all_functions_found(const std::set<std::string> &functions) const;
80 
94  void replace_calls(const std::set<std::string> &to_replace);
95 
116  void enforce_contracts(
117  const std::set<std::string> &to_enforce,
118  const std::set<std::string> &to_exclude_from_nondet_init = {});
119 
124  const std::set<std::string> &to_exclude_from_nondet_init = {});
125 
127  const irep_idt &function_name,
128  goto_functionst::goto_functiont &goto_function,
129  const local_may_aliast &local_may_alias,
130  goto_programt::targett loop_head,
131  goto_programt::targett loop_end,
132  const loopt &loop,
133  exprt assigns_clause,
134  exprt invariant,
135  exprt decreases_clause,
136  const irep_idt &mode);
137 
138  std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
140  {
142  }
143 
144  std::unordered_set<goto_programt::const_targett, const_target_hash>
146  {
147  return loop_havoc_set;
148  }
149 
150  const namespacet ns;
151 
152 protected:
156 
158 
159  std::unordered_set<irep_idt> summarized;
160 
162  std::list<std::string> loop_names;
163 
168  std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
170 
172  std::unordered_set<goto_programt::const_targett, const_target_hash>
174 
175  // Loop contract configuration
177 
178 public:
180  void enforce_contract(const irep_idt &function);
181 
183  void check_frame_conditions_function(const irep_idt &function);
184 
187  void apply_loop_contract(
188  const irep_idt &function,
189  goto_functionst::goto_functiont &goto_function);
190 
195  const irep_idt &function,
196  const source_locationt &location,
197  goto_programt &function_body,
198  goto_programt::targett &target);
199 
202  void add_contract_check(
203  const irep_idt &wrapper_function,
204  const irep_idt &mangled_function,
205  goto_programt &dest);
206 };
207 
208 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > get_original_loop_number_map() const
Definition: contracts.h:139
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 ...
Definition: contracts.cpp:609
void enforce_contract(const irep_idt &function)
Enforce contract of a single function.
Definition: contracts.cpp:1213
goto_modelt & goto_model
Definition: contracts.h:153
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.
Definition: contracts.cpp:836
void check_all_functions_found(const std::set< std::string > &functions) const
Throws an exception if some function functions is found in the program.
Definition: contracts.cpp:1427
void check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
Definition: contracts.cpp:1122
messaget & log
Definition: contracts.h:157
void apply_loop_contracts(const std::set< std::string > &to_exclude_from_nondet_init={})
Applies loop contract transformations.
Definition: contracts.cpp:1482
std::unordered_set< goto_programt::const_targett, const_target_hash > get_loop_havoc_set() const
Definition: contracts.h:145
symbol_tablet & symbol_table
Definition: contracts.h:154
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.
Definition: contracts.cpp:1563
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.
Definition: contracts.cpp:1442
std::unordered_set< irep_idt > summarized
Definition: contracts.h:159
const namespacet ns
Definition: contracts.h:150
std::unordered_set< goto_programt::const_targett, const_target_hash > loop_havoc_set
Loop havoc instructions instrumented during applying loop contracts.
Definition: contracts.h:173
loop_contract_configt loop_contract_config
Definition: contracts.h:176
std::list< std::string > loop_names
Name of loops we are going to unwind.
Definition: contracts.h:162
goto_functionst & goto_functions
Definition: contracts.h:155
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:169
code_contractst(goto_modelt &goto_model, messaget &log, const loop_contract_configt &loop_contract_config)
Definition: contracts.h:65
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:1269
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
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.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The symbol table.
Definition: symbol_table.h:14
Goto Programs with Functions.
Symbol Table + CFG.
Config for loop contract.
Helper functions for k-induction and loop invariants.
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
Loop contract configurations.