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

class EP_BOOGIE_VERIFIER

inherit

	SHARED_EP_ENVIRONMENT
		export {NONE} all end

	SHARED_WORKBENCH
		export {NONE} all end

	EIFFEL_LAYOUT
		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_input.make_empty
			create boogie_output.make_empty
		ensure
			is_reset: is_reset
		end

feature -- Access

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

feature -- Status report

	is_reset: BOOLEAN
			-- Is verifier reset for another verification?
		do
			Result := boogie_input.is_empty and boogie_output.is_empty
		end

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_input.wipe_out
			boogie_output.wipe_out


			-- TODO: move someplace else
			if {l_feature: !FEATURE_I} system.any_class.compiled_class.feature_named ("default_create") then
				feature_list.mark_creation_routine_as_generated (l_feature)
			else
				check false end
			end
			type_list.mark_type_as_generated (system.any_type)
		ensure
			is_reset: is_reset
		end

	verify
			-- Do verification.
		require
			is_reset: is_reset
		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_code_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_code_file_name))
				errors.extend (l_error)
			else
				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
--			l_registry: WEL_REGISTRY
--			l_registry_value: WEL_REGISTRY_KEY_VALUE
			l_executable: STRING
			l_error: EP_GENERAL_ERROR
			l_path_string: STRING
			l_path: DIRECTORY_NAME
			l_file_name: FILE_NAME
			l_file: RAW_FILE
		do
				-- Prepare command line arguments
			create l_arguments.make
			l_arguments.extend ("/trace")
			l_arguments.extend (boogie_code_file_name)

				-- Find Boogie executable

				-- 1. Look in preferences
			l_executable := preferences.boogie_executable

				-- 2. Look in deliversy
			if l_executable.is_empty then
				l_path := eiffel_layout.shared_application_path.twin
				l_path.extend ("tools")
				l_path.extend ("boogie")
				l_path.extend ("bin")
				create l_file_name.make
				l_file_name.set_directory (l_path.string)
				l_file_name.set_file_name ("Boogie.exe")
				create l_file.make (l_file_name.string)
				if l_file.exists then
					l_executable := l_file_name.string
				end
			end

				-- 2.1. Delivery of development version
			if l_executable.is_empty then
				create l_ee
				l_path_string := l_ee.get("EIFFEL_SRC") + "/Delivery/studio/tools/boogie/bin/Boogie.exe"
				create l_file.make (l_path_string)
				if not l_file.exists then
					l_path_string := l_ee.get("EIFFEL_SRC") + "/../Delivery/studio/tools/boogie/bin/Boogie.exe"
					create l_file.make (l_path_string)
				end

				if l_file.exists then
					l_executable := l_path_string
				end
			end

				-- 3. Windows only: Look in registry
--			if l_executable.is_empty and {PLATFORM}.is_windows then
--				create l_registry
--				l_registry_value := l_registry.open_key_value ("HKEY_LOCAL_MACHINE\SOFTWARE\Microsoft\SpecSharp", "InstallDir")
--				if l_registry_value /= Void then
--					l_executable := l_registry_value.string_value + "Boogie.exe"
--				end
--			end

				-- 4. Just launch it an hope for the best (i.e. it's in the PATH)
			if l_executable.is_empty then
				l_executable := "Boogie.exe"
			end

			if {PLATFORM}.is_unix then
					-- On Linux, run Boogie via Mono
				l_arguments.put_front (l_executable)
				l_executable := "mono"
			end

				-- Launch Boogie
			create l_ee
			create l_process_factory
			l_process := l_process_factory.process_launcher (l_executable, 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_executable, l_arguments))
			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 (a_executable: STRING; a_arguments: LINKED_LIST [STRING])
			-- Handle launch of Boogie failed.
		local
			l_error: EP_GENERAL_ERROR
		do
			create l_error.make (names.error_launching_boogie_failed)
				-- TODO: provide better help with executable
			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_code_file_name: STRING
			-- 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
			if {PLATFORM}.is_windows then
				Result := "C:\Temp\output.bpl"
			elseif {PLATFORM}.is_unix then
				Result := "/var/tmp/output.bpl"
			end
		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