Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file wp_multicore.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316(**************************************************************************)(* *)(* This file is part of the Frama-C's Luncov plug-in. *)(* *)(* Copyright (C) 2012-2025 *)(* CEA (Commissariat à l'énergie atomique et aux énergies *)(* alternatives) *)(* *)(* you can redistribute it and/or modify it under the terms of the GNU *)(* Lesser General Public License as published by the Free Software *)(* Foundation, version 2.1. *)(* *)(* It is distributed in the hope that it will be useful, *)(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)(* GNU Lesser General Public License for more details. *)(* *)(* See the GNU Lesser General Public License version 2.1 *)(* for more details (enclosed in the file LICENSE) *)(* *)(**************************************************************************)openUnixopenCil_typesopenWpletnumber_of_processes=ref1(** Process pool: a pool of unix processes that compute label statuses in parallel **)(* Helper Functions *)letget_kf_namekf=matchkf.fundecwith|Definition(f,_)->f.svar.vname|Declaration(_,f,_,_)->f.vnameletwait_for_children()=letoutput_file=(string_of_int(Unix.getpid()))^"wfc.tmp"inignore(Sys.command("pgrep -c -P "^(string_of_int(Unix.getpid()))^" --full \"[alt\\-ergo] <defunct>\" > "^output_file));ifSys.file_existsoutput_filethenbeginletic=open_inoutput_fileinletline=input_lineicinclose_inic;Sys.removeoutput_file;letnb_children=int_of_string(String.trimline)infori=1tonb_childrendoignore(i);ignore(Unix.wait())doneendletget_resident_memory_usagepid=letoutput_file=(string_of_int(Unix.getpid()))^"mu.tmp"inignore(Sys.command("ps -p "^(string_of_intpid)^" --no-headers -o rss > "^output_file));letic=open_inoutput_fileinletline=input_lineicinclose_inic;Sys.removeoutput_file;int_of_string(String.trimline)letrecn_first_alna=match(l,n)with|(l,0)->(a,l)|(h::t,n)->letnew_a=h::ainletnew_n=n-1in(n_first_atnew_nnew_a)|([],_)->(a,[])letn_firstln=n_first_aln[](* Splits the list l after n elements *)letrecsplit_list_size_alna=matchn_firstlnwith|(f,h::t)->letnew_l=h::tinletnew_a=f::ain(split_list_size_anew_lnnew_a)|(f,[])->f::aletsplit_list_sizel=letn=Options.WPMaxNbLabelPerCall.get()inifn>0thensplit_list_size_aln[]else[l](* Splits a list l in list chunks of size n *)letno_output()=letdevnull=descr_of_out_channel(open_out"/dev/null")indup2devnullstdout(* The task of one worker process, with result marshalling of the results to the main process *)letwp_callkflabelschannel=(* Adding annotations for labels *)letips=Instrument_multicore.add_annotations_get_ipslabelsin(* Proving annotations with WP *)ifnot(Options.WPQedOptim.get())thenbeginWp_parameters.Simpl.setfalse;Wp_parameters.Let.setfalse;Wp_parameters.Prune.setfalse;Wp_parameters.Clean.setfalseend;List.iter(funs->Wp_parameters.Model.adds)["typed";"int";"float";"var"];letflag=reftrueinbegintryVC.(command(generate_kfkf))withe->flag:=false;Options.feedback"WP was interrupted during check: aborting computation for these labels";raiseeend;(* Gathering annotation statuses and sending to root process *)Hashtbl.iter(funlblidip->letstatus=(matchipwith|None->"invalid"|Someip_v->letvalue_st=List.for_allVC.is_valid(VC.proofip_v)in(*let value_st = (try (is_valid ip_v) with _ -> false) in*)ifvalue_st&&!flagthen("valid")else("invalid"))inletmessage=("false"^"\n"^(string_of_intlblid)^"\n"^status^"\n")inoutput_stringchannelmessage;flushchannel)ips(* The task of one intermediate process, creating and managing worker processes *)lettasktaskschannel=(* Successive calls are made to WP, handling each a part of the labels from labs: avoids WP to consume to much memory if all labels are handled in one time *)List.iter(fun(kf,labels)->matchfork()with|0->(* Handling time-out or memory overflow properly, notably killing and cleaning alt-ergo grand-children processes *)Sys.set_signalSys.sigalrm(Sys.Signal_handle(fun_->ignore(Sys.command("pkill --signal 9 --parent "^(string_of_int(getpid()))));wait_for_children();exit0));ifnot(Options.WPShowLogs.get())thenno_output();(* Calling WP *)wp_callkflabelschannel;(* Exiting properly *)wait_for_children();(* WP doesn't seem to wait correctly for the alt-ergo processes it creates. This is repaired here. *)exit0|child_pid->Options.feedback"Starting worker process with pid %d to process %d labels of function %s."child_pid(List.lengthlabels)(get_kf_namekf);lettimeout=Options.MultiCoreKillTimeout.get()inletmaxmemory=Options.MultiCoreMaxMemory.get()inlettime=ref0inletexited=reffalsein(* Wait for child to die (via wait) or kills it if its memory usage overflows or execution time takes too long *)while!time<=timeout&¬(!exited)&&(get_resident_memory_usagechild_pid)<maxmemorydoUnix.sleep1;let(pid,_)=Unix.waitpid[Unix.WNOHANG]child_pidinifpid>0thenexited:=true;incrtimedone;(* Child died *)if!exitedthenbeginOptions.feedback"Worker process with pid %d ended normally"child_pid;()endelsebegin(* Killing child *)Options.feedback"Killing worker process with pid %d"child_pid;Unix.killchild_pidSys.sigalrm;ignore(Unix.waitpid[]child_pid);(* Saving all labels treated by child as unknown *)List.iter(funlblid->letmessage=("false"^"\n"^(string_of_intlblid)^"\n"^"invalid"^"\n")inoutput_stringchannelmessage;flushchannel)labelsend;)tasks;(* Termination *)letmessage=("true"^"\n"^(string_of_int(getpid()))^"\n"^"na"^"\n")inoutput_stringchannelmessage;flushchannel;close_outchannel(* The main process creates the intermediate processes through unix fork and pipes *)letrecinitialize_pool(_,checker)schedule=create_children0([],(Hashtbl.create!number_of_processes))checkerscheduleandcreate_childrencntacc_fdchksch=letparameter=(List.hdsch)inflush_all();let(fd_in,fd_out)=pipe()inmatchfork()with|0->closefd_in;taskparameter(out_channel_of_descrfd_out);exit0|child_pid->closefd_out;Options.feedback"Starting supervisor process with pid %d"child_pid;letnew_cnt=cnt+1inifnew_cnt<!number_of_processesthenbeginletres=(create_childrennew_cntacc_fdchk(List.tlsch))in(Hashtbl.add(sndres)fd_in(in_channel_of_descrfd_in));(fd_in::(fstres),sndres)endelsebegin(Hashtbl.add(sndacc_fd)fd_in(in_channel_of_descrfd_in));(fd_in::(fstacc_fd),sndacc_fd)end(* The main process receives and saves the label statuses computed by the worker processes transmitted through pipes *)letrecprocess_resultsfdschsforce(checker_name,_)data=get_resultsfdschs0forcechecker_namedataandget_resultsfdschscntforcechecker_namedata=match(Unix.selectfds[][](-1.0))with|fdl,[],[]->letprocessaccfd=(letchannel=Hashtbl.findchsfdinleteof=(input_linechannel="true")inletlblid=int_of_string(input_linechannel)inletstatus=if(input_linechannel="valid")thenData_labels.UncoverableelseData_labels.Unknowninignore(Sys.command"pkill --signal 9 --parent 1 --full alt-ergo");(* Dirty but alt-ergo can create polluting subprocesses orphaned when killing wp because of time-out. *)ifeofthenbeginclose_inchannel;Options.feedback"Exiting supervisor process with pid %d"lblid;ignore(Unix.wait());fd::accendelsebeginData_labels.updatedata~force~status~emitter:checker_namelblid;accend)inletkilled_children=(List.fold_leftprocess[]fdl)inletnb_killed_children=cnt+(List.lengthkilled_children)inifnb_killed_children<!number_of_processesthenget_results(List.filter(funfd->not(List.memfdkilled_children))fds)chsnb_killed_childrenforcechecker_namedataelse()|_,_,_->failwith"Unexpected pipe interaction with main process."letprocess_in_parallelforcecheckerscheduledata=let(fds,chs)=initialize_poolcheckerscheduleinprocess_resultsfdschsforcecheckerdataletwp_property_checker=letcheck~label:__=()in("WP",check)(** Task a-priori scheduling: given a set of tasks, provide an a-priori distribution between a set of processes **)(* head_nary [1;2;3;4;5] 2 = ([1,2],[3,4,5]) *)letrechead_naryln=split_head[]lnandsplit_headhtn=ifn>0thenbeginmatchtwith|hd::tl->split_head(h@[hd])tl(n-1)|[]->(h,t)endelse(h,t)(* split_in_n [1;2;3;4;5] 2 = [[1,2],[3,4],[5]] *)letrecsplit_in_nln=matchlwith|_::_->letfirst=head_narylnin(fstfirst)::(split_in_n(sndfirst)n)|[]->[]letcompare_tasks(_,labsl)(_,labsr)=letnbl=List.lengthlabslinletnbr=List.lengthlabsrinnbr-nblletrecinvert_oddsl=matchlwith|[]->l|_::[]->l|f::s::t->f::(List.revs)::(invert_oddst)letcompose_with_i_ththe_spliti=List.fold_left(funacclt->if(List.lengthlt)<=ithenaccelse(List.nthlti)::acc)[]the_splitletreccreate_up_to_nthe_splitnacc=ifn<=0thenaccelse(create_up_to_nthe_split(n-1)((compose_with_i_ththe_split(n-1))::acc))letsplittasksnb_processes=letthe_split=invert_odds(split_in_ntasksnb_processes)increate_up_to_nthe_splitnb_processes[]letsplit_tasks_for_fair_sharing_of_nb_lablelstasksnb_process=letsorted_tasks=List.sortcompare_taskstasksinsplitsorted_tasksnb_processletgenerate_tasks(kfs,kf_lb)=lettasks=ref[]inInstrument_multicore.KFSet.iter(funkf->List.iter(funel->tasks:=(kf,el)::!tasks)(split_list_size(Hashtbl.find_allkf_lb(get_kf_namekf))))kfs;!tasksletcompute_multicore?(force=false)data=letchecker=wp_property_checkerinifOptions.Rte.get()thenRteGen.Api.compute();Instrument_multicore.at:=true;ignore(Instrument_multicore.create_project());lettasks=generate_tasks(Instrument_multicore.get_kf_lbl_partition())inOptions.feedback"start weakest-precondition-based detection";letnbTasks=(List.lengthtasks)inifnbTasks>0thenbeginletnb_processes=minnbTasks(Options.Multicore.get())innumber_of_processes:=nb_processes;letschedule=split_tasks_for_fair_sharing_of_nb_lablelstasksnb_processesinprocess_in_parallelforcecheckerscheduledataend;Options.feedback"WP-based detection done"letcompute_multicoreAT?(force=false)data=letchecker=wp_property_checkerinifOptions.Rte.get()thenRteGen.Api.compute();Instrument_multicore.at:=false;ignore(Instrument_multicore.create_project());lettasks=generate_tasks(Instrument_multicore.get_kf_lbl_partition())inOptions.feedback"start weakest-precondition-based detection (for always true labels)";letnbTasks=(List.lengthtasks)inifnbTasks>0thenbeginletnb_processes=minnbTasks(Options.Multicore.get())innumber_of_processes:=nb_processes;letschedule=split_tasks_for_fair_sharing_of_nb_lablelstasksnb_processesinprocess_in_parallelforcecheckerscheduledataend;Options.feedback"WP-based detection (for always true labels) done"