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