Skip to content

Commit 6c5b2a6

Browse files
author
Remi Delmas
committed
CONTRACTS: new context tracking flags in write set
Enable checking for the presence of dynamic allocations or deallocations in loop bodies and transitively in the functions called from loop bodies. - Adds `allow_allocate` and `allow_deallocate` flags in the write set struct - Modify `add_allocated` to fail an assertion when called on a write set with `allow_allocate` set to false. - Modify `check_deallocate` to return false when called on a write set with `allow_deallocate` set to false. - Don't treat replacement mode specially anymore, always store freeable targets in both the object map (for lookups) and in the append list (for inclusion checks).
1 parent 8427b1f commit 6c5b2a6

File tree

5 files changed

+69
-81
lines changed

5 files changed

+69
-81
lines changed

src/ansi-c/library/cprover_contracts.c

+59-73
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ typedef struct
7272
/// \brief Set of freeable pointers derived from the contract (indexed mode)
7373
__CPROVER_contracts_obj_set_t contract_frees;
7474
/// \brief Set of freeable pointers derived from the contract (append mode)
75-
__CPROVER_contracts_obj_set_t contract_frees_replacement;
75+
__CPROVER_contracts_obj_set_t contract_frees_append;
7676
/// \brief Set of objects allocated by the function under analysis
7777
/// (indexed mode)
7878
__CPROVER_contracts_obj_set_t allocated;
@@ -83,12 +83,9 @@ typedef struct
8383
/// (indexed mode)
8484
__CPROVER_contracts_obj_set_ptr_t linked_is_fresh;
8585
/// \brief Object set recording the is_fresh allocations in post conditions
86-
/// (replacement mode only)
8786
__CPROVER_contracts_obj_set_ptr_t linked_allocated;
8887
/// \brief Object set recording the deallocations (used by was_freed)
8988
__CPROVER_contracts_obj_set_ptr_t linked_deallocated;
90-
/// \brief True iff this write set is used for contract replacement
91-
__CPROVER_bool replacement;
9289
/// \brief True iff the write set checks requires clauses in an assumption ctx
9390
__CPROVER_bool assume_requires_ctx;
9491
/// \brief True iff the write set checks requires clauses in an assertion ctx
@@ -97,6 +94,10 @@ typedef struct
9794
__CPROVER_bool assume_ensures_ctx;
9895
/// \brief True iff this write set checks ensures clauses in an assertion ctx
9996
__CPROVER_bool assert_ensures_ctx;
97+
/// \brief True iff dynamic allocation is allowed (default: true)
98+
__CPROVER_bool allow_allocate;
99+
/// \brief True iff dynamic deallocation is allowed (default: true)
100+
__CPROVER_bool allow_deallocate;
100101
} __CPROVER_contracts_write_set_t;
101102

102103
/// \brief Type of pointers to \ref __CPROVER_contracts_write_set_t.
@@ -388,7 +389,6 @@ __CPROVER_HIDE:;
388389
/// \param[inout] set Pointer to the object to initialise
389390
/// \param[in] contract_assigns_size Max size of the assigns clause
390391
/// \param[in] contract_frees_size Max size of the frees clause
391-
/// \param[in] replacement True iff this write set is used to replace a contract
392392
/// \param[in] assume_requires_ctx True iff this write set is used to check side
393393
/// effects in a requires clause in contract checking mode
394394
/// \param[in] assert_requires_ctx True iff this write set is used to check side
@@ -397,15 +397,20 @@ __CPROVER_HIDE:;
397397
/// side effects in an ensures clause in contract replacement mode
398398
/// \param[in] assert_ensures_ctx True iff this write set is used to check for
399399
/// side effects in an ensures clause in contract checking mode
400+
/// \param[in] allow_allocate True iff the context gobally allows dynamic
401+
/// allocation.
402+
/// \param[in] allow_deallocate True iff the context gobally allows dynamic
403+
/// deallocation.
400404
void __CPROVER_contracts_write_set_create(
401405
__CPROVER_contracts_write_set_ptr_t set,
402406
__CPROVER_size_t contract_assigns_size,
403407
__CPROVER_size_t contract_frees_size,
404-
__CPROVER_bool replacement,
405408
__CPROVER_bool assume_requires_ctx,
406409
__CPROVER_bool assert_requires_ctx,
407410
__CPROVER_bool assume_ensures_ctx,
408-
__CPROVER_bool assert_ensures_ctx)
411+
__CPROVER_bool assert_ensures_ctx,
412+
__CPROVER_bool allow_allocate,
413+
__CPROVER_bool allow_deallocate)
409414
{
410415
__CPROVER_HIDE:;
411416
#ifdef DFCC_DEBUG
@@ -417,16 +422,8 @@ __CPROVER_HIDE:;
417422
&(set->contract_assigns), contract_assigns_size);
418423
__CPROVER_contracts_obj_set_create_indexed_by_object_id(
419424
&(set->contract_frees));
420-
set->replacement = replacement;
421-
if(replacement)
422-
{
423-
__CPROVER_contracts_obj_set_create_append(
424-
&(set->contract_frees_replacement), contract_frees_size);
425-
}
426-
else
427-
{
428-
set->contract_frees_replacement.elems = 0;
429-
}
425+
__CPROVER_contracts_obj_set_create_append(
426+
&(set->contract_frees_append), contract_frees_size);
430427
__CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->allocated));
431428
__CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->deallocated));
432429
set->linked_is_fresh = 0;
@@ -436,6 +433,8 @@ __CPROVER_HIDE:;
436433
set->assert_requires_ctx = assert_requires_ctx;
437434
set->assume_ensures_ctx = assume_ensures_ctx;
438435
set->assert_ensures_ctx = assert_ensures_ctx;
436+
set->allow_allocate = allow_allocate;
437+
set->allow_deallocate = allow_deallocate;
439438
}
440439

441440
/// \brief Releases resources used by \p set.
@@ -454,20 +453,16 @@ __CPROVER_HIDE:;
454453
__CPROVER_rw_ok(&(set->contract_frees.elems), 0),
455454
"contract_frees writable");
456455
__CPROVER_assert(
457-
(set->replacement == 0) ||
458-
__CPROVER_rw_ok(&(set->contract_frees_replacement.elems), 0),
459-
"contract_frees_replacement writable");
456+
__CPROVER_rw_ok(&(set->contract_frees_append.elems), 0),
457+
"contract_frees_append writable");
460458
__CPROVER_assert(
461459
__CPROVER_rw_ok(&(set->allocated.elems), 0), "allocated writable");
462460
__CPROVER_assert(
463461
__CPROVER_rw_ok(&(set->deallocated.elems), 0), "deallocated writable");
464462
#endif
465463
__CPROVER_deallocate(set->contract_assigns.elems);
466464
__CPROVER_deallocate(set->contract_frees.elems);
467-
if(set->replacement != 0)
468-
{
469-
__CPROVER_deallocate(set->contract_frees_replacement.elems);
470-
}
465+
__CPROVER_deallocate(set->contract_frees_append.elems);
471466
__CPROVER_deallocate(set->allocated.elems);
472467
__CPROVER_deallocate(set->deallocated.elems);
473468
// do not free set->linked_is_fresh->elems or set->deallocated_linked->elems
@@ -585,29 +580,44 @@ __CPROVER_HIDE:;
585580

586581
// append pointer if available
587582
#ifdef DFCC_DEBUG
588-
if(set->replacement)
589-
__CPROVER_contracts_obj_set_append(&(set->contract_frees_replacement), ptr);
583+
__CPROVER_contracts_obj_set_append(&(set->contract_frees_append), ptr);
590584
#else
591-
if(set->replacement)
592-
{
593-
set->contract_frees_replacement.nof_elems =
594-
set->contract_frees_replacement.watermark;
595-
set->contract_frees_replacement
596-
.elems[set->contract_frees_replacement.watermark] = ptr;
597-
set->contract_frees_replacement.watermark += 1;
598-
set->contract_frees_replacement.is_empty = 0;
599-
}
585+
set->contract_frees_append.nof_elems = set->contract_frees_append.watermark;
586+
set->contract_frees_append.elems[set->contract_frees_append.watermark] = ptr;
587+
set->contract_frees_append.watermark += 1;
588+
set->contract_frees_append.is_empty = 0;
600589
#endif
601590
}
602591

603-
/// \brief Adds the pointer \p ptr to \p set->allocated.
592+
/// \brief Adds the dynamically allocated pointer \p ptr to \p set->allocated.
604593
/// \param[inout] set The set to update
605-
/// \param[in] ptr Pointer to an object declared using a `DECL x` or
606-
/// `x = __CPROVER_allocate(...)` GOTO instruction.
594+
/// \param[in] ptr Pointer to a dynamic object `x = __CPROVER_allocate(...)`.
607595
void __CPROVER_contracts_write_set_add_allocated(
608596
__CPROVER_contracts_write_set_ptr_t set,
609597
void *ptr)
610598
{
599+
__CPROVER_HIDE:;
600+
__CPROVER_assert(set->allow_allocate, "dynamic allocation is allowed");
601+
#if DFCC_DEBUG
602+
// call inlined below
603+
__CPROVER_contracts_obj_set_add(&(set->allocated), ptr);
604+
#else
605+
__CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
606+
set->allocated.nof_elems = (set->allocated.elems[object_id] != 0)
607+
? set->allocated.nof_elems
608+
: set->allocated.nof_elems + 1;
609+
set->allocated.elems[object_id] = ptr;
610+
set->allocated.is_empty = 0;
611+
#endif
612+
}
613+
614+
/// \brief Adds the pointer \p ptr to \p set->allocated.
615+
/// \param[inout] set The set to update
616+
/// \param[in] ptr Pointer to an object declared using `DECL x`.
617+
void __CPROVER_contracts_write_set_add_decl(
618+
__CPROVER_contracts_write_set_ptr_t set,
619+
void *ptr)
620+
{
611621
__CPROVER_HIDE:;
612622
#if DFCC_DEBUG
613623
// call inlined below
@@ -659,10 +669,6 @@ void __CPROVER_contracts_write_set_record_deallocated(
659669
void *ptr)
660670
{
661671
__CPROVER_HIDE:;
662-
#ifdef DFCC_DEBUG
663-
__CPROVER_assert(set->replacement == 0, "!replacement");
664-
#endif
665-
666672
#if DFCC_DEBUG
667673
// we record the deallocation to be able to evaluate was_freed post conditions
668674
__CPROVER_contracts_obj_set_add(&(set->deallocated), ptr);
@@ -735,7 +741,6 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_assignment(
735741
// manually inlined below
736742
{
737743
__CPROVER_HIDE:;
738-
__CPROVER_assert(set->replacement == 0, "!replacement");
739744
__CPROVER_assert(
740745
((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
741746
"ptr NULL or writable up to size");
@@ -904,16 +909,13 @@ __CPROVER_HIDE:;
904909
/// \param[in] set Write set to check the deallocation against
905910
/// \param[in] ptr Deallocated pointer to check set to check the deallocation
906911
/// against
907-
/// \return True iff \p ptr is contained in \p set->contract_frees or
908-
/// \p set->allocated.
912+
/// \return True iff deallocation is allowed and \p ptr is contained in
913+
/// \p set->contract_frees or \p set->allocated.
909914
__CPROVER_bool __CPROVER_contracts_write_set_check_deallocate(
910915
__CPROVER_contracts_write_set_ptr_t set,
911916
void *ptr)
912917
{
913918
__CPROVER_HIDE:;
914-
#ifdef DFCC_DEBUG
915-
__CPROVER_assert(set->replacement == 0, "!replacement");
916-
#endif
917919
__CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
918920

919921
#ifdef DFCC_DEBUG
@@ -924,16 +926,15 @@ __CPROVER_HIDE:;
924926
set->allocated.indexed_by_object_id,
925927
"set->allocated is indexed by object id");
926928
#endif
927-
return (ptr == 0) | (set->contract_frees.elems[object_id] == ptr) |
928-
(set->allocated.elems[object_id] == ptr);
929+
return (set->allow_deallocate) &
930+
((ptr == 0) | (set->contract_frees.elems[object_id] == ptr) |
931+
(set->allocated.elems[object_id] == ptr));
929932
}
930933

931934
/// \brief Checks the inclusion of the \p candidate->contract_assigns elements
932935
/// in \p reference->contract_assigns or \p reference->allocated.
933936
///
934-
/// \pre \p reference must not be in replacement mode.
935-
/// \pre \p candidate must be in replacement mode and \p candidate->allocated
936-
/// must be empty.
937+
/// \pre \p candidate->allocated must be empty.
937938
///
938939
/// \param[in] reference Reference write set from a caller
939940
/// \param[in] candidate Candidate write set from a contract being replaced
@@ -944,11 +945,6 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_assigns_clause_inclusion(
944945
__CPROVER_contracts_write_set_ptr_t candidate)
945946
{
946947
__CPROVER_HIDE:;
947-
#ifdef DFCC_DEBUG
948-
__CPROVER_assert(
949-
reference->replacement == 0, "reference set in !replacement");
950-
__CPROVER_assert(candidate->replacement != 0, "candidate set in replacement");
951-
#endif
952948
__CPROVER_bool incl = 1;
953949
__CPROVER_contracts_car_t *current = candidate->contract_assigns.elems;
954950
__CPROVER_size_t idx = candidate->contract_assigns.max_elems;
@@ -969,9 +965,7 @@ __CPROVER_HIDE:;
969965
/// \brief Checks the inclusion of the \p candidate->contract_frees elements
970966
/// in \p reference->contract_frees or \p reference->allocated.
971967
///
972-
/// \pre \p reference must not be in replacement mode.
973-
/// \pre \p candidate must be in replacement mode and \p candidate->allocated
974-
/// must be empty.
968+
/// \pre \p candidate->allocated must be empty.
975969
///
976970
/// \param[in] reference Reference write set from a caller
977971
/// \param[in] candidate Candidate write set from a contract being replaced
@@ -983,9 +977,6 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_frees_clause_inclusion(
983977
{
984978
__CPROVER_HIDE:;
985979
#ifdef DFCC_DEBUG
986-
__CPROVER_assert(
987-
reference->replacement == 0, "reference set in !replacement");
988-
__CPROVER_assert(candidate->replacement != 0, "candidate set in replacement");
989980
__CPROVER_assert(
990981
reference->contract_frees.indexed_by_object_id,
991982
"reference->contract_frees is indexed by object id");
@@ -994,8 +985,8 @@ __CPROVER_HIDE:;
994985
"reference->allocated is indexed by object id");
995986
#endif
996987
__CPROVER_bool all_incl = 1;
997-
void **current = candidate->contract_frees_replacement.elems;
998-
__CPROVER_size_t idx = candidate->contract_frees_replacement.max_elems;
988+
void **current = candidate->contract_frees_append.elems;
989+
__CPROVER_size_t idx = candidate->contract_frees_append.max_elems;
999990

1000991
SET_CHECK_FREES_CLAUSE_INCLUSION_LOOP:
1001992
while(idx != 0)
@@ -1030,13 +1021,8 @@ void __CPROVER_contracts_write_set_deallocate_freeable(
10301021
__CPROVER_contracts_write_set_ptr_t target)
10311022
{
10321023
__CPROVER_HIDE:;
1033-
#ifdef DFCC_DEBUG
1034-
__CPROVER_assert(set->replacement == 1, "set is in replacement");
1035-
__CPROVER_assert(
1036-
(target == 0) | (target->replacement == 0), "target is in !replacement");
1037-
#endif
1038-
void **current = set->contract_frees_replacement.elems;
1039-
__CPROVER_size_t idx = set->contract_frees_replacement.max_elems;
1024+
void **current = set->contract_frees_append.elems;
1025+
__CPROVER_size_t idx = set->contract_frees_append.max_elems;
10401026
SET_DEALLOCATE_FREEABLE_LOOP:
10411027
while(idx != 0)
10421028
{

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp

+5-6
Original file line numberDiff line numberDiff line change
@@ -380,8 +380,7 @@ void dfcc_instrumentt::instrument_function_body(
380380
for(const auto &local_static : local_statics)
381381
{
382382
// automatically add local statics to the write set
383-
insert_add_allocated_call(
384-
function_id, write_set, local_static, begin, body);
383+
insert_add_decl_call(function_id, write_set, local_static, begin, body);
385384

386385
// automatically remove local statics to the write set
387386
insert_record_dead_call(function_id, write_set, local_static, end, body);
@@ -510,7 +509,7 @@ bool dfcc_instrumentt::must_track_decl_or_dead(
510509
return retval;
511510
}
512511

513-
void dfcc_instrumentt::insert_add_allocated_call(
512+
void dfcc_instrumentt::insert_add_decl_call(
514513
const irep_idt &function_id,
515514
const exprt &write_set,
516515
const symbol_exprt &symbol_expr,
@@ -523,7 +522,7 @@ void dfcc_instrumentt::insert_add_allocated_call(
523522

524523
payload.add(goto_programt::make_function_call(
525524
code_function_callt{
526-
library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_ALLOCATED].symbol_expr(),
525+
library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_DECL].symbol_expr(),
527526
{write_set, address_of_exprt(symbol_expr)}},
528527
target->source_location()));
529528

@@ -538,7 +537,7 @@ void dfcc_instrumentt::insert_add_allocated_call(
538537
/// ```c
539538
/// DECL x;
540539
/// ----
541-
/// insert_add_allocated_call(...);
540+
/// insert_add_decl_call(...);
542541
/// ```
543542
void dfcc_instrumentt::instrument_decl(
544543
const irep_idt &function_id,
@@ -552,7 +551,7 @@ void dfcc_instrumentt::instrument_decl(
552551

553552
const auto &decl_symbol = target->decl_symbol();
554553
target++;
555-
insert_add_allocated_call(
554+
insert_add_decl_call(
556555
function_id, write_set, decl_symbol, target, goto_program);
557556
target--;
558557
}

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -175,15 +175,15 @@ class dfcc_instrumentt
175175
/// forward.
176176
/// ```
177177
/// IF !write_set GOTO skip_target;
178-
/// CALL __CPROVER_contracts_write_set_add_allocated(write_set, &x);
178+
/// CALL __CPROVER_contracts_write_set_add_decl(write_set, &x);
179179
/// skip_target: SKIP;
180180
/// ```
181181
/// \param function_id Name of the function in which the instructions is added
182182
/// \param write_set The write set to the symbol expr to
183183
/// \param symbol_expr The symbol to add to the write set
184184
/// \param target The instruction pointer to insert at
185185
/// \param goto_program the goto_program being instrumented
186-
void insert_add_allocated_call(
186+
void insert_add_decl_call(
187187
const irep_idt &function_id,
188188
const exprt &write_set,
189189
const symbol_exprt &symbol_expr,

src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,7 @@ const std::map<dfcc_funt, irep_idt> create_dfcc_fun_to_name()
9191
CONTRACTS_PREFIX "write_set_add_freeable"},
9292
{dfcc_funt::WRITE_SET_ADD_ALLOCATED,
9393
CONTRACTS_PREFIX "write_set_add_allocated"},
94+
{dfcc_funt::WRITE_SET_ADD_DECL, CONTRACTS_PREFIX "write_set_add_decl"},
9495
{dfcc_funt::WRITE_SET_RECORD_DEAD,
9596
CONTRACTS_PREFIX "write_set_record_dead"},
9697
{dfcc_funt::WRITE_SET_RECORD_DEALLOCATED,

src/goto-instrument/contracts/dynamic-frames/dfcc_library.h

+2
Original file line numberDiff line numberDiff line change
@@ -87,6 +87,8 @@ enum class dfcc_funt
8787
WRITE_SET_ADD_FREEABLE,
8888
/// \see __CPROVER_contracts_write_set_add_allocated
8989
WRITE_SET_ADD_ALLOCATED,
90+
/// \see __CPROVER_contracts_write_set_add_decl
91+
WRITE_SET_ADD_DECL,
9092
/// \see __CPROVER_contracts_write_set_record_dead
9193
WRITE_SET_RECORD_DEAD,
9294
/// \see __CPROVER_contracts_write_set_record_deallocated

0 commit comments

Comments
 (0)