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'). |