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