Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
85f440f6
Commit
85f440f6
authored
3 years ago
by
Loïc Correnson
Browse files
Options
Downloads
Patches
Plain Diff
[server] non-blocking double-buffer read
parent
333189be
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/server/server_socket.ml
+41
-42
41 additions, 42 deletions
src/plugins/server/server_socket.ml
with
41 additions
and
42 deletions
src/plugins/server/server_socket.ml
+
41
−
42
View file @
85f440f6
...
@@ -55,17 +55,23 @@ type channel = {
...
@@ -55,17 +55,23 @@ type channel = {
mutable
eof
:
bool
;
mutable
eof
:
bool
;
inc
:
in_channel
;
inc
:
in_channel
;
out
:
out_channel
;
out
:
out_channel
;
tmp
:
bytes
;
buffer
:
Buffer
.
t
;
buffer
:
Buffer
.
t
;
}
}
let
feed
ch
=
let
feed
_bytes
ch
=
if
not
ch
.
eof
then
if
not
ch
.
eof
then
try
Buffer
.
add_channel
ch
.
buffer
ch
.
inc
buffer_size
try
with
End_of_file
->
ch
.
eof
<-
true
let
n
=
input
ch
.
inc
ch
.
tmp
0
buffer_size
in
if
n
>
0
then
Format
.
eprintf
"READ %d bytes@."
n
;
Buffer
.
add_subbytes
ch
.
buffer
ch
.
tmp
0
n
;
with
|
Sys_blocked_io
->
()
|
End_of_file
->
ch
.
eof
<-
true
let
read
ch
=
let
read
_data
ch
=
try
try
Format
.
printf
"
READ
%S@."
(
Buffer
.
contents
ch
.
buffer
);
Format
.
e
printf
"
DATA
%S@."
(
Buffer
.
contents
ch
.
buffer
)
;
let
h
=
match
Buffer
.
nth
ch
.
buffer
0
with
let
h
=
match
Buffer
.
nth
ch
.
buffer
0
with
|
'
S'
->
3
|
'
S'
->
3
|
'
L'
->
7
|
'
L'
->
7
...
@@ -84,7 +90,7 @@ let read ch =
...
@@ -84,7 +90,7 @@ let read ch =
with
Invalid_argument
_
->
with
Invalid_argument
_
->
None
None
let
write
ch
data
=
let
write
_data
ch
data
=
begin
begin
let
len
=
String
.
length
data
in
let
len
=
String
.
length
data
in
let
hex
=
let
hex
=
...
@@ -143,17 +149,14 @@ let encode (resp : string Main.response) : string =
...
@@ -143,17 +149,14 @@ let encode (resp : string Main.response) : string =
in
Yojson
.
Basic
.
to_string
~
std
:
false
js
in
Yojson
.
Basic
.
to_string
~
std
:
false
js
let
parse
ch
=
let
parse
ch
=
begin
let
rec
scan
cmds
ch
=
feed
ch
;
match
read_data
ch
with
let
rec
scan
cmds
ch
=
|
None
->
List
.
rev
cmds
match
read
ch
with
|
Some
data
->
|
None
->
List
.
rev
cmds
match
decode
data
with
|
Some
data
->
|
cmd
->
scan
(
cmd
::
cmds
)
ch
match
decode
data
with
|
exception
_
->
scan
cmds
ch
|
cmd
->
scan
(
cmd
::
cmds
)
ch
in
scan
[]
ch
|
exception
_
->
scan
cmds
ch
in
scan
[]
ch
end
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* --- Socket Messages --- *)
(* --- Socket Messages --- *)
...
@@ -163,15 +166,18 @@ let callback ch rs =
...
@@ -163,15 +166,18 @@ let callback ch rs =
List
.
iter
List
.
iter
(
fun
r
->
(
fun
r
->
match
encode
r
with
match
encode
r
with
|
data
->
write
ch
data
|
data
->
write
_data
ch
data
|
exception
_
->
()
|
exception
_
->
()
)
rs
)
rs
let
commands
ch
=
let
commands
ch
=
if
ch
.
eof
then
None
else
if
ch
.
eof
then
None
else
match
parse
ch
with
begin
|
[]
->
None
feed_bytes
ch
;
|
requests
->
Some
Main
.{
requests
;
callback
=
callback
ch
}
match
parse
ch
with
|
[]
->
None
|
requests
->
Some
Main
.{
requests
;
callback
=
callback
ch
}
end
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* --- Establish the Server --- *)
(* --- Establish the Server --- *)
...
@@ -182,43 +188,40 @@ type socket = {
...
@@ -182,43 +188,40 @@ type socket = {
mutable
channel
:
channel
option
;
mutable
channel
:
channel
option
;
}
}
let
close
(
s
:
socket
)
=
match
s
.
channel
with
None
->
()
|
Some
ch
->
begin
s
.
channel
<-
None
;
close_in
ch
.
inc
;
close_out
ch
.
out
;
end
let
fetch
(
s
:
socket
)
()
=
let
fetch
(
s
:
socket
)
()
=
Format
.
printf
"SOCKET-FETCH@."
;
try
try
match
s
.
channel
with
match
s
.
channel
with
|
Some
ch
->
commands
ch
|
Some
ch
->
commands
ch
|
None
->
|
None
->
let
fd
,_
=
Unix
.
accept
~
cloexec
:
true
s
.
socket
in
let
fd
,_
=
Unix
.
accept
~
cloexec
:
true
s
.
socket
in
Unix
.
set_nonblock
fd
;
let
inc
=
Unix
.
in_channel_of_descr
fd
in
let
inc
=
Unix
.
in_channel_of_descr
fd
in
let
out
=
Unix
.
out_channel_of_descr
fd
in
let
out
=
Unix
.
out_channel_of_descr
fd
in
Senv
.
debug
"Client connected"
;
Senv
.
debug
"Client connected"
;
let
ch
=
{
let
ch
=
{
eof
=
false
;
inc
;
out
;
eof
=
false
;
inc
;
out
;
tmp
=
Bytes
.
create
buffer_size
;
buffer
=
Buffer
.
create
buffer_size
;
buffer
=
Buffer
.
create
buffer_size
;
}
in
}
in
s
.
channel
<-
Some
ch
;
s
.
channel
<-
Some
ch
;
commands
ch
commands
ch
with
with
|
Unix
.
Unix_error
(
EAGAIN
,_,_
)
->
None
|
Unix
.
Unix_error
_
->
close
s
;
None
|
Stdlib
.
Sys_error
msg
->
Senv
.
warning
"SocketClient: sys %s"
msg
;
None
|
exn
->
|
exn
->
Senv
.
warning
"SocketClient: exn %s"
(
Printexc
.
to_string
exn
)
;
Senv
.
warning
"Socket: exn %s"
(
Printexc
.
to_string
exn
)
;
None
close
s
;
None
let
close
(
s
:
socket
)
=
Unix
.
shutdown
s
.
socket
SHUTDOWN_ALL
;
match
s
.
channel
with
None
->
()
|
Some
ch
->
begin
close_in
ch
.
inc
;
close_out
ch
.
out
;
end
let
bind
fd
=
let
bind
fd
=
let
socket
=
{
socket
=
fd
;
channel
=
None
}
in
let
socket
=
{
socket
=
fd
;
channel
=
None
}
in
try
try
Unix
.
set_nonblock
fd
;
Unix
.
listen
fd
1
;
Unix
.
listen
fd
1
;
Unix
.
set_nonblock
fd
;
Unix
.
set_nonblock
fd
;
ignore
(
Sys
.
signal
Sys
.
sigpipe
Signal_ignore
)
;
ignore
(
Sys
.
signal
Sys
.
sigpipe
Signal_ignore
)
;
...
@@ -229,11 +232,7 @@ let bind fd =
...
@@ -229,11 +232,7 @@ let bind fd =
close
socket
;
close
socket
;
end
;
end
;
Main
.
start
server
;
Main
.
start
server
;
Cmdline
.
at_normal_exit
(
fun
()
->
Cmdline
.
at_normal_exit
(
fun
()
->
Main
.
run
server
)
;
Format
.
eprintf
"SERVER-RUN@."
;
Main
.
run
server
;
Format
.
eprintf
"SERVER-OUT@."
;
)
;
with
exn
->
with
exn
->
close
socket
;
close
socket
;
raise
exn
raise
exn
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment