1		% (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(prob_socketserver, [start_prob_socketserver/1, start_prob_socketserver/2,
6		prob2_call_back_available/0,
7		prob2_call_back/2]).
8
9		:- use_module(module_information,[module_info/2]).
10		:- module_info(group,cli).
11		:- module_info(description,'The socket server is used to interface to Java and other languages.').
12
13		/*
14
15		possible input terms read by Prolog on socket stream (sent e.g. by sendCommand of CommandProcessor.java):
16		- end_of_file (not a real term)
17		- halt
18		- Call(s) on white_list, exported by either eclipse_interface or prob2_interface
19		(can be a conjunction)
20
21		possible return values written by Prolog on socket stream:
22		- exception(CallEx)
23		- interrupted
24		- yes(Vars)
25		- no
26		- progress(Term)
27		- call_back(Call)
28		A result is terminated by character 1, see ProBConnection.java
29		(which uses inputScanner.next() with inputScanner = new Scanner(socket.getInputStream()).useDelimiter("\u0001"))
30		*/
31
32		:- use_module(version).
33		:- use_module(eclipse_interface).
34		:- use_module(prob2_interface).
35		:- use_module(error_manager).
36		:- use_module(debug,[debug_println/2]).
37		:- use_module(extension('user_signal/user_signal'),[get_user_signal_ref/1,
38		user_interruptable_call_det/2,
39		ignore_user_interrupt_det/1]).
40
41		:- use_module(logger, [writeln_log/1, get_log_file/1,
42		logging_is_enabled/0]).
43		:- use_module(library(sockets)).
44		:- use_module(library(lists)).
45		:- use_module(library(terms)).
46		:- use_module(probsrc(parsercall),[register_parsing_call_back/1, deregister_parsing_call_back/0]).
47
48		:- op(1150, fx, type).
49
50		%prolog_socket :- start(_).
51
52
53		start_prob_socketserver(Port) :- start_prob_socketserver(Port,true).
54
55		start_prob_socketserver(Port,Loopback) :-
56		catch(
57		ignore_user_interrupt_det(start_socket_loop2(Port,Loopback)),
58		% CTRL-C will be ignored in start_socket_loop2; unless explicitly allowed by user_interruptable_call_det
59		E,
60		( E=halt(C) -> throw(halt(C))
61		; my_format_error("Exception in Socket Server: ~w~n",[E]),fail)),
62		!.
63		start_prob_socketserver(Port,Loopback) :-
64		my_format_error("Listening to Port failed: ~w (loopback=~w)~n",[Port,Loopback]).
65
66
67		socket_server_open_sp4(Port,Socket,Loopback) :-
68		(socket_server_open(Port,Socket,[loopback(Loopback)]) % was true
69		-> true
70		; my_format_error("Unable to bind sp4 socket: ~w to localhost:~w.~n",[Socket,Port]),fail).
71
72		% Page 725, Chapter 10 of SICStus Manual for loopback(Bool) option:
73		% If true then the nodename will be ignored and the socket will only listen to connection
74		% from the loopback device, i.e. the local machine.
75
76		socket_server_close_sp4(Socket) :- deregister_parsing_call_back,
77		retractall(current_socket_stream(_)),
78		socket_server_close(Socket).
79
80		socket_accept_sp4(Socket, Stream) :-
81		deregister_parsing_call_back,
82		retractall(current_socket_stream(_)),
83		socket_server_accept(Socket, Client, Stream, [type(text),encoding(utf8)]),
84		my_format("Connected: ~w~n",[Client]),
85		assertz(current_socket_stream(Stream)), % for call_backs
86		register_parsing_call_back(prob2_parse_call_back).
87
88		:- dynamic current_socket_stream/1.
89
90
91		start_socket_loop2(Port,Loopback) :-
92		% print(socket('AF_INET', Socket)),nl,
93		socket_server_open_sp4(Port,Socket,Loopback),
94		call_cleanup(start_socket_loop3(Port,Socket),
95		stop_socket_loop3(Socket)).
96
97		start_socket_loop3(Port,Socket) :-
98		format(user_output,'Port: ~w~n', [Port]), % ProB2 matches against this in PortPattern.java
99		writeln_log(port(Port)),
100		revision(Revision),
101		format(user_output,'probcli revision: ~w~n',[Revision]),
102		get_user_signal_ref(Ref),
103		format(user_output,'user interrupt reference id: ~w~n',[Ref]), % ProB2 matches against this in InterruptRefPattern.java
104		format(user_output,'-- starting command loop --~n', []), % ProB2 matches against this in CliStarter.java
105		flush_output(user_output),
106		main_socket_loop(Socket).
107
108		stop_socket_loop3(Socket) :-
109		socket_server_close_sp4(Socket),!,
110		my_format("Socket closed: ~w~n",[Socket]), flush_output,
111		writeln_log(socket_closed(Socket)).
112
113
114		%% Wait for a connection on the given socket
115		main_socket_loop(Socket) :-
116		socket_accept_sp4(Socket, Stream),
117		read_socket(Socket, Stream).
118
119		% adding meta_predicate makes ProB2 fail:
120		%:- meta_predicate make_call(-,0,-).
121		%:- meta_predicate do_call(0,-,-).
122
123		%% We have a connection so just wait for valid terms, and return either
124		%% OK X=val\000Y=val1
125		%% FAIL\000
126		%% ERROR SHORT long message here\000
127		read_socket(Socket,Stream) :-
128		%print(listening_on_socket(Socket)),nl, flush_output(user_output),
129		catch(read_term(Stream, Term, [variable_names(Vars)]), E, (
130		portray_clause(user_output,goal_parse_error),
131		Parse=fail,
132		process_exception(E,Stream)
133		)),
134
135		% print(received_term(Term,Parse)),nl, flush_output(user_output),
136		(Parse=ok ->
137		((Term == end_of_file ; Term==halt) ->
138		throw(halt(0))
139		; %portray_clause(user_output,calling(Term)),
140		make_call(Stream, Term, Vars)
141		%portray_clause(user_output,exit(Term))
142		)
143		;
144		%% Parse failed, but we have already written error message
145		%print(an_exception_occurred(E)),nl,
146		portray_clause(user_output, an_exception_occurred(E))
147		),
148		flush_output(Stream),
149		% Explicitly flush stdout.
150		% When stdout is not connected to a terminal
151		% (i. e. probcli is run non-interactively),
152		% the stream defaults to being fully buffered,
153		% so some short prints may not be output right away.
154		% As a workaround, we flush stdout here,
155		% so that buffered prints are output at least when the command has finished.
156		% It might be better to switch stdout to line buffering instead,
157		% but SICStus apparently has no way to do this.
158		flush_output(user_output),
159		read_socket(Socket, Stream).
160
161		% predicate to parse formulas via ProB2 Java API
162		prob2_parse_call_back(Kind,DefList,Formula,Tree) :-
163		prob2_call_back(parse_classical_b(Kind,DefList,Formula),Tree).
164
165		% predicate to allow Prolog to call back into ProB2 Java API
166		prob2_call_back(Call,Res) :- \+ call_back_white_list(Call),!,
167		add_error(prob_socketserver,'Callback not on whitelist: ',Call),
168		Res=fail.
169		prob2_call_back(Call,CBResult) :-
170		current_socket_stream(Stream),!,
171		debug_println(19,call_back(Call)),
172		write_canonical(Stream,call_back(Call)),nl(Stream), put_code(Stream,1), flush_output(Stream),
173		read_term(Stream,CBResult,[]).
174		prob2_call_back(Call,_) :-
175		add_error(prob_socketserver,'No socket stream available for call back: ',Call),fail.
176
177		call_back_white_list(parse_classical_b(_,_,_)).
178		call_back_white_list(interrupt_is_requested).
179
180		% check if call_back to ProB2 is available
181		prob2_call_back_available :- current_socket_stream(_).
182
183		% SWI-Prolog write_canonical writes lists using regular list syntax
184		% while SICStus uses dot terms, but ProB 2's answerparser can deal with both
185		% although regular list syntax would be better (less characters to send and parse)
186		write_result_term(Stream, Result) :-
187		write_canonical(Stream, Result).
188
189		%% We have a valid term so make the call
190		make_call(Stream,Term, Vars) :-
191		% write(make_call(Term)),nl,flush_output(user_output),
192		%(Term=get_user_signal_reference(_) -> true ; Term=get_version(_,_,_,_,_,_,_) -> true ; parsercall:parse_x(formula,false,"22>10+3",Tree), print(res(Tree)),nl),
193		%write_canonical(Stream,progress(start_call)), %writeln_log(result(Result)),
194		%nl(Stream), put_code(Stream,1), flush_output(Stream),
195		catch(do_call(Term,Vars,Result), CallEx, (
196		portray_clause(user_output, exception(make_call/3, CallEx)),
197		writeln_log(exception(CallEx)),
198		Result=exception(CallEx)
199		)),
200		write_result_term(Stream,Result), %writeln_log(result(Result)),
201		nl(Stream), put_code(Stream,1), %print(end),debug:nl_time,
202		flush_output(Stream).
203
204		do_call(Call,Vars,ResOut) :- %print(do_call(Call)),nl,flush_output(user_output),
205		writeln_logtime_call_start(Call,Timer), %logger:writeln_log_time(do_call(Call)),
206		(white_list(Call)
207		-> (do_not_interrupt_this_call(Call)
208		-> do_prolog_call(Call),
209		IRes = ok
210		; user_interruptable_call_det(do_prolog_call(Call),IRes)
211		),
212		(IRes = interrupted -> ResOut = interrupted
213		; ResOut = yes(Vars))
214		; my_format_error('Call not on whitelist: ~w.\n',[Call]),fail
215		),
216
217		((ground(Vars) ; call_not_required_to_ground_all_vars(Call) ; ResOut = interrupted)
218		% print(success(Call)),nl,flush_output(user_output),
219		-> writeln_logtime_call_end(Call,Timer)
220		%-> logger:writeln_log_time(success(Call))
221		; throw(result_is_not_ground)),
222		% \+ next_char_is_semicolon(Stream), /*Otherwise force backtracking */
223		!.
224		do_call(_Call,_Vars,no) :-
225		writeln_log(no).
226
227		:- use_module(library(timeout),[time_out/3]).
228		% for debugging purposes
229		do_prolog_call((A,B)) :- !, do_prolog_call(A),do_prolog_call(B).
230		% comment in to detect timeouts:
231		%do_prolog_call(A) :- !, format(user_output,'Socketserver calling: ~w~n',[A]), flush_output, time_out(A,10000,Res), format(user_output,'Socketserver res=~w~n',[Res]),(Res==time_out -> throw(time_out) ; true).
232		do_prolog_call(A) :- call(A).
233
234		%calls should be ground, however there are expections where free variables are needed
235		%calls are insereted in list of (A,B)
236		call_not_required_to_ground_all_vars((A,B)) :- !,
237		call_not_required_to_ground_all_vars(A), ground(B).
238
239
240
241		:- dynamic exported_by_eclipse_interface/2.
242		white_list(halt). % needed to stop ProB
243		white_list(true). % to prevent fails because of empty queries
244		white_list((A,B)) :- white_list(A),white_list(B). % concatenation used to send several commands at once
245		white_list(C) :- nonvar(C),functor(C,Functor,Arity), % all public predicates of the module
246		is_exported_by_eclipse_interface(Functor,Arity). % eclipse_interface can be used
247		is_exported_by_eclipse_interface(Functor,Arity) :-
248		exported_by_eclipse_interface(Functor,Arity),!.
249		is_exported_by_eclipse_interface(Functor,Arity) :-
250		% check that the list has not already been generated
251		\+ exported_by_eclipse_interface(_,_),
252		% generate the list
253		create_exported_by_eclipse_interface_list,
254		% do the check again
255		exported_by_eclipse_interface(Functor,Arity).
256		create_exported_by_eclipse_interface_list :-
257		% fail-driven loop over the predicates imported from eclipse_interface
258		predicate_property(prob_socketserver:P,imported_from(eclipse_interface)),
259		functor(P,Functor,Arity),
260		assertz(exported_by_eclipse_interface(Functor,Arity)),
261		fail.
262		create_exported_by_eclipse_interface_list :-
263		% fail-driven loop over the predicates imported from prob2_interface
264		predicate_property(prob_socketserver:P,imported_from(prob2_interface)),
265		functor(P,Functor,Arity),
266		assertz(exported_by_eclipse_interface(Functor,Arity)),
267		fail.
268		create_exported_by_eclipse_interface_list.
269
270
271		do_not_interrupt_this_call((A,B)) :-
272		(do_not_interrupt_this_call(A) ; do_not_interrupt_this_call(B)).
273		do_not_interrupt_this_call(do_modelchecking(_,_,_,_,_)). % interrupting prob can lead to spurious deadlocks at the moment
274
275		%next_char_is_semicolon(Stream) :- %print(peeking(Stream)),nl,
276		% peek_code(Stream,X),!,
277		% ((X=10;X=13)
278		% -> (get_code(Stream,_),next_char_is_semicolon(Stream))
279		% ; (X=59,get_code(Stream,_))).
280
281
282		get_stream_info(S,Info) :-
283		catch(get_stream_info1(S,Info), E, portray_clause(user_output, exception(E))).
284
285		get_stream_info1(S,blank):-
286		portray_clause(user_output, stream_is(S)),
287		%true.
288		fail.
289		get_stream_info1(S, Info) :-
290		stream_property(S,file_name(Info)),!.
291		get_stream_info1(S, Info) :-
292		stream_property(S,alias(Info)),
293		!.
294		get_stream_info1(_S, unknown).
295
296
297		tokens_to_string([],[]).
298		tokens_to_string([A|As], [B|Bs]) :-
299		token_to_string1(A,B),
300		tokens_to_string(As,Bs).
301
302		token_to_string1(atom(A)-_, A) :- !.
303		token_to_string1(var(_,S,_)-_, A) :- !,
304		atom_codes(A,S).
305		token_to_string1(A, A).
306
307
308		%% Exception handlers
309		%% First Argument is Sicstus exception, second is verbose message for user
310		process_exception(E,_Stream) :-
311		portray_clause(user_output,E),fail.
312		process_exception(syntax_error(Call, Pos, Msg, Tokens,Lineend),Stream) :-
313		!,
314		portray_clause(user_output,syntax_stream(Call)),
315		(Call = read_term(Err,_,_) ->
316		get_stream_info(Err,Info)
317		;
318		Info = unknown_stream
319		),
320		tokens_to_string(Tokens,Where),
321
322		my_format_error(Stream,'exception(ERR-~@PARSE~@~w in ~w\nlines::~w-~w\nCheck ~w)\n', [put_code(1),put_code(1),Msg,Info,Pos,Lineend,Where]),
323		put_code(Stream, 1).
324		process_exception(existence_error(_, _, _, _, past_end_of_stream),Stream) :-
325		!,
326		my_format_error(Stream,'exception(ERR-~@EXISTENCE~@Attempted to read past end of stream)', [put_code(1),put_code(1)]),
327		put_code(Stream, 1) .
328		process_exception(existence_error(_, _,procedure,PredSpec,_),Stream) :-
329		!,
330		my_format_error(Stream,'exception(ERR-~@EXISTENCE~@Unable to call predicate ~w)', [put_code(1),put_code(1),PredSpec]),
331		put_code(Stream, 1) .
332		process_exception(existence_error(_, _,file,PredSpec,_),Stream) :-
333		!,
334		my_format_error(Stream,'exception(ERR-~@EXISTENCE~@Unable to open file ~w)', [put_code(1),put_code(1),PredSpec]),
335		put_code(Stream, 1) .
336		process_exception(E,Stream) :-
337		my_format_error(Stream,'exception(ERR-~@UNKNOWN~@~w)', [put_code(1),put_code(1),E]),
338		put_code(Stream, 1),
339		portray_clause(user_output,unknown_exception(E)).
340
341
342
343		my_format(FS,Args) :- my_format(user_output,FS,Args).
344		my_format_error(FS,Args) :- my_format(user_error,FS,Args).
345		my_format_error(Stream,FS,Args) :- my_format(Stream,FS,Args).
346
347		my_format(Stream,FS,Args) :- format(Stream,FS,Args),
348		(get_log_file(F)
349		-> open(F,append,S),
350		format(S,FS,Args),
351		close(S)
352		; true
353		).
354
355		writeln_logtime_call_start(Term,timer(Time,WTime)) :-
356		((logging_is_enabled ; runtime_profile_available) ->
357		statistics(runtime,[Time,_]),
358		statistics(walltime,[WTime,_]),
359		(logging_is_enabled
360		-> get_functors(Term,Fs),
361		writeln_log(start_call(walltime(WTime),Fs))
362		; true)
363		; true).
364
365		:- use_module(probsrc(tools),[statistics_memory_used/1]).
366		:- use_module(runtime_profiler,[register_profiler_runtime/4, runtime_profile_available/0]).
367		writeln_logtime_call_end(Term,timer(Time,WTime)) :-
368		%format(user_output,'End for ~w~n',[Time]),
369		((logging_is_enabled ; runtime_profile_available) ->
370		statistics(runtime,[Time2,_]), RT is Time2-Time,
371		statistics(walltime,[WTime2,_]), WT is WTime2-WTime,
372		get_functors(Term,Fs),
373		(logging_is_enabled
374		-> statistics_memory_used(M), MB is M / 1000000, % used instead of deprecated 1048576
375		writeln_log(end___call(walltime(WTime2),delta_rt_wt(RT,WT),mb_used(MB),Fs))
376		; true),
377		register_profiler_runtime(Fs,unknown,RT,WT)
378		; true).
379
380		get_functors(Var,V) :- var(Var),!, V='_'.
381		get_functors((A,B),(FA,FB)) :- !, get_functors(A,FA), get_functors(B,FB).
382		%get_functors(A,F/list(Len)) :- functor(A,F,1), arg(1,A,Ls), nonvar(Ls), Ls = [_|_],
383		% ground(Ls), length(Ls,Len),!.
384		get_functors(A,F/N) :- functor(A,F,N).
385
386		%runtime_entry(start) :- go_cli.
387
388		%save :- save_program('probcli.sav').