let error_prefix = "Main"
let error = Error.global_error error_prefix


let log_file = Filename.temp_file "log" ""


let print_verbose i s =
  if Options.get_verbose_level () >= i then Printf.printf "%s%!" s
let print_verbose1 = print_verbose 1
let print_verbose2 = print_verbose 2


let exec cmd error_callback error_msg success_callback success_msg =
  print_verbose2 ("  -> executing command \"" ^ cmd ^ "\"...\n") ;
  let res = Sys.command cmd in
  if res <> 0 then (error_callback () ; error error_msg)
  else
    (print_verbose1 (success_msg ^ "\n") ;
     success_callback ())


let has_extension filename =
  try ignore (Filename.chop_extension filename) ; true
  with Invalid_argument ("Filename.chop_extension") -> false

let lustre_compilation filename node =
  print_verbose1
    ("Compiling node " ^ node ^ " of Lustre file " ^ filename ^ "...\n") ;
  let filename_quote = Filename.quote filename in
  let base =
    if has_extension filename then Filename.chop_extension filename
    else filename in
  let base =
    Misc.fresh_base base
      [".c" ; "-annotated.c" ; ".s" ; ".hex" ; ".cerco" ; ".cost_results" ;
       ".jessie_results" ; "-annotated_test.c" ; "-annotated_test.s" ;
       "-annotated_test.hex" ; "-annotated_test.results"] in
  let res_file = base ^ ".c" in
  let res_file_quote = Filename.quote res_file in
  let cmd =
    "lus2c " ^ filename_quote ^ " " ^ node ^ " -o " ^ res_file_quote ^ " >> " ^
      log_file in
  let error_callback () = () in
  let error_msg =
    "Failed to compile node " ^ node ^ " of Lustre file " ^ filename ^ "." in
  let success_callback () = res_file in
  let success_msg = "Done. Result is in file " ^ res_file ^ "." in
  exec cmd error_callback error_msg success_callback success_msg


let extract_inputs_booleans filename =
  print_verbose1
    ("Extracting boolean inputs from file " ^ filename ^ "...\n") ;
  try
    let ic = open_in filename in
    let rec inputs_booleans b =
      try
	let str_inputs = Str.regexp " *//INPUTS *" in
	(* let str_registers = Str.regexp " *//REGISTERS *" in *)
	let is_input_start s =
	  Str.string_match str_inputs s 0
	  (* || Str.string_match str_registers s 0 *) in
	let str_outputs = Str.regexp " *//OUTPUTS *" in
	let str_acc = Str.regexp ".*}.*" in
	let is_input_end s =
	  Str.string_match str_outputs s 0 ||
	  Str.string_match str_acc s 0 in
	let str_boolean = Str.regexp "   _boolean .*;" in
	let str_input = Str.regexp "   [^ ]* .*;" in
	let extract_input s =
	  let i = String.index_from s 3 ' ' in
	  String.sub s (i+1) (String.length s - (i+2)) in
	let s = input_line ic in
	let (added_input, added_boolean) =
	  let extract cond = if b && cond then [extract_input s] else [] in
	  (extract (Str.string_match str_input s 0),
	   extract (Str.string_match str_boolean s 0)) in
	let next_b = (b || (is_input_start s)) && (not (is_input_end s)) in
	let (inputs, booleans) = inputs_booleans next_b in
	(added_input @ inputs, added_boolean @ booleans)
      with End_of_file -> close_in ic ; ([], []) in
    let res = inputs_booleans false in
    print_verbose1 "Done.\n" ;
    res
  with Sys_error _ ->
    error ("Could not extract boolean inputs from file " ^ filename ^ ".")


let framac_option () =
  "-cost-lustre " ^
    (if Options.test_requested () then "-cost-lustre-test " else "") ^
    (if Options.verify_requested () then "-cost-lustre-verify " else "")

let cost_plugin filename =
  print_verbose1 ("Running Cost plug-in on file " ^ filename ^ "...\n") ;
  let filename_quote = Filename.quote filename in
  let base =
    if has_extension filename then Filename.chop_extension filename
    else filename in
  let annotated_file = base ^ "-annotated.c" in
  let results_file = base ^ ".cost_results" in
  let hex_file = base ^ ".hex" in
  let cerco_file = base ^ ".cerco" in
  let option = framac_option () in
  let cmd = "frama-c -cost " ^ option ^ filename_quote ^ " >> " ^
      log_file in
  let error_callback () = () in
  let error_msg = "Failed to run Cost plug-in on file " ^ filename ^ "." in
  let success_callback () = (annotated_file, results_file, cerco_file) in
  let success_msg =
    "Done. Annotations are in file " ^ annotated_file ^
      ", object code is in file " ^ hex_file ^
      ", cost results are in file " ^ results_file ^
      (if Options.test_requested () then
	  ", CerCo information is in file " ^ cerco_file
       else "") ^
      "." in
  exec cmd error_callback error_msg success_callback success_msg


let print_step_result filename =
  print_verbose1 ("Reading the cost results in file " ^ filename ^ "...\n") ;
  let ic = open_in filename in
  let rec aux () =
    try
      let s = input_line ic in
      if String.contains s ' ' then
	let i = String.index s ' ' in
	let fun_name = String.sub s 0 i in
	let cost = String.sub s (i+1) ((String.length s) - (i+1)) in
	let suffix = "_step" in
	let l = String.length fun_name in
	let l' = String.length suffix in
	if l > l' && String.sub s (l - l') l' = suffix then
	  (print_verbose1 "Done.\n" ;
	   Printf.printf
	     "WCET of %s: %s (not verified).\n%!"
	     fun_name cost ;
	   (fun_name, cost))
	else aux ()
      else error ("Bad format of result file " ^ filename ^ ".")
    with End_of_file ->
      error "No step function found or its cost could not be computed." in
  aux ()


let prover () =
  if Options.gui_requested () then ""
  else "-jessie-atp " ^ (Options.get_prover ()) ^ " "

let jessie filename =
  print_verbose1 ("Running Frama-C/Jessie on file " ^ filename ^ "...\n") ;
  let filename_quote = Filename.quote filename in
  let base =
    if has_extension filename then Filename.chop_extension filename
    else filename in
  let res_file = base ^ ".jessie_results" in
  let timeout = string_of_int (Options.get_timeout ()) in
  let cmd =
    "TIMEOUT=" ^ timeout ^ " frama-c -jessie -jessie-behavior default " ^
    "-jessie-why-opt=\"-fast-wp\" " ^ (prover ()) ^
    filename_quote ^ " >> " ^ res_file in
  let error_callback () = () in
  let error_msg = "Failed to run Frama-C/Jessie on file " ^ filename ^ "." in
  let success_callback () = res_file in
  let success_msg = "Done. Results are in file " ^ res_file ^ "." in
  exec cmd error_callback error_msg success_callback success_msg

let string_starts_with prefix s =
  let l = String.length prefix in
  (l <= String.length s) && (String.sub s 0 l = prefix)

let read_jessie_results filename =
  if not (Options.gui_requested ()) then
    begin
      print_verbose1
	("Reading Frama-C/Jessie results in file " ^ filename ^ "...\n" ) ;
      let print_failed () = Printf.printf "Failed to prove the result.\n%!" in
      try
	let ic = open_in filename in
	let rec aux () =
	  let s = input_line ic in
	  if string_starts_with "valid" s then
	    let regexp = Str.regexp (".*100%.*") in
	    if Str.string_match regexp s 0 then
	      (print_verbose1 "Done.\n" ;
	       Printf.printf "WCET is proven correct.\n%!")
	    else print_failed ()
	  else aux () in
	aux ()
      with Sys_error _ | End_of_file -> print_failed ()
    end

let verification filename =
  Printf.printf "Verifying the result (this may take some time)...\n%!" ;
  let res_file = jessie filename in
  read_jessie_results res_file


let cerco_test_info (inputs, booleans) step_fun step_cost cerco_file =
  print_verbose1
    ("Adding step function information to CerCo file " ^ cerco_file ^ "...\n") ;
  try
    let ic = open_in cerco_file in
    let rec contents () =
      try let s = input_line ic in s ^ "\n" ^ (contents ())
      with End_of_file -> close_in ic ; "" in
    let contents = step_fun ^ "\n" ^ step_cost ^ "\n" ^ contents () ^ "\n" in
    let f contents s = contents ^ s ^ "\n" in
    let contents = (List.fold_left f contents inputs) ^ "\n" in
    let contents = List.fold_left f contents booleans in
    let oc = open_out cerco_file in
    output_string oc contents ;
    close_out oc ;
    print_verbose1 "Done.\n" ;
    cerco_file
  with Sys_error _ ->
    error ("Could not add step function information to CerCo file " ^
	      cerco_file ^ ".")

let cerco_test_file filename cerco_test_info =
  print_verbose1 ("Adding a main to file " ^ filename ^ "...\n") ;
  let filename_quote = Filename.quote filename in
  let base =
    if has_extension filename then Filename.chop_extension filename
    else filename in
  let res_base = base ^ "_test" in
  let res_c = res_base ^ ".c" in
  let cmd =
    "acc -o " ^ res_base ^ " -lustre-test " ^ cerco_test_info ^
      " -lustre-test-cases " ^ (string_of_int (Options.get_test_cases ())) ^
      " -lustre-test-cycles " ^ (string_of_int (Options.get_test_cycles ())) ^
      " -lustre-test-min-int " ^ (string_of_int (Options.get_test_min_int ())) ^
      " -lustre-test-max-int " ^ (string_of_int (Options.get_test_max_int ())) ^
      " " ^ filename_quote ^ " >> " ^ log_file in
  let error_callback () = () in
  let error_msg = "Failed to add a main to file " ^ filename ^ "." in
  let success_callback () = res_c in
  let success_msg = "Done. Result is in files " ^ res_c ^ "." in
  exec cmd error_callback error_msg success_callback success_msg

let test_exec filename =
  print_verbose1 ("Simulating the generated code in file " ^ filename ^
		  "...\n") ;
  let filename_quote = Filename.quote filename in
  let base =
    if has_extension filename then Filename.chop_extension filename
    else filename in
  let res_file = base ^ ".results" in
  let cmd = "acc -l Clight -i " ^ filename_quote ^ " > " ^ res_file in
  let error_callback () = () in
  let error_msg = "Failed to run acc on file " ^ filename ^ "." in
  let success_callback () = res_file in
  let success_msg = "Done. Results are in file " ^ res_file ^ "." in
  exec cmd error_callback error_msg success_callback success_msg

let read_test_results filename =
  print_verbose1
    ("Reading simulation results in file " ^ filename ^ "...\n" ) ;
  try
    let ic = open_in filename in
    Misc.repeat 2 (fun () -> ignore (input_line ic)) () ;
    let wcet = int_of_string (input_line ic) in
    let min = int_of_string (input_line ic) in
    let max = int_of_string (input_line ic) in
    let average = int_of_string (input_line ic) in
    let wcet_correct = max <= wcet in
    print_verbose1 "Done.\n" ;
    Printf.printf "Estimated WCET: %d\nMinimum: %d\nMaximum: %d\nAverage: %d\nEstimated WCET is %scorrect for these executions.\n%!"
      wcet min max average (if wcet_correct then "" else "in")
  with Sys_error _ | End_of_file | Failure "int_of_string" ->
    error "Failed to test the result."

let test filename inputs_booleans step_fun step_cost cerco_file =
  Printf.printf "Testing the result (this may take some time)...\n%!" ;
  let cerco_test_info =
    cerco_test_info inputs_booleans step_fun step_cost cerco_file in
  let cerco_test_file = cerco_test_file filename cerco_test_info in
  let test_results = test_exec cerco_test_file in
  read_test_results test_results


let _ =
  let args = OptionsParsing.results () in
  if List.length args < 2 then error OptionsParsing.usage_msg
  else
    begin
      let lustre_file = List.nth args 0 in
      let node = List.nth args 1 in
      print_verbose1
	("*** Processing node " ^ node ^ " of Lustre file " ^ lustre_file ^
	 ". ***\n") ;
      let c_file = lustre_compilation lustre_file node in
      let inputs_booleans = extract_inputs_booleans c_file in
      let (c_annotated_file, cost_results_file, cerco_file) =
	cost_plugin c_file in
      let (step_fun, step_cost) = print_step_result cost_results_file in
      if Options.verify_requested () then verification c_annotated_file ;
      if Options.test_requested () then
	test c_annotated_file inputs_booleans step_fun step_cost cerco_file ;
    end