]> matita.cs.unibo.it Git - pkg-cerco/acc.git/blob - src/clight/clightLustreMain.ml
Package description and copyright added.
[pkg-cerco/acc.git] / 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