plugin/cerco.ml

   1
   2 type cost_id =
   3   {
   4     cost_id : string;
   5     cost_incr : string;
   6     extern_costs : string Misc.String.Map.t;
   7   }
   8 (** This file makes the interface between the cost plug-in and CerCo's
   9     compiler. *)
  10
  11
  12 let rec read_extern_cost_variables cin =
  13   try
  14     let s = input_line cin in
  15     assert (String.contains s ' ') ;
  16     let i = String.index s ' ' in
  17     assert (String.length s > i + 1) ;
  18     let fun_name = String.sub s 0 i in
  19     let var_name = String.sub s (i+1) (String.length s - (i+1)) in
  20     Misc.String.Map.add fun_name var_name (read_extern_cost_variables cin)
  21   with End_of_file -> Misc.String.Map.empty
  22
  23 (** [multifile_exists exts filename] returns true if and only if the file name
  24     [filename] concatenated with an extension from the list [exts] exists. *)
  25
  26 let multifile_exists exts filename =
  27   let f b ext = b || (Sys.file_exists (filename ^ ext)) in
  28   List.fold_left f false exts
  29
  30 (** [fresh_multifile exts filename] returns a file name whose base is [filename]
  31     and suffixed with an integer such that the result is fresh when concatenated
  32     with any extension from the list [exts]. *)
  33
  34 let fresh_multifile exts filename =
  35   if not (multifile_exists exts filename) then filename
  36   else
  37     let rec aux i =
  38       let new_filename = filename ^ (string_of_int i) in
  39       if not (multifile_exists exts new_filename) then new_filename
  40       else aux (i+1) in
  41     aux 0
  42
  43 (** [index_of e l] returns the index of the element [e] in the list [l], if
  44     any. *)
  45
  46 let index_of e l =
  47   let f (i, res) e' =
  48     let res' = if e' = e then Some i else res in
  49     (i+1, res') in
  50   match snd (List.fold_left f (0, None) l) with
  51     | None -> raise (Failure "Cerco.index_of")
  52     | Some i -> i
  53
  54 let acc_option lustre_option lustre_verify_option lustre_test_option =
  55   if lustre_verify_option || lustre_test_option then "-remove-lustre-externals "
  56   else
  57     if lustre_option then "-lustre "
  58     else ""
  59
  60 (** [apply (filename, _)] apply CerCo's compiler on the file [filename]. The
  61     result is a new C file with cost annotations, the name of the cost
  62     variable, and the name of the cost update function. *)
  63
  64 let apply acc_name lustre_option lustre_verify_option lustre_test_option
  65     user_output_filename
  66     (filename, _) =
  67   let annotated_ext = "-instrumented.c" in
  68   let asm_ext = ".s" in
  69   let cerco_ext = ".cerco" in
  70   let cerco_stack_ext = ".stack_cerco" in
  71   let hex_ext = ".hex" in
  72   let exts =
  73     [annotated_ext ; asm_ext ; cerco_ext ; cerco_stack_ext ; hex_ext] in
  74   let tmp_filename =
  75     if user_output_filename <> "" then user_output_filename else
  76       let tmp_filename = Filename.chop_extension filename in
  77       fresh_multifile exts tmp_filename in
  78   let acc_option =
  79     acc_option lustre_option lustre_verify_option lustre_test_option in
  80   let com_acc =
  81     Printf.sprintf "%s -a %s -o %s %s"
  82       acc_name acc_option tmp_filename filename in
  83   let ext_tmp_filename ext = tmp_filename ^ ext in
  84   let tmp_filenames = List.map ext_tmp_filename exts in
  85   let index_of s = List.nth tmp_filenames (index_of s exts) in
  86   let c_tmp_filename = index_of annotated_ext in
  87   let s_tmp_filename = index_of asm_ext in
  88   let cerco_tmp_filename = index_of cerco_ext in
  89   let cerco_stack_tmp_filename = index_of cerco_stack_ext in
  90   (* let hex_tmp_filename = index_of hex_ext in *)
  91   let rm () =
  92     let com =
  93       "rm -rf " ^ s_tmp_filename ^ " " ^
  94         (if lustre_test_option then "" else cerco_tmp_filename)
  95     (* ^ " " ^ hex_tmp_filename *) in
  96     ignore (Sys.command com) in
  97   if Sys.command com_acc <> 0 then
  98     (rm () ; failwith "Error calling acc.")
  99   else
 100     (let (_, file) = Frontc.parse c_tmp_filename () in
 101      let time =
 102        let cin = open_in cerco_tmp_filename in
 103        let cost_id = input_line cin in
 104        let cost_incr = input_line cin in
 105        let extern_cost_variables = read_extern_cost_variables cin in
 106        close_in cin ;
 107       {cost_id = cost_id; cost_incr = cost_incr;
 108        extern_costs = extern_cost_variables} in
 109      let stack =
 110        try
 111          let cin = try open_in cerco_stack_tmp_filename with _ -> raise Exit in
 112          let cost_stack_id = input_line cin in
 113          let cost_stack_max_id = input_line cin in
 114          let cost_stack_incr = input_line cin in
 115          let extern_cost_stack_variables = read_extern_cost_variables cin in
 116          close_in cin ;
 117          Some ({cost_id = cost_stack_max_id; cost_incr = cost_stack_incr;
 118                 extern_costs = extern_cost_stack_variables},
 119                cost_stack_id)
 120        with Exit -> None in
 121      rm () ;
 122      (file, c_tmp_filename, time, stack))