Patchwork [Ada] Static predicate checks on type conversions

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 1, 2012, 1:21 p.m.
Message ID <20121001132144.GA14301@adacore.com>
Download mbox | patch
Permalink /patch/188293/
State New
Headers show

Comments

Arnaud Charlet - Oct. 1, 2012, 1:21 p.m.
In Ada 2012, if a subtype has predicates, a predicate check must be applied to
the expression in a type conversion to the subtype. Furthermore, if the
expression is a scalar static constant, the predicate must be evluated at
compile-time, and the program must be rejected if the predicate is false.

Compiling

   gcc -c -gnat12 -gnata main.adb

must yield:

   main.adb:6:16: static expression fails static predicate check on "T"

---
procedure Main is
   subtype T is Integer
   with Static_Predicate => T >= 10;
   V : T := 10;
begin
   V := 1000 / T (9);
end Main;

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

2012-10-01  Ed Schonberg  <schonberg@adacore.com>

	* checks.adb (Apply_Predicate_Check): If the predicate is a
	static one and the operand is static, evaluate the predicate at
	compile time.
	* sem_eval.ads, sem_eval.adb (Eval_Static_Predicate_Check): new
	procedure, to evaluate a static predicate check whenever possible.
	* sem_res.adb (Resolve_Type_Conversion): Apply predicate check
	on the conversion if the target type has predicates.

Patch

Index: checks.adb
===================================================================
--- checks.adb	(revision 191920)
+++ checks.adb	(working copy)
@@ -2337,6 +2337,23 @@ 
                  (Sloc (N), Reason => SE_Infinite_Recursion));
 
          else
+
+            --  If the predicate is a static predicate and the operand is
+            --  static, the predicate must be evaluated statically. If the
+            --  evaluation fails this is a static constraint error.
+
+            if Is_OK_Static_Expression (N) then
+               if  Present (Static_Predicate (Typ)) then
+                  if Eval_Static_Predicate_Check (N, Typ) then
+                     return;
+                  else
+                     Error_Msg_NE
+                       ("static expression fails static predicate check on&",
+                          N, Typ);
+                  end if;
+               end if;
+            end if;
+
             Insert_Action (N,
               Make_Predicate_Check (Typ, Duplicate_Subexpr (N)));
          end if;
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 191920)
+++ sem_res.adb	(working copy)
@@ -9713,6 +9713,22 @@ 
             end if;
          end;
       end if;
+
+      --  Ada 2012: if target type has predicates, the result requires a
+      --  predicate check. If the context is a call to another predicate
+      --  check we must prevent infinite recursion.
+
+      if Has_Predicates (Target_Typ) then
+         if Nkind (Parent (N)) = N_Function_Call
+           and then Present (Name (Parent (N)))
+           and then Has_Predicates (Entity (Name (Parent (N))))
+         then
+            null;
+
+         else
+            Apply_Predicate_Check (N, Target_Typ);
+         end if;
+      end if;
    end Resolve_Type_Conversion;
 
    ----------------------
Index: sem_eval.adb
===================================================================
--- sem_eval.adb	(revision 191895)
+++ sem_eval.adb	(working copy)
@@ -3249,6 +3249,37 @@ 
       end if;
    end Eval_Slice;
 
+   ---------------------------------
+   -- Eval_Static_Predicate_Check --
+   ---------------------------------
+
+   function Eval_Static_Predicate_Check
+     (N   : Node_Id;
+      Typ : Entity_Id) return Boolean
+   is
+      Loc  : constant Source_Ptr := Sloc (N);
+      Pred : constant List_Id := Static_Predicate (Typ);
+      Test : Node_Id;
+   begin
+      if No (Pred) then
+         return True;
+      end if;
+
+      --  The static predicate is a list of alternatives in the proper format
+      --  for an Ada 2012 membership test. If the argument is a literal, the
+      --  membership test can be evaluated statically. The caller transforms
+      --  a result of False into a static contraint error.
+
+      Test := Make_In (Loc,
+         Left_Opnd    => New_Copy_Tree (N),
+         Right_Opnd   => Empty,
+         Alternatives => Pred);
+      Analyze_And_Resolve (Test, Standard_Boolean);
+
+      return Nkind (Test) = N_Identifier
+        and then Entity (Test) = Standard_True;
+   end Eval_Static_Predicate_Check;
+
    -------------------------
    -- Eval_String_Literal --
    -------------------------
Index: sem_eval.ads
===================================================================
--- sem_eval.ads	(revision 191888)
+++ sem_eval.ads	(working copy)
@@ -317,6 +317,11 @@ 
    procedure Eval_Unary_Op               (N : Node_Id);
    procedure Eval_Unchecked_Conversion   (N : Node_Id);
 
+   function Eval_Static_Predicate_Check
+     (N  : Node_Id;
+     Typ : Entity_Id) return Boolean;
+   --  Evaluate a static predicate check applied to a scalar literal.
+
    procedure Fold_Str (N : Node_Id; Val : String_Id; Static : Boolean);
    --  Rewrite N with a new N_String_Literal node as the result of the compile
    --  time evaluation of the node N. Val is the resulting string value from