diff mbox

[Ada] Static predicates on strings

Message ID 20170113100529.GA47700@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Jan. 13, 2017, 10:05 a.m. UTC
RM 3.2.4 stipulates that comparison operators on strings are legal in the
expression for a Static_Predicate aspect of a string type. The implementation
of this capability was deferred because it conflicts with the definition of
static expression (RM 4.9) which excludes string comparisons from staticness.
This inconsistency will eventually be resolved by the ARG, but it is worth
implementing the wider scope of static predicates to include string comparison.

Executing:

   gnatmake -q -gnatws -gnata main
   main

must yield:

   Some_String OK
   Early_String OK
   Middle_String  OK
   Late_String  OK

---
with Text_IO; use Text_IO;
with support; use support;
procedure main is
  Maybe : Boolean := String'("ABC") < "CDE";
begin
  begin
     declare
        Wrong : constant some_String := "abcdefg";
     begin
        null;
     end;
  exception
     when others => Put_Line ("Some_String OK");
  end;

  begin
     declare
        Wrong : Early_String := "ebcdefg";
     begin
        null;
     end;
  exception
     when others => Put_Line ("Early_String OK");
  end;
  begin
     declare
        Wrong : Middle_String := "abcdefg";
     begin
        null;
     end;
  exception
     when others => Put_Line ("Middle_String  OK");
  end;
  begin
     declare
        Wrong : Late_String := "abcdefg";
     begin
        null;
     end;
  exception
     when others => Put_Line ("Late_String  OK");
  end;
end;
---
package Support is
   subtype My_String is String (1 .. 7);

   subtype My_Special_String is My_String with
     Static_Predicate => My_Special_String = "aaaaaaa";

   subtype My_short_String is My_String with
     Static_Predicate => My_short_String'length > 6;

   subtype Early_String is My_String with
     Static_Predicate => Early_String < "ddddddd";

   subtype Late_String is My_String with
     Static_Predicate => "ddddddd" < Late_String;

   subtype Middle_String is MY_String with
      Static_Predicate => Middle_String >= "aaa"
         and then "ggg" < Middle_String;

   subtype Some_String is My_String with
      Static_Predicate => Some_String in "aaaaaaa" | "zzzzzzz";
end Support;

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

2017-01-13  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch13.adb (Is_Predicate_Static): Following the intent of the RM,
	treat comparisons on strings as legal in a Static_Predicate.
	(Is_Predicate_Static, Is_Type_Ref): Predicate also returns true on
	a function call that is the expansion of a string comparison.The
	function call is built when compiling the corresponding predicate
	function, but the expression has been found legal as a static
	predicate during earlier analysis.
	* sem_eval.adb (Real_Or_String_Static_Predicate_Matches): Handle
	properly a function call that is the expansion of a string
	comparison operation, in order to recover the Static_Predicate
	expression and apply it to a static argument when needed.
diff mbox

Patch

Index: sem_eval.adb
===================================================================
--- sem_eval.adb	(revision 244369)
+++ sem_eval.adb	(working copy)
@@ -5469,6 +5469,40 @@ 
                return Skip;
             end;
 
+         --  The predicate function may contain string-comparison operations
+         --  that have been converted into calls to run-time array-comparison
+         --  routines. To evaluate the predicate statically, we recover the
+         --  original comparison operation and replace the occurrence of the
+         --  formal by the static string value. The actuals of the generated
+         --  call are of the form X'Address.
+
+         elsif Nkind (N) in N_Op_Compare
+           and then Nkind (Left_Opnd (N)) = N_Function_Call
+         then
+            declare
+               C : constant Node_Id := Left_Opnd (N);
+               F : constant Node_Id := First (Parameter_Associations (C));
+               L : constant Node_Id := Prefix (F);
+               R : constant Node_Id := Prefix (Next (F));
+
+            begin
+               --  If an operand is an entity name, it is the formal of the
+               --  predicate function, so replace it with the string value.
+               --  It may be either operand in the call. The other operand
+               --  is a static string from the original predicate.
+
+               if Is_Entity_Name (L) then
+                  Rewrite (Left_Opnd (N),  New_Copy (Val));
+                  Rewrite (Right_Opnd (N), New_Copy (R));
+
+               else
+                  Rewrite (Left_Opnd (N),  New_Copy (L));
+                  Rewrite (Right_Opnd (N), New_Copy (Val));
+               end if;
+
+               return Skip;
+            end;
+
          else
             return OK;
          end if;
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 244396)
+++ sem_ch13.adb	(working copy)
@@ -11603,11 +11603,18 @@ 
 
       function Is_Type_Ref (N : Node_Id) return Boolean;
       pragma Inline (Is_Type_Ref);
+
       --  Returns True if N is a reference to the type for the predicate in the
       --  expression (i.e. if it is an identifier whose Chars field matches the
       --  Nam given in the call). N must not be parenthesized, if the type name
       --  appears in parens, this routine will return False.
 
+      --  The routine also returns True for function calls generated during the
+      --  expansion of comparison operators on strings, which are intended to
+      --  be legal in static predicates, and are converted into calls to array
+      --  comparison routines in the body of the corresponding predicate
+      --  function.
+
       ----------------------------------
       -- All_Static_Case_Alternatives --
       ----------------------------------
@@ -11671,9 +11678,10 @@ 
 
       function Is_Type_Ref (N : Node_Id) return Boolean is
       begin
-         return Nkind (N) = N_Identifier
-           and then Chars (N) = Nam
-           and then Paren_Count (N) = 0;
+         return (Nkind (N) = N_Identifier
+                  and then Chars (N) = Nam
+                  and then Paren_Count (N) = 0)
+           or else Nkind (N) = N_Function_Call;
       end Is_Type_Ref;
 
    --  Start of processing for Is_Predicate_Static
@@ -11723,10 +11731,12 @@ 
       --  and inequality operations to be valid on strings (this helps deal
       --  with cases where we transform A in "ABC" to A = "ABC).
 
+      --  In fact, it appears that the intent of the ARG is to extend static
+      --  predicates to strings, and that the extension should probably apply
+      --  to static expressions themselves. The code below accepts comparison
+      --  operators that apply to static strings.
+
       elsif Nkind (Expr) in N_Op_Compare
-        and then ((not Is_String_Type (Etype (Left_Opnd (Expr))))
-                    or else (Nkind_In (Expr, N_Op_Eq, N_Op_Ne)
-                              and then not Comes_From_Source (Expr)))
         and then ((Is_Type_Ref (Left_Opnd (Expr))
                     and then Is_OK_Static_Expression (Right_Opnd (Expr)))
                   or else
@@ -12323,7 +12333,7 @@ 
            and then From_Aspect_Specification (N)
          then
             Error_Msg_NE
-              ("aspect specification causes premature freezing of&", T, N);
+              ("aspect specification causes premature freezing of&", N, T);
             Set_Has_Delayed_Freeze (T, False);
             return True;
          end if;