gcc/ada/libgnat/a-strmap.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                     A D A . S T R I N G S . M A P S                      --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --          Copyright (C) 1992-2023, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  17 --                                                                          --
  18 -- As a special exception under Section 7 of GPL version 3, you are granted --
  19 -- additional permissions described in the GCC Runtime Library Exception,   --
  20 -- version 3.1, as published by the Free Software Foundation.               --
  21 --                                                                          --
  22 -- You should have received a copy of the GNU General Public License and    --
  23 -- a copy of the GCC Runtime Library Exception along with this program;     --
  24 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  25 -- <http://www.gnu.org/licenses/>.                                          --
  26 --                                                                          --
  27 -- GNAT was originally developed  by the GNAT team at  New York University. --
  28 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  29 --                                                                          --
  30 ------------------------------------------------------------------------------
  31
  32 --  Note: parts of this code are derived from the ADAR.CSH public domain
  33 --  Ada 83 versions of the Appendix C string handling packages. The main
  34 --  differences are that we avoid the use of the minimize function which
  35 --  is bit-by-bit or character-by-character and therefore rather slow.
  36 --  Generally for character sets we favor the full 32-byte representation.
  37
  38 --  Assertions, ghost code and loop invariants in this unit are meant for
  39 --  analysis only, not for run-time checking, as it would be too costly
  40 --  otherwise. This is enforced by setting the assertion policy to Ignore.
  41
  42 pragma Assertion_Policy (Assert         => Ignore,
  43                          Ghost          => Ignore,
  44                          Loop_Invariant => Ignore);
  45
  46 package body Ada.Strings.Maps
  47   with SPARK_Mode
  48 is
  49
  50    ---------
  51    -- "-" --
  52    ---------
  53
  54    function "-" (Left, Right : Character_Set) return Character_Set is
  55    begin
  56       return Left and not Right;
  57    end "-";
  58
  59    ---------
  60    -- "=" --
  61    ---------
  62
  63    function "=" (Left, Right : Character_Set) return Boolean is
  64    begin
  65       return Character_Set_Internal (Left) = Character_Set_Internal (Right);
  66    end "=";
  67
  68    -----------
  69    -- "and" --
  70    -----------
  71
  72    function "and" (Left, Right : Character_Set) return Character_Set is
  73    begin
  74       return Character_Set
  75         (Character_Set_Internal (Left) and Character_Set_Internal (Right));
  76    end "and";
  77
  78    -----------
  79    -- "not" --
  80    -----------
  81
  82    function "not" (Right : Character_Set) return Character_Set is
  83    begin
  84       return Character_Set (not Character_Set_Internal (Right));
  85    end "not";
  86
  87    ----------
  88    -- "or" --
  89    ----------
  90
  91    function "or" (Left, Right : Character_Set) return Character_Set is
  92    begin
  93       return Character_Set
  94         (Character_Set_Internal (Left) or Character_Set_Internal (Right));
  95    end "or";
  96
  97    -----------
  98    -- "xor" --
  99    -----------
 100
 101    function "xor" (Left, Right : Character_Set) return Character_Set is
 102    begin
 103       return Character_Set
 104         (Character_Set_Internal (Left) xor Character_Set_Internal (Right));
 105    end "xor";
 106
 107    -----------
 108    -- Is_In --
 109    -----------
 110
 111    function Is_In
 112      (Element : Character;
 113       Set     : Character_Set) return Boolean
 114    is
 115       (Set (Element));
 116
 117    ---------------
 118    -- Is_Subset --
 119    ---------------
 120
 121    function Is_Subset
 122      (Elements : Character_Set;
 123       Set      : Character_Set) return Boolean
 124    is
 125    begin
 126       return (Elements and Set) = Elements;
 127    end Is_Subset;
 128
 129    ---------------
 130    -- To_Domain --
 131    ---------------
 132
 133    function To_Domain (Map : Character_Mapping) return Character_Sequence is
 134       Result : String (1 .. Map'Length) with Relaxed_Initialization;
 135       J      : Natural;
 136
 137       type Character_Index is array (Character) of Natural with Ghost;
 138       Indexes : Character_Index := [others => 0] with Ghost;
 139
 140    begin
 141       J := 0;
 142       for C in Map'Range loop
 143          if Map (C) /= C then
 144             J := J + 1;
 145             Result (J) := C;
 146             Indexes (C) := J;
 147          end if;
 148
 149          pragma Loop_Invariant (if Map = Identity then J = 0);
 150          pragma Loop_Invariant (J <= Character'Pos (C) + 1);
 151          pragma Loop_Invariant (Result (1 .. J)'Initialized);
 152          pragma Loop_Invariant (for all K in 1 .. J => Result (K) <= C);
 153          pragma Loop_Invariant
 154            (SPARK_Proof_Sorted_Character_Sequence (Result (1 .. J)));
 155          pragma Loop_Invariant
 156            (for all D in Map'First .. C =>
 157               (if Map (D) = D then
 158                  Indexes (D) = 0
 159                else
 160                  Indexes (D) in 1 .. J
 161                    and then Result (Indexes (D)) = D));
 162          pragma Loop_Invariant
 163            (for all Char of Result (1 .. J) => Map (Char) /= Char);
 164       end loop;
 165
 166       return Result (1 .. J);
 167    end To_Domain;
 168
 169    ----------------
 170    -- To_Mapping --
 171    ----------------
 172
 173    function To_Mapping
 174      (From, To : Character_Sequence) return Character_Mapping
 175    is
 176       Result   : Character_Mapping with Relaxed_Initialization;
 177       Inserted : Character_Set := Null_Set;
 178       From_Len : constant Natural := From'Length;
 179       To_Len   : constant Natural := To'Length;
 180
 181    begin
 182       if From_Len /= To_Len then
 183          raise Strings.Translation_Error;
 184       end if;
 185
 186       for Char in Character loop
 187          Result (Char) := Char;
 188          pragma Loop_Invariant (Result (Result'First .. Char)'Initialized);
 189          pragma Loop_Invariant
 190            (for all C in Result'First .. Char => Result (C) = C);
 191       end loop;
 192
 193       for J in From'Range loop
 194          if Inserted (From (J)) then
 195             raise Strings.Translation_Error;
 196          end if;
 197
 198          Result   (From (J)) := To (J - From'First + To'First);
 199          Inserted (From (J)) := True;
 200
 201          pragma Loop_Invariant (Result'Initialized);
 202          pragma Loop_Invariant
 203            (for all K in From'First .. J =>
 204               Result (From (K)) = To (K - From'First + To'First)
 205                 and then Inserted (From (K)));
 206          pragma Loop_Invariant
 207            (for all Char in Character =>
 208               (Inserted (Char) =
 209                  (for some K in From'First .. J => Char = From (K))));
 210          pragma Loop_Invariant
 211            (for all Char in Character =>
 212               (if not Inserted (Char) then Result (Char) = Char));
 213          pragma Loop_Invariant
 214            (if (for all K in From'First .. J =>
 215                   From (K) = To (J - From'First + To'First))
 216             then Result = Identity);
 217       end loop;
 218
 219       return Result;
 220    end To_Mapping;
 221
 222    --------------
 223    -- To_Range --
 224    --------------
 225
 226    function To_Range (Map : Character_Mapping) return Character_Sequence is
 227
 228       --  Extract from the postcondition of To_Domain the essential properties
 229       --  that define Seq as the domain of Map.
 230       function Is_Domain
 231         (Map : Character_Mapping;
 232          Seq : Character_Sequence)
 233          return Boolean
 234       is
 235         (Seq'First = 1
 236            and then
 237          SPARK_Proof_Sorted_Character_Sequence (Seq)
 238            and then
 239          (for all Char in Character =>
 240             (if (for all X of Seq => X /= Char)
 241              then Map (Char) = Char))
 242            and then
 243          (for all Char of Seq => Map (Char) /= Char))
 244       with
 245         Ghost;
 246
 247       --  Given Map, there is a unique sequence Seq for which
 248       --  Is_Domain(Map,Seq) holds.
 249       procedure Lemma_Domain_Unicity
 250         (Map        : Character_Mapping;
 251          Seq1, Seq2 : Character_Sequence)
 252       with
 253         Ghost,
 254         Pre  => Is_Domain (Map, Seq1)
 255           and then Is_Domain (Map, Seq2),
 256         Post => Seq1 = Seq2;
 257
 258       --  Isolate the proof that To_Domain(Map) returns a sequence for which
 259       --  Is_Domain holds.
 260       procedure Lemma_Is_Domain (Map : Character_Mapping)
 261       with
 262         Ghost,
 263         Post => Is_Domain (Map, To_Domain (Map));
 264
 265       --  Deduce the alternative expression of sortedness from the one in
 266       --  SPARK_Proof_Sorted_Character_Sequence which compares consecutive
 267       --  elements.
 268       procedure Lemma_Is_Sorted (Seq : Character_Sequence)
 269       with
 270         Ghost,
 271         Pre  => SPARK_Proof_Sorted_Character_Sequence (Seq),
 272         Post => (for all J in Seq'Range =>
 273                    (for all K in Seq'Range =>
 274                       (if J < K then Seq (J) < Seq (K))));
 275
 276       --------------------------
 277       -- Lemma_Domain_Unicity --
 278       --------------------------
 279
 280       procedure Lemma_Domain_Unicity
 281         (Map        : Character_Mapping;
 282          Seq1, Seq2 : Character_Sequence)
 283       is
 284          J : Positive := 1;
 285
 286       begin
 287          while J <= Seq1'Last
 288            and then J <= Seq2'Last
 289            and then Seq1 (J) = Seq2 (J)
 290          loop
 291             pragma Loop_Invariant
 292               (Seq1 (Seq1'First .. J) = Seq2 (Seq2'First .. J));
 293             pragma Loop_Variant (Increases => J);
 294
 295             if J = Positive'Last then
 296                return;
 297             end if;
 298
 299             J := J + 1;
 300          end loop;
 301
 302          Lemma_Is_Sorted (Seq1);
 303          Lemma_Is_Sorted (Seq2);
 304
 305          if J <= Seq1'Last
 306            and then J <= Seq2'Last
 307          then
 308             if Seq1 (J) < Seq2 (J) then
 309                pragma Assert (for all X of Seq2 => X /= Seq1 (J));
 310                pragma Assert (Map (Seq1 (J)) = Seq1 (J));
 311                pragma Assert (False);
 312             else
 313                pragma Assert (for all X of Seq1 => X /= Seq2 (J));
 314                pragma Assert (Map (Seq2 (J)) = Seq2 (J));
 315                pragma Assert (False);
 316             end if;
 317
 318          elsif J <= Seq1'Last then
 319             pragma Assert (for all X of Seq2 => X /= Seq1 (J));
 320             pragma Assert (Map (Seq1 (J)) = Seq1 (J));
 321             pragma Assert (False);
 322
 323          elsif J <= Seq2'Last then
 324             pragma Assert (for all X of Seq1 => X /= Seq2 (J));
 325             pragma Assert (Map (Seq2 (J)) = Seq2 (J));
 326             pragma Assert (False);
 327          end if;
 328       end Lemma_Domain_Unicity;
 329
 330       ---------------------
 331       -- Lemma_Is_Domain --
 332       ---------------------
 333
 334       procedure Lemma_Is_Domain (Map : Character_Mapping) is
 335          Ignore : constant Character_Sequence := To_Domain (Map);
 336       begin
 337          null;
 338       end Lemma_Is_Domain;
 339
 340       ---------------------
 341       -- Lemma_Is_Sorted --
 342       ---------------------
 343
 344       procedure Lemma_Is_Sorted (Seq : Character_Sequence) is
 345       begin
 346          for A in Seq'Range loop
 347             exit when A = Positive'Last;
 348
 349             for B in A + 1 .. Seq'Last loop
 350                pragma Loop_Invariant
 351                  (for all K in A + 1 .. B => Seq (A) < Seq (K));
 352             end loop;
 353
 354             pragma Loop_Invariant
 355               (for all J in Seq'First .. A =>
 356                  (for all K in Seq'Range =>
 357                     (if J < K then Seq (J) < Seq (K))));
 358          end loop;
 359       end Lemma_Is_Sorted;
 360
 361       --  Local variables
 362
 363       Result : String (1 .. Map'Length) with Relaxed_Initialization;
 364       J      : Natural;
 365
 366       --  Repeat the computation from To_Domain in ghost code, in order to
 367       --  prove the relationship between Result and To_Domain(Map).
 368
 369       Domain : String (1 .. Map'Length) with Ghost, Relaxed_Initialization;
 370       type Character_Index is array (Character) of Natural with Ghost;
 371       Indexes : Character_Index := [others => 0] with Ghost;
 372
 373    --  Start of processing for To_Range
 374
 375    begin
 376       J := 0;
 377       for C in Map'Range loop
 378          if Map (C) /= C then
 379             J := J + 1;
 380             Result (J) := Map (C);
 381             Domain (J) := C;
 382             Indexes (C) := J;
 383          end if;
 384
 385          --  Repeat the loop invariants from To_Domain regarding Domain and
 386          --  Indexes. Add similar loop invariants for Result and Indexes.
 387
 388          pragma Loop_Invariant (J <= Character'Pos (C) + 1);
 389          pragma Loop_Invariant (Result (1 .. J)'Initialized);
 390          pragma Loop_Invariant (Domain (1 .. J)'Initialized);
 391          pragma Loop_Invariant (for all K in 1 .. J => Domain (K) <= C);
 392          pragma Loop_Invariant
 393            (SPARK_Proof_Sorted_Character_Sequence (Domain (1 .. J)));
 394          pragma Loop_Invariant
 395            (for all D in Map'First .. C =>
 396               (if Map (D) = D then
 397                  Indexes (D) = 0
 398                else
 399                  Indexes (D) in 1 .. J
 400                    and then Domain (Indexes (D)) = D
 401                    and then Result (Indexes (D)) = Map (D)));
 402          pragma Loop_Invariant
 403            (for all Char of Domain (1 .. J) => Map (Char) /= Char);
 404          pragma Loop_Invariant
 405            (for all K in 1 .. J => Result (K) = Map (Domain (K)));
 406       end loop;
 407
 408       --  Show the equality of Domain and To_Domain(Map)
 409
 410       Lemma_Is_Domain (Map);
 411       Lemma_Domain_Unicity (Map, Domain (1 .. J), To_Domain (Map));
 412       pragma Assert
 413         (for all K in 1 .. J => Domain (K) = To_Domain (Map) (K));
 414       pragma Assert (To_Domain (Map)'Length = J);
 415
 416       return Result (1 .. J);
 417    end To_Range;
 418
 419    ---------------
 420    -- To_Ranges --
 421    ---------------
 422
 423    function To_Ranges (Set : Character_Set) return Character_Ranges is
 424       Max_Ranges : Character_Ranges (1 .. Set'Length / 2 + 1)
 425         with Relaxed_Initialization;
 426       Range_Num  : Natural;
 427       C          : Character;
 428       C_Iter     : Character with Ghost;
 429
 430    begin
 431       C := Character'First;
 432       Range_Num := 0;
 433
 434       loop
 435          C_Iter := C;
 436
 437          --  Skip gap between subsets
 438
 439          while not Set (C) loop
 440             pragma Loop_Invariant
 441               (Character'Pos (C) >= Character'Pos (C'Loop_Entry));
 442             pragma Loop_Invariant
 443               (for all Char in C'Loop_Entry .. C => not Set (Char));
 444             pragma Loop_Variant (Increases => C);
 445             exit when C = Character'Last;
 446             C := Character'Succ (C);
 447          end loop;
 448
 449          exit when not Set (C);
 450
 451          Range_Num := Range_Num + 1;
 452          Max_Ranges (Range_Num).Low := C;
 453
 454          --  Span a subset
 455
 456          loop
 457             pragma Loop_Invariant
 458               (Character'Pos (C) >= Character'Pos (C'Loop_Entry));
 459             pragma Loop_Invariant
 460               (for all Char in C'Loop_Entry .. C =>
 461                  (if Char /= C then Set (Char)));
 462             pragma Loop_Variant (Increases => C);
 463             exit when not Set (C) or else C = Character'Last;
 464             C := Character'Succ (C);
 465          end loop;
 466
 467          if Set (C) then
 468             Max_Ranges (Range_Num).High := C;
 469             exit;
 470          else
 471             Max_Ranges (Range_Num).High := Character'Pred (C);
 472          end if;
 473
 474          pragma Assert
 475            (for all Char in C_Iter .. C =>
 476               (Set (Char) =
 477                  (Char in Max_Ranges (Range_Num).Low ..
 478                           Max_Ranges (Range_Num).High)));
 479          pragma Assert
 480            (for all Char in Character'First .. C_Iter =>
 481               (if Char /= C_Iter then
 482                  (Set (Char) =
 483                     (for some Span of Max_Ranges (1 .. Range_Num - 1) =>
 484                        Char in Span.Low .. Span.High))));
 485
 486          pragma Loop_Invariant (2 * Range_Num <= Character'Pos (C) + 1);
 487          pragma Loop_Invariant (Max_Ranges (1 .. Range_Num)'Initialized);
 488          pragma Loop_Invariant (not Set (C));
 489          pragma Loop_Invariant
 490            (for all Char in Character'First .. C =>
 491               (Set (Char) =
 492                  (for some Span of Max_Ranges (1 .. Range_Num) =>
 493                     Char in Span.Low .. Span.High)));
 494          pragma Loop_Invariant
 495            (for all Span of Max_Ranges (1 .. Range_Num) =>
 496               (for all Char in Span.Low .. Span.High => Set (Char)));
 497          pragma Loop_Variant (Increases => Range_Num);
 498       end loop;
 499
 500       return Max_Ranges (1 .. Range_Num);
 501    end To_Ranges;
 502
 503    -----------------
 504    -- To_Sequence --
 505    -----------------
 506
 507    function To_Sequence (Set : Character_Set) return Character_Sequence is
 508       Result : String (1 .. Character'Pos (Character'Last) + 1)
 509         with Relaxed_Initialization;
 510       Count  : Natural := 0;
 511    begin
 512       for Char in Set'Range loop
 513          if Set (Char) then
 514             Count := Count + 1;
 515             Result (Count) := Char;
 516          end if;
 517
 518          pragma Loop_Invariant (Count <= Character'Pos (Char) + 1);
 519          pragma Loop_Invariant (Result (1 .. Count)'Initialized);
 520          pragma Loop_Invariant (for all K in 1 .. Count => Result (K) <= Char);
 521          pragma Loop_Invariant
 522            (SPARK_Proof_Sorted_Character_Sequence (Result (1 .. Count)));
 523          pragma Loop_Invariant
 524            (for all C in Set'First .. Char =>
 525               (Set (C) = (for some X of Result (1 .. Count) => C = X)));
 526          pragma Loop_Invariant
 527            (for all Char of Result (1 .. Count) => Is_In (Char, Set));
 528       end loop;
 529
 530       return Result (1 .. Count);
 531    end To_Sequence;
 532
 533    ------------
 534    -- To_Set --
 535    ------------
 536
 537    function To_Set (Ranges : Character_Ranges) return Character_Set is
 538       Result : Character_Set := Null_Set;
 539    begin
 540       for R in Ranges'Range loop
 541          for C in Ranges (R).Low .. Ranges (R).High loop
 542             Result (C) := True;
 543             pragma Loop_Invariant
 544               (for all Char in Character =>
 545                  Result (Char) =
 546                    ((for some Prev in Ranges'First .. R - 1 =>
 547                        Char in Ranges (Prev).Low .. Ranges (Prev).High)
 548                     or else Char in Ranges (R).Low .. C));
 549          end loop;
 550
 551          pragma Loop_Invariant
 552            (for all Char in Character =>
 553               Result (Char) =
 554                 (for some Prev in Ranges'First .. R =>
 555                    Char in Ranges (Prev).Low .. Ranges (Prev).High));
 556       end loop;
 557
 558       return Result;
 559    end To_Set;
 560
 561    function To_Set (Span : Character_Range) return Character_Set is
 562       Result : Character_Set := Null_Set;
 563    begin
 564       for C in Span.Low .. Span.High loop
 565          Result (C) := True;
 566          pragma Loop_Invariant
 567            (for all Char in Character =>
 568               Result (Char) = (Char in Span.Low .. C));
 569       end loop;
 570
 571       return Result;
 572    end To_Set;
 573
 574    function To_Set (Sequence : Character_Sequence) return Character_Set is
 575       Result : Character_Set := Null_Set;
 576    begin
 577       for J in Sequence'Range loop
 578          Result (Sequence (J)) := True;
 579          pragma Loop_Invariant
 580            (for all Char in Character =>
 581               Result (Char) =
 582                 (for some K in Sequence'First .. J => Char = Sequence (K)));
 583       end loop;
 584
 585       return Result;
 586    end To_Set;
 587
 588    function To_Set (Singleton : Character) return Character_Set is
 589       Result : Character_Set := Null_Set;
 590    begin
 591       Result (Singleton) := True;
 592       return Result;
 593    end To_Set;
 594
 595    -----------
 596    -- Value --
 597    -----------
 598
 599    function Value
 600      (Map     : Character_Mapping;
 601       Element : Character) return Character
 602    is
 603       (Map (Element));
 604
 605 end Ada.Strings.Maps;