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(parsercall, [load_b_machine_as_term/3,
6 load_b_machine_probfile_as_term/2, % a way to directly load a .prob file
7 load_b_machine_probfile_as_term/3,
8 load_b_machine_list_of_facts_as_term/2,
9 get_parser_version/1,
10 get_parser_version/2,
11 get_parser_version/6,
12 get_java_command_path/1,
13 check_java_version/2,
14 get_java_fullversion/1, get_java_fullversion/3, get_java_version/1,
15 ensure_console_parser_launched/0, % just make sure the console parser is up and running
16 connect_to_external_console_parser_on_port/1, % connect to a separately started parser
17 release_console_parser/0,
18 console_parser_jar_available_in_lib/0,
19 call_ltl_parser/3,
20 call_tla2b_parser/1, tla2b_filename/2,
21 %call_promela_parser/1, promela_prolog_filename/2,
22 call_alloy2pl_parser/2,
23 tla2prob_filename/2,
24 parse/3,
25 parse_at_position_in_file/5,
26 parse_formula/2, parse_predicate/2, parse_expression/2,
27 parse_substitution/2,
28 transform_string_template/3,
29 call_fuzz_parser/2,
30 register_parsing_call_back/1, deregister_parsing_call_back/0,
31 set_default_filenumber/2, reset_default_filenumber/2
32 ]).
33
34 :- meta_predicate register_parsing_call_back(4).
35
36 :- use_module(module_information,[module_info/2]).
37 :- module_info(group,typechecker).
38 :- module_info(description,'This module takes care of calling the Java B Parser if necessary.').
39
40 :- use_module(library(lists)).
41 :- use_module(library(process)).
42 :- use_module(library(file_systems)).
43 :- use_module(library(codesio)).
44 :- use_module(library(system)).
45 :- use_module(library(sockets)).
46
47 :- use_module(error_manager,[add_error/2, add_error/3, add_error/4, add_error_fail/3,
48 add_failed_call_error/1, add_internal_error/2, add_warning/3, add_warning/4, real_error_occurred/0,
49 add_message/3, add_message/4, extract_line_col/5, add_all_perrors/3]).
50 :- use_module(self_check).
51 :- use_module(preferences).
52 :- use_module(tools, [split_filename/3, same_file_name/2, get_PROBPATH/1, safe_atom_chars/3]).
53 :- use_module(tools_platform, [host_platform/1, platform_is_64_bit/0]).
54 :- use_module(tools_strings,[ajoin_with_sep/3, ajoin/2]).
55 :- use_module(tools_printing,[print_error/1, format_with_colour_nl/4]).
56 :- use_module(debug).
57 :- use_module(bmachine,[b_get_definition_name_with_pos/4, b_machine_is_loaded/0]).
58 :- use_module(specfile, [b_or_z_mode/0]).
59 :- use_module(system_call).
60
61 :- set_prolog_flag(double_quotes, codes).
62
63 :- dynamic java_parser_version/6.
64
65 % stores the java process of the parser, consisting of ProcessIdentifier, Socket Stream, STDErrStream
66 :- dynamic java_parser_process/4.
67 :- volatile java_parser_process/4.
68
69
70 send_definition(Stream,def(Name,Type,Arity)) :-
71 write(Stream,'definition'), nl(Stream),
72 format(Stream,'~w\n~w\n~w\n',[Name,Type,Arity]).
73
74 :- dynamic definitions_already_sent/0.
75 :- volatile definitions_already_sent/0.
76
77 send_definitions(ToParser) :-
78 b_or_z_mode, b_machine_is_loaded,
79 \+ definitions_already_sent,
80 !,
81 findall_definitions(L),
82 % format('~nSending definitions ~w~n~n',[L]),
83 maplist(send_definition(ToParser),L),
84 assertz(definitions_already_sent).
85 send_definitions(_).
86
87 findall_definitions(DefList) :-
88 findall(def(Name,Type,Arity),b_get_definition_name_with_pos(Name,Arity,Type,_),DefList).
89
90 get_definitions(L) :- b_or_z_mode, b_machine_is_loaded,!, findall_definitions(L).
91 get_definitions([]).
92
93 reset_definitions :-
94 retractall(definitions_already_sent),
95 parser_is_launched, % otherwise no need to reset; inside prob2_kernel there is no Java parser for probcli
96 (debug_mode(off) -> true
97 ; get_parser_version(Version),
98 format('Resetting DEFINITIONS for parser version ~w ~n',[Version])
99 ),
100 % TO DO: check if parser Version is at least 2.9.27
101 get_console_parser(ParserStream,Out,Err),!,
102 write(ParserStream,'resetdefinitions'), nl(ParserStream), % only supported in more recent versions of the parser
103 flush_output(ParserStream),
104 display_pending_outputs(Out,user_output),
105 display_pending_outputs(Err,user_error).
106 reset_definitions.
107
108 % update preferences of parser using new PREPL commands
109 update_jvm_parser_preferences :-
110 get_preference(jvm_parser_fastrw,FAST),
111 try_set_parser_option_nc(fastPrologOutput,FAST,_),
112 get_preference(jvm_parser_position_infos,LINENO),
113 try_set_parser_option_nc(addLineNumbers,LINENO,_),
114 % we have to set the swi mode here so it works with older parser versions
115 (current_prolog_flag(dialect, swi) -> SWI=true ; SWI=false),
116 try_set_parser_option_nc(swiSupport,SWI,_),
117 (debug_mode(off) -> VERBOSE=false ; VERBOSE=true),
118 try_set_parser_option_nc(verbose,VERBOSE,_).
119
120
121 :- dynamic cur_defaultFileNumber/1.
122
123 try_set_parser_option(defaultFileNumber,Value,Res) :- !,
124 (cur_defaultFileNumber(Value) % cache last value to avoid unnecessary parser calls
125 -> Res=prev_value(Value) % nothing to do
126 ; retractall(cur_defaultFileNumber(_)),
127 assert(cur_defaultFileNumber(Value)),
128 try_set_parser_option_nc(defaultFileNumber,Value,Res)
129 ).
130 try_set_parser_option(Name,Value,Res) :-
131 try_set_parser_option_nc(Name,Value,Res).
132
133 reset_parser_option_cache :- retractall(cur_defaultFileNumber(_)).
134
135 % try_set_parser_option_nc: non-caching version
136 try_set_parser_option_nc(Name,Value,Res) :-
137 parser_command_supported(setoption),
138 !,
139 debug_format(4,'Updating parser option: ~q=~q~n',[Name,Value]),
140 get_console_parser(Stream,_Out,Err),
141 write(Stream,setoption), nl(Stream),
142 write(Stream,Name), nl(Stream),
143 write(Stream,Value), nl(Stream),
144 flush_output(Stream),
145 read_line(Stream,CodesIn),
146 my_read_from_codes(CodesIn,Res,Stream,Err).
147 try_set_parser_option_nc(Name,Value,Res) :-
148 old_option_command(Name,Command),
149 parser_command_supported(Command),
150 !,
151 debug_format(19,'Updating JVM parser option (using old command ~q): ~q=~q~n',[Command,Name,Value]),
152 get_console_parser(Stream,_Out,_Err),
153 write(Stream,Command), nl(Stream),
154 write(Stream,Value), nl(Stream),
155 flush_output(Stream),
156 Res = changed. % prev_value isn't returned here
157 try_set_parser_option_nc(Name,Value,unsupported) :-
158 debug_format(19,'Parser too old to change option at runtime: ~q=~q~n',[Name,Value]).
159
160 %get_parser_option(Name,Value) :-
161 % parser_command_supported(getoption),
162 % !,
163 % debug_format(4,'Getting parser option: ~q~n',[Name]),
164 % get_console_parser(Stream,_Out,Err),
165 % write(Stream,getoption), nl(Stream),
166 % write(Stream,Name), nl(Stream),
167 % flush_output(Stream),
168 % read_line(Stream,CodesIn),
169 % my_read_from_codes(CodesIn,Value,Stream,Err).
170
171 old_option_command(addLineNumbers,lineno).
172 old_option_command(verbose,verbose).
173 old_option_command(fastPrologOutput,fastprolog).
174 old_option_command(compactPrologPositions,compactpos).
175 old_option_command(machineNameMustMatchFileName,checkname).
176
177 reset_old_parser_option_value(Name,Value,prev_value(Old)) :- \+ unchanged(Value,Old), !,
178 try_set_parser_option(Name,Old,_).
179 reset_old_parser_option_value(_,_,_).
180
181 % the Java values are stored as strings, even for number attributes
182 unchanged(V,V).
183 unchanged(N,A) :- number(N), atom(A), number_codes(N,C), atom_codes(A,C).
184
185 reset_parser :- reset_definitions, reset_parser_option_cache.
186 :- use_module(probsrc(eventhandling),[register_event_listener/3]).
187 :- register_event_listener(clear_specification,reset_parser,
188 'Remove DEFINITIONS from parser cache and reset parer options cache.').
189
190 crlf(10).
191 crlf(13).
192
193 % remove newlines in a B formula so that we can pass the formula as a single line to the parser
194 cleanup_newlines([],[]).
195 cleanup_newlines([H|T],CleanCodes) :- crlf(H),!,
196 % this could also be inside a multi-line string; the string will be modified by this conversion
197 CleanCodes=[8232|TC], % 8232 \x2028 is Unicode line separator
198 cleanup_newlines(T,TC).
199 %cleanup_newlines([47,47|T],CleanCodes) :-
200 % % a B Comment '//': we used to skip until end of line
201 % % but this could be inside a string ! see test 2236
202 % CleanCodes=[8232|TC], skip_until_crlf(T,T2), !, cleanup_newlines(T2,TC).
203 cleanup_newlines([H|T],[H|R]) :- cleanup_newlines(T,R).
204
205 %skip_until_crlf([],[]).
206 %skip_until_crlf([H|T],T) :- crlf(H),!.
207 %skip_until_crlf([_|T],R) :- skip_until_crlf(T,R).
208
209 % register parsing call back from prob_socket_server within ProB2
210 :- dynamic prob2_call_back_available/1.
211 register_parsing_call_back(CallBackPred4) :- deregister_parsing_call_back,
212 assertz(prob2_call_back_available(CallBackPred4)).
213 deregister_parsing_call_back :-
214 retractall(prob2_call_back_available(_)).
215
216 % ---------
217
218 %! parse_x(+Kind,+Codes,-Tree)
219 % Kind is formula, expression, predicate, substitution
220 %:- use_module(prob_socketserver,[prob2_call_back_available/0, prob2_call_back/2]).
221 parse_x(Kind,CodesWithNewlines,Tree) :-
222 parse_simple(Kind,CodesWithNewlines,Res),!,
223 % format('Parse simple ~s : ~w~n',[CodesWithNewlines,Res]),
224 Tree=Res.
225 parse_x(Kind,CodesWithNewlines,Tree) :-
226 parse_y(Kind,CodesWithNewlines,Tree).
227
228 % a version which does not attempt simple parsing without calling Java:
229 parse_y(Kind,CodesWithNewlines,Tree) :-
230 prob2_call_back_available(ParseCallBackPred),
231 cleanup_newlines(CodesWithNewlines,Codes), atom_codes(Formula,Codes),
232 debug_format(19,'Parsing ~w via call_back: ~w~n',[Kind,Formula]),
233 get_definitions(DefList),
234 call(ParseCallBackPred,Kind,DefList,Formula,Tree),
235 % TO DO: deal with substitutions
236 debug_println(19,prob2_call_back_available_parse_result(Tree)),
237 (Tree = call_back_not_supported ->
238 % Parsing callback isn't implemented (e. g. ProB Rodin plugin) - don't try to use it again in the future.
239 deregister_parsing_call_back,
240 fail
241 ; true),
242 !,
243 (Tree = parse_error(Exception)
244 -> handle_parser_exception(Exception)
245 ; functor(Tree,parse_error,_) % deprecated
246 -> throw(parse_errors([error('Parse error occurred via ProB2 call_back:',unknown)]))
247 ; true).
248 parse_y(Kind,CodesWithNewlines,Tree) :-
249 % Java parser expects only one line of input -> remove newlines
250 cleanup_newlines(CodesWithNewlines,Codes),
251 % statistics(walltime,[Tot,Delta]), format('~s~n~w~n0 ~w (Delta ~w) ms ~n',[Codes,Kind,Tot,Delta]),
252 get_console_parser(Stream,Out,Err),
253 send_definitions(Stream),
254 write(Stream,Kind),
255 nl(Stream),
256 format(Stream,'~s',[Codes]), %format(user_output,'sent: ~s~n',[Codes]),
257 nl(Stream),
258 flush_output(Stream),
259 read_line(Stream,CodesIn),
260 %format('read: ~s~n',[CodesIn]),
261 catch(
262 (my_read_from_codes(CodesIn,Tree,Stream,Err),handle_parser_exception(Tree)),
263 error(_,_),
264 (append("Illegal parser result exception: ",CodesIn,ErrMsgCodes),
265 atom_codes(ErrMsg,ErrMsgCodes),
266 throw(parse_errors([internal_error(ErrMsg,none)])))),
267 display_pending_outputs(Out,user_output).
268 %statistics(walltime,[Tot4,Delta4]), format('4 ~w (Delta ~w) ms ~n ~n',[Tot4,Delta4]).
269
270 % a few very simple cases, which can be parsed without accessing Java parser:
271 % common e.g., in JSON trace files or Latex files to avoid overhead of calling parser
272 parse_simple(Kind,Codes,AST) :-
273 (Kind=expression -> true ; Kind=formula),
274 (cur_defaultFileNumber(FN) -> true ; FN = -1),
275 parse_simple_codes(Codes,FN,1,1,AST).
276
277 % ---------------------------
278
279 % benchmarking code:
280 % statistics(walltime,[_W1,_]),(for(I,1,10000) do parsercall:parse_formula("123",Tree)),statistics(walltime,[_W2,_]),D is _W2-_W1.
281 % | ?- findall("|-> 123",between(2,10000,X),L), append(["123 "|L],Str), statistics(walltime,[_W1,_]),parsercall:parse_expression(Str,Tree), statistics(walltime,[_W2,_]),D is _W2-_W1.
282
283 parse_simple_codes(Codes,FileNr,SL,SC,AST) :-
284 parse_int_codes(Codes,Len,Val), !,
285 L2 is Len+SC, % EndColumn of p4 position (same line)
286 AST=integer(p4(FileNr,SL,SC,L2),Val).
287 parse_simple_codes("TRUE",FileNr,SL,SC,AST) :- !, EC is SC+4, AST=boolean_true(p4(FileNr,SL,SC,EC)).
288 parse_simple_codes("FALSE",FileNr,SL,SC,AST) :- !, EC is SC+5, AST=boolean_false(p4(FileNr,SL,SC,EC)).
289 parse_simple_codes("{}",FileNr,SL,SC,AST) :- !, EC is SC+2, AST=empty_set(p4(FileNr,SL,SC,EC)).
290 parse_simple_codes(Codes,FileNr,SL,SC,AST) :- is_real_literal_codes(Codes),!,
291 length(Codes,Len), L2 is Len+SC,
292 atom_codes(Atom,Codes),
293 AST=real(p4(FileNr,SL,SC,L2),Atom).
294 % TO DO: maybe simple string values, simple identifiers: but we need to know the keyword list for this
295
296 :- assert_must_succeed((parsercall:parse_int_codes("0",Len,Res), Len==1, Res==0)).
297 :- assert_must_succeed((parsercall:parse_int_codes("1",Len,Res), Len==1, Res==1)).
298 :- assert_must_succeed((parsercall:parse_int_codes("12",Len,Res), Len==2, Res==12)).
299 :- assert_must_succeed((parsercall:parse_int_codes("931",Len,Res), Len==3, Res==931)).
300 :- assert_must_succeed((parsercall:parse_int_codes("100931",Len,Res), Len==6, Res==100931)).
301 parse_int_codes([Digit|T],Len,Res) :- digit_code_2_int(Digit,DVal),
302 (DVal=0 -> T=[], Len=1, Res=0
303 ; parse_int2(T,DVal,Res,1,Len)).
304
305 parse_int2([],Acc,Acc,LenAcc,LenAcc).
306 parse_int2([Digit|T],Acc,Res,LenAcc,Len) :-
307 digit_code_2_int(Digit,DVal),
308 NewAcc is Acc*10 + DVal,
309 L1 is LenAcc+1,
310 parse_int2(T,NewAcc,Res,L1,Len).
311
312 digit_code_2_int(X,Val) :- X >= 48, X =< 57, Val is X - 48.
313 is_digit(X) :- X >= 48, X =< 57.
314
315 :- assert_must_succeed(parsercall:is_real_literal_codes("0.0")).
316 :- assert_must_succeed(parsercall:is_real_literal_codes("112300.0010")).
317 :- assert_must_succeed(parsercall:is_real_literal_codes("1234567890.9876543210")).
318 :- assert_must_succeed(parsercall:is_real_literal_codes("001.0")). % is accepted by parser
319 :- assert_must_fail(parsercall:is_real_literal_codes("0")).
320 :- assert_must_fail(parsercall:is_real_literal_codes("11.")).
321 :- assert_must_fail(parsercall:is_real_literal_codes(".12")).
322 :- assert_must_fail(parsercall:is_real_literal_codes("12a.0")).
323 % TODO: we could return length and merge with parse_int_codes to do only one traversal
324
325 ?is_real_literal_codes([Digit|T]) :- is_digit(Digit), is_real_lit1(T).
326 is_real_lit1([0'.,Digit|T]) :- is_digit(Digit), is_real_lit2(T).
327 ?is_real_lit1([Digit|T]) :- is_digit(Digit), is_real_lit1(T).
328 is_real_lit2([]).
329 is_real_lit2([Digit|T]) :- is_digit(Digit), is_real_lit2(T).
330
331 % ---------------------
332
333 my_read_from_codes(end_of_file,_,_,Err) :- !,
334 read_line_if_ready(Err,Err1Codes), % we just read one line
335 safe_name(ErrMsg,Err1Codes),
336 add_error(parsercall,'Abnormal termination of parser: ',ErrMsg),
337 missing_parser_diagnostics,
338 ajoin(['Parser not available (',ErrMsg,')'],FullErrMsg),
339 read_lines_and_add_as_error(Err), % add other info on error stream as single error
340 throw(parse_errors([error(FullErrMsg,none)])).
341 my_read_from_codes(ErrorCodes,_Tree,Out,_) :-
342 append("Error",_,ErrorCodes),!,
343 atom_codes(ErrMsg,ErrorCodes),
344 add_error(parsercall,'Error running/starting parser: ',ErrMsg),
345 read_lines_and_add_as_error(Out),
346 fail.
347 my_read_from_codes(CodesIn,Tree,_,_) :- read_from_codes(CodesIn,Tree).
348
349 % a version of my_read_from_codes which has no access to error stream
350 my_read_from_codes(end_of_file,_) :- !,
351 missing_parser_diagnostics,
352 throw(parse_errors([error('Parser not available (end_of_file on input stream)',none)])).
353 my_read_from_codes(ErrorCodes,_Tree) :-
354 append("Error",_,ErrorCodes),!,
355 atom_codes(ErrMsg,ErrorCodes),
356 add_error(parsercall,'Error running/starting parser: ',ErrMsg),
357 fail.
358 my_read_from_codes(CodesIn,Tree) :- read_from_codes(CodesIn,Tree).
359
360 :- use_module(probsrc(preferences),[get_prob_application_type/1]).
361 missing_parser_diagnostics :-
362 parser_location(Classpath), debug_println(9,classpath(Classpath)),fail.
363 missing_parser_diagnostics :- runtime_application_path(P),
364 atom_concat(P,'/lib/probcliparser.jar',ConParser), % TODO: adapt for GraalVM cliparser
365 (file_exists(ConParser)
366 -> add_error(parsercall,'The Java B parser (probcliparser.jar) cannot be launched: ',ConParser),
367 (get_prob_application_type(tcltk) ->
368 add_error(parsercall,'Please check that Java and B Parser are available using the "Check Java and Parser Version" command in the Debug menu.')
369 ; host_platform(windows) ->
370 add_error(parsercall,'Please check that Java and B Parser are available, e.g., using "probcli.exe -check_java_version" command.')
371 ; add_error(parsercall,'Please check that Java and B Parser are available, e.g., using "probcli -check_java_version" command.')
372 % application_type
373 % TODO: avoid printing the message when the user is already calling check_java_version
374 ),
375 (get_preference(jvm_parser_additional_args,ExtraArgStr), ExtraArgStr\=''
376 -> add_error(parsercall,'Also check your JVM_PARSER_ARGS preference value:',ExtraArgStr)
377 ; true)
378 ; add_internal_error('Java B parser (probcliparser.jar) is missing from lib directory in: ',P)
379 ).
380
381 % ProB2 cli builds do not have the cli parser bundled
382 % check if there is a jar available in the lib folder:
383 % should only happen for get_prob_application_type(probcli) in ProB2
384 console_parser_jar_available_in_lib :-
385 runtime_application_path(P),
386 atom_concat(P,'/lib/probcliparser.jar',ConParser),
387 file_exists(ConParser).
388
389 handle_parser_exception(Exception) :-
390 handle_parser_exception(Exception,ExAuxs,[]),
391 !,
392 throw(parse_errors(ExAuxs)).
393 handle_parser_exception(_).
394
395 handle_parser_exception(compound_exception([])) --> [].
396 handle_parser_exception(compound_exception([Ex|MoreEx])) -->
397 handle_parser_exception(Ex),
398 handle_parser_exception(compound_exception(MoreEx)).
399 % Non-list version of parse_exception is handled in handle_parser_exception_aux.
400 % (Note: The non-list version is no longer generated by the parser -
401 % see comments on handle_console_parser_result below.)
402 handle_parser_exception(parse_exception([],_Msg)) --> [].
403 handle_parser_exception(parse_exception([Pos|MorePos],Msg)) -->
404 [error(Msg,Pos)],
405 handle_parser_exception(parse_exception(MorePos,Msg)).
406 handle_parser_exception(Ex) -->
407 {handle_parser_exception_aux(Ex,ExAux)},
408 [ExAux].
409
410 handle_parser_exception_aux(parse_exception(Pos,Msg),error(SanitizedMsg,Pos)) :-
411 remove_msg_posinfo_known(Msg,SanitizedMsg).
412 handle_parser_exception_aux(io_exception(Pos,Msg),error(Msg,Pos)).
413 handle_parser_exception_aux(io_exception(Msg),error(Msg,unknown)).
414 handle_parser_exception_aux(exception(Msg),error(Msg,unknown)). % TO DO: get Pos from Java parser !
415
416 %! parse_formula(+Codes,-Tree)
417 parse_formula(Codes,Tree) :-
418 parse_x(formula,Codes,Tree).
419
420 %! parse_expression(+Codes,-Tree)
421 parse_expression(Codes,Tree) :-
422 parse_x(expression,Codes,Tree).
423
424 %! parse_predicate(+Codes,-Tree)
425 parse_predicate(Codes,Tree) :-
426 parse_x(predicate,Codes,Tree).
427
428 %! parse_substitution(+Codes,-Tree)
429 parse_substitution(Codes,Tree) :-
430 parse_x(substitution,Codes,Tree).
431
432 % parse in the context of particular files and position within the file (e.g., VisB JSON file)
433
434 parse_at_position_in_file(Kind,Codes,Tree,Span,Filenumber) :- Span \= unknown,
435 %format('Parse @ ~w~n ~s~n',[Span,Codes]),
436 extract_line_col_for_b_parser(Span,Line,Col),!,
437 parse_at_position_in_file2(Kind,Codes,Tree,Filenumber,Line,Col).
438 parse_at_position_in_file(Kind,Codes,Tree,_,_) :-
439 parse_x(Kind,Codes,Tree).
440
441 parse_at_position_in_file2(Kind,Codes,Tree,Filenumber,Line,Col) :-
442 (Kind=expression -> true ; Kind=formula),
443 % special case to avoid setting parser options if parser not called in parse_x !
444 parse_simple_codes(Codes,Filenumber,Line,Col,AST),!,
445 Tree=AST.
446 parse_at_position_in_file2(Kind,Codes,Tree,Filenumber,Line,Col) :-
447 (Line \= 1 -> try_set_parser_option_nc(startLineNumber,Line,_OldLine)
448 ; true), % default in ParsingBehaviour.java: 1
449 (Col \= 1 -> try_set_parser_option_nc(startColumnNumber,Col,_OldCol)
450 ; true), % default in ParsingBehaviour.java: 1
451 (integer(Filenumber) -> Fnr=Filenumber ; format('Invalid filenumber : ~w~n',[Filenumber]), Fnr = -1),
452 try_set_parser_option(defaultFileNumber,Fnr,OldFile),
453 % Note: Filenumber will be used in AST, but parse errors will have null as filename
454 % format('Parsing at line ~w col ~w in file ~w (old ~w:~w in ~w)~n',[Line,Col,Filenumber,OldLine,OldCol,OldFile]),
455 call_cleanup(parse_y(Kind,Codes,Tree),
456 (%reset_old_parser_option_value(startLineNumber,Line,OldLine), % not required anymore, is now volatile
457 %reset_old_parser_option_value(startColumnNumber,Col,OldCol), % not required anymore, is now volatile
458 % TODO: should we check at startup whether the parser has volatilePosOptions feature?
459 reset_old_parser_option_value(defaultFileNumber,Filenumber,OldFile))).
460
461 extract_line_col_for_b_parser(Span,Line,Col1) :-
462 extract_line_col(Span,Line,Col,_EndLine,_EndCol),
463 Col1 is Col+1. % the BParser starts column numbering at 1
464
465 set_default_filenumber(Filenumber,OldFile) :- try_set_parser_option(defaultFileNumber,Filenumber,OldFile).
466 reset_default_filenumber(Filenumber,OldFile) :- reset_old_parser_option_value(defaultFileNumber,Filenumber,OldFile).
467
468 %! parse(+Kind,+Codes,-Tree)
469 parse(Kind,Codes,Tree) :- parse_x(Kind,Codes,Tree).
470
471 %! parse_temporal_formula(+Kind,+LanguageExtension,+Formula,-Tree)
472 % Formula is either an atom or a codes list
473 % LanguageExtension is either ltl, ctl or pctl
474 % TODO: we could check if the parser supports the pctl command before sending it
475 parse_temporal_formula(Kind,LanguageExtension,Formula,Tree) :-
476 (Formula = [Nr|_], integer(Nr)
477 -> CodesWithNewlines = Formula
478 ; write_to_codes(Formula,CodesWithNewlines)
479 ),
480 % Java parser expects only one line of input -> remove newlines
481 cleanup_newlines(CodesWithNewlines,Codes),
482 get_console_parser(Stream,Out,Err),
483 send_definitions(Stream),
484 format(Stream,'~s', [Kind]), nl(Stream),
485 format(Stream,'~s', [LanguageExtension]), nl(Stream),
486 format(Stream,'~s',[Codes]), nl(Stream),
487 flush_output(Stream),
488 % format('Parsing temporal formula, kind=~s, lge=~s, formula="~s"~n',[Kind,LanguageExtension,Codes]),
489 read_line(Stream,CodesIn), % TODO: Improve feedback from java!
490 catch(my_read_from_codes(CodesIn,Tree,Stream,Err),_,throw(parse_errors([error(exception,none)]))),
491 display_pending_outputs(Out,user_output).
492
493 % throws parse_errors(Errors) in case of syntax errors
494 load_b_machine_as_term(Filename, Machine,Options) :- %print(load_b_machine(Filename)),nl,
495 prob_filename(Filename, ProBFile),
496 debug_println(9,prob_filename(Filename,ProBFile)),
497 ( get_preference(jvm_parser_force_parsing,false),
498 dont_need_compilation(Filename,ProBFile,Machine,LoadResult,Options) ->
499 % no compilation is needed, .prob file was loaded
500 release_parser_if_requested(Options),
501 (LoadResult=loaded -> debug_println(20,'.prob file up-to-date')
502 ; print_error('*** Loading failed *** '),nl,fail)
503 ; % we need to parse and generate .prob file
504 (debug:debug_mode(on) ->
505 time_with_msg('generating .prob file with Java parser',call_console_parser(Filename,ProBFile))
506 ; call_console_parser(Filename,ProBFile)
507 ),
508 release_parser_if_requested(Options),
509 load_b_machine_probfile_as_term(ProBFile, Options, Machine)
510 ).
511 release_parser_if_requested(Options) :- (member(release_java_parser,Options) -> release_console_parser ; true).
512
513 % converts the filename of the machine into a filename for the parsed machine
514 prob_filename(Filename, ProB) :-
515 split_filename(Filename,Basename,_Extension),
516 safe_atom_chars(Basename,BasenameC,prob_filename1),
517 append(BasenameC,['.','p','r','o','b'],ProBC),
518 safe_atom_chars(ProB,ProBC,prob_filename2),!.
519 prob_filename(Filename, ProB) :-
520 add_failed_call_error(prob_filename(Filename,ProB)),fail.
521
522 check_version_and_read_machine(Filename,ProBFile, ProbTime, Version, GitSha, Machine,Options) :-
523 (Version='$UNKNOWN'
524 -> add_warning(parsercall,'*** Unknown parser version number. Trying to load parsed file: ',ProBFile)
525 /* keep CheckVersionNr as variable */
526 ; CheckVersionNr=Version),
527 read_machine_term_from_file(ProBFile,prob_parser_version(CheckVersionNr,GitSha),
528 [check_if_up_to_date(Filename,ProbTime)|Options],Machine).
529
530 read_machine_term_from_file(ProBFile,VersionTerm,Options,CompleteMachine) :-
531 (debug:debug_mode(on)
532 -> time_with_msg('loading .prob file',
533 read_machine_term_from_file_aux(ProBFile,VersionTerm,Options,CompleteMachine))
534 ; read_machine_term_from_file_aux(ProBFile,VersionTerm,Options,CompleteMachine)).
535
536 read_machine_term_from_file_aux(ProBFile,VersionTerm,Options,complete_machine(MainName,Machines,Files)) :-
537 open_probfile(ProBFile,Options,Stream,Opt2),
538 call_cleanup(( safe_read_term(Stream,Opt2,ProBFile,parser_version,VersionTermInFile),
539 debug_format(9,'Parser version term in file: ~w~n',[VersionTermInFile]),
540 same_parser_version(VersionTermInFile,VersionTerm), % CHECK correct version
541 read_machines(Stream,ProBFile,Opt2,Machines,MainName,Files),
542 (var(MainName)
543 -> add_internal_error('Missing classical_b fact',ProBFile), MainName=unknown,Files=[]
544 ; true)
545 ),
546 close(Stream)).
547
548 % open a .prob file:
549 open_probfile(ProBFile,Options,NewStream,NewOptions) :-
550 open(ProBFile, read, Stream),
551 file_property(ProBFile,size_in_bytes,Size),
552 check_prob_file_not_empty(Stream,Size,ProBFile,Options),
553 peek_code(Stream,Code),
554 open_probfile_aux(Code,Size,Stream,ProBFile,Options,NewStream,NewOptions).
555
556 open_probfile_aux(Code,_,Stream,ProBFile,Options,NewStream,NewOptions) :-
557 fastrw_start_code(Code),!,
558 close(Stream),
559 add_message(parsercall,'Reading .prob file using fastrw library: ',ProBFile),
560 open(ProBFile, read, NewStream, [type(binary)]),
561 % delete(use_fastread)
562 NewOptions = [use_fastrw|Options].
563 open_probfile_aux(Code,Size,Stream,ProBFile,Options,Stream,NewOptions) :-
564 check_prob_file_first_code(Code,Stream,ProBFile,Options),
565 update_options(Options,Size,NewOptions).
566
567 % automatically use fastread if file large
568 update_options(Options,Size,Opt2) :- nonmember(use_fastread,Options),
569 nonmember(use_fastrw,Options),
570 Size>1000000, % greater than 1 MB
571 !, Opt2 = [use_fastread|Options],
572 debug_println(19,automatically_using_fastread(Size)).
573 update_options(Opts,_,Opts).
574
575 % check if the file starts out in an expected way
576 check_prob_file_not_empty(Stream,Size,ProBFile,Options) :- Size=<0,!,
577 close(Stream),
578 (member(check_if_up_to_date(_,_),Options)
579 -> add_warning(parsercall,'Re-running parser as .prob file is empty: ',ProBFile)
580 % due to possible crash or CTRL-C of previous parser run
581 ; add_internal_error('Generated .prob file is empty',ProBFile)
582 ),fail.
583 check_prob_file_not_empty(_,_,_,_).
584
585 % check first character code
586 check_prob_file_first_code(Code,Stream,ProBFile,Options) :-
587 (valid_start_code(Code) -> true
588 ; fastrw_start_code(Code)
589 -> close(Stream),
590 % we need to do: open(ProBFile,read,S,[type(binary)]),
591 (member(check_if_up_to_date(_,_),Options)
592 -> add_warning(parsercall,'Re-running parser as .prob file seems to be in new fast-rw format: ',ProBFile)
593 ; add_error(parsercall,'Cannot load .prob file; it seems to be in new fast-rw format:',ProBFile)
594 ),
595 fail
596 ; add_message(parsercall,'Strange start character code in .prob file: ',[Code]) % probably syntax error will happen
597 ).
598
599 :- if(current_prolog_flag(dialect, swi)).
600 fastrw_start_code(C) :- fastrw_start_code_swi(C).
601
602 fastrw_start_code_swi(C) :- platform_is_64_bit -> fastrw_start_code_swi_64(C) ; fastrw_start_code_swi_32(C).
603 fastrw_start_code_swi_64(98). % b / 0x62, base header for 64bit
604 fastrw_start_code_swi_64(114). % r / 0x72, base header + ground for 64bit
605 fastrw_start_code_swi_64(118). % v / 0x76, int fast path for 64bit
606 fastrw_start_code_swi_64(122). % z / 0x7a, atom fast path for 64bit
607 fastrw_start_code_swi_32(97). % a / 0x61, base header for 32bit
608 fastrw_start_code_swi_32(113). % q / 0x71, base header + ground for 32bit
609 fastrw_start_code_swi_32(117). % u / 0x75, int fast path for 32bit
610 fastrw_start_code_swi_32(121). % y / 0x79, atom fast path for 32bit
611 :- else.
612 fastrw_start_code(C) :- fastrw_start_code_sicstus(C).
613
614 fastrw_start_code_sicstus(0'D). % typical start DS...
615 :- endif.
616
617
618
619 valid_start_code(0'p). % from parser_version(_) term
620 valid_start_code(37). % percentage sign; appears when parser called with verbose flag
621 valid_start_code(47). % start of comment slash (inserted by user)
622 valid_start_code(39). % ' (inserted by user)
623 valid_start_code(32). % whitespace (inserted by user)
624 valid_start_code(8). % tab (inserted by user)
625 valid_start_code(10). % lf (inserted by user)
626 valid_start_code(13). % cr (inserted by user)
627
628 % --------------------
629
630 % use various read_term mechanisms depending on Options
631
632 safe_read_term(Stream,Options,File,Expecting,T) :-
633 catch(
634 safe_read_term2(Options,Stream,File,Expecting,T),
635 error(permission_error(_,_,_),ERR),
636 (
637 ajoin(['Permission error in .prob file trying to read ',Expecting,' term in ',File,':'],Msg),
638 add_internal_error(Msg,ERR),
639 fail
640 )).
641
642 :- use_module(tools_fastread,[read_term_from_stream/2, fastrw_read/3]).
643
644 safe_read_term2([use_fastrw|_],Stream,File,Expecting,Term) :- !,
645 fastrw_read(Stream,Term,Error),
646 (Error=false -> true
647 ; ajoin(['.prob (fastrw) file has error in ',Expecting,' term:'],Msg),
648 add_internal_error(Msg,File),
649 fail
650 ), functor(Term,F,N),debug_println(19,fast_read_term(F,N)).
651 safe_read_term2([use_fastread|_],Stream,File,Expecting,Term) :- !,
652 (read_term_from_stream(Stream,Term) -> true
653 ; ajoin(['.prob file has Prolog syntax error in ',Expecting,' term:'],Msg),
654 add_internal_error(Msg,File), fail
655 ).
656 safe_read_term2([_|Opts],Stream,File,Expecting,T) :- !,
657 safe_read_term2(Opts,Stream,File,Expecting,T).
658 safe_read_term2([],Stream,File,Expecting,T) :- % use regular SICStus Prolog reader
659 catch(read(Stream,T), error(E1,E2), (
660 ajoin(['.prob file (',File,') has error in ',Expecting,' term:'],Msg),
661 add_error(parser_call,Msg,error(E1,E2)),
662 fail
663 )).
664
665
666
667 % ------------------
668
669 % check if file was parsed with same parser version as currently in use by ProB
670 same_parser_version(parser_version(V), prob_parser_version(VB,GitSha)) :- !,
671 (V=VB -> true ; V=GitSha).
672 same_parser_version(end_of_file,_) :- !, debug_format(19,'.prob file is empty~n',[]).
673 same_parser_version(T,_) :-
674 add_internal_error('.prob file contains illegal parser_version term:',T),fail.
675
676 load_b_machine_list_of_facts_as_term(Facts,Machine) :-
677 read_machine_term_from_list_of_facts(Facts,_,Machine).
678 read_machine_term_from_list_of_facts(Facts,VersionTerm,complete_machine(MainName,Machines,FileList)) :-
679 (select(parser_version(VERS),Facts,F2) -> VersionTerm = parser_version(VERS)
680 ; add_internal_error('No parser_version available',read_machine_from_list_of_facts),
681 F2=Facts, VersionTerm = unknown),
682 (select(classical_b(MainName,FileList),F2,F3) -> true
683 ; add_internal_error('No classical_b file information available',read_machine_from_list_of_facts),
684 fail),
685 debug_println(9,loading_classical_b(VersionTerm,MainName,FileList)),
686 include(is_machine_term,F3,F4),
687 maplist(get_machine_term,F4,Machines).
688
689 is_machine_term(machine(_M)).
690 get_machine_term(machine(M),M).
691
692 load_b_machine_probfile_as_term(ProBFile, Machine) :-
693 load_b_machine_probfile_as_term(ProBFile, [], Machine).
694
695 load_b_machine_probfile_as_term(ProBFile, Options, Machine) :-
696 debug_println(9,consulting(ProBFile)),
697 ( read_machine_term_from_file(ProBFile,_VersionTerm,Options,Machine) -> true
698 ; add_error(parsercall,'Failed to read parser output: wrong format?',ProBFile),fail).
699
700 read_machines(S,ProBFile,Options,Machines,MainName,Files) :-
701 safe_read_term(S,Options,ProBFile,machine,Term),
702 %, write_term(Term,[max_depth(5),numbervars(true)]),nl,
703 ( Term == end_of_file ->
704 Machines = []
705 ; Term = classical_b(M,F) ->
706 ((M,F)=(MainName,Files) -> true ; add_internal_error('Inconsistent classical_b fact: ',classical_b(M,F))),
707 (member(check_if_up_to_date(MainFileName,ProbTime),Options)
708 -> debug_format(9,'Checking if .prob file up-to-date for subsidiary files and if it was generated for ~w~n',[MainFileName]),
709 all_older(Files, ProbTime), % avoid reading rest if subsidiary source files not all_older !
710 (Files = [File1|_],
711 same_file_name(MainFileName,File1) -> true
712 ; format('Re-parsing: .prob file created for different source file:~n ~w~n',[MainFileName]),
713 % this can happen, e.g., when we have M.def and M.mch and we previously loaded the other file
714 Files = [File1|_],
715 format(' ~w~n',[File1]),
716 fail
717 )
718 ; true),
719 read_machines(S,ProBFile,Options,Machines,MainName,Files)
720 ; Term = machine(M) ->
721 Machines = [M|Mrest],
722 read_machines(S,ProBFile,Options,Mrest,MainName,Files)
723 ).
724
725
726 % checks if all files that the prob-file depends on
727 % are older than the prob-file
728 dont_need_compilation(Filename,ProB,Machine,LoadResult,Options) :-
729 file_exists(Filename),
730 catch( ( get_parser_version(Version,GitSha),
731 file_property(Filename, modify_timestamp, BTime),
732 debug_format(9, 'Parser Version: ~w, Filename Timestamp: ~w : ~w~n',[Version,Filename,BTime]),
733 file_exists(ProB), % the .prob file exists
734 file_property(ProB, modify_timestamp, ProbTime),
735 debug_format(9, '.prob Timestamp: ~w : ~w~n',[ProB,ProbTime]),
736 % print(time_stamps(ProB,ProbTime,Filename,BTime)),nl,
737 BTime < ProbTime, % .mch file is older than .prob file
738 file_property(ProB,size_in_bytes,Size),
739 (Size>0 -> true
740 ; debug_mode(on),
741 add_message(parsercall,'.prob file is empty; parsing again',ProB),
742 % possibly due to crash or error before, cf second run of test 254
743 fail),
744 check_version_and_read_machine(Filename,ProB, ProbTime, Version, GitSha, Machine,Options),
745 %Machine = complete_machine(_,_,_),
746 LoadResult = loaded),
747 error(A,B),
748 (debug_println(9,error(A,B)),
749 (A=resource_error(memory)
750 -> add_error(load_b_machine,'Insufficient memory to load file.\nTry starting up ProB with more memory\n (e.g., setting GLOBALSTKSIZE=500M before starting ProB).'),
751 LoadResult=A
752 ; fail))).
753
754 % check that all included files are older than the .prob file (ProbTime):
755 all_older([],_).
756 all_older([File|Rest],ProbTime) :-
757 (file_exists(File)
758 -> file_property(File, modify_timestamp, BTime),
759 debug_format(9,' Subsidiary File Timestamp: ~w:~w~n',[File,BTime]),
760 ( BTime < ProbTime -> true
761 ; format('File has changed : ~w : ~w~n',[File,BTime]),
762 fail )
763 ; virtual_dsl_file(File) -> debug_format(9,'Virtual file generated by DSL translator: ~w~n',[File])
764 ; debug_format(20,'File does not exist anymore: ~w; calling parser.~n',[File]),fail),
765 all_older(Rest,ProbTime).
766
767 virtual_dsl_file(File) :- atom_codes(File,Codes),
768 Codes = [95|_], % file name starts with _ underscore
769 nonmember(47,Codes), % no slash
770 nonmember(92,Codes). % no backslash
771
772
773 get_extra_args_list(ExtraArgs) :-
774 get_preference(jvm_parser_additional_args,ExtraArgsStr),
775 ExtraArgsStr \= '',
776 atom_codes(ExtraArgsStr,C),
777 split_chars(C," ",CA),
778 maplist(atom_codes,ExtraArgs,CA).
779
780 jvm_options -->
781 ({get_preference(jvm_parser_heap_size_mb,Heap), Heap>0} ->
782 {ajoin(['-Xmx',Heap,'m'],HeapOpt)},
783 [HeapOpt]
784 ;
785 % comment in to simulate low-memory situations
786 % use -Xmx221500000m instead to force exception and test ProB's response
787 [] %['-Xmx20m']
788 ),
789
790 ({get_extra_args_list(ExtraArgs)} ->
791 {debug_format(19,'Using additional arguments for JVM (JVM_PARSER_ARGS): ~w~n',[ExtraArgs])},
792 ExtraArgs
793 % use the former LARGE_JVM / use_large_jvm_for_parser by default
794 % if we are running on a 64-bit system
795 % FIXME Is it intentional that this option is not added if JVM_PARSER_ARGS is set?
796 ; {platform_is_64_bit} -> ['-Xss5m'] % default stacksize; set to -Xss150k to mimic low stack setting
797 ; []
798 ).
799
800 parser_jvm_options -->
801 {get_PROBPATH(PROBPATH), atom_concat('-Dprob.stdlib=', PROBPATH, Stdlibpref)},
802 [Stdlibpref],
803 jvm_options.
804
805
806 % we could do something like this: or allow user to provide list of JVM options
807 %get_gc_options([]) :- !,get_preference(jvm_parser_aggressive_gc,true).
808 %get_gc_options(['-XX:GCTimeRatio=19', '-XX:MinHeapFreeRatio=20', '-XX:MaxHeapFreeRatio=30']).
809 % see https://stackoverflow.com/questions/30458195/does-gc-release-back-memory-to-os
810
811 parser_cli_options -->
812 %% ['-v'], % comment in for verbose, -time for timing info
813 ({debug_mode(on)} -> ['-v', '-time'] ; []),
814
815 % useful for very large data validation machines
816 ({get_preference(jvm_parser_position_infos,true)} -> ['-lineno'] ; []),
817
818 %( get_preference(jvm_parser_fastrw,false) ; parser_version_at_least(2,12,0) )
819 % we cannot call: parser_version_at_least(2,12,0) as parser not yet started
820 % older parsers were printing comments into the binary fastrw output; TODO: perform check later
821 ({get_preference(jvm_parser_fastrw,true)} -> ['-fastprolog'] ; ['-prolog']),
822
823 % enable swi support when required
824 % does not work on older parsers and version check is inaccessible here
825 % ({current_prolog_flag(dialect, swi)} -> ['-swi'] ; []),
826
827 % -compactpos enables new p3, p4, p5 position terms and disables node numbering
828 ['-prepl', '-compactpos'].
829
830 parser_command_args(native(NativeCmd), NativeCmd) -->
831 parser_jvm_options,
832 parser_cli_options.
833 parser_command_args(java_jar(NativeCmd,JarPath), NativeCmd) -->
834 parser_jvm_options,
835 ['-jar', JarPath],
836 parser_cli_options.
837
838 % ensure that the console Java process is running
839 ensure_console_parser_launched :-
840 catch(parse_formula("1",_), E, (
841 add_internal_error('Cannot launch console parser (probcliparser.jar)',E),
842 fail
843 )).
844
845 parser_is_launched :-
846 java_parser_process(_,_,_,_).
847
848
849 % TO DO: also store output stream for debugging messages
850 get_console_parser(Stream,Out,Err) :-
851 java_parser_process(PID,Stream,Out,Err),
852 % On SICStus, calling is_process seams to be unreliable (if the process has crashed)
853 % and process_wait does not always work either,
854 % so first check if in and output streams are still available.
855 \+ at_end_of_stream(Stream),
856 % On SWI, at_end_of_stream doesn't detect broken pipes,
857 % so additionally also check that the process has not exited/crashed.
858 process_wait(PID,timeout,[timeout(0)]),
859 !,
860 (at_end_of_stream(Err)
861 -> add_error(parsercall,'Java process not running'),
862 read_lines_and_add_as_error(Stream)
863 ; true).
864 get_console_parser(Stream,Out,Err) :-
865 clear_old_console_parsers,
866 get_java_command_for_parser(ParserCmd),
867 phrase(parser_command_args(ParserCmd, NativeCmd), FullArgs),
868 debug_println(19,launching_java_console_parser(NativeCmd,FullArgs)),
869 debug_print_system_call(NativeCmd,FullArgs),
870 system_call_keep_open_no_stdin(NativeCmd,FullArgs,PID,Out,Err,[]), % note: if probcliparser.jar does not exist we will not yet get an error here !
871 debug_println(9,java_console_parser_launched(PID)),
872 % read first line to get port number
873 safe_read_line(Out,Err,1,[],PortTerm),
874 connect_to_console_parser_on_port(PortTerm,PID,Out,Err,Stream),
875 !.
876 get_console_parser(_,_,_) :- missing_parser_diagnostics, fail.
877
878
879
880
881 connect_to_console_parser_on_port(PortTerm,PID,Out,Err,Stream) :-
882 catch(
883 socket_client_open('':PortTerm, Stream, [type(text),encoding(utf8)]),
884 Exc, %error(system_error,system_error(E)), % SPIO_E_NET_HOST_NOT_FOUND
885 (
886 ajoin(['Exception while opening parser socket on port ', PortTerm,
887 ' (possibly an error occurred during startup of the parser): '],Msg),
888 add_internal_error(Msg,Exc),
889 % e.g., not enough memory to start parser and wait for socket connection
890 read_lines_and_add_as_error(Err), % try and read additional info;
891 % if we set the stack size to be very small (-Xss20k) we get: Error: Could not create the Java Virtual Machine
892 fail
893 )),
894 assertz(java_parser_process(PID,Stream,Out,Err)).
895
896 % connect to a separately started parser
897 % allow to connect to a separately started java command line parser (java -jar probcliparser.jar -prepl)
898 connect_to_external_console_parser_on_port(PortNumber) :-
899 clear_old_console_parsers,
900 format('Trying to connect to external parser on port ~w~n',[PortNumber]),
901 Out=user_input, Err=user_input,
902 (connect_to_console_parser_on_port(PortNumber,external_process,Out,Err,_)
903 -> format('Connected to parser on port ~w~n',[PortNumber])
904 ; add_error(parsercall,'Could not connect to parser on port:',PortNumber)
905 ).
906
907 clear_old_console_parsers :-
908 retract(java_parser_process(PID,Stream,Out,Err)),
909 close_parser_stream(Stream), close_parser_stream(Out), close_parser_stream(Err),
910 parser_process_release(PID),
911 fail.
912 clear_old_console_parsers.
913
914 parser_process_release(external_process) :- !.
915 parser_process_release(PID) :- process_release(PID).
916
917 close_parser_stream(user_input) :- !. % happens when we call connect_to_external_console_parser_on_port
918 close_parser_stream(user_output) :- !.
919 close_parser_stream(Stream) :- close(Stream).
920
921 % useful to try and free up memory
922 % alternatively we could add some JVM options: -XX:GCTimeRatio=19 -XX:MinHeapFreeRatio=20 -XX:MaxHeapFreeRatio=30
923 % see https://stackoverflow.com/questions/30458195/does-gc-release-back-memory-to-os
924 release_console_parser :-
925 (java_parser_process(PID,Stream,Out,Err),
926 PID \= external_process
927 -> format('Releasing Java parser id=~w (note: access to DEFINITIONS is lost)~n',[PID]),
928 write(Stream,'halt'), nl(Stream),
929 flush_output(Stream), % handled in Java in runPRepl in CliBParser.java;
930 close_parser_stream(Stream), close_parser_stream(Out), close_parser_stream(Err),
931 retract(java_parser_process(PID,_,_,_)),
932 parser_process_release(PID) % or should we call process_kill ? process_kill(PID)
933 % translate:print_open_stream_stats
934 % Note: parser maybe launched again, but then we not have access to DEFINITIONS
935 ; true).
936
937 :- use_module(runtime_profiler,[profile_single_call/3]).
938 call_console_parser(Filename, ProB) :-
939 profile_single_call('$parsing',unknown,parsercall:call_console_parser2(Filename, ProB)).
940 call_console_parser2(Filename, ProB) :-
941 update_jvm_parser_preferences,
942 get_console_parser(Stream,Out,Err),
943
944 % path to the .prob file
945 replace_windows_path_backslashes(ProB,ProBW),
946 % the input file
947 replace_windows_path_backslashes(Filename,FilenameW),
948 % call PREPL 'machine' command
949 debug_format(4,'PREPL command: machine~n~w~n~w~n',[FilenameW,ProBW]),
950 format(Stream,'machine~n~w~n~w~n',[FilenameW,ProBW]), % tell parser to write output to ProBW .prob file
951 flush_output(Stream),
952
953 %% WARNING: if the java parser writes too much output on the out stream it will block
954 %% until its output is read and we have a deadlock !
955 %% hence we use safe_polling_read_line
956 safe_polling_read_line(Stream,Out,Err,1,[],Term),
957
958 display_pending_outputs(Out,user_output),
959 handle_console_parser_result(Term,Err).
960
961
962 safe_read_line(Out,Err,LineNr,SoFar,Term) :-
963 safe_read_line_aux(read_line,Out,Err,LineNr,SoFar,Term).
964
965 safe_read_line_if_ready(Out,Err,LineNr,SoFar,Term) :-
966 safe_read_line_aux(read_line_if_ready,Out,Err,LineNr,SoFar,Term).
967
968 % a version that will check every second if there is output to be read
969 safe_polling_read_line(Stream,_Out,Err,LineNr,SoFar,Term) :-
970 stream_ready_to_read(Stream,2),!, % try for two seconds
971 safe_read_line_aux(read_line,Stream,Err,LineNr,SoFar,Term).
972 safe_polling_read_line(Stream,Out,Err,LineNr,SoFar,Term) :-
973 % this should normally not happen unless we have a debugging version of the parser
974 debug_format(19,'Parser not responded yet, trying to read its output~n',[]),
975 display_pending_outputs(Out,user_output),
976 read_lines_and_add_as_error(Err),
977 safe_polling_read_line(Stream,Out,Err,LineNr,SoFar,Term).
978
979 safe_read_line_aux(Pred,Out,Err,LineNr,SoFar,Term) :-
980 catch(call(Pred,Out,Codes),Exception, % read another line
981 (add_error(parsercall,'Exception while reading next line: ',Exception),
982 read_lines_and_add_as_error(Err),
983 display_pending_outputs(user_error,Out),
984 throw(Exception))),
985 Codes \= end_of_file, !, % happens if parser crashed and stream is closed
986 append(SoFar,Codes,NewCodes),
987 catch(my_read_from_codes(NewCodes,Term,Out,Err),Exception,
988 safe_read_exception(Out,Err,LineNr,Exception,NewCodes,Term)).
989 safe_read_line_aux(_Pred,_Out,Err,_LineNr,CodesSoFar,_) :-
990 safe_name(T,CodesSoFar),
991 add_error(parsercall,'Unexpected error while parsing machine: ',T),
992 read_lines_and_add_as_error(Err),fail.
993
994
995 safe_read_exception(Out,_,1,_Exception,CodesSoFar,_Term) :- append("Error",_,CodesSoFar),!,
996 % probably some Java error, we do not obtain a correct Prolog term, but probably something like:
997 % "Error occurred during initialization of VM"
998 safe_name(T,CodesSoFar),
999 add_error(parsercall,'Java error while parsing machine: ',T),
1000 read_lines_and_add_as_error(Out),fail.
1001 safe_read_exception(Out,Err,LineNr,error(syntax_error(M),_),CodesSoFar,Term) :- LineNr<10, % avoid infinite loop in case unexpected errors occur which cannot be solved by reading more input lines
1002 !,
1003 %(debug:debug_mode(off) -> true ; format('Syntax error in parser result (line ~w): ~w~nTrying to read another line.~n',[LineNr,M])),
1004 add_warning(parsercall,'Syntax error in parser result; trying to read another line. Line:Error = ',LineNr:M),
1005 L1 is LineNr+1,
1006 safe_read_line_if_ready(Out,Err,L1,CodesSoFar,Term). % try and read another line; we assume the syntax error is because the TERM is not complete yet and transmitted on multiple lines (Windows issue)
1007 safe_read_exception(_,_,_LineNr,parse_errors(Errors),_CodesSoFar,_Term) :- !,
1008 debug_println(4,read_parse_errors(Errors)),
1009 throw(parse_errors(Errors)).
1010 safe_read_exception(_,_,_LineNr,Exception,_CodesSoFar,_Term) :-
1011 add_internal_error('Unexpected exception occurred during parsing: ',Exception),fail.
1012 %safe_name(T,CodesSoFar), add_error_fail(parsercall,'Unexpected error while parsing machine: ',T).
1013
1014 safe_name(Name,Codes) :- var(Name),Codes == end_of_file,!,
1015 %add_internal_error('Parser does not seem to be available',''),
1016 Name=end_of_file.
1017 safe_name(Name,Codes) :- number(Name),!,
1018 safe_number_codes(Name,Codes).
1019 safe_name(Name,Codes) :-
1020 catch(atom_codes(Name,Codes), E,
1021 (print('Exception during atom_codes: '),print(E),nl,nl,throw(E))).
1022
1023 safe_number_codes(Name,Codes) :-
1024 catch(number_codes(Name,Codes), E,
1025 (print('Exception during number_codes: '),print(E),nl,nl,throw(E))).
1026
1027 % Note: As of parser version 2.9.28 commit ee2592d8ca2900b4e339da973920e034dff43658,
1028 % all parse errors are reported as terms of the form
1029 % parse_exception(Positions,Msg) where Positions is a list of pos/5 terms.
1030 % The term formats preparse_exception(Tokens,Msg) (where Tokens is a list of none/0 or pos/3 terms)
1031 % and parse_exception(Pos,Msg) (where Pos is a single none/0, pos/3 or pos/5 term)
1032 % are no longer generated by the parser.
1033 % The code for handling these old term formats can probably be removed soon.
1034
1035 % see also handle_parser_exception
1036 %handle_console_parser_result(E,_) :- nl,print(E),nl,fail.
1037 handle_console_parser_result(exit(0),_) :- !.
1038 handle_console_parser_result(io_exception(Msg),_) :- !,
1039 add_error_fail(parsercall,'Error while opening the B file: ',Msg).
1040 handle_console_parser_result(compound_exception(List),ErrStream) :- !,
1041 get_compound_exceptions(List,ErrStream,ParseErrors,[]),
1042 throw(parse_errors(ParseErrors)).
1043 handle_console_parser_result(preparse_exception(Tokens,Msg),_) :- !,
1044 remove_msg_posinfo(Msg,SanitizedMsg,MsgPos),
1045 findall(error(SanitizedMsg,Pos),member(Pos,Tokens),Errors1),
1046 (Errors1 = []
1047 -> /* if there are no error tokens: use pos. info from text Msg */
1048 Errors = [error(SanitizedMsg,MsgPos)]
1049 ; Errors = Errors1),
1050 debug_println(4,preparse_exception_parse_errors(Tokens,Msg,Errors)),
1051 throw(parse_errors(Errors)).
1052 handle_console_parser_result(parse_exception([],Msg),_) :-
1053 atom(Msg), atom_codes(Msg,MC),
1054 append("StackOverflowError",_,MC),!,
1055 add_error(parsercall,'Java VM error while running parser: ',Msg),
1056 print_hint('Try increasing stack size for Java using the JVM_PARSER_ARGS preference (e.g.,"-Xss10m").'),
1057 fail.
1058 handle_console_parser_result(parse_exception(Positions,Msg),_) :-
1059 (Positions = [] ; Positions = [_|_]), !,
1060 remove_msg_posinfo(Msg,SanitizedMsg,MsgPos),
1061 findall(error(SanitizedMsg,Pos),member(Pos,Positions),Errors1),
1062 (Errors1 = []
1063 -> /* if there are no error tokens: use pos. info from text Msg */
1064 Errors = [error(SanitizedMsg,MsgPos)]
1065 ; Errors = Errors1),
1066 debug_println(4,parse_exception_parse_errors(Positions,Msg,Errors)),
1067 throw(parse_errors(Errors)).
1068 handle_console_parser_result(parse_exception(Pos,Msg),_) :- !,
1069 remove_msg_posinfo_known(Msg,SanitizedMsg), %print(sanitized(SanitizedMsg)),nl,
1070 debug_println(4,parse_exception(Pos,Msg,SanitizedMsg)),
1071 throw(parse_errors([error(SanitizedMsg,Pos)])).
1072 handle_console_parser_result(exception(Msg),_) :- !,
1073 %add_error(bmachine,'Error in the classical B parser: ', Msg),
1074 remove_msg_posinfo(Msg,SanitizedMsg,Pos),
1075 debug_println(4,exception_in_parser(Msg,SanitizedMsg,Pos)),
1076 throw(parse_errors([error(SanitizedMsg,Pos)])).
1077 handle_console_parser_result(end_of_file,Err) :- !,
1078 % probably NullPointerException or similar in parser; no result on StdOut
1079 debug_println(9,end_of_file_on_parser_output_stream),
1080 format(user_error,'Detected abnormal termination of B Parser~n',[]), % print in case we block
1081 read_line_if_ready(Err,Err1),
1082 (Err1=end_of_file -> Msg = 'Abnormal termination of B Parser: EOF on streams'
1083 ; append("Abnormal termination of B Parser: ",Err1,ErrMsgCodes),
1084 safe_name(Msg,ErrMsgCodes),
1085 read_lines_and_add_as_error(Err) % also show additional error infos
1086 ),
1087 throw(parse_errors([error(Msg,none)])).
1088 handle_console_parser_result(compound_exception(Exs),_) :- !,
1089 maplist(handle_parser_exception_aux,Exs,ExAuxs),
1090 debug_println(4,compound_exception(Exs,ExAuxs)),
1091 throw(parse_errors(ExAuxs)).
1092 handle_console_parser_result(Term,_) :- !,
1093 write_term_to_codes(Term,Text,[]),
1094 safe_name(Msg,Text),
1095 %add_error(bmachine,'Error in the classical B parser: ', Msg),
1096 remove_msg_posinfo(Msg,SanitizedMsg,Pos),
1097 debug_println(4,unknown_error_term(Term,SanitizedMsg,Pos)),
1098 throw(parse_errors([error(SanitizedMsg,Pos)])).
1099
1100 % get all compound exceptions as a single result to be thrown once later:
1101 get_compound_exceptions([],_) --> [].
1102 get_compound_exceptions([Err1|T],ErrStream) -->
1103 {handle_and_catch(Err1,ErrStream,ParseErrors) },
1104 ParseErrors,
1105 get_compound_exceptions(T,ErrStream).
1106
1107 handle_and_catch(Exception,ErrStream,ParseErrors) :-
1108 catch(
1109 (handle_console_parser_result(Exception,ErrStream) -> ParseErrors=[] ; ParseErrors=[]),
1110 parse_errors(Errors1),
1111 ParseErrors=Errors1).
1112
1113 % now replaced by remove_msg_posinfo:
1114 %extract_position_info(Text,pos(Row,Col,Filename)) :-
1115 % atom_codes(Text,Codes),
1116 % epi(Row,Col,Filename,Codes,_),!.
1117 %extract_position_info(_Text,none).
1118
1119 :- assert_must_succeed((parsercall:epi(R,C,F,"[2,3] xxx in file: /usr/lib.c",[]), R==2,C==3,F=='/usr/lib.c')).
1120 :- assert_must_succeed((parsercall:epi(R,C,F,"[22,33] xxx yyy ",_), R==22,C==33,F=='unknown')).
1121
1122 % we expect error messages to start with [Line,Col] information
1123 epi(Row,Col,Filename) --> " ",!,epi(Row,Col,Filename).
1124 epi(Row,Col,Filename) --> "[", epi_number(Row),",",epi_number(Col),"]",
1125 (epi_filename(Filename) -> [] ; {Filename=unknown}).
1126 epi_number(N) --> epi_numbers(Chars),{safe_number_codes(N,Chars)}.
1127 epi_numbers([C|Rest]) --> [C],{is_number(C)},epi_numbers2(Rest).
1128 epi_numbers2([C|Rest]) --> [C],{is_number(C),!},epi_numbers2(Rest).
1129 epi_numbers2("") --> !.
1130 ?is_number(C) :- member(C,"0123456789"),!.
1131 epi_filename(F) --> " in file: ",!,epi_path2(Chars),{safe_name(F,Chars)}.
1132 epi_filename(F) --> [_], epi_filename(F).
1133 epi_path2([C|Rest]) --> [C],!,epi_path2(Rest). % assume everything until the end is a filename
1134 epi_path2([]) --> [].
1135
1136 :- assert_must_succeed((parsercall:remove_rowcol(R,C,"[22,33] xxx yyy ",_), R==22,C==33)).
1137 % remove parser location info from message to avoid user clutter
1138 remove_rowcol(Row,Col) --> " ",!, remove_rowcol(Row,Col).
1139 remove_rowcol(Row,Col) --> "[", epi_number(Row),",",epi_number(Col),"]".
1140
1141 :- assert_must_succeed((parsercall:remove_filename(F,C,"xxx yyy in file: a.out",R), F == 'a.out', C == "xxx yyy", R==[])).
1142 remove_filename(F,[]) --> " in file: ",!,epi_path2(Chars),{safe_name(F,Chars)}.
1143 remove_filename(F,[C|T]) --> [C], remove_filename(F,T).
1144
1145 :- assert_must_succeed((parsercall:remove_filename_from_codes("xxx yyy in file: a.out",F,C), F == 'a.out', C == "xxx yyy")).
1146 :- assert_must_succeed((parsercall:remove_filename_from_codes("xxx yyy zzz",F,C), F == 'unknown', C == "xxx yyy zzz")).
1147 remove_filename_from_codes(Codes,F,NewCodes) :-
1148 (remove_filename(F,C1,Codes,C2) -> append(C1,C2,NewCodes) ; F=unknown, NewCodes=Codes).
1149
1150 % obtain position information from a message atom and remove the parts from the message at the same time
1151 remove_msg_posinfo_known(Msg,NewMsg) :- remove_msg_posinfo(Msg,NewMsg,_,pos_already_known).
1152 remove_msg_posinfo(Msg,NewMsg,Pos) :- remove_msg_posinfo(Msg,NewMsg,Pos,not_known).
1153 remove_msg_posinfo(Msg,NewMsg,Pos,AlreadyKnown) :- %print(msg(Msg,AlreadyKnown)),nl,
1154 atom_codes(Msg,Codes),
1155 (remove_rowcol(Row,Col,Codes,RestCodes)
1156 -> Pos=pos(Row,Col,Filename),
1157 remove_filename_from_codes(RestCodes,Filename,NewCodes)
1158 ; AlreadyKnown==pos_already_known ->
1159 Pos = none,
1160 remove_filename_from_codes(Codes,_Filename2,NewCodes)
1161 ;
1162 NewCodes=Codes, Pos=none
1163 % do not remove filename: we have not found a position and cannot return the filename
1164 % see, e.g., public_examples/B/Tickets/Hansen27_NestedMchErr/M1.mch
1165 ),
1166 !,
1167 atom_codes(NewMsg,NewCodes).
1168 remove_msg_posinfo(M,M,none,_).
1169
1170
1171 % ----------------------
1172
1173 parser_command_supported(_) :-
1174 prob2_call_back_available(_), % TODO: support at least setoption in parser callback in ProB2
1175 !,
1176 fail.
1177 parser_command_supported(Command) :-
1178 parser_version_at_least(2,12,2),
1179 !,
1180 query_command_supported(Command,true).
1181 parser_command_supported(Command) :-
1182 (Command = fastprolog
1183 ; Command = compactpos
1184 ; Command = verbose
1185 ; Command = checkname
1186 ; Command = lineno
1187 ),
1188 !,
1189 parser_version_at_least(2,12,0).
1190
1191 :- dynamic query_command_supported_cached/2.
1192
1193 query_command_supported(Command,Res) :-
1194 query_command_supported_cached(Command,Res),
1195 !.
1196 query_command_supported(Command,Res) :-
1197 get_console_parser(Stream,_Out,Err),
1198 !,
1199 write(Stream,'commandsupported'), nl(Stream),
1200 write(Stream,Command), nl(Stream),
1201 flush_output(Stream),
1202 read_line(Stream,CodesIn),
1203 my_read_from_codes(CodesIn,Res,Stream,Err),
1204 assertz(query_command_supported_cached(Command,Res)).
1205
1206 % java_parser_version(VersionStr) :- java_parser_version(VersionStr,_,_,_,_,_).
1207
1208 parser_version_at_least(RV1,RV2,RV3) :-
1209 get_parser_version(_,V1,V2,V3,_,_),
1210 lex_leq([RV1,RV2,RV3],[V1,V2,V3]).
1211
1212 lex_leq([V1|_],[VV1|_]) :- number(VV1), % with old parsers this can be '?'
1213 V1 < VV1,!.
1214 lex_leq([V1|T1],[V1|T2]) :- lex_leq(T1,T2).
1215 lex_leq([],_).
1216
1217
1218 get_parser_version(VersionStr) :- get_parser_version(VersionStr,_).
1219 get_parser_version(VersionStr,GitSha) :- get_parser_version(VersionStr,_,_,_,_,GitSha).
1220
1221 get_parser_version(VersionStr,V1,V2,V3,SNAPSHOT,GitSha) :- java_parser_version(VersionStr,V1,V2,V3,SNAPSHOT,GitSha),!.
1222 get_parser_version(VersionStr,V1,V2,V3,SNAPSHOT,GitSha) :-
1223 get_version_from_parser(VersionStr),
1224 !,
1225 ? (get_version_numbers(VersionStr,V1,V2,V3,SNAPSHOT,GitSha)
1226 -> assertz(java_parser_version(VersionStr,V1,V2,V3,SNAPSHOT,GitSha)),
1227 debug_format(19,'Parser version recognized ~w.~w.~w (SNAPSHOT=~w)~n',[V1,V2,V3,SNAPSHOT])
1228 ; assertz(java_parser_version(VersionStr,'?','?','?','?','?'))
1229 ).
1230 get_parser_version(_Vers,_V1,_V2,_V3,_SNAPSHOT,_GitSha) :-
1231 (real_error_occurred -> true % already produced error messages in get_version_from_parser
1232 ; add_error(get_parser_version,'Could not get parser version.')),
1233 %missing_parser_diagnostics, % already called if necessary by get_version_from_parser
1234 fail.
1235
1236 :- use_module(probsrc(tools),[split_atom/3,atom_to_number/2]).
1237 % newer parsers generate a version string like 2.9.27-GITSHA or 2.9.27-SNAPSHOT-GITSHA; older ones just GITSHA
1238 get_version_numbers(VersionStr,V1,V2,V3,SNAPSHOT,GitSha) :-
1239 split_atom(VersionStr,['.'],List),
1240 [AV1,AV2,AV3T] = List,
1241 split_atom(AV3T,['-'],List2),
1242 [AV3,Suffix1|T] = List2,
1243 ? atom_to_number(AV1,V1),
1244 ? atom_to_number(AV2,V2),
1245 ? atom_to_number(AV3,V3),
1246 (Suffix1 = 'SNAPSHOT' -> SNAPSHOT=true, [GitSha]=T
1247 ; T=[], SNAPSHOT=false, GitSha=Suffix1).
1248
1249
1250 get_version_from_parser(Version) :-
1251 get_console_parser(Stream,Out,Err),
1252 write(Stream,'version'), nl(Stream),
1253 flush_output(Stream),
1254 read_line(Stream,Text), % if parser cannot be started we receive end_of_file; length will fail
1255 (Text = end_of_file -> add_error(parsercall,'Could not get parser version: '),
1256 read_lines_and_add_as_error(Err),fail
1257 ; length(Text,Length),
1258 ( append("Error",_,Text)
1259 -> atom_codes(ErrMsg,Text),
1260 add_error(parsercall,'Error getting parser version: ',ErrMsg),
1261 read_lines_and_add_as_error(Stream),fail
1262 ; Length < 100 -> atom_codes(Version,Text)
1263 ; prefix_length(Text,Prefix,100),
1264 append(Prefix,"...",Full),
1265 safe_name(Msg,Full),
1266 add_error_fail(parsercall, 'B parser returned unexpected version string: ', Msg))
1267 ),
1268 display_pending_outputs(Out,user_output).
1269
1270 :- use_module(library(sockets),[socket_select/7]).
1271 % check if a stream is ready for reading
1272 stream_ready_to_read(Out) :- stream_ready_to_read(Out,1). % wait 1 second, off: wait forever
1273 stream_ready_to_read(Out,TO) :- var(Out),!,
1274 add_internal_error('Illegal stream: ',stream_ready_to_read(Out,TO)),fail.
1275 stream_ready_to_read(Out,TO) :-
1276 socket_select([],_, [Out],RReady, [],_, TO), % wait TO sec at most %print(ready(Out,RReady)),nl,
1277 RReady == [Out].
1278
1279
1280 read_lines_and_add_as_error(Out) :- read_lines_until_eof(Out,false,ErrMsgCodes,[]),
1281 (ErrMsgCodes=[] -> true
1282 ; ErrMsgCodes=[10] -> true % just a single newline
1283 ; ErrMsgCodes=[13] -> true % ditto
1284 ; safe_name(ErrMsg,ErrMsgCodes),
1285 add_error(parsercall,'Additional information: ',ErrMsg),
1286 analyse_java_error_msg(ErrMsgCodes)
1287 ).
1288
1289 % analyse error messages from the JVM; providing possible solutions:
1290 analyse_java_error_msg(ErrMsgCodes) :-
1291 append([_,"java.lang.OutOfMemoryError",_],ErrMsgCodes),!,
1292 % a typical message contains: Exception in thread "main" java.lang.OutOfMemoryError: GC overhead limit exceeded
1293 % or: Exception in ...: Java heap space
1294 print_hint('Try increasing memory for Java by setting the JVM_PARSER_HEAP_MB preference.'),
1295 print_hint('You can also provide custom JVM arguments using the JVM_PARSER_ARGS preference.').
1296 analyse_java_error_msg(ErrMsgCodes) :-
1297 append([_,"java.lang.StackOverflowError",_],ErrMsgCodes),!,
1298 print_hint('Try increasing stack size for Java using the JVM_PARSER_ARGS preference (e.g.,"-Xss10m").').
1299 analyse_java_error_msg(_).
1300
1301 print_hint(Msg) :- format_with_colour_nl(user_error,[blue],'~w',[Msg]).
1302
1303 read_line_if_ready(Stream,Line) :- stream_ready_to_read(Stream), !, read_line(Stream,Line).
1304 read_line_if_ready(_,end_of_file). % pretend we are at the eof
1305
1306 read_lines_until_eof(Out,NewlineRequired) --> {read_line_if_ready(Out,Text)},
1307 !,
1308 ({Text = end_of_file} -> []
1309 ; ({NewlineRequired==true} -> "\n" ; []),
1310 Text, %{format("read: ~s~n",[Text])},
1311 read_lines_until_eof(Out,true)).
1312 read_lines_until_eof(_Out,_) --> [].
1313
1314 % display pending output lines from a stream
1315 display_pending_outputs(OutStream,ToStream) :- stream_ready_to_read(OutStream,0), !, read_line(OutStream,Line),
1316 (Line=end_of_file -> true
1317 ; format(ToStream,' =parser-output=> ~s~n',[Line]),
1318 display_pending_outputs(OutStream,ToStream)).
1319 display_pending_outputs(_,_).
1320
1321 :- use_module(tools,[get_tail_filename/2]).
1322 get_java_command_for_parser(native(GraalNativeCmd)) :-
1323 (parser_location(GraalNativeCmd)
1324 -> get_tail_filename(GraalNativeCmd,'cliparser'),
1325 (file_exists(GraalNativeCmd) -> true
1326 ; add_warning(parsercall,'Path to parser points to non-existant compiled GraalVM binary: ',GraalNativeCmd)
1327 )
1328 ; fail, % comment out fail to enable auto-detection of cliparser in lib folder
1329 library_abs_name('cliparser',GraalNativeCmd),
1330 file_exists(GraalNativeCmd)
1331 ),
1332 format('Using GRAAL native parser at ~w~n',[GraalNativeCmd]),
1333 !.
1334 get_java_command_for_parser(java_jar(JavaCmdW,JarPathW)) :-
1335 (parser_location(JarPath) -> true ; library_abs_name('probcliparser.jar',JarPath)),
1336 get_java_command_path(JavaCmdW),
1337 replace_windows_path_backslashes(JarPath,JarPathW).
1338
1339 parser_location(PathToParser) :- get_preference(path_to_java_parser,PathToParser), PathToParser \= ''.
1340
1341 % a predicate to check whether we have correct java version number and whether java seems to work ok
1342 % ResultStatus=compatible if everything is ok
1343 check_java_version(VersionCheckResult,ResultStatus) :- get_java_fullversion(Version),!,
1344 check_java_version_aux(Version,VersionCheckResult,ResultStatus).
1345 check_java_version(VersionCheckResult,error) :- get_java_command_for_parser(java_jar(JavaCmdW,JarPathW)),!,
1346 ajoin(['*** Unable to launch java command: ',JavaCmdW,' (classpath: ',JarPathW,')!'],VersionCheckResult).
1347 check_java_version('*** Unable to launch Java or get path to java command!',error). % should not happen
1348
1349 check_java_version_aux(VersionCodes,VersionCheckResult,ResultStatus) :-
1350 get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom),!,
1351 check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,ResultStatus).
1352 check_java_version_aux(VersionCodes,VersionCheckResult,error) :-
1353 atom_codes(VersionA,VersionCodes),
1354 ajoin(['*** Unable to identify Java version number: ',VersionA, ' !'],VersionCheckResult).
1355
1356 check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,compatible) :- java_version_ok_for_parser(V1,V2,V3Atom),
1357 get_java_version(_),!, % if get_java_version fails, this is an indication that Java not fully installed with admin rights
1358 ajoin(['Java is correctly installed and version ',V1,'.',V2,'.',V3Atom,
1359 ' is compatible with ProB requirements (>= 1.7).'],VersionCheckResult).
1360 check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,error) :- java_version_ok_for_parser(V1,V2,V3Atom),!,
1361 ajoin(['*** Java version ',V1,'.',V2,'.',V3Atom,
1362 ' is compatible with ProB requirements (>= 1.7) ',
1363 'but does not seem to be correctly installed: reinstall Java with admin rights!'],VersionCheckResult).
1364 check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,incompatible) :-
1365 get_java_version(_),!,
1366 ajoin(['*** Java is correctly installed but version ',V1,'.',V2,'.',V3Atom,
1367 ' is *not* compatible with ProB requirements (>= 1.7)!'],VersionCheckResult).
1368 check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,error) :-
1369 ajoin(['*** Java is not correctly installed and version ',V1,'.',V2,'.',V3Atom,
1370 ' is *not* compatible with ProB requirements (>= 1.7)!'],VersionCheckResult).
1371
1372
1373 % we need Java 1.7 or higher
1374 java_version_ok_for_parser(V1,_V2,_) :- V1>1.
1375 java_version_ok_for_parser(1,V2,_) :- V2>=7.
1376
1377 get_java_fullversion(V1,V2,V3Atom) :-
1378 get_java_fullversion(VersionCodes),
1379 get_java_fullversion_numbers(VersionCodes,VV1,VV2,VV3),!,
1380 V1=VV1, V2=VV2, V3Atom=VV3.
1381
1382 :- assert_must_succeed((parsercall:get_java_fullversion_numbers("openjdk full version \"1.8.0_312\"",V1,V2,V3),
1383 V1==1, V2==8, V3=='0_312')).
1384 :- assert_must_succeed((parsercall:get_java_fullversion_numbers("openjdk full version \"15+36-1562\"",V1,V2,V3),
1385 V1==1, V2==15, V3=='36-1562')).
1386 :- assert_must_succeed((parsercall:get_java_fullversion_numbers("java full version \"17.0.1+12-LTS-39\"",V1,V2,V3),
1387 V1==1, V2==17, V3=='0.1+12-LTS-39')). % Oracle JDK on macOS
1388 :- use_module(tools,[split_chars/3]).
1389 get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom) :-
1390 append("java full version """,Tail,VersionCodes), !,
1391 get_java_fullversion_numbers_aux(Tail,V1,V2,V3Atom).
1392 get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom) :-
1393 append("openjdk full version """,Tail,VersionCodes), !,
1394 get_java_fullversion_numbers_aux(Tail,V1,V2,V3Atom).
1395 get_java_fullversion_numbers_aux(Tail,1,V2,V3Atom) :-
1396 % new version scheme (https://openjdk.java.net/jeps/223), leading 1 dropped, 13+33 stands for 1.13.33
1397 split_chars(Tail,"+",[V2C,V3C]),
1398 !,
1399 (try_number_codes(V2,V2C)
1400 -> get_v3_atom(V3C,V3Atom)
1401 ; append(V2CC,[0'. | FurtherC], V2C) % there is at least one more dot in the version nr (e.g. 17.0.1+12-LTS-39)
1402 ->
1403 try_number_codes(V2,V2CC),
1404 append(FurtherC,[0'+ | V3C], V3C3),
1405 get_v3_atom(V3C3,V3Atom)
1406 ).
1407 get_java_fullversion_numbers_aux(Tail,V1,V2,V3Atom) :-
1408 split_chars(Tail,".",[V1C,V2C|FurtherC]),
1409 append(FurtherC,V3C),
1410 try_number_codes(V1,V1C),
1411 try_number_codes(V2,V2C),!,
1412 get_v3_atom(V3C,V3Atom).
1413
1414 get_v3_atom(V3C,V3Atom) :- strip_closing_quote(V3C,V3C2),
1415 atom_codes(V3Atom,V3C2).
1416
1417 try_number_codes(Name,Codes) :-
1418 catch(number_codes(Name,Codes), _Exc, fail).
1419
1420 strip_closing_quote([],[]).
1421 strip_closing_quote([H|_],R) :- (H=34 ; H=32),!, R=[]. % closing " or newline
1422 strip_closing_quote([H|T],[H|R]) :- strip_closing_quote(T,R).
1423
1424 % get java fullversion as code list; format "java full version "...."\n"
1425 get_java_fullversion(Version) :-
1426 get_java_command_path(JavaCmdW),
1427 (my_system_call(JavaCmdW, ['-fullversion'],java_version,Text) -> Text=Version
1428 ; format(user_error,'Could not execute ~w -fullversion~n',[JavaCmdW]),
1429 fail).
1430
1431 % when java -fullversion works but not java -version it seems that Java was improperly
1432 % installed without admin rights (http://stackoverflow.com/questions/11808829/jre-1-7-returns-java-lang-noclassdeffounderror-java-lang-object)
1433 get_java_version(Version) :-
1434 get_java_command_path(JavaCmdW),
1435 (my_system_call(JavaCmdW, ['-version'],java_version,Text) -> Text=Version
1436 ; format(user_error,'Could not execute ~w -version~n',[JavaCmdW]),
1437 fail).
1438 % should we check for JAVA_PATH first ? would allow user to override java; but default pref would have to be set to ''
1439 get_java_command_path(JavaCmdW) :-
1440 %host_platform(darwin)
1441 get_preference(path_to_java,X),
1442 debug_println(8,path_to_java_preference(X)),
1443 (X=''
1444 ; preference_default_value(path_to_java,Default), debug_println(8,default(Default)),
1445 Default=X
1446 ),
1447 % only try this when the Java path has not been set explicitly
1448 % on Mac: /usr/bin/java exists even when Java not installed ! it is a fake java command that launches a dialog
1449 ? absolute_file_name(path(java),
1450 JavaCmd,
1451 [access(exist),extensions(['.exe','']),solutions(all),file_errors(fail)]),
1452 debug_println(8,obtained_java_cmd_from_path(JavaCmd)),
1453 replace_windows_path_backslashes(JavaCmd,JavaCmdW),
1454 !.
1455 get_java_command_path(JavaCmdW) :- get_preference(path_to_java,JavaCmd),
1456 JavaCmd \= '',
1457 debug_println(8,using_path_to_java_preference(JavaCmd)),
1458 (file_exists(JavaCmd) -> true
1459 ; directory_exists(JavaCmd) -> add_warning(get_java_command_path,'No Java Runtime (7 or newer) found; please correct the JAVA_PATH advanced preference (it has to point to the java tool, *not* the directory enclosing it): ',JavaCmd)
1460 ; add_warning(get_java_command_path,'No Java Runtime (7 or newer) found; please correct the JAVA_PATH advanced preference: ',JavaCmd)),
1461 replace_windows_path_backslashes(JavaCmd,JavaCmdW),
1462 !.
1463 get_java_command_path(_JavaCmd) :-
1464 add_error(get_java_command_path,'Could not get path to the java tool. Make sure a Java Runtime (7 or newer) is installed',''),
1465 fail.
1466
1467 library_abs_name(Lib,Abs) :- absolute_file_name(prob_lib(Lib),Abs).
1468
1469 % CtlOrLtl is either ctl, ltl, or pctl
1470 call_ltl_parser(Formulas, CtlOrLtl, Result) :-
1471 get_ltl_lang_spec(LangSpec),
1472 maplist(parse_temporal_formula(CtlOrLtl,LangSpec),Formulas,Result).
1473
1474 :- use_module(specfile,[b_or_z_mode/0,csp_with_bz_mode/0]).
1475 get_ltl_lang_spec('B,none') :- csp_with_bz_mode,!.
1476 get_ltl_lang_spec('B') :- b_or_z_mode,!.
1477 get_ltl_lang_spec(none).
1478
1479 /* unused code :
1480 generate_formula_codes([F]) -->
1481 !,generate_formula_codes2(F),"\n".
1482 generate_formula_codes([F|Rest]) -->
1483 generate_formula_codes2(F), "###\n",
1484 generate_formula_codes(Rest).
1485 generate_formula_codes2(F) -->
1486 write_to_codes(F).
1487 */
1488
1489
1490 % ---------------------------
1491
1492 % call the TLA2B parser to translate a TLA file into a B machine
1493 call_tla2b_parser(TLAFile) :-
1494 get_java_command_path(JavaCmdW),
1495 replace_windows_path_backslashes(TLAFile,TLAFileW),
1496 phrase(jvm_options, XOpts),
1497 absolute_file_name(prob_lib('TLA2B.jar'),TLA2BJAR),
1498 append(XOpts,['-jar',file(TLA2BJAR),file(TLAFileW)],FullArgs),
1499 % other possible options -verbose -version -config FILE
1500 (my_system_call(JavaCmdW, FullArgs,tla2b_parser)
1501 -> true
1502 ; \+ file_exists(TLA2BJAR),
1503 print_error('Be sure to download TLA2B.jar from https://stups.hhu-hosting.de/downloads/prob/tcltk/jars/,'),
1504 print_error('and put it into the ProB lib/ directory.'),
1505 fail
1506 ).
1507
1508 %call_cspmj_parser(CSPFile,PrologFile) :-
1509 % get_java_command_path(JavaCmdW),
1510 % replace_windows_path_backslashes(CSPFile,CSPFileW),
1511 % phrase(jvm_options, XOpts),
1512 % absolute_file_name(prob_lib('cspmj.jar'),CSPMJAR),
1513 % get_writable_compiled_filename(CSPFile,'.pl',PrologFile),
1514 % tools:string_concatenate('--prologOut=', PrologFile, PrologFileOutArg),
1515 % append(XOpts,['-jar',CSPMJAR,'-parse',CSPFileW,PrologFileOutArg],FullArgs),
1516 % debug_println(9,calling_java(FullArgs)),
1517 % (my_system_call(JavaCmdW, FullArgs,cspmj_parser) -> true
1518 % ; print_error('Be sure that cspmj.jar parser is installed.'),
1519 % fail).
1520
1521
1522 tla2prob_filename(TLAFile,GeneratedProbFile) :-
1523 split_filename(TLAFile,Basename,_Extension),
1524 atom_chars(Basename,BasenameC),
1525 append(BasenameC,['.','p','r','o','b'],TLABC),
1526 atom_chars(GeneratedProbFile,TLABC),!.
1527 tla2prob_filename(Filename, GeneratedProbFile) :-
1528 add_failed_call_error(tla2b_filename(Filename,GeneratedProbFile)),fail.
1529
1530 tla2b_filename(TLAFile,BFile) :-
1531 split_filename(TLAFile,Basename,_Extension),
1532 atom_chars(Basename,BasenameC),
1533 append(BasenameC,['_',t,l,a,'.','m','c','h'],TLABC),
1534 atom_chars(BFile,TLABC),!.
1535 tla2b_filename(Filename, BFile) :-
1536 add_failed_call_error(tla2b_filename(Filename,BFile)),fail.
1537
1538
1539 my_system_call(Command,Args,Origin) :- my_system_call(Command,Args,Origin,_Text).
1540 my_system_call(Command,Args,Origin,ErrText) :-
1541 debug_print_system_call(Command,Args),
1542 system_call(Command,Args,ErrText,Exit), %nl,print(exit(Exit)),nl,nl,
1543 treat_exit_code(Exit,Command,Args,ErrText,Origin).
1544
1545 debug_print_system_call(Command,Args) :-
1546 (debug_mode(off) -> true ; print_system_call(Command,Args), flush_output).
1547 print_system_call(Command,Args) :-
1548 ajoin_with_sep(Args,' ',FS), format(user_output,'Executing: ~w ~w~n',[Command,FS]).
1549
1550 my_system_call5(Command,Args,Origin,OutputText,ErrText) :-
1551 system_call(Command,Args,OutputText,ErrText,Exit), %nl,print(exit(Exit)),nl,nl,
1552 treat_exit_code(Exit,Command,Args,ErrText,Origin).
1553
1554 treat_exit_code(exit(0),_,_,_,_) :- !.
1555 treat_exit_code(Exit,Command,Args,ErrText,Origin) :-
1556 debug_println(9,treat_exit_code(Exit,Command,Args,ErrText,Origin)),
1557 catch( my_read_from_codes(ErrText,Term),
1558 _,
1559 (safe_name(T,ErrText),Term = T)), !,
1560 %print_error(Term),
1561 (Term = end_of_file -> ErrMsg = '' ; ErrMsg = Term),
1562 ajoin(['Exit code ',Exit,' for command ',Command, ', error message: '],Msg),
1563 (get_error_position_from_term(Origin,Term,Pos)
1564 -> add_error(Origin,Msg,ErrMsg,Pos)
1565 ; add_error(Origin,Msg,ErrMsg)
1566 ),
1567 fail.
1568
1569
1570 get_error_position_from_term(alloy2b,Term,Pos) :- atom(Term),
1571 atom_codes(Term,Codes), get_error_position_from_codes(Codes,Pos).
1572
1573 % Alloy error message: ! Exception in thread "main" Type error in .../Restrictions.als at line 41 column 23:
1574 get_error_position_from_codes([97,116,32,108,105,110,101,32|Tail],lineCol(Line,Col)) :- % "at line "
1575 epi_number(Line,Tail,RestTail),
1576 (RestTail = [32,99,111,108,117,109,110,32|Tail2], % "column "
1577 epi_number(Col,Tail2,_) -> true
1578 ; Col=0).
1579 get_error_position_from_codes([_|T],Pos) :- get_error_position_from_codes(T,Pos).
1580
1581 % replace backslashes by forward slashes in atoms, only under windows
1582 % TODO(DP,14.8.2008): Check if still needed with SICStus 4.0.4 and if
1583 % everybody uses that version
1584 replace_windows_path_backslashes(Old,New) :-
1585 ( host_platform(windows) ->
1586 safe_name(Old,OldStr),
1587 replace_string_backslashes(OldStr,NewStr),
1588 safe_name(New,NewStr)
1589 ;
1590 Old=New).
1591
1592 replace_string_backslashes([],[]) :- !.
1593 replace_string_backslashes([C|OldRest],[N|NewRest]) :- !,
1594 ( C=92 /* backslash */ ->
1595 N=47 /* forward slash */
1596 ;
1597 N=C ),
1598 replace_string_backslashes(OldRest,NewRest).
1599 replace_string_backslashes(X,Y) :-
1600 add_error(parsercall,'Illegal call: ',replace_string_backslashes(X,Y)),
1601 fail.
1602
1603 % ---------------------------
1604
1605 :- assert_must_succeed((parsercall:parse_string_template("0",Res), Res==[string_codes("0")])).
1606 :- assert_must_succeed((parsercall:parse_string_template("ab${xy}cd",Res),
1607 Res==[string_codes("ab"),template_codes("xy",2,3,[]),string_codes("cd")])).
1608 :- assert_must_succeed((parsercall:parse_string_template("ab${xy}$<<z>>cd$\xab\v\xbb\",Res),
1609 Res==[string_codes("ab"),template_codes("xy",2,3,[]),template_codes("z",3,5,[]),
1610 string_codes("cd"),template_codes("v",2,3,[])])). % \xab\ is double angle
1611
1612 % parse a ProB string template
1613 % each recognised template is an expression.
1614 parse_string_template(Codes,TemplateList) :- %format("parsing: ~s~n",[Codes]),
1615 parse_string_template([],TemplateList,Codes,[]).
1616
1617 parse_string_template(Acc,TemplateList) -->
1618 ? template_inside_string(Str,StartOffset,AdditionalChars,Options),!,
1619 {add_acc_string(Acc,TemplateList,
1620 [template_codes(Str,StartOffset,AdditionalChars,Options)|T])},
1621 parse_string_template([],T).
1622 parse_string_template(Acc,TemplateList) --> [H], !, parse_string_template([H|Acc],TemplateList).
1623 parse_string_template(Acc,TemplateList) --> "", {add_acc_string(Acc,TemplateList,[])}.
1624
1625 % add accumulator as regular string before a detected template ${...}
1626 add_acc_string([],L,R) :- !, L=R.
1627 add_acc_string(Acc,[string_codes(Str)|T],T) :- reverse(Acc,Str).
1628
1629 template_inside_string(Str,StartOffset,AdditionalChars,Options) --> "$",
1630 template_options(Options,OptLen),
1631 ? template_open_paren(ClosingParen,ParenLen),
1632 {StartOffset is OptLen+ParenLen+1,
1633 AdditionalChars is StartOffset+ParenLen}, % add closing parentheses length
1634 template_content(Str,ClosingParen).
1635
1636 template_options(Options,Len) --> "[", template_options2(Options,Len).
1637 template_options([],0) --> [].
1638
1639 template_options2([H|T],Len) --> template_option(H,HLen), !, template_options3(T,HLen,Len).
1640 template_options2([],2) --> "]".
1641 template_options3([H|T],AccLen,Len) --> ",", template_option(H,HLen), !,
1642 {A1 is AccLen+HLen},template_options3(T,A1,Len).
1643 template_options3([],AccLen,Len) --> "]", {Len is AccLen+2}.
1644 template_option(ascii,5) --> "ascii".
1645 template_option(ascii,1) --> "a".
1646 template_option(unicode,7) --> "unicode".
1647 template_option(unicode,1) --> "u".
1648 template_option(template_width(Option,Nr),L1) --> digits(Nr,Len),template_width_option(Option,LO), {L1 is Len+LO}.
1649 % other options could be hex output or padding, ...
1650 % TODO: provide error feedback when option/template parsing fails
1651
1652 template_width_option(float_fixed_point,1) --> "f".
1653 template_width_option(integer_decimal_string,1) --> "d".
1654 template_width_option(pad_string(' '),1) --> "p".
1655
1656 digits(MinusNr,Len) --> "-",!, digit(X), digits2(X,Nr,2,Len), {MinusNr is -Nr}.
1657 digits(Nr,Len) --> digit(X), digits2(X,Nr,1,Len).
1658 digits2(X,Nr,AccLen,Len) --> digit(Y), !, {XY is X*10+Y, A1 is AccLen+1}, digits2(XY,Nr,A1,Len).
1659 digits2(X,X,Len,Len) --> "".
1660
1661 digit(Nr) --> [X], {X >= 48, X=<57, Nr is X-48}.
1662
1663 template_open_paren("}",1) --> "{".
1664 template_open_paren(">>",2) --> "<<".
1665 template_open_paren([187],1) --> [ 171 ]. % Double angle quotation mark "«»"
1666
1667 template_content("",Closing) --> Closing,!.
1668 template_content([H|T],Closing) --> [H], template_content(T,Closing).
1669
1670 % TODO: offset span within template
1671 parse_template_b_expression(Span,Filenumber,template_codes(Codes,_,_,Options),RawStrExpr) :-
1672 \+ get_prob_application_type(rodin), % in Rodin parser callback is not available
1673 !,
1674 catch( parse_at_position_in_file(expression,Codes,RawExpr,Span,Filenumber),
1675 parse_errors(Errors),
1676 (add_all_perrors(Errors,[],parse_template_string), % add_all_perrors_in_context_of_used_filenames?
1677 fail)
1678 ),
1679 create_to_string_conversion(RawExpr,Span,Options,RawStrExpr).
1680 parse_template_b_expression(Span,_,template_codes(Codes,_,_,_),string(Span,Atom)) :-
1681 atom_codes(Atom,Codes).
1682 parse_template_b_expression(Span,_,string_codes(Codes),string(Span,Atom)) :-
1683 atom_codes(Atom,Codes).
1684
1685 :- assert_must_succeed((parsercall:transform_string_template('1+1 = ${1+1}',p3(1,1,12),Res),
1686 Res= general_concat(_,sequence_extension(_,[_|_])) )).
1687 :- assert_must_succeed((parsercall:transform_string_template('abc',p3(1,1,3),Res),
1688 Res= string(_,'abc') )).
1689
1690 :- use_module(error_manager,[extract_file_number_and_name/3]).
1691 % transform a string template into a raw expression that computes a string value
1692 transform_string_template(Atom,Span,RawExpr) :-
1693 atom_codes(Atom,Codes),
1694 parse_string_template(Codes,TemplateList),
1695 ? transform_str_templ_aux(TemplateList,Atom,Span,RawExpr).
1696
1697 transform_str_templ_aux([string_codes(_)],Atom,Span,RawExpr) :- !,
1698 debug_println(19,unnecessary_string_template(Span)), % regular string suffices
1699 RawExpr = string(Span,Atom).
1700 transform_str_templ_aux(TemplateList,_,Span,RawExpr) :-
1701 (extract_file_number_and_name(Span,FileNr,_) -> true ; FileNr = -1),
1702 InitialOffset = 3, % for three starting quotes
1703 ? l_parse_templates(TemplateList,0,InitialOffset,Span,FileNr,BTemplateList),
1704 generate_conc_expr(BTemplateList,Span,RawExpr).
1705
1706 :- use_module(tools_positions, [add_col_offset_to_position/3, add_line_col_offset_to_position/4]).
1707 l_parse_templates([],_,_,_,_,[]).
1708 l_parse_templates([Templ1|T],LineOffset,ColOffset,Span,FileNr,[RawStrExpr|BT]) :-
1709 templ_start_offset(Templ1,StartOffset),
1710 CO2 is ColOffset+StartOffset, % e.g., add two chars for ${ in case Templ1 is a template
1711 add_line_col_offset_to_position(Span,LineOffset,CO2,Span1),
1712 % it is only start position of Span1 that is important
1713 parse_template_b_expression(Span1,FileNr,Templ1,RawStrExpr),
1714 ? count_template_offset(Templ1,LineOffset,ColOffset,LineOffset2,ColOffset2),
1715 ? l_parse_templates(T,LineOffset2,ColOffset2,Span,FileNr,BT).
1716
1717 % accumulate length of template part and add to line/col offset to be added to start of template string
1718 count_template_offset(template_codes(Codes,_StartOffset,AdditionalChars,_),L,C,LineOffset,C3) :-
1719 ? count_offset(Codes,L,C,LineOffset,ColOffset),
1720 C3 is ColOffset+AdditionalChars. % e.g., 3 for ${.}
1721 count_template_offset(string_codes(Codes),L,C,LineOffset,ColOffset) :-
1722 ? count_offset(Codes,L,C,LineOffset,ColOffset).
1723
1724 templ_start_offset(template_codes(_,StartOffset,_,_),StartOffset). % usually 2 for ${
1725 templ_start_offset(string_codes(_),0).
1726
1727 % count line/column offset inside a list of codes:
1728 %count_offset(Codes,LineOffset,ColOffset) :- count_offset(Codes,0,0,LineOffset,ColOffset).
1729 count_offset([],Line,Col,Line,Col).
1730 count_offset(Codes,L,_ColOffset,Line,Col) :- newline(Codes,T),!,
1731 L1 is L+1,
1732 count_offset(T,L1,0,Line,Col).
1733 count_offset([_|T],L,ColOffset,Line,Col) :- C1 is ColOffset+1,
1734 ? count_offset(T,L,C1,Line,Col).
1735
1736 newline([10|T],T).
1737 newline([13|X],T) :- (X=[10|TX] -> T=TX ; T=X). % TO DO: should we check if we are on Windows ?
1738
1739 % generate a raw expression for the concatenation of a list of expressions
1740 generate_conc_expr([],Pos,string(Pos,'')).
1741 generate_conc_expr([OneEl],_,Res) :- !, Res = OneEl. % no need to concatenate
1742 generate_conc_expr(List,Pos,general_concat(Pos,sequence_extension(Pos,List))).
1743
1744 create_to_string_conversion(RawExpr,Pos,Options,
1745 external_function_call_auto(Pos,'STRING_PADLEFT',[RawStrExpr,Len,Char])) :-
1746 select(template_width(pad_string(PadChar),Nr),Options,RestOpts),!,
1747 create_to_string_conversion(RawExpr,Pos,RestOpts,RawStrExpr),
1748 Char = string(Pos,PadChar),
1749 Len = integer(Pos,Nr).
1750 create_to_string_conversion(RawExpr,Pos,Options,RawStrExpr) :-
1751 is_definitely_string(RawExpr),!,
1752 (Options=[] -> true
1753 ; add_warning(string_template,'Ignoring options in string template (already a string): ',Options, Pos)),
1754 RawStrExpr=RawExpr.
1755 create_to_string_conversion(RawExpr,Pos,Options,external_function_call_auto(Pos,'REAL_TO_DEC_STRING',[RawExpr,Prec])) :-
1756 select_option(template_width(float_fixed_point,Nr),Options,Pos),!,
1757 Prec = integer(Pos,Nr).
1758 create_to_string_conversion(RawExpr,Pos,Options,external_function_call_auto(Pos,'INT_TO_DEC_STRING',[RawExpr,Prec])) :-
1759 select_option(template_width(integer_decimal_string,Nr),Options,Pos),!,
1760 Prec = integer(Pos,Nr).
1761 create_to_string_conversion(RawExpr,Pos,Options,external_function_call_auto(Pos,'TO_STRING_UNICODE',[RawExpr])) :-
1762 select_option(unicode,Options,Pos),!. % TODO use a TO_STRING function with options list
1763 create_to_string_conversion(RawExpr,Pos,_Options,external_function_call_auto(Pos,'TO_STRING',[RawExpr])).
1764
1765 select_option(Option,Options,Pos) :-
1766 select(Option,Options,Rest),
1767 (Rest=[] -> true ; add_warning(string_template,'Ignoring additional string template options: ',Rest,Pos)).
1768
1769
1770 is_definitely_string(string(_,_)).
1771
1772 % ---------------------------
1773 :- use_module(pathes,[runtime_application_path/1]).
1774
1775 call_jar_parser(PMLFile,JARFile,Args,ParserName) :-
1776 get_java_command_path(JavaCmdW),
1777 replace_windows_path_backslashes(PMLFile,PMLFileW),
1778 phrase(jvm_options, XOpts),
1779 absolute_file_name(prob_lib(JARFile),FullJAR),
1780 append(XOpts,['-jar',FullJAR,PMLFileW|Args],FullArgs),
1781 %format('Java: ~w, Parser: ~w, Args: ~w~n',[JavaCmdW,ParserName,FullArgs]),
1782 my_system_call(JavaCmdW, FullArgs,ParserName).
1783
1784
1785
1786 call_alloy2pl_parser(AlloyFile,BFile) :-
1787 alloy_pl_filename(AlloyFile,BFile),
1788 call_alloy2pl_parser_aux(AlloyFile,'alloy2b.jar',BFile).
1789
1790 call_alloy2pl_parser_aux(AlloyFile,JARFile,PrologBFile) :-
1791 compilation_not_needed(AlloyFile,PrologBFile,JARFile),!.
1792 call_alloy2pl_parser_aux(AlloyFile,JARFile,PrologBFile) :-
1793 (file_exists(PrologBFile) -> delete_file(PrologBFile) ; true), % TODO: only delete generated files
1794 replace_windows_path_backslashes(PrologBFile,BFileW),
1795 call_jar_parser(AlloyFile,JARFile,['-toProlog',BFileW],alloy2b).
1796
1797 alloy_pl_filename(AlloyFile,BFile) :- atom_codes(AlloyFile,BasenameC),
1798 append(BasenameC,".pl",NewC),
1799 atom_codes(BFile,NewC),!.
1800 alloy_pl_filename(Filename, BFile) :-
1801 add_failed_call_error(alloy_pl_filename(Filename,BFile)),fail.
1802
1803 compilation_not_needed(BaseFile,DerivedFile,LibraryFile) :-
1804 file_exists(BaseFile),
1805 file_property(BaseFile, modify_timestamp, BTime),
1806 %system:datime(BTime,datime(_Year,Month,Day,Hour,Min,Sec)), format('~w modfied on ~w/~w at ~w:~w (~w sec)~n',[BaseFile,Day,Month,Hour,Min,Sec]),
1807 file_exists(DerivedFile),
1808 file_property(DerivedFile, modify_timestamp, DTime),
1809 DTime > BTime,
1810 absolute_file_name(prob_lib(LibraryFile),FullLibFile),
1811 (file_exists(FullLibFile)
1812 -> file_property(FullLibFile, modify_timestamp, LibTime),
1813 DTime > LibTime % check that file was generated by this library (hopefully); ideally we should put version numbers into the DerivedFiles
1814 ; true % Jar/command not available anyway; use the derived file
1815 ).
1816
1817 % ---------------------------
1818
1819 call_fuzz_parser(TexFile,FuzzFile) :-
1820 get_command_in_lib(fuzz,FuzzCmd),
1821 absolute_file_name(prob_lib('fuzzlib'),FUZZLIB), % TO DO: windows
1822 fuzz_filename(TexFile,FuzzFile),
1823 % fuzz options:
1824 % -d Allow use before definition
1825 % -l Lisp-style echoing of input
1826 % -p file Use <file> in place of standard prelude
1827 debug_format(19,'Fuzz: running ~w -d -l with library ~w on ~w~n',[FuzzCmd,FUZZLIB,TexFile]),
1828 (file_exists(FUZZLIB)
1829 -> my_system_call5(FuzzCmd,['-d', '-l', '-p', file(FUZZLIB), file(TexFile)],call_fuzz_parser,Text,_ErrText)
1830 ; my_system_call5(FuzzCmd,['-d', '-l', file(TexFile)],call_fuzz_parser,Text,_ErrText)
1831 ),
1832 format('Writing fuzz AST to ~s~n',[FuzzFile]),
1833 open(FuzzFile,write,Stream),
1834 call_cleanup(format(Stream,'~s~n',[Text]), close(Stream)).
1835
1836 get_command_in_lib(Name,Command) :-
1837 get_binary_extensions(Extensions),
1838 absolute_file_name(prob_lib(Name),
1839 Command,
1840 [access(exist),extensions(Extensions),solutions(all),file_errors(fail)]).
1841
1842 get_binary_extensions(List) :-
1843 host_platform(windows),!, List=['.exe','']. % will backtrack in get_command_in_lib
1844 get_binary_extensions(['']).
1845
1846 fuzz_filename(TexFile,FuzzFile) :-
1847 split_filename(TexFile,Basename,_Extension),
1848 atom_chars(Basename,BasenameC),
1849 append(BasenameC,['.','f','u','z','z'],CC),
1850 atom_chars(FuzzFile,CC),!.
1851 fuzz_filename(TexFile, FuzzFile) :-
1852 add_failed_call_error(fuzz_filename(TexFile,FuzzFile)),fail.