CBMC
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"
41#include "dfcc_spec_functions.h"
42#include "dfcc_swap_and_wrap.h"
43
44#include <map>
45#include <set>
46
47class goto_modelt;
48class messaget;
50class symbolt;
52class optionst;
53
54#define FLAG_DFCC "dfcc"
55#define OPT_DFCC "(" FLAG_DFCC "):"
56
57#define HELP_DFCC \
58 " {y--dfcc} {uharness} \t " \
59 "activate dynamic frame condition checking for contracts using the given " \
60 "harness as entry point\n"
61
62#define FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec"
63#define OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):"
64#define HELP_ENFORCE_CONTRACT_REC \
65 " {y--enforce-contract-rec} {ufunction}[{y/}{ucontract}] \t " \
66 "wrap {ufunction} with an assertion of the contract and assume recursive " \
67 "calls to " \
68 "{ufunction} satisfy the contract\n"
69
73{
74public:
76 std::string reason,
77 std::string correct_format = "");
78
79 std::string what() const override;
80
81 std::string correct_format;
82};
83
102void dfcc(
103 const optionst &options,
104 goto_modelt &goto_model,
105 const irep_idt &harness_id,
106 const std::optional<irep_idt> &to_check,
107 const bool allow_recursive_calls,
108 const std::set<irep_idt> &to_replace,
109 const loop_contract_configt loop_contract_config,
110 const std::set<std::string> &to_exclude_from_nondet_static,
111 message_handlert &message_handler);
112
115class dfcct
116{
117public:
129 dfcct(
130 const optionst &options,
132 const irep_idt &harness_id,
133 const std::optional<std::pair<irep_idt, irep_idt>> &to_check,
134 const bool allow_recursive_calls,
135 const std::map<irep_idt, irep_idt> &to_replace,
138 const std::set<std::string> &to_exclude_from_nondet_static);
139
165
166protected:
170 const std::optional<std::pair<irep_idt, irep_idt>> &to_check;
172 const std::map<irep_idt, irep_idt> &to_replace;
174 const std::set<std::string> &to_exclude_from_nondet_static;
177
178 // Singletons that hold the global state of the program transformation
179 // (caches etc.)
188
192
193 // partition the set of functions of the goto_model
194 std::set<irep_idt> pure_contract_symbols;
195 std::set<irep_idt> other_symbols;
196 std::set<irep_idt> function_pointer_contracts;
197
213
217 std::set<irep_idt> &pure_contract_symbols,
218 std::set<irep_idt> &other_symbols);
219
227
273 void reinitialize_model();
274};
275
276#endif
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition c_expr.h:233
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:116
goto_modelt & goto_model
Definition dfcc.h:168
std::set< irep_idt > function_pointer_contracts
Definition dfcc.h:196
const optionst & options
Definition dfcc.h:167
std::set< irep_idt > pure_contract_symbols
Definition dfcc.h:194
dfcc_spec_functionst spec_functions
Definition dfcc.h:182
void instrument_harness_function()
Definition dfcc.cpp:291
void instrument_other_functions()
Definition dfcc.cpp:432
const loop_contract_configt loop_contract_config
Definition dfcc.h:173
void reinitialize_model()
Re-initialise the GOTO model.
Definition dfcc.cpp:507
const std::set< std::string > & to_exclude_from_nondet_static
Definition dfcc.h:174
void link_model_and_load_dfcc_library()
Definition dfcc.cpp:269
dfcc_swap_and_wrapt swap_and_wrap
Definition dfcc.h:187
dfcc_lift_memory_predicatest memory_predicates
Definition dfcc.h:185
void wrap_checked_function()
Definition dfcc.cpp:316
void lift_memory_predicates()
Definition dfcc.cpp:304
messaget log
Definition dfcc.h:176
const std::optional< std::pair< irep_idt, irep_idt > > & to_check
Definition dfcc.h:170
void check_transform_goto_model_preconditions()
Checks preconditions on arguments of transform_goto_model.
Definition dfcc.cpp:172
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:191
void transform_goto_model()
Applies function contracts and loop contracts transformation to GOTO model using the dynamic frame co...
Definition dfcc.cpp:452
dfcc_instrumentt instrument
Definition dfcc.h:184
dfcc_libraryt library
Definition dfcc.h:180
void wrap_replaced_functions()
Definition dfcc.cpp:345
message_handlert & message_handler
Definition dfcc.h:175
const irep_idt & harness_id
Definition dfcc.h:169
dfcc_contract_clauses_codegent contract_clauses_codegen
Definition dfcc.h:183
const bool allow_recursive_calls
Definition dfcc.h:171
std::set< irep_idt > other_symbols
Definition dfcc.h:195
dfcc_contract_handlert contract_handler
Definition dfcc.h:186
const std::map< irep_idt, irep_idt > & to_replace
Definition dfcc.h:172
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:236
void wrap_discovered_function_pointer_contracts()
Definition dfcc.cpp:362
namespacet ns
Definition dfcc.h:181
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Exception thrown for bad function/contract specification pairs passed on the CLI.
Definition dfcc.h:73
std::string what() const override
A human readable description of what went wrong.
Definition dfcc.cpp:38
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: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,...
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 std::optional< irep_idt > &to_check, const bool allow_recursive_calls, const std::set< irep_idt > &to_replace, const loop_contract_configt loop_contract_config, 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:93
Loop contract configurations.