Miscellanious Crashes #542

joe-hauns · 2024-04-05T10:15:34Z

Doing some randomized testing I ran into a couple of miscellanious crashes. Many of them are related to parsing. In some cases we just do not support what's being parsed, in some cases it's an actual crash. I decided I'll make an issue here so we can dicuss all of these crashes, and decide how to fix them, or how to exit more gracefully than crashing:

Bug 1:

Files:
- ITP/ITP236_4.p
- ITP/ITP285_4.p
- ITP/ITP266_4.p
- ITP/ITP235_4.p
- ITP/ITP220_4.p
Options: none
Issue: some crash in the TPTP parser

Example:

❯ ./cmake-build/vampire-master-Debug/clang/vampire TPTP-v8.2.0/Problems/ITP/ITP285_4.p
% Running in auto input_syntax mode. Trying TPTP
Condition in file /Users/jo/projects/vampire/master/Kernel/SortHelper.cpp, line 95 violated:
!subst.isEmpty() || (result.isTerm() && (result.term()->isSuper() || result.term()->ground()))
----- stack dump -----
Version : Vampire 4.8 (commit 23d7e9c3b on 2024-03-22 08:41:08 +0000)
call stack: 0x182bce0e0 0x10055eb04 0x100b7545c 0x100b74f14 0x100b74344 0x100b9ccc4 0x100b9dce4 0x100ba0de4 0x100bb053c 0x100bb1084 0x1006c74f0 0x1006c7244 0x10056c99c 0x10056ec44
(use '--traceback on' to get a human-readable stack trace)
----- end of stack dump -----

Bug 2

Files:

SWW/SWW508_5.p

Options: -fda 4

Issue: Crash in function definition introduction

Example:

❮ ./cmake-build/vampire-master-Debug/clang/vampire  TPTP-v8.2.0/Problems/SWW/SWW508_5.p -fdi 4

% Running in auto input_syntax mode. Trying TPTP
Condition env.signature->functionArity(function) == arity in file /Users/jo/projects/vampire/master/Kernel/Term.cpp, line 833 was violated, as:
env.signature->functionArity(function) == 2
arity == 1
----- stack dump -----
Version : Vampire 4.8 (commit 23d7e9c3b on 2024-03-22 08:41:08 +0000)
call stack: 0x182bce0e0 0x102216d28 0x102214fc0 0x102213e00 0x1022110b8 0x10265b220 0x10265b478 0x1022fe9e8 0x1026631ac 0x102662ef4 0x102662c5c 0x10266262c 0x10264c90c 0x10264c96c 0x10246db44 0x10246d780 0x102668c30 0x1025e0408 0x1025dfccc 0x1025def4c 0x10238f194 0x10221c714 0x102226c44
(use '--traceback on' to get a human-readable stack trace)
----- end of stack dump -----

Bug 3

Files:

RAL/RAL034^1.p
GEO/GEO423^1.p
RAL/RAL034^1.p
GEO/GEO423^1.p
ANA/ANA047^1.p
NUN/NUN036^1.p
GEO/GEO359^1.p
LIN/LIN003^1.p
GEO/GEO370^1.p
MSC/MSC030^1.p
GEO/GEO363^1.p
RAL/RAL033^1.p
RAL/RAL041^1.p
Options: --input_syntax tptp
Issue: We return a Parser Error on valid TPTP because of a feature (HOL + Theories) that we don't support. Here we should actually return a User Error instead, right?

Example:

❯ ./cmake-build/vampire-master-Debug/clang/vampire TPTP-v8.2.0/Problems/GEO/GEO423^1.p  --input_syntax tptp
Parsing Error on line 1737: Vampire higher-order is currently not compatible with theory reasoning

Bug 4:

Files:

SYO/SYO378^5.p
SYO/SYO304^5.p
SEU/SEU563^1.p
SEU/SEU642^1.p
SEU/SEU587^1.p
ITP/ITP104^1.p
ITP/ITP161^2.p
SEU/SEU596^1.p
ITP/ITP059^2.p
SEU/SEU781^1.p
SEU/SEU814^1.p
ITP/ITP275^3.p
ITP/ITP186^2.p
SEU/SEU570^1.p
ITP/ITP120^2.p
SEU/SEU570^1.p
ITP/ITP057^1.p
SEU/SEU625^1.p
ITP/ITP193^2.p
DAT/DAT162^1.p
SEU/SEU708^1.p
ITP/ITP185^1.p
SEU/SEU632^1.p
ITP/ITP220^1.p
PRO/PRO020^1.p
PRO/PRO023^1.p
SWW/SWW474^3.p
ITP/ITP219^4.p
ITP/ITP206^4.p
ITP/ITP186^2.p
ITP/ITP185^1.p
COM/COM202^1.p
ITP/ITP186^2.p
ITP/ITP276^3.p
ITP/ITP290^3.p
ITP/ITP294^2.p
ITP/ITP273^2.p
ITP/ITP221^3.p
ITP/ITP290^3.p
ITP/ITP287^1.p
ITP/ITP283^3.p
SEU/SEU625^1.p
SEU/SEU587^1.p
SEU/SEU596^1.p
SEU/SEU708^1.p
SEU/SEU781^1.p
ITP/ITP057^1.p
ITP/ITP104^1.p
ITP/ITP120^2.p
SYO/SYO304^5.p
ITP/ITP161^2.p
ITP/ITP193^2.p
SEU/SEU642^1.p
PRO/PRO020^1.p
SYO/SYO378^5.p
SEU/SEU632^1.p
DAT/DAT162^1.p
SEU/SEU814^1.p
ITP/ITP275^3.p
ITP/ITP206^4.p
ITP/ITP059^2.p
ITP/ITP220^1.p
SEU/SEU563^1.p
ITP/ITP273^2.p
ITP/ITP276^3.p
COM/COM202^1.p
ITP/ITP219^4.p
ITP/ITP294^2.p
SWW/SWW474^3.p
PRO/PRO023^1.p
ITP/ITP221^3.p
ITP/ITP287^1.p
ITP/ITP283^3.p
ITP/ITP279^2.p
ITP/ITP254^1.p
ITP/ITP214^1.p
ITP/ITP227^3.p
SEU/SEU645^1.p
ITP/ITP238^1.p
ITP/ITP268^2.p
Options: --input_syntax tptp
Issue: Vampire reports that the sorts of an equality do not agree during parsing. I guess this is a bug in vampire and the input files are actually valid tptp (considering how many times this issue occurrs).
Example:

❮ ./cmake-build/vampire-master-Debug/clang/vampire TPTP-v8.2.0/Problems/SYO/SYO378^5.p --input_syntax tptp
Parsing Error on line 46: Cannot create equality between terms of different types.
c is $i
(^[X0 : $i] : (X0)) is $i > $i

Bug 5:

Files:

DAT/DAT118^1.p
DAT/DAT118^1.p
ITP/ITP207^3.p
DAT/DAT118^1.p
DAT/DAT118^1.p
ITP/ITP207^3.p

Options: --input_syntax tptp
Issue Vampire reports that some term is not of boolean sort but used as formula. Again I reckon the TPTP is valid and there is some bug in vampire.
Example:

❯ ./cmake-build/vampire-master-Debug/clang/vampire  TPTP-v8.2.0/Problems/DAT/DAT118^1.p --input_syntax tptp
Parsing Error on line 578: Non-boolean term X28 of sort coindu1593790203_llist(X0) is used in a formula context

Bug 6:

Files:

PUZ/PUZ091^5.p

Options: -newcnf on
Issue: crash somewhere in newcnf due to some boolean term not being special.

Example:

❮ ./cmake-build/vampire-master-Debug/clang/vampire /Users/jo/data/TPTP-v8.2.0/Problems/PUZ/PUZ091^5.p -newcnf on
% Running in auto input_syntax mode. Trying TPTP
Condition in file /Users/jo/projects/vampire/master/Shell/NewCNF.cpp, line 1139 violated:
term->isSpecial()
Value of term->toString() is: cEARNEST
----- stack dump -----
Version : Vampire 4.8 (commit 23d7e9c3b on 2024-03-22 08:41:08 +0000)
call stack: 0x182bce0e0 0x1040bad28 0x1040b8fc0 0x1040b7e00 0x1040b5050 0x1040b4ee0 0x10468a070 0x10468b15c 0x104538304 0x104538ce0 0x1045425ac 0x104148b90 0x1040cac44
(use '--traceback on' to get a human-readable stack trace)
----- end of stack dump -----

Bug 7:

Files:

ITP/ITP086^2.p
SCT/SCT211_5.p
LCL/LCL808_5.p
ITP/ITP164^1.p
ITP/ITP030^2.p
SEV/SEV300^5.p
SEV/SEV293^5.p
COM/COM152^1.p
COM/COM155^1.p
ITP/ITP128^2.p
Issue: Crash in the TPTP parser.
Options: None
Example:

❮ ./cmake-build/vampire-master-Debug/clang/vampire '/Users/jo/data/TPTP-v8.2.0/Problems/ITP/ITP086^2.p'
% Running in auto input_syntax mode. Trying TPTP
Condition in file /Users/jo/projects/vampire/master/Parse/TPTP.cpp, line 1940 violated:
lhsSort.isTerm() && lhsSort.term()->arity() == 2
Value of lhs.toString() is: X4
Value of lhsSort.toString() is: $i
----- stack dump -----
Version : Vampire 4.8 (commit 23d7e9c3b on 2024-03-22 08:41:08 +0000)
call stack: 0x182bce0e0 0x102c3ab04 0x10325145c 0x103250f14 0x103250344 0x103278cc4 0x103279d5c 0x103280194 0x102db84e0 0x102c4ac44
(use '--traceback on' to get a human-readable stack trace)
----- end of stack dump -----

The text was updated successfully, but these errors were encountered:

joe-hauns · 2024-04-05T11:05:48Z

Bug 8

Files:
- NUM/NUM930_5.p
- NUM/NUM950_5.p
- NUM/NUM955_5.p
- NUM/NUM979_5.p
- NUM/NUM977_5.p
- LCL/LCL841_5.p
- LCL/LCL822_5.p
- LCL/LCL794_5.p
Issue: Polymorphism well-sortedness check fails for some formula:
Options: -fdi 41

> ./bin/vampire-23d7e9c3b61479bc14e1687f917c22f80dc7c8f1-Debug-z3 -fdi 41 TPTP-v8.2.0//Problems/NUM/NUM930_5.p
% Running in auto input_syntax mode. Trying TPTP
Condition in file /home/jschoiss/.vampire-benchexec/build/repos/vampire/Indexing/TermSharing.cpp, line 177 violated:
_wellSortednessCheckingDisabled || SortHelper::areImmediateSortsValidPoly(t)
Value of t->toString() is: one_one(fFalse)
----- stack dump -----
Version : Vampire 4.8 (commit 23d7e9c3b61 on 2024-03-22 08:41:08 +0000)
call stack: 0x406f0a 0x2690a99 0x40a036 0x4090a7 0x4084b1 0x407522 0x7a4c52 0x7a4ff9 0x4eca59 0x7aa92e 0x7aa6eb 0x7aa472 0x7a9efa 0x797d24 0x79a142 0x621f11 0x621a60 0x7adede 0x73ac73 0x73a9b9 0x73a532 0x56467b 0x663506 0x486d07 0x416598
(use '--traceback on' to get a human-readable stack trace)
----- end of stack dump -----

joe-hauns · 2024-04-05T11:50:39Z

Bug 9

Files:

SYO/SYO500_8.008.p
Issue: Unsound saturation.
Options: --decode lrs+11_5309:524288_anc=all:drc=encompass:foolp=on:gs=on:kws=precedence:nm=13:nwc=5.0321:spb=units_1

Example:

./bin/vampire-23d7e9c3b61479bc14e1687f917c22f80dc7c8f1-Debug-z3 --input_syntax tptp --decode lrs+11_5309:524288_anc=all:drc=encompass:foolp=on:gs=on:kws=precedence:nm=13:nwc=5.0321:spb=units_1 --time_limit 3 /TPTP-v8.2.0//Problems/SYO/SYO500_8.008.p

(...)

% # SZS output end Saturation.
Condition in file /home/jschoiss/.vampire-benchexec/build/repos/vampire/Shell/UIHelper.cpp, line 536 violated:
!s_expecting_unsat
----- stack dump -----
Version : Vampire 4.8 (commit 23d7e9c3b61 on 2024-03-22 08:41:08 +0000)
call stack: 0x406f0a 0x2690a99 0x40a036 0x4090a7 0x4084cf 0x943bf8 0x4144e0 0x416598
(use '--traceback on' to get a human-readable stack trace)
----- end of stack dump -----

joe-hauns · 2024-04-05T11:53:41Z

Bug 10

Files:

SYN/SYN000_4.p
Options: --input_syntax tptp
Issue: Crash in TPTP parser
Example:

/home/jschoiss/.vampire-benchexec/build/bin/vampire-23d7e9c3b61479bc14e1687f917c22f80dc7c8f1-Debug-z3 --input_syntax tptp --time_limit 10 /home/jschoiss/TPTP-v8.2.0//Problems/SYN/SYN000_4.p


--------------------------------------------------------------------------------


Condition in file /home/jschoiss/.vampire-benchexec/build/repos/vampire/Lib/Stack.hpp, line 201 violated:
_stack+n < _cursor
----- stack dump -----
Version : Vampire 4.8 (commit 23d7e9c3b61 on 2024-03-22 08:41:08 +0000)
call stack: 0x406f0a 0x2690a99 0x40a01d 0x942f21 0x9429c6 0x9423d1 0x96a7a3 0x96ab4c 0x97db3e 0x97e427 0x565ab1 0x564516 0x40b2d7 0x40e278 0x4144e0 0x416598
(use '--traceback on' to get a human-readable stack trace)
----- end of stack dump -----

joe-hauns · 2024-04-05T12:56:03Z

Bug 11

Files:

SYN/SYN000+2.p
SYN/SYN000-2.p
SYN/SYN000_2.p

Issue: TPTP parser fails.
Options --input_syntax tptp

Example:

./bin/vampire-23d7e9c3b61479bc14e1687f917c22f80dc7c8f1-Debug-z3 --input_syntax tptp --time_limit 9 TPTP-v8.2.0//Problems/SYN/SYN000_2.p


--------------------------------------------------------------------------------


Parsing Error on line 69: Unsupported unit type 'assumption' found at position 2013

Bug 12

Files:

LCL/LCL946_10.p

Issue: TPTP parsing fails.
Options --input_syntax tptp

./bin/vampire-23d7e9c3b61479bc14e1687f917c22f80dc7c8f1-Debug-z3 --input_syntax tptp --time_limit 7 TPTP-v8.2.0//Problems/LCL/LCL946_10.p


--------------------------------------------------------------------------------


Parsing Error on line 688: Failed to create predicate application for $ki_exists_in_world_$i of type 0x4967a90
The sort $i of the intended term argument X0 (at index 0) is not an instance of sort '$ki_world'

joe-hauns · 2024-04-08T09:08:32Z

I ran the current master in default mode on all of smtlib and tptp over the weekend and here are the results:

benchmarks: 119661
solved: 58232 (48 %)
----------------------------------------------------------------------

solver master:

  options: 

  errors: 4
    assertion violation: /home/jschoiss/.vampire-benchexec/build/repos/vampire/Kernel/SortHelper.cpp@95: 88
      master ITP/ITP276_4.p
      master ITP/ITP210_4.p
      master ITP/ITP278_4.p
      master ITP/ITP217_4.p
      master ITP/ITP222_4.p
      master ITP/ITP236_4.p
      master ITP/ITP225_4.p
      master ITP/ITP259_4.p
      master ITP/ITP288_4.p
      master ITP/ITP231_4.p
      ...

    assertion violation: /home/jschoiss/.vampire-benchexec/build/repos/vampire/Lib/Stack.hpp@201: 1
      master SYN/SYN000_4.p

    assertion violation: /home/jschoiss/.vampire-benchexec/build/repos/vampire/Parse/TPTP.cpp@1940: 49
      master SWW/SWW470^3.p
      master ITP/ITP216^1.p
      master ITP/ITP088^1.p
      master ITP/ITP198^2.p
      master ITP/ITP030^2.p
      master ITP/ITP089^2.p
      master SEU/SEU907^5.p
      master ITP/ITP094^2.p
      master SWW/SWW470^2.p
      master ITP/ITP039^2.p
      ...

    parser exception: 1371
      master LIN/LIN003^1.p
      master SEU/SEU678^1.p
      master SEU/SEU547^1.p
      master SEU/SEU510^1.p
      master SEU/SEU720^1.p
      master SEU/SEU681^1.p
      master SEU/SEU583^1.p
      master GEO/GEO438^1.p
      master SEU/SEU607^1.p
      master SEU/SEU645^1.p
      ...

  unsound: 0

  solved: 58232
    master SWC/SWC128-1.p
    master SYN/SYN915-1.p
    master HWV/HWV095-1.p
    master HWV/HWV093-1.p
    master HWV/HWV089-1.p
    master COL/COL086-1.p
    master COL/COL083-1.p
    master COL/COL084-1.p
    master COL/COL085-1.p
    master ALG/ALG399-1.p
    ...

  unique: 58232
    master SWC/SWC128-1.p
    master SYN/SYN915-1.p
    master HWV/HWV095-1.p
    master HWV/HWV093-1.p
    master HWV/HWV089-1.p
    master COL/COL086-1.p
    master COL/COL083-1.p
    master COL/COL084-1.p
    master COL/COL085-1.p
    master ALG/ALG399-1.p
    ...

I think this is the same bugs as i reported (but a bit more coarse as i didn't look into all the parser exceptions for this run.
Here is the full problem list: analyse-res.txt

MichaelRawson · 2024-04-08T18:36:21Z

Bug 1 seems to result from an instance of polymorphic $let. Minimised, it looks something like this:

tff(ty_t_List_Olist,type,
    list: $tType > $tType ).

tff(sy_c_List_Olist_OCons,type,
    cons: 
      !>[A: $tType] : ( A > fun(list(A),list(A)) ) ).

tff(sy_c_List_Oappend,type,
    append: 
      !>[A: $tType] : ( ( list(A) * list(A) ) > list(A) ) ).

tff(sy_c_List_Osubseqs,type,
    subseqs: 
      !>[A: $tType] : ( list(A) > list(list(A)) ) ).

tff(sy_c_List_Olist_Omap,type,
    map: 
      !>[A: $tType,Aa: $tType] : ( ( fun(A,Aa) * list(A) ) > list(Aa) ) ).

tff(sy_c_aa,type,
    aa: 
      !>[A: $tType,B: $tType] : ( ( fun(A,B) * A ) > B ) ).

% nth_append
tff(fact_2816_subseqs_Osimps_I2_J,axiom,
    ! [A: $tType,Xa: A,Xs: list(A)] :
      subseqs(A,aa(list(A),list(A),cons(A,Xa),Xs)) = $let(
        xss: list(list(A)),
        xss:= subseqs(A,Xs),
        append(list(A),map(list(A),list(A),cons(A,Xa),xss),xss) ) ).

We ask SortHelper for the type of xss and it fails with the assertion above, because xss is just xss, not xss(A). If you disable the assertion, it seems to go through and get clausified OK into something well-typed. @mezpusz - I think you're the expert here. Is my assessment correct? What do you think the fix should be?

The assertion seems OK for most cases, but maybe we could set a flag for let-constants like this one and skip it for those.

mezpusz · 2024-04-09T08:11:32Z

@MichaelRawson As far as I understand, the declaration of xss is not well-formed, and rather it should be something like !>[A: $tType] : list(list(A)), so that A is not free and we can access it (at least internally). But then we would need to use xss(A) everywhere internally. I couldn't find a good reference for polymorphic lets, I suppose the input is correct.

MichaelRawson mentioned this issue Apr 10, 2024

avoid sortedness errors with polymorphically let-bound constants #544

Open

MichaelRawson mentioned this issue Apr 24, 2024

Subsumption and Subsumption Resolution via SAT solving #546

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Miscellanious Crashes #542

Miscellanious Crashes #542

joe-hauns commented Apr 5, 2024 •

edited

joe-hauns commented Apr 5, 2024 •

edited

joe-hauns commented Apr 5, 2024

joe-hauns commented Apr 5, 2024

joe-hauns commented Apr 5, 2024

joe-hauns commented Apr 8, 2024

MichaelRawson commented Apr 8, 2024

mezpusz commented Apr 9, 2024

Miscellanious Crashes #542

Miscellanious Crashes #542

Comments

joe-hauns commented Apr 5, 2024 • edited

Bug 1:

Bug 2

Bug 3

Bug 4:

Bug 5:

Bug 6:

Bug 7:

joe-hauns commented Apr 5, 2024 • edited

Bug 8

joe-hauns commented Apr 5, 2024

Bug 9

joe-hauns commented Apr 5, 2024

Bug 10

joe-hauns commented Apr 5, 2024

Bug 11

Bug 12

joe-hauns commented Apr 8, 2024

MichaelRawson commented Apr 8, 2024

mezpusz commented Apr 9, 2024

joe-hauns commented Apr 5, 2024 •

edited

joe-hauns commented Apr 5, 2024 •

edited