#|
Copyright (C) 1994 by Yuan Yu.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Yuan Yu PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS IS"
WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT NOT
LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Yuan Yu BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST PROFITS,
LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT
OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT LIMITED TO LOSS
OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD
PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR
FOR ANY CLAIM BY ANY OTHER PARTY.
|#

Event: Start with the library "mc20-2" using the compiled version.

;          Proof of the Correctness of the STRRCHR Function
#|
This is part of our effort to verify the Berkeley string library.  The
Berkeley string library is widely used as part of the Berkeley Unix OS.
This is the source code of strrchr function in the Berkeley string library.
char *
strrchr(p, ch)
register const char *p;
       register char ch;
{
register const char *save;
for (save = NULL;; ++p) {
if (*p == ch)

save = p;
if (!*p)
return((char *)save);
}
/* NOTREACHED */
}
The MC68020 assembly code of the C function strrchr on SUN-3 is given as
follows.  This binary is generated by "gcc -O".
0x26c8 <strrchr>:       linkw fp,#0
0x26cc <strrchr+4>:     moveal fp@(8),a0
0x26d0 <strrchr+8>:     moveb fp@(15),d1
0x26d4 <strrchr+12>:    clrl d0
0x26d6 <strrchr+14>:    cmpb a0@,d1
0x26d8 <strrchr+16>:    bne 0x26dc <strrchr+20>
0x26da <strrchr+18>:    movel a0,d0
0x26dc <strrchr+20>:    tstb a0@
0x26de <strrchr+22>:    beq 0x26e4 <strrchr+28>
0x26e0 <strrchr+24>:    addqw #1,a0
0x26e2 <strrchr+26>:    bra 0x26d6 <strrchr+14>
0x26e4 <strrchr+28>:    unlk fp
0x26e6 <strrchr+30>:    rts
The machine code of the above program is:
<strrchr>:     0x4e56  0x0000  0x206e  0x0008  0x122e  0x000f  0x4280  0xb210
<strrchr+16>:  0x6602  0x2008  0x4a10  0x6704  0x5248  0x60f2  0x4e5e  0x4e75
'(78      86      0       0       32      110     0       8
  18      46      0       15      66      128     178     16
  102     2       32      8       74      16      103     4
  82      72      96      242     78      94      78      117)
|#
; in the logic, the above program is defined by (strrchr-code).

Definition: strrchr-code

= '(78 86 0 0 32 110 0 8 18 46 0 15 66 128 178 16 102 2
      32 8 74 16 103 4 82 72 96 242 78 94 78 117)
; the computation time of the program.

Definition: strrchr-t1 (i, n, lst, ch) = if i < n

then if get-nth (i, lst) = ch

then if get-nth (i, lst) = 0 then 7

else splus (7, strrchr-t1 (1 + i, n, lst, ch)) endif elseif get-nth (i, lst) = 0 then 6 else splus (6, strrchr-t1 (1 + i, n, lst, ch)) endif

else 0 endif

Definition: strrchr-t (n, lst, ch) = splus (4, strrchr-t1 (0, n, lst, ch))

; an induction hint.

Definition: strrchr-induct (s, i* , i, n, lst, ch, j* , j ) = if i < n

then if get-nth (i, lst) = ch

then if get-nth (i, lst) = 0 then t

else strrchr-induct (stepn (s, 7), add (32, i* , 1), 1 + i, n, lst, ch, i* ,

i) endif

elseif get-nth (i, lst) = 0 then t else strrchr-induct (stepn (s, 6),

add (32, i* , 1), 1 + i, n, lst, ch, j* , j ) endif

else t endif

; the preconditions of the initial state.

Definition: strrchr-statep (s, str, n, lst, ch) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s))

∧ rom-addrp (mc-pc (s), mc-mem (s), 32)

∧ mcode-addrp (mc-pc (s), mc-mem (s), strrchr-code) ∧ ram-addrp (sub (32, 4, read-sp (s)), mc-mem (s), 16) ∧ ram-addrp (str, mc-mem (s), n) ∧ mem-lst (1, str, mc-mem (s), n, lst) ∧ disjoint (sub (32, 4, read-sp (s)), 16, str, n) ∧ (str = read-mem (add (32, read-sp (s), 4), mc-mem (s), 4)) ∧ (ch = uread-mem (add (32, read-sp (s), 11), mc-mem (s), 1)) ∧ stringp (0, n, lst) ∧ (n ∈ N) ∧ uint-rangep (n, 32) ∧ (nat-to-uint (str) ≠ 0) ∧ uint-rangep (nat-to-uint (str) + n, 32))

; an intermediate state.

Definition: index-j (str, j* , j ) = if j then add (32, str, j* )

else 0 endif

Definition: strrchr-s0p (s, i* , i, str, n, lst, ch, j* , j ) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s)) ∧ rom-addrp (sub (32, 14, mc-pc (s)), mc-mem (s), 32) ∧ mcode-addrp (sub (32, 14, mc-pc (s)), mc-mem (s), strrchr-code) ∧ ram-addrp (read-an (32, 6, s), mc-mem (s), 16) ∧ ram-addrp (str, mc-mem (s), n) ∧ mem-lst (1, str, mc-mem (s), n, lst) ∧ disjoint (read-an (32, 6, s), 16, str, n) ∧ equal* (read-an (32, 0, s), add (32, str, i* )) ∧ (ch = nat-to-uint (read-dn (8, 1, s))) ∧ equal* (read-dn (32, 0, s), index-j (str, j* , j )) ∧ stringp (i, n, lst) ∧ (i < n) ∧ (i* ∈ N) ∧ nat-rangep (i* , 32) ∧ (i = nat-to-uint (i* )) ∧ (n ∈ N) ∧ uint-rangep (n, 32))

; from the initial state s to s0: s --> s0;

Theorem: strrchr-s-s0 strrchr-statep (s, str, n, lst, ch) → strrchr-s0p (stepn (s, 4), 0, 0, str, n, lst, ch, f, f)

Theorem: strrchr-s-s0-else strrchr-statep (s, str, n, lst, ch) → ((linked-rts-addr (stepn (s, 4)) = rts-addr (s))

∧ (linked-a6 (stepn (s, 4)) = read-an (32, 6, s))

∧ (read-rn (32, 14, mc-rfile (stepn (s, 4))) = sub (32, 4, read-sp (s))))

Theorem: strrchr-s-s0-rfile (strrchr-statep (s, str, n, lst, ch) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 4)))

= read-rn (oplen, rn, mc-rfile (s)))

Theorem: strrchr-s-s0-mem (strrchr-statep (s, str, n, lst, ch) ∧ disjoint (x, k, sub (32, 4, read-sp (s)), 16)) → (read-mem (x, mc-mem (stepn (s, 4)), k) = read-mem (x, mc-mem (s), k))

; from s0 to exit: s0 --> sn.
; base case 1. s0 --> sn, when lst[i] = ch and lst[i] = 0.

Theorem: strrchr-s0-sn-base1 (strrchr-s0p (s, i* , i, str, n, lst, ch, j* , j ) ∧ (get-nth (i, lst) ≠ ch) ∧ (get-nth (i, lst) = 0)) → ((mc-status (stepn (s, 6)) = 'running)

∧ (mc-pc (stepn (s, 6)) = linked-rts-addr (s))

∧ (read-dn (32, 0, stepn (s, 6)) = index-j (str, j* , j )) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 6))) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 6))) = add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (stepn (s, 6)), k) = read-mem (x, mc-mem (s), k)))

Theorem: strrchr-s0-sn-rfile-base1 (strrchr-s0p (s, i* , i, str, n, lst, ch, j* , j ) ∧ (get-nth (i, lst) ≠ ch) ∧ (get-nth (i, lst) = 0) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 6)))

= read-rn (oplen, rn, mc-rfile (s)))

; base case 2: s0 --> sn, when lst[i] =\= ch and lst[i] = 0.

Theorem: strrchr-s0-sn-base2 (strrchr-s0p (s, i* , i, str, n, lst, ch, j* , j ) ∧ (get-nth (i, lst) = ch)

∧ (get-nth (i, lst) = 0)) → ((mc-status (stepn (s, 7)) = 'running)

∧ (mc-pc (stepn (s, 7)) = linked-rts-addr (s)) ∧ (read-dn (32, 0, stepn (s, 7)) = add (32, str, i* )) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 7))) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 7)))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (stepn (s, 7)), k)

= read-mem (x, mc-mem (s), k)))

Theorem: strrchr-s0-sn-rfile-base2 (strrchr-s0p (s, i* , i, str, n, lst, ch, j* , j ) ∧ (get-nth (i, lst) = ch) ∧ (get-nth (i, lst) = 0) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 7)))

= read-rn (oplen, rn, mc-rfile (s)))

; induction case 1: s0 --> s0, when lst[i] = ch and lst[i] =\= 0.

Theorem: index-j-la j → (index-j (str, j* , j ) = add (32, str, j* ))

Theorem: strrchr-s0-s0-1 (strrchr-s0p (s, i* , i, str, n, lst, ch, j* , j ) ∧ (get-nth (i, lst) = ch) ∧ (get-nth (i, lst) ≠ 0)) → (strrchr-s0p (stepn (s, 7), add (32, i* , 1), 1 + i, str, n, lst, ch, i* , i)

∧ (read-rn (32, 14, mc-rfile (stepn (s, 7)))

= read-rn (32, 14, mc-rfile (s))) ∧ (linked-a6 (stepn (s, 7)) = linked-a6 (s)) ∧ (linked-rts-addr (stepn (s, 7)) = linked-rts-addr (s)) ∧ (read-mem (x, mc-mem (stepn (s, 7)), k)

= read-mem (x, mc-mem (s), k)))

Theorem: strrchr-s0-s0-rfile-1 (strrchr-s0p (s, i* , i, str, n, lst, ch, j* , j ) ∧ (get-nth (i, lst) = ch) ∧ (get-nth (i, lst) ≠ 0) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 7)))

= read-rn (oplen, rn, mc-rfile (s)))

; induction case 2: s0 --> s0, when lst[i] =\= ch and lst[i] =\= 0.

Theorem: strrchr-s0-s0-2 (strrchr-s0p (s, i* , i, str, n, lst, ch, j* , j ) ∧ (get-nth (i, lst) ≠ ch) ∧ (get-nth (i, lst) ≠ 0)) → (strrchr-s0p (stepn (s, 6), add (32, i* , 1), 1 + i, str, n, lst, ch, j* , j )

∧ (read-rn (32, 14, mc-rfile (stepn (s, 6))) = read-rn (32, 14, mc-rfile (s))) ∧ (linked-a6 (stepn (s, 6)) = linked-a6 (s)) ∧ (linked-rts-addr (stepn (s, 6)) = linked-rts-addr (s)) ∧ (read-mem (x, mc-mem (stepn (s, 6)), k) = read-mem (x, mc-mem (s), k)))

Theorem: strrchr-s0-s0-rfile-2 (strrchr-s0p (s, i* , i, str, n, lst, ch, j* , j ) ∧ (get-nth (i, lst) ≠ ch) ∧ (get-nth (i, lst) ≠ 0) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 6)))

= read-rn (oplen, rn, mc-rfile (s)))

; put together. s0 --> exit.

Theorem: strrchr-s0p-info strrchr-s0p (s, i* , i, str, n, lst, ch, j* , j ) → (((i < n) = t) ∧ (i ∈ N))

Theorem: strrchr-s0p-la ¬ strrchr-s0p (s, i* , f, str, n, lst, ch, j* , j )

Theorem: strrchr-s0-sn let sn be stepn (s, strrchr-t1 (i, n, lst, ch)) in strrchr-s0p (s, i* , i, str, n, lst, ch, j* , j ) → ((mc-status (sn) = 'running)

∧ (mc-pc (sn) = linked-rts-addr (s))

∧ (read-dn (32, 0, sn)

= if strrchr (i, n, lst, ch, j )

then add (32, str, strrchr* (i* , i, n, lst, ch, j* )) else 0 endif)

∧ (read-rn (32, 14, mc-rfile (sn)) = linked-a6 (s))

∧ (read-rn (32, 15, mc-rfile (sn))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (sn), k) = read-mem (x, mc-mem (s), k))) endlet

Event: Disable strrchr-s0p-info.

Theorem: strrchr-s0-sn-rfile (strrchr-s0p (s, i* , i, str, n, lst, ch, j* , j ) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, strrchr-t1 (i, n, lst, ch))))

= read-rn (oplen, rn, mc-rfile (s)))

; the correctness of strrchr.

Theorem: strrchr-correctness let sn be stepn (s, strrchr-t (n, lst, ch)) in strrchr-statep (s, str, n, lst, ch) → ((mc-status (sn) = 'running)

∧ (mc-pc (sn) = rts-addr (s)) ∧ (read-rn (32, 14, mc-rfile (sn))

= read-rn (32, 14, mc-rfile (s))) ∧ (read-rn (32, 15, mc-rfile (sn)) = add (32, read-sp (s), 4))

∧ (d2-7a2-5p (rn)

→ (read-rn (oplen, rn, mc-rfile (sn))

= read-rn (oplen, rn, mc-rfile (s))))

∧ (disjoint (x, k, sub (32, 4, read-sp (s)), 16) → (read-mem (x, mc-mem (sn), k)

= read-mem (x, mc-mem (s), k)))

∧ (read-dn (32, 0, sn)

= if strrchr (0, n, lst, ch, f)

then add (32, str, strrchr* (0, 0, n, lst, ch, f)) else 0 endif)) endlet

Event: Disable strrchr-t.

; strrchr* --> strrchr.

Theorem: strrchr*-strrchr (strrchr (i, n, lst, ch, j ) ∧ (i = nat-to-uint (i* )) ∧ nat-rangep (i* , 32) ∧ uint-rangep (n, 32)) → (nat-to-uint (strrchr* (i* , i, n, lst, ch, j* ))

= if j = f then strrchr (i, n, lst, ch, f) else strrchr (i, n, lst, ch, nat-to-uint (j* )) endif)

Theorem: strrchr-non-zerop-la let sn be stepn (s, strrchr-t (n, lst, ch)) in (strrchr-statep (s, str, n, lst, ch) ∧ nat-rangep (str, 32) ∧ (nat-to-uint (str) ≠ 0) ∧ uint-rangep (nat-to-uint (str) + n, 32) ∧ strrchr (0, n, lst, ch, f)) → (nat-to-uint (read-dn (32, 0, sn)) ≠ 0) endlet

Theorem: strrchr-non-zerop let sn be stepn (s, strrchr-t (n, lst, ch)) in (strrchr-statep (s, str, n, lst, ch) ∧ strrchr (0, n, lst, ch, f)) → (nat-to-uint (read-dn (32, 0, sn)) ≠ 0) endlet

Event: Disable strrchr*.

; some properties of the function strrchr.
; see file cstring.events.

Index

add, 3–8

d2-7a2-5p, 5–8 disjoint, 4, 5, 8

equal*, 4 evenp, 3, 4

get-nth, 3, 5–7

index-j, 4–6 index-j-la, 6

linked-a6, 5–7 linked-rts-addr, 5–7

mc-mem, 3–8 mc-pc, 3–8 mc-rfile, 5–8 mc-status, 3–8 mcode-addrp, 4 mem-lst, 4

nat-rangep, 4, 8, 9 nat-to-uint, 4, 8, 9

ram-addrp, 4 read-an, 4–7 read-dn, 4–9 read-mem, 4–8 read-rn, 5–8 read-sp, 4, 5, 8 rom-addrp, 3, 4 rts-addr, 5, 8

splus, 3 stepn, 3–9 stringp, 4 strrchr, 7–9 strrchr*, 7, 8 strrchr*-strrchr, 8 strrchr-code, 2, 4 strrchr-correctness, 8 strrchr-induct, 3 strrchr-non-zerop, 9 strrchr-non-zerop-la, 8 strrchr-s-s0, 4 strrchr-s-s0-else, 5 strrchr-s-s0-mem, 5 strrchr-s-s0-rfile, 5 strrchr-s0-s0-1, 6 strrchr-s0-s0-2, 7 strrchr-s0-s0-rfile-1, 6 strrchr-s0-s0-rfile-2, 7 strrchr-s0-sn, 7 strrchr-s0-sn-base1, 5 strrchr-s0-sn-base2, 5 strrchr-s0-sn-rfile, 8 strrchr-s0-sn-rfile-base1, 5 strrchr-s0-sn-rfile-base2, 6 strrchr-s0p, 4–8 strrchr-s0p-info, 7 strrchr-s0p-la, 7 strrchr-statep, 3–5, 8, 9 strrchr-t, 3, 8, 9 strrchr-t1, 2, 3, 7, 8 sub, 4, 5, 8

uint-rangep, 4, 8, 9 uread-mem, 4