cprover
Loading...
Searching...
No Matches
dfcc.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for function contracts
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7\*******************************************************************/
8
10
13
28
29#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_H
30#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_H
31
33#include <util/irep.h>
34#include <util/message.h>
35
38#include "dfcc_instrument.h"
39#include "dfcc_library.h"
42#include "dfcc_spec_functions.h"
43#include "dfcc_swap_and_wrap.h"
44
45#include <map>
46#include <set>
47
48class goto_modelt;
49class messaget;
51class symbolt;
53class optionst;
54
55#define FLAG_DFCC "dfcc"
56#define OPT_DFCC "(" FLAG_DFCC "):"
57
58#define HELP_DFCC \
59 " {y--dfcc} {uharness} \t " \
60 "activate dynamic frame condition checking for contracts using the given " \
61 "harness as entry point\n"
62
63#define FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec"
64#define OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):"
65#define HELP_ENFORCE_CONTRACT_REC \
66 " {y--enforce-contract-rec} {ufunction}[{y/}{ucontract}] \t " \
67 "wrap {ufunction} with an assertion of the contract and assume recursive " \
68 "calls to " \
69 "{ufunction} satisfy the contract\n"
70
74{
75public:
77 std::string reason,
78 std::string correct_format = "");
79
80 std::string what() const override;
81
82 std::string correct_format;
83};
84
105void dfcc(
106 const optionst &options,
107 goto_modelt &goto_model,
108 const irep_idt &harness_id,
109 const optionalt<irep_idt> &to_check,
110 const bool allow_recursive_calls,
111 const std::set<irep_idt> &to_replace,
112 const bool apply_loop_contracts,
113 const bool unwind_transformed_loops,
114 const std::set<std::string> &to_exclude_from_nondet_static,
115 message_handlert &message_handler);
116
138void dfcc(
139 const optionst &options,
140 goto_modelt &goto_model,
141 const irep_idt &harness_id,
142 const optionalt<std::pair<irep_idt, irep_idt>> &to_check,
143 const bool allow_recursive_calls,
144 const std::map<irep_idt, irep_idt> &to_replace,
145 const bool apply_loop_contracts,
146 const bool unwind_transformed_loops,
147 const std::set<std::string> &to_exclude_from_nondet_static,
148 message_handlert &message_handler);
149
152class dfcct
153{
154public:
166 dfcct(
167 const optionst &options,
169 const irep_idt &harness_id,
170 const optionalt<std::pair<irep_idt, irep_idt>> &to_check,
171 const bool allow_recursive_calls,
172 const std::map<irep_idt, irep_idt> &to_replace,
175 const std::set<std::string> &to_exclude_from_nondet_static);
176
202
203protected:
209 const std::map<irep_idt, irep_idt> &to_replace;
211 const std::set<std::string> &to_exclude_from_nondet_static;
214
215 // Singletons that hold the global state of the program transformation
216 // (caches etc.)
225
229
230 // partition the set of functions of the goto_model
231 std::set<irep_idt> pure_contract_symbols;
232 std::set<irep_idt> other_symbols;
233 std::set<irep_idt> function_pointer_contracts;
234
250
254 std::set<irep_idt> &pure_contract_symbols,
255 std::set<irep_idt> &other_symbols);
256
264
310 void reinitialize_model();
311};
312
313#endif
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition c_expr.h:232
Base class for exceptions thrown in the cprover project.
Definition c_errors.h:64
std::string reason
The reason this exception was generated.
Definition c_errors.h:83
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
A contract is represented by a function declaration or definition with contract clauses attached to i...
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
Class interface to library types and functions defined in cprover_contracts.c.
This class rewrites GOTO functions that use the built-ins:
Entry point into the contracts transformation.
Definition dfcc.h:153
goto_modelt & goto_model
Definition dfcc.h:205
std::set< irep_idt > function_pointer_contracts
Definition dfcc.h:233
const optionst & options
Definition dfcc.h:204
std::set< irep_idt > pure_contract_symbols
Definition dfcc.h:231
dfcc_spec_functionst spec_functions
Definition dfcc.h:219
void instrument_harness_function()
Definition dfcc.cpp:335
void instrument_other_functions()
Definition dfcc.cpp:476
void reinitialize_model()
Re-initialise the GOTO model.
Definition dfcc.cpp:551
const std::set< std::string > & to_exclude_from_nondet_static
Definition dfcc.h:211
void link_model_and_load_dfcc_library()
Definition dfcc.cpp:313
dfcc_swap_and_wrapt swap_and_wrap
Definition dfcc.h:224
dfcc_lift_memory_predicatest memory_predicates
Definition dfcc.h:222
dfcct(const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const optionalt< std::pair< irep_idt, irep_idt > > &to_check, const bool allow_recursive_calls, const std::map< irep_idt, irep_idt > &to_replace, const dfcc_loop_contract_modet loop_contract_mode, message_handlert &message_handler, const std::set< std::string > &to_exclude_from_nondet_static)
Class constructor.
Definition dfcc.cpp:171
void wrap_checked_function()
Definition dfcc.cpp:360
void lift_memory_predicates()
Definition dfcc.cpp:348
messaget log
Definition dfcc.h:213
const dfcc_loop_contract_modet loop_contract_mode
Definition dfcc.h:210
const optionalt< std::pair< irep_idt, irep_idt > > & to_check
Definition dfcc.h:207
void check_transform_goto_model_preconditions()
Checks preconditions on arguments of transform_goto_model.
Definition dfcc.cpp:222
std::size_t max_assigns_clause_size
Tracks the maximum number of targets in any assigns clause handled in the transformation (used to spe...
Definition dfcc.h:228
void transform_goto_model()
Applies function contracts and loop contracts transformation to GOTO model using the dynamic frame co...
Definition dfcc.cpp:496
dfcc_instrumentt instrument
Definition dfcc.h:221
dfcc_libraryt library
Definition dfcc.h:217
void wrap_replaced_functions()
Definition dfcc.cpp:389
message_handlert & message_handler
Definition dfcc.h:212
const irep_idt & harness_id
Definition dfcc.h:206
dfcc_contract_clauses_codegent contract_clauses_codegen
Definition dfcc.h:220
const bool allow_recursive_calls
Definition dfcc.h:208
std::set< irep_idt > other_symbols
Definition dfcc.h:232
dfcc_contract_handlert contract_handler
Definition dfcc.h:223
const std::map< irep_idt, irep_idt > & to_replace
Definition dfcc.h:209
void partition_function_symbols(std::set< irep_idt > &pure_contract_symbols, std::set< irep_idt > &other_symbols)
Partitions the function symbols of the symbol table into pure contracts and other function symbols sy...
Definition dfcc.cpp:286
void wrap_discovered_function_pointer_contracts()
Definition dfcc.cpp:406
namespacet ns
Definition dfcc.h:218
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Exception thrown for bad function/contract specification pairs passed on the CLI.
Definition dfcc.h:74
invalid_function_contract_pair_exceptiont(std::string reason, std::string correct_format="")
Definition dfcc.cpp:51
std::string what() const override
A human readable description of what went wrong.
Definition dfcc.cpp:59
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
Symbol table entry.
Definition symbol.h:28
Translates assigns and frees clauses of a function contract or loop contract into goto programs that ...
Specialisation of dfcc_contract_handlert for contracts.
Add instrumentation to a goto program to perform frame condition checks.
Dynamic frame condition checking library loading.
Collects all user-defined predicates that call functions is_fresh, pointer_in_range,...
Enumeration representing the instrumentation mode for loop contracts.
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
Translate functions that specify assignable and freeable targets declaratively into active functions ...
Given a function_id and contract_id, swaps its body to a function with a fresh mangled name,...
void dfcc(const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const optionalt< irep_idt > &to_check, const bool allow_recursive_calls, const std::set< irep_idt > &to_replace, const bool apply_loop_contracts, const bool unwind_transformed_loops, const std::set< std::string > &to_exclude_from_nondet_static, message_handlert &message_handler)
Applies function contracts transformation to GOTO model, using the dynamic frame condition checking a...
Definition dfcc.cpp:116
nonstd::optional< T > optionalt
Definition optional.h:35