1------------------------------------------------------------------------------ 2-- -- 3-- GNAT RUN-TIME COMPONENTS -- 4-- -- 5-- A D A . S T R I N G S . U N B O U N D E D -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 1992-2021, Free Software Foundation, Inc. -- 10-- -- 11-- This specification is derived from the Ada Reference Manual for use with -- 12-- GNAT. The copyright notice above, and the license provisions that follow -- 13-- apply solely to the contents of the part following the private keyword. -- 14-- -- 15-- GNAT is free software; you can redistribute it and/or modify it under -- 16-- terms of the GNU General Public License as published by the Free Soft- -- 17-- ware Foundation; either version 3, or (at your option) any later ver- -- 18-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- 19-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- 20-- or FITNESS FOR A PARTICULAR PURPOSE. -- 21-- -- 22-- As a special exception under Section 7 of GPL version 3, you are granted -- 23-- additional permissions described in the GCC Runtime Library Exception, -- 24-- version 3.1, as published by the Free Software Foundation. -- 25-- -- 26-- You should have received a copy of the GNU General Public License and -- 27-- a copy of the GCC Runtime Library Exception along with this program; -- 28-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- 29-- <http://www.gnu.org/licenses/>. -- 30-- -- 31-- GNAT was originally developed by the GNAT team at New York University. -- 32-- Extensive contributions were provided by Ada Core Technologies Inc. -- 33-- -- 34------------------------------------------------------------------------------ 35 36-- Preconditions in this unit are meant for analysis only, not for run-time 37-- checking, so that the expected exceptions are raised. This is enforced by 38-- setting the corresponding assertion policy to Ignore. 39 40pragma Assertion_Policy (Pre => Ignore); 41 42-- This package provides an implementation of Ada.Strings.Unbounded that uses 43-- reference counts to implement copy on modification (rather than copy on 44-- assignment). This is significantly more efficient on many targets. 45 46-- This version is supported on: 47-- - all Alpha platforms 48-- - all AARCH64 platforms 49-- - all ARM platforms 50-- - all ia64 platforms 51-- - all PowerPC platforms 52-- - all SPARC V9 platforms 53-- - all x86 platforms 54-- - all x86_64 platforms 55 56 -- This package uses several techniques to increase speed: 57 58 -- - Implicit sharing or copy-on-write. An Unbounded_String contains only 59 -- the reference to the data which is shared between several instances. 60 -- The shared data is reallocated only when its value is changed and 61 -- the object mutation can't be used or it is inefficient to use it. 62 63 -- - Object mutation. Shared data object can be reused without memory 64 -- reallocation when all of the following requirements are met: 65 -- - the shared data object is no longer used by anyone else; 66 -- - the size is sufficient to store the new value; 67 -- - the gap after reuse is less than a defined threshold. 68 69 -- - Memory preallocation. Most of used memory allocation algorithms 70 -- align allocated segments on the some boundary, thus some amount of 71 -- additional memory can be preallocated without any impact. Such 72 -- preallocated memory can used later by Append/Insert operations 73 -- without reallocation. 74 75 -- Reference counting uses GCC builtin atomic operations, which allows safe 76 -- sharing of internal data between Ada tasks. Nevertheless, this does not 77 -- make objects of Unbounded_String thread-safe: an instance cannot be 78 -- accessed by several tasks simultaneously. 79 80with Ada.Strings.Maps; 81private with Ada.Finalization; 82private with System.Atomic_Counters; 83private with Ada.Strings.Text_Buffers; 84 85package Ada.Strings.Unbounded with 86 Initial_Condition => Length (Null_Unbounded_String) = 0 87is 88 pragma Preelaborate; 89 90 type Unbounded_String is private with 91 Default_Initial_Condition => Length (Unbounded_String) = 0; 92 pragma Preelaborable_Initialization (Unbounded_String); 93 94 Null_Unbounded_String : constant Unbounded_String; 95 96 function Length (Source : Unbounded_String) return Natural with 97 Global => null; 98 99 type String_Access is access all String; 100 101 procedure Free (X : in out String_Access); 102 103 -------------------------------------------------------- 104 -- Conversion, Concatenation, and Selection Functions -- 105 -------------------------------------------------------- 106 107 function To_Unbounded_String 108 (Source : String) return Unbounded_String 109 with 110 Post => Length (To_Unbounded_String'Result) = Source'Length, 111 Global => null; 112 113 function To_Unbounded_String 114 (Length : Natural) return Unbounded_String 115 with 116 Post => 117 Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length, 118 Global => null; 119 120 function To_String (Source : Unbounded_String) return String with 121 Post => To_String'Result'Length = Length (Source), 122 Global => null; 123 124 procedure Set_Unbounded_String 125 (Target : out Unbounded_String; 126 Source : String) 127 with 128 Global => null; 129 pragma Ada_05 (Set_Unbounded_String); 130 131 procedure Append 132 (Source : in out Unbounded_String; 133 New_Item : Unbounded_String) 134 with 135 Pre => Length (New_Item) <= Natural'Last - Length (Source), 136 Post => Length (Source) = Length (Source)'Old + Length (New_Item), 137 Global => null; 138 139 procedure Append 140 (Source : in out Unbounded_String; 141 New_Item : String) 142 with 143 Pre => New_Item'Length <= Natural'Last - Length (Source), 144 Post => Length (Source) = Length (Source)'Old + New_Item'Length, 145 Global => null; 146 147 procedure Append 148 (Source : in out Unbounded_String; 149 New_Item : Character) 150 with 151 Pre => Length (Source) < Natural'Last, 152 Post => Length (Source) = Length (Source)'Old + 1, 153 Global => null; 154 155 function "&" 156 (Left : Unbounded_String; 157 Right : Unbounded_String) return Unbounded_String 158 with 159 Pre => Length (Right) <= Natural'Last - Length (Left), 160 Post => Length ("&"'Result) = Length (Left) + Length (Right), 161 Global => null; 162 163 function "&" 164 (Left : Unbounded_String; 165 Right : String) return Unbounded_String 166 with 167 Pre => Right'Length <= Natural'Last - Length (Left), 168 Post => Length ("&"'Result) = Length (Left) + Right'Length, 169 Global => null; 170 171 function "&" 172 (Left : String; 173 Right : Unbounded_String) return Unbounded_String 174 with 175 Pre => Left'Length <= Natural'Last - Length (Right), 176 Post => Length ("&"'Result) = Left'Length + Length (Right), 177 Global => null; 178 179 function "&" 180 (Left : Unbounded_String; 181 Right : Character) return Unbounded_String 182 with 183 Pre => Length (Left) < Natural'Last, 184 Post => Length ("&"'Result) = Length (Left) + 1, 185 Global => null; 186 187 function "&" 188 (Left : Character; 189 Right : Unbounded_String) return Unbounded_String 190 with 191 Pre => Length (Right) < Natural'Last, 192 Post => Length ("&"'Result) = Length (Right) + 1, 193 Global => null; 194 195 function Element 196 (Source : Unbounded_String; 197 Index : Positive) return Character 198 with 199 Pre => Index <= Length (Source), 200 Global => null; 201 202 procedure Replace_Element 203 (Source : in out Unbounded_String; 204 Index : Positive; 205 By : Character) 206 with 207 Pre => Index <= Length (Source), 208 Post => Length (Source) = Length (Source)'Old, 209 Global => null; 210 211 function Slice 212 (Source : Unbounded_String; 213 Low : Positive; 214 High : Natural) return String 215 with 216 Pre => Low - 1 <= Length (Source) and then High <= Length (Source), 217 Post => Slice'Result'Length = Natural'Max (0, High - Low + 1), 218 Global => null; 219 220 function Unbounded_Slice 221 (Source : Unbounded_String; 222 Low : Positive; 223 High : Natural) return Unbounded_String 224 with 225 Pre => Low - 1 <= Length (Source) and then High <= Length (Source), 226 Post => 227 Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1), 228 Global => null; 229 pragma Ada_05 (Unbounded_Slice); 230 231 procedure Unbounded_Slice 232 (Source : Unbounded_String; 233 Target : out Unbounded_String; 234 Low : Positive; 235 High : Natural) 236 with 237 Pre => Low - 1 <= Length (Source) and then High <= Length (Source), 238 Post => Length (Target) = Natural'Max (0, High - Low + 1), 239 Global => null; 240 pragma Ada_05 (Unbounded_Slice); 241 242 function "=" 243 (Left : Unbounded_String; 244 Right : Unbounded_String) return Boolean 245 with 246 Global => null; 247 248 function "=" 249 (Left : Unbounded_String; 250 Right : String) return Boolean 251 with 252 Global => null; 253 254 function "=" 255 (Left : String; 256 Right : Unbounded_String) return Boolean 257 with 258 Global => null; 259 260 function "<" 261 (Left : Unbounded_String; 262 Right : Unbounded_String) return Boolean 263 with 264 Global => null; 265 266 function "<" 267 (Left : Unbounded_String; 268 Right : String) return Boolean 269 with 270 Global => null; 271 272 function "<" 273 (Left : String; 274 Right : Unbounded_String) return Boolean 275 with 276 Global => null; 277 278 function "<=" 279 (Left : Unbounded_String; 280 Right : Unbounded_String) return Boolean 281 with 282 Global => null; 283 284 function "<=" 285 (Left : Unbounded_String; 286 Right : String) return Boolean 287 with 288 Global => null; 289 290 function "<=" 291 (Left : String; 292 Right : Unbounded_String) return Boolean 293 with 294 Global => null; 295 296 function ">" 297 (Left : Unbounded_String; 298 Right : Unbounded_String) return Boolean 299 with 300 Global => null; 301 302 function ">" 303 (Left : Unbounded_String; 304 Right : String) return Boolean 305 with 306 Global => null; 307 308 function ">" 309 (Left : String; 310 Right : Unbounded_String) return Boolean 311 with 312 Global => null; 313 314 function ">=" 315 (Left : Unbounded_String; 316 Right : Unbounded_String) return Boolean 317 with 318 Global => null; 319 320 function ">=" 321 (Left : Unbounded_String; 322 Right : String) return Boolean 323 with 324 Global => null; 325 326 function ">=" 327 (Left : String; 328 Right : Unbounded_String) return Boolean 329 with 330 Global => null; 331 332 ------------------------ 333 -- Search Subprograms -- 334 ------------------------ 335 336 function Index 337 (Source : Unbounded_String; 338 Pattern : String; 339 Going : Direction := Forward; 340 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural 341 with 342 Pre => Pattern'Length /= 0, 343 Global => null; 344 345 function Index 346 (Source : Unbounded_String; 347 Pattern : String; 348 Going : Direction := Forward; 349 Mapping : Maps.Character_Mapping_Function) return Natural 350 with 351 Pre => Pattern'Length /= 0, 352 Global => null; 353 354 function Index 355 (Source : Unbounded_String; 356 Set : Maps.Character_Set; 357 Test : Membership := Inside; 358 Going : Direction := Forward) return Natural 359 with 360 Global => null; 361 362 function Index 363 (Source : Unbounded_String; 364 Pattern : String; 365 From : Positive; 366 Going : Direction := Forward; 367 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural 368 with 369 Pre => (if Length (Source) /= 0 then From <= Length (Source)) 370 and then Pattern'Length /= 0, 371 Global => null; 372 pragma Ada_05 (Index); 373 374 function Index 375 (Source : Unbounded_String; 376 Pattern : String; 377 From : Positive; 378 Going : Direction := Forward; 379 Mapping : Maps.Character_Mapping_Function) return Natural 380 with 381 Pre => (if Length (Source) /= 0 then From <= Length (Source)) 382 and then Pattern'Length /= 0, 383 Global => null; 384 pragma Ada_05 (Index); 385 386 function Index 387 (Source : Unbounded_String; 388 Set : Maps.Character_Set; 389 From : Positive; 390 Test : Membership := Inside; 391 Going : Direction := Forward) return Natural 392 with 393 Pre => (if Length (Source) /= 0 then From <= Length (Source)), 394 Global => null; 395 pragma Ada_05 (Index); 396 397 function Index_Non_Blank 398 (Source : Unbounded_String; 399 Going : Direction := Forward) return Natural 400 with 401 Global => null; 402 403 function Index_Non_Blank 404 (Source : Unbounded_String; 405 From : Positive; 406 Going : Direction := Forward) return Natural 407 with 408 Pre => (if Length (Source) /= 0 then From <= Length (Source)), 409 Global => null; 410 pragma Ada_05 (Index_Non_Blank); 411 412 function Count 413 (Source : Unbounded_String; 414 Pattern : String; 415 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural 416 with 417 Pre => Pattern'Length /= 0, 418 Global => null; 419 420 function Count 421 (Source : Unbounded_String; 422 Pattern : String; 423 Mapping : Maps.Character_Mapping_Function) return Natural 424 with 425 Pre => Pattern'Length /= 0, 426 Global => null; 427 428 function Count 429 (Source : Unbounded_String; 430 Set : Maps.Character_Set) return Natural 431 with 432 Global => null; 433 434 procedure Find_Token 435 (Source : Unbounded_String; 436 Set : Maps.Character_Set; 437 From : Positive; 438 Test : Membership; 439 First : out Positive; 440 Last : out Natural) 441 with 442 Pre => (if Length (Source) /= 0 then From <= Length (Source)), 443 Global => null; 444 pragma Ada_2012 (Find_Token); 445 446 procedure Find_Token 447 (Source : Unbounded_String; 448 Set : Maps.Character_Set; 449 Test : Membership; 450 First : out Positive; 451 Last : out Natural) 452 with 453 Global => null; 454 455 ------------------------------------ 456 -- String Translation Subprograms -- 457 ------------------------------------ 458 459 function Translate 460 (Source : Unbounded_String; 461 Mapping : Maps.Character_Mapping) return Unbounded_String 462 with 463 Post => Length (Translate'Result) = Length (Source), 464 Global => null; 465 466 procedure Translate 467 (Source : in out Unbounded_String; 468 Mapping : Maps.Character_Mapping) 469 with 470 Post => Length (Source) = Length (Source)'Old, 471 Global => null; 472 473 function Translate 474 (Source : Unbounded_String; 475 Mapping : Maps.Character_Mapping_Function) return Unbounded_String 476 with 477 Post => Length (Translate'Result) = Length (Source), 478 Global => null; 479 480 procedure Translate 481 (Source : in out Unbounded_String; 482 Mapping : Maps.Character_Mapping_Function) 483 with 484 Post => Length (Source) = Length (Source)'Old, 485 Global => null; 486 487 --------------------------------------- 488 -- String Transformation Subprograms -- 489 --------------------------------------- 490 491 function Replace_Slice 492 (Source : Unbounded_String; 493 Low : Positive; 494 High : Natural; 495 By : String) return Unbounded_String 496 with 497 Pre => 498 Low - 1 <= Length (Source) 499 and then (if High >= Low 500 then Low - 1 501 <= Natural'Last - By'Length 502 - Natural'Max (Length (Source) - High, 0) 503 else Length (Source) <= Natural'Last - By'Length), 504 Contract_Cases => 505 (High >= Low => 506 Length (Replace_Slice'Result) 507 = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0), 508 others => 509 Length (Replace_Slice'Result) = Length (Source)'Old + By'Length), 510 Global => null; 511 512 procedure Replace_Slice 513 (Source : in out Unbounded_String; 514 Low : Positive; 515 High : Natural; 516 By : String) 517 with 518 Pre => 519 Low - 1 <= Length (Source) 520 and then (if High >= Low 521 then Low - 1 522 <= Natural'Last - By'Length 523 - Natural'Max (Length (Source) - High, 0) 524 else Length (Source) <= Natural'Last - By'Length), 525 Contract_Cases => 526 (High >= Low => 527 Length (Source) 528 = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0), 529 others => 530 Length (Source) = Length (Source)'Old + By'Length), 531 Global => null; 532 533 function Insert 534 (Source : Unbounded_String; 535 Before : Positive; 536 New_Item : String) return Unbounded_String 537 with 538 Pre => Before - 1 <= Length (Source) 539 and then New_Item'Length <= Natural'Last - Length (Source), 540 Post => Length (Insert'Result) = Length (Source) + New_Item'Length, 541 Global => null; 542 543 procedure Insert 544 (Source : in out Unbounded_String; 545 Before : Positive; 546 New_Item : String) 547 with 548 Pre => Before - 1 <= Length (Source) 549 and then New_Item'Length <= Natural'Last - Length (Source), 550 Post => Length (Source) = Length (Source)'Old + New_Item'Length, 551 Global => null; 552 553 function Overwrite 554 (Source : Unbounded_String; 555 Position : Positive; 556 New_Item : String) return Unbounded_String 557 with 558 Pre => Position - 1 <= Length (Source) 559 and then (if New_Item'Length /= 0 560 then 561 New_Item'Length <= Natural'Last - (Position - 1)), 562 Post => 563 Length (Overwrite'Result) 564 = Natural'Max (Length (Source), Position - 1 + New_Item'Length), 565 Global => null; 566 567 procedure Overwrite 568 (Source : in out Unbounded_String; 569 Position : Positive; 570 New_Item : String) 571 with 572 Pre => Position - 1 <= Length (Source) 573 and then (if New_Item'Length /= 0 574 then 575 New_Item'Length <= Natural'Last - (Position - 1)), 576 Post => 577 Length (Source) 578 = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length), 579 580 Global => null; 581 582 function Delete 583 (Source : Unbounded_String; 584 From : Positive; 585 Through : Natural) return Unbounded_String 586 with 587 Pre => (if Through <= From then From - 1 <= Length (Source)), 588 Contract_Cases => 589 (Through >= From => 590 Length (Delete'Result) = Length (Source) - (Through - From + 1), 591 others => 592 Length (Delete'Result) = Length (Source)), 593 Global => null; 594 595 procedure Delete 596 (Source : in out Unbounded_String; 597 From : Positive; 598 Through : Natural) 599 with 600 Pre => (if Through <= From then From - 1 <= Length (Source)), 601 Contract_Cases => 602 (Through >= From => 603 Length (Source) = Length (Source)'Old - (Through - From + 1), 604 others => 605 Length (Source) = Length (Source)'Old), 606 Global => null; 607 608 function Trim 609 (Source : Unbounded_String; 610 Side : Trim_End) return Unbounded_String 611 with 612 Post => Length (Trim'Result) <= Length (Source), 613 Global => null; 614 615 procedure Trim 616 (Source : in out Unbounded_String; 617 Side : Trim_End) 618 with 619 Post => Length (Source) <= Length (Source)'Old, 620 Global => null; 621 622 function Trim 623 (Source : Unbounded_String; 624 Left : Maps.Character_Set; 625 Right : Maps.Character_Set) return Unbounded_String 626 with 627 Post => Length (Trim'Result) <= Length (Source), 628 Global => null; 629 630 procedure Trim 631 (Source : in out Unbounded_String; 632 Left : Maps.Character_Set; 633 Right : Maps.Character_Set) 634 with 635 Post => Length (Source) <= Length (Source)'Old, 636 Global => null; 637 638 function Head 639 (Source : Unbounded_String; 640 Count : Natural; 641 Pad : Character := Space) return Unbounded_String 642 with 643 Post => Length (Head'Result) = Count, 644 Global => null; 645 646 procedure Head 647 (Source : in out Unbounded_String; 648 Count : Natural; 649 Pad : Character := Space) 650 with 651 Post => Length (Source) = Count, 652 Global => null; 653 654 function Tail 655 (Source : Unbounded_String; 656 Count : Natural; 657 Pad : Character := Space) return Unbounded_String 658 with 659 Post => Length (Tail'Result) = Count, 660 Global => null; 661 662 procedure Tail 663 (Source : in out Unbounded_String; 664 Count : Natural; 665 Pad : Character := Space) 666 with 667 Post => Length (Source) = Count, 668 Global => null; 669 670 function "*" 671 (Left : Natural; 672 Right : Character) return Unbounded_String 673 with 674 Pre => Left <= Natural'Last, 675 Post => Length ("*"'Result) = Left, 676 Global => null; 677 678 function "*" 679 (Left : Natural; 680 Right : String) return Unbounded_String 681 with 682 Pre => (if Left /= 0 then Right'Length <= Natural'Last / Left), 683 Post => Length ("*"'Result) = Left * Right'Length, 684 Global => null; 685 686 function "*" 687 (Left : Natural; 688 Right : Unbounded_String) return Unbounded_String 689 with 690 Pre => (if Left /= 0 then Length (Right) <= Natural'Last / Left), 691 Post => Length ("*"'Result) = Left * Length (Right), 692 Global => null; 693 694private 695 pragma Inline (Length); 696 697 package AF renames Ada.Finalization; 698 699 type Shared_String (Max_Length : Natural) is limited record 700 Counter : System.Atomic_Counters.Atomic_Counter; 701 -- Reference counter 702 703 Last : Natural := 0; 704 Data : String (1 .. Max_Length); 705 -- Last is the index of last significant element of the Data. All 706 -- elements with larger indexes are currently insignificant. 707 end record; 708 709 type Shared_String_Access is access all Shared_String; 710 711 procedure Reference (Item : not null Shared_String_Access); 712 -- Increment reference counter. 713 -- Do nothing if Item points to Empty_Shared_String. 714 715 procedure Unreference (Item : not null Shared_String_Access); 716 -- Decrement reference counter, deallocate Item when counter goes to zero. 717 -- Do nothing if Item points to Empty_Shared_String. 718 719 function Can_Be_Reused 720 (Item : not null Shared_String_Access; 721 Length : Natural) return Boolean; 722 -- Returns True if Shared_String can be reused. There are two criteria when 723 -- Shared_String can be reused: its reference counter must be one (thus 724 -- Shared_String is owned exclusively) and its size is sufficient to 725 -- store string with specified length effectively. 726 727 function Allocate 728 (Required_Length : Natural; 729 Reserved_Length : Natural := 0) return not null Shared_String_Access; 730 -- Allocates new Shared_String. Actual maximum length of allocated object 731 -- is at least the specified required length. Additional storage is 732 -- allocated to allow to store up to the specified reserved length when 733 -- possible. Returns reference to Empty_Shared_String when requested length 734 -- is zero. 735 736 Empty_Shared_String : aliased Shared_String (0); 737 738 function To_Unbounded (S : String) return Unbounded_String 739 renames To_Unbounded_String; 740 -- This renames are here only to be used in the pragma Stream_Convert 741 742 type Unbounded_String is new AF.Controlled with record 743 Reference : not null Shared_String_Access := Empty_Shared_String'Access; 744 end record with Put_Image => Put_Image; 745 746 procedure Put_Image 747 (S : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class; 748 V : Unbounded_String); 749 750 pragma Stream_Convert (Unbounded_String, To_Unbounded, To_String); 751 -- Provide stream routines without dragging in Ada.Streams 752 753 pragma Finalize_Storage_Only (Unbounded_String); 754 -- Finalization is required only for freeing storage 755 756 overriding procedure Initialize (Object : in out Unbounded_String); 757 overriding procedure Adjust (Object : in out Unbounded_String); 758 overriding procedure Finalize (Object : in out Unbounded_String); 759 pragma Inline (Initialize, Adjust); 760 761 Null_Unbounded_String : constant Unbounded_String := 762 (AF.Controlled with 763 Reference => Empty_Shared_String'Access); 764 765end Ada.Strings.Unbounded; 766