Skip to content

CONTRACTS: refactor DFCC code for loop contracts #7551

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Feb 22, 2023
Merged

CONTRACTS: refactor DFCC code for loop contracts #7551

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
1ad6ecc
CONTRACTS: new inlining and loop detection methods
Feb 16, 2023
8427b1f
CONTRACTS: rearchitecture code for loop contracts
Feb 16, 2023
6c5b2a6
CONTRACTS: new context tracking flags in write set
Feb 17, 2023
da85771
CONTRACTS: new c++ methods to build calls to cprover_contracts library
Feb 17, 2023
fb35a17
address review comments
Feb 22, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
132 changes: 59 additions & 73 deletions src/ansi-c/library/cprover_contracts.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ typedef struct
/// \brief Set of freeable pointers derived from the contract (indexed mode)
__CPROVER_contracts_obj_set_t contract_frees;
/// \brief Set of freeable pointers derived from the contract (append mode)
__CPROVER_contracts_obj_set_t contract_frees_replacement;
__CPROVER_contracts_obj_set_t contract_frees_append;
/// \brief Set of objects allocated by the function under analysis
/// (indexed mode)
__CPROVER_contracts_obj_set_t allocated;
Expand All @@ -83,12 +83,9 @@ typedef struct
/// (indexed mode)
__CPROVER_contracts_obj_set_ptr_t linked_is_fresh;
/// \brief Object set recording the is_fresh allocations in post conditions
/// (replacement mode only)
__CPROVER_contracts_obj_set_ptr_t linked_allocated;
/// \brief Object set recording the deallocations (used by was_freed)
__CPROVER_contracts_obj_set_ptr_t linked_deallocated;
/// \brief True iff this write set is used for contract replacement
__CPROVER_bool replacement;
/// \brief True iff the write set checks requires clauses in an assumption ctx
__CPROVER_bool assume_requires_ctx;
/// \brief True iff the write set checks requires clauses in an assertion ctx
Expand All @@ -97,6 +94,10 @@ typedef struct
__CPROVER_bool assume_ensures_ctx;
/// \brief True iff this write set checks ensures clauses in an assertion ctx
__CPROVER_bool assert_ensures_ctx;
/// \brief True iff dynamic allocation is allowed (default: true)
__CPROVER_bool allow_allocate;
/// \brief True iff dynamic deallocation is allowed (default: true)
__CPROVER_bool allow_deallocate;
} __CPROVER_contracts_write_set_t;

/// \brief Type of pointers to \ref __CPROVER_contracts_write_set_t.
Expand Down Expand Up @@ -388,7 +389,6 @@ __CPROVER_HIDE:;
/// \param[inout] set Pointer to the object to initialise
/// \param[in] contract_assigns_size Max size of the assigns clause
/// \param[in] contract_frees_size Max size of the frees clause
/// \param[in] replacement True iff this write set is used to replace a contract
/// \param[in] assume_requires_ctx True iff this write set is used to check side
/// effects in a requires clause in contract checking mode
/// \param[in] assert_requires_ctx True iff this write set is used to check side
Expand All @@ -397,15 +397,20 @@ __CPROVER_HIDE:;
/// side effects in an ensures clause in contract replacement mode
/// \param[in] assert_ensures_ctx True iff this write set is used to check for
/// side effects in an ensures clause in contract checking mode
/// \param[in] allow_allocate True iff the context gobally allows dynamic
/// allocation.
/// \param[in] allow_deallocate True iff the context gobally allows dynamic
/// deallocation.
void __CPROVER_contracts_write_set_create(
__CPROVER_contracts_write_set_ptr_t set,
__CPROVER_size_t contract_assigns_size,
__CPROVER_size_t contract_frees_size,
__CPROVER_bool replacement,
__CPROVER_bool assume_requires_ctx,
__CPROVER_bool assert_requires_ctx,
__CPROVER_bool assume_ensures_ctx,
__CPROVER_bool assert_ensures_ctx)
__CPROVER_bool assert_ensures_ctx,
__CPROVER_bool allow_allocate,
__CPROVER_bool allow_deallocate)
{
__CPROVER_HIDE:;
#ifdef DFCC_DEBUG
Expand All @@ -417,16 +422,8 @@ __CPROVER_HIDE:;
&(set->contract_assigns), contract_assigns_size);
__CPROVER_contracts_obj_set_create_indexed_by_object_id(
&(set->contract_frees));
set->replacement = replacement;
if(replacement)
{
__CPROVER_contracts_obj_set_create_append(
&(set->contract_frees_replacement), contract_frees_size);
}
else
{
set->contract_frees_replacement.elems = 0;
}
__CPROVER_contracts_obj_set_create_append(
&(set->contract_frees_append), contract_frees_size);
__CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->allocated));
__CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->deallocated));
set->linked_is_fresh = 0;
Expand All @@ -436,6 +433,8 @@ __CPROVER_HIDE:;
set->assert_requires_ctx = assert_requires_ctx;
set->assume_ensures_ctx = assume_ensures_ctx;
set->assert_ensures_ctx = assert_ensures_ctx;
set->allow_allocate = allow_allocate;
set->allow_deallocate = allow_deallocate;
}

/// \brief Releases resources used by \p set.
Expand All @@ -454,20 +453,16 @@ __CPROVER_HIDE:;
__CPROVER_rw_ok(&(set->contract_frees.elems), 0),
"contract_frees writable");
__CPROVER_assert(
(set->replacement == 0) ||
__CPROVER_rw_ok(&(set->contract_frees_replacement.elems), 0),
"contract_frees_replacement writable");
__CPROVER_rw_ok(&(set->contract_frees_append.elems), 0),
"contract_frees_append writable");
__CPROVER_assert(
__CPROVER_rw_ok(&(set->allocated.elems), 0), "allocated writable");
__CPROVER_assert(
__CPROVER_rw_ok(&(set->deallocated.elems), 0), "deallocated writable");
#endif
__CPROVER_deallocate(set->contract_assigns.elems);
__CPROVER_deallocate(set->contract_frees.elems);
if(set->replacement != 0)
{
__CPROVER_deallocate(set->contract_frees_replacement.elems);
}
__CPROVER_deallocate(set->contract_frees_append.elems);
__CPROVER_deallocate(set->allocated.elems);
__CPROVER_deallocate(set->deallocated.elems);
// do not free set->linked_is_fresh->elems or set->deallocated_linked->elems
Expand Down Expand Up @@ -585,29 +580,44 @@ __CPROVER_HIDE:;

// append pointer if available
#ifdef DFCC_DEBUG
if(set->replacement)
__CPROVER_contracts_obj_set_append(&(set->contract_frees_replacement), ptr);
__CPROVER_contracts_obj_set_append(&(set->contract_frees_append), ptr);
#else
if(set->replacement)
{
set->contract_frees_replacement.nof_elems =
set->contract_frees_replacement.watermark;
set->contract_frees_replacement
.elems[set->contract_frees_replacement.watermark] = ptr;
set->contract_frees_replacement.watermark += 1;
set->contract_frees_replacement.is_empty = 0;
}
set->contract_frees_append.nof_elems = set->contract_frees_append.watermark;
set->contract_frees_append.elems[set->contract_frees_append.watermark] = ptr;
set->contract_frees_append.watermark += 1;
set->contract_frees_append.is_empty = 0;
#endif
}

/// \brief Adds the pointer \p ptr to \p set->allocated.
/// \brief Adds the dynamically allocated pointer \p ptr to \p set->allocated.
/// \param[inout] set The set to update
/// \param[in] ptr Pointer to an object declared using a `DECL x` or
/// `x = __CPROVER_allocate(...)` GOTO instruction.
/// \param[in] ptr Pointer to a dynamic object `x = __CPROVER_allocate(...)`.
void __CPROVER_contracts_write_set_add_allocated(
__CPROVER_contracts_write_set_ptr_t set,
void *ptr)
{
__CPROVER_HIDE:;
__CPROVER_assert(set->allow_allocate, "dynamic allocation is allowed");
#if DFCC_DEBUG
// call inlined below
__CPROVER_contracts_obj_set_add(&(set->allocated), ptr);
#else
__CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
set->allocated.nof_elems = (set->allocated.elems[object_id] != 0)
? set->allocated.nof_elems
: set->allocated.nof_elems + 1;
set->allocated.elems[object_id] = ptr;
set->allocated.is_empty = 0;
#endif
}

/// \brief Adds the pointer \p ptr to \p set->allocated.
/// \param[inout] set The set to update
/// \param[in] ptr Pointer to an object declared using `DECL x`.
void __CPROVER_contracts_write_set_add_decl(
__CPROVER_contracts_write_set_ptr_t set,
void *ptr)
{
__CPROVER_HIDE:;
#if DFCC_DEBUG
// call inlined below
Expand Down Expand Up @@ -659,10 +669,6 @@ void __CPROVER_contracts_write_set_record_deallocated(
void *ptr)
{
__CPROVER_HIDE:;
#ifdef DFCC_DEBUG
__CPROVER_assert(set->replacement == 0, "!replacement");
#endif

#if DFCC_DEBUG
// we record the deallocation to be able to evaluate was_freed post conditions
__CPROVER_contracts_obj_set_add(&(set->deallocated), ptr);
Expand Down Expand Up @@ -735,7 +741,6 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_assignment(
// manually inlined below
{
__CPROVER_HIDE:;
__CPROVER_assert(set->replacement == 0, "!replacement");
__CPROVER_assert(
((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
"ptr NULL or writable up to size");
Expand Down Expand Up @@ -904,16 +909,13 @@ __CPROVER_HIDE:;
/// \param[in] set Write set to check the deallocation against
/// \param[in] ptr Deallocated pointer to check set to check the deallocation
/// against
/// \return True iff \p ptr is contained in \p set->contract_frees or
/// \p set->allocated.
/// \return True iff deallocation is allowed and \p ptr is contained in
/// \p set->contract_frees or \p set->allocated.
__CPROVER_bool __CPROVER_contracts_write_set_check_deallocate(
__CPROVER_contracts_write_set_ptr_t set,
void *ptr)
{
__CPROVER_HIDE:;
#ifdef DFCC_DEBUG
__CPROVER_assert(set->replacement == 0, "!replacement");
#endif
__CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);

#ifdef DFCC_DEBUG
Expand All @@ -924,16 +926,15 @@ __CPROVER_HIDE:;
set->allocated.indexed_by_object_id,
"set->allocated is indexed by object id");
#endif
return (ptr == 0) | (set->contract_frees.elems[object_id] == ptr) |
(set->allocated.elems[object_id] == ptr);
return (set->allow_deallocate) &
((ptr == 0) | (set->contract_frees.elems[object_id] == ptr) |
(set->allocated.elems[object_id] == ptr));
}

/// \brief Checks the inclusion of the \p candidate->contract_assigns elements
/// in \p reference->contract_assigns or \p reference->allocated.
///
/// \pre \p reference must not be in replacement mode.
/// \pre \p candidate must be in replacement mode and \p candidate->allocated
/// must be empty.
/// \pre \p candidate->allocated must be empty.
///
/// \param[in] reference Reference write set from a caller
/// \param[in] candidate Candidate write set from a contract being replaced
Expand All @@ -944,11 +945,6 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_assigns_clause_inclusion(
__CPROVER_contracts_write_set_ptr_t candidate)
{
__CPROVER_HIDE:;
#ifdef DFCC_DEBUG
__CPROVER_assert(
reference->replacement == 0, "reference set in !replacement");
__CPROVER_assert(candidate->replacement != 0, "candidate set in replacement");
#endif
__CPROVER_bool incl = 1;
__CPROVER_contracts_car_t *current = candidate->contract_assigns.elems;
__CPROVER_size_t idx = candidate->contract_assigns.max_elems;
Expand All @@ -969,9 +965,7 @@ __CPROVER_HIDE:;
/// \brief Checks the inclusion of the \p candidate->contract_frees elements
/// in \p reference->contract_frees or \p reference->allocated.
///
/// \pre \p reference must not be in replacement mode.
/// \pre \p candidate must be in replacement mode and \p candidate->allocated
/// must be empty.
/// \pre \p candidate->allocated must be empty.
///
/// \param[in] reference Reference write set from a caller
/// \param[in] candidate Candidate write set from a contract being replaced
Expand All @@ -983,9 +977,6 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_frees_clause_inclusion(
{
__CPROVER_HIDE:;
#ifdef DFCC_DEBUG
__CPROVER_assert(
reference->replacement == 0, "reference set in !replacement");
__CPROVER_assert(candidate->replacement != 0, "candidate set in replacement");
__CPROVER_assert(
reference->contract_frees.indexed_by_object_id,
"reference->contract_frees is indexed by object id");
Expand All @@ -994,8 +985,8 @@ __CPROVER_HIDE:;
"reference->allocated is indexed by object id");
#endif
__CPROVER_bool all_incl = 1;
void **current = candidate->contract_frees_replacement.elems;
__CPROVER_size_t idx = candidate->contract_frees_replacement.max_elems;
void **current = candidate->contract_frees_append.elems;
__CPROVER_size_t idx = candidate->contract_frees_append.max_elems;

SET_CHECK_FREES_CLAUSE_INCLUSION_LOOP:
while(idx != 0)
Expand Down Expand Up @@ -1030,13 +1021,8 @@ void __CPROVER_contracts_write_set_deallocate_freeable(
__CPROVER_contracts_write_set_ptr_t target)
{
__CPROVER_HIDE:;
#ifdef DFCC_DEBUG
__CPROVER_assert(set->replacement == 1, "set is in replacement");
__CPROVER_assert(
(target == 0) | (target->replacement == 0), "target is in !replacement");
#endif
void **current = set->contract_frees_replacement.elems;
__CPROVER_size_t idx = set->contract_frees_replacement.max_elems;
void **current = set->contract_frees_append.elems;
__CPROVER_size_t idx = set->contract_frees_append.max_elems;
SET_DEALLOCATE_FREEABLE_LOOP:
while(idx != 0)
{
Expand Down
1 change: 1 addition & 0 deletions src/goto-instrument/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ SRC = accelerate/accelerate.cpp \
contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp \
contracts/dynamic-frames/dfcc_instrument.cpp \
contracts/dynamic-frames/dfcc_spec_functions.cpp \
contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp \
contracts/dynamic-frames/dfcc_contract_functions.cpp \
contracts/dynamic-frames/dfcc_wrapper_program.cpp \
contracts/dynamic-frames/dfcc_contract_handler.cpp \
Expand Down
15 changes: 12 additions & 3 deletions src/goto-instrument/contracts/dynamic-frames/dfcc.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,14 +92,14 @@ parse_function_contract_pair(const irep_idt &cli_flag)
else if(split.size() == 2)
{
auto function_name = split[0];
if(function_name.size() == 0)
if(function_name.empty())
{
throw invalid_function_contract_pair_exceptiont{
"couldn't find function name before '/' in '" + cli_flag_str + "'",
correct_format_message};
}
auto contract_name = split[1];
if(contract_name.size() == 0)
if(contract_name.empty())
{
throw invalid_function_contract_pair_exceptiont{
"couldn't find contract name after '/' in '" + cli_flag_str + "'",
Expand Down Expand Up @@ -191,14 +191,21 @@ dfcct::dfcct(
instrument(goto_model, message_handler, utils, library),
memory_predicates(goto_model, utils, library, instrument, message_handler),
spec_functions(goto_model, message_handler, utils, library, instrument),
contract_clauses_codegen(
goto_model,
message_handler,
utils,
library,
spec_functions),
contract_handler(
goto_model,
message_handler,
utils,
library,
instrument,
memory_predicates,
spec_functions),
spec_functions,
contract_clauses_codegen),
swap_and_wrap(
goto_model,
message_handler,
Expand Down Expand Up @@ -483,6 +490,8 @@ void dfcct::instrument_other_functions()

goto_model.goto_functions.update();

// TODO specialise the library functions for the max size of
// loop and function contracts
Comment on lines +493 to +494
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shall we create a GitHub issue about this and add the link here? It might be better to track this later.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is still work in progress this will already be addressed in the final version

Copy link
Collaborator Author

@remi-delmas-3000 remi-delmas-3000 Feb 21, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

DELETED

Copy link
Collaborator

@tautschnig tautschnig Feb 22, 2023 •
edited by remi-delmas-3000
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But then ... haven't you resolved the "TODO" and should remove this comment?

This has to be implemented in the forthcoming loop contracts PR, this TODO is just a marker that tells you where to do it

Copy link
Collaborator Author

@remi-delmas-3000 remi-delmas-3000 Feb 22, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry this one is a TODO for @qinheping , my comment above applied to two other TODOs I've turned into reqs.

if(to_check.has_value())
{
log.status() << "Specializing cprover_contracts functions for assigns "
Expand Down
5 changes: 4 additions & 1 deletion src/goto-instrument/contracts/dynamic-frames/dfcc.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ Author: Remi Delmas, [email protected]
#include <util/irep.h>
#include <util/message.h>

#include "dfcc_contract_clauses_codegen.h"
#include "dfcc_contract_handler.h"
#include "dfcc_instrument.h"
#include "dfcc_library.h"
Expand Down Expand Up @@ -208,13 +209,15 @@ class dfcct
message_handlert &message_handler;
messaget log;

// hold the global state of the transformation (caches etc.)
// Singletons that hold the global state of the program transformation
// (caches etc.)
dfcc_utilst utils;
dfcc_libraryt library;
namespacet ns;
dfcc_instrumentt instrument;
dfcc_lift_memory_predicatest memory_predicates;
dfcc_spec_functionst spec_functions;
dfcc_contract_clauses_codegent contract_clauses_codegen;
dfcc_contract_handlert contract_handler;
dfcc_swap_and_wrapt swap_and_wrap;

Expand Down
Loading