(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2011                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(** This is the main module of the plug-in. It makes itself available in
    Frama-C and apply the cost synthesis on every input file. *)


module Self =
  Plugin.Register
    (struct
      let name = "cost synthesis"
      let shortname = "cost"
      let module_name = "Cost.Self"
      let help = "synthesis of the execution cost of each function"
      let is_dynamic = true
     end)


module Enabled = Self.False
  (struct
    let module_name = "Cost.Enabled"
    let option_name = "-cost"
    let help = "makes a synthesis of the execution cost of each function"
    let kind = `Tuning
   end)
  
module Lustre = Self.False
  (struct
    let option_name = "-cost-lustre"
    let help = "input file is a Lustre file"
    let kind = `Tuning
   end)
  
module Lustre_verify = Self.False
  (struct
    let option_name = "-cost-lustre-verify"
    let help =
      "input file is a Lustre file, verification of the results requested"
    let kind = `Tuning
   end)
  
module Lustre_test = Self.False
  (struct
    let option_name = "-cost-lustre-test"
    let help =
      "input file is a Lustre file, testing of the results requested"
    let kind = `Tuning
   end)

module Old_computation = Self.False
  (struct
    let option_name = "-cost-old-computation"
    let help =
      "Compute the cost formula by the old way"
    let kind = `Tuning
   end)

module Output_suffix = Self.String
  (struct
    let option_name = "-cost-output"
    let help =
      "Choose the prefix to output the annotation (without -annotated.c)"
    let kind = `Tuning
    let arg_name = ""
    let default = ""
   end)

module Acc_prog = Self.String
  (struct
    let option_name = "-cost-acc"
    let help =
      "Specify which program must be used for annotation (default: acc)"
    let kind = `Tuning
    let arg_name = ""
    let default = "acc"
   end)

module Already_instrumented = Self.False
  (struct
    let option_name = "-cost-already-instrumented"
    let help = "input file is already instrumented"
    let kind = `Tuning
   end)


(** The main function: apply CerCo's compiler and the cost synthesis on each
    input file. *)

(** Save file *)
let save_file fname =
  Kernel.CodeOutput.set fname ;
  File.pretty_ast ()

let run () =
  if Enabled.get () then
    let lustre_option = Lustre.get () in
    let lustre_verify_option = Lustre_verify.get () in
    let lustre_test_option = Lustre_test.get () in
    let acc_name = Acc_prog.get () in
    let user_output_filename = Output_suffix.get () in
    let debug = Self.Debug.get () <> 0 in
    Compute.debug := debug;
    Parameters.debug := debug;
    let files : Cabs.file list = Ast.UntypedFiles.get () in
    let run_one ((f_name,_) as file) =
      let (_,new_name,_,_) as file =
        if Already_instrumented.get () then
          let default_time = { Cerco.cost_id = "__cost";
                               cost_incr = "__cost_incr";
                               extern_costs = Misc.String.Map.empty;
                             } in
          let default_stack_max = Some ({ Cerco.cost_id = "__stack_size_max";
                                          cost_incr = "__stack_size_incr";
                                          extern_costs = Misc.String.Map.empty;
                                        },"__stack_size") in
          let new_name =
            (if user_output_filename <> "" then user_output_filename else
                (Filename.chop_extension f_name))^"-annotated.c" in
          (file,new_name,default_time,default_stack_max)
        else
          let (((fname,_),_,_,_) as file) = Cerco.apply
            acc_name lustre_option lustre_verify_option lustre_test_option
            user_output_filename file in
          Kernel.Files.set [fname] ;
          File.init_from_cmdline () ;
          file
      in
      if Old_computation.get ()
      then Compute.cost file
      else begin
        save_file "toto1.c";
        if debug then Printf.printf "Make CFG\n%!" ;
        Compute_simple.make_CFG () ;
        save_file "toto2.c";
        if debug then Compute_simple.print_CFG () ;
        Compute_simple.cost file;
        Compute_simple_stack_size.cost file;
        Simplify_terms.add_def_max_logic_info ();
        if debug then Printf.printf "Save file\n%!" ;
        save_file new_name
      end in
    List.iter run_one files

let () = Db.Main.extend run