Skip to content

Commit

Permalink
Merge pull request #6 from NinaRanns/contracts-constify
Browse files Browse the repository at this point in the history
constification of postcondition variable, automatic variables, and pa…
  • Loading branch information
villevoutilainen authored Jun 5, 2024
2 parents f33d20d + 35bc179 commit f08882e
Show file tree
Hide file tree
Showing 5 changed files with 86 additions and 2 deletions.
4 changes: 4 additions & 0 deletions gcc/c-family/c.opt
Original file line number Diff line number Diff line change
Expand Up @@ -1733,6 +1733,10 @@ fcontracts-nonattr
C++ Var(flag_contracts_nonattr) Init(0)
Enable the non-attribute syntax for contracts.

fcontracts-nonattr-noconst
C++ Var(flag_contracts_nonattr_noconst) Init(0)
Disable the consitification of entities appearing in a contract condition.

fcontract-assumption-mode=
C++ Joined RejectNegative
-fcontract-assumption-mode=[on|off] Enable or disable treating axiom level contracts as assumptions (default on).
Expand Down
31 changes: 29 additions & 2 deletions gcc/cp/contracts.cc
Original file line number Diff line number Diff line change
Expand Up @@ -601,7 +601,7 @@ invalidate_contract (tree t)
return t;
}

/* Returns an invented parameter declration of the form 'TYPE ID' for the
/* Returns an invented parameter declaration of the form 'TYPE ID' for the
purpose of parsing the postcondition.
We use a PARM_DECL instead of a VAR_DECL so that tsubst forces a lookup
Expand All @@ -617,6 +617,10 @@ make_postcondition_variable (cp_expr id, tree type)
DECL_ARTIFICIAL (decl) = true;
DECL_SOURCE_LOCATION (decl) = id.get_location ();

// constify the postcondition variable
if (flag_contracts_nonattr && !flag_contracts_nonattr_noconst)
TREE_READONLY(decl) = 1;

pushdecl (decl);
return decl;
}
Expand Down Expand Up @@ -980,7 +984,7 @@ retain_decl (tree decl, copy_body_data *)
When declarations are merged, we sometimes need to update contracts to
refer to new parameters.
If DUPLICATE_P is true, this is called by duplicate_decls to rewrite contacts
If DUPLICATE_P is true, this is called by duplicate_decls to rewrite contracts
in terms of a new set of parameters. In this case, we can retain local
variables appearing in the contract because the contract is not being
prepared for insertion into a new function. Importantly, this preserves the
Expand Down Expand Up @@ -1929,6 +1933,29 @@ finish_contract_condition (cp_expr condition)
return condition_conversion (condition);
}

/* constify access to an id from within the contract condition */
tree
constify_contract_access(tree decl)
{
/* only constifies the automatic storage variables for now.
* The postcondition variable is created const. Parameters need to be
* checked separately, and we also need to make references and *this const
*/

if (!TREE_READONLY (decl)
&& ((VAR_P (decl) && decl_storage_duration (decl) == dk_auto)
|| (REFERENCE_REF_P(decl) && decl_storage_duration (TREE_OPERAND (decl, 0)) == dk_auto)
|| (TREE_CODE (decl) == PARM_DECL)))
{

tree ctype = TREE_TYPE (decl);
ctype = cp_build_qualified_type (ctype, (cp_type_quals (ctype)
| TYPE_QUAL_CONST));
decl = build1 (VIEW_CONVERT_EXPR, ctype, decl);
}
return decl;
}

void
maybe_update_postconditions (tree fco)
{
Expand Down
1 change: 1 addition & 0 deletions gcc/cp/cp-tree.h
Original file line number Diff line number Diff line change
Expand Up @@ -8644,6 +8644,7 @@ extern tree make_postcondition_variable (cp_expr);
extern tree make_postcondition_variable (cp_expr, tree);
extern tree grok_contract (tree, tree, tree, cp_expr, location_t);
extern tree finish_contract_condition (cp_expr);
extern tree constify_contract_access (tree);

/* Return the first contract in ATTRS, or NULL_TREE if there are none. */

Expand Down
6 changes: 6 additions & 0 deletions gcc/cp/semantics.cc
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ along with GCC; see the file COPYING3. If not see
#include "gomp-constants.h"
#include "predict.h"
#include "memmodel.h"
#include "print-tree.h"

/* There routines provide a modular interface to perform many parsing
operations. They may therefore be used during actual parsing, or
Expand Down Expand Up @@ -4424,6 +4425,11 @@ finish_id_expression_1 (tree id_expression,
}
}

if (flag_contracts_nonattr && !flag_contracts_nonattr_noconst
&& processing_contract_condition)
{
decl = constify_contract_access(decl);
}
return cp_expr (decl, location);
}

Expand Down
46 changes: 46 additions & 0 deletions gcc/testsuite/g++.dg/contracts/new/constification.C
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
// generic assert contract parsing checks
// check omitted, 'default', 'audit', and 'axiom' contract levels parse
// check that all concrete semantics parse
// check omitted, '%default' contract roles parse
// ensure that an invalid contract level 'invalid' errors
// ensure that a predicate referencing an undefined variable errors
// ensure that a missing colon after contract level errors
// ensure that an invalid contract role 'invalid' errors
// ensure that a missing colon after contract role errors
// { dg-do compile }
// { dg-options "-std=c++2a -fcontracts -fcontracts-nonattr " }

static_assert (__cpp_contracts >= 201906);
static_assert (__cpp_contracts_literal_semantics >= 201906);
static_assert (__cpp_contracts_roles >= 201906);

int gi = 7;

void f1(int i) pre(i++); // { dg-error "increment of read-only location" }
void f2(int &i) pre(i++); // { dg-error "increment of read-only location" }
void f3(int *i) pre(i++); // { dg-error "increment of read-only location" }
void f4(int *i) pre((*i)++); // ok, not deep const
void f5(int *i) pre(gi++); // ok, non automatic storage

// todo structured binding test
// lambda tests
// template tests
int main()
{
int i;
contract_assert(i++); // { dg-error "increment of read-only location" }
i = 5;

int& ri = i;
contract_assert(ri++); // { dg-error "increment of read-only location" }
ri = 6;

int *pi= &i;
contract_assert(pi++); // { dg-error "increment of read-only location" }
contract_assert((*pi)++); // ok, not deep const

contract_assert(i == 4 ? i : i ); // ok, no name clash


return 0;
}

0 comments on commit f08882e

Please sign in to comment.