From patchwork Tue Jan 11 13:32:05 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 49847 Return-Path: X-Original-To: patchwork@sourceware.org Delivered-To: patchwork@sourceware.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 159EF38A9412 for ; Tue, 11 Jan 2022 13:48:17 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 159EF38A9412 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1641908897; bh=u5SGSLAfk8EaKftMqwlhhpSl1Dy4aBZDX+RP1GbTFmc=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=EWHeC0ksFhKV02Pi/PwByj/Bka7uyUfW+9mKpmK+rG9+jxhy3z9CBGc+hMs2C5Wf2 X8IqHx0V/eHKwZRuqalQM4ILpcyK2FyXi1IsvuSdaYu3X5wenCZUm7B4tvENrckT88 mC1Mmty3Q+M0l+WWtGeRwOYJLAiJ0kzVSIT1QUto= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x433.google.com (mail-wr1-x433.google.com [IPv6:2a00:1450:4864:20::433]) by sourceware.org (Postfix) with ESMTPS id 4700938AAC19 for ; Tue, 11 Jan 2022 13:32:08 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 4700938AAC19 Received: by mail-wr1-x433.google.com with SMTP id q8so32889358wra.12 for ; Tue, 11 Jan 2022 05:32:08 -0800 (PST) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=u5SGSLAfk8EaKftMqwlhhpSl1Dy4aBZDX+RP1GbTFmc=; b=1pxQ95hfmQI5L8pCbg1vtAfjelem58MTCgOt9ArABEVeXBFrfKSGyMFExYX2B+0uyt fvZzHO8phwg/YT5XkFPaueAY0EVkdRhW7bDEGKa/j+H/wSon4c1wofQQWtbhPSX2EPtx /5KjosF2vtuS8UTJRQ5vmk+Q5CAG8pWtqvnsKgBSHQtWOLW8FObEDL53s4nP81Iuml2Y DEO3e+EzzfDgg/utCVZ27eEWP5r7wW4n1+r4iG/ucdSrhdEnqql24bl9Dg+t1QFJvOZv jhaK4W1lkOh7MkduuOp2t62hqEjNpRw/r7b+HUWhriGm5q81dBrrYcb8KbZICeNb/KZD hBgQ== X-Gm-Message-State: AOAM533e0lgOKZANNEsZ0xgMDmFFJAV+yR8dXDo5XHHMVhAGfzkR6Jl5 fJugdUNpyiqMTKsn5mScIigZFLWEZAnM6Q== X-Google-Smtp-Source: ABdhPJx1LarI+qsGtrwTGA8pPCWKiZF4ZTxCSu/rehC4+bK4SbpqXQGvsZmfc7+b+CqwnvWWRLWR4w== X-Received: by 2002:adf:d1e9:: with SMTP id g9mr3917112wrd.238.1641907927327; Tue, 11 Jan 2022 05:32:07 -0800 (PST) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id g15sm8518193wrm.2.2022.01.11.05.32.06 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 11 Jan 2022 05:32:06 -0800 (PST) Date: Tue, 11 Jan 2022 13:32:05 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Proof of System.Vectors.Boolean_Operations Message-ID: <20220111133205.GA748595@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-13.1 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, WEIRD_QUOTING autolearn=ham autolearn_force=no version=3.4.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Yannick Moy Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" This proves in SPARK the unit System.Vectors.Boolean_Operations. The specification models explicitly the array of Boolean represented by Vectors.Vector, so that the result of functions can be specified by expressing the relationship between input and output models. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-veboop.adb: Add ghost code for proof. * libgnat/s-veboop.ads: Add specification. diff --git a/gcc/ada/libgnat/s-veboop.adb b/gcc/ada/libgnat/s-veboop.adb --- a/gcc/ada/libgnat/s-veboop.adb +++ b/gcc/ada/libgnat/s-veboop.adb @@ -29,7 +29,17 @@ -- -- ------------------------------------------------------------------------------ -package body System.Vectors.Boolean_Operations is +-- Ghost code, loop invariants and assertions in this unit are meant for +-- analysis only, not for run-time checking, as it would be too costly +-- otherwise. This is enforced by setting the assertion policy to Ignore. + +pragma Assertion_Policy (Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); + +package body System.Vectors.Boolean_Operations + with SPARK_Mode +is SU : constant := Storage_Unit; -- Convenient short hand, used throughout @@ -76,7 +86,26 @@ package body System.Vectors.Boolean_Operations is ----------- function "not" (Item : Vectors.Vector) return Vectors.Vector is + + procedure Prove_Not (Result : Vectors.Vector) + with + Ghost, + Pre => Valid (Item) + and then Result = (Item xor True_Val), + Post => Valid (Result) + and then (for all J in 1 .. Vector_Boolean_Size => + Model (Result) (J) = not Model (Item) (J)); + + procedure Prove_Not (Result : Vectors.Vector) is + begin + for J in 1 .. Vector_Boolean_Size loop + pragma Assert + (Element (Result, J) = 1 - Element (Item, J)); + end loop; + end Prove_Not; + begin + Prove_Not (Item xor True_Val); return Item xor True_Val; end "not"; @@ -90,7 +119,32 @@ package body System.Vectors.Boolean_Operations is end Nand; function Nand (Left, Right : Vectors.Vector) return Vectors.Vector is + + procedure Prove_And (Result : Vectors.Vector) + with + Ghost, + Pre => Valid (Left) + and then Valid (Right) + and then Result = (Left and Right), + Post => Valid (Result) + and then (for all J in 1 .. Vector_Boolean_Size => + Model (Result) (J) = + (Model (Left) (J) and Model (Right) (J))); + + procedure Prove_And (Result : Vectors.Vector) is + begin + for J in 1 .. Vector_Boolean_Size loop + pragma Assert + (Element (Result, J) = + (if Element (Left, J) = 1 + and Element (Right, J) = 1 + then 1 + else 0)); + end loop; + end Prove_And; + begin + Prove_And (Left and Right); return not (Left and Right); end Nand; @@ -104,7 +158,32 @@ package body System.Vectors.Boolean_Operations is end Nor; function Nor (Left, Right : Vectors.Vector) return Vectors.Vector is + + procedure Prove_Or (Result : Vectors.Vector) + with + Ghost, + Pre => Valid (Left) + and then Valid (Right) + and then Result = (Left or Right), + Post => Valid (Result) + and then (for all J in 1 .. Vector_Boolean_Size => + Model (Result) (J) = + (Model (Left) (J) or Model (Right) (J))); + + procedure Prove_Or (Result : Vectors.Vector) is + begin + for J in 1 .. Vector_Boolean_Size loop + pragma Assert + (Element (Result, J) = + (if Element (Left, J) = 1 + or Element (Right, J) = 1 + then 1 + else 0)); + end loop; + end Prove_Or; + begin + Prove_Or (Left or Right); return not (Left or Right); end Nor; @@ -118,7 +197,32 @@ package body System.Vectors.Boolean_Operations is end Nxor; function Nxor (Left, Right : Vectors.Vector) return Vectors.Vector is + + procedure Prove_Xor (Result : Vectors.Vector) + with + Ghost, + Pre => Valid (Left) + and then Valid (Right) + and then Result = (Left xor Right), + Post => Valid (Result) + and then (for all J in 1 .. Vector_Boolean_Size => + Model (Result) (J) = + (Model (Left) (J) xor Model (Right) (J))); + + procedure Prove_Xor (Result : Vectors.Vector) is + begin + for J in 1 .. Vector_Boolean_Size loop + pragma Assert + (Element (Result, J) = + (if Element (Left, J) = 1 + xor Element (Right, J) = 1 + then 1 + else 0)); + end loop; + end Prove_Xor; + begin + Prove_Xor (Left xor Right); return not (Left xor Right); end Nxor; diff --git a/gcc/ada/libgnat/s-veboop.ads b/gcc/ada/libgnat/s-veboop.ads --- a/gcc/ada/libgnat/s-veboop.ads +++ b/gcc/ada/libgnat/s-veboop.ads @@ -31,15 +31,77 @@ -- This package contains functions for runtime operations on boolean vectors -package System.Vectors.Boolean_Operations is - pragma Pure; +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced by +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore); + +package System.Vectors.Boolean_Operations + with Pure, SPARK_Mode +is + pragma Warnings (Off, "aspect ""Pre"" not enforced on inlined subprogram", + Reason => "Pre only used in proof"); + pragma Warnings (Off, "aspect ""Post"" not enforced on inlined subprogram", + Reason => "Post only used in proof"); + + -- Type Vectors.Vector represents an array of Boolean, each of which + -- takes 8 bits of the representation, with the 7 msb set to zero. Express + -- in contracts the constraint on valid vectors and the model that they + -- represent, and the relationship between input models and output model. + + Vector_Boolean_Size : constant Positive := + System.Word_Size / System.Storage_Unit + with Ghost; + + type Vector_Element is mod 2 ** System.Storage_Unit with Ghost; + + type Vector_Boolean_Array is array (1 .. Vector_Boolean_Size) of Boolean + with Ghost; + + function Shift_Right (V : Vectors.Vector; N : Natural) return Vectors.Vector + with Ghost, Import, Convention => Intrinsic; + + function Element (V : Vectors.Vector; N : Positive) return Vector_Element is + (Vector_Element (Shift_Right (V, (N - 1) * System.Storage_Unit) + and (2 ** System.Storage_Unit - 1))) + with + Ghost, + Pre => N <= Vector_Boolean_Size; + -- Return the Nth element represented by the vector + + function Valid (V : Vectors.Vector) return Boolean is + (for all J in 1 .. Vector_Boolean_Size => + Element (V, J) in 0 .. 1) + with Ghost; + -- A valid vector is one for which all elements are 0 (representing False) + -- or 1 (representing True). + + function Model (V : Vectors.Vector) return Vector_Boolean_Array + with + Ghost, + Pre => Valid (V); + + function Model (V : Vectors.Vector) return Vector_Boolean_Array is + (for J in 1 .. Vector_Boolean_Size => Element (V, J) = 1); + -- The model of a valid vector is the corresponding array of Boolean values -- Although in general the boolean operations on arrays of booleans are -- identical to operations on arrays of unsigned words of the same size, -- for the "not" operator this is not the case as False is typically -- represented by 0 and true by 1. - function "not" (Item : Vectors.Vector) return Vectors.Vector; + function "not" (Item : Vectors.Vector) return Vectors.Vector + with + Pre => Valid (Item), + Post => Valid ("not"'Result) + and then (for all J in 1 .. Vector_Boolean_Size => + Model ("not"'Result) (J) = not Model (Item) (J)); -- The three boolean operations "nand", "nor" and "nxor" are needed -- for cases where the compiler moves boolean array operations into @@ -51,13 +113,44 @@ package System.Vectors.Boolean_Operations is -- (not X) xor (not Y) = X xor Y -- X xor (not Y) = not (X xor Y) = Nxor (X, Y) - function Nand (Left, Right : Boolean) return Boolean; - function Nor (Left, Right : Boolean) return Boolean; - function Nxor (Left, Right : Boolean) return Boolean; + function Nand (Left, Right : Boolean) return Boolean + with + Post => Nand'Result = not (Left and Right); + + function Nor (Left, Right : Boolean) return Boolean + with + Post => Nor'Result = not (Left or Right); + + function Nxor (Left, Right : Boolean) return Boolean + with + Post => Nxor'Result = not (Left xor Right); + + function Nand (Left, Right : Vectors.Vector) return Vectors.Vector + with + Pre => Valid (Left) + and then Valid (Right), + Post => Valid (Nand'Result) + and then (for all J in 1 .. Vector_Boolean_Size => + Model (Nand'Result) (J) = + Nand (Model (Left) (J), Model (Right) (J))); + + function Nor (Left, Right : Vectors.Vector) return Vectors.Vector + with + Pre => Valid (Left) + and then Valid (Right), + Post => Valid (Nor'Result) + and then (for all J in 1 .. Vector_Boolean_Size => + Model (Nor'Result) (J) = + Nor (Model (Left) (J), Model (Right) (J))); - function Nand (Left, Right : Vectors.Vector) return Vectors.Vector; - function Nor (Left, Right : Vectors.Vector) return Vectors.Vector; - function Nxor (Left, Right : Vectors.Vector) return Vectors.Vector; + function Nxor (Left, Right : Vectors.Vector) return Vectors.Vector + with + Pre => Valid (Left) + and then Valid (Right), + Post => Valid (Nxor'Result) + and then (for all J in 1 .. Vector_Boolean_Size => + Model (Nxor'Result) (J) = + Nxor (Model (Left) (J), Model (Right) (J))); pragma Inline_Always ("not"); pragma Inline_Always (Nand);