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 
27 
28 #include <langapi/language_util.h>
29 
30 #include <util/message.h>
31 #include <util/namespace.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_REPLACE_ALL_CALLS "replace-all-calls-with-contracts"
45 #define HELP_REPLACE_ALL_CALLS \
46  " --replace-all-calls-with-contracts\n" \
47  " as above for all functions with a contract\n"
48 
49 #define FLAG_ENFORCE_CONTRACT "enforce-contract"
50 #define HELP_ENFORCE_CONTRACT \
51  " --enforce-contract <fun> wrap fun with an assertion of its contract\n"
52 
53 #define FLAG_ENFORCE_ALL_CONTRACTS "enforce-all-contracts"
54 #define HELP_ENFORCE_ALL_CONTRACTS \
55  " --enforce-all-contracts as above for all functions with a contract\n"
56 
57 class assigns_clauset;
58 class local_may_aliast;
59 class replace_symbolt;
60 
62 {
63 public:
65  : ns(goto_model.symbol_table),
66  symbol_table(goto_model.symbol_table),
67  goto_functions(goto_model.goto_functions),
68  log(log),
69  converter(symbol_table, log.get_message_handler())
70 
71  {
72  }
73 
87  bool replace_calls(const std::set<std::string> &functions);
88 
105  bool enforce_contracts(const std::set<std::string> &functions);
106 
109  bool enforce_contracts();
110 
114  bool replace_calls();
115 
116  void apply_loop_contracts();
117 
118  const symbolt &new_tmp_symbol(
119  const typet &type,
120  const source_locationt &source_location,
121  const irep_idt &mode);
122 
124  goto_functionst::goto_functiont &goto_function,
125  const local_may_aliast &local_may_alias,
126  goto_programt::targett loop_head,
127  const loopt &loop,
128  const irep_idt &mode);
129 
130  // for "helper" classes to update symbol table.
133 
135 
136 protected:
139 
142 
143  std::unordered_set<irep_idt> summarized;
144 
146  bool enforce_contract(const irep_idt &function);
147 
149  bool check_frame_conditions_function(const irep_idt &function);
150 
153  void check_frame_conditions(goto_programt &program, const symbolt &target);
154 
157  bool check_for_looped_mallocs(const goto_programt &program);
158 
164  goto_programt::instructionst::iterator &instruction_it,
165  goto_programt &program,
166  exprt &assigns,
167  std::set<irep_idt> &freely_assignable_symbols,
168  assigns_clauset &assigns_clause);
169 
175  goto_programt::instructionst::iterator &ins_it,
176  goto_programt &program,
177  exprt &assigns,
178  std::set<irep_idt> &freely_assignable_symbols,
179  assigns_clauset &assigns_clause);
180 
185  const exprt &lhs,
186  std::vector<exprt> &aliasable_references);
187 
190  void apply_loop_contract(
191  const irep_idt &function,
192  goto_functionst::goto_functiont &goto_function);
193 
195  bool has_contract(const irep_idt);
196 
201  goto_programt &goto_program,
202  goto_programt::targett target);
203 
206  void add_contract_check(
207  const irep_idt &wrapper_function,
208  const irep_idt &mangled_function,
209  goto_programt &dest);
210 
216  const exprt &expression,
218  const irep_idt &mode);
219 
223  exprt &expr,
224  std::map<exprt, exprt> &parameter2history,
225  source_locationt location,
226  const irep_idt &mode,
227  goto_programt &history,
228  const irep_idt &id);
229 
233  std::pair<goto_programt, goto_programt> create_ensures_instruction(
234  codet &expression,
235  source_locationt location,
236  const irep_idt &mode);
237 };
238 
239 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
namespacet ns
Definition: contracts.h:134
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
Definition: contracts.cpp:1261
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:453
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:395
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &mode)
Definition: contracts.cpp:645
void instrument_call_statement(goto_programt::instructionst::iterator &ins_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 function call at ins_it, to ensure that any me...
Definition: contracts.cpp:711
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:625
messaget & log
Definition: contracts.h:140
goto_functionst & get_goto_functions()
Definition: contracts.cpp:664
void check_frame_conditions(goto_programt &program, const symbolt &target)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
Definition: contracts.cpp:914
void apply_loop_contracts()
Definition: contracts.cpp:1244
symbol_tablet & symbol_table
Definition: contracts.h:137
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: contracts.cpp:669
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:327
void check_apply_loop_contracts(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:95
bool check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
Definition: contracts.cpp:886
bool apply_function_contract(goto_programt &goto_program, goto_programt::targett target)
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for ...
Definition: contracts.cpp:475
bool replace_calls()
Call replace_calls() on all calls to any function that has a contract.
Definition: contracts.cpp:1250
bool enforce_contract(const irep_idt &function)
Enforce contract of a single function.
Definition: contracts.cpp:984
std::unordered_set< irep_idt > summarized
Definition: contracts.h:143
bool has_contract(const irep_idt)
Does the named function have a contract?
Definition: contracts.cpp:320
code_contractst(goto_modelt &goto_model, messaget &log)
Definition: contracts.h:64
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:823
goto_convertt converter
Definition: contracts.h:141
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: contracts.cpp:682
goto_functionst & goto_functions
Definition: contracts.h:138
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:1047
symbol_tablet & get_symbol_table()
Definition: contracts.cpp:659
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
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:71
instructionst::iterator targett
Definition: goto_program.h:646
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
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:28
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
API to expression classes for Pointers.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)