------------------------------------------------------------------------------ -- -- -- GNAT RUN-TIME COMPONENTS -- -- -- -- A D A . S T R I N G S . M A P S -- -- -- -- B o d y -- -- -- -- Copyright (C) 1992-2023, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- -- ware Foundation; either version 3, or (at your option) any later ver- -- -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- -- or FITNESS FOR A PARTICULAR PURPOSE. -- -- -- -- As a special exception under Section 7 of GPL version 3, you are granted -- -- additional permissions described in the GCC Runtime Library Exception, -- -- version 3.1, as published by the Free Software Foundation. -- -- -- -- You should have received a copy of the GNU General Public License and -- -- a copy of the GCC Runtime Library Exception along with this program; -- -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- -- . -- -- -- -- GNAT was originally developed by the GNAT team at New York University. -- -- Extensive contributions were provided by Ada Core Technologies Inc. -- -- -- ------------------------------------------------------------------------------ -- Note: parts of this code are derived from the ADAR.CSH public domain -- Ada 83 versions of the Appendix C string handling packages. The main -- differences are that we avoid the use of the minimize function which -- is bit-by-bit or character-by-character and therefore rather slow. -- Generally for character sets we favor the full 32-byte representation. -- Assertions, ghost code and loop invariants 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 (Assert => Ignore, Ghost => Ignore, Loop_Invariant => Ignore); package body Ada.Strings.Maps with SPARK_Mode is --------- -- "-" -- --------- function "-" (Left, Right : Character_Set) return Character_Set is begin return Left and not Right; end "-"; --------- -- "=" -- --------- function "=" (Left, Right : Character_Set) return Boolean is begin return Character_Set_Internal (Left) = Character_Set_Internal (Right); end "="; ----------- -- "and" -- ----------- function "and" (Left, Right : Character_Set) return Character_Set is begin return Character_Set (Character_Set_Internal (Left) and Character_Set_Internal (Right)); end "and"; ----------- -- "not" -- ----------- function "not" (Right : Character_Set) return Character_Set is begin return Character_Set (not Character_Set_Internal (Right)); end "not"; ---------- -- "or" -- ---------- function "or" (Left, Right : Character_Set) return Character_Set is begin return Character_Set (Character_Set_Internal (Left) or Character_Set_Internal (Right)); end "or"; ----------- -- "xor" -- ----------- function "xor" (Left, Right : Character_Set) return Character_Set is begin return Character_Set (Character_Set_Internal (Left) xor Character_Set_Internal (Right)); end "xor"; ----------- -- Is_In -- ----------- function Is_In (Element : Character; Set : Character_Set) return Boolean is (Set (Element)); --------------- -- Is_Subset -- --------------- function Is_Subset (Elements : Character_Set; Set : Character_Set) return Boolean is begin return (Elements and Set) = Elements; end Is_Subset; --------------- -- To_Domain -- --------------- function To_Domain (Map : Character_Mapping) return Character_Sequence is Result : String (1 .. Map'Length) with Relaxed_Initialization; J : Natural; type Character_Index is array (Character) of Natural with Ghost; Indexes : Character_Index := [others => 0] with Ghost; begin J := 0; for C in Map'Range loop if Map (C) /= C then J := J + 1; Result (J) := C; Indexes (C) := J; end if; pragma Loop_Invariant (if Map = Identity then J = 0); pragma Loop_Invariant (J <= Character'Pos (C) + 1); pragma Loop_Invariant (Result (1 .. J)'Initialized); pragma Loop_Invariant (for all K in 1 .. J => Result (K) <= C); pragma Loop_Invariant (SPARK_Proof_Sorted_Character_Sequence (Result (1 .. J))); pragma Loop_Invariant (for all D in Map'First .. C => (if Map (D) = D then Indexes (D) = 0 else Indexes (D) in 1 .. J and then Result (Indexes (D)) = D)); pragma Loop_Invariant (for all Char of Result (1 .. J) => Map (Char) /= Char); end loop; return Result (1 .. J); end To_Domain; ---------------- -- To_Mapping -- ---------------- function To_Mapping (From, To : Character_Sequence) return Character_Mapping is Result : Character_Mapping with Relaxed_Initialization; Inserted : Character_Set := Null_Set; From_Len : constant Natural := From'Length; To_Len : constant Natural := To'Length; begin if From_Len /= To_Len then raise Strings.Translation_Error; end if; for Char in Character loop Result (Char) := Char; pragma Loop_Invariant (Result (Result'First .. Char)'Initialized); pragma Loop_Invariant (for all C in Result'First .. Char => Result (C) = C); end loop; for J in From'Range loop if Inserted (From (J)) then raise Strings.Translation_Error; end if; Result (From (J)) := To (J - From'First + To'First); Inserted (From (J)) := True; pragma Loop_Invariant (Result'Initialized); pragma Loop_Invariant (for all K in From'First .. J => Result (From (K)) = To (K - From'First + To'First) and then Inserted (From (K))); pragma Loop_Invariant (for all Char in Character => (Inserted (Char) = (for some K in From'First .. J => Char = From (K)))); pragma Loop_Invariant (for all Char in Character => (if not Inserted (Char) then Result (Char) = Char)); pragma Loop_Invariant (if (for all K in From'First .. J => From (K) = To (J - From'First + To'First)) then Result = Identity); end loop; return Result; end To_Mapping; -------------- -- To_Range -- -------------- function To_Range (Map : Character_Mapping) return Character_Sequence is -- Extract from the postcondition of To_Domain the essential properties -- that define Seq as the domain of Map. function Is_Domain (Map : Character_Mapping; Seq : Character_Sequence) return Boolean is (Seq'First = 1 and then SPARK_Proof_Sorted_Character_Sequence (Seq) and then (for all Char in Character => (if (for all X of Seq => X /= Char) then Map (Char) = Char)) and then (for all Char of Seq => Map (Char) /= Char)) with Ghost; -- Given Map, there is a unique sequence Seq for which -- Is_Domain(Map,Seq) holds. procedure Lemma_Domain_Unicity (Map : Character_Mapping; Seq1, Seq2 : Character_Sequence) with Ghost, Pre => Is_Domain (Map, Seq1) and then Is_Domain (Map, Seq2), Post => Seq1 = Seq2; -- Isolate the proof that To_Domain(Map) returns a sequence for which -- Is_Domain holds. procedure Lemma_Is_Domain (Map : Character_Mapping) with Ghost, Post => Is_Domain (Map, To_Domain (Map)); -- Deduce the alternative expression of sortedness from the one in -- SPARK_Proof_Sorted_Character_Sequence which compares consecutive -- elements. procedure Lemma_Is_Sorted (Seq : Character_Sequence) with Ghost, Pre => SPARK_Proof_Sorted_Character_Sequence (Seq), Post => (for all J in Seq'Range => (for all K in Seq'Range => (if J < K then Seq (J) < Seq (K)))); -------------------------- -- Lemma_Domain_Unicity -- -------------------------- procedure Lemma_Domain_Unicity (Map : Character_Mapping; Seq1, Seq2 : Character_Sequence) is J : Positive := 1; begin while J <= Seq1'Last and then J <= Seq2'Last and then Seq1 (J) = Seq2 (J) loop pragma Loop_Invariant (Seq1 (Seq1'First .. J) = Seq2 (Seq2'First .. J)); pragma Loop_Variant (Increases => J); if J = Positive'Last then return; end if; J := J + 1; end loop; Lemma_Is_Sorted (Seq1); Lemma_Is_Sorted (Seq2); if J <= Seq1'Last and then J <= Seq2'Last then if Seq1 (J) < Seq2 (J) then pragma Assert (for all X of Seq2 => X /= Seq1 (J)); pragma Assert (Map (Seq1 (J)) = Seq1 (J)); pragma Assert (False); else pragma Assert (for all X of Seq1 => X /= Seq2 (J)); pragma Assert (Map (Seq2 (J)) = Seq2 (J)); pragma Assert (False); end if; elsif J <= Seq1'Last then pragma Assert (for all X of Seq2 => X /= Seq1 (J)); pragma Assert (Map (Seq1 (J)) = Seq1 (J)); pragma Assert (False); elsif J <= Seq2'Last then pragma Assert (for all X of Seq1 => X /= Seq2 (J)); pragma Assert (Map (Seq2 (J)) = Seq2 (J)); pragma Assert (False); end if; end Lemma_Domain_Unicity; --------------------- -- Lemma_Is_Domain -- --------------------- procedure Lemma_Is_Domain (Map : Character_Mapping) is Ignore : constant Character_Sequence := To_Domain (Map); begin null; end Lemma_Is_Domain; --------------------- -- Lemma_Is_Sorted -- --------------------- procedure Lemma_Is_Sorted (Seq : Character_Sequence) is begin for A in Seq'Range loop exit when A = Positive'Last; for B in A + 1 .. Seq'Last loop pragma Loop_Invariant (for all K in A + 1 .. B => Seq (A) < Seq (K)); end loop; pragma Loop_Invariant (for all J in Seq'First .. A => (for all K in Seq'Range => (if J < K then Seq (J) < Seq (K)))); end loop; end Lemma_Is_Sorted; -- Local variables Result : String (1 .. Map'Length) with Relaxed_Initialization; J : Natural; -- Repeat the computation from To_Domain in ghost code, in order to -- prove the relationship between Result and To_Domain(Map). Domain : String (1 .. Map'Length) with Ghost, Relaxed_Initialization; type Character_Index is array (Character) of Natural with Ghost; Indexes : Character_Index := [others => 0] with Ghost; -- Start of processing for To_Range begin J := 0; for C in Map'Range loop if Map (C) /= C then J := J + 1; Result (J) := Map (C); Domain (J) := C; Indexes (C) := J; end if; -- Repeat the loop invariants from To_Domain regarding Domain and -- Indexes. Add similar loop invariants for Result and Indexes. pragma Loop_Invariant (J <= Character'Pos (C) + 1); pragma Loop_Invariant (Result (1 .. J)'Initialized); pragma Loop_Invariant (Domain (1 .. J)'Initialized); pragma Loop_Invariant (for all K in 1 .. J => Domain (K) <= C); pragma Loop_Invariant (SPARK_Proof_Sorted_Character_Sequence (Domain (1 .. J))); pragma Loop_Invariant (for all D in Map'First .. C => (if Map (D) = D then Indexes (D) = 0 else Indexes (D) in 1 .. J and then Domain (Indexes (D)) = D and then Result (Indexes (D)) = Map (D))); pragma Loop_Invariant (for all Char of Domain (1 .. J) => Map (Char) /= Char); pragma Loop_Invariant (for all K in 1 .. J => Result (K) = Map (Domain (K))); end loop; -- Show the equality of Domain and To_Domain(Map) Lemma_Is_Domain (Map); Lemma_Domain_Unicity (Map, Domain (1 .. J), To_Domain (Map)); pragma Assert (for all K in 1 .. J => Domain (K) = To_Domain (Map) (K)); pragma Assert (To_Domain (Map)'Length = J); return Result (1 .. J); end To_Range; --------------- -- To_Ranges -- --------------- function To_Ranges (Set : Character_Set) return Character_Ranges is Max_Ranges : Character_Ranges (1 .. Set'Length / 2 + 1) with Relaxed_Initialization; Range_Num : Natural; C : Character; C_Iter : Character with Ghost; begin C := Character'First; Range_Num := 0; loop C_Iter := C; -- Skip gap between subsets while not Set (C) loop pragma Loop_Invariant (Character'Pos (C) >= Character'Pos (C'Loop_Entry)); pragma Loop_Invariant (for all Char in C'Loop_Entry .. C => not Set (Char)); pragma Loop_Variant (Increases => C); exit when C = Character'Last; C := Character'Succ (C); end loop; exit when not Set (C); Range_Num := Range_Num + 1; Max_Ranges (Range_Num).Low := C; -- Span a subset loop pragma Loop_Invariant (Character'Pos (C) >= Character'Pos (C'Loop_Entry)); pragma Loop_Invariant (for all Char in C'Loop_Entry .. C => (if Char /= C then Set (Char))); pragma Loop_Variant (Increases => C); exit when not Set (C) or else C = Character'Last; C := Character'Succ (C); end loop; if Set (C) then Max_Ranges (Range_Num).High := C; exit; else Max_Ranges (Range_Num).High := Character'Pred (C); end if; pragma Assert (for all Char in C_Iter .. C => (Set (Char) = (Char in Max_Ranges (Range_Num).Low .. Max_Ranges (Range_Num).High))); pragma Assert (for all Char in Character'First .. C_Iter => (if Char /= C_Iter then (Set (Char) = (for some Span of Max_Ranges (1 .. Range_Num - 1) => Char in Span.Low .. Span.High)))); pragma Loop_Invariant (2 * Range_Num <= Character'Pos (C) + 1); pragma Loop_Invariant (Max_Ranges (1 .. Range_Num)'Initialized); pragma Loop_Invariant (not Set (C)); pragma Loop_Invariant (for all Char in Character'First .. C => (Set (Char) = (for some Span of Max_Ranges (1 .. Range_Num) => Char in Span.Low .. Span.High))); pragma Loop_Invariant (for all Span of Max_Ranges (1 .. Range_Num) => (for all Char in Span.Low .. Span.High => Set (Char))); pragma Loop_Variant (Increases => Range_Num); end loop; return Max_Ranges (1 .. Range_Num); end To_Ranges; ----------------- -- To_Sequence -- ----------------- function To_Sequence (Set : Character_Set) return Character_Sequence is Result : String (1 .. Character'Pos (Character'Last) + 1) with Relaxed_Initialization; Count : Natural := 0; begin for Char in Set'Range loop if Set (Char) then Count := Count + 1; Result (Count) := Char; end if; pragma Loop_Invariant (Count <= Character'Pos (Char) + 1); pragma Loop_Invariant (Result (1 .. Count)'Initialized); pragma Loop_Invariant (for all K in 1 .. Count => Result (K) <= Char); pragma Loop_Invariant (SPARK_Proof_Sorted_Character_Sequence (Result (1 .. Count))); pragma Loop_Invariant (for all C in Set'First .. Char => (Set (C) = (for some X of Result (1 .. Count) => C = X))); pragma Loop_Invariant (for all Char of Result (1 .. Count) => Is_In (Char, Set)); end loop; return Result (1 .. Count); end To_Sequence; ------------ -- To_Set -- ------------ function To_Set (Ranges : Character_Ranges) return Character_Set is Result : Character_Set := Null_Set; begin for R in Ranges'Range loop for C in Ranges (R).Low .. Ranges (R).High loop Result (C) := True; pragma Loop_Invariant (for all Char in Character => Result (Char) = ((for some Prev in Ranges'First .. R - 1 => Char in Ranges (Prev).Low .. Ranges (Prev).High) or else (Char in Ranges (R).Low .. C))); end loop; pragma Loop_Invariant (for all Char in Character => Result (Char) = (for some Prev in Ranges'First .. R => Char in Ranges (Prev).Low .. Ranges (Prev).High)); end loop; return Result; end To_Set; function To_Set (Span : Character_Range) return Character_Set is Result : Character_Set := Null_Set; begin for C in Span.Low .. Span.High loop Result (C) := True; pragma Loop_Invariant (for all Char in Character => Result (Char) = (Char in Span.Low .. C)); end loop; return Result; end To_Set; function To_Set (Sequence : Character_Sequence) return Character_Set is Result : Character_Set := Null_Set; begin for J in Sequence'Range loop Result (Sequence (J)) := True; pragma Loop_Invariant (for all Char in Character => Result (Char) = (for some K in Sequence'First .. J => Char = Sequence (K))); end loop; return Result; end To_Set; function To_Set (Singleton : Character) return Character_Set is Result : Character_Set := Null_Set; begin Result (Singleton) := True; return Result; end To_Set; ----------- -- Value -- ----------- function Value (Map : Character_Mapping; Element : Character) return Character is (Map (Element)); end Ada.Strings.Maps;