Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 1066

Synopsis:        Soundness bug in PVS
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Fri Sep 10 10:30:08 -0700 2010
Originator:      "Munoz, Cesar Augusto (LARC-D320)"
Release:         PVS 4.2
Organization:    nasa.gov
Environment:
System:
Architecture:

Description:
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: quoted-printable

Hi Sam,

By running our examples, Mauricio and I discovered a soundness bug in PVS.
See attached dump file.

My version of PVS is: PVS Version 4.2 - Allegro CL Enterprise Edition 8.1
[Mac OS X (Intel)] (Jul   22, 2008 4:19). The bug occurs with and without
the latest patch (which I include for completeness).

The error seems to be in GRIND, which manages to prove the first lemma whic=
h
is false. Surprisingly, the second lemma cannot be proved with GRIND.

bug : THEORY
BEGIN

bug : LEMMA
FORALL (m: int, (n: int | m /=3D 0 OR n /=3D 0)):
abs(m) > abs(n) AND NOT (m =3D 0 OR n =3D 0) AND NOT abs(m) =3D abs(=
n)
IMPLIES
abs(rem(abs(n))(abs(m))) > abs(n)

rem : LEMMA
FORALL (m: nat, (n: nat | m /=3D 0 OR n /=3D 0)):
m > n AND NOT (m =3D 0 OR n =3D 0) AND NOT m =3D n
IMPLIES
rem(n)(m) > n

miracle : LEMMA
FALSE

END bug

Unrelated to the soundness bug, we have also discovered a bug in the comman=
d
show-declaration-tccs. To recreate this bug, just issue the comment M-x
show-declaration-tccs on the definition Fibonacci in the following

theory.test : THEORY
BEGIN

factorial(n:posint) : RECURSIVE nat =3D
IF n <=3D 1 THEN 1
ELSE n*factorial(n-1)
ENDIF
MEASURE n

fibonacci(n:int) : RECURSIVE nat =3D
COND n >=3D 2 -> fibonacci(n-1) + fibonacci(n-2),
n =3D 1  -> fibonacci(0),
n =3D 0  -> 1,
ELSE   -> fibonacci(0)
ENDCOND
MEASURE n=20
END test

You will get the message:

There is garbage at the end of your file or string:
Line 34:    (disjointness
^

Curiously, in both cases, we spent a few hours blaming our code for these
behaviors until we discovered that they were actually PVS errors.

Cesar
--=20
Cesar A. Munoz                             NASA Langley Research Center
Cesar.A.Munoz@nasa.gov                     Bldg. 1220  Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234

Content-Type: text/plain; name="bug.dmp"
Content-Description: bug.dmp
Content-Disposition: attachment; filename="bug.dmp"; size=6503;
creation-date="Fri, 10 Sep 2010 10:57:46 GMT";
modification-date="Fri, 10 Sep 2010 10:57:46 GMT"
Content-Transfer-Encoding: base64

CiUlIFBWUyBWZXJzaW9uIDQuMiAtIEFsbGVncm8gQ0wgRW50ZXJwcmlzZSBFZGl0aW9uIDguMSBb
TWFjIE9TIFggKEludGVsKV0gKEp1bCAyMiwgMjAwOCA0OjE5KQolJSA4LjEgW01hYyBPUyBYIChJ
bnRlbCldIChKdWwgMjIsIDIwMDggNDoxOSkKJCQkYnVnLnB2cwpidWcgOiBUSEVPUlkKQkVHSU4K
CiAgYnVnIDogTEVNTUEKICAgIEZPUkFMTCAobTogaW50LCAobjogaW50IHwgbSAvPSAwIE9SIG4g
Lz0gMCkpOgogICAgICAgYWJzKG0pID4gYWJzKG4pIEFORCBOT1QgKG0gPSAwIE9SIG4gPSAwKSBB
TkQgTk9UIGFicyhtKSA9IGFicyhuKQogICAgICAgSU1QTElFUwogICAgICAgIGFicyhyZW0oYWJz
MCBPUiBuID0gMCkgQU5EIE5PVCBtID0gbgogICAgICAgSU1QTElFUwogICAgICAgICByZW0obiko
bSkgPiBuCgogIG1pcmFjbGUgOiBMRU1NQQogICAgRkFMU0UKCkVORCBidWcKCiQkJGJ1Zy5wcmYK
KGJ1ZwogKGJ1Z19UQ0MxIDAKICAoYnVnX1RDQzEtMSBuaWwgMzQ5MzExNjAzNSAzNDkzMTE2NjYw
ICgiIiAoc3VidHlwZS10Y2MpIG5pbCBuaWwpCiAgIHVuY2hlY2tlZAogICAoKGJvb2xlYW4gbm9u
ZW1wdHktdHlwZS1kZWNsIG5pbCBib29sZWFucyBuaWwpCiAgICAoYm9vbCBub25lbXB0eS10eXBl
LWVxLWRlY2wgbmlsIGJvb2xlYW5zIG5pbCkKICAgIChOT1QgY29uc3QtZGVjbCAiW2Jvb2wgLT4g
Ym9vbF0iIGJvb2xlYW5zIG5pbCkKICAgIChudW1iZXIgbm9uZW1wdHktdHlwZS1kZWNsIG5pbCBu
dW1iZXJzIG5pbCkKICAgIChudW1iZXJfZmllbGRfcHJlZCBjb25zdC1kZWNsICJbbnVtYmVyIC0+
IGJvb2xlYW5dIiBudW1iZXJfZmllbGRzCiAgICAgbmlsKQogICAgKG51bWJlcl9maWVsZCBub25l
bXB0eS10eXBlLWZyb20tZGVjbCBuaWwgbnVtYmVyX2ZpZWxkcyBuaWwpCiAgICAocmVhbF9wcmVk
IGNvbnN0LWRlY2wgIltudW1iZXJfZmllbGQgLT4gYm9vbGVhbl0iIHJlYWxzIG5pbCkKICAgIChy
ZWFsIG5vbmVtcHR5LXR5cGUtZnJvbS1kZWNsIG5pbCByZWFscyBuaWwpCiAgICAocmF0aW9uYWxf
cHJlZCBjb25zdC1kZWNsICJbcmVhbCAtPiBib29sZWFuXSIgcmF0aW9uYWxzIG5pbCkKICAgIChy
YXRpb25hbCBub25lbXB0eS10eXBlLWZyb20tZGVjbCBuaWwgcmF0aW9uYWxzIG5pbCkKICAgIChp
bnRlZ2VyX3ByZWQgY29uc3QtZGVjbCAiW3JhdGlvbmFsIC0+IGJvb2xlYW5dIiBpbnRlZ2VycyBu
aWwpCiAgICAoaW50IG5vbmVtcHR5LXR5cGUtZXEtZGVjbCBuaWwgaW50ZWdlcnMgbmlsKQogICAg
KE9SIGNvbnN0LWRlY2wgIltib29sLCBib29sIC0+IGJvb2xdIiBib29sZWFucyBuaWwpCiAgICAo
Lz0gY29uc3QtZGVjbCAiYm9vbGVhbiIgbm90ZXF1YWwgbmlsKQogICAgKHJlYWxfbHRfaXNfc3Ry
aWN0X3RvdGFsX29yZGVyIG5hbWUtanVkZ2VtZW50CiAgICAgIihzdHJpY3RfdG90YWxfb3JkZXI/
W3JlYWxdKSIgcmVhbF9wcm9wcyBuaWwpCiAgICAoaW50X2Fic19pc19ub25uZWcgYXBwbGljYXRp
b24tanVkZ2VtZW50ICJ7ajogbm9ubmVnX2ludCB8IGogPj0gaX0iCiAgICAgcmVhbF9kZWZzIG5p
ICIoc3RyaWN0X3RvdGFsX29yZGVyP1tyZWFsXSkiIHJlYWxfcHJvcHMgbmlsKSkKICAgNDcgNDAg
bmlsIG5pbCkpCiAoYnVnIDAKICAoYnVnLTEgbmlsIDM0OTMxMTYwNDMgMzQ5MzExNjE0OQogICAo
IiIgKHNrb3NpbXApICgoIiIgKGdyaW5kKSBuaWwgbmlsKSkgbmlsKSB1bmNoZWNrZWQKICAgKChh
YnMgY29uc3QtZGVjbCAie246IG5vbm5lZ19yZWFsIHwgbiA+PSBtIEFORCBuID49IC1tfSIgcmVh
bF9kZWZzCiAgICAgICAgIG5pbCkKICAgIChyZWFsX2x0X2lzX3N0cmljdF90b3RhbF9vcmRlciBu
YW1lLWp1ZGdlbWVudAogICAgICIoc3RyaWN0X3RvdGFsX29yZGVyP1tyZWFsXSkiIHJlYWxfcHJv
cHMgbmlsKQogICAgKG1pbnVzX2ludF9pc19pbnQgYXBwbGljYXRpb24tanVkZ2VtZW50ICJpbnQi
ZGdlbWVudAogICAgICIoc3RyaWN0X3RvdGFsX29yZGVyP1tyZWFsXSkiIHJlYWxfcHJvcHMgbmls
KQogICAgKG11bHRfZGl2aWRlczIgYXBwbGljYXRpb24tanVkZ2VtZW50ICIoZGl2aWRlcyhtKSki
IGRpdmlkZXMgbmlsKQogICAgKG11bHRfZGl2aWRlczEgYXBwbGljYXRpb24tanVkZ2VtZW50ICIo
ZGl2aWRlcyhuKSkiIGRpdmlkZXMgbmlsKQogICAgKGludF9hYnNfaXNfbm9ubmVnIGFwcGxpY2F0
aW9uLWp1ZGdlbWVudCAie2o6IG5vbm5lZ19pbnQgfCBqID49IGl9IgogICAgIHJlYWxfZGVmcyBu
aWwpKQogICA0NzI1IDEzMCB0IHNob3N0YWspKQogKHJlbV9UQ0MxIDAKICAocmVtX1RDQzEtMSBu
aWwgMzQ5MzExNjgwMyBuaWwgKCIiIChzdWJ0eXBlLXRjYykgbmlsIG5pbCkgbmlsIG5pbCBuaWwK
ICAgbmlsIG5pbCBuaWwpKQogKHJlbSAwCiAgICAgIChyZW0tMSBuaWwgMzQ5MzExNjgwMyAzNDkz
MTE2ODA4CiAgICAgICAoIiIgKGxlbW1hICJidWciKQogICAgICAgICgoIiIgKHNrb3NpbXApCiAg
ICAgICAgICAoKCIiIChpbnN0IC0xICJtITEiICJuITEiKSAoKCIiIChncmluZCkgbmlsIG5pbCkp
IG5pbCkpIG5pbCkpCiAgICAgICAgbmlsKQogICAgICAgcHJvdmVkCiAgICAgICAoKGJ1ZyBmb3Jt
dWxhLWRlY2wgbmlsIGJ1ZyBuaWwpCiAgICAgICAgKGludF9hYnNfaXNfbm9ubmVnIGFwcGxpY2F0
aW9uLWp1ZGdlbWVudAogICAgICAgICAie2o6IG5vbm5lZ19pbnQgfCBqID49IGl9IiByZWFsX2Rl
ZnMgbmlsKQogICAgICAgIChudW1iZXIgbm9uZW1wdHktdHlwZS1kZWNsIG5pbCBudW1iZXJzIG5p
bCkKICAgICAgICAoYm9vbGVhbiBub25lbXB0eS10eXBlLWRlY2wgbmlsIGJvb2xlYW5zIG5pbCkK
ICAgICAgICAobnVtYmVyX2ZpZWxkX3ByZWQgY29uc3QtZGVjbCAiW251bWJlciAtPiBib29sZWFu
XSIKICAgICAgICAgbnVtYmVyX2ZpZWxkcyBuaWwpCiAgICAgICAgKG51bWJlcl9maWVsZCBub25l
bXB0eS10eXBlLWZyb20tZGVjbCBuaWwgbnVtYmVyX2ZpZWxkcyBuaWwpCiAgICAgICAgKHJlYWxf
cHJlZCBjb25zdC1kZWNsICJbbnVtYmVyX2ZpZWxkIC0+IGJvb2xlYW5dIiByZWFscyBuaWwpCiAg
ICAgICAgKHJlYWwgbm9uZW1wdHktdHlwZS1mcm9tLWRlY2wgbmlsIHJlYWxzIG5pbCkKICAgICAg
ICAocmF0aW9uYWxfcHJlZCBjb25zdC1kZWNsICJbcmVhbCAtPiBib29sZWFuXSIgcmF0aW9uYWxz
IG5pbCkKICAgICAgICAocmF0aW9uYWwgbm9uZW1wdHktdHlwZS1mcm9tLWRlY2wgbmlsIHJhdGlv
bmFscyBuaWwpCiAgICAgICAgKGludGVnZXJfcHJlZCBjb25zdC1kZWNsICJbcmF0aW9uYWwgLT4g
Ym9vbGVhbl0iIGludGVnZXJzIG5pbCkKICAgICAgICAoaW50IG5vbmVtcHR5LXR5cGUtZXEtZGVj
bCBuaWwgaW50ZWdlcnMgbmlsKQogICAgICAgIChib29sIG5vbmVtcHR5LXR5cGUtZXEtZGVjbCBu
aWwgYm9vbGVhbnMgbmlsKQogICAgICAgICg+PSBjb25zdC1kZWNsICJib29sIiByZWFscyBuaWwp
CiAgICAgICAgKG5hdCBub25lbXB0eS10eXBlLWVxLWRlY2wgbmlsIG5hdHVyYWxudW1iZXJzIG5p
bCkKICAgICAgICAoT1IgY29uc3QtZGVjbCAiW2Jvb2wsIGJvb2wgLT4gYm9vbF0iIGJvb2xlYW5z
IG5pbCkKICAgICAgICAoLz0gY29uc3QtZGVjbCAiYm9vbGVhbiIgbm90ZXF1YWwgbmlsKQogICAg
ICAgIChhYnMgY29uc3QtZGVjbCAie246IG5vbm5lZ19yZWFsIHwgbiA+PSBtIEFORCBuID49IC1t
fSIKICAgICAgICAgICAgIHJlYWxfZGVmcyBuaWwpCiAgICAgICAgKHJlYWxfZ3RfaXNfc3RyaWN0
X3RvdGFsX29yZGVyIG5hbWUtanVkZ2VtZW50CiAgICAgICAgICIoc3RyaWN0X3RvdGFsX29yZGVy
P1tyZWFsXSkiIHJlYWxfcHJvcHMgbmlsKQogICAgICAgIChyZWFsX2x0X2lzX3N0cmljdF90b3Rh
bF0pIiByZWFsX3Byb3BzIG5pbCkKICAgICAgICAobWludXNfaW50X2lzX2ludCBhcHBsaWNhdGlv
bi1qdWRnZW1lbnQgImludCIgaW50ZWdlcnMgbmlsKQogICAgICAgIChtdWx0X2RpdmlkZXMyIGFw
cGxpY2F0aW9uLWp1ZGdlbWVudCAiKGRpdmlkZXMobSkpIiBkaXZpZGVzCiAgICAgICAgIG5pbCkK
ICAgICAgICAobXVsdF9kaXZpZGVzMSBhcHBsaWNhdGlvbi1qdWRnZW1lbnQgIihkaXZpZGVzKG4p
KSIgZGl2aWRlcwogICAgICAgICBuaWwpKQogICAgICAgMjEzMyAxMDAgdCBuaWwpKQogKG1pcmFj
bGUgMAogIChtaXJhY2xlLTEgbmlsIDM0OTMxMTY2NjkgMzQ5MzExNzA4OAogICAoIiIgKGNhc2Ug
InJlbSgxKSgyKSA+IDEiKQogICAgKCgiMSIgKHR5cGVwcmVkICJyZW0oMSkoMikiKSAoKCIxIiAo
YXNzZXJ0KSBuaWwgbmlsKSkgbmlsKQogICAgICgiMiIgKGxlbW1hICJyZW0iKSAoKCIyIiAoaW5z
dD8pICgoIjIiIChhc3NlcnQpIG5pbCBuaWwpKSBuaWwpKQogICAgICBuaWwpKQogICAgbmlsKQog
ICBwcm92ZWQKICAgKChyZW0gZm9ybXVsYS1kZWNsIG5pbCBidWcgbmlsKQogICAgKE9SIGNvbnN0
LWRlY2wgIltib29sLCBib29sIC0+IGJvb2xdIiBib29sZWFucyBuaWwpCiAgICAoLz0gY29uc3Qt
ZGVjbCAiYm9vbGVhbiIgbm90ZXF1YWwgbmlsKQogICAgKE5PVCBjb25zdC1kZWNsICJbYm9vbCAt
PiBib29sXSIgYm9vbGVhbnMgbmlsKQogICAgKHJlYWxfbHRfaXNfc3RyaWN0X3RvdGFsX29yZGVy
IG5hbWUtanVkZ2VtZW50CiAgICAgIihzdHJpY3RfdG90YWxfb3JkZXI/W3JlYWxdKSIgcmVhbF9w
cm9wcyBuaWwpCiAgICAocmVhbF9ndF9pc19zdHJpY3RfdG90YWxfb3JkZXIgbmFtZS1qdWRnZW1l
bnQKICAgICAiKHN0cmljdF90b3RhbF9vcmRlcj9bcmVhbF0pIiByZWFsX3Byb3BzIG5pbCkKICAg
IChtdWx0X2RpdmlkZXMxIGFwcGxpY2F0aW9uLWp1ZGdlbWVudCAiKGRpdmlkZXMobikpIiBkaXZp
ZGVzIG5pbCkKICAgIChtdWx0X2RpdmlkZXMyIGFwcGxpY2F0aW9uLWp1ZGdlbWVudCAiKGRpdmlk
ZXMobSkpIiBkaXZpZGVzIG5pbCkKICAgIChudW1iZXIgbm9uZW1wdHktdHlwZS1kZWNsIG5pbCBu
dW1iZXJzIG5pbCkKICAgIChib29sZWFuIG5vbmVtcHR5LXR5cGUtZGVjbCBuaWwgYm9vbGVhbnMg
bmlsKQogICAgKG51bWJlcl9maWVsZF9wcmVkIGNvbnN0LWRlY2wgIltudW1iZXIgLT4gYm9vbGVh
bl0iIG51bWJlcl9maWVsZHMKICAgICBuaWwpCiAgICAobnVtYmVyX2ZpZWxkIG5vbmVtcHR5LXR5
cGUtZnJvbS1kZWNsIG5pbCBudW1iZXJfZmllbGRzIG5pbCkKICAgIChyZWFsX3ByZWQgY29uc3Qt
ZGVjbCAiW251bWJlcl9maWVsZCAtPiBib29sZWFuXSIgcmVhbHMgbmlsKQogICAgKHJlYWwgbm9u
ZW1wdHktdHlwZS1mcm9tLWRlY2wgbmlsIHJlYWxzIG5pbCkKICAgIChib29sIG5vbmVtcHR5LXR5
cGUtZXEtZGVjbCBuaWwgYm9vbGVhbnMgbmlsKQogICAgKD4gY29uc3QtZGVjbCAiYm9vbCIgcmVh
bHMgbmlsKQogICAgKHJhdGlvbmFsX3ByZWQgY29uc3QtZGVjbCAiW3JlYWwgLT4gYm9vbGVhbl0i
IHJhdGlvbmFscyBuaWwpCiAgICAocmF0aW9uYWwgbm9uZW1wdHktdHlwZS1mcm9tLWRlY2wgbmls
IHJhdGlvbmFscyBuaWwpCiAgICAoaW50ZWdlcl9wcmVkIGNvbnN0LWRlY2wgIltyYXRpb25hbCAt
PiBib29sZWFuXSIgaW50ZWdlcnMgbmlsKQogICAgKGludCBub25lbXB0eS10eXBlLWVxLWRlY2wg
bmlsIGludGVnZXJzIG5pbCkKICAgICg+PSBjb25zdC1kZWNsICJib29sIiByZWFscyBuaWwpCiAg
ICAobm9ubmVnX2ludCBub25lbXB0eS10eXBlLWVxLWRlY2wgbmlsIGludGVnZXJzIG5pbCkKICAg
IChwb3NuYXQgbm9uZW1wdHktdHlwZS1lcS1kZWNsIG5pbCBpbnRlZ2VycyBuaWwpCiAgICAobmF0
IG5vbmVtcHR5LXR5cGUtZXEtZGVjbCBuaWwgbmF0dXJhbG51bWJlcnMgbmlsKQogICAgKDwgY29u
c3QtZGVjbCAiYm9vbCIgcmVhbHMgbmlsKQogICAgKG1vZCBub25lbXB0eS10eXBlLWVxLWRlY2wg
bmlsIGV1Y2xpZGVhbl9kaXZpc2lvbiBuaWwpCiAgICAoPSBjb25zdC1kZWNsICJbVCwgVCAtPiBi
b29sZWFuXSIgZXF1YWxpdGllcyBuaWwpCiAgICAobnVtZmllbGQgbm9uZW1wdHktdHlwZS1lcS1k
ZWNsIG5pbCBudW1iZXJfZmllbGRzIG5pbCkKICAgICgrIGNvbnN0LWRlY2wgIltudW1maWVsZCwg
bnVtZmllbGQgLT4gbnVtZmllbGRdIiBudW1iZXJfZmllbGRzIG5pbCkKICAgICgqIGNvbnN0LWRl
Y2wgIltudW1maWVsZCwgbnVtZmllbGQgLT4gbnVtZmllbGRdIiBudW1iZXJfZmllbGRzIG5pbCkK
ICAgIChyZW0gY29uc3QtZGVjbCAie3I6IG1vZChiKSB8IEVYSVNUUyBxOiB4ID0gYiAqIHEgKyBy
fSIKICAgICAgICAgbW9kdWxvX2FyaXRobWV0aWMgbmlsKSkKICAgNjg5NjcgNDAgdCBzaG9zdGFr
KSkpCgo=

Content-Type: application/octet-stream; name="patch.lisp"
Content-Description: patch.lisp
Content-Disposition: attachment; filename="patch.lisp"; size=6049;
creation-date="Fri, 10 Sep 2010 10:57:46 GMT";
modification-date="Fri, 10 Sep 2010 10:57:46 GMT"
Content-Transfer-Encoding: base64

KGRlZnVuIHBhcnNlLXJld3JpdGUtbmFtZSAoZm9ybSBiYW5ncy1hbGxvd2VkPyAmb3B0aW9uYWwg
YmFuZ3MpCiAgKHVubGVzcyAob3IgKHN0cmluZ3AgZm9ybSkKICAgICAgICAgICAgICAoc3ltYm9s
cCBmb3JtKQogICAgICAgICAgICAgIChpbnRlZ2VycCBmb3JtKQogICAgICAgICAgICAgIChyZXdy
aXRlLW5hbWU/IGZvcm0pKQogICAgKGVycm9yLWZvcm1hdC1pZiAifiVJbGxlZ2FsIHJld3JpdGUg
bmFtZTogfmEiIGZvcm0pKQogIChsZXQqICgocmV3cml0ZSAocGMtcGFyc2UgZm9ybSAncmV3cml0
ZS1uYW1lLW9yLWZudW0pKQogICAgICAgICAocmV3cml0ZS1uYW1lCiAgICAgICAgICAodHlwZWNh
c2UgcmV3cml0ZQogICAgICAgICAgICAobGF6eS1yZXdyaXRlLW5hbWUKICAgICAgICAgICAgIChj
YXNlIGJhbmdzCiAgICAgICAgICAgICAgICghIChjaGFuZ2UtY2xhc3MgcmV3cml0ZSAnZWFnZXIt
cmV3cml0ZS1uYW1lKSkKICAgICAgICAgICAgICAgKCEhIChjaGFuZ2UtY2xhc3MgcmV3cml0ZSAn
bWFjcm8tcmV3cml0ZS1uYW1lKSkKICAgICAgICAgICAgICAgKHQgcmV3cml0ZSkpKQogICAgICAg
ICAgICAobGF6eS1mbnVtLXJld3JpdGUKICAgICAgICAgICAgIChjYXNlIGJhbmdzCiAgICAgICAg
ICAgICAgICghIChjaGFuZ2UtY2xhc3MgcmV3cml0ZSAnZWFnZXItZm51bS1yZXdyaXRlKSkKICAg
ICAgICAgICAgICAgKCEhIChjaGFuZ2UtY2xhc3MgcmV3cml0ZSAnbWFjcm8tZm51bS1yZXdyaXRl
KSkKICAgICAgICAgICAgICAgKHQgcmV3cml0ZSkpKQogICAgICAgICAgICAodAogICAgICAgICAg
ICAgKHVubGVzcyBiYW5ncy1hbGxvd2VkPwogICAgICAgICAgICAgICAoZXJyb3ItZm9ybWF0LWlm
CiAgICAgICAgICAgICAgICAifiVEbyBub3QgbWl4IHBhcmVucyBhbmQgISdzIGluIHJld3JpdGUg
bmFtZXMiKSkKICAgICAgICAgICAgIHJld3JpdGUpKSkpCiAgICAodW5sZXNzIChvciAoZm51bS1y
ZXdyaXRlPyByZXdyaXRlLW5hbWUpCiAgICAgICAgICAgICAgICAocmVzb2x1dGlvbnMgcmV3cml0
ZS1uYW1lKSkKICAgICAgKHR5cGVjaGVjayByZXdyaXRlLW5hbWUpKQogICAgcmV3cml0ZS1uYW1l
KSkKCihkZWZ1biBpbnN0YWxsLXJld3JpdGUtcmVzIChyZXMgbmFtZSBmbWxhIGFsd2F5cz8pICAg
ICAgICAgICAgCiAgKG11bHRpcGxlLXZhbHVlLWJpbmQgKGxocyByaHMgaHlwKQogICAgICAoc3Bs
aXQtcmV3cml0ZSBmbWxhKQogICAgKGxldCogKChyZXMgKG9yIChpcy1yZXMtcmV3cml0ZSByZXMp
IHJlcykpCiAgICAgICAgICAgKGxocy1mcmVldmFycyAoZnJlZXZhcnMgbGhzKSkKICAgICAgICAg
ICAocmhzLWZyZWV2YXJzIChmcmVldmFycyByaHMpKQogICAgICAgICAgIChoeXAtZnJlZXZhcnMg
KGZyZWV2YXJzIGh5cCkpCiAgICAgICAgICAgKG9wKiAob3BlcmF0b3IqIGxocykpCiAgICAgICAg
ICAgKGhhc2huYW1lIChhdXRvLXJld3JpdGUtaGFzaG5hbWUgb3AqKSkKICAgICAgICAgICAoZGVj
bCAoaWYgKHR5cGVwIGhhc2huYW1lICduYW1lLWV4cHIpCiAgICAgICAgICAgICAgICAgICAgIChk
ZWNsYXJhdGlvbiBoYXNobmFtZSkKICAgICAgICAgICAgICAgICAgICAgaGFzaG5hbWUpKSkgOzso
YnJlYWsgImluc3RhbGwtcmV3cml0ZS1yZXMiKQogICAgICAoY29uZAogICAgICAgKChudWxsIGhh
c2huYW1lKQogICAgICAgIChlcnJvci1mb3JtYXQtaWYgIn4lQ2FuJ3QgcmV3cml0ZSB1c2luZyB+
aHMtZnJlZXZhcnMgbGhzLWZyZWV2YXJzCiAgICAgICAgICAgICAgICAgICAgICA6dGVzdCAjJ3Rj
LWVxKSkKICAgICAgICAoZXJyb3ItZm9ybWF0LWlmICJ+JUNhbid0IHJld3JpdGUgdXNpbmcgfmE6
IG5vbi1MSFMgZnJlZXZhcnMgaW4gUkhTLiIgbmFtZSApKQogICAgICAgKChub3QgKHN1YnNldHAg
aHlwLWZyZWV2YXJzIGxocy1mcmVldmFycwogICAgICAgICAgICAgICAgICAgICAgOnRlc3QgIyd0
Yy1lcSkpCiAgICAgICAgKGVycm9yLWZvcm1hdC1pZiAifiVDYW4ndCByZXdyaXRlIHVzaW5nIH5h
ZXNvbHV0aW9uPyByZXMpCiAgICAgICAgICAgICAoZml4cG9pbnQtZGVjbD8gKGRlY2xhcmF0aW9u
IHJlcykpKQogICAgICAgIChlcnJvci1mb3JtYXQtaWYgIn4lQ2FuJ3QgcmV3cml0ZSB1c2luZyB+
YTogKGNvKWluZHVjdGl2ZSBkZWZpbml0aW9uIGNhbm5vdCBiZSB1c2VkLiIgbmFtZSkpCiAgICAg
ICAodAogICAgICAgICh1bmxlc3MgKGNvbnNwIHJlcykgOzsoNi4xNi45NSlhdm9pZHMgYW50ZWNl
ZGVudCByZXdyaXRlcwogICAgICAgICAgKHR5cGVjaGVjayAobW9kdWxlLWluc3RhbmNlIHJlcykg
OnRjY3MgJ2FsbCkpCiAgICAgICAgOztOU0goNi4xNC45NSk6IGFib3ZlIHR5cGVjaGVjayBuZWVk
ZWQgdG8gZ2VuZXJhdGUKICAgICAgICA7O2Fzc3VtaW5nIFRDQ1MuIAogICAgICAgIChwdXNobmV3
CiAgICAgICAgIChtYWtlLWluc3RhbmNlICdyZXdyaXRlCiAgICAgICAgICAgOmxocyBsaHMKICAg
ICAgICAgICA6cmhzIHJocwogICAgICAgICAgIDpoeXAgaHlwCiAgICAgICAgICAgOnJlcyByZXMp
CiAgICAgICAgIChnZXRoYXNoIGRlY2wKICAgICAgICAgICAgICAgICAgKmF1dG8tcmV3cml0ZXMq
KQogICAgICAgICA6dGVzdCAjJyhsYW1iZGEgKHggeSkodGMtZXEgKHJlcyB4KShyZXMgeSkpKSkK
ICAgICAgICAocHVzaG5ldyByZXMgKmFsbC1yZXdyaXRlcy1uYW1lcyopIDs7ZG9uJ3QgbmVlZCB0
Yy1lcQogICAgICAgIDs7ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgKCphdXRvLXJld3Jp
dGVzKikKICAgICAgICAoY29uZCAoKGFuZCAoZXEgYWx3YXlzPyAnISEpIDs7TlNIKDUuOC45OCkg
aW5zZXJ0ZWQgbWFjcm8gY2FzZQogICAgICAgICAgICAgICAgICAgIChub3QgKGFuZCAocmVzb2x1
dGlvbj8gcmVzKSA7O05TSCgxMi4xLjk1KQogICAgICAgICAgICAgICAgICAgICAgICAgICAgICAo
ZGVmLWRlY2w/IChkZWNsYXJhdGlvbiByZXMpKSkpKQogICAgICAgICAgICAgICAocHVzaG5ldyBy
ZXMgKm1hY3JvLW5hbWVzKikKICAgICAgICAgICAgICAgOzs6dGVzdCAjJ3RjLWVxCiAgICAgICAg
ICAgICAgIChzZXRxICphdXRvLXJld3JpdGVzLW5hbWVzKgogICAgICAgICAgICAgICAgICAgICAo
cmVtb3ZlIHJlcyAqYXV0by1yZXdyaXRlcy1uYW1lcyopKQogICAgICAgICAgICAgICAoc2V0cSAq
YXV0by1yZXdyaXRlcyEtbmFtZXMqCiAgICAgICAgICAgICAgICAgICAgIChyZW1vdmUgcmVzICph
dXRvLXJld3JpdGVzIS1uYW1lcyopKQogICAgICAgICAgICAgICA7Ozp0ZXN0ICMndGMtZXEKICAg
ICAgICAgICAgICAgKGZvcm1hdC1pZiAifiVJbnN0YWxsaW5nIG1hY3JvKCEhKSB+YX5AWyB+YX5d
IgogICAgICAgICAgICAgICAgICAgICAgICAgIChpZiAocmVzb2x1dGlvbj8gcmVzKQogICAgICAg
ICAgICAgICAgICAgICAgICAgICAgICAocmVzb2x1dGlvbi1zdHJpbmcgcmVzKQogICAgICAgICAg
KHJlc29sdXRpb24/IHJlcykKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChub3QgKGZ1
bGx5LWluc3RhbnRpYXRlZD8gcmVzKSkKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICIo
YWxsIGluc3RhbmNlcykiKSkpCiAgICAgICAgICAgICAgKChhbmQgYWx3YXlzPyA7O05TSCgxMC43
Ljk1KSBkZWNsIC0+IChkZWNsYXJhdGlvbiByZXMpCiAgICAgICAgICAgICAgICAgICAgKG5vdCAo
YW5kIChyZXNvbHV0aW9uPyByZXMpIDs7TlNIKDEyLjEuOTUpCiAgICAgICAgICAgICAgICAgICAg
ICAgICAgICAgIChkZWYtZGVjbD8gKGRlY2xhcmF0aW9uIHJlcykpKSkpCiAgICAgICAgICAgICAg
IChwdXNobmV3IHJlcyAqYXV0by1yZXdyaXRlcyEtbmFtZXMqKQogICAgICAgICAgICAgICA7Ozp0
ZXN0ICMndGMtZXEKICAgICAgICAgICAgICAgKHNldHEgKmF1dG8tcmV3cml0ZXMtbmFtZXMqCiAg
ICAgICAgICAgICAgICAgICAgIChyZW1vdmUgcmVzICphdXRvLXJld3JpdGVzLW5hbWVzKikpCiAg
ICAgICAgICAgICAgIChzZXRxICptYWNyby1uYW1lcyoKICAgICAgICAgICAgICAgICAgICAgKHJl
bW92ZSByZXMgKm1hY3JvLW5hbWVzKikpCiAgICAgICAgICAgICAgIDs7OnRlc3QgIyd0Yy1lcQog
ICAgICAgICAgICAgICAoZm9ybWF0LWlmICJ+JUluc3RhbGxpbmcgcmV3cml0ZSBydWxlKCEpIH5h
fkBbIH5hfl0iCiAgICAgICAgICAgICAgICAgICAgICAgICAgKGlmIChyZXNvbHV0aW9uPyByZXMp
CiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChyZXNvbHV0aW9uLXN0cmluZyByZXMpCiAg
ICAgICAgICAgICAgICAgICAgICAgICAgICAgIG5hbWUpCiAgICAgICAgICAgICAgICAgICAgICAg
ICAgKGFuZCAocmVzb2x1dGlvbj8gcmVzKQogICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
KG5vdCAoZnVsbHktaW5zdGFudGlhdGVkPyByZXMpKQogICAgICAgICAgICAgICAgICAgICAgICAg
ICAgICAgIihhbGwgaW5zdGFuY2VzKSIpKSkKICAgICAgICAgICAgICAodCAocHVzaG5ldyByZXMg
KmF1dG8tcmV3cml0ZXMtbmFtZXMqKQogICAgICAgICAgICAgICAgIDs7OnRlc3QgIyd0Yy1lcQog
ICAgICAgICAgICAgICAgIChzZXRxICphdXRvLXJld3JpdGVzIS1uYW1lcyoKICAgICAgICAgICAg
ICAgICAgICAgICAocmVtb3ZlIHJlcyAqYXV0by1yZXdyaXRlcyEtbmFtZXMqKSkKICAgICAgICAg
ICAgICAgICAoc2V0cSAqbWFjcm8tbmFtZXMqCiAgICAgICAgICAgICAgICAgICAgICAgKHJlbW92
ZSByZXMgKm1hY3JvLW5hbWVzKikpCiAgICAgICAgICAgICAgICAgOzs6dGVzdCAjJ3RjLWVxCiAg
ICAgICAgICAgICAgICAgKGZvcm1hdC1pZiAifiVJbnN0YWxsaW5nIHJld3JpdGUgcnVsZSB+YX5A
WyB+YX5dIgogICAgICAgICAgICAgICAgICAgICAgICAgICAgKGlmIChyZXNvbHV0aW9uPyByZXMp
CiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChyZXNvbHV0aW9uLXN0cmluZyByZXMpCiAg
ICAgICAgICAgICAgICAgICAgICAgICAgICAgIG5hbWUpCiAgICAgICAgICAgICAgICAgICAgICAg
ICAgICAoYW5kIChyZXNvbHV0aW9uPyByZXMpCiAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
ICAobm90IChmdWxseS1pbnN0YW50aWF0ZWQ/IHJlcykpCiAgICAgICAgICAgICAgICAgICAgICAg
ICAgICAgICAiKGFsbCBpbnN0YW5jZXMpIikpKSkKICAgICAgICAoc2V0ZiAoZ2V0aGFzaCAocmV3
cml0ZS1kZWNsYXJhdGlvbiBoYXNobmFtZSkgKmF1dG8tcmV3cml0ZXMtb3BzKikgdCkKICAgICAg
ICA7Oyhmb3JtYXQtaWYgIn4lSW5zdGFsbGluZyByZXdyaXRlIHJ1bGUgfmEiIG5hbWUpCiAgICAg
ICAgKSkpKSkKCihkZWZ1biByZXNvbHV0aW9uLXN0cmluZyAocmVzKQogIChmb3JtYXQgbmlsICJ+
QDx+QFt+YUB+XX5hfkBbfkl+PFt+O35Ae35Xfl4sIH46X359fjtdfjo+fl1+QFt+SX48e3t+O35A
e35Xfl4sIH46X359fjt9fX46Pn5dfkBbLn5hfl1+Oj4iCiAgICAoYW5kIChtb2R1bGUtaW5zdGFu
Y2UgcmVzKSAobGlicmFyeSAobW9kdWxlLWluc3RhbmNlIHJlcykpKQogICAgKGFuZCAobW9kdWxl
LWluc3RhbmNlIHJlcykgKGlkIChtb2R1bGUtaW5zdGFuY2UgcmVzKSkpCiAgICAoYW5kIChtb2R1
bGUtaW5zdGFuY2UgcmVzKSAoYWN0dWFscyAobW9kdWxlLWluc3RhbmNlIHJlcykpKQogICAgKGFu
ZCAobW9kdWxlLWluc3RhbmNlIHJlcykgKG1hcHBpbmdzIChtb2R1bGUtaW5zdGFuY2UgcmVzKSkp
CiAgICAod2hlbiAoZGVjbGFyYXRpb24gcmVzKSAoaWQgKGRlY2xhcmF0aW9uIHJlcykpKQogICAg
KHdoZW4gKGRlY2xhcmF0aW9uIHJlcykKICAgICAgKGlmIChlcSAoa2luZC1vZiAoZGVjbGFyYXRp
b24gcmVzKSkgJ2V4cHIpCiAgICAgICAgICAob3IgKHR5cGUgcmVzKSAodHlwZSAoZGVjbGFyYXRp
b24gcmVzKSkpCiAgICAgICAgICAoa2luZC1vZiAoZGVjbGFyYXRpb24gcmVzKSkpKSkpCgogICAg
ICAgICAKCg==