Revision e2380d4d src/c_backend.ml
src/c_backend.ml | ||
---|---|---|
28 | 28 |
open Corelang |
29 | 29 |
open Machine_code |
30 | 30 |
|
31 |
|
|
32 | 31 |
(********************************************************************************************) |
33 | 32 |
(* Basic Printing functions *) |
34 | 33 |
(********************************************************************************************) |
... | ... | |
92 | 91 |
let rec aux t pp_suffix = |
93 | 92 |
match (Types.repr t).Types.tdesc with |
94 | 93 |
| Types.Tclock t' -> aux t' pp_suffix |
95 |
| Types.Tbool -> Format.fprintf fmt "_Bool %s%a" var pp_suffix ()
|
|
96 |
| Types.Treal -> Format.fprintf fmt "double %s%a" var pp_suffix ()
|
|
97 |
| Types.Tint -> Format.fprintf fmt "int %s%a" var pp_suffix ()
|
|
94 |
| Types.Tbool -> fprintf fmt "_Bool %s%a" var pp_suffix () |
|
95 |
| Types.Treal -> fprintf fmt "double %s%a" var pp_suffix () |
|
96 |
| Types.Tint -> fprintf fmt "int %s%a" var pp_suffix () |
|
98 | 97 |
| Types.Tarray (d, t') -> |
99 |
let pp_suffix' fmt () = Format.fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
|
|
98 |
let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in |
|
100 | 99 |
aux t' pp_suffix' |
101 |
| Types.Tstatic (_, t') -> Format.fprintf fmt "const "; aux t' pp_suffix
|
|
102 |
| Types.Tconst ty -> Format.fprintf fmt "%s %s" ty var
|
|
103 |
| Types.Tarrow (_, _) -> Format.fprintf fmt "void (*%s)()" var
|
|
104 |
| _ -> Format.eprintf "internal error: pp_c_type %a@." Types.print_ty t; assert false
|
|
100 |
| Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix |
|
101 |
| Types.Tconst ty -> fprintf fmt "%s %s" ty var |
|
102 |
| Types.Tarrow (_, _) -> fprintf fmt "void (*%s)()" var |
|
103 |
| _ -> eprintf "internal error: pp_c_type %a@." Types.print_ty t; assert false |
|
105 | 104 |
in aux t (fun fmt () -> ()) |
106 | 105 |
|
107 | 106 |
let rec pp_c_initialize fmt t = |
... | ... | |
111 | 110 |
| Types.Tbool -> pp_print_string fmt "0" |
112 | 111 |
| Types.Treal -> pp_print_string fmt "0." |
113 | 112 |
| Types.Tarray (d, t') when Dimension.is_dimension_const d -> |
114 |
Format.fprintf fmt "{%a}"
|
|
113 |
fprintf fmt "{%a}" |
|
115 | 114 |
(Utils.fprintf_list ~sep:"," (fun fmt _ -> pp_c_initialize fmt t')) |
116 | 115 |
(Utils.duplicate 0 (Dimension.size_const_dimension d)) |
117 | 116 |
| _ -> assert false |
... | ... | |
146 | 145 |
pp_c_type id.var_id fmt id.var_type |
147 | 146 |
|
148 | 147 |
let pp_c_decl_array_mem self fmt id = |
149 |
Format.fprintf fmt "%a = (%a) (%s->_reg.%s)"
|
|
148 |
fprintf fmt "%a = (%a) (%s->_reg.%s)" |
|
150 | 149 |
(pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type |
151 | 150 |
(pp_c_type "(*)") id.var_type |
152 | 151 |
self |
... | ... | |
169 | 168 |
let pp_c_var_read m fmt id = |
170 | 169 |
if Types.is_array_type id.var_type |
171 | 170 |
then |
172 |
Format.fprintf fmt "%s" id.var_id
|
|
171 |
fprintf fmt "%s" id.var_id |
|
173 | 172 |
else |
174 | 173 |
if List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs (* id is output *) |
175 |
then Format.fprintf fmt "*%s" id.var_id
|
|
176 |
else Format.fprintf fmt "%s" id.var_id
|
|
174 |
then fprintf fmt "*%s" id.var_id |
|
175 |
else fprintf fmt "%s" id.var_id |
|
177 | 176 |
|
178 | 177 |
(* Addressable value of a variable, the one that is passed around in calls: |
179 | 178 |
- if it's not a scalar non-output, then its name is enough |
... | ... | |
183 | 182 |
let pp_c_var_write m fmt id = |
184 | 183 |
if Types.is_array_type id.var_type |
185 | 184 |
then |
186 |
Format.fprintf fmt "%s" id.var_id
|
|
185 |
fprintf fmt "%s" id.var_id |
|
187 | 186 |
else |
188 | 187 |
if List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs (* id is output *) |
189 | 188 |
then |
190 |
Format.fprintf fmt "%s" id.var_id
|
|
189 |
fprintf fmt "%s" id.var_id |
|
191 | 190 |
else |
192 |
Format.fprintf fmt "&%s" id.var_id
|
|
191 |
fprintf fmt "&%s" id.var_id |
|
193 | 192 |
|
194 | 193 |
let pp_c_decl_instance_var fmt (name, (node, static)) = |
195 |
Format.fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
|
|
194 |
fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name |
|
196 | 195 |
|
197 | 196 |
let pp_c_tag fmt t = |
198 | 197 |
pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t) |
... | ... | |
204 | 203 |
| Const_real r -> pp_print_string fmt r |
205 | 204 |
| Const_float r -> pp_print_float fmt r |
206 | 205 |
| Const_tag t -> pp_c_tag fmt t |
207 |
| Const_array ca -> Format.fprintf fmt "{%a}" (Utils.fprintf_list ~sep:"," pp_c_const) ca
|
|
206 |
| Const_array ca -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:"," pp_c_const) ca |
|
208 | 207 |
|
209 | 208 |
(* Prints a value expression [v], with internal function calls only. |
210 | 209 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
... | ... | |
213 | 212 |
let rec pp_c_val self pp_var fmt v = |
214 | 213 |
match v with |
215 | 214 |
| Cst c -> pp_c_const fmt c |
216 |
| Array vl -> Format.fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
|
|
217 |
| Access (t, i) -> Format.fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
|
|
215 |
| Array vl -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl |
|
216 |
| Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i |
|
218 | 217 |
| Power (v, n) -> assert false |
219 | 218 |
| LocalVar v -> pp_var fmt v |
220 | 219 |
| StateVar v -> |
221 | 220 |
if Types.is_array_type v.var_type |
222 |
then Format.fprintf fmt "*%a" pp_var v
|
|
223 |
else Format.fprintf fmt "%s->_reg.%a" self pp_var v
|
|
221 |
then fprintf fmt "*%a" pp_var v |
|
222 |
else fprintf fmt "%s->_reg.%a" self pp_var v |
|
224 | 223 |
| Fun (n, vl) -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl |
225 | 224 |
|
226 | 225 |
let pp_c_checks self fmt m = |
227 |
Utils.fprintf_list ~sep:"" (fun fmt (loc, check) -> Format.fprintf fmt "@[<v>%a@,assert (%a);@]@," Location.pp_c_loc loc (pp_c_val self (pp_c_var_read m)) check) fmt m.mstep.step_checks
|
|
226 |
Utils.fprintf_list ~sep:"" (fun fmt (loc, check) -> fprintf fmt "@[<v>%a@,assert (%a);@]@," Location.pp_c_loc loc (pp_c_val self (pp_c_var_read m)) check) fmt m.mstep.step_checks |
|
228 | 227 |
|
229 | 228 |
|
230 | 229 |
(********************************************************************************************) |
... | ... | |
269 | 268 |
(* Prints a one loop variable suffix for arrays *) |
270 | 269 |
let pp_loop_var fmt lv = |
271 | 270 |
match snd lv with |
272 |
| LVar v -> Format.fprintf fmt "[%s]" v
|
|
273 |
| LInt r -> Format.fprintf fmt "[%d]" !r
|
|
271 |
| LVar v -> fprintf fmt "[%s]" v |
|
272 |
| LInt r -> fprintf fmt "[%d]" !r |
|
274 | 273 |
|
275 | 274 |
(* Prints a suffix of loop variables for arrays *) |
276 | 275 |
let pp_suffix fmt loop_vars = |
... | ... | |
286 | 285 |
| _ , Fun (n, vl) -> |
287 | 286 |
Basic_library.pp_c n (pp_value_suffix self loop_vars pp_value) fmt vl |
288 | 287 |
| _ , _ -> |
289 |
let pp_var_suffix fmt v = Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in
|
|
288 |
let pp_var_suffix fmt v = fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in |
|
290 | 289 |
pp_c_val self pp_var_suffix fmt value |
291 | 290 |
|
292 | 291 |
(* type_directed assignment: array vs. statically sized type |
... | ... | |
297 | 296 |
*) |
298 | 297 |
let pp_assign m self pp_var fmt var_type var_name value = |
299 | 298 |
let depth = expansion_depth value in |
300 |
(*Format.eprintf "pp_assign %a %a %d@." Types.print_ty var_type pp_val value depth;*)
|
|
299 |
(*eprintf "pp_assign %a %a %d@." Types.print_ty var_type pp_val value depth;*) |
|
301 | 300 |
let loop_vars = mk_loop_variables m var_type depth in |
302 | 301 |
let reordered_loop_vars = reorder_loop_variables loop_vars in |
303 | 302 |
let rec aux fmt vars = |
... | ... | |
305 | 304 |
| [] -> |
306 | 305 |
fprintf fmt "%a = %a;" (pp_value_suffix self loop_vars pp_var) var_name (pp_value_suffix self loop_vars pp_var) value |
307 | 306 |
| (d, LVar i) :: q -> |
308 |
(*Format.eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
|
|
309 |
Format.fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
|
|
307 |
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*) |
|
308 |
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}" |
|
310 | 309 |
i i i Dimension.pp_dimension d i |
311 | 310 |
aux q |
312 | 311 |
| (d, LInt r) :: q -> |
313 |
(*Format.eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
|
|
312 |
(*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*) |
|
314 | 313 |
let szl = Utils.enumerate (Dimension.size_const_dimension d) in |
315 |
Format.fprintf fmt "@[<v 2>{@,%a@]@,}"
|
|
314 |
fprintf fmt "@[<v 2>{@,%a@]@,}" |
|
316 | 315 |
(Utils.fprintf_list ~sep:"@," (fun fmt i -> r := i; aux fmt q)) szl |
317 | 316 |
in |
318 | 317 |
begin |
... | ... | |
324 | 323 |
let pp_instance_call m self fmt i (inputs: value_t list) (outputs: var_decl list) = |
325 | 324 |
try (* stateful node instance *) |
326 | 325 |
let (n,_) = List.assoc i m.minstances in |
327 |
Format.fprintf fmt "%s_step (%a%t%a%t%s->%s);"
|
|
326 |
fprintf fmt "%s_step (%a%t%a%t%s->%s);" |
|
328 | 327 |
(node_name n) |
329 | 328 |
(Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs |
330 | 329 |
(Utils.pp_final_char_if_non_empty ", " inputs) |
... | ... | |
334 | 333 |
i |
335 | 334 |
with Not_found -> (* stateless node instance *) |
336 | 335 |
let (n,_) = List.assoc i m.mcalls in |
337 |
Format.fprintf fmt "%s (%a%t%a);"
|
|
336 |
fprintf fmt "%s (%a%t%a);" |
|
338 | 337 |
(node_name n) |
339 | 338 |
(Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs |
340 | 339 |
(Utils.pp_final_char_if_non_empty ", " inputs) |
... | ... | |
385 | 384 |
(Utils.fprintf_list ~sep:"@," (pp_machine_branch m self)) hl |
386 | 385 |
|
387 | 386 |
and pp_machine_branch m self fmt (t, h) = |
388 |
Format.fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" pp_c_tag t (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) h |
|
387 |
fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" pp_c_tag t (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) h |
|
388 |
|
|
389 |
|
|
390 |
(**************************************************************************) |
|
391 |
(* Printing spec for c *) |
|
392 |
|
|
393 |
(**************************************************************************) |
|
394 |
|
|
395 |
|
|
396 |
let pp_econst fmt c = |
|
397 |
match c with |
|
398 |
| EConst_int i -> pp_print_int fmt i |
|
399 |
| EConst_real r -> pp_print_string fmt r |
|
400 |
| EConst_float r -> pp_print_float fmt r |
|
401 |
| EConst_bool b -> pp_print_bool fmt b |
|
402 |
| EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"") |
|
403 |
|
|
404 |
let rec pp_eexpr is_output fmt eexpr = |
|
405 |
let pp_eexpr = pp_eexpr is_output in |
|
406 |
match eexpr.eexpr_desc with |
|
407 |
| EExpr_const c -> pp_econst fmt c |
|
408 |
| EExpr_ident id -> |
|
409 |
if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id |
|
410 |
| EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el |
|
411 |
| EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2 |
|
412 |
| EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2 |
|
413 |
(* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *) |
|
414 |
(* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *) |
|
415 |
| EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e |
|
416 |
| EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id |
|
417 |
| EExpr_merge (id, e1, e2) -> |
|
418 |
fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2 |
|
419 |
| EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r |
|
420 |
| EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" Printers.pp_node_args vars pp_eexpr e |
|
421 |
| EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" Printers.pp_node_args vars pp_eexpr e |
|
422 |
|
|
423 |
|
|
424 |
(* | EExpr_whennot _ *) |
|
425 |
(* | EExpr_uclock _ *) |
|
426 |
(* | EExpr_dclock _ *) |
|
427 |
(* | EExpr_phclock _ -> assert false *) |
|
428 |
and pp_eapp is_output fmt id e r = |
|
429 |
let pp_eexpr = pp_eexpr is_output in |
|
430 |
match r with |
|
431 |
| None -> |
|
432 |
(match id, e.eexpr_desc with |
|
433 |
| "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2 |
|
434 |
| "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e |
|
435 |
| "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2 |
|
436 |
| "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2 |
|
437 |
| "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2 |
|
438 |
| "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2 |
|
439 |
| "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2 |
|
440 |
| "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2 |
|
441 |
| "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2 |
|
442 |
| "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2 |
|
443 |
| "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2 |
|
444 |
| "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2 |
|
445 |
| ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2 |
|
446 |
| ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2 |
|
447 |
| "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2 |
|
448 |
| "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2 |
|
449 |
| "not", _ -> fprintf fmt "(! %a)" pp_eexpr e |
|
450 |
| "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3 |
|
451 |
| _ -> fprintf fmt "%s (%a)" id pp_eexpr e) |
|
452 |
| Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x |
|
453 |
|
|
454 |
let pp_ensures is_output fmt e = |
|
455 |
match e with |
|
456 |
| EnsuresExpr e -> fprintf fmt "ensures %a;@ " (pp_eexpr is_output) e |
|
457 |
| SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (Utils.fprintf_list ~sep:", " (pp_eexpr is_output)) args |
|
458 |
|
|
459 |
let pp_acsl_spec outputs fmt spec = |
|
460 |
let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in |
|
461 |
let pp_eexpr = pp_eexpr is_output in |
|
462 |
fprintf fmt "@[<v 2>/*@@ "; |
|
463 |
Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires; |
|
464 |
Utils.fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures; |
|
465 |
fprintf fmt "@ "; |
|
466 |
(* fprintf fmt "assigns *self%t%a;@ " *) |
|
467 |
(* (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *) |
|
468 |
(* (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *) |
|
469 |
Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> |
|
470 |
fprintf fmt "behavior %s:@[@ %a@ %a@]" |
|
471 |
name |
|
472 |
(Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes |
|
473 |
(Utils.fprintf_list ~sep:"@ " (pp_ensures is_output)) requires |
|
474 |
) fmt spec.behaviors; |
|
475 |
fprintf fmt "@]@ */@."; |
|
476 |
() |
|
389 | 477 |
|
390 | 478 |
(********************************************************************************************) |
391 | 479 |
(* Prototype Printing functions *) |
... | ... | |
567 | 655 |
(match m.mspec with |
568 | 656 |
| None -> () |
569 | 657 |
| Some spec -> |
570 |
Printers.pp_acsl_spec m.mstep.step_outputs fmt spec
|
|
658 |
pp_acsl_spec m.mstep.step_outputs fmt spec |
|
571 | 659 |
); |
572 | 660 |
fprintf fmt "extern %a;@.@." |
573 | 661 |
(print_step_prototype self) |
... | ... | |
772 | 860 |
|
773 | 861 |
let print_makefile basename nodename fmt = |
774 | 862 |
fprintf fmt "GCC=gcc@."; |
775 |
fprintf fmt "INC=/usr/local/include/lustrec@."; |
|
863 |
fprintf fmt "LUSTREC=%s@." Sys.executable_name; |
|
864 |
fprintf fmt "LUSTREC_BASE=%s@." (Filename.dirname (Filename.dirname Sys.executable_name)); |
|
865 |
fprintf fmt "INC=${LUSTREC_BASE}/include/lustrec@."; |
|
776 | 866 |
fprintf fmt "@."; |
777 | 867 |
fprintf fmt "%s_%s:@." basename nodename; |
778 | 868 |
fprintf fmt "\t${GCC} -I${INC} -I. -c %s.c@." basename; |
779 | 869 |
fprintf fmt "\t${GCC} -I${INC} -c ${INC}/io_frontend.c@."; |
780 | 870 |
(* fprintf fmt "\t${GCC} -I${INC} -c ${INC}/StdLibrary.c@."; *) |
781 | 871 |
(* fprintf fmt "\t${GCC} -o %s_%s io_frontend.o StdLibrary.o -lm %s.o@." basename nodename basename*) |
782 |
fprintf fmt "\t${GCC} -o %s_%s io_frontend.o -lm %s.o@." basename nodename basename |
|
872 |
fprintf fmt "\t${GCC} -o %s_%s io_frontend.o -lm %s.o@." basename nodename basename; |
|
873 |
fprintf fmt "@."; |
|
874 |
fprintf fmt "clean:@."; |
|
875 |
fprintf fmt "\t\\rm -f *.o %s_%s@." basename nodename |
|
783 | 876 |
|
784 | 877 |
|
785 | 878 |
|
Also available in: Unified diff