CBMC
dfcc_contract_handler.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for function contracts
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 Date: August 2022
7 
8 \*******************************************************************/
9 
10 #include "dfcc_contract_handler.h"
11 
12 #include <util/arith_tools.h>
13 #include <util/c_types.h>
14 #include <util/expr_util.h>
15 #include <util/format_type.h>
16 #include <util/fresh_symbol.h>
17 #include <util/invariant.h>
18 #include <util/mathematical_expr.h>
19 #include <util/namespace.h>
21 #include <util/std_expr.h>
22 
25 
26 #include <ansi-c/c_expr.h>
28 #include <langapi/language_util.h>
29 
30 #include "dfcc_instrument.h"
31 #include "dfcc_library.h"
32 #include "dfcc_spec_functions.h"
33 #include "dfcc_wrapper_program.h"
34 
35 std::map<irep_idt, dfcc_contract_functionst>
37 
39  goto_modelt &goto_model,
40  message_handlert &message_handler,
41  dfcc_libraryt &library,
42  dfcc_instrumentt &instrument,
43  dfcc_lift_memory_predicatest &memory_predicates,
44  dfcc_spec_functionst &spec_functions,
45  dfcc_contract_clauses_codegent &contract_clauses_codegen)
46  : goto_model(goto_model),
47  message_handler(message_handler),
48  log(message_handler),
49  library(library),
50  instrument(instrument),
51  memory_predicates(memory_predicates),
52  spec_functions(spec_functions),
53  contract_clauses_codegen(contract_clauses_codegen),
54  ns(goto_model.symbol_table)
55 {
56 }
57 
60 {
61  auto iter = dfcc_contract_handlert::contract_cache.find(contract_id);
62 
63  // return existing value
65  return iter->second;
66 
67  // insert new value
69  .insert(
70  {contract_id,
72  get_pure_contract_symbol(contract_id),
73  goto_model,
75  library,
78  instrument)})
79  .first->second;
80 }
81 
82 const std::size_t
84 {
85  return get_contract_functions(contract_id).get_nof_assigns_targets();
86 }
87 
89  const dfcc_contract_modet contract_mode,
90  const irep_idt &wrapper_id,
91  const irep_idt &wrapped_id,
92  const irep_idt &contract_id,
93  const symbolt &wrapper_write_set_symbol,
94  goto_programt &dest,
95  std::set<irep_idt> &function_pointer_contracts)
96 {
98  contract_mode,
101  get_contract_functions(contract_id),
102  wrapper_write_set_symbol,
103  goto_model,
105  library,
106  instrument,
108  .add_to_dest(dest, function_pointer_contracts);
109 }
110 
112  const irep_idt &contract_id,
113  const std::optional<irep_idt> function_id_opt)
114 {
115  auto pure_contract_id = "contract::" + id2string(contract_id);
116  const symbolt *pure_contract_symbol = nullptr;
117  if(!ns.lookup(pure_contract_id, pure_contract_symbol))
118  {
119  if(function_id_opt.has_value())
120  {
121  auto function_id = function_id_opt.value();
122  const auto &function_symbol =
125  function_id,
126  to_code_type(function_symbol.type),
127  pure_contract_id,
128  to_code_type(pure_contract_symbol->type));
129  }
130  return *pure_contract_symbol;
131  }
132  else
133  {
134  // The contract symbol might not have been created if the function had
135  // no contract or a contract with all empty clauses (which is equivalent).
136  // in that case we create a fresh symbol again with empty clauses.
138  function_id_opt.has_value(),
139  "Contract '" + pure_contract_id +
140  "' not found, the identifier of an existing function must be provided "
141  "to derive a default contract");
142 
143  auto function_id = function_id_opt.value();
144  const auto &function_symbol =
146 
147  log.warning() << "Contract '" << contract_id
148  << "' not found, deriving empty pure contract '"
149  << pure_contract_id << "' from function '" << function_id
150  << "'" << messaget::eom;
151 
152  symbolt new_symbol{
153  pure_contract_id, function_symbol.type, function_symbol.mode};
154  new_symbol.base_name = pure_contract_id;
155  new_symbol.pretty_name = pure_contract_id;
156  new_symbol.is_property = true;
157  new_symbol.module = function_symbol.module;
158  new_symbol.location = function_symbol.location;
159  auto entry = goto_model.symbol_table.insert(std::move(new_symbol));
160  INVARIANT(
161  entry.second,
162  "contract '" + id2string(function_symbol.display_name()) +
163  "' already set at " + id2string(entry.first.location.as_string()));
164  // this lookup will work and set the pointer
165  // no need to check for signature compatibility
166  ns.lookup(pure_contract_id, pure_contract_symbol);
167  return *pure_contract_symbol;
168  }
169 }
170 
172  const irep_idt &contract_id,
173  const code_typet &contract_type,
174  const irep_idt &pure_contract_id,
175  const code_typet &pure_contract_type)
176 {
177  // can we turn a call to `contract` into a call to `pure_contract` ?
178  bool compatible =
179  function_is_type_compatible(true, contract_type, pure_contract_type, ns);
180 
181  if(!compatible)
182  {
183  std::ostringstream err_msg;
184  err_msg << "dfcc_contract_handlert: function '" << contract_id
185  << "' and the corresponding pure contract symbol '"
186  << pure_contract_id << "' have incompatible type signatures:\n";
187 
188  err_msg << "- contract return type "
189  << from_type(ns, contract_id, contract_type.return_type()) << "\n";
190 
191  for(const auto &param : contract_type.parameters())
192  {
193  err_msg << "- contract param type "
194  << from_type(ns, contract_id, param.type()) << "\n";
195  }
196 
197  err_msg << "- pure contract return type "
198  << from_type(ns, pure_contract_id, pure_contract_type.return_type())
199  << "\n";
200 
201  for(const auto &param : pure_contract_type.parameters())
202  {
203  err_msg << "- pure contract param type "
204  << from_type(ns, pure_contract_id, param.type()) << "\n";
205  }
206 
207  err_msg << "aborting."
208  << "\n";
210  err_msg.str(), contract_type.source_location());
211  }
212 }
API to expression classes that are internal to the C frontend.
Base type of functions.
Definition: std_types.h:583
const typet & return_type() const
Definition: std_types.h:689
const parameterst & parameters() const
Definition: std_types.h:699
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
Generates GOTO functions modelling a contract assigns and frees clauses.
const std::size_t get_nof_assigns_targets() const
Returns the maximum number of targets in the assigns clause.
void check_signature_compat(const irep_idt &contract_id, const code_typet &contract_type, const irep_idt &pure_contract_id, const code_typet &pure_contract_type)
Throws an error if the type signatures are not compatible.
dfcc_spec_functionst & spec_functions
const symbolt & get_pure_contract_symbol(const irep_idt &contract_id, const std::optional< irep_idt > function_id_opt={})
Searches for a symbol named "contract::contract_id" in the symbol table.
static std::map< irep_idt, dfcc_contract_functionst > contract_cache
dfcc_lift_memory_predicatest & memory_predicates
message_handlert & message_handler
dfcc_contract_clauses_codegent & contract_clauses_codegen
const std::size_t get_assigns_clause_size(const irep_idt &contract_id)
Returns the size assigns clause of the given contract in number of targets.
void add_contract_instructions(const dfcc_contract_modet contract_mode, const irep_idt &wrapper_id, const irep_idt &wrapped_id, const irep_idt &contract_id, const symbolt &wrapper_write_set_symbol, goto_programt &dest, std::set< irep_idt > &function_pointer_contracts)
Adds instructions in dest modeling contract checking, assuming that ret_t wrapper_id(params) is the f...
dfcc_instrumentt & instrument
dfcc_contract_handlert(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)
const dfcc_contract_functionst & get_contract_functions(const irep_idt &contract_id)
Returns the dfcc_contract_functionst object for the given contract from the cache,...
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.
Definition: dfcc_library.h:154
This class rewrites GOTO functions that use the built-ins:
Generates the body of a wrapper function from a contract specified using requires,...
void add_to_dest(goto_programt &dest, std::set< irep_idt > &dest_fp_contracts)
Adds the whole program to dest and the discovered function pointer contracts dest_fp_contracts.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
Thrown when we can't handle something in an input source file.
mstreamt & warning() const
Definition: message.h:396
static eomt eom
Definition: message.h:289
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
exprt value
Initial value of symbol.
Definition: symbol.h:34
const source_locationt & source_location() const
Definition: type.h:72
Specialisation of dfcc_contract_handlert for contracts.
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
Add instrumentation to a goto program to perform frame condition checks.
Dynamic frame condition checking library loading.
Translate functions that specify assignable and freeable targets declaratively into active functions ...
Generates the body of a wrapper function from a contract for contract checking or contract replacemen...
Deprecated expression utility functions.
Fresh auxiliary symbol creation.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
double log(double x)
Definition: math.c:2776
API to expression classes for 'mathematical' expressions.
Pointer Logic.
bool function_is_type_compatible(bool return_value_used, const code_typet &call_type, const code_typet &function_type, const namespacet &ns)
Returns true iff call_type can be converted to produce a function call of the same type as function_t...
Remove Indirect Function Calls.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464
API to expression classes.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
Definition: dfcc_utils.cpp:72