indexing
	description:
		"[
			Verifier which handles the interaction with Boogie.
		]"
	date: "$Date$"
	revision: "$Revision$"

class EP_VERIFIER

inherit

	SHARED_EP_ENVIRONMENT
		export {NONE} all end

	SHARED_WORKBENCH
		export {NONE} all end

create
	make

feature {NONE} -- Initialization

	make
			-- Initialize verifier.
		do
			create {LINKED_LIST [TUPLE [name: STRING; content: STRING]]} verification_content.make
			create boogie_output.make_empty
		end

feature -- Access

	verification_content: !LIST [TUPLE [name: STRING; content: STRING]]
			-- Boogie code to verify

feature -- Element change

	add_file_content (a_file_name: !STRING)
			-- Add Boogie code file denoted by `a_file_name' to verifier.
		local
			a_file: PLAIN_TEXT_FILE
			l_error: EP_GENERAL_ERROR
		do
			create a_file.make (a_file_name)
			try_open_file (a_file)
			if a_file.is_open_read then
				a_file.read_stream (a_file.count)
				verification_content.extend (["File: " + a_file_name, a_file.last_string])
				a_file.close
			else
				verification_content.extend ([a_file_name, "// Error: Unable to open file " + a_file_name])

				create l_error.make (names.error_file_not_found)
				l_error.set_description (names.description_file_not_found (a_file_name))
				errors.extend (l_error)
			end
		ensure
			file_content_added: verification_content.count = old verification_content.count + 1
		end

	add_string_content (a_content: !STRING; a_content_name: !STRING)
			-- Add Boogie code in `a_content' to verifier.
		do
			verification_content.extend ([a_content_name, a_content])
		ensure
			string_content_added: verification_content.count = old verification_content.count + 1
		end

	add_buffer_content (a_content: !EP_OUTPUT_BUFFER; a_content_name: !STRING)
			-- Add Boogie code in `a_content' to verifier.
		do
			verification_content.extend ([a_content_name, a_content.string])
		ensure
			string_content_added: verification_content.count = old verification_content.count + 1
		end

feature -- Basic operations

	reset
			-- Reset verifier.
		do
			verification_content.wipe_out
			boogie_output.wipe_out
		end

	verify
			-- Do verification.
		do
			generate_boogie_file
			launch_boogie
			evaluate_boogie_output
		end

feature {NONE} -- Implementation

	generate_boogie_file
			-- Generate a Boogie code file from all added content.
		local
			l_output_file: KL_TEXT_OUTPUT_FILE
			l_error: EP_GENERAL_ERROR
		do
			create l_output_file.make (boogie_output_file_name)
			l_output_file.recursive_open_write
			if not l_output_file.is_open_write then
				create l_error.make (names.error_file_not_writable)
				l_error.set_description (names.description_file_not_writable (boogie_output_file_name))
				errors.extend (l_error)
			else
				create boogie_input.make_empty
				boogie_input.append ("// Automatically generated by EVE Proofs%N%N")
				from
					verification_content.start
				until
					verification_content.after
				loop
					boogie_input.append ("// ===========================================================================%N")
					boogie_input.append ("// " + verification_content.item.name + "%N")
					boogie_input.append ("// ===========================================================================%N%N")
					boogie_input.append (verification_content.item.content)
					boogie_input.append_character ('%N')
					boogie_input.append_character ('%N')

					verification_content.forth
				end

				l_output_file.put_string (boogie_input)
				l_output_file.close
			end
		end

	launch_boogie
			-- Launch Boogie on output file.
		local
			l_ee: EXECUTION_ENVIRONMENT
			l_arguments: LINKED_LIST [STRING]
			l_process_factory: PROCESS_FACTORY
			l_process: PROCESS
		do
			create l_ee
				-- Prepare command line arguments
			create l_arguments.make
			l_arguments.extend ("/trace")
			l_arguments.extend (boogie_output_file_name)

			create l_process_factory
			l_process := l_process_factory.process_launcher ("boogie", l_arguments, l_ee.current_working_directory)

			l_process.redirect_output_to_agent (agent handle_boogie_output (?))
			l_process.redirect_error_to_same_as_output
			l_process.set_on_fail_launch_handler (agent handle_launch_failed)
			l_process.launch
			l_process.wait_for_exit
		end

	handle_boogie_output (a_output: STRING)
			-- Handle output from Boogie.
		do
			boogie_output.append (a_output)
		end

	handle_launch_failed
			-- Handle launch of Boogie failed.
		local
			l_error: EP_GENERAL_ERROR
		do
			create l_error.make (names.error_launching_boogie_failed)
			l_error.set_description (names.description_launching_boogie_failed)
			errors.extend (l_error)
		end

	evaluate_boogie_output
			-- Evaluate Boogie output stored in `boogie_output'.
		local
			l_boogie_output_parser: EP_BOOGIE_OUTPUT_PARSER
		do
			create l_boogie_output_parser.make (boogie_input, boogie_output)
			l_boogie_output_parser.parse
		end

feature {NONE} -- Implementation

	boogie_input: STRING
			-- Input for Boogie

	boogie_output: STRING
			-- Output from Boogie execution

	boogie_output_file_name: STRING
			-- Output file name for Boogie code file
		local
			l_output_path: FILE_NAME
		do
			create l_output_path.make_from_string (system.eiffel_project.project_directory.target_path)
			l_output_path.extend ("Boogie")
			l_output_path.extend ("output.bpl")
			Result := l_output_path

				-- TODO: remove this to use the EIFGENs directory
			Result := "C:\Temp\output.bpl"
		end

	try_open_file (a_file: PLAIN_TEXT_FILE)
			-- Try to open the file.
		local
			l_retry: BOOLEAN
		do
			if not l_retry then
				a_file.open_read
			end
		rescue
			l_retry := True
			retry
		end

end