backup/EWF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

add precondition saying the request line should not be empty

Browse Source
This commit is contained in:
Jocelyn Fiat
2011-09-21 15:26:23 +02:00
parent 9fef2d71f0
commit 58767bb1c1
1 changed files with 182 additions and 182 deletions
Download Patch File Download Diff File Expand all files Collapse all files

364
library/http_connection_handler.e
View File

@@ -1,183 +1,183 @@
note note
description: "Summary description for {HTTP_CONNECTION_HANDLER}." description: "Summary description for {HTTP_CONNECTION_HANDLER}."
author: "" author: ""
date: "$Date$" date: "$Date$"
revision: "$Revision$" revision: "$Revision$"
deferred class deferred class
HTTP_CONNECTION_HANDLER HTTP_CONNECTION_HANDLER
inherit inherit
HTTP_HANDLER HTTP_HANDLER
redefine redefine
make make
end end
feature {NONE} -- Initialization feature {NONE} -- Initialization
make (a_main_server: like main_server; a_name: STRING) make (a_main_server: like main_server; a_name: STRING)
-- Creates a {HTTP_CONNECTION_HANDLER}, assigns the main_server and sets the current_request_message to empty. -- Creates a {HTTP_CONNECTION_HANDLER}, assigns the main_server and sets the current_request_message to empty.
-- --
-- `a_main_server': The main server object -- `a_main_server': The main server object
-- `a_name': The name of this module -- `a_name': The name of this module
do do
Precursor (a_main_server, a_name) Precursor (a_main_server, a_name)
reset reset
end end
reset reset
do do
create method.make_empty create method.make_empty
create uri.make_empty create uri.make_empty
create request_header.make_empty create request_header.make_empty
create request_header_map.make (10) create request_header_map.make (10)
remote_info := Void remote_info := Void
end end
feature -- Execution feature -- Execution
receive_message_and_send_reply (client_socket: TCP_STREAM_SOCKET) receive_message_and_send_reply (client_socket: TCP_STREAM_SOCKET)
local local
l_input: HTTP_INPUT_STREAM l_input: HTTP_INPUT_STREAM
l_output: HTTP_OUTPUT_STREAM l_output: HTTP_OUTPUT_STREAM
l_remote_info: detachable like remote_info l_remote_info: detachable like remote_info
do do
create l_input.make (client_socket) create l_input.make (client_socket)
create l_output.make (client_socket) create l_output.make (client_socket)
create l_remote_info create l_remote_info
if attached client_socket.peer_address as l_addr then if attached client_socket.peer_address as l_addr then
l_remote_info.addr := l_addr.host_address.host_address l_remote_info.addr := l_addr.host_address.host_address
l_remote_info.hostname := l_addr.host_address.host_name l_remote_info.hostname := l_addr.host_address.host_name
l_remote_info.port := l_addr.port l_remote_info.port := l_addr.port
remote_info := l_remote_info remote_info := l_remote_info
end end
analyze_request_message (l_input) analyze_request_message (l_input)
process_request (Current, l_input, l_output) process_request (Current, l_input, l_output)
reset reset
end end
feature -- Request processing feature -- Request processing
process_request (a_handler: HTTP_CONNECTION_HANDLER; a_input: HTTP_INPUT_STREAM; a_output: HTTP_OUTPUT_STREAM) process_request (a_handler: HTTP_CONNECTION_HANDLER; a_input: HTTP_INPUT_STREAM; a_output: HTTP_OUTPUT_STREAM)
-- Process request ... -- Process request ...
require require
a_handler_attached: a_handler /= Void a_handler_attached: a_handler /= Void
a_uri_attached: a_handler.uri /= Void a_uri_attached: a_handler.uri /= Void
a_method_attached: a_handler.method /= Void a_method_attached: a_handler.method /= Void
a_header_map_attached: a_handler.request_header_map /= Void a_header_map_attached: a_handler.request_header_map /= Void
a_header_text_attached: a_handler.request_header /= Void a_header_text_attached: a_handler.request_header /= Void
a_input_attached: a_input /= Void a_input_attached: a_input /= Void
a_output_attached: a_output /= Void a_output_attached: a_output /= Void
deferred deferred
end end
feature -- Access feature -- Access
request_header: STRING request_header: STRING
-- Header' source -- Header' source
request_header_map : HASH_TABLE [STRING,STRING] request_header_map : HASH_TABLE [STRING,STRING]
-- Contains key:value of the header -- Contains key:value of the header
method: STRING method: STRING
-- http verb -- http verb
uri: STRING uri: STRING
-- http endpoint -- http endpoint
version: detachable STRING version: detachable STRING
-- http_version -- http_version
--| unused for now --| unused for now
remote_info: detachable TUPLE [addr: STRING; hostname: STRING; port: INTEGER] remote_info: detachable TUPLE [addr: STRING; hostname: STRING; port: INTEGER]
feature -- Parsing feature -- Parsing
parse_http_request_line (line: STRING) parse_http_request_line (line: STRING)
require require
line /= Void line /= Void
local local
pos, next_pos: INTEGER pos, next_pos: INTEGER
do do
print ("%N parse http request line:%N" + line) print ("%N parse http request line:%N" + line)
-- parse (this should be done by a lexer) -- parse (this should be done by a lexer)
pos := line.index_of (' ', 1) pos := line.index_of (' ', 1)
method := line.substring (1, pos - 1) method := line.substring (1, pos - 1)
next_pos := line.index_of (' ', pos+1) next_pos := line.index_of (' ', pos+1)
uri := line.substring (pos+1, next_pos-1) uri := line.substring (pos+1, next_pos-1)
ensure ensure
not_void_method: method /= Void not_void_method: method /= Void
end end
analyze_request_message (a_input: HTTP_INPUT_STREAM) analyze_request_message (a_input: HTTP_INPUT_STREAM)
require require
input_readable: a_input /= Void and then a_input.is_readable input_readable: a_input /= Void and then a_input.is_readable
local local
end_of_stream : BOOLEAN end_of_stream : BOOLEAN
pos,n : INTEGER pos,n : INTEGER
line : STRING line : STRING
k, val: STRING k, val: STRING
txt: STRING txt: STRING
do do
create txt.make (64) create txt.make (64)
a_input.read_line a_input.read_line
line := a_input.last_string line := a_input.last_string
analyze_request_line (line) analyze_request_line (line)
txt.append (line) txt.append (line)
txt.append_character ('%N') txt.append_character ('%N')
request_header := txt request_header := txt
from from
a_input.read_line a_input.read_line
until until
end_of_stream end_of_stream
loop loop
line := a_input.last_string line := a_input.last_string
n := line.count n := line.count
print ("%N" +line+ "%N") print ("%N" +line+ "%N")
pos := line.index_of (':',1) pos := line.index_of (':',1)
if pos > 0 then if pos > 0 then
k := line.substring(1, pos-1) k := line.substring(1, pos-1)
if line[pos+1].is_space then if line[pos+1].is_space then
pos := pos + 1 pos := pos + 1
end end
if line[n] = '%R' then if line[n] = '%R' then
n := n - 1 n := n - 1
end end
val := line.substring (pos + 1, n) val := line.substring (pos + 1, n)
request_header_map.put (val, k) request_header_map.put (val, k)
end end
txt.append (line) txt.append (line)
txt.append_character ('%N') txt.append_character ('%N')
if line.is_empty or else line[1] = '%R' then if line.is_empty or else line[1] = '%R' then
end_of_stream := True end_of_stream := True
else else
a_input.read_line a_input.read_line
end end
end end
end end
analyze_request_line (line: STRING) analyze_request_line (line: STRING)
require require
line /= Void line /= Void and then line.count > 0
local local
pos, next_pos: INTEGER pos, next_pos: INTEGER
do do
print ("%N parse request line:%N" + line) print ("%N parse request line:%N" + line)
pos := line.index_of (' ', 1) pos := line.index_of (' ', 1)
method := line.substring (1, pos - 1) method := line.substring (1, pos - 1)
next_pos := line.index_of (' ', pos+1) next_pos := line.index_of (' ', pos+1)
uri := line.substring (pos+1, next_pos-1) uri := line.substring (pos+1, next_pos-1)
version := line.substring (next_pos + 1, line.count) version := line.substring (next_pos + 1, line.count)
ensure ensure
not_void_method: method /= Void not_void_method: method /= Void
end end
invariant invariant
request_header_attached: request_header /= Void request_header_attached: request_header /= Void
end end