src/clight/clightLustreMain.ml

   1
   2 let error_prefix = "Clight-Lustre main"
   3 let error s = Error.global_error error_prefix s
   4
   5
   6 let extract_info lustre_test =
   7   let error () = error ("bad format of file " ^ lustre_test) in
   8   try
   9     let ic = open_in lustre_test in
  10     let step_fun = input_line ic in
  11     let step_cost = input_line ic in
  12     let cost_var = input_line ic in
  13     let cost_incr = input_line ic in
  14     let rec aux_external_costs () =
  15       try
  16         let s = input_line ic in
  17         if s = "" then StringTools.Map.empty
  18         else
  19           if String.contains s ' ' then
  20             let i = String.index s ' ' in
  21             let extern_name = String.sub s 0 i in
  22             let cost = String.sub s (i+1) ((String.length s) - (i+1)) in
  23             StringTools.Map.add extern_name cost (aux_external_costs ())
  24           else error ()
  25       with End_of_file -> error () in
  26     let rec aux_inputs () =
  27       try
  28         let s = input_line ic in
  29         if s = "" then []
  30         else s :: (aux_inputs ())
  31       with End_of_file -> error () in
  32     let rec aux_booleans () =
  33       try
  34         let s = input_line ic in
  35         s :: (aux_booleans ())
  36       with End_of_file -> [] in
  37     let external_costs = aux_external_costs () in
  38     let inputs = aux_inputs () in
  39     let booleans = aux_booleans () in
  40     (booleans, inputs, step_fun, step_cost,
  41      cost_var, cost_incr, external_costs)
  42   with Sys_error _ | End_of_file -> error ()
  43
  44
  45 let define_void_external cost_incr arg_types ret_type cost_var =
  46   let fresh = StringTools.make_fresh StringTools.Set.empty "x" in
  47   let fn_return = ret_type in
  48   let fn_params = List.map (fun t -> (fresh (), t)) arg_types in
  49   let fn_vars = [] in
  50   let int_type = Clight.Tint (Clight.I32, AST.Signed) in
  51   let f_type = Clight.Tfunction ([int_type], Clight.Tvoid) in
  52   let f = Clight.Expr (Clight.Evar cost_incr, f_type) in
  53   let args = [Clight.Expr (Clight.Evar cost_var, int_type)] in
  54   let fn_body = Clight.Scall (None, f, args) in
  55   { Clight.fn_return = fn_return ; Clight.fn_params = fn_params ;
  56     Clight.fn_vars = fn_vars ; Clight.fn_body = fn_body }
  57
  58 let define_void_externals_funct cost_incr external_costs (id, def) =
  59   let def' = match def with
  60     | Clight.External (_, args, Clight.Tvoid)
  61         when StringTools.Map.mem id external_costs ->
  62       Clight.Internal
  63         (define_void_external cost_incr args Clight.Tvoid
  64            (StringTools.Map.find id external_costs))
  65     | _ -> def in
  66   (id, def')
  67
  68 let define_void_externals cost_incr external_costs p =
  69   let prog_funct =
  70     List.map
  71       (define_void_externals_funct cost_incr external_costs)
  72       p.Clight.prog_funct in
  73   { p with Clight.prog_funct = prog_funct }
  74
  75
  76 let get_struct_arg fun_name p =
  77   let error () =
  78     error ("could not fetch the structure of the context of function " ^
  79               fun_name ^ ".") in
  80   if List.mem_assoc fun_name p.Clight.prog_funct then
  81     match List.assoc fun_name p.Clight.prog_funct with
  82       | Clight.Internal def when List.length def.Clight.fn_params = 1 ->
  83         (match snd (List.hd def.Clight.fn_params) with
  84           | Clight.Tpointer (Clight.Tstruct (struct_name, fields)) ->
  85             (struct_name, fields)
  86           | _ -> error ())
  87       | _ -> error ()
  88   else error ()
  89
  90 let first_init_field ctx (id, t) = match t with
  91   | Clight.Tint _ -> ctx ^ "." ^ id ^ " = 0;\n"
  92   | _ when id = "client_data" -> ""
  93   | _ -> error ("unsupported type " ^ (ClightPrinter.string_of_ctype t) ^ ".")
  94
  95 let init_fields ctx fields =
  96   let f res field = res ^ (first_init_field ctx field) in
  97   List.fold_left f "" fields
  98
  99 let init_field
 100     lustre_test_min_int lustre_test_max_int booleans inputs ctx (id, t) =
 101   let lustre_full_range = (lustre_test_max_int - lustre_test_min_int) + 1 in
 102   match t with
 103     | Clight.Tint _ when List.mem id inputs && List.mem id booleans ->
 104       ctx ^ "." ^ id ^ " = rand_bool();\n"
 105     | Clight.Tint _ when List.mem id inputs ->
 106       ctx ^ "." ^ id ^ " = rand_int(" ^ (string_of_int lustre_full_range) ^
 107         ") - " ^ (string_of_int lustre_test_min_int) ^ ";\n"
 108     | _ when id = "client_data" || not (List.mem id inputs) -> ""
 109     | _ -> error ("unsupported type " ^ (ClightPrinter.string_of_ctype t) ^ ".")
 110
 111 let main_fields
 112     lustre_test_min_int lustre_test_max_int booleans inputs ctx fields =
 113   let f res field =
 114     res ^
 115       (init_field
 116          lustre_test_min_int lustre_test_max_int booleans inputs ctx field) in
 117   List.fold_left f "" fields
 118
 119 let main_def
 120     lustre_test_cases lustre_test_cycles lustre_test_min_int lustre_test_max_int
 121     (struct_name, fields) booleans inputs step_fun step_cost cost_var =
 122   let ctx = "ctx" in
 123   let reset_fun = Str.global_replace (Str.regexp "_step") "_reset" step_fun in
 124   let big_init = init_fields ctx fields in
 125   let init_inputs =
 126     main_fields lustre_test_min_int lustre_test_max_int booleans inputs ctx
 127       fields in
 128
 129   "int main () {\n" ^
 130   (* Initializations *)
 131   "  " ^ struct_name ^ " " ^ ctx ^ ";\n" ^
 132   "  int wcet = " ^ step_cost ^ ";\n" ^
 133   "  int old_cost;\n" ^
 134   "  int et = 0;\n" ^
 135   "  int min = -1, max = -1, nb_cycles = 0\n;" ^
 136   "  int i_case, i_cycle;\n" ^
 137
 138   (* Body *)
 139   big_init ^
 140   "  for (i_case = 0 ; i_case < " ^ (string_of_int lustre_test_cases) ^
 141     " ; i_case++) {\n" ^
 142   "    old_cost = " ^ cost_var ^ ";\n" ^
 143   "    " ^ reset_fun ^ "(&" ^ ctx ^ ");\n" ^
 144   "    " ^ cost_var ^ " = old_cost;\n" ^
 145   "    for (i_cycle = 0 ; i_cycle < " ^ (string_of_int lustre_test_cycles) ^
 146     " ; i_cycle++) {\n" ^
 147          init_inputs ^
 148   "      old_cost = " ^ cost_var ^ ";\n" ^
 149   "      " ^ step_fun ^ "(&" ^ ctx ^ ");\n" ^
 150   "      et = " ^ cost_var ^ " - old_cost;\n" ^
 151   "      if ((min == -1) || (et < min)) min = et;\n" ^
 152   "      if ((max == -1) || (et > max)) max = et;\n" ^
 153   "      nb_cycles++;\n" ^
 154   "    }\n" ^
 155   "  }\n" ^
 156
 157   (* Printing the results *)
 158   "  print_sint(wcet);\n" ^
 159   "  newline();\n" ^
 160   "  print_sint(min);\n" ^
 161   "  newline();\n" ^
 162   "  print_sint(max);\n" ^
 163   "  newline();\n" ^
 164   "  if (nb_cycles == 0) print_sint(-1);\n" ^
 165   "  else print_sint(" ^ cost_var ^ "/nb_cycles);\n" ^
 166   "  newline();\n" ^
 167   "  return(0);\n" ^
 168   "}\n"
 169
 170 let add_main_def
 171     lustre_test_cases lustre_test_cycles lustre_test_min_int
 172     lustre_test_max_int booleans inputs step_fun step_cost cost_var p =
 173   let tmp_file = Filename.temp_file "lustre_add_main" ".c" in
 174   try
 175     let struct_arg = get_struct_arg step_fun p in
 176     let s =
 177       (ClightPrinter.print_program p) ^
 178       (main_def
 179          lustre_test_cases lustre_test_cycles lustre_test_min_int
 180          lustre_test_max_int struct_arg booleans inputs
 181          step_fun step_cost cost_var) in
 182     let oc = open_out tmp_file in
 183     output_string oc s ;
 184     close_out oc ;
 185     ClightParser.process (`Filename tmp_file)
 186   with Sys_error _ ->
 187     error ("could not save temporary file " ^ tmp_file ^ " with main.")
 188
 189
 190 let add lustre_test lustre_test_cases lustre_test_cycles
 191     lustre_test_min_int lustre_test_max_int  p =
 192   let (booleans, inputs, step_fun, step_cost,
 193        cost_var, cost_incr, external_costs) =
 194     extract_info lustre_test in
 195   let p = define_void_externals cost_incr external_costs p in
 196   add_main_def lustre_test_cases lustre_test_cycles lustre_test_min_int
 197     lustre_test_max_int booleans inputs step_fun step_cost cost_var p