plugin/cost.ml

   1 (**************************************************************************)
   2 (*                                                                        *)
   3 (*  This file is part of Frama-C.                                         *)
   4 (*                                                                        *)
   5 (*  Copyright (C) 2007-2011                                               *)
   6 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
   7 (*         alternatives)                                                  *)
   8 (*                                                                        *)
   9 (*  you can redistribute it and/or modify it under the terms of the GNU   *)
  10 (*  Lesser General Public License as published by the Free Software       *)
  11 (*  Foundation, version 2.1.                                              *)
  12 (*                                                                        *)
  13 (*  It is distributed in the hope that it will be useful,                 *)
  14 (*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
  15 (*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
  16 (*  GNU Lesser General Public License for more details.                   *)
  17 (*                                                                        *)
  18 (*  See the GNU Lesser General Public License version 2.1                 *)
  19 (*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
  20 (*                                                                        *)
  21 (**************************************************************************)
  22
  23 (** This is the main module of the plug-in. It makes itself available in
  24     Frama-C and apply the cost synthesis on every input file. *)
  25
  26
  27 module Self =
  28   Plugin.Register
  29     (struct
  30       let name = "cost synthesis"
  31       let shortname = "cost"
  32       let module_name = "Cost.Self"
  33       let help = "synthesis of the execution cost of each function"
  34       let is_dynamic = true
  35      end)
  36
  37
  38 module Enabled = Self.False
  39   (struct
  40     let module_name = "Cost.Enabled"
  41     let option_name = "-cost"
  42     let help = "makes a synthesis of the execution cost of each function"
  43     let kind = `Tuning
  44    end)
  45
  46 module Lustre = Self.False
  47   (struct
  48     let option_name = "-cost-lustre"
  49     let help = "input file is a Lustre file"
  50     let kind = `Tuning
  51    end)
  52
  53 module Lustre_verify = Self.False
  54   (struct
  55     let option_name = "-cost-lustre-verify"
  56     let help =
  57       "input file is a Lustre file, verification of the results requested"
  58     let kind = `Tuning
  59    end)
  60
  61 module Lustre_test = Self.False
  62   (struct
  63     let option_name = "-cost-lustre-test"
  64     let help =
  65       "input file is a Lustre file, testing of the results requested"
  66     let kind = `Tuning
  67    end)
  68
  69 module Old_computation = Self.False
  70   (struct
  71     let option_name = "-cost-old-computation"
  72     let help =
  73       "Compute the cost formula by the old way"
  74     let kind = `Tuning
  75    end)
  76
  77 module Output_suffix = Self.String
  78   (struct
  79     let option_name = "-cost-output"
  80     let help =
  81       "Choose the prefix to output the annotation (without -annotated.c)"
  82     let kind = `Tuning
  83     let arg_name = ""
  84     let default = ""
  85    end)
  86
  87 module Acc_prog = Self.String
  88   (struct
  89     let option_name = "-cost-acc"
  90     let help =
  91       "Specify which program must be used for annotation (default: acc)"
  92     let kind = `Tuning
  93     let arg_name = ""
  94     let default = "acc"
  95    end)
  96
  97 module Already_instrumented = Self.False
  98   (struct
  99     let option_name = "-cost-already-instrumented"
 100     let help = "input file is already instrumented"
 101     let kind = `Tuning
 102    end)
 103
 104
 105 (** The main function: apply CerCo's compiler and the cost synthesis on each
 106     input file. *)
 107
 108 (** Save file *)
 109 let save_file fname =
 110   Kernel.CodeOutput.set fname ;
 111   File.pretty_ast ()
 112
 113 let run () =
 114   if Enabled.get () then
 115     let lustre_option = Lustre.get () in
 116     let lustre_verify_option = Lustre_verify.get () in
 117     let lustre_test_option = Lustre_test.get () in
 118     let acc_name = Acc_prog.get () in
 119     let user_output_filename = Output_suffix.get () in
 120     let debug = Self.Debug.get () <> 0 in
 121     Compute.debug := debug;
 122     Parameters.debug := debug;
 123     let files : Cabs.file list = Ast.UntypedFiles.get () in
 124     let run_one ((f_name,_) as file) =
 125       let (_,new_name,_,_) as file =
 126         if Already_instrumented.get () then
 127           let default_time = { Cerco.cost_id = "__cost";
 128                                cost_incr = "__cost_incr";
 129                                extern_costs = Misc.String.Map.empty;
 130                              } in
 131           let default_stack_max = Some ({ Cerco.cost_id = "__stack_size_max";
 132                                           cost_incr = "__stack_size_incr";
 133                                           extern_costs = Misc.String.Map.empty;
 134                                         },"__stack_size") in
 135           let new_name =
 136             (if user_output_filename <> "" then user_output_filename else
 137                 (Filename.chop_extension f_name))^"-annotated.c" in
 138           (file,new_name,default_time,default_stack_max)
 139         else
 140           let (((fname,_),_,_,_) as file) = Cerco.apply
 141             acc_name lustre_option lustre_verify_option lustre_test_option
 142             user_output_filename file in
 143           Kernel.Files.set [fname] ;
 144           File.init_from_cmdline () ;
 145           file
 146       in
 147       if Old_computation.get ()
 148       then Compute.cost file
 149       else begin
 150         save_file "toto1.c";
 151         if debug then Printf.printf "Make CFG\n%!" ;
 152         Compute_simple.make_CFG () ;
 153         save_file "toto2.c";
 154         if debug then Compute_simple.print_CFG () ;
 155         Compute_simple.cost file;
 156         Compute_simple_stack_size.cost file;
 157         Simplify_terms.add_def_max_logic_info ();
 158         if debug then Printf.printf "Save file\n%!" ;
 159         save_file new_name
 160       end in
 161     List.iter run_one files
 162
 163 let () = Db.Main.extend run