[Ada] Set range checks flag on 'Update for GNATprove in expansion

Message ID 20200706113855.GA135539@adacore.com
State New
Headers show
Series
  • [Ada] Set range checks flag on 'Update for GNATprove in expansion
Related show

Commit Message

Pierre-Marie de Rodat July 6, 2020, 11:38 a.m.
Range check flag on scalar expression in attribute Update was originally
set when this attribute is expanded into a sequence of assignment.
However, in GNATprove mode we have a custom expansion, which does
nothing with attribute Update; in particular, it didn't set the required
range check. As a workaround, we set this flag while resolving the
attribute, both for GNAT
and GNATprove.

Yet, this didn't really work for attribute Update in subprograms
"inlined for proof", where for some reason no checks at all were
inserted.

Also, this extra range check was unnecessary for a code like this:

   type T is record C : Natural; end record;
   X : T := (C => 1);
   Y : T := X'Update (C => X.C + 1);

because an overflow check (which is emitted anyway) is enough to protect
from a failing range check. A similar code, just without attribute
Update, does not have a range check:

   Y.C := X.C + 1;

This extra range check was hurting both compilation (by generating
useless run-time checks) and proof (by triggering messages about checks
that can never fail).

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

gcc/ada/

	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Apply
	scalar range checks.
	* sem_attr.adb (Resolve_Attribute): Do not set scalar range
	checks when resolving attribute Update.

Patch

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -251,6 +251,53 @@  package body Exp_SPARK is
             Analyze_And_Resolve (N, Standard_Boolean);
          end if;
 
+      elsif Attr_Id = Attribute_Update then
+         declare
+            Aggr : constant Node_Id := First (Expressions (N));
+            --  The aggregate expression
+
+            Assoc     : Node_Id;
+            Comp      : Node_Id;
+            Comp_Type : Node_Id;
+            Expr      : Node_Id;
+
+         begin
+            --  Apply scalar range checks on the updated components, if needed
+
+            if Is_Array_Type (Typ) then
+               Assoc := First (Component_Associations (Aggr));
+
+               while Present (Assoc) loop
+                  Expr      := Expression (Assoc);
+                  Comp_Type := Component_Type (Typ);
+
+                  if Is_Scalar_Type (Comp_Type) then
+                     Apply_Scalar_Range_Check (Expr, Comp_Type);
+                  end if;
+
+                  Next (Assoc);
+               end loop;
+
+            else pragma Assert (Is_Record_Type (Typ));
+
+               Assoc := First (Component_Associations (Aggr));
+               while Present (Assoc) loop
+                  Expr      := Expression (Assoc);
+                  Comp      := First (Choices (Assoc));
+                  Comp_Type := Etype (Entity (Comp));
+
+                  --  Use the type of the first component from the Choices
+                  --  list, as multiple components can only appear there if
+                  --  they have exactly the same type.
+
+                  if Is_Scalar_Type (Comp_Type) then
+                     Apply_Scalar_Range_Check (Expr, Comp_Type);
+                  end if;
+
+                  Next (Assoc);
+               end loop;
+            end if;
+         end;
       end if;
    end Expand_SPARK_N_Attribute_Reference;
 


diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -11995,26 +11995,6 @@  package body Sem_Attr is
                   Expr := Expression (Assoc);
                   Resolve (Expr, Component_Type (Typ));
 
-                  --  For scalar array components set Do_Range_Check when
-                  --  needed. Constraint checking on non-scalar components
-                  --  is done in Aggregate_Constraint_Checks, but only if
-                  --  full analysis is enabled. These flags are not set in
-                  --  the front-end in GnatProve mode.
-
-                  if Is_Scalar_Type (Component_Type (Typ))
-                    and then not Is_OK_Static_Expression (Expr)
-                    and then not Range_Checks_Suppressed (Component_Type (Typ))
-                  then
-                     if Is_Entity_Name (Expr)
-                       and then Etype (Expr) = Component_Type (Typ)
-                     then
-                        null;
-
-                     else
-                        Set_Do_Range_Check (Expr);
-                     end if;
-                  end if;
-
                   --  The choices in the association are static constants,
                   --  or static aggregates each of whose components belongs
                   --  to the proper index type. However, they must also
@@ -12072,14 +12052,6 @@  package body Sem_Attr is
                     and then not Error_Posted (Comp)
                   then
                      Resolve (Expr, Etype (Entity (Comp)));
-
-                     if Is_Scalar_Type (Etype (Entity (Comp)))
-                       and then not Is_OK_Static_Expression (Expr)
-                       and then not Range_Checks_Suppressed
-                                      (Etype (Entity (Comp)))
-                     then
-                        Set_Do_Range_Check (Expr);
-                     end if;
                   end if;
 
                   Next (Assoc);