123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341(**************************************************************************)(* *)(* This file is part of Frama-C. *)(* *)(* Copyright (C) 2007-2023 *)(* 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 licenses/LGPLv2.1). *)(* *)(**************************************************************************)(* -------------------------------------------------------------------------- *)(* --- Socket Server Options --- *)(* -------------------------------------------------------------------------- *)moduleSenv=Server_parametersletsocket_group=Senv.add_group"Protocol Unix Sockets"let()=Parameter_customize.set_groupsocket_groupmoduleSocket=Senv.String(structletoption_name="-server-socket"letarg_name="url"letdefault=""lethelp="Launch the UnixSocket server (in background).\n\
The server can handle GET requests during the\n\
execution of the frama-c command line.\n\
Finally, the server is executed until shutdown."end)let()=Parameter_customize.set_groupsocket_groupmoduleSocketSize=Senv.Int(structletoption_name="-server-socket-size"letarg_name="n"letdefault=256lethelp="Control the size of socket buffers (in ko, default 256)."end)let_=Server_doc.protocol~title:"Unix Socket Protocol"~readme:"server_socket.md"(* -------------------------------------------------------------------------- *)(* --- Socket Bytes Read & Write --- *)(* -------------------------------------------------------------------------- *)typechannel={sock:Unix.file_descr;(* Socket *)snd:bytes;(* SND bytes buffer, re-used for transport *)rcv:bytes;(* RCV bytes buffer, re-used for transport *)brcv:Buffer.t;(* RCV data buffer, accumulated *)bsnd:Buffer.t;(* SND data buffer, accumulated *)}letread_bytes{sock;rcv;brcv}=(* rcv buffer is only used locally *)lets=Bytes.lengthrcvinletrecscanp=(* try to fill RCV buffer *)letn=tryUnix.readsockrcvp(s-p)withUnix.Unix_error((EAGAIN|EWOULDBLOCK),_,_)->0inletp=p+ninifn>0&&p<sthenscanpelsepinletn=scan0inifn>0thenBuffer.add_subbytesbrcvrcv0nletsend_bytes{sock;snd;bsnd}=(* snd buffer is only used locally *)letn=Buffer.lengthbsndinifn>0thenlets=Bytes.lengthsndinletrecsendp=(* try to flush BSND buffer *)letw=min(n-p)sinBuffer.blitbsndpsnd0w;letr=tryUnix.single_writesocksnd0wwithUnix.Unix_error((EAGAIN|EWOULDBLOCK),_,_)->0inletp=p+rinifr>0&&p<nthensendpelsepinletp=send0inifp>0thenlettail=Buffer.subbsndp(n-p)inBuffer.resetbsnd;Buffer.add_stringbsndtail(* -------------------------------------------------------------------------- *)(* --- Data Chunks Encoding --- *)(* -------------------------------------------------------------------------- *)letread_datach=try(* Try to read all the data.
In case there is not enough bytes in the buffer,
calls to Buffer.sub would raise Invalid_argument. *)leth=matchBuffer.nthch.brcv0with|'S'->3|'L'->7|'W'->15|_->raise(Invalid_argument"Server_socket.read")inlethex=Buffer.subch.brcv1hinletlen=int_of_string("0x"^hex)inletdata=Buffer.subch.brcv(1+h)leninletp=1+h+leninletn=Buffer.lengthch.brcv-pin(* TODO[LC]: inefficient move. Requires a ring-buffer. *)letrest=Buffer.subch.brcvpninBuffer.resetch.brcv;Buffer.add_stringch.brcvrest;SomedatawithInvalid_argument_->Noneletwrite_datachdata=beginletlen=String.lengthdatainlethex=iflen<0xFFFthenPrintf.sprintf"S%03x"lenelseiflen<0xFFFFFFFthenPrintf.sprintf"L%07x"lenelsePrintf.sprintf"W%015x"leninBuffer.add_stringch.bsndhex;Buffer.add_stringch.bsnddata;end(* -------------------------------------------------------------------------- *)(* --- Request Encoding --- *)(* -------------------------------------------------------------------------- *)letjfieldfdjs=Json.fieldfdjs|>Json.stringletdecode(data:string):stringMain.request=matchdatawith|"\"POLL\""->`Poll|"\"SHUTDOWN\""->`Shutdown|_->letjs=Yojson.Basic.from_stringdatainmatchjfield"cmd"jswith|"GET"|"SET"|"EXEC"->letid=jfield"id"jsinletrequest=jfield"request"jsinletdata=Json.field"data"jsin`Request(id,request,data)|"SIGON"->`SigOn(jfield"id"js)|"SIGOFF"->`SigOff(jfield"id"js)|"KILL"->`Kill(jfield"id"js)|_->Senv.debug~level:2"Invalid socket command:@ @[<hov 2>%a@]"Json.ppjs;raiseNot_foundletencode(resp:stringMain.response):string=letjs=matchrespwith|`Data(id,data)->`Assoc["res",`String"DATA";"id",`Stringid;"data",data]|`Error(id,msg)->`Assoc["res",`String"ERROR";"id",`Stringid;"msg",`Stringmsg]|`Killedid->`Assoc["res",`String"KILLED";"id",`Stringid]|`Rejectedid->`Assoc["res",`String"REJECTED";"id",`Stringid]|`Signalid->`Assoc["res",`String"SIGNAL";"id",`Stringid]|`CmdLineOn->`String"CMDLINEON"|`CmdLineOff->`String"CMDLINEOFF"inYojson.Basic.to_string~std:falsejsletparsech=letrecscancmdsch=matchread_datachwith|None->List.revcmds|Somedata->matchdecodedatawith|cmd->scan(cmd::cmds)ch|exception_->scancmdschinscan[]ch(* -------------------------------------------------------------------------- *)(* --- Socket Messages --- *)(* -------------------------------------------------------------------------- *)letcallbackchrs=List.iter(funr->matchencoderwith|data->write_datachdata|exceptionerr->Senv.debug"Socket: encoding error %S@."(Printexc.to_stringerr))rs;send_byteschletcommandsch=beginread_bytesch;matchparsechwith|[]->send_bytesch;None|requests->SomeMain.{requests;callback=callbackch}end(* -------------------------------------------------------------------------- *)(* --- Establish the Server --- *)(* -------------------------------------------------------------------------- *)typesocket={socket:Unix.file_descr;mutablechannel:channeloption;}letclose(s:socket)=matchs.channelwithNone->()|Somech->s.channel<-None;Unix.closech.sockletset_socket_sizesockopts=beginletnbytes=s*1024in(tryUnix.setsockopt_intsockoptnbyteswithUnix.Unix_error(err,_,_)->letmsg=Unix.error_messageerrinSenv.warning~once:true"Invalid socket size (%d: %s)"nbytesmsg);Unix.getsockopt_intsockoptendletchannel(s:socket)=matchs.channelwith|Some_aschan->chan|None->tryletsock,_=Unix.accept~cloexec:trues.socketinUnix.set_nonblocksock;letsize=SocketSize.get()inletrcv=set_socket_sizesockSO_RCVBUFsizeinletsnd=set_socket_sizesockSO_SNDBUFsizeinSenv.debug~level:2"Socket size in:%d out:%d@."rcvsnd;Senv.debug"Client connected";letch=Some{sock;snd=Bytes.createsnd;rcv=Bytes.creatercv;bsnd=Buffer.createsnd;brcv=Buffer.creatercv;}ins.channel<-ch;chwithUnix.Unix_error(EAGAIN,_,_)->Noneletfetch(s:socket)()=trymatchchannelswith|None->None|Somech->commandschwith|Unix.Unix_error(EPIPE,_,_)->Senv.debug"Client disconnected";closes;None|exn->Senv.warning"Socket: exn %s"(Printexc.to_stringexn);closes;Noneletestablish_serverfd=letsocket={socket=fd;channel=None}intryUnix.listenfd1;ignore(Sys.signalSys.sigpipeSignal_ignore);letpretty=Format.pp_print_stringinletserver=Main.create~pretty~fetch:(fetchsocket)()inExtlib.safe_at_exitbeginfun()->Main.stopserver;closesocket;end;Main.startserver;Cmdline.at_normal_exitbeginfun()->Main.runserver;closesocket;end;withexn->closesocket;raiseexn(* -------------------------------------------------------------------------- *)(* --- Synchronous Server --- *)(* -------------------------------------------------------------------------- *)letserver=refNoneletcmdline()=letoption=matchSocket.get()with""->None|a->Someainmatch!server,optionwith|_,None->()|Someaddr0,Someaddr->ifaddr0<>addrthenSenv.warning"Socket server already running on [%s]."addr0|None,Someaddr->begintryserver:=option;letaddr_path=Filepath.Normalized.of_stringaddrinifFilepath.existsaddr_paththenUnix.unlinkaddr;letfd=Unix.socketPF_UNIXSOCK_STREAM0inUnix.bindfd(ADDR_UNIXaddr);ifSenv.debug_atleast1thenSenv.feedback"Socket server running on [%s]."addrelseSenv.feedback"Socket server running.";establish_serverfd;withexn->Senv.fatal"Server socket failed.@\nError: %s@"(Printexc.to_stringexn)endlet()=Db.Main.extendcmdline(* -------------------------------------------------------------------------- *)