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,
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,
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);
133 auto &arguments = code_function_call.arguments();
134 for(auto &arg : funcall.arguments())
135 arguments.emplace_back(arg);
136 dest.add(
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.
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(
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);
218 {
219 // for calls to user-defined functions a call expression `foo(params)`
220 // becomes an instruction `CALL foo(params);`
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(
228 }
229 }
230 else if(can_cast_type<pointer_typet>(target.type()))
231 {
232 // A plain `target` becomes `CALL __CPROVER_freeable(target);`
236 .symbol_expr());
237 auto &arguments = code_function_call.arguments();
238 arguments.emplace_back(target);
239
240 dest.add(
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,
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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
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
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.
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.
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
API to expression classes.
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