Skip to content

Commit 0255aa2

Browse files
author
Remi Delmas
committed
CONTRACTS: Add dfcc_dsl_contract_handlert class
This class implements the abstract `dfcc_contract_handlert` interface for DSL-style contracts by delegating to the class `dfcc_dsl_wrapper_programt`.
1 parent e96aede commit 0255aa2

File tree

4 files changed

+379
-2
lines changed

4 files changed

+379
-2
lines changed

‎src/goto-instrument/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ SRC = accelerate/accelerate.cpp \
2525
contracts/dynamic-frames/dfcc_spec_functions.cpp \
2626
contracts/dynamic-frames/dfcc_dsl_contract_functions.cpp \
2727
contracts/dynamic-frames/dfcc_dsl_wrapper_program.cpp \
28+
contracts/dynamic-frames/dfcc_dsl_contract_handler.cpp \
2829
contracts/havoc_assigns_clause_targets.cpp \
2930
contracts/instrument_spec_assigns.cpp \
3031
contracts/memory_predicates.cpp \

‎src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_contract_handler.cpp

Lines changed: 210 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,210 @@
1+
/*******************************************************************\
2+
3+
Module: Dynamic frame condition checking for function contracts
4+
5+
Author: Remi Delmas, [email protected]
6+
Date: August 2022
7+
8+
\*******************************************************************/
9+
10+
#include "dfcc_dsl_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_expr.h>
16+
#include <util/format_type.h>
17+
#include <util/fresh_symbol.h>
18+
#include <util/invariant.h>
19+
#include <util/mathematical_expr.h>
20+
#include <util/namespace.h>
21+
#include <util/pointer_offset_size.h>
22+
#include <util/std_expr.h>
23+
24+
#include <goto-programs/goto_model.h>
25+
#include <goto-programs/remove_function_pointers.h>
26+
27+
#include <ansi-c/c_expr.h>
28+
#include <goto-instrument/contracts/contracts.h>
29+
#include <goto-instrument/contracts/utils.h>
30+
#include <langapi/language_util.h>
31+
32+
#include "dfcc_dsl_wrapper_program.h"
33+
#include "dfcc_instrument.h"
34+
#include "dfcc_library.h"
35+
#include "dfcc_spec_functions.h"
36+
#include "dfcc_utils.h"
37+
38+
std::map<irep_idt, dfcc_dsl_contract_functionst>
39+
dfcc_dsl_contract_handlert::contract_cache;
40+
41+
dfcc_dsl_contract_handlert::dfcc_dsl_contract_handlert(
42+
goto_modelt &goto_model,
43+
messaget &log,
44+
dfcc_utilst &utils,
45+
dfcc_libraryt &library,
46+
dfcc_instrumentt &instrument,
47+
dfcc_spec_functionst &spec_functions)
48+
: goto_model(goto_model),
49+
log(log),
50+
message_handler(log.get_message_handler()),
51+
utils(utils),
52+
library(library),
53+
instrument(instrument),
54+
spec_functions(spec_functions),
55+
ns(goto_model.symbol_table)
56+
{
57+
}
58+
59+
const dfcc_dsl_contract_functionst &
60+
dfcc_dsl_contract_handlert::get_contract_functions(const irep_idt &contract_id)
61+
{
62+
auto found = dfcc_dsl_contract_handlert::contract_cache.find(contract_id);
63+
if(found == dfcc_dsl_contract_handlert::contract_cache.end())
64+
{
65+
dfcc_dsl_contract_handlert::contract_cache.insert(
66+
{contract_id,
67+
dfcc_dsl_contract_functionst(
68+
get_pure_contract_symbol(contract_id),
69+
goto_model,
70+
log,
71+
utils,
72+
library,
73+
spec_functions)});
74+
}
75+
return dfcc_dsl_contract_handlert::contract_cache.at(contract_id);
76+
}
77+
78+
const int
79+
dfcc_dsl_contract_handlert::get_assigns_clause_size(const irep_idt &contract_id)
80+
{
81+
return get_contract_functions(contract_id).get_nof_assigns_targets();
82+
}
83+
84+
void dfcc_dsl_contract_handlert::add_contract_instructions(
85+
const dfcc_contract_modet contract_mode,
86+
const irep_idt &wrapper_id,
87+
const irep_idt &wrapped_id,
88+
const irep_idt &contract_id,
89+
const symbolt &wrapper_write_set_symbol,
90+
goto_programt &dest,
91+
std::set<irep_idt> &function_pointer_contracts)
92+
{
93+
dfcc_dsl_wrapper_programt(
94+
contract_mode,
95+
utils.get_function_symbol(wrapper_id),
96+
utils.get_function_symbol(wrapped_id),
97+
get_contract_functions(contract_id),
98+
wrapper_write_set_symbol,
99+
goto_model,
100+
log,
101+
utils,
102+
library,
103+
instrument)
104+
.add_to_dest(dest, function_pointer_contracts);
105+
}
106+
107+
const symbolt *dfcc_dsl_contract_handlert::get_pure_contract_symbol_ptr(
108+
const irep_idt &contract_id)
109+
{
110+
const auto &contract_symbol = utils.get_function_symbol(contract_id);
111+
const symbolt *pure_contract_symbol = nullptr;
112+
auto pure_contract_id = "contract::" + id2string(contract_id);
113+
if(!ns.lookup(pure_contract_id, pure_contract_symbol))
114+
{
115+
log.debug() << "contract_symbol: " << contract_symbol.name << messaget::eom;
116+
log.debug() << contract_symbol.type.pretty() << messaget::eom;
117+
log.debug() << "pure_contract_symbol: " << pure_contract_id
118+
<< messaget::eom;
119+
log.debug() << pure_contract_symbol->type.pretty() << messaget::eom;
120+
121+
check_signature_compat(
122+
contract_id,
123+
to_code_type(contract_symbol.type),
124+
pure_contract_id,
125+
to_code_type(pure_contract_symbol->type));
126+
}
127+
else
128+
{
129+
// The contract symbol might not have been created if the function had
130+
// no contract or a contract with all empty clauses (which is equivalent).
131+
// in that case we create a fresh symbol again with empty clauses
132+
symbolt new_symbol;
133+
new_symbol.name = pure_contract_id;
134+
new_symbol.base_name = pure_contract_id;
135+
new_symbol.pretty_name = pure_contract_id;
136+
new_symbol.is_property = true;
137+
new_symbol.type = contract_symbol.type;
138+
new_symbol.mode = contract_symbol.mode;
139+
new_symbol.module = contract_symbol.module;
140+
new_symbol.location = contract_symbol.location;
141+
auto entry = goto_model.symbol_table.insert(std::move(new_symbol));
142+
if(!entry.second)
143+
{
144+
log.error().source_location = contract_symbol.location;
145+
log.error() << "contract '" << contract_symbol.display_name()
146+
<< "' already set at " << entry.first.location.as_string()
147+
<< messaget::eom;
148+
throw 0;
149+
}
150+
// this lookup must work, and no need to check for signature compatibility
151+
ns.lookup(pure_contract_id, pure_contract_symbol);
152+
}
153+
return pure_contract_symbol;
154+
}
155+
156+
const symbolt &dfcc_dsl_contract_handlert::get_pure_contract_symbol(
157+
const irep_idt &contract_id)
158+
{
159+
auto result = get_pure_contract_symbol_ptr(contract_id);
160+
if(result != nullptr)
161+
return *result;
162+
163+
log.error() << "dfcc_dsl_contract_handlert: pure contract symbol for "
164+
<< contract_id << " was not found, aborting" << messaget::eom;
165+
throw 0;
166+
}
167+
168+
const bool dfcc_dsl_contract_handlert::pure_contract_symbol_exists(
169+
const irep_idt &contract_id)
170+
{
171+
auto result = get_pure_contract_symbol_ptr(contract_id);
172+
return result != nullptr;
173+
}
174+
175+
void dfcc_dsl_contract_handlert::check_signature_compat(
176+
const irep_idt &contract_id,
177+
const code_typet &contract_type,
178+
const irep_idt &pure_contract_id,
179+
const code_typet &pure_contract_type)
180+
{
181+
// can we turn a call to `contract` into a call to `pure_contract` ?
182+
bool compatible =
183+
function_is_type_compatible(true, contract_type, pure_contract_type, ns);
184+
185+
if(!compatible)
186+
{
187+
log.error() << "dfcc_dsl_contract_handlert: function '" << contract_id
188+
<< "' and the corresponding pure contract symbol '"
189+
<< pure_contract_id
190+
<< "' have incompatible type signatures:" << messaget::eom;
191+
log.error() << "- contract return type "
192+
<< format(contract_type.return_type()) << messaget::eom;
193+
for(const auto &param : contract_type.parameters())
194+
{
195+
log.error() << "- contract param type " << format(param.type())
196+
<< messaget::eom;
197+
}
198+
199+
log.error() << "- pure contract return type "
200+
<< format(pure_contract_type.return_type()) << messaget::eom;
201+
for(const auto &param : pure_contract_type.parameters())
202+
{
203+
log.error() << "- pure contract param type " << format(param.type())
204+
<< messaget::eom;
205+
}
206+
207+
log.error() << "aborting." << messaget::eom;
208+
throw 0;
209+
}
210+
}

‎src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_contract_handler.h

Lines changed: 166 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,166 @@
1+
/*******************************************************************\
2+
3+
Module: Dynamic frame condition checking for function contracts
4+
5+
Author: Remi Delmas, [email protected]
6+
Date: August 2022
7+
8+
\*******************************************************************/
9+
10+
/// \file
11+
/// Specialisation of \ref dfcc_contract_handlert for DSL-style contracts
12+
13+
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_DSL_CONTRACT_HANDLER_H
14+
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_DSL_CONTRACT_HANDLER_H
15+
16+
#include <goto-programs/goto_convert_class.h>
17+
18+
#include <util/namespace.h>
19+
#include <util/optional.h>
20+
#include <util/std_expr.h>
21+
22+
#include "dfcc_contract_handler.h"
23+
#include "dfcc_dsl_contract_functions.h"
24+
25+
#include <set>
26+
27+
class goto_modelt;
28+
class messaget;
29+
class message_handlert;
30+
class dfcc_libraryt;
31+
class dfcc_utilst;
32+
class dfcc_instrumentt;
33+
class dfcc_spec_functionst;
34+
class code_with_contract_typet;
35+
class conditional_target_group_exprt;
36+
class function_pointer_obeys_contract_exprt;
37+
38+
/// A DSL-style contract is represented by a function declaration or definition
39+
/// with contract clauses attached to its signature:
40+
///
41+
/// ```
42+
/// ret_t foo(foo_params)
43+
/// __CPROVER_requires(R)
44+
/// __CPROVER_requires_contract(ptr, contract)
45+
/// __CPROVER_assigns(A)
46+
/// __CPROVER_frees(F)
47+
/// __CPROVER_ensures(E)
48+
/// __CPROVER_ensures_contract(ptr, contract)
49+
/// { foo_body; } [optional]
50+
/// ```
51+
///
52+
/// In the symbol table, this declaration creates two symbols:
53+
/// - `ret_t foo(foo_params)` which represents the function (with optional body)
54+
/// - `ret_t contract::foo(foo_params)` which represents the pure contract part
55+
/// and carries the contract clauses in its `.type` attribute.
56+
///
57+
/// This class allows, given a contract name `foo`, to lookup the symbol
58+
/// `contract::foo` and translate its assigns and frees clauses into GOTO
59+
/// functions that build dynamic frames at runtime (stored in an object of
60+
/// type \ref dfcc_dsl_contract_functionst).
61+
///
62+
/// Translation results are cached so it is safe to call
63+
/// `get_contract_functions` several times.
64+
class dfcc_dsl_contract_handlert : public dfcc_contract_handlert
65+
{
66+
public:
67+
dfcc_dsl_contract_handlert(
68+
goto_modelt &goto_model,
69+
messaget &log,
70+
dfcc_utilst &utils,
71+
dfcc_libraryt &library,
72+
dfcc_instrumentt &instrument,
73+
dfcc_spec_functionst &spec_functions);
74+
75+
/// Adds instructions in `dest` modeling contract checking, assuming
76+
/// that `ret_t wrapper_id(params)` is the function receiving
77+
/// the instructions.
78+
///
79+
/// \param[in] contract_mode checking or replacement mode
80+
/// \param[in] wrapper_id name of function receiving the instructions
81+
/// \param[in] wrapped_id name of function that is being checked/replaced
82+
/// \param[in] contract_id name of the contract to check
83+
/// \param[in] wrapper_write_set_symbol write_set parameter of the wrapper
84+
/// \param[out] dest destination program where instructions are added
85+
/// (should eventually become the body of wrapper_id)
86+
/// \param[out] function_pointer_contracts list of contracts found in either
87+
/// pre or post conditions of the processed contract. These contracts need to
88+
/// be swapped_and_wrapped in replacement mode if they are not already.
89+
void add_contract_instructions(
90+
const dfcc_contract_modet contract_mode,
91+
const irep_idt &wrapper_id,
92+
const irep_idt &wrapped_id,
93+
const irep_idt &contract_id,
94+
const symbolt &wrapper_write_set_symbol,
95+
goto_programt &dest,
96+
std::set<irep_idt> &function_pointer_contracts) override;
97+
98+
/// Returns the size assigns clause of the given contract in number of targets
99+
const int get_assigns_clause_size(const irep_idt &contract_id) override;
100+
101+
/// Searches for a symbol named "contract::contract_id" that has a type
102+
/// signature compatible with that of "contract_id", or creates an empty one
103+
/// if it does not exist.
104+
/// Returns true if found or created, throws an exception if
105+
/// "contract::contract_id" already exists but has signature incompatible
106+
/// with that of "contract_id".
107+
const bool pure_contract_symbol_exists(const irep_idt &contract_id);
108+
109+
protected:
110+
goto_modelt &goto_model;
111+
messaget &log;
112+
message_handlert &message_handler;
113+
dfcc_utilst &utils;
114+
dfcc_libraryt &library;
115+
dfcc_instrumentt &instrument;
116+
dfcc_spec_functionst &spec_functions;
117+
namespacet ns;
118+
119+
// Caches the functions generated from DSL contracts
120+
static std::map<irep_idt, dfcc_dsl_contract_functionst> contract_cache;
121+
122+
/// Searches for a symbol named "contract::contract_id" in the symbol table.
123+
///
124+
/// If a symbol "contract::contract_id" was found and its type signature is
125+
/// compatible with that of "contract_id" a pointer to the symbol is returned.
126+
///
127+
/// If a symbol "contract::contract_id" was found but its type signature is
128+
/// not compatible with that of "contract_id" an exception is thrown.
129+
///
130+
/// If a symbol "contract::contract_id" was found, a fresh symbol representing
131+
/// a contract with empty clauses is inserted in the symbol table and a
132+
/// pointer to that symbol is returned.
133+
const symbolt *get_pure_contract_symbol_ptr(const irep_idt &contract_id);
134+
135+
/// Searches for a symbol named "contract::contract_id" in the symbol table.
136+
///
137+
/// If a symbol "contract::contract_id" was found and its type signature is
138+
/// compatible with that of "contract_id" a reference to the symbol is
139+
/// returned.
140+
///
141+
/// If a symbol "contract::contract_id" was found but its type signature is
142+
/// not compatible with that of "contract_id" an exception is thrown.
143+
///
144+
/// If a symbol "contract::contract_id" was found, a fresh symbol representing
145+
/// a contract with empty clauses is inserted in the symbol table and a
146+
/// reference to that symbol is returned.
147+
const symbolt &get_pure_contract_symbol(const irep_idt &contract_id);
148+
149+
/// Returns the `dfcc_dsl_contract_functionst` object for the given contract
150+
/// from the cache, creates it if it does not exists.
151+
const dfcc_dsl_contract_functionst &
152+
get_contract_functions(const irep_idt &contract_id);
153+
154+
/// \brief Throws an error if the type signatures are not compatible
155+
/// \param contract_id name of the function that carries the contract
156+
/// \param contract_type code_type of contract_id
157+
/// \param pure_contract_id name of the pure contract symbol for contract_id
158+
/// \param pure_contract_type code_type of pure_contract_id
159+
void check_signature_compat(
160+
const irep_idt &contract_id,
161+
const code_typet &contract_type,
162+
const irep_idt &pure_contract_id,
163+
const code_typet &pure_contract_type);
164+
};
165+
166+
#endif

‎src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_wrapper_program.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,8 @@ Author: Remi Delmas, [email protected]
1010
/// Generates the body of a wrapper function from a DSL-style contract
1111
/// for contract checking or contract replacement
1212

13-
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DFCC_DSL_WRAPPER_PROGRAM_H
14-
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DFCC_DSL_WRAPPER_PROGRAM_H
13+
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_DSL_WRAPPER_PROGRAM_H
14+
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_DSL_WRAPPER_PROGRAM_H
1515

1616
#include <goto-programs/goto_convert_class.h>
1717

0 commit comments

Comments
 (0)