lustrec / src / backends / C / c_backend_spec.ml @ ef34b4ae
History | View | Annotate | Download (8.19 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
5 |
(* *) |
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 |
(* under the terms of the GNU Lesser General Public License *) |
8 |
(* version 2.1. *) |
9 |
(* *) |
10 |
(********************************************************************) |
11 |
|
12 |
open Format |
13 |
open LustreSpec |
14 |
open Machine_code |
15 |
open C_backend_common |
16 |
open Utils |
17 |
|
18 |
(**************************************************************************) |
19 |
(* Printing spec for c *) |
20 |
|
21 |
(**************************************************************************) |
22 |
(* OLD STUFF ??? |
23 |
|
24 |
|
25 |
let pp_acsl_type var fmt t = |
26 |
let rec aux t pp_suffix = |
27 |
match (Types.repr t).Types.tdesc with |
28 |
| Types.Tclock t' -> aux t' pp_suffix |
29 |
| Types.Tbool -> fprintf fmt "int %s%a" var pp_suffix () |
30 |
| Types.Treal -> fprintf fmt "real %s%a" var pp_suffix () |
31 |
| Types.Tint -> fprintf fmt "int %s%a" var pp_suffix () |
32 |
| Types.Tarray (d, t') -> |
33 |
let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in |
34 |
aux t' pp_suffix' |
35 |
(* | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix *) |
36 |
(* | Types.Tconst ty -> fprintf fmt "%s %s" ty var *) |
37 |
(* | Types.Tarrow (_, _) -> fprintf fmt "void (\*%s)()" var *) |
38 |
| _ -> eprintf "internal error: pp_acsl_type %a@." Types.print_ty t; assert false |
39 |
in aux t (fun fmt () -> ()) |
40 |
|
41 |
let pp_acsl_var_decl fmt id = |
42 |
pp_acsl_type id.var_id fmt id.var_type |
43 |
|
44 |
|
45 |
let rec pp_eexpr is_output fmt eexpr = |
46 |
let pp_eexpr = pp_eexpr is_output in |
47 |
match eexpr.eexpr_desc with |
48 |
| EExpr_const c -> Printers.pp_econst fmt c |
49 |
| EExpr_ident id -> |
50 |
if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id |
51 |
| EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el |
52 |
| EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2 |
53 |
| EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2 |
54 |
(* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *) |
55 |
(* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *) |
56 |
| EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e |
57 |
| EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id |
58 |
| EExpr_merge (id, e1, e2) -> |
59 |
fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2 |
60 |
| EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r |
61 |
| EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" Printers.pp_node_args vars pp_eexpr e |
62 |
| EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" Printers.pp_node_args vars pp_eexpr e |
63 |
|
64 |
|
65 |
(* | EExpr_whennot _ *) |
66 |
(* | EExpr_uclock _ *) |
67 |
(* | EExpr_dclock _ *) |
68 |
(* | EExpr_phclock _ -> assert false *) |
69 |
and pp_eapp is_output fmt id e r = |
70 |
let pp_eexpr = pp_eexpr is_output in |
71 |
match r with |
72 |
| None -> |
73 |
(match id, e.eexpr_desc with |
74 |
| "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2 |
75 |
| "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e |
76 |
| "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2 |
77 |
| "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2 |
78 |
| "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2 |
79 |
| "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2 |
80 |
| "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2 |
81 |
| "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2 |
82 |
| "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2 |
83 |
| "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2 |
84 |
| "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2 |
85 |
| "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2 |
86 |
| ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2 |
87 |
| ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2 |
88 |
| "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2 |
89 |
| "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2 |
90 |
| "not", _ -> fprintf fmt "(! %a)" pp_eexpr e |
91 |
| "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3 |
92 |
| _ -> fprintf fmt "%s (%a)" id pp_eexpr e) |
93 |
| Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x |
94 |
|
95 |
let pp_ensures is_output fmt e = |
96 |
match e with |
97 |
| EnsuresExpr e -> fprintf fmt "ensures %a;@ " (pp_eexpr is_output) e |
98 |
| SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (Utils.fprintf_list ~sep:", " (pp_eexpr is_output)) args |
99 |
|
100 |
let pp_acsl_spec outputs fmt spec = |
101 |
let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in |
102 |
let pp_eexpr = pp_eexpr is_output in |
103 |
fprintf fmt "@[<v 2>/*@@ "; |
104 |
Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires; |
105 |
Utils.fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures; |
106 |
fprintf fmt "@ "; |
107 |
(* fprintf fmt "assigns *self%t%a;@ " *) |
108 |
(* (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *) |
109 |
(* (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *) |
110 |
Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> |
111 |
fprintf fmt "behavior %s:@[@ %a@ %a@]" |
112 |
name |
113 |
(Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes |
114 |
(Utils.fprintf_list ~sep:"@ " (pp_ensures is_output)) requires |
115 |
) fmt spec.behaviors; |
116 |
fprintf fmt "@]@ */@."; |
117 |
() |
118 |
|
119 |
|
120 |
|
121 |
|
122 |
let print_machine_decl_prefix fmt m = |
123 |
(* Print specification if any *) |
124 |
(match m.mspec with |
125 |
| None -> () |
126 |
| Some spec -> |
127 |
pp_acsl_spec m.mstep.step_outputs fmt spec |
128 |
) |
129 |
|
130 |
*) |
131 |
|
132 |
(**************************************************************************) |
133 |
(* MAKEFILE *) |
134 |
(**************************************************************************) |
135 |
|
136 |
let makefile_targets fmt basename nodename dependencies = |
137 |
fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@."; |
138 |
(* EACSL version of library file . c *) |
139 |
fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename; |
140 |
fprintf fmt |
141 |
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@." |
142 |
basename basename; |
143 |
fprintf fmt "@."; |
144 |
fprintf fmt "@."; |
145 |
|
146 |
(* EACSL version of library file . c + main .c *) |
147 |
fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename; |
148 |
fprintf fmt "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c -then-on e-acsl -print -ocode %s_main_eacsl.i@." |
149 |
basename basename basename; |
150 |
(* Ugly hack to deal with eacsl bugs *) |
151 |
fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename; |
152 |
fprintf fmt "@."; |
153 |
fprintf fmt "@."; |
154 |
|
155 |
(* EACSL version of binary *) |
156 |
fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename; |
157 |
fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *) |
158 |
C_backend_makefile.fprintf_dependencies fmt dependencies; |
159 |
fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@." |
160 |
basename |
161 |
(Utils.fprintf_list ~sep:" " (fun fmt (_, s, _) -> Format.fprintf fmt "%s.o" s)) |
162 |
(C_backend_makefile.compiled_dependencies dependencies) |
163 |
("${FRAMACEACSL}/e_acsl.c " |
164 |
^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c " |
165 |
^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c") |
166 |
basename |
167 |
(Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib)) |
168 |
(C_backend_makefile.lib_dependencies dependencies) |
169 |
; |
170 |
fprintf fmt "@."; |
171 |
|
172 |
module MakefileMod = |
173 |
struct |
174 |
let other_targets = makefile_targets |
175 |
|
176 |
end |
177 |
|
178 |
(* Local Variables: *) |
179 |
(* compile-command:"make -C ../../.." *) |
180 |
(* End: *) |