[Ada] Reject certain constants as constituents

Message ID 20171215111642.GA47507@adacore.com
State New
Headers show
Series
  • [Ada] Reject certain constants as constituents
Related show

Commit Message

Pierre-Marie de Rodat Dec. 15, 2017, 11:16 a.m.
This patch updates the analysis of pragma Refined_State to reject constants
which are used as refinement constituents and are either

   * Part of the visible state of a package

   * Part of the hidden state of a package, and lack indicator Part_Of.

------------
-- Source --
------------

--  var.ads

package Var
  with SPARK_Mode,
       Initializes => Input
is
   Input : Integer := 0;
end Var;

--  pack.ads

with Var;

package Pack
  with SPARK_Mode,
       Abstract_State => State
is
   procedure Force_Body;

private
   Const_1 : constant Integer := Var.Input;
   Const_2 : constant Integer := 2 with Part_Of => State;

   Var_1 : Integer := 1;
   Var_2 : Integer := 2 with Part_Of => State;

   package Priv_Pack is
      Const_3 : constant Integer := Var.Input;
      Const_4 : constant Integer := 4 with Part_Of => State;

      Var_3 : Integer := 3;
      Var_4 : Integer := 4 with Part_Of => State;
   end Priv_Pack;
end Pack;

--  pack.adb

package body Pack
  with SPARK_Mode,
       Refined_State =>
         (State =>
           (Const_1,                                                 --  Error
            Const_2,                                                 --  OK
            Var_1,                                                   --  Error
            Var_2,                                                   --  OK
            Priv_Pack.Const_3,                                       --  Error
            Priv_Pack.Const_4,                                       --  OK
            Priv_Pack.Var_3,                                         --  Error
            Priv_Pack.Var_4,                                         --  OK
            Const_5,                                                 --  OK
            Const_6,                                                 --  OK
            Body_Pack.Const_7,                                       --  OK
            Body_Pack.Const_8))                                      --  OK
is
   Const_5 : constant Integer := Var.Input;
   Const_6 : constant Integer := 6;

   package Body_Pack is
      Const_7 : constant Integer := Var.Input;
      Const_8 : constant Integer := 8;
   end Body_Pack;

   procedure Force_Body is begin null; end Force_Body;
end Pack;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c -gnatf pack.adb
pack.adb:5:13: cannot use "Const_1" in refinement, constituent is not a hidden
  state of package "Pack"
pack.adb:7:13: cannot use "Var_1" in refinement, constituent is not a hidden
  state of package "Pack"
pack.adb:9:22: cannot use "Const_3" in refinement, constituent is not a hidden
  state of package "Pack"
pack.adb:11:22: cannot use "Var_3" in refinement, constituent is not a hidden
  state of package "Pack"
pack.ads:13:04: indicator Part_Of is required in this context (SPARK RM
  7.2.6(2))
pack.ads:13:04: "Var_1" is declared in the private part of package "Pack"
pack.ads:20:07: indicator Part_Of is required in this context (SPARK RM
  7.2.6(2))
pack.ads:20:07: "Var_3" is declared in the private part of package "Pack"

Tested on x86_64-pc-linux-gnu, committed on trunk

2017-12-15  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Match_Constituent): Do not quietly accept constants as
	suitable constituents.
	* exp_util.adb: Minor reformatting.

Patch

Index: exp_util.adb
===================================================================
--- exp_util.adb	(revision 255683)
+++ exp_util.adb	(working copy)
@@ -165,6 +165,10 @@ 
    --  Force evaluation of bounds of a slice, which may be given by a range
    --  or by a subtype indication with or without a constraint.
 
+   function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean;
+   --  Determine whether pragma Default_Initial_Condition denoted by Prag has
+   --  an assertion expression that should be verified at run time.
+
    function Make_CW_Equivalent_Type
      (T : Entity_Id;
       E : Node_Id) return Entity_Id;
@@ -1500,6 +1504,7 @@ 
       --  Start of processing for Add_Own_DIC
 
       begin
+         pragma Assert (Present (DIC_Expr));
          Expr := New_Copy_Tree (DIC_Expr);
 
          --  Perform the following substitution:
@@ -1733,8 +1738,6 @@ 
          --  Produce an empty completing body in the following cases:
          --    * Assertions are disabled
          --    * The DIC Assertion_Policy is Ignore
-         --    * Pragma DIC appears without an argument
-         --    * Pragma DIC appears with argument "null"
 
          if No (Stmts) then
             Stmts := New_List (Make_Null_Statement (Loc));
@@ -8715,6 +8718,21 @@ 
           and then Is_Itype (Full_Typ);
    end Is_Untagged_Private_Derivation;
 
+   ------------------------------
+   -- Is_Verifiable_DIC_Pragma --
+   ------------------------------
+
+   function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean is
+      Args : constant List_Id := Pragma_Argument_Associations (Prag);
+
+   begin
+      --  To qualify as verifiable, a DIC pragma must have a non-null argument
+
+      return
+        Present (Args)
+          and then Nkind (Get_Pragma_Arg (First (Args))) /= N_Null;
+   end Is_Verifiable_DIC_Pragma;
+
    ---------------------------
    -- Is_Volatile_Reference --
    ---------------------------
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 255678)
+++ sem_prag.adb	(working copy)
@@ -27327,25 +27327,14 @@ 
                      end loop;
                   end if;
 
-                  --  Constants are part of the hidden state of a package, but
-                  --  the compiler cannot determine whether they have variable
-                  --  input (SPARK RM 7.1.1(2)) and cannot classify them as a
-                  --  hidden state. Accept the constant quietly even if it is
-                  --  a visible state or lacks a Part_Of indicator.
+                  --  At this point it is known that the constituent is not
+                  --  part of the package hidden state and cannot be used in
+                  --  a refinement (SPARK RM 7.2.2(9)).
 
-                  if Ekind (Constit_Id) = E_Constant then
-                     Collect_Constituent;
-
-                  --  If we get here, then the constituent is not a hidden
-                  --  state of the related package and may not be used in a
-                  --  refinement (SPARK RM 7.2.2(9)).
-
-                  else
-                     Error_Msg_Name_1 := Chars (Spec_Id);
-                     SPARK_Msg_NE
-                       ("cannot use & in refinement, constituent is not a "
-                        & "hidden state of package %", Constit, Constit_Id);
-                  end if;
+                  Error_Msg_Name_1 := Chars (Spec_Id);
+                  SPARK_Msg_NE
+                    ("cannot use & in refinement, constituent is not a hidden "
+                     & "state of package %", Constit, Constit_Id);
                end if;
             end Match_Constituent;