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>
26
27#include "dfcc_library.h"
28#include "dfcc_utils.h"
29
31 goto_modelt &goto_model,
32 message_handlert &message_handler,
33 dfcc_libraryt &library)
34 : goto_model(goto_model),
35 message_handler(message_handler),
36 log(message_handler),
37 library(library),
38 ns(goto_model.symbol_table)
39{
40}
41
43 const irep_idt &language_mode,
44 const exprt::operandst &assigns_clause,
45 goto_programt &dest)
46{
47 for(const auto &expr : assigns_clause)
48 {
49 if(
50 auto target_group =
52 {
53 encode_assignable_target_group(language_mode, *target_group, dest);
54 }
55 else
56 {
57 encode_assignable_target(language_mode, expr, dest);
58 }
59 }
60
61 // inline resulting program and check for loops
63 dest.update();
65 is_loop_free(dest, ns, log),
66 "loops in assigns clause specification functions must be unwound before "
67 "contracts instrumentation");
68}
69
71 const irep_idt &language_mode,
72 const exprt::operandst &frees_clause,
73 goto_programt &dest)
74{
75 for(const auto &expr : frees_clause)
76 {
77 if(
78 auto target_group =
80 {
81 encode_freeable_target_group(language_mode, *target_group, dest);
82 }
83 else
84 {
85 encode_freeable_target(language_mode, expr, dest);
86 }
87 }
88
89 // inline resulting program and check for loops
92 is_loop_free(dest, ns, log),
93 "loops in assigns clause specification functions must be unwound before "
94 "contracts instrumentation");
95}
96
98 const irep_idt &language_mode,
100 goto_programt &dest)
101{
102 const source_locationt &source_location = group.source_location();
103
104 // clean up side effects from the condition expression if needed
106 exprt condition(group.condition());
107 if(has_subexpr(condition, ID_side_effect))
108 cleaner.clean(condition, dest, language_mode);
109
110 // Jump target if condition is false
111 auto goto_instruction = dest.add(
112 goto_programt::make_incomplete_goto(not_exprt{condition}, source_location));
113
114 for(const auto &target : group.targets())
115 encode_assignable_target(language_mode, target, dest);
116
117 auto label_instruction = dest.add(goto_programt::make_skip(source_location));
118 goto_instruction->complete_goto(label_instruction);
119}
120
122 const irep_idt &language_mode,
123 const exprt &target,
124 goto_programt &dest)
125{
126 const source_locationt &source_location = target.source_location();
127
129 {
130 // A function call target `foo(params)` becomes `CALL foo(params);`
131 const auto &funcall = to_side_effect_expr_function_call(target);
132 code_function_callt code_function_call(to_symbol_expr(funcall.function()));
133 auto &arguments = code_function_call.arguments();
134 for(auto &arg : funcall.arguments())
135 arguments.emplace_back(arg);
136 dest.add(
137 goto_programt::make_function_call(code_function_call, source_location));
138 }
139 else if(is_assignable(target))
140 {
141 // An lvalue `target` becomes
142 //` CALL __CPROVER_assignable(&target, sizeof(target), is_ptr_to_ptr);`
143 const auto &size =
145
146 if(!size.has_value())
147 {
149 "no definite size for lvalue assigns clause target " +
150 from_expr_using_mode(ns, language_mode, target),
151 target.source_location()};
152 }
153 // we have to build the symbol manually because it might not
154 // be present in the symbol table if the user program does not already
155 // use it.
156 code_function_callt code_function_call(
157 symbol_exprt(CPROVER_PREFIX "assignable", empty_typet()));
158 auto &arguments = code_function_call.arguments();
159
160 // ptr
161 arguments.emplace_back(typecast_exprt::conditional_cast(
163
164 // size
165 arguments.emplace_back(size.value());
166
167 // is_ptr_to_ptr
168 arguments.emplace_back(make_boolean_expr(target.type().id() == ID_pointer));
169
170 dest.add(
171 goto_programt::make_function_call(code_function_call, source_location));
172 }
173 else
174 {
175 // any other type of target is unsupported
177 "unsupported assigns clause target " +
178 from_expr_using_mode(ns, language_mode, target),
179 target.source_location());
180 }
181}
182
184 const irep_idt &language_mode,
186 goto_programt &dest)
187{
188 const source_locationt &source_location = group.source_location();
189
190 // clean up side effects from the condition expression if needed
192 exprt condition(group.condition());
193 if(has_subexpr(condition, ID_side_effect))
194 cleaner.clean(condition, dest, language_mode);
195
196 // Jump target if condition is false
197 auto goto_instruction = dest.add(
198 goto_programt::make_incomplete_goto(not_exprt{condition}, source_location));
199
200 for(const auto &target : group.targets())
201 encode_freeable_target(language_mode, target, dest);
202
203 auto label_instruction = dest.add(goto_programt::make_skip(source_location));
204 goto_instruction->complete_goto(label_instruction);
205}
206
208 const irep_idt &language_mode,
209 const exprt &target,
210 goto_programt &dest)
211{
212 const source_locationt &source_location = target.source_location();
213
215 {
216 const auto &funcall = to_side_effect_expr_function_call(target);
217 if(can_cast_expr<symbol_exprt>(funcall.function()))
218 {
219 // for calls to user-defined functions a call expression `foo(params)`
220 // becomes an instruction `CALL foo(params);`
221 code_function_callt code_function_call(
222 to_symbol_expr(funcall.function()));
223 auto &arguments = code_function_call.arguments();
224 for(auto &arg : funcall.arguments())
225 arguments.emplace_back(arg);
226 dest.add(
227 goto_programt::make_function_call(code_function_call, source_location));
228 }
229 }
230 else if(can_cast_type<pointer_typet>(target.type()))
231 {
232 // A plain `target` becomes `CALL __CPROVER_freeable(target);`
233 code_function_callt code_function_call(
236 .symbol_expr());
237 auto &arguments = code_function_call.arguments();
238 arguments.emplace_back(target);
239
240 dest.add(
241 goto_programt::make_function_call(code_function_call, source_location));
242 }
243 else
244 {
245 // any other type of target is unsupported
247 "unsupported frees clause target " +
248 from_expr_using_mode(ns, language_mode, target),
249 target.source_location());
250 }
251}
252
254 goto_programt &goto_program)
255{
256 std::set<irep_idt> no_body;
257 std::set<irep_idt> missing_function;
258 std::set<irep_idt> recursive_call;
259 std::set<irep_idt> not_enough_arguments;
260
263 goto_program,
264 no_body,
265 recursive_call,
266 missing_function,
267 not_enough_arguments,
269
270 // check that the only no body / missing functions are the cprover builtins
271 for(const auto &id : no_body)
272 {
273 INVARIANT(
275 "no body for '" + id2string(id) + "' when inlining goto program");
276 }
277
278 for(auto it : missing_function)
279 {
280 INVARIANT(
282 "missing function '" + id2string(it) + "' when inlining goto program");
283 }
284
285 INVARIANT(
286 recursive_call.empty(), "recursive calls found when inlining goto program");
287
288 INVARIANT(
289 not_enough_arguments.empty(),
290 "not enough arguments when inlining goto program");
291}
API to expression classes that are internal to the C frontend.
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
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:35
void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
Definition utils.h:44
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:232
const exprt::operandst & targets() const
Definition c_expr.h:276
const exprt & condition() const
Definition c_expr.h:266
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:39
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:223
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:396
message_handlert & get_message_handler()
Definition message.h:184
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Boolean negation.
Definition std_expr.h:2278
Expression to hold a symbol (variable)
Definition std_expr.h:113
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:2025
#define CPROVER_PREFIX
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
Deprecated expression utility functions.
Fresh auxiliary symbol creation.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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.
optionalt< 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:206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
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, namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
Definition utils.cpp:268