Segmentation fault: 11

[triska]

To reproduce this issue, please download the file:

https://www.metalevel.at/prolog/scryer/segmentation_fault_20231008.pl

and then do:

$ scryer-prolog -f segmentation_fault_20231008.pl
?- use_module(library(lists)),
   use_module(library(format)),
   clpz:parse_clpz_clauses(Clauses),
   maplist(portray_clause, Clauses).

Yielding:

parse_clpz(A,B) :-
   [cyclic_term(A),!,domain_error(clpz_expression,A)].
parse_clpz(A,B) :-
   [var(A),!,non_monotonic(A),constrain_to_integer(A),A=B].
parse_clpz(A,B) :-
   [integer(A),!,B=A].
parse_clpz(?(A),B) :-
   [!,must_be_fd_integer(A),B=A].
parse_clpz(#A,B) :-
   [!,must_be_fd_integer(A),B=A].
Segmentation fault: 11

[haijinSk]

For the record, I ran the example with precompiled "zip" version v0.9.4 (4163437) for Ubuntu 22.04 and it does not yield the "Segmentation fault: 11"; it is yielding the "clpz things" and then it terminates.

And the same with "cargo:0.9.2" (not git actual) version, compiled via Rust on my computer.

[triska]

Can you please test it with the latest git version? It would be interesting if this reproduces on other machines. Thank you a lot!

[haijinSk]

I did it right now, the github "scryer-prolog-master.zip" via "cargo build --release" and it does yield the segmentation fault...

[triska]

Perfect, thank you a lot! This means the problem is reproducible on OSX (which I used) and also on Ubuntu! This is very valuable to know.

If you are interested in helping further with this, you can try to systematically shorten the test case by removing predicates to make the file shorter, as long as the crash can still be observed. I would greatly appreciate your help with this issue!

[haijinSk]

I have no idea what I'm doing, but it seems to me, this predicate has something to do with the issue.

parse_goal(p(Prop)) -->
        { term_variables(Prop0, Vs) },
        [morphing_propagator(Prop0, Prop),
         make_propagator(Prop, P),
         new_queue(Q0),
         phrase(init_propagator_(Vs, P), [Q0], [Q]),
         variables_same_queue(Vs),
         trigger_once_(P, Q)].

[haijinSk]

If I comment out the: "[morphing_propagator(Prop0, Prop), ...]" part, It yields:

Warning: singleton variables Prop, Prop0, Vs at line 2639 of segmentation_fault_20231008.pl

but I can run the queries and it prints some "clpz things"...

[triska]

Yes, I also highly suspect that this part is responsible! I think a lot of the remaining code can be removed, so that we can obtain a shorter test case. This may make it easier to address this issue.

[haijinSk]

Yes, If I comment out the entire predicate, it answers "false" and I can delete everything after the predicate.

[haijinSk]

Not everything...

[triska]

The point would be to retain just enough in the file so that we can still observe the crash, but with a simpler test case!

A crash is a mistake in the Prolog engine itself, it is something that cannot be fixed by us as Prolog programmers. This issue is not about a mistake in the provided file, but about the underlying Rust system.

[haijinSk]

I have to have this, after the problematic predicate:

automaton(Sigs, Ns, As) :- automaton(_, _, Sigs, Ns, As, [], [], _).

disjoint2(Rs0) :-
        must_be(list, Rs0),
        maplist(=.., Rs0, Rs),
        non_overlapping(Rs).

non_overlapping([]).
non_overlapping([R|Rs]) :-
        maplist(non_overlapping_(R), Rs),
        non_overlapping(Rs).

non_overlapping_(A, B) :-
        a_not_in_b(A, B),
        a_not_in_b(B, A).

a_not_in_b([_,AX,AW,AY,AH], [_,BX,BW,BY,BH]) :-
        #AX #=< #BX #/\ #BX #< #AX + #AW #==>
                   #AY + #AH #=< #BY #\/ #BY + #BH #=< #AY,
        #AY #=< #BY #/\ #BY #< #AY + #AH #==>
                   #AX + #AW #=< #BX #\/ #BX + #BW #=< #AX.

cumulative(Tasks) :- cumulative(Tasks, [limit(1)]).

circuit(Vs) :-
        must_be(list, Vs),
        maplist(fd_variable, Vs),
        length(Vs, L),
        Vs ins 1..L,
        (   L =:= 1 -> true
        ;   neq_index(Vs, 1),
            make_propagator(pcircuit(Vs), Prop),
            new_queue(Q0),
            phrase((distinct_attach(Vs, Prop, []),trigger_prop(Prop),do_queue), [Q0], _)
        ).

element(N, Is, V) :-
        must_be(list, Is),
        length(Is, L),
        N in 1..L,
        element_(Is, 1, N, V),
        propagator_init_trigger([N|Is], pelement(N,Is,V)).

element_domain(V, VD) :-
        (   fd_get(V, VD, _) -> true
        ;   VD = from_to(n(V), n(V))
        ).

element_([], _, _, _).
element_([I|Is], N0, N, V) :-
        #I #\= #V #==> #N #\= N0,
        N1 is N0 + 1,
        element_(Is, N1, N, V).

integers_remaining([], _, _, D, D).
integers_remaining([V|Vs], N0, Dom, D0, D) :-
        (   domain_contains(Dom, N0) ->
            element_domain(V, VD),
            domains_union(D0, VD, D1)
        ;   D1 = D0
        ),
        N1 is N0 + 1,
        integers_remaining(Vs, N1, Dom, D1, D).

global_cardinality(Xs, Pairs) :- global_cardinality(Xs, Pairs, []).

serialized(Starts, Durations) :-
        must_be(list(integer), Durations),
        pairs_keys_values(SDs, Starts, Durations),
        Orig = original_goal(_, serialized(Starts, Durations)),
        serialize(SDs, Orig).

tuples_in(Tuples, Relation) :-
        must_be(list(list), Tuples),
        maplist(maplist(fd_variable), Tuples),
        must_be(list(list(integer)), Relation),
        new_queue(Q0),
        phrase(tuples_relation(Tuples, Relation), [Q0], [Q]),
        append(Tuples, Vs),
        variables_same_queue(Vs),
        phrase(do_queue, [Q], _).

lex_chain(Lss) :-
        must_be(list(list), lex_chain(Lss)-1, Lss),
        maplist(maplist(fd_variable), Lss),
        (   Lss == [] -> true
        ;   Lss = [First|Rest],
            make_propagator(presidual(lex_chain(Lss)), Prop),
            foldl(lex_chain_(Prop), Rest, First, _)
        ).

#\ Q       :- reify(Q, 0), do_queue.

L #<==> R  :- reify(L, B), reify(R, B), do_queue.

L #<== R   :- R #==> L.

L #/\ R    :- reify(L, 1), reify(R, 1), do_queue.

L #\/ R :-
        (   disjunctive_eqs_var_drep(L #\/ R, Var, Drep) -> Var in Drep
        ;   reify(L, X, Ps1),
            reify(R, Y, Ps2),
            propagator_init_trigger([X,Y], reified_or(X,Ps1,Y,Ps2,1))
        ).

L #\ R :- (L #\/ R) #/\ #\ (L #/\ R).

X #>= Y :- clpz_geq(X, Y).

[haijinSk]

Now, I do not need this (from the above):

non_overlapping([]).

non_overlapping([R|Rs]) :-
        maplist(non_overlapping_(R), Rs),
        non_overlapping(Rs).

non_overlapping_(A, B) :-
        a_not_in_b(A, B),
        a_not_in_b(B, A).

[triska]

Nice work! In this way, you can systematically reduce the test case, and try to find a shortest version of the file that still exhibits the crash.

It is not unusual for such systematic reductions to take many hours of work. In this way, we can help Mark with short snippets that show the problem. And sometimes, we even find additional mistakes in this process! If you find anything that seems unusual in this process, such as different kinds of crashes, then please also consider filing this as an issue!

It is also worth thinking about whether and how such a process can be automated! For example, it could be worth trying to construct a Prolog program that performs this task for you, by reading in clauses (with read/1) from the file, and writing some of them to a different file that can serve as the basis for further reductions.

[haijinSk]

I know, I have to be more systematic, but to summarize my observations so far (and some new predicates to retain that I omitted before).

Down to this predicate I have everything as the original file, but after this ("problematic" or "key" so far) predicate:

parse_goal(p(Prop)) -->
        { term_variables(Prop0, Vs) },
       [morphing_propagator(Prop0, Prop),
         make_propagator(Prop, P),
         new_queue(Q0),
         phrase(init_propagator_(Vs, P), [Q0], [Q]),
         variables_same_queue(Vs),
         trigger_once_(P, Q)]. 

to reproduce the segment. fault with the queries, I need to retain (at least as I see/know it in this moment):

#=(X, Y, T) :-
        X #= Y #<==> B,
        zo_t(B, T).

#<(X, Y, T) :-
        X #< Y #<==> B,
        zo_t(B, T).

zo_t(0, false).
zo_t(1, true).

fd_dom(X, Drep) :-
        (   fd_get(X, XD, _) ->
            domain_to_drep(XD, Drep)
        ;   must_be(integer, X),
            Drep = X..X
        ).

zcompare(Order, A, B) :-
        (   nonvar(Order) ->
            zcompare_(Order, A, B)
        ;   integer(A), integer(B) ->
            compare(Order, A, B)
        ;   freeze(Order, zcompare_(Order, A, B)),
            fd_variable(A),
            fd_variable(B),
            propagator_init_trigger([A,B], pzcompare(Order, A, B))
        ).        

chain(Relation, Zs) :-
        must_be(list, Zs),
        maplist(fd_variable, Zs),
        must_be(ground, Relation),
        (   chain_relation(Relation) -> true
        ;   domain_error(chain_relation, Relation)
        ),
        chain_(Zs, Relation).

automaton(Sigs, Ns, As) :- automaton(_, _, Sigs, Ns, As, [], [], _).

disjoint2(Rs0) :-
        must_be(list, Rs0),
        maplist(=.., Rs0, Rs),
        non_overlapping(Rs).

a_not_in_b([_,AX,AW,AY,AH], [_,BX,BW,BY,BH]) :-
        #AX #=< #BX #/\ #BX #< #AX + #AW #==>
                   #AY + #AH #=< #BY #\/ #BY + #BH #=< #AY,
        #AY #=< #BY #/\ #BY #< #AY + #AH #==>
                   #AX + #AW #=< #BX #\/ #BX + #BW #=< #AX.

cumulative(Tasks) :- cumulative(Tasks, [limit(1)]).

circuit(Vs) :-
        must_be(list, Vs),
        maplist(fd_variable, Vs),
        length(Vs, L),
        Vs ins 1..L,
        (   L =:= 1 -> true
        ;   neq_index(Vs, 1),
            make_propagator(pcircuit(Vs), Prop),
            new_queue(Q0),
            phrase((distinct_attach(Vs, Prop, []),trigger_prop(Prop),do_queue), [Q0], _)
        ).

element(N, Is, V) :-
        must_be(list, Is),
        length(Is, L),
        N in 1..L,
        element_(Is, 1, N, V),
        propagator_init_trigger([N|Is], pelement(N,Is,V)).

element_domain(V, VD) :-
        (   fd_get(V, VD, _) -> true
        ;   VD = from_to(n(V), n(V))
        ).

element_([], _, _, _).
element_([I|Is], N0, N, V) :-
        #I #\= #V #==> #N #\= N0,
        N1 is N0 + 1,
        element_(Is, N1, N, V).

integers_remaining([], _, _, D, D).
integers_remaining([V|Vs], N0, Dom, D0, D) :-
        (   domain_contains(Dom, N0) ->
            element_domain(V, VD),
            domains_union(D0, VD, D1)
        ;   D1 = D0
        ),
        N1 is N0 + 1,
        integers_remaining(Vs, N1, Dom, D1, D).

global_cardinality(Xs, Pairs) :- global_cardinality(Xs, Pairs, []).

serialized(Starts, Durations) :-
        must_be(list(integer), Durations),
        pairs_keys_values(SDs, Starts, Durations),
        Orig = original_goal(_, serialized(Starts, Durations)),
        serialize(SDs, Orig).

tuples_in(Tuples, Relation) :-
        must_be(list(list), Tuples),
        maplist(maplist(fd_variable), Tuples),
        must_be(list(list(integer)), Relation),
        new_queue(Q0),
        phrase(tuples_relation(Tuples, Relation), [Q0], [Q]),
        append(Tuples, Vs),
        variables_same_queue(Vs),
        phrase(do_queue, [Q], _).

lex_chain(Lss) :-
        must_be(list(list), lex_chain(Lss)-1, Lss),
        maplist(maplist(fd_variable), Lss),
        (   Lss == [] -> true
        ;   Lss = [First|Rest],
            make_propagator(presidual(lex_chain(Lss)), Prop),
            foldl(lex_chain_(Prop), Rest, First, _)
        ).

#\ Q       :- reify(Q, 0), do_queue.

L #<==> R  :- reify(L, B), reify(R, B), do_queue.

L #<== R   :- R #==> L.

L #/\ R    :- reify(L, 1), reify(R, 1), do_queue.

L #\/ R :-
        (   disjunctive_eqs_var_drep(L #\/ R, Var, Drep) -> Var in Drep
        ;   reify(L, X, Ps1),
            reify(R, Y, Ps2),
            propagator_init_trigger([X,Y], reified_or(X,Ps1,Y,Ps2,1))
        ).

L #\ R :- (L #\/ R) #/\ #\ (L #/\ R).

X #>= Y :- clpz_geq(X, Y).

[haijinSk]

A too obvious note to my naive self, but as we know, the git version stops with the fault displaying/portraying as the last clause this:

parse_clpz(#A,B) :-
   [!,must_be_fd_integer(A),B=A].

My "precompiled zip" version v0.9.4 (4163437) for Ubuntu 22.04 continues with this "portrait":

parse_clpz(A+B,C) :-
[!,parse_clpz(A,D),parse_clpz(B,E),morphing_propagator(F,pplus(D,E,C)),make_propagator(pplus(D,E,C),G),new_queue(H),phrase(init_propagator_([['B'=B,'C'=C,'D'=D,'E'=E,'F'=F,'G'=G,'H'=H,'I'=I]],G),[H],[I]),variables_same_queue([['B'=B,'C'=C,'D'=D,'E'=E,'F'=F,'G'=G,'H'=H,'I'=I]]),trigger_once_(G,I)].

Ad so on...

[haijinSk]

And with this query:

?- use_module(library(lists)),
   use_module(library(format)),
   clpz:parse_clpz_clauses(Clauses),
   maplist(write, Clauses).  % Or: write(Clauses).

or with:

?- use_module(library(lists)),
   use_module(library(format)),
   length(Clauses,N),clpz:parse_clpz_clauses(Clauses).

it terminates normally. Except the second case with length/2 will show only the first list (N = 30) and when pressing "A" it does not terminate.

[haijinSk]

My newest observation. I terminates if I remove:

morphing_propagator(Prop0, Prop)

from:

parse_goal(p(Prop)) -->
        { term_variables(Prop0, Vs) },
       [ morphing_propagator(Prop0, Prop),
         make_propagator(Prop, P),
         new_queue(Q0),
         phrase(init_propagator_(Vs, P), [Q0], [Q]),
         variables_same_queue(Vs),
         trigger_once_(P, Q)]. 

[haijinSk]

I can change the morphing_propagator(Prop0, Prop) with anything like, for example, anything_I_want(Prop0, Prop) to reproduce the segment. fault.

But it terminates with:anything_I_want(Prop) or anything_I_want.

[haijinSk]

In an older (not "seg. fault ending") version of clpz.pl, there is no morphing_propagator(Prop0, Prop) in the parse_goal//1.

[haijinSk]

But there is something more/something else to it. I can't reproduce the seg. fault with the older clpz.pl if I simply transplant the morphing_propagator/2 (with its definition) to that older clpz.pl.

[haijinSk]

I think this is my bad shot, but for crazy sake of certainty, in the DCG predicate, are the names/relations between variables OK? Prop0 and Prop, Prop and P... I mean OK in the context of the extra-logical mysterious "segmentation fault possibility".

parse_goal(p(Prop)) -->
        { term_variables(Prop0, Vs) },
       [ morphing_propagator(Prop0, Prop),
         make_propagator(Prop, P),
         new_queue(Q0),
         phrase(init_propagator_(Vs, P), [Q0], [Q]),
         variables_same_queue(Vs),
         trigger_once_(P, Q)]. 

[haijinSk]

If I consult a file with:

:- use_module(library(format)).

parse_goal(p(Prop)) -->  
       { term_variables(Prop0, Vs)},
       [Prop0, Vs]. 

then this query:

phrase(parse_goal(p(X)),O), portray_clause(O).

will yield the seg. fault.

To terminate normally, I have to change the Prop to Prop0.

[UWN]

Shorter:

:- use_module(library(format)).

parse_goal(Xs0) :-
   term_variables(Prop0, Vs),
   Xs0 = [Prop0|Vs].

run :-
   call((parse_goal(W),portray_clause(W))),
   false.

ulrich@gupu:~/vv$ /opt/gupu/scryer-prolog/target/release/scryer-prolog -f sv.pl -g run
Segmentation fault (core dumped)

[triska]

@haijinSk: That's really excellent work, thank you a lot for this contribution, I think this will help considerably to analyze the crash!

[UWN]

On problem here is just term_variables/2:

parse_goal(Xs0) :-
   term_variables(Prop0, Vs),
   Xs0 = [Prop0|Vs].

myportray_clause(Term) :-
   term_variables(Term, Vs),
   writeq(Vs), nl.

run :-
   parse_goal(W),
   myportray_clause(W).

ulrich@gupu:~/vv$ /opt/gupu/scryer-prolog/target/release/scryer-prolog -f sv2.pl -g run
[_1262,user_output]

This is unexpected. There should be a list with one variable. Sometimes, the same variable shows twice, and this time, there is this user_output in it.

[UWN]

Shorter for the segv

parse_goal(Xs0) :-
   term_variables(Prop0, Vs),
   Xs0 = [Prop0|Vs].

myportray_clause(Term) :-
   term_variables(Term, Vs),
   writeq(Vs),
   foldlvar_name(Vs),
   writeq(Vs).

foldlvar_name([]).
foldlvar_name([_|_]) :-
   nr_var_name(0,1),
   foldlvar_name([]).

nr_var_name(Num0, Num) :-
   atom_codes(_, [0'A]),
   Num is Num0 + 1.

run :-
   call((parse_goal(W),myportray_clause(W))).

ulrich@gupu:~/vv$ /opt/gupu/scryer-prolog/target/release/scryer-prolog -f sv3.pl -g run
[_2067,_2067]Segmentation fault (core dumped)

[triska]

Thank you all, truly terrific teamwork!