Skip to content

Commit 142db0b

Browse files
Merge pull request #6821 from remi-delmas-3000/contracts-obeys-clause
CONTRACTS: adding requires and ensures clauses for function pointers
2 parents e3dd810 + 63cd722 commit 142db0b

File tree

18 files changed

+551
-21
lines changed

18 files changed

+551
-21
lines changed
Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
#include <stdbool.h>
2+
#include <stdlib.h>
3+
4+
bool nondet_bool();
5+
6+
// type of functions that manipulate arrays
7+
typedef void (*arr_fun_t)(char *arr, size_t size);
8+
9+
// A contract for the arr_fun_t type
10+
// requires a fresh array and positive size
11+
// resets the first element to zero
12+
void contract(char *arr, size_t size)
13+
// clang-format off
14+
__CPROVER_requires((size > 0 && __CPROVER_is_fresh(arr, size)))
15+
__CPROVER_assigns(arr[0])
16+
__CPROVER_ensures(arr[0] == 0)
17+
// clang-format on
18+
{
19+
}
20+
21+
arr_fun_t bar()
22+
// clang-format off
23+
__CPROVER_ensures_contract(__CPROVER_return_value, contract)
24+
// clang-format on
25+
{
26+
return contract;
27+
}
28+
29+
// Testing pre-conditions constructs
30+
// Takes a function pointer as input, uses it if its preconditions are met
31+
int foo(char *arr, size_t size, arr_fun_t fun)
32+
// clang-format off
33+
__CPROVER_requires_contract(fun, contract)
34+
__CPROVER_requires(arr == NULL || __CPROVER_is_fresh(arr, size))
35+
__CPROVER_assigns(arr && size > 0: arr[0])
36+
__CPROVER_ensures(arr && size > 0 ==> (arr[0] == 0 && __CPROVER_return_value == 0))
37+
__CPROVER_ensures(!(arr && size > 0) ==> __CPROVER_return_value == -1)
38+
// clang-format on
39+
{
40+
if(nondet_bool())
41+
fun = bar(); // non-deterministically get a function pointer from bar()
42+
43+
int retval = -1;
44+
if(arr && size > 0)
45+
{
46+
// calls the function pointer to do update the array
47+
fun(arr, size);
48+
retval = 0;
49+
}
50+
return retval;
51+
}
52+
53+
void main()
54+
{
55+
size_t size;
56+
char *arr;
57+
arr_fun_t fun;
58+
// The precondition that `fun` obeys `contract`
59+
// and that bar returns a function that obeys `contract`
60+
// are used establish the post-conditions of `foo`
61+
foo(arr, size, fun);
62+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--enforce-contract foo --restrict-function-pointer foo.function_pointer_call.1/contract --replace-call-with-contract contract --replace-call-with-contract bar
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
This test checks that we can require that a function pointer satisfies some named
10+
contract when verifying another function, and successfully replace a call to this
11+
function pointer by the contract.
Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
// type of functions that manipulate arrays
5+
typedef void (*arr_fun_t)(char *arr, size_t size);
6+
7+
// A contract for the arr_fun_t type
8+
void contract(char *arr, size_t size)
9+
// clang-format off
10+
__CPROVER_requires((size > 0 && __CPROVER_is_fresh(arr, size)))
11+
__CPROVER_assigns(arr[0])
12+
__CPROVER_ensures(arr[0] == 0)
13+
// clang-format on
14+
{
15+
}
16+
17+
arr_fun_t foo(arr_fun_t infun, arr_fun_t *outfun)
18+
// clang-format off
19+
__CPROVER_requires_contract(infun, contract)
20+
__CPROVER_ensures_contract(*outfun, contract)
21+
__CPROVER_ensures_contract(__CPROVER_return_value, contract)
22+
// clang-format on
23+
{
24+
*outfun = contract;
25+
return infun;
26+
}
27+
28+
void main()
29+
{
30+
// establish pre-conditions before replacement
31+
arr_fun_t infun = contract;
32+
33+
arr_fun_t outfun1 = NULL;
34+
arr_fun_t outfun2 = foo(infun, &outfun1);
35+
36+
// checking post-conditions after replacement
37+
assert(outfun1 == contract);
38+
assert(outfun2 == contract);
39+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--replace-call-with-contract foo
4+
^\[precondition.\d+] Assert function pointer 'infun' obeys contract 'contract': SUCCESS$
5+
^\[main.assertion.\d+].* assertion outfun1 == contract: SUCCESS$
6+
^\[main.assertion.\d+].* assertion outfun2 == contract: SUCCESS$
7+
^EXIT=0$
8+
^SIGNAL=0$
9+
^VERIFICATION SUCCESSFUL$
10+
--
11+
--
12+
This test checks that, when replacing a call by its contract,
13+
requires_contract clauses are translated to equality checks
14+
and that ensures_contract are translated to assignments.

src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -259,6 +259,12 @@ void ansi_c_convert_typet::read_rec(const typet &type)
259259
static_cast<const exprt &>(static_cast<const irept &>(type));
260260
requires.push_back(to_unary_expr(as_expr).op());
261261
}
262+
else if(type.id() == ID_C_spec_requires_contract)
263+
{
264+
const exprt &as_expr =
265+
static_cast<const exprt &>(static_cast<const irept &>(type));
266+
requires_contract.push_back(to_unary_expr(as_expr).op());
267+
}
262268
else if(type.id() == ID_C_spec_assigns)
263269
{
264270
const exprt &as_expr =
@@ -273,6 +279,12 @@ void ansi_c_convert_typet::read_rec(const typet &type)
273279
static_cast<const exprt &>(static_cast<const irept &>(type));
274280
ensures.push_back(to_unary_expr(as_expr).op());
275281
}
282+
else if(type.id() == ID_C_spec_ensures_contract)
283+
{
284+
const exprt &as_expr =
285+
static_cast<const exprt &>(static_cast<const irept &>(type));
286+
ensures_contract.push_back(to_unary_expr(as_expr).op());
287+
}
276288
else
277289
other.push_back(type);
278290
}
@@ -322,12 +334,20 @@ void ansi_c_convert_typet::write(typet &type)
322334
if(!requires.empty())
323335
to_code_with_contract_type(type).requires() = std::move(requires);
324336

337+
if(!requires_contract.empty())
338+
to_code_with_contract_type(type).requires_contract() =
339+
std::move(requires_contract);
340+
325341
if(!assigns.empty())
326342
to_code_with_contract_type(type).assigns() = std::move(assigns);
327343

328344
if(!ensures.empty())
329345
to_code_with_contract_type(type).ensures() = std::move(ensures);
330346

347+
if(!ensures_contract.empty())
348+
to_code_with_contract_type(type).ensures_contract() =
349+
std::move(ensures_contract);
350+
331351
if(constructor || destructor)
332352
{
333353
if(constructor && destructor)

src/ansi-c/ansi_c_convert_type.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,8 @@ class ansi_c_convert_typet:public messaget
4747
bool constructor, destructor;
4848

4949
// contracts
50-
exprt::operandst assigns, ensures, requires;
50+
exprt::operandst assigns, ensures, requires, ensures_contract,
51+
requires_contract;
5152

5253
// storage spec
5354
c_storage_spect c_storage_spec;

src/ansi-c/c_expr.h

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -320,4 +320,96 @@ to_conditional_target_group_expr(exprt &expr)
320320
return ret;
321321
}
322322

323+
/// \brief A class for expressions representing a
324+
/// `requires_contract(fptr, contract)` clause
325+
/// or an `ensures_contract(fptr, contract)` clause
326+
/// in a function contract.
327+
class function_pointer_obeys_contract_exprt : public exprt
328+
{
329+
public:
330+
explicit function_pointer_obeys_contract_exprt(
331+
exprt _function_pointer,
332+
exprt _contract)
333+
: exprt(ID_function_pointer_obeys_contract, empty_typet{})
334+
{
335+
add_to_operands(std::move(_function_pointer));
336+
add_to_operands(std::move(_contract));
337+
}
338+
339+
static void check(
340+
const exprt &expr,
341+
const validation_modet vm = validation_modet::INVARIANT)
342+
{
343+
DATA_CHECK(
344+
vm,
345+
expr.operands().size() == 2,
346+
"function pointer obeys contract expression must have two operands");
347+
}
348+
349+
static void validate(
350+
const exprt &expr,
351+
const namespacet &,
352+
const validation_modet vm = validation_modet::INVARIANT)
353+
{
354+
check(expr, vm);
355+
}
356+
357+
const exprt &function_pointer() const
358+
{
359+
return op0();
360+
}
361+
362+
exprt &function_pointer()
363+
{
364+
return op0();
365+
}
366+
367+
const exprt &contract() const
368+
{
369+
return op1();
370+
}
371+
372+
exprt &contract()
373+
{
374+
return op1();
375+
}
376+
};
377+
378+
inline void validate_expr(const function_pointer_obeys_contract_exprt &value)
379+
{
380+
function_pointer_obeys_contract_exprt::check(value);
381+
}
382+
383+
template <>
384+
inline bool
385+
can_cast_expr<function_pointer_obeys_contract_exprt>(const exprt &base)
386+
{
387+
return base.id() == ID_function_pointer_obeys_contract;
388+
}
389+
390+
/// \brief Cast an exprt to a \ref function_pointer_obeys_contract_exprt
391+
///
392+
/// \a expr must be known to be \ref function_pointer_obeys_contract_exprt
393+
///
394+
/// \param expr: Source expression
395+
/// \return Object of type \ref function_pointer_obeys_contract_exprt
396+
inline const function_pointer_obeys_contract_exprt &
397+
to_function_pointer_obeys_contract_expr(const exprt &expr)
398+
{
399+
PRECONDITION(expr.id() == ID_function_pointer_obeys_contract);
400+
auto &ret = static_cast<const function_pointer_obeys_contract_exprt &>(expr);
401+
validate_expr(ret);
402+
return ret;
403+
}
404+
405+
/// \copydoc to_function_pointer_obeys_contract_expr(const exprt &expr)
406+
inline function_pointer_obeys_contract_exprt &
407+
to_function_pointer_obeys_contract_expr(exprt &expr)
408+
{
409+
PRECONDITION(expr.id() == ID_function_pointer_obeys_contract);
410+
auto &ret = static_cast<function_pointer_obeys_contract_exprt &>(expr);
411+
validate_expr(ret);
412+
return ret;
413+
}
414+
323415
#endif // CPROVER_ANSI_C_C_EXPR_H

src/ansi-c/c_typecheck_base.cpp

Lines changed: 32 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -699,6 +699,15 @@ void c_typecheck_baset::typecheck_declaration(
699699

700700
typecheck_symbol(symbol);
701701

702+
auto check_history_expr = [&](const exprt expr) {
703+
disallow_subexpr_by_id(
704+
expr, ID_old, CPROVER_PREFIX "old is not allowed in preconditions.");
705+
disallow_subexpr_by_id(
706+
expr,
707+
ID_loop_entry,
708+
CPROVER_PREFIX "loop_entry is not allowed in preconditions.");
709+
};
710+
702711
// check the contract, if any
703712
symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
704713
if(new_symbol.type.id() == ID_code)
@@ -708,29 +717,36 @@ void c_typecheck_baset::typecheck_declaration(
708717
// available
709718
auto &code_type = to_code_with_contract_type(new_symbol.type);
710719

720+
for(auto &expr : code_type.requires_contract())
721+
{
722+
typecheck_spec_function_pointer_obeys_contract(expr);
723+
check_history_expr(expr);
724+
}
725+
711726
for(auto &requires : code_type.requires())
712727
{
713728
typecheck_expr(requires);
714729
implicit_typecast_bool(requires);
715-
disallow_subexpr_by_id(
716-
requires,
717-
ID_old,
718-
CPROVER_PREFIX "old is not allowed in preconditions.");
719-
disallow_subexpr_by_id(
720-
requires,
721-
ID_loop_entry,
722-
CPROVER_PREFIX "loop_entry is not allowed in preconditions.");
730+
check_history_expr(requires);
723731
}
724732

725733
typecheck_spec_assigns(code_type.assigns());
726734

727-
if(!as_const(code_type).ensures().empty())
728-
{
729-
const auto &return_type = code_type.return_type();
735+
const auto &return_type = code_type.return_type();
736+
if(return_type.id() != ID_empty)
737+
parameter_map[CPROVER_PREFIX "return_value"] = return_type;
730738

731-
if(return_type.id() != ID_empty)
732-
parameter_map[CPROVER_PREFIX "return_value"] = return_type;
739+
for(auto &expr : code_type.ensures_contract())
740+
{
741+
typecheck_spec_function_pointer_obeys_contract(expr);
742+
disallow_subexpr_by_id(
743+
expr,
744+
ID_loop_entry,
745+
CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
746+
}
733747

748+
if(!as_const(code_type).ensures().empty())
749+
{
734750
for(auto &ensures : code_type.ensures())
735751
{
736752
typecheck_expr(ensures);
@@ -740,10 +756,10 @@ void c_typecheck_baset::typecheck_declaration(
740756
ID_loop_entry,
741757
CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
742758
}
743-
744-
if(return_type.id() != ID_empty)
745-
parameter_map.erase(CPROVER_PREFIX "return_value");
746759
}
760+
761+
if(return_type.id() != ID_empty)
762+
parameter_map.erase(CPROVER_PREFIX "return_value");
747763
}
748764
}
749765
}

src/ansi-c/c_typecheck_base.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -146,6 +146,7 @@ class c_typecheck_baset:
146146
virtual void typecheck_start_thread(codet &code);
147147

148148
// contracts
149+
virtual void typecheck_spec_function_pointer_obeys_contract(exprt &expr);
149150
virtual void typecheck_spec_assigns(exprt::operandst &targets);
150151
virtual void typecheck_spec_assigns_condition(exprt &condition);
151152
virtual void typecheck_spec_assigns_target(exprt &target);

0 commit comments

Comments
 (0)