gcc/ada/libgnat/a-strsea.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                   A D A . S T R I N G S . S E A R C H                    --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --          Copyright (C) 1992-2024, 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: This code is derived from the ADAR.CSH public domain Ada 83
  33 --  versions of the Appendix C string handling packages (code extracted
  34 --  from Ada.Strings.Fixed). A significant change is that we optimize the
  35 --  case of identity mappings for Count and Index, and also Index_Non_Blank
  36 --  is specialized (rather than using the general Index routine).
  37
  38 --  Ghost code, loop invariants and assertions 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 (Ghost          => Ignore,
  43                          Loop_Invariant => Ignore,
  44                          Assert         => Ignore);
  45
  46 with Ada.Strings.Maps; use Ada.Strings.Maps;
  47 with System;           use System;
  48
  49 package body Ada.Strings.Search with SPARK_Mode is
  50
  51    -----------------------
  52    -- Local Subprograms --
  53    -----------------------
  54
  55    function Belongs
  56      (Element : Character;
  57       Set     : Maps.Character_Set;
  58       Test    : Membership) return Boolean;
  59    pragma Inline (Belongs);
  60    --  Determines if the given element is in (Test = Inside) or not in
  61    --  (Test = Outside) the given character set.
  62
  63    -------------
  64    -- Belongs --
  65    -------------
  66
  67    function Belongs
  68      (Element : Character;
  69       Set     : Maps.Character_Set;
  70       Test    : Membership) return Boolean
  71    is
  72       (if Test = Inside then
  73           Is_In (Element, Set)
  74       else not (Is_In (Element, Set)));
  75
  76    -----------
  77    -- Count --
  78    -----------
  79
  80    function Count
  81      (Source  : String;
  82       Pattern : String;
  83       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
  84    is
  85       PL1 : constant Integer := Pattern'Length - 1;
  86       Num : Natural;
  87       Ind : Natural;
  88
  89    begin
  90       if Pattern = "" then
  91          raise Pattern_Error;
  92       end if;
  93
  94       --  Isolating the null string case to ensure Source'First, Source'Last in
  95       --  Positive.
  96
  97       if Source = "" then
  98          return 0;
  99       end if;
 100
 101       Num := 0;
 102       Ind := Source'First - 1;
 103
 104       --  Unmapped case
 105
 106       if Is_Identity (Mapping) then
 107          while Ind < Source'Last - PL1 loop
 108             Ind := Ind + 1;
 109             if Pattern = Source (Ind .. Ind + PL1) then
 110                Num := Num + 1;
 111                Ind := Ind + PL1;
 112             end if;
 113
 114             pragma Loop_Invariant (Num <= Ind - (Source'First - 1));
 115             pragma Loop_Invariant (Ind >= Source'First);
 116             pragma Loop_Variant (Increases => Ind);
 117          end loop;
 118
 119       --  Mapped case
 120
 121       else
 122          while Ind < Source'Last - PL1 loop
 123             Ind := Ind + 1;
 124             for K in Pattern'Range loop
 125                if Pattern (K) /= Value (Mapping,
 126                  Source (Ind + (K - Pattern'First)))
 127                then
 128                   pragma Assert (not (Match (Source, Pattern, Mapping, Ind)));
 129                   goto Cont;
 130                end if;
 131
 132                pragma Loop_Invariant
 133                  (for all J in Pattern'First .. K =>
 134                     Pattern (J) = Value (Mapping,
 135                       Source (Ind + (J - Pattern'First))));
 136             end loop;
 137
 138             pragma Assert (Match (Source, Pattern, Mapping, Ind));
 139             Num := Num + 1;
 140             Ind := Ind + PL1;
 141
 142             <<Cont>>
 143             null;
 144             pragma Loop_Invariant (Num <= Ind - (Source'First - 1));
 145             pragma Loop_Invariant (Ind >= Source'First);
 146             pragma Loop_Variant (Increases => Ind);
 147          end loop;
 148       end if;
 149
 150       --  Return result
 151
 152       return Num;
 153    end Count;
 154
 155    function Count
 156      (Source  : String;
 157       Pattern : String;
 158       Mapping : Maps.Character_Mapping_Function) return Natural
 159    is
 160       PL1 : constant Integer := Pattern'Length - 1;
 161       Num : Natural;
 162       Ind : Natural;
 163
 164    begin
 165       if Pattern = "" then
 166          raise Pattern_Error;
 167       end if;
 168
 169       --  Isolating the null string case to ensure Source'First, Source'Last in
 170       --  Positive.
 171
 172       if Source = "" then
 173          return 0;
 174       end if;
 175
 176       --  Check for null pointer in case checks are off
 177
 178       if Mapping = null then
 179          raise Constraint_Error;
 180       end if;
 181
 182       Num := 0;
 183       Ind := Source'First - 1;
 184       while Ind < Source'Last - PL1 loop
 185          Ind := Ind + 1;
 186          for K in Pattern'Range loop
 187             if Pattern (K) /= Mapping (Source (Ind + (K - Pattern'First))) then
 188                pragma Annotate (GNATprove, False_Positive,
 189                                 "call via access-to-subprogram",
 190                                 "function Mapping must always terminate");
 191                pragma Assert (not (Match (Source, Pattern, Mapping, Ind)));
 192                goto Cont;
 193             end if;
 194
 195             pragma Loop_Invariant
 196               (for all J in Pattern'First .. K =>
 197                  Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
 198             pragma Annotate (GNATprove, False_Positive,
 199                              "call via access-to-subprogram",
 200                              "function Mapping must always terminate");
 201          end loop;
 202
 203          pragma Assert (Match (Source, Pattern, Mapping, Ind));
 204          Num := Num + 1;
 205          Ind := Ind + PL1;
 206
 207       <<Cont>>
 208          null;
 209          pragma Loop_Invariant (Num <= Ind - (Source'First - 1));
 210          pragma Loop_Invariant (Ind >= Source'First);
 211          pragma Loop_Variant (Increases => Ind);
 212       end loop;
 213
 214       return Num;
 215    end Count;
 216
 217    function Count
 218      (Source : String;
 219       Set    : Maps.Character_Set) return Natural
 220    is
 221       N : Natural := 0;
 222
 223    begin
 224       for J in Source'Range loop
 225          pragma Loop_Invariant (N <= J - Source'First);
 226          if Is_In (Source (J), Set) then
 227             N := N + 1;
 228          end if;
 229       end loop;
 230
 231       return N;
 232    end Count;
 233
 234    ----------------
 235    -- Find_Token --
 236    ----------------
 237
 238    procedure Find_Token
 239      (Source : String;
 240       Set    : Maps.Character_Set;
 241       From   : Positive;
 242       Test   : Membership;
 243       First  : out Positive;
 244       Last   : out Natural)
 245    is
 246    begin
 247       --  AI05-031: Raise Index error if Source non-empty and From not in range
 248
 249       if Source'Length /= 0 and then From not in Source'Range then
 250          raise Index_Error;
 251       end if;
 252
 253       --  If Source is the empty string, From may still be out of its
 254       --  range.  The following ensures that in all cases there is no
 255       --  possible erroneous access to a non-existing character.
 256
 257       for J in Integer'Max (From, Source'First) .. Source'Last loop
 258          if Belongs (Source (J), Set, Test) then
 259             First := J;
 260
 261             if J < Source'Last then
 262                for K in J + 1 .. Source'Last loop
 263                   if not Belongs (Source (K), Set, Test) then
 264                      Last := K - 1;
 265                      return;
 266                   end if;
 267
 268                   pragma Loop_Invariant
 269                     (for all L in J .. K =>
 270                        Belongs (Source (L), Set, Test));
 271                end loop;
 272             end if;
 273
 274             --  Here if J indexes first char of token, and all chars after J
 275             --  are in the token.
 276
 277             Last := Source'Last;
 278             return;
 279          end if;
 280
 281          pragma Loop_Invariant
 282            (for all K in Integer'Max (From, Source'First) .. J =>
 283                 not (Belongs (Source (K), Set, Test)));
 284       end loop;
 285
 286       --  Here if no token found
 287
 288       First := From;
 289       Last  := 0;
 290    end Find_Token;
 291
 292    procedure Find_Token
 293      (Source : String;
 294       Set    : Maps.Character_Set;
 295       Test   : Membership;
 296       First  : out Positive;
 297       Last   : out Natural)
 298    is
 299    begin
 300       for J in Source'Range loop
 301          if Belongs (Source (J), Set, Test) then
 302             First := J;
 303
 304             if J < Source'Last then
 305                for K in J + 1 .. Source'Last loop
 306                   if not Belongs (Source (K), Set, Test) then
 307                      Last := K - 1;
 308                      return;
 309                   end if;
 310
 311                   pragma Loop_Invariant
 312                     (for all L in J .. K =>
 313                        Belongs (Source (L), Set, Test));
 314                end loop;
 315             end if;
 316
 317             --  Here if J indexes first char of token, and all chars after J
 318             --  are in the token.
 319
 320             Last := Source'Last;
 321             return;
 322          end if;
 323
 324          pragma Loop_Invariant
 325            (for all K in Source'First .. J =>
 326               not (Belongs (Source (K), Set, Test)));
 327       end loop;
 328
 329       --  Here if no token found
 330
 331       --  RM 2005 A.4.3 (68/1) specifies that an exception must be raised if
 332       --  Source'First is not positive and is assigned to First. Formulation
 333       --  is slightly different in RM 2012, but the intent seems similar, so
 334       --  we check explicitly for that condition.
 335
 336       if Source'First not in Positive then
 337          raise Constraint_Error;
 338
 339       else
 340          First := Source'First;
 341          Last  := 0;
 342       end if;
 343    end Find_Token;
 344
 345    -----------
 346    -- Index --
 347    -----------
 348
 349    function Index
 350      (Source  : String;
 351       Pattern : String;
 352       Going   : Direction := Forward;
 353       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
 354    is
 355       PL1 : constant Integer := Pattern'Length - 1;
 356
 357    begin
 358       if Pattern = "" then
 359          raise Pattern_Error;
 360       end if;
 361
 362       --  If Pattern is longer than Source, it can't be found
 363
 364       if Pattern'Length > Source'Length then
 365          return 0;
 366       end if;
 367
 368       --  Forwards case
 369
 370       if Going = Forward then
 371
 372          --  Unmapped forward case
 373
 374          if Is_Identity (Mapping) then
 375             for Ind in Source'First .. Source'Last - PL1 loop
 376                if Pattern = Source (Ind .. Ind + PL1) then
 377                   pragma Assert (Match (Source, Pattern, Mapping, Ind));
 378                   return Ind;
 379                end if;
 380
 381                pragma Loop_Invariant
 382                  (for all J in Source'First .. Ind =>
 383                     not (Match (Source, Pattern, Mapping, J)));
 384             end loop;
 385
 386          --  Mapped forward case
 387
 388          else
 389             for Ind in Source'First .. Source'Last - PL1 loop
 390                for K in Pattern'Range loop
 391                   if Pattern (K) /= Value (Mapping,
 392                     Source (Ind + (K - Pattern'First)))
 393                   then
 394                      goto Cont1;
 395                   end if;
 396
 397                   pragma Loop_Invariant
 398                     (for all J in Pattern'First .. K =>
 399                        Pattern (J) = Value (Mapping,
 400                          Source (Ind + (J - Pattern'First))));
 401                end loop;
 402
 403                pragma Assert (Match (Source, Pattern, Mapping, Ind));
 404                return Ind;
 405
 406                <<Cont1>>
 407                pragma Loop_Invariant
 408                  (for all J in Source'First .. Ind =>
 409                     not (Match (Source, Pattern, Mapping, J)));
 410                null;
 411             end loop;
 412          end if;
 413
 414       --  Backwards case
 415
 416       else
 417          --  Unmapped backward case
 418
 419          if Is_Identity (Mapping) then
 420             for Ind in reverse Source'First .. Source'Last - PL1 loop
 421                if Pattern = Source (Ind .. Ind + PL1) then
 422                   pragma Assert (Match (Source, Pattern, Mapping, Ind));
 423                   return Ind;
 424                end if;
 425
 426                pragma Loop_Invariant
 427                  (for all J in Ind .. Source'Last - PL1 =>
 428                     not (Match (Source, Pattern, Mapping, J)));
 429             end loop;
 430
 431          --  Mapped backward case
 432
 433          else
 434             for Ind in reverse Source'First .. Source'Last - PL1 loop
 435                for K in Pattern'Range loop
 436                   if Pattern (K) /= Value (Mapping,
 437                     Source (Ind + (K - Pattern'First)))
 438                   then
 439                      goto Cont2;
 440                   end if;
 441
 442                   pragma Loop_Invariant
 443                     (for all J in Pattern'First .. K =>
 444                        Pattern (J) = Value (Mapping,
 445                          Source (Ind + (J - Pattern'First))));
 446                end loop;
 447
 448                pragma Assert (Match (Source, Pattern, Mapping, Ind));
 449                return Ind;
 450
 451                <<Cont2>>
 452                pragma Loop_Invariant
 453                  (for all J in Ind .. Source'Last - PL1 =>
 454                     not (Match (Source, Pattern, Mapping, J)));
 455                null;
 456             end loop;
 457          end if;
 458       end if;
 459
 460       --  Fall through if no match found. Note that the loops are skipped
 461       --  completely in the case of the pattern being longer than the source.
 462
 463       return 0;
 464    end Index;
 465
 466    function Index
 467      (Source  : String;
 468       Pattern : String;
 469       Going   : Direction := Forward;
 470       Mapping : Maps.Character_Mapping_Function) return Natural
 471    is
 472       PL1 : constant Integer := Pattern'Length - 1;
 473    begin
 474       if Pattern = "" then
 475          raise Pattern_Error;
 476       end if;
 477
 478       --  Check for null pointer in case checks are off
 479
 480       if Mapping = null then
 481          raise Constraint_Error;
 482       end if;
 483
 484       --  If Pattern longer than Source it can't be found
 485
 486       if Pattern'Length > Source'Length then
 487          return 0;
 488       end if;
 489
 490       --  Forwards case
 491
 492       if Going = Forward then
 493          for Ind in Source'First .. Source'Last - PL1 loop
 494             for K in Pattern'Range loop
 495                if Pattern (K) /= Mapping.all
 496                  (Source (Ind + (K - Pattern'First)))
 497                then
 498                   pragma Annotate (GNATprove, False_Positive,
 499                                    "call via access-to-subprogram",
 500                                    "function Mapping must always terminate");
 501                   goto Cont1;
 502                end if;
 503
 504                pragma Loop_Invariant
 505                  (for all J in Pattern'First .. K =>
 506                    Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
 507                pragma Annotate (GNATprove, False_Positive,
 508                                 "call via access-to-subprogram",
 509                                 "function Mapping must always terminate");
 510             end loop;
 511
 512             pragma Assert (Match (Source, Pattern, Mapping, Ind));
 513             return Ind;
 514
 515             <<Cont1>>
 516             pragma Loop_Invariant
 517               (for all J in Source'First .. Ind =>
 518                  not (Match (Source, Pattern, Mapping, J)));
 519             null;
 520          end loop;
 521
 522       --  Backwards case
 523
 524       else
 525          for Ind in reverse Source'First .. Source'Last - PL1 loop
 526             for K in Pattern'Range loop
 527                if Pattern (K) /= Mapping.all
 528                  (Source (Ind + (K - Pattern'First)))
 529                then
 530                   pragma Annotate (GNATprove, False_Positive,
 531                                    "call via access-to-subprogram",
 532                                    "function Mapping must always terminate");
 533                   goto Cont2;
 534                end if;
 535
 536                pragma Loop_Invariant
 537                  (for all J in Pattern'First .. K =>
 538                    Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
 539                pragma Annotate (GNATprove, False_Positive,
 540                                 "call via access-to-subprogram",
 541                                 "function Mapping must always terminate");
 542             end loop;
 543
 544             return Ind;
 545
 546             <<Cont2>>
 547             pragma Loop_Invariant
 548               (for all J in Ind .. Source'Last - PL1 =>
 549                 not (Match (Source, Pattern, Mapping, J)));
 550             null;
 551          end loop;
 552       end if;
 553
 554       --  Fall through if no match found. Note that the loops are skipped
 555       --  completely in the case of the pattern being longer than the source.
 556
 557       return 0;
 558    end Index;
 559
 560    function Index
 561      (Source : String;
 562       Set    : Maps.Character_Set;
 563       Test   : Membership := Inside;
 564       Going  : Direction  := Forward) return Natural
 565    is
 566    begin
 567       --  Forwards case
 568
 569       if Going = Forward then
 570          for J in Source'Range loop
 571             if Belongs (Source (J), Set, Test) then
 572                return J;
 573             end if;
 574
 575             pragma Loop_Invariant
 576               (for all C of Source (Source'First .. J) =>
 577                    not (Belongs (C, Set, Test)));
 578          end loop;
 579
 580       --  Backwards case
 581
 582       else
 583          for J in reverse Source'Range loop
 584             if Belongs (Source (J), Set, Test) then
 585                return J;
 586             end if;
 587
 588             pragma Loop_Invariant
 589               (for all C of Source (J .. Source'Last) =>
 590                    not (Belongs (C, Set, Test)));
 591          end loop;
 592       end if;
 593
 594       --  Fall through if no match
 595
 596       return 0;
 597    end Index;
 598
 599    function Index
 600      (Source  : String;
 601       Pattern : String;
 602       From    : Positive;
 603       Going   : Direction := Forward;
 604       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
 605    is
 606       Result : Natural;
 607       PL1    : constant Integer := Pattern'Length - 1;
 608    begin
 609
 610       --  AI05-056: If source is empty result is always zero
 611
 612       if Source'Length = 0 then
 613          return 0;
 614
 615       elsif Going = Forward then
 616          if From < Source'First then
 617             raise Index_Error;
 618          end if;
 619
 620          Result :=
 621            Index (Source (From .. Source'Last), Pattern, Forward, Mapping);
 622          pragma Assert
 623            (if (for some J in From .. Source'Last - PL1 =>
 624                  Match (Source, Pattern, Mapping, J))
 625             then Result in From .. Source'Last - PL1
 626               and then Match (Source, Pattern, Mapping, Result)
 627             else Result = 0);
 628
 629       else
 630          if From > Source'Last then
 631             raise Index_Error;
 632          end if;
 633
 634          Result :=
 635            Index (Source (Source'First .. From), Pattern, Backward, Mapping);
 636          pragma Assert
 637            (if (for some J in Source'First .. From - PL1 =>
 638                   Match (Source, Pattern, Mapping, J))
 639             then Result in Source'First .. From - PL1
 640               and then Match (Source, Pattern, Mapping, Result)
 641             else Result = 0);
 642       end if;
 643
 644       return Result;
 645    end Index;
 646
 647    function Index
 648      (Source  : String;
 649       Pattern : String;
 650       From    : Positive;
 651       Going   : Direction := Forward;
 652       Mapping : Maps.Character_Mapping_Function) return Natural
 653    is
 654    begin
 655
 656       --  AI05-056: If source is empty result is always zero
 657
 658       if Source'Length = 0 then
 659          return 0;
 660
 661       elsif Going = Forward then
 662          if From < Source'First then
 663             raise Index_Error;
 664          end if;
 665
 666          return Index
 667            (Source (From .. Source'Last), Pattern, Forward, Mapping);
 668
 669       else
 670          if From > Source'Last then
 671             raise Index_Error;
 672          end if;
 673
 674          return Index
 675            (Source (Source'First .. From), Pattern, Backward, Mapping);
 676       end if;
 677    end Index;
 678
 679    function Index
 680      (Source  : String;
 681       Set     : Maps.Character_Set;
 682       From    : Positive;
 683       Test    : Membership := Inside;
 684       Going   : Direction := Forward) return Natural
 685    is
 686    begin
 687
 688       --  AI05-056 : if source is empty result is always 0.
 689
 690       if Source'Length = 0 then
 691          return 0;
 692
 693       elsif Going = Forward then
 694          if From < Source'First then
 695             raise Index_Error;
 696          end if;
 697
 698          return
 699            Index (Source (From .. Source'Last), Set, Test, Forward);
 700
 701       else
 702          if From > Source'Last then
 703             raise Index_Error;
 704          end if;
 705
 706          return
 707            Index (Source (Source'First .. From), Set, Test, Backward);
 708       end if;
 709    end Index;
 710
 711    ---------------------
 712    -- Index_Non_Blank --
 713    ---------------------
 714
 715    function Index_Non_Blank
 716      (Source : String;
 717       Going  : Direction := Forward) return Natural
 718    is
 719    begin
 720       if Going = Forward then
 721          for J in Source'Range loop
 722             if Source (J) /= ' ' then
 723                return J;
 724             end if;
 725
 726             pragma Loop_Invariant
 727               (for all C of Source (Source'First .. J) => C = ' ');
 728          end loop;
 729
 730       else -- Going = Backward
 731          for J in reverse Source'Range loop
 732             if Source (J) /= ' ' then
 733                return J;
 734             end if;
 735
 736             pragma Loop_Invariant
 737               (for all C of Source (J .. Source'Last) => C = ' ');
 738          end loop;
 739       end if;
 740
 741       --  Fall through if no match
 742
 743       return 0;
 744    end Index_Non_Blank;
 745
 746    function Index_Non_Blank
 747      (Source : String;
 748       From   : Positive;
 749       Going  : Direction := Forward) return Natural
 750    is
 751    begin
 752
 753       --  For equivalence with Index, if Source is empty the result is 0
 754
 755       if Source'Length = 0 then
 756          return 0;
 757       end if;
 758
 759       if Going = Forward then
 760          if From < Source'First then
 761             raise Index_Error;
 762          end if;
 763
 764          return
 765            Index_Non_Blank (Source (From .. Source'Last), Forward);
 766
 767       else
 768          if From > Source'Last then
 769             raise Index_Error;
 770          end if;
 771
 772          return
 773            Index_Non_Blank (Source (Source'First .. From), Backward);
 774       end if;
 775    end Index_Non_Blank;
 776
 777    function Is_Identity
 778      (Mapping : Maps.Character_Mapping) return Boolean
 779    with SPARK_Mode => Off
 780    is
 781    begin
 782       return Mapping'Address = Maps.Identity'Address;
 783    end Is_Identity;
 784
 785 end Ada.Strings.Search;