cprover
Loading...
Searching...
No Matches
dfcc_contract_clauses_codegen.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for function contracts
4
5Author: Remi Delmas, delmasrd@amazon.com
6Date: February 2023
7
8\*******************************************************************/
10
11#include <util/c_types.h>
12#include <util/expr_util.h>
13#include <util/fresh_symbol.h>
14#include <util/invariant.h>
16#include <util/namespace.h>
17#include <util/pointer_expr.h>
19#include <util/std_expr.h>
20
22
23#include <ansi-c/c_expr.h>
27
28#include "dfcc_library.h"
29#include "dfcc_utils.h"
30
32 goto_modelt &goto_model,
33 message_handlert &message_handler,
34 dfcc_libraryt &library)
35 : goto_model(goto_model),
36 message_handler(message_handler),
37 log(message_handler),
38 library(library),
39 ns(goto_model.symbol_table)
40{
41}
42
44 const irep_idt &language_mode,
45 const exprt::operandst &assigns_clause,
46 goto_programt &dest)
47{
48 for(const auto &expr : assigns_clause)
49 {
50 if(
51 auto target_group =
53 {
54 encode_assignable_target_group(language_mode, *target_group, dest);
55 }
56 else
57 {
58 encode_assignable_target(language_mode, expr, dest);
59 }
60 }
61
62 // inline resulting program and check for loops
64 dest.update();
66 is_loop_free(dest, ns, log),
67 "loops in assigns clause specification functions must be unwound before "
68 "contracts instrumentation");
69}
70
72 const irep_idt &language_mode,
73 const exprt::operandst &frees_clause,
74 goto_programt &dest)
75{
76 for(const auto &expr : frees_clause)
77 {
78 if(
79 auto target_group =
81 {
82 encode_freeable_target_group(language_mode, *target_group, dest);
83 }
84 else
85 {
86 encode_freeable_target(language_mode, expr, dest);
87 }
88 }
89
90 // inline resulting program and check for loops
93 is_loop_free(dest, ns, log),
94 "loops in assigns clause specification functions must be unwound before "
95 "contracts instrumentation");
96}
97
99 const irep_idt &language_mode,
101 goto_programt &dest)
102{
103 const source_locationt &source_location = group.source_location();
104
105 // clean up side effects from the condition expression if needed
107 exprt condition(group.condition());
108 std::list<irep_idt> new_vars;
109 if(has_subexpr(condition, ID_side_effect))
110 new_vars = cleaner.clean(condition, dest, language_mode);
111
112 // Jump target if condition is false
113 auto goto_instruction = dest.add(goto_programt::make_incomplete_goto(
114 boolean_negate(condition), source_location));
115
116 for(const auto &target : group.targets())
117 encode_assignable_target(language_mode, target, dest);
118
119 auto label_instruction = dest.add(goto_programt::make_skip(source_location));
120 goto_instruction->complete_goto(label_instruction);
121
122 destruct_locals(new_vars, dest, ns);
123}
124
126 const irep_idt &language_mode,
127 const exprt &target,
128 goto_programt &dest)
129{
130 const source_locationt &source_location = target.source_location();
131
133 {
134 // A function call target `foo(params)` becomes `CALL foo(params);`
135 const auto &funcall = to_side_effect_expr_function_call(target);
136 code_function_callt code_function_call(to_symbol_expr(funcall.function()));
137 auto &arguments = code_function_call.arguments();
138 for(auto &arg : funcall.arguments())
139 arguments.emplace_back(arg);
140 dest.add(
141 goto_programt::make_function_call(code_function_call, source_location));
142 }
143 else if(is_assignable(target))
144 {
145 // An lvalue `target` becomes
146 //` CALL __CPROVER_assignable(&target, sizeof(target), is_ptr_to_ptr);`
147 const auto &size =
149
150 if(!size.has_value())
151 {
153 "no definite size for lvalue assigns clause target " +
154 from_expr_using_mode(ns, language_mode, target),
155 target.source_location()};
156 }
157 // we have to build the symbol manually because it might not
158 // be present in the symbol table if the user program does not already
159 // use it.
160 code_function_callt code_function_call(
161 symbol_exprt(CPROVER_PREFIX "assignable", empty_typet()));
162 auto &arguments = code_function_call.arguments();
163
164 // ptr
165 arguments.emplace_back(typecast_exprt::conditional_cast(
167
168 // size
169 arguments.emplace_back(size.value());
170
171 // is_ptr_to_ptr
172 arguments.emplace_back(make_boolean_expr(target.type().id() == ID_pointer));
173
174 dest.add(
175 goto_programt::make_function_call(code_function_call, source_location));
176 }
177 else
178 {
179 // any other type of target is unsupported
181 "unsupported assigns clause target " +
182 from_expr_using_mode(ns, language_mode, target),
183 target.source_location());
184 }
185}
186
188 const irep_idt &language_mode,
190 goto_programt &dest)
191{
192 const source_locationt &source_location = group.source_location();
193
194 // clean up side effects from the condition expression if needed
196 exprt condition(group.condition());
197 std::list<irep_idt> new_vars;
198 if(has_subexpr(condition, ID_side_effect))
199 new_vars = cleaner.clean(condition, dest, language_mode);
200
201 // Jump target if condition is false
202 auto goto_instruction = dest.add(goto_programt::make_incomplete_goto(
203 boolean_negate(condition), source_location));
204
205 for(const auto &target : group.targets())
206 encode_freeable_target(language_mode, target, dest);
207
208 auto label_instruction = dest.add(goto_programt::make_skip(source_location));
209 goto_instruction->complete_goto(label_instruction);
210
211 destruct_locals(new_vars, dest, ns);
212}
213
215 const irep_idt &language_mode,
216 const exprt &target,
217 goto_programt &dest)
218{
219 const source_locationt &source_location = target.source_location();
220
222 {
223 const auto &funcall = to_side_effect_expr_function_call(target);
224 if(can_cast_expr<symbol_exprt>(funcall.function()))
225 {
226 // for calls to user-defined functions a call expression `foo(params)`
227 // becomes an instruction `CALL foo(params);`
228 code_function_callt code_function_call(
229 to_symbol_expr(funcall.function()));
230 auto &arguments = code_function_call.arguments();
231 for(auto &arg : funcall.arguments())
232 arguments.emplace_back(arg);
233 dest.add(
234 goto_programt::make_function_call(code_function_call, source_location));
235 }
236 }
237 else if(can_cast_type<pointer_typet>(target.type()))
238 {
239 // A plain `target` becomes `CALL __CPROVER_freeable(target);`
240 code_function_callt code_function_call(
243 .symbol_expr());
244 auto &arguments = code_function_call.arguments();
245 arguments.emplace_back(target);
246
247 dest.add(
248 goto_programt::make_function_call(code_function_call, source_location));
249 }
250 else
251 {
252 // any other type of target is unsupported
254 "unsupported frees clause target " +
255 from_expr_using_mode(ns, language_mode, target),
256 target.source_location());
257 }
258}
259
261 goto_programt &goto_program)
262{
263 std::set<irep_idt> no_body;
264 std::set<irep_idt> missing_function;
265 std::set<irep_idt> recursive_call;
266 std::set<irep_idt> not_enough_arguments;
267
270 goto_program,
271 no_body,
272 recursive_call,
273 missing_function,
274 not_enough_arguments,
276
277 // check that the only no body / missing functions are the cprover builtins
278 for(const auto &id : no_body)
279 {
280 INVARIANT(
282 "no body for '" + id2string(id) + "' when inlining goto program");
283 }
284
285 for(auto it : missing_function)
286 {
287 INVARIANT(
289 "missing function '" + id2string(it) + "' when inlining goto program");
290 }
291
292 INVARIANT(
293 recursive_call.empty(), "recursive calls found when inlining goto program");
294
295 INVARIANT(
296 not_enough_arguments.empty(),
297 "not enough arguments when inlining goto program");
298}
API to expression classes that are internal to the C frontend.
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
Operator to return the address of an object.
Class that allows to clean expressions of side effects and to generate havoc_slice expressions.
Definition utils.h:37
std::list< irep_idt > clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
Definition utils.h:47
goto_instruction_codet representation of a function call statement.
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition c_expr.h:233
const exprt::operandst & targets() const
Definition c_expr.h:277
const exprt & condition() const
Definition c_expr.h:267
void encode_freeable_target_group(const irep_idt &language_mode, const conditional_target_group_exprt &group, goto_programt &dest)
Generates GOTO instructions to build the representation of the given conditional target group.
void encode_assignable_target(const irep_idt &language_mode, const exprt &target, goto_programt &dest)
Generates GOTO instructions to build the representation of the given assignable target.
void encode_assignable_target_group(const irep_idt &language_mode, const conditional_target_group_exprt &group, goto_programt &dest)
Generates GOTO instructions to build the representation of the given conditional target group.
void gen_spec_assigns_instructions(const irep_idt &language_mode, const exprt::operandst &assigns_clause, goto_programt &dest)
Generates instructions encoding the assigns_clause targets and adds them to dest.
void encode_freeable_target(const irep_idt &language_mode, const exprt &target, goto_programt &dest)
Generates GOTO instructions to build the representation of the given freeable target.
void gen_spec_frees_instructions(const irep_idt &language_mode, const exprt::operandst &frees_clause, goto_programt &dest)
Generates instructions encoding the frees_clause targets and adds them to dest.
void inline_and_check_warnings(goto_programt &goto_program)
Inlines all calls in the given program and checks that the only missing functions or functions withou...
dfcc_contract_clauses_codegent(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library)
Class interface to library types and functions defined in cprover_contracts.c.
bool is_front_end_builtin(const irep_idt &function_id) const
Returns true iff the given function_id is one of __CPROVER_assignable, __CPROVER_object_whole,...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:231
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
A generic container class for the GOTO intermediate representation of one function.
void update()
Update all indices.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Thrown when we can't handle something in an input source file.
const irep_idt & id() const
Definition irep.h:388
message_handlert & get_message_handler()
Definition message.h:183
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
Expression to hold a symbol (variable)
Definition std_expr.h:131
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
#define CPROVER_PREFIX
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
Destructor Calls.
Translates assigns and frees clauses of a function contract or loop contract into goto programs that ...
Dynamic frame condition checking library loading.
Dynamic frame condition checking utility functions.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition expr_util.cpp:24
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
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_expr_using_mode(const namespacet &ns, const irep_idt &mode, const exprt &expr)
Formats an expression using the given namespace, using the given mode to retrieve the language printe...
API to expression classes for 'mathematical' expressions.
API to expression classes for Pointers.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition std_code.h:1739
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
Definition std_code.h:1730
API to expression classes.
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:256
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static void inline_program(goto_modelt &goto_model, goto_programt &goto_program, std::set< irep_idt > &no_body, std::set< irep_idt > &recursive_call, std::set< irep_idt > &missing_function, std::set< irep_idt > &not_enough_arguments, message_handlert &message_handler)
Inlines the given program, and returns function symbols that caused warnings.
bool is_loop_free(const goto_programt &goto_program, const namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
Definition utils.cpp:271