mthom / scryer-prolog

A modern Prolog implementation written mostly in Rust.
BSD 3-Clause "New" or "Revised" License
1.93k stars 116 forks source link

Rust thread panics on certain input #2423

Open stevemolloy opened 2 weeks ago

stevemolloy commented 2 weeks ago

Hi, I am quite sure that my Prolog code is bad, but I do not think that it should result in a panic of the Rust thread.

To reproduce:

  1. Clone this branch: https://github.com/stevemolloy/prolog_mps/tree/rust_panic
  2. From inside that folder: $ scryer-prolog parsing.pl
  3. ?- phrase(statement(S), "(X AND (A OR NOT B)) AND Z").
  4. ?- phrase(statement(S), "A OR B").

Result:

thread 'main' panicked at src/machine/machine_state_impl.rs:70:26:
index out of bounds: the len is 223308 but the index is 223316
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Details:

$ scryer-prolog --version
379cbfd
$ rustc --version
rustc 1.78.0 (9b00956e5 2024-04-29)
stevemolloy commented 2 weeks ago

Weirdly, skipping step 3 in the above will allow the query to work without a crash.

triska commented 2 weeks ago

Excellent find!

Cloning the branch directly does not work; to reproduce the issue, you can obtain parsing.pl with:

$ wget https://raw.githubusercontent.com/stevemolloy/prolog_mps/rust_panic/parsing.pl
haijinSk commented 2 weeks ago

Maybe another example.

A file to consult:

:- use_module(library(tabling)).

:- table countdown/1.

countdown(0).
countdown(N) :- 
  N > 0,
  N2 is N - 1,
  countdown(N2).

crash :-
  countdown(19),
  countdown(20).

A crashing query:

?- crash.
thread 'main' panicked at src/machine/machine_state_impl.rs:70:26:
index out of bounds: the len is 796039 but the index is 796040
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
triska commented 2 weeks ago

The underlying reason for this could be #2408, an issue apparently related to bb_put/2 which is also used by tabling:

$ scryer-prolog -f
?- use_module(library(freeze)).
   true.
?- use_module(library(iso_ext)).
   true.
?- freeze(W,write('ok')), bb_put(key, W).
thread 'main' panicked at 'index out of bounds: the len is 280 but the index is 281', src/machine/machine_state_impl.rs:70:17
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
triska commented 2 weeks ago

@stevemolloy: As a workaround until the underlying issue is addressed, you may be able to formulate your grammar so that it works without tabling, for instance by expressing statement//1 instead as follows, or something similar:

statement(T) --> term(T).
statement([Id1, Op, Id2]) --> term(Id1), binop(Op), statement(Id2).

term(Id)        --> ident(Id).
term([Unop,Id]) --> unop(Unop), statement(Id).
term(S)         --> ws, "(", statement(S), ")", ws.

Note that seq("(") is equivalent to "(".

stevemolloy commented 2 weeks ago

That's brilliant @triska , thanks! I was trying to implement something like that when your comment appeared, so thank you.

Now I just have to figure out why it is so slow with my input :(

triska commented 2 weeks ago

I think this can be tracked down to the way ws//0 is currently defined; in particular, we observe many (I think unintended) solutions in the following cases:

?- phrase((ws,ws)," ").
   true
;  true
;  false.
?- phrase((ws,ws,ws)," ").
   true
;  true
;  true
;  false.
?- phrase((ws,ws,ws),"  ").
   true
;  true
;  true
;  true
;  true
;  true
;  false.

The reason is that with the current definition, ws//0 may or may not describe an actual whitespace character.

haijinSk commented 1 week ago

I apologize, if this is going to be too much for one issue, or in other words: I don't know if fixing the "panic/crash" issue alone will also fix yet another problematic example with tabling, so I'm posting it...

A file to consult:

:- use_module(library(tabling)).

:- table countdown/1.

countdown(0).
countdown(N) :- 
  N > 0,
  N2 is N - 1,
  countdown(N2).

Two subsequent query examples with two unexpected false. answers; the key point is that the first query is interrupted using "Ctrl+C":

?- countdown(3000).
^C   false. 
?- countdown(3000).
   false.