buffered_connection.anubis
4.21 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
/*
*
* User: David RENE
* Date: 16/08/2009
* Time: 21:28
* (c) Calexium
*
*/
read tools/basis.anubis
read tools/connections.anubis
public type BC_Result:
failure,
timeout,
success(Word8).
public type BC_Error: //BC for Buffered Connection
cannot_read_from_connection,
timeout(Int).
public type Buffered_connection:
buffered_connection(Connection conn,
Var(ByteArray) buffer,
Var(Int) read_pos,
Var(List(Word8)) unput_buffer).
public define One
unput_byte // unputting a character (add it in front of the list)
(
Buffered_connection buf_con,
Word8 character
) =
buf_con.unput_buffer <- (List(Word8))[character . * buf_con.unput_buffer].
define String
pid
=
"[" + virtual_machine_id + "] ".
define One
put
(
ByteArray source,
ByteArray dest,
Int position,
Int i
) =
if nth(i,source) is
{
failure then unique,
success(b) then if put(dest,position,b) is
{
failure then unique,
success(_) then put(source,dest,position+1,i+1)
}
}.
define ReadResult
read_from_connexion
(
Buffered_connection connection,
Int size,
Int time_out,
ByteArray result_buffer,
Int position
) =
println(pid + "read_from_connexion(" + size + ")");
if *connection.read_pos < length(*connection.buffer) then
println(pid + " reading from buffer (size = " + length(*connection.buffer) + ", pos = " + *connection.read_pos);
//with t1_tmp = (UTime) unow,
with result = extract(*connection.buffer, *connection.read_pos, *connection.read_pos + size),
size_read = length(result),
put(result,result_buffer,position,0);
connection.read_pos <- *connection.read_pos + size_read;
//accumulate_t1(t1_tmp);
if size > size_read then
println("Wanted " + size + ", read only " + size_read);
terminal read_from_connexion(connection, size - size_read, time_out, result_buffer,position+size_read)
// {
// error then error,
// timeout then ok(result),
// ok(ba) then ok(result + ba)
// }
else
ok(result_buffer)
else
//if unow > dead_line then record_dubious_connection(connection,dead_line,dos) else
if read(connection.conn, 16384, time_out) is // the connection is closed after 10 minutes of inactivity
{
error then println(pid + "read failed)"); error,
timeout then timeout,
ok(ba) then
println(pid + "ba = " + length(ba));
connection.buffer <- ba;
connection.read_pos <- 0;
//println(pid + "rb = " + length(*read_buffer));
terminal read_from_connexion(connection, size, time_out, result_buffer,position)
}.
/** next_char
* Read char on buffered connection.
* reading a character (check the list first, and read on the connection
* only when the list is empty).
*/
public define BC_Result
read_byte
(
Buffered_connection connection,
Int t_out
) =
if *connection.unput_buffer is
{
[ ] then
// ///////////////////
// Buffered reading
if nth(*connection.read_pos, *connection.buffer) is
{
failure then
if read_from_connexion(connection, 1, t_out, constant_byte_array(1,0),0) is // the connection is closed after 10 minutes of inactivity
{
error then failure, //error(cannot_read_from_connection), */
timeout then timeout, //error(timeout(600)), */
ok(ba) then if nth(0,ba) is
{
failure then failure // error(cannot_read_from_connection),
success(c) then
//println("read_byte 1 ["+c+"]");
success(c)
}
},
success(c) then connection.read_pos <- *connection.read_pos + 1;
//println("read_byte 2 ["+c+"]");
success(c)
},
[h . t] then
connection.unput_buffer <- t;
//println("read byte from unput queue ["+h+"]");
success(h)
}.