stdlib/string.mlw

   1 (** {1 Theory of strings}
   2
   3 This file provides a theory over strings. It contains all the
   4 predicates and functions currently supported by the smt-solvers CVC4
   5 and Z3.
   6
   7 *)
   8
   9 (** {2 String operations} *)
  10
  11 module String
  12
  13   use int.Int
  14
  15   (** The type `string` is built-in. Indexes for strings start at `0`. *)
  16
  17   (** The following functions/predicates are available in this theory:
  18   {h
  19 <style type="text/css">td{padding:0 15px 0 15px;}</style>
  20 <table cellpadding="5" cellspacing="0" border="1" style="border-collapse:collapse">
  21   <tr><th> Description </th> <th> Name </th> <th> Arguments </th> <th> Result </th> </tr>
  22   <tr>
  23     <td/> Concatenate
  24       <td/> <code> concat <code>      <td/> string string       <td/> string
  25   </tr><tr>
  26     <td/> Length
  27       <td/><code> length </code>     <td/> string              <td/> int
  28   </tr><tr>
  29     <td/> Get string of length 1
  30       <td/><code> s_at </code>       <td/> string int           <td/> string
  31   </tr><tr>
  32     <td/> Get substring
  33       <td/><code> substring </code> <td/> string int int       <td/> string
  34   </tr><tr>
  35     <td/> Index of substring
  36       <td/><code> indexof </code>   <td/> string string int    <td/> int
  37   </tr><tr>
  38     <td/> Replace first occurrence
  39       <td/><code> replace </code>   <td/> string string string <td/> string
  40   </tr><tr>
  41     <td/> Replace all occurrences
  42       <td/><code> replaceall </code><td/> string string string <td/> string
  43   </tr><tr>
  44     <td/> String to int
  45       <td/><code> to_int </code>     <td/> string               <td/> int
  46   </tr><tr>
  47     <td/> Int to string
  48       <td/><code> from_int </code>   <td/> int                  <td/> string
  49   </tr><tr>
  50     <td/> Comparison less than
  51       <td/><code> lt </code>         <td/> string string <td/>
  52   </tr><tr>
  53     <td/> Comparison less or equal than
  54       <td/><code> le </code>         <td/> string string <td/>
  55   </tr><tr>
  56     <td/> Check if it a prefix
  57       <td/><code> prefixof </code>  <td/> string string <td/>
  58   </tr><tr>
  59     <td/> Check if it is a suffix
  60       <td/><code> suffixof </code>  <td/> string string <td/>
  61   </tr><tr>
  62     <td/> Check if contains
  63       <td/><code> contains </code>  <td/> string string <td/>
  64   </tr><tr>
  65     <td/> Check if it is a digit
  66       <td/><code> is_digit </code>   <td/> string <td/>
  67   </tr>
  68
  69
  70 </table>}
  71    *)
  72
  73
  74   constant empty : string = ""
  75   (** the empty string. *)
  76
  77   function concat string string : string
  78   (** `concat s1 s2` is the concatenation of `s1` and `s2`.  *)
  79
  80   axiom concat_assoc: forall s1 s2 s3.
  81     concat (concat s1 s2) s3 = concat s1 (concat s2 s3)
  82
  83   axiom concat_empty: forall s.
  84     concat s empty = concat empty s = s
  85
  86   function length string : int
  87   (** `length s` is the length of the string `s`. *)
  88
  89   (* axiom length_nonneg: forall s. length s >= 0 *)
  90
  91   axiom length_empty: length "" = 0
  92
  93   axiom length_concat: forall s1 s2.
  94     length (concat s1 s2) = length s1 + length s2
  95
  96   predicate lt string string
  97   (** `lt s1 s2` returns `True` iff `s1` is lexicographically smaller
  98   than `s2`. *)
  99
 100   axiom lt_empty: forall s.
 101     s <> empty -> lt empty s
 102
 103   axiom lt_not_com: forall s1 s2.
 104     lt s1 s2 -> not (lt s2 s1)
 105
 106   axiom lt_ref: forall s1. not (lt s1 s1)
 107
 108   axiom lt_trans: forall s1 s2 s3.
 109     lt s1 s2 && lt s2 s3 -> lt s1 s3
 110
 111   predicate le string string
 112   (** `le s1 s2` returns `True` iff `s1` is lexicographically smaller
 113   or equal than `s2`. *)
 114
 115   axiom le_empty: forall s.
 116     le empty s
 117
 118   axiom le_ref: forall s1.
 119     le s1 s1
 120
 121   axiom lt_le: forall s1 s2.
 122     lt s1 s2 -> le s1 s2
 123
 124   axiom lt_le_eq: forall s1 s2.
 125     le s1 s2 -> lt s1 s2 || s1 = s2
 126
 127   axiom le_trans: forall s1 s2 s3.
 128     le s1 s2 && le s2 s3 -> le s1 s3
 129
 130   function s_at string int : string
 131   (** `s_at s i` is:
 132
 133        (1) `empty`, if either `i < 0` or `i >= length s`;
 134
 135        (2) the string of length `1` containing the character of
 136            position `i` in string `s`, if `0 <= i < length s`. *)
 137
 138   axiom at_out_of_range: forall s i.
 139     i < 0 || i >= length s -> s_at s i = empty
 140
 141   axiom at_empty: forall i.
 142     s_at empty i = empty
 143
 144   axiom at_length: forall s i.
 145     let j = s_at s i in
 146     if 0 <= i < length s then length j = 1 else length j = 0
 147
 148   axiom concat_at: forall s1 s2.
 149     let s = concat s1 s2 in
 150     forall i. (0 <= i < length s1 -> s_at s i = s_at s1 i) &&
 151               (length s1 <= i < length s -> s_at s i = s_at s2 (i - length s1))
 152
 153   function substring string int int : string
 154   (** `substring s i x` is:
 155
 156       (1) the `empty` string if `i < 0`, `i >= length s`, or `x <= 0`;
 157
 158       (2) the substring of `s` starting at `i` and of length
 159           `min x (length s - i)`. *)
 160
 161   axiom substring_out_of_range: forall s i x.
 162     i < 0 || i >= length s -> substring s i x = empty
 163
 164   axiom substring_of_length_zero_or_less: forall s i x.
 165     x <= 0 -> substring s i x = ""
 166
 167   axiom substring_of_empty: forall i x.
 168     substring "" i x = ""
 169
 170   axiom substring_smaller: forall s i x.
 171     length (substring s i x) <= length s
 172
 173   axiom substring_smaller_x: forall s i x.
 174     x >= 0 -> length (substring s i x) <= x
 175
 176   axiom substring_length: forall s i x.
 177     x >= 0 && 0 <= i < length s ->
 178       if i + x > length s then
 179         length (substring s i x) = length s - i
 180       else length (substring s i x) = x
 181
 182   axiom substring_at: forall s i.
 183     s_at s i = substring s i 1
 184
 185   axiom substring_substring:
 186     forall s ofs len ofs' len'.
 187     0 <= ofs <= length s -> 0 <= len -> ofs + len <= length s ->
 188     0 <= ofs' <= len -> 0 <= len' -> ofs' + len' <= len ->
 189     substring (substring s ofs len) ofs' len' = substring s (ofs + ofs') len'
 190
 191   axiom concat_substring:
 192     forall s ofs len len'.
 193     0 <= ofs <= length s -> 0 <= len -> ofs + len <= length s ->
 194     0 <= len' -> 0 <= ofs + len + len' <= length s ->
 195     concat (substring s ofs len) (substring s (ofs+len) len') =
 196     substring s ofs (len + len')
 197
 198   predicate prefixof string string
 199   (** `prefixof s1 s2` is `True` iff `s1` is a prefix of `s2`. *)
 200
 201   axiom prefixof_substring: forall s1 s2.
 202     prefixof s1 s2 <-> s1 = substring s2 0 (length s1)
 203
 204   axiom prefixof_concat: forall s1 s2.
 205     prefixof s1 (concat s1 s2)
 206
 207   axiom prefixof_empty: forall s2.
 208     prefixof "" s2
 209
 210   axiom prefixof_empty2: forall s1.
 211     s1 <> empty -> not (prefixof s1 "")
 212
 213   predicate suffixof string string
 214   (** `suffixof s1 s2` is `True` iff `s1` is a suffix of `s2`. *)
 215
 216   axiom suffixof_substring: forall s1 s2.
 217     suffixof s1 s2 <-> s1 = substring s2 (length s2 - length s1) (length s1)
 218
 219   axiom suffixof_concat: forall s1 s2.
 220     suffixof s2 (concat s1 s2)
 221
 222   axiom suffixof_empty: forall s2.
 223     suffixof "" s2
 224
 225   axiom suffixof_empty2: forall s1.
 226     s1 <> empty -> not (suffixof s1 "")
 227
 228   predicate contains string string
 229   (** `contains s1 s2` is `True` iff `s1` contains `s2`. *)
 230
 231   axiom contains_prefixof: forall s1 s2.
 232     prefixof s1 s2 -> contains s2 s1
 233
 234   axiom contains_suffixof: forall s1 s2.
 235     suffixof s1 s2 -> contains s2 s1
 236
 237   axiom contains_empty: forall s2.
 238     contains "" s2 <-> s2 = empty
 239
 240   axiom contains_empty2: forall s1.
 241     contains s1 ""
 242
 243   axiom contains_substring: forall s1 s2 i.
 244     substring s1 i (length s2) = s2 -> contains s1 s2
 245
 246   (*** The following should hold, but are not proved by SMT provers *)
 247   (*** axiom substring_contains: forall s1 s2.
 248     contains s1 s2 -> exists i. substring s1 i (length s2) = s2 *)
 249
 250   axiom contains_concat: forall s1 s2.
 251     contains (concat s1 s2) s1 && contains (concat s1 s2) s2
 252
 253   axiom contains_at: forall s1 s2 i.
 254     s_at s1 i = s2 -> contains s1 s2
 255
 256   (*** The following should hold, but are not proved by SMT provers *)
 257   (*** axiom at_contains: forall s1 s2.
 258     contains s1 s2 && length s2 = 1 -> exists i. s_at s1 i = s2 *)
 259
 260   function indexof string string int : int
 261   (** `indexof s1 s2 i` is:
 262
 263       (1) the first occurrence of `s2` in `s1` after `i`, if `0 <= i <=
 264           length s1` (note: the result is `i`, if `s2 = empty` and `0
 265           <= i <= length s1`);
 266
 267       (2) `-1`, if `i < 0`, `i > length s1`, or `0 <= i <= length s1`
 268           and `s2` does not occur in `s1` after `i`.  *)
 269
 270   axiom indexof_empty: forall s i.
 271     0 <= i <= length s -> indexof s "" i = i
 272
 273   axiom indexof_empty1: forall s i.
 274     let j = indexof "" s i in
 275     j = -1 || (s = "" && i = j = 0)
 276
 277   axiom indexof_contains: forall s1 s2.
 278     let j = indexof s1 s2 0 in
 279     contains s1 s2 ->
 280       0 <= j <= length s1 && substring s1 j (length s2) = s2
 281
 282   axiom contains_indexof: forall s1 s2 i.
 283     indexof s1 s2 i >= 0 -> contains s1 s2
 284
 285   axiom not_contains_indexof: forall s1 s2 i.
 286     not (contains s1 s2)  -> indexof s1 s2 i = -1
 287
 288   axiom substring_indexof: forall s1 s2 i.
 289     let j = indexof s1 s2 i in
 290     j >= 0 -> substring s1 j (length s2) = s2
 291
 292   axiom indexof_out_of_range: forall i s1 s2.
 293     not (0 <= i <= length s1) -> indexof s1 s2 i = -1
 294
 295   axiom indexof_in_range: forall s1 s2 i.
 296     let j = indexof s1 s2 i in
 297     0 <= i <= length s1 -> j = -1 || i <= j <= length s1
 298
 299   axiom indexof_contains_substring: forall s1 s2 i.
 300     0 <= i <= length s1 && contains (substring s1 i (length s1 - i)) s2 ->
 301       i <= indexof s1 s2 i <= length s1
 302
 303   function replace string string string : string
 304   (** `replace s1 s2 s3` is:
 305
 306       (1) `concat s3 s1`, if `s2 = empty`;
 307
 308       (2) the string obtained by replacing the first occurrence of `s2`
 309           (if any) by `s3` in `s1`. *)
 310
 311   axiom replace_empty: forall s1 s3.
 312     replace s1 "" s3 = concat s3 s1
 313
 314   axiom replace_not_contains: forall s1 s2 s3.
 315     not (contains s1 s2) -> replace s1 s2 s3 = s1
 316
 317   axiom replace_empty2: forall s2 s3.
 318     let s4 = replace empty s2 s3 in
 319     if s2 = empty then s4 = s3 else s4 = empty
 320
 321   axiom replace_substring_indexof: forall s1 s2 s3.
 322     let j = indexof s1 s2 0 in
 323     replace s1 s2 s3 =
 324       if j < 0 then s1 else
 325         concat (concat (substring s1 0 j) s3)
 326                (substring s1 (j + length s2) (length s1 - j - length s2))
 327
 328   (*** Not in SMT-LIB standard, but in CVC4 *)
 329   function replaceall string string string : string
 330   (** `replaceall s1 s2 s3` is:
 331
 332       (1) `s1`, if `s2 = empty`;
 333
 334       (2) the string obtained by replacing all occurrences of `s2` by
 335           `s3` in `s1`. *)
 336
 337   axiom replaceall_empty1: forall s1 s3.
 338     replaceall s1 "" s3 = s1
 339
 340   axiom not_contains_replaceall: forall s1 s2 s3.
 341     not (contains s1 s2) -> replaceall s1 s2 s3 = s1
 342
 343   function to_int string : int
 344   (** `to_int s` is:
 345
 346       (1) an `int` consisting on the digits of `s`, if `s` contains
 347           exclusively ascii characters in the range 0x30 ... 0x39;
 348
 349       (2) `-1`, if `s` contains a character that is not in the range
 350           0x30 ... 0x39. *)
 351
 352   axiom to_int_gt_minus_1: forall s. to_int s >= -1
 353
 354   axiom to_int_empty: to_int "" = -1
 355
 356   (*** The following lemmas should hold, but CVC4 is not able to prove them *)
 357   (*** axiom to_int_only_digits: forall s.
 358         s <> empty &&
 359           (forall i. 0 <= i < length s -> le "0" (s_at s i) && le (s_at s i) "9")
 360             -> to_int s >= 0 *)
 361
 362   (*** axiom to_int_lt_0: forall s i.
 363          0 <= i < length s && lt (s_at s i) "0"
 364              -> to_int s = -1 *)
 365
 366   (*** In SMT-Lib now *)
 367   predicate is_digit (s:string) = 0 <= to_int s <= 9 && length s = 1
 368   (** `is_digit s` returns `True` iff `s` is of length `1` and
 369       corresponds to a decimal digit, that is, to a code point in the
 370       range 0x30 ... 0x39 *)
 371
 372   function from_int int : string
 373   (** `from_int i` is:
 374
 375       (1) the corresponding string in the decimal notation if `i >= 0`;
 376
 377       (2) `empty`, if `i < 0`. *)
 378
 379   axiom from_int_negative: forall i.
 380     i < 0 <-> from_int i = empty
 381
 382   axiom from_int_to_int: forall i.
 383     if i >= 0 then to_int (from_int i) = i else to_int (from_int i) = -1
 384
 385 end
 386
 387 (** {2 Characters} *)
 388
 389 module Char
 390
 391   use String
 392   use int.Int
 393
 394   (** to be mapped into the OCaml char type. *)
 395   type char = abstract {
 396     contents: string;
 397   } invariant {
 398     length contents = 1
 399   }
 400
 401   axiom char_eq: forall c1 c2.
 402     c1.contents = c2.contents -> c1 = c2
 403
 404   function code char : int
 405
 406   axiom code: forall c. 0 <= code c < 256
 407
 408   function chr (n: int) : char
 409
 410   axiom code_chr: forall n. 0 <= n < 256 -> code (chr n) = n
 411
 412   axiom chr_code: forall c. chr (code c) = c
 413
 414   function get (s: string) (i: int) : char
 415
 416   axiom get: forall s i.
 417     0 <= i < length s -> (get s i).contents = s_at s i
 418
 419   axiom substring_get:
 420     forall s ofs len i.
 421     0 <= ofs <= length s -> 0 <= len -> ofs + len <= length s -> 0 <= i < len ->
 422     get (substring s ofs len) i = get s (ofs + i)
 423
 424   lemma concat_first: forall s1 s2.
 425     let s3 = concat s1 s2 in
 426     forall i. 0 <= i < length s1 ->
 427       get s3 i = get s1 i
 428
 429   lemma concat_second: forall s1 s2.
 430     let s3 = concat s1 s2 in
 431     forall i. length s1 <= i < length s1 + length s2 ->
 432       get s3 i = get s2 (i - length s1)
 433
 434   function ([]) (s: string) (i: int) : char = get s i
 435
 436   predicate eq_string (s1 s2: string) = length s1 = length s2 &&
 437     (forall i. 0 <= i < length s1 -> get s1 i = get s2 i)
 438
 439   axiom extensionality [@W:non_conservative_extension:N]:
 440     forall s1 s2. eq_string s1 s2 -> s1 = s2
 441
 442   meta extensionality predicate eq_string
 443
 444   function make (size: int) (v: char) : string
 445
 446   axiom make_length: forall size v. size >= 0 ->
 447     length (make size v) = size
 448
 449   axiom make_contents: forall size v. size >= 0 ->
 450     (forall i. 0 <= i < size -> get (make size v) i = v)
 451
 452 end
 453
 454 (** {3 Programming API}
 455
 456   The following program functions are mapped to OCaml's functions.
 457   See also module `io.StdIO`. *)
 458
 459 module OCaml
 460
 461   use int.Int
 462   use mach.int.Int63
 463   use String
 464   use Char
 465
 466   (* In OCaml max_string_length is 144_115_188_075_855_863 *)
 467
 468   val eq_char (c1 c2: char) : bool
 469     ensures { result <-> c1 = c2 }
 470
 471   val get (s: string) (i: int63) : char
 472     requires { 0 <= i < length s }
 473     ensures  { result = get s i }
 474
 475   let ([]) (s: string) (i: int63) : char
 476     requires { 0 <= i < length s }
 477     ensures  { result = get s i }
 478   = get s i
 479
 480   val code (c: char) : int63
 481     ensures { result = code c }
 482
 483   val chr (n: int63) : char
 484     requires { 0 <= n < 256 }
 485     ensures  { result = chr n }
 486
 487   val (=) (x y: string) : bool
 488     ensures { result <-> x = y }
 489
 490   val partial length (s: string) : int63
 491     ensures { result = length s >= 0 }
 492
 493   val sub (s: string) (start: int63) (len: int63) : string
 494     requires { 0 <= start <= length s }
 495     requires { 0 <= len <= length s - start }
 496     ensures  { result = substring s start len }
 497
 498   val concat (s1 s2: string) : string
 499     ensures  { result = concat s1 s2 }
 500
 501   val make (size: int63) (v: char) : string
 502     requires { 0 <= size }
 503     ensures  { result = make size v }
 504
 505 end
 506
 507 (** The following module is extracted to OCaml's Buffer *)
 508
 509 module StringBuffer
 510
 511   use int.Int
 512   use mach.int.Int63
 513   use String
 514   use Char
 515   use OCaml
 516
 517   type buffer = abstract {
 518     mutable str: string;
 519   }
 520   meta coercion function str
 521
 522   val create (_: int63) : buffer
 523     ensures { result.str = "" }
 524
 525   val length (b: buffer) : int63
 526     ensures { result = length b.str }
 527
 528   val contents (b: buffer) : string
 529     ensures { result = b.str }
 530
 531   val clear (b: buffer) : unit
 532     writes  { b }
 533     ensures { b.str = "" }
 534
 535   val reset (b: buffer) : unit
 536     writes  { b }
 537     ensures { b.str = "" }
 538
 539   val sub (b: buffer) (ofs len: int63) : string
 540     requires { 0 <= ofs /\ 0 <= len /\ ofs + len <= length b.str }
 541     ensures  { result = substring b.str ofs len }
 542
 543   val add_char (b: buffer) (c: char) : unit
 544     writes   { b }
 545     ensures  { b.str = concat (old b.str) c.Char.contents }
 546
 547   val add_string (b: buffer) (s: string) : unit
 548     writes   { b }
 549     ensures  { b.str = concat (old b.str) s }
 550
 551   val truncate (b: buffer) (n: int63) : unit
 552     requires { 0 <= n <= length b.str }
 553     writes   { b }
 554     ensures  { b.str = substring (old b.str) 0 n }
 555
 556 end
 557
 558 (** {2 String realization}
 559
 560 This module is intended for string realization. It clones the `String`
 561 module replacing axioms by goals.
 562
 563 *)
 564
 565 module StringRealization
 566
 567   clone export String
 568     with goal .
 569   (** trick to remove axioms from the `String` theory. See file
 570      `examples/stdlib/stringCheck.mlw` *)
 571
 572 end
 573
 574 (** {2 Regular expressions} *)
 575
 576 module RegExpr
 577
 578   use String as S
 579
 580   type re
 581   (** type for regular expressions *)
 582
 583   function to_re string : re
 584   (** string to regular expression injection *)
 585
 586   predicate in_re string re
 587   (** regular expression membership *)
 588
 589   function concat re re : re
 590   (** regular expressions concatenation, left associativity *)
 591
 592   function union re re : re
 593   (** regular expressions union, left associativity *)
 594
 595   function inter re re : re
 596   (** regular expressions intersection, left associativity *)
 597
 598   function star re : re
 599   (** Kleene closure *)
 600
 601   function plus re : re
 602   (** Kleene cross *)
 603   (*** forall re. plus re = concat re (star re) *)
 604
 605   constant none : re
 606   (** the empty set of strings *)
 607
 608   constant allchar : re
 609   (** the set of all strings of length 1 *)
 610
 611   constant all : re = star allchar
 612   (** the set of all strings *)
 613
 614   function opt re : re
 615   (** regular expression option *)
 616   (*** forall re. opt re = union re (to_re "") *)
 617
 618   function range string string : re
 619   (** `range s1 s2` is the set of singleton strings such that all
 620   element `s` of `range s1 s2` satisfies the condition `Str.<= s1 s`
 621   and `Str.<= s s2`. *)
 622
 623   function power int re : re
 624   (** `power n r` is the `n`th power of `r`; `n` must be an
 625       integer literal. *)
 626   (*** power 0 e = to_re ""
 627      power n e = concat e (power (n-1) e) *)
 628
 629   function loop int int re : re
 630   (** `loop n1 n2 r = if n1 > ne then none else
 631                     if n1 = n2 then power n1 r else
 632                     union (power n1 e) (loop (n1+1) n2 e)` *)
 633   (*** `n1` and `n2` must be literals. *)
 634
 635 end