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 % If Loopback=true then nodename will be ignored and
69 % socket will only listen to connection from loopback device, i.e. local machine.
70 (socket_server_open(Port,Socket,[loopback(Loopback)]) % was true
71 -> true
72 ; my_format_error("Unable to bind sp4 socket: ~w to localhost:~w.~n",[Socket,Port]),fail).
73
74 % Page 725, Chapter 10 of SICStus Manual for loopback(Bool) option:
75 % If true then the nodename will be ignored and the socket will only listen to connection
76 % from the loopback device, i.e. the local machine.
77
78 socket_server_close_sp4(Socket) :- deregister_parsing_call_back,
79 retractall(current_socket_stream(_)),
80 socket_server_close(Socket).
81
82 socket_accept_sp4(Socket, Stream) :-
83 deregister_parsing_call_back,
84 retractall(current_socket_stream(_)),
85 socket_server_accept(Socket, Client, Stream, [type(text),encoding(utf8)]),
86 my_format("Connected: ~w~n",[Client]),
87 assertz(current_socket_stream(Stream)), % for call_backs
88 register_parsing_call_back(prob2_parse_call_back).
89
90 :- dynamic current_socket_stream/1.
91
92
93 start_socket_loop2(Port,Loopback) :-
94 % print(socket('AF_INET', Socket)),nl,
95 socket_server_open_sp4(Port,Socket,Loopback),
96 call_cleanup(start_socket_loop3(Port,Socket),
97 stop_socket_loop3(Socket)).
98
99 start_socket_loop3(Port,Socket) :-
100 format(user_output,'Port: ~w~n', [Port]), % ProB2 matches against this in PortPattern.java
101 writeln_log(port(Port)),
102 revision(Revision),
103 format(user_output,'probcli revision: ~w~n',[Revision]),
104 get_user_signal_ref(Ref),
105 format(user_output,'user interrupt reference id: ~w~n',[Ref]), % ProB2 matches against this in InterruptRefPattern.java
106 format(user_output,'-- starting command loop --~n', []), % ProB2 matches against this in CliStarter.java
107 flush_output(user_output),
108 main_socket_loop(Socket).
109
110 stop_socket_loop3(Socket) :-
111 socket_server_close_sp4(Socket),!,
112 my_format("Socket closed: ~w~n",[Socket]), flush_output,
113 writeln_log(socket_closed(Socket)).
114
115
116 %% Wait for a connection on the given socket
117 main_socket_loop(Socket) :-
118 socket_accept_sp4(Socket, Stream),
119 read_socket(Socket, Stream).
120
121 % adding meta_predicate makes ProB2 fail:
122 %:- meta_predicate make_call(-,0,-).
123 %:- meta_predicate do_call(0,-,-).
124
125 %% We have a connection so wait for valid terms
126 read_socket(Socket,Stream) :-
127 %print(listening_on_socket(Socket)),nl, flush_output(user_output),
128 catch(read_term(Stream, Term, [variable_names(Vars)]), E, (
129 portray_clause(user_output,goal_parse_error),
130 Parse=fail,
131 write_result_term(Stream,exception(E))
132 )),
133
134 % print(received_term(Term,Parse)),nl, flush_output(user_output),
135 (Parse=ok ->
136 ((Term == end_of_file ; Term==halt) ->
137 throw(halt(0))
138 ; %portray_clause(user_output,calling(Term)),
139 make_call(Stream, Term, Vars)
140 %portray_clause(user_output,exit(Term))
141 )
142 ;
143 %% Parse failed, but we have already written error message
144 %print(an_exception_occurred(E)),nl,
145 portray_clause(user_output, an_exception_occurred(E))
146 ),
147 flush_output(Stream),
148 % Explicitly flush stdout.
149 % When stdout is not connected to a terminal
150 % (i. e. probcli is run non-interactively),
151 % the stream defaults to being fully buffered,
152 % so some short prints may not be output right away.
153 % As a workaround, we flush stdout here,
154 % so that buffered prints are output at least when the command has finished.
155 % It might be better to switch stdout to line buffering instead,
156 % but SICStus apparently has no way to do this.
157 flush_output(user_output),
158 read_socket(Socket, Stream).
159
160 % predicate to parse formulas via ProB2 Java API
161 prob2_parse_call_back(Kind,DefList,Formula,Tree) :-
162 prob2_call_back(parse_classical_b(Kind,DefList,Formula),Tree).
163
164 % predicate to allow Prolog to call back into ProB2 Java API
165 prob2_call_back(Call,Res) :- \+ call_back_white_list(Call),!,
166 add_error(prob_socketserver,'Callback not on whitelist: ',Call),
167 Res=fail.
168 prob2_call_back(Call,CBResult) :-
169 current_socket_stream(Stream),!,
170 debug_println(19,call_back(Call)),
171 write_canonical(Stream,call_back(Call)),nl(Stream), put_code(Stream,1), flush_output(Stream),
172 read_term(Stream,CBResult,[]).
173 prob2_call_back(Call,_) :-
174 add_error(prob_socketserver,'No socket stream available for call back: ',Call),fail.
175
176 call_back_white_list(parse_classical_b(_,_,_)).
177 call_back_white_list(interrupt_is_requested).
178
179 % check if call_back to ProB2 is available
180 prob2_call_back_available :- current_socket_stream(_).
181
182 % SWI-Prolog write_canonical writes lists using regular list syntax
183 % while SICStus uses dot terms, but ProB 2's answerparser can deal with both
184 % although regular list syntax would be better (less characters to send and parse)
185 write_result_term(Stream, Result) :-
186 write_canonical(Stream, Result), %writeln_log(result(Result)),
187 nl(Stream), put_code(Stream,1), %print(end),debug:nl_time,
188 flush_output(Stream).
189
190 %% We have a valid term so make the call
191 make_call(Stream,Term, Vars) :-
192 % write(make_call(Term)),nl,flush_output(user_output),
193 %(Term=get_user_signal_reference(_) -> true ; Term=get_version(_,_,_,_,_,_,_) -> true ; parsercall:parse_x(formula,false,"22>10+3",Tree), print(res(Tree)),nl),
194 %write_canonical(Stream,progress(start_call)), %writeln_log(result(Result)),
195 %nl(Stream), put_code(Stream,1), flush_output(Stream),
196 catch(do_call(Term,Vars,Result), CallEx, (
197 portray_clause(user_output, exception(make_call/3, CallEx)),
198 writeln_log(exception(CallEx)),
199 Result=exception(CallEx)
200 )),
201 write_result_term(Stream,Result).
202
203 do_call(Call,Vars,ResOut) :- %print(do_call(Call)),nl,flush_output(user_output),
204 writeln_logtime_call_start(Call,Timer), %logger:writeln_log_time(do_call(Call)),
205 (white_list(Call)
206 -> (do_not_interrupt_this_call(Call)
207 -> do_prolog_call(Call),
208 IRes = ok
209 ; user_interruptable_call_det(do_prolog_call(Call),IRes)
210 ),
211 (IRes = interrupted -> ResOut = interrupted
212 ; ResOut = yes(Vars))
213 ; my_format_error('Call not on whitelist: ~w.\n',[Call]),fail
214 ),
215
216 ((ground(Vars) ; call_not_required_to_ground_all_vars(Call) ; ResOut = interrupted)
217 % print(success(Call)),nl,flush_output(user_output),
218 -> writeln_logtime_call_end(Call,Timer)
219 %-> logger:writeln_log_time(success(Call))
220 ; throw(result_is_not_ground)),
221 % \+ next_char_is_semicolon(Stream), /*Otherwise force backtracking */
222 !.
223 do_call(_Call,_Vars,no) :-
224 writeln_log(no).
225
226 :- use_module(library(timeout),[time_out/3]).
227 % for debugging purposes
228 do_prolog_call((A,B)) :- !, do_prolog_call(A),do_prolog_call(B).
229 % comment in to detect timeouts:
230 %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).
231 do_prolog_call(A) :- call(A).
232
233 %calls should be ground, however there are expections where free variables are needed
234 %calls are insereted in list of (A,B)
235 call_not_required_to_ground_all_vars((A,B)) :- !,
236 call_not_required_to_ground_all_vars(A), ground(B).
237
238
239
240 :- dynamic exported_by_eclipse_interface/2.
241 white_list(halt). % needed to stop ProB
242 white_list(true). % to prevent fails because of empty queries
243 white_list((A,B)) :- white_list(A),white_list(B). % concatenation used to send several commands at once
244 white_list(C) :- nonvar(C),functor(C,Functor,Arity), % all public predicates of the module
245 is_exported_by_eclipse_interface(Functor,Arity). % eclipse_interface can be used
246 is_exported_by_eclipse_interface(Functor,Arity) :-
247 exported_by_eclipse_interface(Functor,Arity),!.
248 is_exported_by_eclipse_interface(Functor,Arity) :-
249 % check that the list has not already been generated
250 \+ exported_by_eclipse_interface(_,_),
251 % generate the list
252 create_exported_by_eclipse_interface_list,
253 % do the check again
254 exported_by_eclipse_interface(Functor,Arity).
255 create_exported_by_eclipse_interface_list :-
256 % fail-driven loop over the predicates imported from eclipse_interface
257 predicate_property(prob_socketserver:P,imported_from(eclipse_interface)),
258 functor(P,Functor,Arity),
259 assertz(exported_by_eclipse_interface(Functor,Arity)),
260 fail.
261 create_exported_by_eclipse_interface_list :-
262 % fail-driven loop over the predicates imported from prob2_interface
263 predicate_property(prob_socketserver:P,imported_from(prob2_interface)),
264 functor(P,Functor,Arity),
265 assertz(exported_by_eclipse_interface(Functor,Arity)),
266 fail.
267 create_exported_by_eclipse_interface_list.
268
269
270 do_not_interrupt_this_call((A,B)) :-
271 (do_not_interrupt_this_call(A) ; do_not_interrupt_this_call(B)).
272 do_not_interrupt_this_call(do_modelchecking(_,_,_,_,_)). % interrupting prob can lead to spurious deadlocks at the moment
273
274 %next_char_is_semicolon(Stream) :- %print(peeking(Stream)),nl,
275 % peek_code(Stream,X),!,
276 % ((X=10;X=13)
277 % -> (get_code(Stream,_),next_char_is_semicolon(Stream))
278 % ; (X=59,get_code(Stream,_))).
279
280
281 %get_stream_info(S,Info) :-
282 % catch(get_stream_info1(S,Info), E, portray_clause(user_output, exception(E))).
283 %
284 %get_stream_info1(S,blank):-
285 % portray_clause(user_output, stream_is(S)),
286 % %true.
287 % fail.
288 %get_stream_info1(S, Info) :-
289 % stream_property(S,file_name(Info)),!.
290 %get_stream_info1(S, Info) :-
291 % stream_property(S,alias(Info)),
292 % !.
293 %get_stream_info1(_S, unknown).
294
295
296
297
298
299
300 my_format(FS,Args) :- my_format(user_output,FS,Args).
301 my_format_error(FS,Args) :- my_format(user_error,FS,Args).
302 %my_format_error(Stream,FS,Args) :- my_format(Stream,FS,Args).
303
304 my_format(Stream,FS,Args) :- format(Stream,FS,Args),
305 (get_log_file(F)
306 -> open(F,append,S, [encoding(utf8)]),
307 format(S,FS,Args),
308 close(S)
309 ; true
310 ).
311
312 writeln_logtime_call_start(Term,timer(Time,WTime)) :-
313 ((logging_is_enabled ; runtime_profile_available) ->
314 statistics(runtime,[Time,_]),
315 statistics(walltime,[WTime,_]),
316 (logging_is_enabled
317 -> get_functors(Term,Fs),
318 writeln_log(start_call(walltime(WTime),Fs))
319 ; true)
320 ; true).
321
322 :- use_module(probsrc(tools),[statistics_memory_used/1]).
323 :- use_module(runtime_profiler,[register_profiler_runtime/5, runtime_profile_available/0]).
324 writeln_logtime_call_end(Term,timer(Time,WTime)) :-
325 %format(user_output,'End for ~w~n',[Time]),
326 (number(Time),number(WTime),
327 (logging_is_enabled ; runtime_profile_available) ->
328 statistics(runtime,[Time2,_]), RT is Time2-Time,
329 statistics(walltime,[WTime2,_]), WT is WTime2-WTime,
330 get_functors(Term,Fs),
331 (logging_is_enabled
332 -> statistics_memory_used(M), MB is M / 1000000, % used instead of deprecated 1048576
333 writeln_log(end___call(walltime(WTime2),delta_rt_wt(RT,WT),mb_used(MB),Fs))
334 ; true),
335 register_profiler_runtime(Fs,socket_server,unknown,RT,WT)
336 ; true).
337
338 get_functors(Var,V) :- var(Var),!, V='_'.
339 get_functors((A,B),(FA,FB)) :- !, get_functors(A,FA), get_functors(B,FB).
340 %get_functors(A,F/list(Len)) :- functor(A,F,1), arg(1,A,Ls), nonvar(Ls), Ls = [_|_],
341 % ground(Ls), length(Ls,Len),!.
342 get_functors(A,F/N) :- functor(A,F,N).
343
344 %runtime_entry(start) :- go_cli.
345
346 %save :- save_program('probcli.sav').