From patchwork Wed Sep 6 11:56:49 2017 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 810536 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (mailfrom) smtp.mailfrom=gcc.gnu.org (client-ip=209.132.180.131; helo=sourceware.org; envelope-from=gcc-patches-return-461591-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="mMWH6CZO"; dkim-atps=neutral Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 3xnMWl5Fnkz9s8J for ; Wed, 6 Sep 2017 21:57:07 +1000 (AEST) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=StqWYjdLKaAq7h4gO7NjtfEf9YPgPLCNg8cXAJw9wyIskq+5By 3NarD9JbEoG5rPX41TEK97HNxaVzEZ8Cs69ATxbkkfPJxCkfZ92ZlStGiNDbAmBM FR4a29KHNfA0Q/pFfoK3UnlC5zq5msrqrl+RvwmocXmxnRvFWVAZGQsHE= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=zNETeY3k8lxF8vCdEm0YlGS2fzQ=; b=mMWH6CZOK/nnXpIYkRXa a+Xdi+SqYXy7sI1WBYq6eWY/9lLc9RzHeGBUWy2pE0Fvb5aKohmoPDL4/qz0WCtu AoOru9zOlFclBqJI1F3heN6OOaaRKv/CY0Ltj9qgtBBznkX9sn/Y/Rguo+bgTgla 6ZJemWSu+esyk+7mAId8Kws= Received: (qmail 56609 invoked by alias); 6 Sep 2017 11:56:53 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 56429 invoked by uid 89); 6 Sep 2017 11:56:52 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-10.4 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy=Dimensional, integrate X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Wed, 06 Sep 2017 11:56:50 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 17DB05614D; Wed, 6 Sep 2017 07:56:49 -0400 (EDT) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id F2B7IKmFE17W; Wed, 6 Sep 2017 07:56:49 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 0689556142; Wed, 6 Sep 2017 07:56:49 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4192) id 0584E4AC; Wed, 6 Sep 2017 07:56:49 -0400 (EDT) Date: Wed, 6 Sep 2017 07:56:49 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Ed Schonberg Subject: [Ada] Dimensional checking and generic subprograms Message-ID: <20170906115649.GA140817@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) This patch enahnces dimensionality checking to cover generic subprograms that are intended to apply to types of different dimensions, such as an integration function. Dimensionality checking is performed in each instance. and rely on a special handling of conversion operations to prevent spurious dimensional errors in the generic unit itself. The following must compile quietly: gcc -c -gnatws integrate.adb --- package Dims with SPARK_Mode is ----------------------------------------- -- Setup Dimension System ----------------------------------------- type Unit_Type is new Float with Dimension_System => ((Unit_Name => Meter, Unit_Symbol => 'm', Dim_Symbol => 'L'), (Unit_Name => Kilogram, Unit_Symbol => "kg", Dim_Symbol => 'M'), (Unit_Name => Second, Unit_Symbol => 's', Dim_Symbol => 'T'), (Unit_Name => Ampere, Unit_Symbol => 'A', Dim_Symbol => 'I'), (Unit_Name => Kelvin, Unit_Symbol => 'K', Dim_Symbol => "Theta"), (Unit_Name => Radian, Unit_Symbol => "Rad", Dim_Symbol => "A")), Default_Value => 0.0; -- Base Dimensions subtype Length_Type is Unit_Type with Dimension => (Symbol => 'm', Meter => 1, others => 0); subtype Time_Type is Unit_Type with Dimension => (Symbol => 's', Second => 1, others => 0); subtype Linear_Velocity_Type is Unit_Type with Dimension => (Meter => 1, Second => -1, others => 0); -- Base Units Meter : constant Length_Type := Length_Type (1.0); Second : constant Time_Type := Time_Type (1.0); end dims; --- with Dims; use Dims; procedure Integrate is generic type Op1 is new Unit_Type; type Op2 is new Unit_Type; type Res is new Unit_Type; function I (X : op1; Y : Op2) return Res; function I (X : op1; Y : Op2) return Res is begin return Res (Unit_Type (X) * Unit_type (Y)); end I; function Distance is new I (Time_Type, Linear_Velocity_Type, Length_Type); Secs : Time_Type := 5.0; Speed : Linear_Velocity_Type := 10.0; Covered : Length_Type; begin Covered := Distance (Secs, Speed); declare subtype Area is Unit_Type with dimension => (Meter => 2, others => 0); My_Little_Acre : Area; function Acres is new I (Length_Type, Length_Type, Area); begin My_Little_Acre := Covered * Covered; My_Little_Acre := Acres (Covered, Covered); end; end Integrate; Tested on x86_64-pc-linux-gnu, committed on trunk 2017-09-06 Ed Schonberg * sem_dim.adb (Analyze_Dimension): In an instance, a type conversion takes its dimensions from the expression, not from the context type. (Dimensions_Of_Operand): Ditto. Index: sem_dim.adb =================================================================== --- sem_dim.adb (revision 251753) +++ sem_dim.adb (working copy) @@ -1161,7 +1161,6 @@ | N_Qualified_Expression | N_Selected_Component | N_Slice - | N_Type_Conversion | N_Unchecked_Type_Conversion => Analyze_Dimension_Has_Etype (N); @@ -1191,7 +1190,17 @@ when N_Subtype_Declaration => Analyze_Dimension_Subtype_Declaration (N); + when N_Type_Conversion => + if In_Instance + and then Exists (Dimensions_Of (Expression (N))) + then + Set_Dimensions (N, Dimensions_Of (Expression (N))); + else + Analyze_Dimension_Has_Etype (N); + end if; + when N_Unary_Op => + Analyze_Dimension_Unary_Op (N); when others => @@ -1378,11 +1387,24 @@ -- A type conversion may have been inserted to rewrite other -- expressions, e.g. function returns. Dimensions are those of - -- the target type. + -- the target type, unless this is a conversion in an instance, + -- in which case the proper dimensions are those of the operand, elsif Nkind (N) = N_Type_Conversion then - return Dimensions_Of (Etype (N)); + if In_Instance + and then Is_Generic_Actual_Type (Etype (Expression (N))) + then + return Dimensions_Of (Etype (Expression (N))); + elsif In_Instance + and then Exists (Dimensions_Of (Expression (N))) + then + return Dimensions_Of (Expression (N)); + + else + return Dimensions_Of (Etype (N)); + end if; + -- Otherwise return the default dimensions else