| 1 | | % (c) 2009-2019 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/2, |
| 6 | | load_b_machine_probfile_as_term/2, % a way to directly load a .prob file |
| 7 | | load_b_machine_list_of_facts_as_term/2, |
| 8 | | get_parser_version/1, |
| 9 | | get_java_command_path/1, |
| 10 | | check_java_version/2, |
| 11 | | get_java_fullversion/1, get_java_fullversion/3, get_java_version/1, |
| 12 | | ensure_console_parser_launched/0, % just make sure the console parser is up and running |
| 13 | | call_ltl_parser/3, |
| 14 | | call_tla2b_parser/1, tla2b_filename/2, |
| 15 | | %call_promela_parser/1, promela_prolog_filename/2, |
| 16 | | call_alloy2pl_parser/2, |
| 17 | | tla2prob_filename/2, |
| 18 | | parse/3, |
| 19 | | parse_formula/2, parse_predicate/2, parse_expression/2, |
| 20 | | parse_substitution/2, |
| 21 | | call_fuzz_parser/2 |
| 22 | | ]). |
| 23 | | |
| 24 | | |
| 25 | | :- use_module(module_information,[module_info/2]). |
| 26 | | :- module_info(group,typechecker). |
| 27 | | :- module_info(description,'This module takes care of calling the Java B Parser if necessary.'). |
| 28 | | |
| 29 | | :- use_module(library(lists)). |
| 30 | | :- use_module(library(process)). |
| 31 | | :- use_module(library(file_systems)). |
| 32 | | :- use_module(library(codesio)). |
| 33 | | :- use_module(library(system)). |
| 34 | | :- use_module(library(sockets)). |
| 35 | | |
| 36 | | :- use_module(error_manager,[add_error/2,add_error/3,add_error/4,add_error_fail/3,add_failed_call_error/1, add_internal_error/2, add_warning/3, real_error_occurred/0]). |
| 37 | | :- use_module(self_check). |
| 38 | | :- use_module(preferences). |
| 39 | | :- use_module(tools,[host_platform/1, split_filename/3, get_PROBPATH/1, safe_atom_chars/3, platform_is_64_bit/0, string_concatenate/3]). |
| 40 | | :- use_module(tools_strings,[ajoin_with_sep/3, ajoin/2]). |
| 41 | | :- use_module(tools_printing,[print_error/1]). |
| 42 | | :- use_module(debug). |
| 43 | | :- use_module(bmachine,[b_get_definition/5]). |
| 44 | | :- use_module(specfile, [b_mode/0]). |
| 45 | | |
| 46 | | :- dynamic java_parser_version/1. |
| 47 | | :- dynamic parser_location/1. |
| 48 | | |
| 49 | | % stores the java process of the parser, consisting of ProcessIdentifier, Socket Stream, STDErrStream |
| 50 | | :- dynamic java_parser_process/3. |
| 51 | | :- volatile java_parser_process/3. |
| 52 | | |
| 53 | | |
| 54 | | send_definition(Stream,def(Name,Type,Arity)) :- |
| 55 | | write(Stream,'definition'), nl(Stream), |
| 56 | | format(Stream,'~w\n~w\n~w\n',[Name,Type,Arity]). |
| 57 | | |
| 58 | | send_definitions(ToParser) :- |
| 59 | ? | b_mode, !, |
| 60 | | findall(def(A,B,Ar),(b_get_definition(A,B,C,_,_),length(C,Ar)),L), |
| 61 | | %format('~nSending definitions ~w~n~n',[L]), |
| 62 | | maplist(send_definition(ToParser),L). |
| 63 | | send_definitions(_). |
| 64 | | |
| 65 | | |
| 66 | | crlf(10). |
| 67 | | crlf(13). |
| 68 | | |
| 69 | | % remove newlines in a B formula so that we can pass the formula as a single line to the parser |
| 70 | | cleanup_newlines([],[]). |
| 71 | | cleanup_newlines([H|T],CleanCodes) :- crlf(H),!, cleanup_newlines(T,CleanCodes). |
| 72 | | cleanup_newlines([47,47|T],CleanCodes) :- % a B Comment: skip until end of line |
| 73 | | skip_until_crlf(T,T2), !, |
| 74 | | cleanup_newlines(T2,CleanCodes). |
| 75 | | cleanup_newlines([H|T],[H|R]) :- cleanup_newlines(T,R). |
| 76 | | |
| 77 | | skip_until_crlf([],[]). |
| 78 | | skip_until_crlf([H|T],T) :- crlf(H),!. |
| 79 | | skip_until_crlf([_|T],R) :- skip_until_crlf(T,R). |
| 80 | | |
| 81 | | send_extended_kind(Extended,Kind,In) :- |
| 82 | | (Extended == true |
| 83 | | -> ajoin([extended,Kind],ToParser) |
| 84 | | ; Kind = ToParser), |
| 85 | | write(In,ToParser), nl(In), |
| 86 | | flush_output(In). |
| 87 | | |
| 88 | | :- mode parse_x(+Kind,+Extended,+Codes,-Tree). |
| 89 | | parse_x(Kind,Extended,CodesWithNewlines,Tree) :- |
| 90 | | % Java parser expects only one line of input -> remove newlines |
| 91 | | cleanup_newlines(CodesWithNewlines,Codes), |
| 92 | | % statistics(walltime,[Tot,Delta]), format('~s~n~w~n0 ~w (Delta ~w) ms ~n',[Codes,Kind,Tot,Delta]), |
| 93 | | get_console_parser(Stream,Err), |
| 94 | | send_definitions(Stream), |
| 95 | | send_extended_kind(Extended,Kind,Stream), |
| 96 | | format(Stream,'~s',[Codes]), |
| 97 | | nl(Stream), |
| 98 | | flush_output(Stream), |
| 99 | | read_line(Stream,CodesIn), |
| 100 | | %format('read: ~s~n',[CodesIn]), |
| 101 | | catch( |
| 102 | | (my_read_from_codes(CodesIn,Tree,Stream,Err),handle_parser_exception(Tree)), |
| 103 | | error(_,_), |
| 104 | | (append("Illegal parser result exception: ",CodesIn,ErrMsgCodes), |
| 105 | | atom_codes(ErrMsg,ErrMsgCodes), |
| 106 | | throw(parse_errors([internal_error(ErrMsg,none)])))). |
| 107 | | %statistics(walltime,[Tot4,Delta4]), format('4 ~w (Delta ~w) ms ~n ~n',[Tot4,Delta4]). |
| 108 | | |
| 109 | | |
| 110 | | my_read_from_codes(end_of_file,_,_,Err) :- !, |
| 111 | | read_line_if_ready(Err,Err1Codes), % we just read one line |
| 112 | | safe_name(ErrMsg,Err1Codes), |
| 113 | | add_error(parsercall,'Abnormal termination of parser: ',ErrMsg), |
| 114 | | missing_parser_diagnostics, |
| 115 | | ajoin(['Parser not available (',ErrMsg,')'],FullErrMsg), |
| 116 | | read_lines_and_add_as_error(Err), % add other info on error stream as single error |
| 117 | | throw(parse_errors([error(FullErrMsg,none)])). |
| 118 | | my_read_from_codes(ErrorCodes,_Tree,Out,_) :- |
| 119 | | append("Error",_,ErrorCodes),!, |
| 120 | | atom_codes(ErrMsg,ErrorCodes), |
| 121 | | add_error(parsercall,'Error running/starting parser: ',ErrMsg), |
| 122 | | read_lines_and_add_as_error(Out), |
| 123 | | fail. |
| 124 | | my_read_from_codes(CodesIn,Tree,_,_) :- read_from_codes(CodesIn,Tree). |
| 125 | | |
| 126 | | % a version of my_read_from_codes which has no access to error stream |
| 127 | | my_read_from_codes(end_of_file,_) :- !, |
| 128 | | missing_parser_diagnostics, |
| 129 | | throw(parse_errors([error('Parser not available (end_of_file on input stream)',none)])). |
| 130 | | my_read_from_codes(ErrorCodes,_Tree) :- |
| 131 | | append("Error",_,ErrorCodes),!, |
| 132 | | atom_codes(ErrMsg,ErrorCodes), |
| 133 | | add_error(parsercall,'Error running/starting parser: ',ErrMsg), |
| 134 | | fail. |
| 135 | | my_read_from_codes(CodesIn,Tree) :- read_from_codes(CodesIn,Tree). |
| 136 | | |
| 137 | | missing_parser_diagnostics :- |
| 138 | | parser_location(Classpath), debug_println(9,classpath(Classpath)),fail. |
| 139 | | missing_parser_diagnostics :- runtime_application_path(P), |
| 140 | | atom_concat(P,'/lib/probcliparser.jar',ConParser), |
| 141 | | (file_exists(ConParser) |
| 142 | | -> add_error(parsercall,'The Java B parser (probcliparser.jar) cannot be launched: ',ConParser), |
| 143 | | add_error(parsercall,'Please check that Java and B Parser are available, e.g., using "probcli -check_java_version" command.') |
| 144 | | ; add_internal_error('Java B parser (probcliparser.jar) is missing from lib directory in: ',P) |
| 145 | | ). |
| 146 | | |
| 147 | | % the position reported by the parser is slightly off, |
| 148 | | % because the formula has to be submitted as |
| 149 | | % "#FORMULA ...", "#EXPRESSION ..." or "#PREDICATE ..." |
| 150 | | %handle_parser_exception(E) :- nl,print(E),nl,fail. |
| 151 | | handle_parser_exception(compound_exception(Exs)) :- !, |
| 152 | | maplist(handle_parser_exception_aux,Exs,ExAuxs), |
| 153 | | throw(parse_errors(ExAuxs)). |
| 154 | | handle_parser_exception(Ex) :- |
| 155 | | handle_parser_exception_aux(Ex,ExAux), !, |
| 156 | | throw(parse_errors([ExAux])). |
| 157 | | handle_parser_exception(_). |
| 158 | | |
| 159 | | handle_parser_exception_aux(parse_exception(Pos,Msg),error(SanitizedMsg,Pos)) :- |
| 160 | | remove_msg_posinfo_known(Msg,SanitizedMsg). |
| 161 | | handle_parser_exception_aux(io_exception(Pos,Msg),error(Msg,Pos)). |
| 162 | | handle_parser_exception_aux(io_exception(Msg),error(Msg,unknown)). |
| 163 | | handle_parser_exception_aux(exception(Msg),error(Msg,unknown)). % TO DO: get Pos from Java parser ! |
| 164 | | |
| 165 | | :- mode parse_formula(+Codes,-Tree). |
| 166 | | parse_formula(Codes,Tree) :- |
| 167 | | get_preference(bool_expression_as_predicate,Extended), |
| 168 | | parse_x(formula,Extended,Codes,Tree). |
| 169 | | |
| 170 | | :- mode parse_expression(+Codes,-Tree). |
| 171 | | parse_expression(Codes,Tree) :- |
| 172 | | get_preference(bool_expression_as_predicate,Extended), |
| 173 | | parse_x(expression,Extended,Codes,Tree). |
| 174 | | |
| 175 | | :- mode parse_predicate(+Codes,-Tree). |
| 176 | | parse_predicate(Codes,Tree) :- |
| 177 | | get_preference(bool_expression_as_predicate,Extended), |
| 178 | | parse_x(predicate,Extended,Codes,Tree). |
| 179 | | |
| 180 | | :- mode parse_substitution(+Codes,-Tree). |
| 181 | | parse_substitution(Codes,Tree) :- |
| 182 | | parse_x(substitution,false,Codes,Tree). |
| 183 | | |
| 184 | | :- mode parse(+Kind,+Codes,-Tree). |
| 185 | | parse(formula,Codes,Tree) :- parse_formula(Codes,Tree). |
| 186 | | parse(expression,Codes,Tree) :- parse_expression(Codes,Tree). |
| 187 | | parse(predicate,Codes,Tree) :- parse_predicate(Codes,Tree). |
| 188 | | parse(substitution,Codes,Tree) :- parse_substitution(Codes,Tree). |
| 189 | | |
| 190 | | :- mode parse_temporal_formula(+Kind,+LanguageExtension,+Formula,-Tree). |
| 191 | | parse_temporal_formula(Kind,LanguageExtension,Formula,Tree) :- |
| 192 | | write_to_codes(Formula,CodesWithNewlines), |
| 193 | | % Java parser expects only one line of input -> remove newlines |
| 194 | | cleanup_newlines(CodesWithNewlines,Codes), |
| 195 | | get_console_parser(Stream,Err), |
| 196 | | send_definitions(Stream), |
| 197 | | format(Stream,'~s', [Kind]), nl(Stream), |
| 198 | | format(Stream,'~s', [LanguageExtension]), nl(Stream), |
| 199 | | format(Stream,'~s',[Codes]), nl(Stream), |
| 200 | | flush_output(Stream), |
| 201 | | read_line(Stream,CodesIn), % TODO: Improve feedback from java! |
| 202 | | catch(my_read_from_codes(CodesIn,Tree,Stream,Err),_,throw(parse_errors([error(exception,none)]))). |
| 203 | | |
| 204 | | % throws parse_errors(Errors) in case of syntax errors |
| 205 | | load_b_machine_as_term(Filename, Machine) :- %print(load_b_machine(Filename)),nl, |
| 206 | | prob_filename(Filename, ProBFile), |
| 207 | | debug_println(9,prob_filename(Filename,ProBFile)), |
| 208 | | ( dont_need_compilation(Filename,ProBFile,Machine,LoadResult) -> |
| 209 | | % no compilation is needed |
| 210 | | (LoadResult=loaded -> debug_println(20,'.prob file up-to-date') |
| 211 | | ; print_error('*** Loading failed *** '),nl,fail) |
| 212 | | ; otherwise -> |
| 213 | | debug_println(20,'Calling Parser'), |
| 214 | | (debug:debug_mode(on) -> |
| 215 | | time(call_console_parser(Filename,ProBFile)) |
| 216 | | ; call_console_parser(Filename,ProBFile) |
| 217 | | ), |
| 218 | | load_b_machine_probfile_as_term(ProBFile, Machine) |
| 219 | | ). |
| 220 | | |
| 221 | | % converts the filename of the machine into a filename for the parsed machine |
| 222 | | prob_filename(Filename, ProB) :- |
| 223 | | split_filename(Filename,Basename,_Extension), |
| 224 | | safe_atom_chars(Basename,BasenameC,prob_filename1), |
| 225 | | append(BasenameC,['.','p','r','o','b'],ProBC), |
| 226 | | safe_atom_chars(ProB,ProBC,prob_filename2),!. |
| 227 | | prob_filename(Filename, ProB) :- |
| 228 | | add_failed_call_error(prob_filename(Filename,ProB)),fail. |
| 229 | | |
| 230 | | check_version_and_read_machine(ProBFile, Version, Machine) :- |
| 231 | | (Version='$UNKNOWN' -> print('*** Unknown parser version number. Trying to load parsed file.'),nl |
| 232 | | /* keep CheckVersionNr as variable */ |
| 233 | | ; CheckVersionNr=Version), |
| 234 | | read_machine_term_from_file(ProBFile,parser_version(CheckVersionNr),Machine). |
| 235 | | |
| 236 | | read_machine_term_from_file(ProBFile,VersionTerm,CompleteMachine) :- |
| 237 | | (debug:debug_mode(on) |
| 238 | | -> time(read_machine_term_from_file_aux(ProBFile,VersionTerm,CompleteMachine)) |
| 239 | | ; read_machine_term_from_file_aux(ProBFile,VersionTerm,CompleteMachine)). |
| 240 | | |
| 241 | | read_machine_term_from_file_aux(ProBFile,VersionTerm,complete_machine(MainName,Machines,Files)) :- |
| 242 | | open(ProBFile, read, S), |
| 243 | | call_cleanup(( read(S,VersionTerm), |
| 244 | | %read(S,classical_b(MainName,Files)), read_machines(S,Machines)), |
| 245 | | read_machines(S,Machines,MainName,Files), |
| 246 | | (var(MainName) -> add_internal_error('Missing classical_b fact',ProBFile), MainName=unknown,Files=[] |
| 247 | | ; true) |
| 248 | | ), |
| 249 | | close(S)). |
| 250 | | |
| 251 | | load_b_machine_list_of_facts_as_term(Facts,Machine) :- |
| 252 | | read_machine_term_from_list_of_facts(Facts,_,Machine). |
| 253 | | read_machine_term_from_list_of_facts(Facts,VersionTerm,complete_machine(MainName,Machines,FileList)) :- |
| 254 | | (select(parser_version(VERS),Facts,F2) -> VersionTerm = parser_version(VERS) |
| 255 | | ; add_internal_error('No parser_version available',read_machine_from_list_of_facts), |
| 256 | | F2=Facts, VersionTerm = unknown), |
| 257 | | (select(classical_b(MainName,FileList),F2,F3) -> true |
| 258 | | ; add_internal_error('No classical_b file information available',read_machine_from_list_of_facts), |
| 259 | | fail), |
| 260 | | debug_println(9,loading_classical_b(VersionTerm,MainName,FileList)), |
| 261 | | include(is_machine_term,F3,F4), |
| 262 | | maplist(get_machine_term,F4,Machines). |
| 263 | | |
| 264 | | is_machine_term(machine(_M)). |
| 265 | | get_machine_term(machine(M),M). |
| 266 | | |
| 267 | | load_b_machine_probfile_as_term(ProBFile, Machine) :- |
| 268 | | debug_println(9,consulting(ProBFile)), |
| 269 | | ( read_machine_term_from_file(ProBFile,_VersionTerm,Machine) -> true |
| 270 | | ; otherwise -> |
| 271 | | add_error(parsercall,'Failed to read parser output: wrong format?',ProBFile),fail). |
| 272 | | |
| 273 | | read_machines(S,Machines,MainName,Files) :- |
| 274 | | read(S,Term), |
| 275 | | ( Term == end_of_file -> |
| 276 | | Machines = [] |
| 277 | | ; Term = classical_b(M,F) -> |
| 278 | | ((M,F)=(MainName,Files) -> true ; add_internal_error('Inconsistent classical_b fact: ',classical_b(M,F))), |
| 279 | | read_machines(S,Machines,MainName,Files) |
| 280 | | ; Term = machine(M) -> |
| 281 | | Machines = [M|Mrest], |
| 282 | | read_machines(S,Mrest,MainName,Files) |
| 283 | | ). |
| 284 | | |
| 285 | | % checks if all files that the prob-file depends on |
| 286 | | % are older than the prob-file |
| 287 | | dont_need_compilation(Filename,ProB,Machine,LoadResult) :- |
| 288 | | file_exists(Filename), |
| 289 | | catch( ( get_parser_version(Version), |
| 290 | | file_property(Filename, modify_timestamp, BTime), |
| 291 | | debug_print(19,'Parser Version: '), debug_println(19,Version), |
| 292 | | debug_println(9,' Filename Timestamp: '), debug_print(9,Filename), debug_print(9,' : '),debug_println(9,BTime), |
| 293 | | file_exists(ProB), % the .prob file exists |
| 294 | | file_property(ProB, modify_timestamp, ProbTime), |
| 295 | | debug_println(9,' .prob Timestamp: '), debug_print(9,ProB), debug_print(9,' : '),debug_println(9,ProbTime), |
| 296 | | % print(time_stamps(ProB,ProbTime,Filename,BTime)),nl, |
| 297 | | BTime < ProbTime, % .mch file is older than .prob file |
| 298 | | check_version_and_read_machine(ProB, Version, Machine), |
| 299 | | Machine = complete_machine(_,_,Files), |
| 300 | | % print(checking_all_older(Files,ProbTime)),nl, |
| 301 | | all_older(Files, ProbTime), |
| 302 | | LoadResult = loaded), |
| 303 | | error(A,B), |
| 304 | | (debug_println(9,error(A,B)), |
| 305 | | (A=resource_error(memory) |
| 306 | | -> 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).'), |
| 307 | | LoadResult=A |
| 308 | | ; fail))). |
| 309 | | all_older([],_). |
| 310 | | all_older([File|Rest],PTime) :- % print(checking(File)),nl,trace, |
| 311 | | (file_exists(File) |
| 312 | | -> file_property(File, modify_timestamp, BTime), |
| 313 | | debug_print(9,' Subsidiary File Timestamp: '), debug_print(9,File), debug_print(9,' : '),debug_println(9,BTime), |
| 314 | | ( BTime < PTime -> true |
| 315 | | ; print('File has changed : '), print(File), print(' : '), print(BTime),nl,fail ) |
| 316 | | ; virtual_dsl_file(File) -> debug_format(9,'Virtual file generated by DSL translator: ~w~n',[File]) |
| 317 | | ; debug_format(20,'File does not exist anymore: ~w; calling parser.~n',[File]),fail), |
| 318 | | all_older(Rest,PTime). |
| 319 | | |
| 320 | | virtual_dsl_file(File) :- atom_codes(File,Codes), |
| 321 | | Codes = [95|_], % file name starts with _ underscore |
| 322 | | nonmember(47,Codes), % no slash |
| 323 | | nonmember(92,Codes). % no backslash |
| 324 | | |
| 325 | | :- use_module(system_call). |
| 326 | | |
| 327 | | % use the former LARGE_JVM / use_large_jvm_for_parser by default |
| 328 | | % if we are running on a 64-bit system |
| 329 | | %get_jvm_options(['-Xmx1500m','-Xss5m']) :- platform_is_64_bit, !. % use -Xmx221500000m instead of -Xss5m or Xmx to force exception and test ProB's response |
| 330 | | %get_jvm_options(['-Xmx20m','-Xss1m']) :- !. % comment in to simulate low-memory situations |
| 331 | | get_jvm_options(['-Xss5m']) :- platform_is_64_bit, !. |
| 332 | | get_jvm_options([]). |
| 333 | | |
| 334 | | % ensure that the console Java process is running |
| 335 | | ensure_console_parser_launched :- |
| 336 | | on_exception(E,parse_formula("1",_), |
| 337 | | (add_internal_error('Cannot launch console parser (probcliparser.jar)',E),fail)). |
| 338 | | |
| 339 | | |
| 340 | | get_console_parser(Stream,Err) :- |
| 341 | | java_parser_process(_PID,Stream,Err), |
| 342 | | % calling is_process seams to be unreliable (if the process has crashed) |
| 343 | | % hence, we call process_wait with a timeout of 0 |
| 344 | | % if this does not return an exit value of 'timeout' |
| 345 | | % the process has either been killed or died on its own |
| 346 | | % -- turns out that using process_wait does not work either |
| 347 | | % -- process_wait(PID,timeout,[timeout(0)]), !. |
| 348 | | % now we just check if in and output streams are still available |
| 349 | | \+ at_end_of_stream(Stream), !, |
| 350 | | (at_end_of_stream(Err) |
| 351 | | -> add_error(parsercall,'Java process not running'), |
| 352 | | read_lines_and_add_as_error(Stream) |
| 353 | | ; true). |
| 354 | | get_console_parser(Stream,Err) :- |
| 355 | | clear_old_console_parsers, |
| 356 | | get_java_command(JavaCmd,Classpath), |
| 357 | | % maybe move to a predicate similar to get_jvm_options for Properties |
| 358 | | get_PROBPATH(PROBPATH), |
| 359 | | atom_concat('-Dprob.stdlib=', PROBPATH, Stdlibpref), |
| 360 | | % |
| 361 | | get_jvm_options(XOpts), |
| 362 | | append(XOpts, [Stdlibpref, '-cp',Classpath,'de.prob.cliparser.CliBParser', |
| 363 | | %% '-v', % comment in for verbose |
| 364 | | %% -time for timing info |
| 365 | | %% -fastprolog instead of Prolog |
| 366 | | '-prolog','-lineno','-prepl'], FullOpts), |
| 367 | | debug_println(9,launching_java_console_parser(JavaCmd,FullOpts,probpath(PROBPATH))), |
| 368 | | system_call_keep_open(JavaCmd,FullOpts,PID,_In,Out,Err,[]), % note: if probcliparser.jar does not exist we will not yet get an error here ! |
| 369 | | debug_println(9,java_console_parser_launched(PID)), |
| 370 | | % read first line to get port number |
| 371 | | safe_read_line(Out,Err,1,[],Term), |
| 372 | | socket_client_open('':Term, Stream, [type(text),encoding('UTF-8')]), |
| 373 | | assert(java_parser_process(PID,Stream,Err)), !. |
| 374 | | get_console_parser(_,_) :- missing_parser_diagnostics, fail. |
| 375 | | |
| 376 | | clear_old_console_parsers :- |
| 377 | | retract(java_parser_process(PID,_,_)), |
| 378 | | process_release(PID), |
| 379 | | fail. |
| 380 | | clear_old_console_parsers. |
| 381 | | |
| 382 | | :- use_module(runtime_profiler,[profile_single_call/3]). |
| 383 | | call_console_parser(Filename, ProB) :- |
| 384 | | profile_single_call('$parsing',unknown,parsercall:call_console_parser2(Filename, ProB)). |
| 385 | | call_console_parser2(Filename, ProB) :- |
| 386 | | get_console_parser(Stream,Err), |
| 387 | | |
| 388 | | % path to the .prob file |
| 389 | | replace_windows_path_backslashes(ProB,ProBW), |
| 390 | | % the input file |
| 391 | | replace_windows_path_backslashes(Filename,FilenameW), |
| 392 | | format(Stream,'machine~n~w~n~w~n',[FilenameW,ProBW]), % tell parser to write output to ProBW .prob file |
| 393 | | flush_output(Stream), |
| 394 | | |
| 395 | | safe_read_line(Stream,Err,1,[],Term), |
| 396 | | %print(result(Term)),nl, |
| 397 | | handle_console_parser_result(Term,Err). |
| 398 | | |
| 399 | | safe_read_line(Out,Err,LineNr,SoFar,Term) :- |
| 400 | | safe_read_line_aux(read_line,Out,Err,LineNr,SoFar,Term). |
| 401 | | safe_read_line_if_ready(Out,Err,LineNr,SoFar,Term) :- |
| 402 | | safe_read_line_aux(read_line_if_ready,Out,Err,LineNr,SoFar,Term). |
| 403 | | |
| 404 | | safe_read_line_aux(Pred,Out,Err,LineNr,SoFar,Term) :- |
| 405 | | catch(call(Pred,Out,Codes),Exception, % read another line |
| 406 | | (add_error(parsercall,'Exception while reading next line: ',Exception),throw(Exception))), |
| 407 | | Codes \= end_of_file, !, % happens if parser crashed and stream is closed |
| 408 | | append(SoFar,Codes,NewCodes), |
| 409 | | catch(my_read_from_codes(NewCodes,Term,Out,Err),Exception, |
| 410 | | safe_read_exception(Out,Err,LineNr,Exception,NewCodes,Term)). |
| 411 | | safe_read_line_aux(_Pred,_Out,Err,_LineNr,CodesSoFar,_) :- |
| 412 | | safe_name(T,CodesSoFar), |
| 413 | | add_error(parsercall,'Unexpected error while parsing machine: ',T), |
| 414 | | read_lines_and_add_as_error(Err),fail. |
| 415 | | |
| 416 | | |
| 417 | | safe_read_exception(Out,_,1,_Exception,CodesSoFar,_Term) :- append("Error",_,CodesSoFar),!, |
| 418 | | % probably some Java error, we do not obtain a correct Prolog term, but probably something like: |
| 419 | | % "Error occurred during initialization of VM" |
| 420 | | safe_name(T,CodesSoFar), |
| 421 | | add_error(parsercall,'Java error while parsing machine: ',T), |
| 422 | | read_lines_and_add_as_error(Out),fail. |
| 423 | | 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 |
| 424 | | !, |
| 425 | | %(debug:debug_mode(off) -> true ; format('Syntax error in parser result (line ~w): ~w~nTrying to read another line.~n',[LineNr,M])), |
| 426 | | add_warning(parsercall,'Syntax error in parser result; trying to read another line. Line:Error = ',LineNr:M), |
| 427 | | L1 is LineNr+1, |
| 428 | | 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) |
| 429 | | safe_read_exception(_,_,_LineNr,parse_errors(Errors),_CodesSoFar,_Term) :- !, |
| 430 | | debug_println(4,read_parse_errors(Errors)), |
| 431 | | throw(parse_errors(Errors)). |
| 432 | | safe_read_exception(_,_,_LineNr,Exception,_CodesSoFar,_Term) :- |
| 433 | | add_internal_error('Unexpected exception occurred during parsing: ',Exception),fail. |
| 434 | | %safe_name(T,CodesSoFar), add_error_fail(parsercall,'Unexpected error while parsing machine: ',T). |
| 435 | | |
| 436 | | safe_name(Name,Codes) :- var(Name),Codes == end_of_file,!, |
| 437 | | %add_internal_error('Parser does not seem to be available',''), |
| 438 | | Name=end_of_file. |
| 439 | | safe_name(Name,Codes) :- number(Name),!, |
| 440 | | safe_number_codes(Name,Codes). |
| 441 | | safe_name(Name,Codes) :- |
| 442 | | on_exception(E,atom_codes(Name,Codes), |
| 443 | | (print('Exception during atom_codes: '),print(E),nl,nl,throw(E))). |
| 444 | | |
| 445 | | safe_number_codes(Name,Codes) :- |
| 446 | | on_exception(E,number_codes(Name,Codes), |
| 447 | | (print('Exception during number_codes: '),print(E),nl,nl,throw(E))). |
| 448 | | |
| 449 | | % see also handle_parser_exception |
| 450 | | %handle_console_parser_result(E,_) :- nl,print(E),nl,fail. |
| 451 | | handle_console_parser_result(exit(0),_) :- !. |
| 452 | | handle_console_parser_result(io_exception(Msg),_) :- !, |
| 453 | | add_error_fail(parsercall,'Error while opening the B file: ',Msg). |
| 454 | | handle_console_parser_result(preparse_exception(Tokens,Msg),_) :- !, |
| 455 | | remove_msg_posinfo(Msg,SanitizedMsg,MsgPos), |
| 456 | | findall(error(SanitizedMsg,Pos),member(Pos,Tokens),Errors1), |
| 457 | | (Errors1 = [] |
| 458 | | -> /* if there are no error tokens: use pos. info from text Msg */ |
| 459 | | Errors = [error(SanitizedMsg,MsgPos)] |
| 460 | | ; Errors = Errors1), |
| 461 | | debug_println(4,preparse_exception_parse_errors(Tokens,Msg,Errors)), |
| 462 | | throw(parse_errors(Errors)). |
| 463 | | handle_console_parser_result(parse_exception(Pos,Msg),_) :- !, |
| 464 | | remove_msg_posinfo_known(Msg,SanitizedMsg), %print(sanitized(SanitizedMsg)),nl, |
| 465 | | debug_println(4,parse_exception(Pos,Msg,SanitizedMsg)), |
| 466 | | throw(parse_errors([error(SanitizedMsg,Pos)])). |
| 467 | | handle_console_parser_result(exception(Msg),_) :- !, |
| 468 | | %add_error(bmachine,'Error in the classical B parser: ', Msg), |
| 469 | | remove_msg_posinfo(Msg,SanitizedMsg,Pos), |
| 470 | | debug_println(4,exception_in_parser(Msg,SanitizedMsg,Pos)), |
| 471 | | throw(parse_errors([error(SanitizedMsg,Pos)])). |
| 472 | | handle_console_parser_result(end_of_file,Err) :- !, |
| 473 | | % probably NullPointerException or similar in parser; no result on StdOut |
| 474 | | debug_println(9,end_of_file_on_parser_output_stream), |
| 475 | | format(user_error,'Detected abnormal termination of B Parser~n',[]), % print in case we block |
| 476 | | read_line_if_ready(Err,Err1), |
| 477 | | (Err1=end_of_file -> Msg = 'Abnormal termination of B Parser: EOF on streams' |
| 478 | | ; append("Abnormal termination of B Parser: ",Err1,ErrMsgCodes), |
| 479 | | safe_name(Msg,ErrMsgCodes), |
| 480 | | read_lines_and_add_as_error(Err) % also show additional error infos |
| 481 | | ), |
| 482 | | throw(parse_errors([error(Msg,none)])). |
| 483 | | handle_console_parser_result(compound_exception(Exs),_) :- !, |
| 484 | | maplist(handle_parser_exception_aux,Exs,ExAuxs), |
| 485 | | debug_println(4,compound_exception(Exs,ExAuxs)), |
| 486 | | throw(parse_errors(ExAuxs)). |
| 487 | | handle_console_parser_result(Term,_) :- !, |
| 488 | | write_term_to_codes(Term,Text,[]), |
| 489 | | safe_name(Msg,Text), |
| 490 | | %add_error(bmachine,'Error in the classical B parser: ', Msg), |
| 491 | | remove_msg_posinfo(Msg,SanitizedMsg,Pos), |
| 492 | | debug_println(4,unknown_error_term(Term,SanitizedMsg,Pos)), |
| 493 | | throw(parse_errors([error(SanitizedMsg,Pos)])). |
| 494 | | |
| 495 | | % now replaced by remove_msg_posinfo: |
| 496 | | %extract_position_info(Text,pos(Row,Col,Filename)) :- |
| 497 | | % atom_codes(Text,Codes), |
| 498 | | % epi(Row,Col,Filename,Codes,_),!. |
| 499 | | %extract_position_info(_Text,none). |
| 500 | | |
| 501 | | :- assert_must_succeed((parsercall:epi(R,C,F,"[2,3] xxx in file: /usr/lib.c",[]), R==2,C==3,F=='/usr/lib.c')). |
| 502 | | :- assert_must_succeed((parsercall:epi(R,C,F,"[22,33] xxx yyy ",_), R==22,C==33,F=='unknown')). |
| 503 | | |
| 504 | | % we expect error messages to start with [Line,Col] information |
| 505 | | epi(Row,Col,Filename) --> " ",!,epi(Row,Col,Filename). |
| 506 | | epi(Row,Col,Filename) --> "[", epi_number(Row),",",epi_number(Col),"]", |
| 507 | | (epi_filename(Filename) -> [] ; {Filename=unknown}). |
| 508 | | epi_number(N) --> epi_numbers(Chars),{safe_number_codes(N,Chars)}. |
| 509 | | epi_numbers([C|Rest]) --> [C],{is_number(C)},epi_numbers2(Rest). |
| 510 | | epi_numbers2([C|Rest]) --> [C],{is_number(C),!},epi_numbers2(Rest). |
| 511 | | epi_numbers2("") --> !. |
| 512 | ? | is_number(C) :- member(C,"0123456789"),!. |
| 513 | | epi_filename(F) --> " in file: ",!,epi_path2(Chars),{safe_name(F,Chars)}. |
| 514 | | epi_filename(F) --> [_], epi_filename(F). |
| 515 | | epi_path2([C|Rest]) --> [C],!,epi_path2(Rest). % assume everything until the end is a filename |
| 516 | | epi_path2([]) --> []. |
| 517 | | |
| 518 | | :- assert_must_succeed((parsercall:remove_rowcol(R,C,"[22,33] xxx yyy ",_), R==22,C==33)). |
| 519 | | % remove parser location info from message to avoid user clutter |
| 520 | | remove_rowcol(Row,Col) --> " ",!, remove_rowcol(Row,Col). |
| 521 | | remove_rowcol(Row,Col) --> "[", epi_number(Row),",",epi_number(Col),"]". |
| 522 | | |
| 523 | | :- assert_must_succeed((parsercall:remove_filename(F,C,"xxx yyy in file: a.out",R), F == 'a.out', C == "xxx yyy", R==[])). |
| 524 | | remove_filename(F,[]) --> " in file: ",!,epi_path2(Chars),{safe_name(F,Chars)}. |
| 525 | | remove_filename(F,[C|T]) --> [C], remove_filename(F,T). |
| 526 | | |
| 527 | | :- assert_must_succeed((parsercall:remove_filename_from_codes("xxx yyy in file: a.out",F,C), F == 'a.out', C == "xxx yyy")). |
| 528 | | :- assert_must_succeed((parsercall:remove_filename_from_codes("xxx yyy zzz",F,C), F == 'unknown', C == "xxx yyy zzz")). |
| 529 | | remove_filename_from_codes(Codes,F,NewCodes) :- |
| 530 | | (remove_filename(F,C1,Codes,C2) -> append(C1,C2,NewCodes) ; F=unknown, NewCodes=Codes). |
| 531 | | |
| 532 | | % obtain position information from a message atom and remove the parts from the message at the same time |
| 533 | | remove_msg_posinfo_known(Msg,NewMsg) :- remove_msg_posinfo(Msg,NewMsg,_,pos_already_known). |
| 534 | | remove_msg_posinfo(Msg,NewMsg,Pos) :- remove_msg_posinfo(Msg,NewMsg,Pos,not_known). |
| 535 | | remove_msg_posinfo(Msg,NewMsg,Pos,AlreadyKnown) :- %print(msg(Msg,AlreadyKnown)),nl, |
| 536 | | atom_codes(Msg,Codes), |
| 537 | | (remove_rowcol(Row,Col,Codes,RestCodes) |
| 538 | | -> Pos=pos(Row,Col,Filename), |
| 539 | | remove_filename_from_codes(RestCodes,Filename,NewCodes) |
| 540 | | ; AlreadyKnown==pos_already_known -> |
| 541 | | Pos = none, |
| 542 | | remove_filename_from_codes(Codes,_Filename2,NewCodes) |
| 543 | | ; otherwise -> |
| 544 | | NewCodes=Codes, Pos=none |
| 545 | | % do not remove filename: we have not found a position and cannot return the filename |
| 546 | | % see, e.g., public_examples/B/Tickets/Hansen27_NestedMchErr/M1.mch |
| 547 | | ), |
| 548 | | !, |
| 549 | | atom_codes(NewMsg,NewCodes). |
| 550 | | remove_msg_posinfo(M,M,none,_). |
| 551 | | |
| 552 | | |
| 553 | | % ---------------------- |
| 554 | | |
| 555 | | get_parser_version(Version) :- java_parser_version(Version),!. |
| 556 | | get_parser_version(Version) :- |
| 557 | | get_version_from_parser(Version), |
| 558 | | assert(java_parser_version(Version)), |
| 559 | | !. |
| 560 | | get_parser_version(_Vers) :- |
| 561 | | (real_error_occurred -> true % already produced error messages in get_version_from_parser |
| 562 | | ; add_error(get_parser_version,'Could not get parser version.')), |
| 563 | | %missing_parser_diagnostics, % already called if necessary by get_version_from_parser |
| 564 | | fail. |
| 565 | | |
| 566 | | |
| 567 | | get_version_from_parser(Version) :- |
| 568 | | get_console_parser(Stream,Err), |
| 569 | | write(Stream,'version'), nl(Stream), |
| 570 | | flush_output(Stream), |
| 571 | | read_line(Stream,Text), % if parser cannot be started we receive end_of_file; length will fail |
| 572 | | (Text = end_of_file -> add_error(parsercall,'Could not get parser version: '), |
| 573 | | read_lines_and_add_as_error(Err),fail |
| 574 | | ; length(Text,Length), |
| 575 | | ( append("Error",_,Text) |
| 576 | | -> atom_codes(ErrMsg,Text), |
| 577 | | add_error(parsercall,'Error getting parser version: ',ErrMsg), |
| 578 | | read_lines_and_add_as_error(Stream),fail |
| 579 | | ; Length < 100 -> atom_codes(Version,Text) |
| 580 | | ; otherwise -> prefix_length(Text,Prefix,100), |
| 581 | | append(Prefix,"...",Full), |
| 582 | | safe_name(Msg,Full), |
| 583 | | add_error_fail(parsercall, 'B parser returned unexpected version string: ', Msg)) |
| 584 | | ). |
| 585 | | |
| 586 | | :- use_module(library(sockets),[socket_select/7]). |
| 587 | | % check if a stream is ready for reading |
| 588 | | stream_ready_to_read(Out) :- var(Out),!, |
| 589 | | add_internal_error('Illegal stream: ',stream_ready_to_read(Out)),fail. |
| 590 | | stream_ready_to_read(Out) :- |
| 591 | | socket_select([],_, [Out],RReady, [],_, 1), % wait 1 sec at most %print(ready(Out,RReady)),nl, |
| 592 | | RReady == [Out]. |
| 593 | | |
| 594 | | |
| 595 | | read_lines_and_add_as_error(Out) :- read_lines_until_eof(Out,false,ErrMsgCodes,[]), |
| 596 | | (ErrMsgCodes=[] -> true |
| 597 | | ; ErrMsgCodes=[10] -> true % just a single newline |
| 598 | | ; ErrMsgCodes=[13] -> true % ditto |
| 599 | | ; safe_name(ErrMsg,ErrMsgCodes), |
| 600 | | add_error(parsercall,'Additional information: ',ErrMsg)). |
| 601 | | |
| 602 | | read_line_if_ready(Stream,Line) :- stream_ready_to_read(Stream), !, read_line(Stream,Line). |
| 603 | | read_line_if_ready(_,end_of_file). % pretend we are at the eof |
| 604 | | |
| 605 | | read_lines_until_eof(Out,NewlineRequired) --> {read_line_if_ready(Out,Text)}, |
| 606 | | !, |
| 607 | | ({Text = end_of_file} -> [] |
| 608 | | ; ({NewlineRequired==true} -> "\n" ; []), |
| 609 | | Text, %{format("read: ~s~n",[Text])}, |
| 610 | | read_lines_until_eof(Out,true)). |
| 611 | | read_lines_until_eof(_Out,_) --> []. |
| 612 | | |
| 613 | | get_java_command(JavaCmdW,ClasspathW) :- |
| 614 | | FileList = ['probcliparser.jar'], |
| 615 | | (parser_location(Classpath) -> true |
| 616 | | ; otherwise -> libraries_as_classpath(FileList,Classpath)), |
| 617 | | get_java_command_path(JavaCmdW), |
| 618 | | replace_windows_path_backslashes(Classpath,ClasspathW). |
| 619 | | |
| 620 | | |
| 621 | | % a predicate to check whether we have correct java version number and whether java seems to work ok |
| 622 | | % ResultStatus=compatible if everything is ok |
| 623 | | check_java_version(VersionCheckResult,ResultStatus) :- get_java_fullversion(Version),!, |
| 624 | | check_java_version_aux(Version,VersionCheckResult,ResultStatus). |
| 625 | | check_java_version(VersionCheckResult,error) :- get_java_command(JavaCmdW,ClasspathW),!, |
| 626 | | ajoin(['*** Unable to launch java command: ',JavaCmdW,' (classpath: ',ClasspathW,')!'],VersionCheckResult). |
| 627 | | check_java_version('*** Unable to launch Java or get path to java command!',error). % should not happen |
| 628 | | |
| 629 | | check_java_version_aux(VersionCodes,VersionCheckResult,ResultStatus) :- |
| 630 | | get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom),!, |
| 631 | | check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,ResultStatus). |
| 632 | | check_java_version_aux(VersionCodes,VersionCheckResult,error) :- |
| 633 | | atom_codes(VersionA,VersionCodes), |
| 634 | | ajoin(['*** Unable to identify Java version number: ',VersionA, ' !'],VersionCheckResult). |
| 635 | | |
| 636 | | check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,compatible) :- java_version_ok_for_parser(V1,V2,V3Atom), |
| 637 | | get_java_version(_),!, % if get_java_version fails, this is an indication that Java not fully installed with admin rights |
| 638 | | ajoin(['Java is correctly installed and version ',V1,'.',V2,'.',V3Atom, |
| 639 | | ' is compatible with ProB requirements (>= 1.7).'],VersionCheckResult). |
| 640 | | check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,error) :- java_version_ok_for_parser(V1,V2,V3Atom),!, |
| 641 | | ajoin(['*** Java version ',V1,'.',V2,'.',V3Atom, |
| 642 | | ' is compatible with ProB requirements (>= 1.7) ', |
| 643 | | 'but does not seem to be correctly installed: reinstall Java with admin rights!'],VersionCheckResult). |
| 644 | | check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,incompatible) :- |
| 645 | | get_java_version(_),!, |
| 646 | | ajoin(['*** Java is correctly installed but version ',V1,'.',V2,'.',V3Atom, |
| 647 | | ' is *not* compatible with ProB requirements (>= 1.7)!'],VersionCheckResult). |
| 648 | | check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,error) :- |
| 649 | | ajoin(['*** Java is not correctly installed and version ',V1,'.',V2,'.',V3Atom, |
| 650 | | ' is *not* compatible with ProB requirements (>= 1.7)!'],VersionCheckResult). |
| 651 | | |
| 652 | | |
| 653 | | % we need Java 1.7 or higher |
| 654 | | java_version_ok_for_parser(V1,_V2,_) :- V1>1. |
| 655 | | java_version_ok_for_parser(1,V2,_) :- V2>=7. |
| 656 | | |
| 657 | | get_java_fullversion(V1,V2,V3Atom) :- get_java_fullversion(VersionCodes), |
| 658 | | get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom). |
| 659 | | |
| 660 | | :- use_module(tools,[split_chars/3]). |
| 661 | | get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom) :- |
| 662 | | append("java full version """,Tail,VersionCodes), |
| 663 | | get_java_fullversion_numbers_aux(Tail,V1,V2,V3Atom). |
| 664 | | get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom) :- |
| 665 | | append("openjdk full version """,Tail,VersionCodes), |
| 666 | | get_java_fullversion_numbers_aux(Tail,V1,V2,V3Atom). |
| 667 | | get_java_fullversion_numbers_aux(Tail,V1,V2,V3Atom) :- |
| 668 | | split_chars(Tail,".",[V1C,V2C|FurtherC]), |
| 669 | | append(FurtherC,V3C), |
| 670 | | number_codes(V1,V1C), number_codes(V2,V2C), |
| 671 | | (append(V3C2,[_,_],V3C) % try remove trailing " and newline |
| 672 | | -> atom_codes(V3Atom,V3C2) ; atom_codes(V3Atom,V3C)). |
| 673 | | |
| 674 | | % get java fullversion as code list; format "java full version "...."\n" |
| 675 | | get_java_fullversion(Version) :- |
| 676 | | get_java_command_path(JavaCmdW), |
| 677 | | (my_system_call(JavaCmdW, ['-fullversion'],java_version,Text) -> Text=Version |
| 678 | | ; format(user_error,'Could not execute ~w -fullversion~n',[JavaCmdW]), |
| 679 | | fail). |
| 680 | | |
| 681 | | % when java -fullversion works but not java -version it seems that Java was improperly |
| 682 | | % installed without admin rights (http://stackoverflow.com/questions/11808829/jre-1-7-returns-java-lang-noclassdeffounderror-java-lang-object) |
| 683 | | get_java_version(Version) :- |
| 684 | | get_java_command_path(JavaCmdW), |
| 685 | | (my_system_call(JavaCmdW, ['-version'],java_version,Text) -> Text=Version |
| 686 | | ; format(user_error,'Could not execute ~w -version~n',[JavaCmdW]), |
| 687 | | fail). |
| 688 | | % should we check for JAVA_PATH first ? would allow user to override java; but default pref would have to be set to '' |
| 689 | | get_java_command_path(JavaCmdW) :- |
| 690 | | %host_platform(darwin) |
| 691 | | get_preference(path_to_java,X), debug_println(8,path_to_java_preference(X)), |
| 692 | | (X='' |
| 693 | | ; preference_default_value(path_to_java,Default), debug_println(8,default(Default)), |
| 694 | | Default=X |
| 695 | | ), |
| 696 | | % only try this when the Java path has not been set explicitly |
| 697 | | % on Mac: /usr/bin/java exists even when Java not installed ! it is a fake java command that launches a dialog |
| 698 | ? | absolute_file_name(path(java), |
| 699 | | JavaCmd, |
| 700 | | [access(exist),extensions(['.exe','']),solutions(all),file_errors(fail)]), |
| 701 | | debug_println(8,obtained_java_cmd_from_path(JavaCmd)), |
| 702 | | replace_windows_path_backslashes(JavaCmd,JavaCmdW), |
| 703 | | !. |
| 704 | | get_java_command_path(JavaCmdW) :- get_preference(path_to_java,JavaCmd), |
| 705 | | JavaCmd \= '', |
| 706 | | debug_println(8,using_path_to_java_preference(JavaCmd)), |
| 707 | | (file_exists(JavaCmd) -> true |
| 708 | | ; 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) |
| 709 | | ; add_warning(get_java_command_path,'No Java Runtime (7 or newer) found; please correct the JAVA_PATH advanced preference: ',JavaCmd)), |
| 710 | | replace_windows_path_backslashes(JavaCmd,JavaCmdW), |
| 711 | | !. |
| 712 | | get_java_command_path(_JavaCmd) :- |
| 713 | | add_error(get_java_command_path,'Could not get path to the java tool. Make sure a Java Runtime (7 or newer) is installed',''), |
| 714 | | fail. |
| 715 | | |
| 716 | | libraries_as_classpath(Libs,Classpath) :- |
| 717 | | %findall(PLD,user:file_search_path(prob_lib,PLD),LL2), print(prob_lib_directory(LL2)),nl, |
| 718 | | maplist(library_abs_name,Libs,ALibs), |
| 719 | | ( host_platform(windows) -> Sep = (';') |
| 720 | | ; otherwise -> Sep = (':')), |
| 721 | | ajoin_with_sep(ALibs,Sep,Classpath). |
| 722 | | library_abs_name(Lib,Abs) :- absolute_file_name(prob_lib(Lib),Abs). |
| 723 | | |
| 724 | | |
| 725 | | call_ltl_parser(Formulas, CtlOrLtl, Result) :- |
| 726 | | get_ltl_lang_spec(LangSpec), |
| 727 | | maplist(parse_temporal_formula(CtlOrLtl,LangSpec),Formulas,Result). |
| 728 | | |
| 729 | | :- use_module(specfile,[b_or_z_mode/0,csp_with_bz_mode/0]). |
| 730 | | get_ltl_lang_spec('B,none') :- csp_with_bz_mode,!. |
| 731 | | get_ltl_lang_spec('B') :- b_or_z_mode,!. |
| 732 | | get_ltl_lang_spec(none). |
| 733 | | |
| 734 | | /* unused code : |
| 735 | | generate_formula_codes([F]) --> |
| 736 | | !,generate_formula_codes2(F),"\n". |
| 737 | | generate_formula_codes([F|Rest]) --> |
| 738 | | generate_formula_codes2(F), "###\n", |
| 739 | | generate_formula_codes(Rest). |
| 740 | | generate_formula_codes2(F) --> |
| 741 | | write_to_codes(F). |
| 742 | | */ |
| 743 | | |
| 744 | | |
| 745 | | % --------------------------- |
| 746 | | |
| 747 | | % call the TLA2B parser to translate a TLA file into a B machine |
| 748 | | call_tla2b_parser(TLAFile) :- |
| 749 | | get_java_command_path(JavaCmdW), |
| 750 | | replace_windows_path_backslashes(TLAFile,TLAFileW), |
| 751 | | get_jvm_options(XOpts), |
| 752 | | absolute_file_name(prob_lib('TLA2B.jar'),TLA2BJAR), |
| 753 | | append(XOpts,['-jar',file(TLA2BJAR),file(TLAFileW)],FullOpts), |
| 754 | | debug_println(9,calling_java(FullOpts)), |
| 755 | | (my_system_call(JavaCmdW, FullOpts,tla2b_parser) -> true |
| 756 | | ; print_error('Be sure to download TLA2B.zip from http://nightly.cobra.cs.uni-duesseldorf.de/tla,'), |
| 757 | | print_error('then unzip the archive and put TLA2B.jar into the ProB lib/ directory.'), |
| 758 | | fail). |
| 759 | | |
| 760 | | %call_cspmj_parser(CSPFile,PrologFile) :- |
| 761 | | % get_java_command_path(JavaCmdW), |
| 762 | | % replace_windows_path_backslashes(CSPFile,CSPFileW), |
| 763 | | % get_jvm_options(XOpts), |
| 764 | | % absolute_file_name(prob_lib('cspmj.jar'),CSPMJAR), |
| 765 | | % get_writable_compiled_filename(CSPFile,'.pl',PrologFile), |
| 766 | | % string_concatenate('--prologOut=', PrologFile, PrologFileOutArg), |
| 767 | | % append(XOpts,['-jar',CSPMJAR,'-parse',CSPFileW,PrologFileOutArg],FullOpts), |
| 768 | | % debug_println(9,calling_java(FullOpts)), |
| 769 | | % (my_system_call(JavaCmdW, FullOpts,cspmj_parser) -> true |
| 770 | | % ; print_error('Be sure that cspmj.jar parser is installed.'), |
| 771 | | % fail). |
| 772 | | |
| 773 | | |
| 774 | | tla2prob_filename(TLAFile,GeneratedProbFile) :- |
| 775 | | split_filename(TLAFile,Basename,_Extension), |
| 776 | | atom_chars(Basename,BasenameC), |
| 777 | | append(BasenameC,['.','p','r','o','b'],TLABC), |
| 778 | | atom_chars(GeneratedProbFile,TLABC),!. |
| 779 | | tla2prob_filename(Filename, GeneratedProbFile) :- |
| 780 | | add_failed_call_error(tla2b_filename(Filename,GeneratedProbFile)),fail. |
| 781 | | |
| 782 | | tla2b_filename(TLAFile,BFile) :- |
| 783 | | split_filename(TLAFile,Basename,_Extension), |
| 784 | | atom_chars(Basename,BasenameC), |
| 785 | | append(BasenameC,['_',t,l,a,'.','m','c','h'],TLABC), |
| 786 | | atom_chars(BFile,TLABC),!. |
| 787 | | tla2b_filename(Filename, BFile) :- |
| 788 | | add_failed_call_error(tla2b_filename(Filename,BFile)),fail. |
| 789 | | |
| 790 | | |
| 791 | | my_system_call(Command,Options,Origin) :- my_system_call(Command,Options,Origin,_Text). |
| 792 | | my_system_call(Command,Options,Origin,ErrText) :- |
| 793 | | system_call(Command,Options,ErrText,Exit), %nl,print(exit(Exit)),nl,nl, |
| 794 | | treat_exit_code(Exit,Command,Options,ErrText,Origin). |
| 795 | | |
| 796 | | my_system_call5(Command,Options,Origin,OutputText,ErrText) :- |
| 797 | | system_call(Command,Options,OutputText,ErrText,Exit), %nl,print(exit(Exit)),nl,nl, |
| 798 | | treat_exit_code(Exit,Command,Options,ErrText,Origin). |
| 799 | | |
| 800 | | treat_exit_code(exit(0),_,_,_,_) :- !. |
| 801 | | treat_exit_code(Exit,Command,Options,ErrText,Origin) :- |
| 802 | | debug_println(9,treat_exit_code(Exit,Command,Options,ErrText,Origin)), |
| 803 | | catch( my_read_from_codes(ErrText,Term), |
| 804 | | _, |
| 805 | | (safe_name(T,ErrText),Term = T)), !, |
| 806 | | %print_error(Term), |
| 807 | | (Term = end_of_file -> ErrMsg = '' ; ErrMsg = Term), |
| 808 | | tools:ajoin(['Exit code ',Exit,' for command ',Command, ', error message: '],Msg), |
| 809 | | (get_error_position_from_term(Origin,Term,Pos) |
| 810 | | -> add_error(Origin,Msg,ErrMsg,Pos) |
| 811 | | ; add_error(Origin,Msg,ErrMsg) |
| 812 | | ), |
| 813 | | fail. |
| 814 | | |
| 815 | | |
| 816 | | get_error_position_from_term(alloy2b,Term,Pos) :- atom(Term), |
| 817 | | atom_codes(Term,Codes), get_error_position_from_codes(Codes,Pos). |
| 818 | | |
| 819 | | % Alloy error message: ! Exception in thread "main" Type error in .../Restrictions.als at line 41 column 23: |
| 820 | | get_error_position_from_codes([97,116,32,108,105,110,101,32|Tail],lineCol(Line,Col)) :- % "at line " |
| 821 | | epi_number(Line,Tail,RestTail), |
| 822 | | (RestTail = [32,99,111,108,117,109,110,32|Tail2], % "column " |
| 823 | | epi_number(Col,Tail2,_) -> true |
| 824 | | ; Col=0). |
| 825 | | get_error_position_from_codes([_|T],Pos) :- get_error_position_from_codes(T,Pos). |
| 826 | | |
| 827 | | % replace backslashes by forward slashes in atoms, only under windows |
| 828 | | % TODO(DP,14.8.2008): Check if still needed with SICStus 4.0.4 and if |
| 829 | | % everybody uses that version |
| 830 | | replace_windows_path_backslashes(Old,New) :- |
| 831 | | ( host_platform(windows) -> |
| 832 | | safe_name(Old,OldStr), |
| 833 | | replace_string_backslashes(OldStr,NewStr), |
| 834 | | safe_name(New,NewStr) |
| 835 | | ; otherwise -> |
| 836 | | Old=New). |
| 837 | | |
| 838 | | replace_string_backslashes([],[]) :- !. |
| 839 | | replace_string_backslashes([C|OldRest],[N|NewRest]) :- !, |
| 840 | | ( C=92 /* backslash */ -> |
| 841 | | N=47 /* forward slash */ |
| 842 | | ; otherwise -> |
| 843 | | N=C ), |
| 844 | | replace_string_backslashes(OldRest,NewRest). |
| 845 | | replace_string_backslashes(X,Y) :- |
| 846 | | add_error(parsercall,'Illegal call: ',replace_string_backslashes(X,Y)), |
| 847 | | fail. |
| 848 | | |
| 849 | | % --------------------------- |
| 850 | | :- use_module(pathes,[runtime_application_path/1]). |
| 851 | | |
| 852 | | call_jar_parser(PMLFile,JARFile,Options,ParserName) :- |
| 853 | | get_java_command_path(JavaCmdW), |
| 854 | | replace_windows_path_backslashes(PMLFile,PMLFileW), |
| 855 | | get_jvm_options(XOpts), |
| 856 | | absolute_file_name(prob_lib(JARFile),FullJAR), |
| 857 | | append(XOpts,['-jar',FullJAR,PMLFileW|Options],FullOpts), |
| 858 | | debug_println(9,calling_java(FullOpts)), |
| 859 | | my_system_call(JavaCmdW, FullOpts,ParserName). |
| 860 | | |
| 861 | | |
| 862 | | |
| 863 | | call_alloy2pl_parser(AlloyFile,BFile) :- |
| 864 | | alloy_pl_filename(AlloyFile,BFile), |
| 865 | | call_alloy2pl_parser_aux(AlloyFile,'alloy2b-1.0-SNAPSHOT.jar',BFile). |
| 866 | | |
| 867 | | call_alloy2pl_parser_aux(AlloyFile,JARFile,BFile) :- |
| 868 | | compilation_not_needed(AlloyFile,BFile,JARFile),!. |
| 869 | | call_alloy2pl_parser_aux(AlloyFile,JARFile,BFile) :- |
| 870 | | (file_exists(BFile) -> delete_file(BFile) ; true), % TODO: only delete generated files |
| 871 | | replace_windows_path_backslashes(BFile,BFileW), |
| 872 | | call_jar_parser(AlloyFile,JARFile,['-toProlog',BFileW],alloy2b). |
| 873 | | |
| 874 | | alloy_pl_filename(AlloyFile,BFile) :- atom_codes(AlloyFile,BasenameC), |
| 875 | | append(BasenameC,".pl",NewC), |
| 876 | | atom_codes(BFile,NewC),!. |
| 877 | | alloy_pl_filename(Filename, BFile) :- |
| 878 | | add_failed_call_error(alloy_b_filename(Filename,BFile)),fail. |
| 879 | | |
| 880 | | compilation_not_needed(BaseFile,DerivedFile,LibraryFile) :- |
| 881 | | file_exists(BaseFile), |
| 882 | | file_property(BaseFile, modify_timestamp, BTime), |
| 883 | | %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]), |
| 884 | | file_exists(DerivedFile), |
| 885 | | file_property(DerivedFile, modify_timestamp, DTime), |
| 886 | | DTime > BTime, |
| 887 | | absolute_file_name(prob_lib(LibraryFile),FullLibFile), |
| 888 | | (file_exists(FullLibFile) |
| 889 | | -> file_property(FullLibFile, modify_timestamp, LibTime), |
| 890 | | DTime > LibTime % check that file was generated by this library (hopefully); ideally we should put version numbers into the DerivedFiles |
| 891 | | ; true % Jar/command not available anyway; use the derived file |
| 892 | | ). |
| 893 | | |
| 894 | | % --------------------------- |
| 895 | | |
| 896 | | call_fuzz_parser(TexFile,FuzzFile) :- |
| 897 | | get_command_in_lib(fuzz,FuzzCmd), |
| 898 | | absolute_file_name(prob_lib('fuzzlib'),FUZZLIB), % TO DO: windows |
| 899 | | fuzz_filename(TexFile,FuzzFile), |
| 900 | | % fuzz options: |
| 901 | | % -d Allow use before definition |
| 902 | | % -l Lisp-style echoing of input |
| 903 | | % -p file Use <file> in place of standard prelude |
| 904 | | debug_format(19,'Fuzz: running ~w -d -l with library ~w on ~w~n',[FuzzCmd,FUZZLIB,TexFile]), |
| 905 | | (file_exists(FUZZLIB) |
| 906 | | -> my_system_call5(FuzzCmd,['-d', '-l', '-p', file(FUZZLIB), file(TexFile)],call_fuzz_parser,Text,_ErrText) |
| 907 | | ; my_system_call5(FuzzCmd,['-d', '-l', file(TexFile)],call_fuzz_parser,Text,_ErrText) |
| 908 | | ), |
| 909 | | format('Writing fuzz AST to ~s~n',[FuzzFile]), |
| 910 | | open(FuzzFile,write,Stream), |
| 911 | | call_cleanup(format(Stream,'~s~n',[Text]), close(Stream)). |
| 912 | | |
| 913 | | get_command_in_lib(Name,Command) :- |
| 914 | | get_binary_extensions(Extensions), |
| 915 | | absolute_file_name(prob_lib(Name), |
| 916 | | Command, |
| 917 | | [access(exist),extensions(Extensions),solutions(all),file_errors(fail)]). |
| 918 | | |
| 919 | | get_binary_extensions(List) :- |
| 920 | | host_platform(windows),!, List=['.exe','']. % will backtrack in get_command_in_lib |
| 921 | | get_binary_extensions(['']). |
| 922 | | |
| 923 | | fuzz_filename(TexFile,FuzzFile) :- |
| 924 | | split_filename(TexFile,Basename,_Extension), |
| 925 | | atom_chars(Basename,BasenameC), |
| 926 | | append(BasenameC,['.','f','u','z','z'],CC), |
| 927 | | atom_chars(FuzzFile,CC),!. |
| 928 | | fuzz_filename(TexFile, FuzzFile) :- |
| 929 | | add_failed_call_error(fuzz_filename(TexFile,FuzzFile)),fail. |