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