source: Deliverables/D2.2/8051/src/clight/clightLustreMain.ml @ 3673

Last change on this file since 3673 was 1490, checked in by ayache, 8 years ago

Function pointers fixed.

File size: 6.9 KB
Line 
1
2let error_prefix = "Clight-Lustre main"
3let error s = Error.global_error error_prefix s
4
5
6let 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
45let 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
58let 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
68let 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
76let 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
90let 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
95let init_fields ctx fields =
96  let f res field = res ^ (first_init_field ctx field) in
97  List.fold_left f "" fields
98
99let 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
111let 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
119let 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  init_inputs ^
146  "    for (i_cycle = 0 ; i_cycle < " ^ (string_of_int lustre_test_cycles) ^
147    " ; i_cycle++) {\n" ^
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
170let 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 tmp_file
186  with Sys_error _ ->
187    error ("could not save temporary file " ^ tmp_file ^ " with main.")
188
189
190let 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
Note: See TracBrowser for help on using the repository browser.