/src/backends/C/c_backend_spec.ml - Annotate - LustreC

| Branch: | Tag: | Revision:

lustrec/src/backends/C/c_backend_spec.ml @ e77a0fa5

1	a2d97a3e	ploc	(********************************************************************)
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	27502d69	Lélio Brun	open Utils
12			open Format
13	8446bf03	ploc	open Lustre_types
14	c226a3ba	Lélio Brun	open Machine_code_types
15			open C_backend_common
16			open Corelang
17	6d1693b9	Lélio Brun	open Spec_types
18			open Machine_code_common
19	a7062da6	Lélio Brun	module Mpfr = Lustrec_mpfr
20
21	13eb21df	ploc	(**************************************************************************)
22			(* Printing spec for c *)
23
24			(**************************************************************************)
25	6d1693b9	Lélio Brun
26	7f03f62d	Lélio Brun	let pp_acsl_basic_type_desc t_desc =
27			if Types.is_bool_type t_desc then
28			(* if !Options.cpp then "bool" else "_Bool" *)
29	8d2d6fa0	Lélio Brun	"_Bool"
30	7f03f62d	Lélio Brun	else if Types.is_int_type t_desc then
31			(* !Options.int_type *)
32	aaa8e454	Lélio Brun	if t_desc.tid = -1 then "int" else "integer"
33	7f03f62d	Lélio Brun	else if Types.is_real_type t_desc then
34			if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
35	ca7ff3f7	Lélio Brun	else assert false
36			(* Not a basic C type. Do not handle arrays or pointers *)
37	7f03f62d	Lélio Brun
38	d29fbec5	Lélio Brun	let pp_acsl pp fmt = fprintf fmt "@[<v>/%@ @[<v>%a@]@,/@]" pp
39	c226a3ba	Lélio Brun
40	0988cb68	Lélio Brun	let pp_acsl_cut pp fmt = fprintf fmt "%a@," (pp_acsl pp)
41	c226a3ba	Lélio Brun
42	ca7ff3f7	Lélio Brun	let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp
43	c226a3ba	Lélio Brun
44	d29fbec5	Lélio Brun	let pp_acsl_line' ?(ghost = false) pp fmt x =
45	5b98398a	Lélio Brun	let op = if ghost then "" else "*" in
46			let cl = if ghost then "@" else "*" in
47			fprintf fmt "/%s%@ @[<h>%a@] %s/" op pp x cl
48	c4780a6a	Lélio Brun
49	d978c46e	Lélio Brun	let pp_acsl_line'_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line' pp)
50	c226a3ba	Lélio Brun
51	d978c46e	Lélio Brun	let pp_requires pp fmt = fprintf fmt "requires %a;" pp
52	c226a3ba	Lélio Brun
53	d978c46e	Lélio Brun	let pp_ensures pp fmt = fprintf fmt "ensures %a;" pp
54
55			let pp_assumes pp fmt = fprintf fmt "assumes %a;" pp
56
57			let pp_terminates pp fmt = fprintf fmt "terminates %a;" pp
58	6d1693b9	Lélio Brun
59	8d2d6fa0	Lélio Brun	let pp_assigns pp =
60	6d1693b9	Lélio Brun	pp_comma_list
61	8d2d6fa0	Lélio Brun	~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
62	d978c46e	Lélio Brun	~pp_epilogue:pp_print_semicolon'
63			pp
64	c226a3ba	Lélio Brun
65	18dada08	Lélio Brun	let pp_ghost pp fmt = fprintf fmt "ghost %a" pp
66	c226a3ba	Lélio Brun
67	18dada08	Lélio Brun	let pp_assert pp fmt = fprintf fmt "assert %a;" pp
68
69			let pp_loop_invariant pp fmt = fprintf fmt "loop invariant %a;" pp
70	c226a3ba	Lélio Brun
71			let pp_mem_valid pp_var fmt (name, var) =
72			fprintf fmt "%s_valid(%a)" name pp_var var
73
74			let pp_mem_valid' = pp_mem_valid pp_print_string
75
76	d978c46e	Lélio Brun	let pp_ref pp fmt = fprintf fmt "&%a" pp
77
78	18dada08	Lélio Brun	let pp_ref' = pp_ref pp_print_string
79
80	8d2d6fa0	Lélio Brun	let pp_indirect pp_ptr pp_field fmt (ptr, field) =
81			fprintf fmt "%a->%a" pp_ptr ptr pp_field field
82	c226a3ba	Lélio Brun
83	8d2d6fa0	Lélio Brun	let pp_indirect' = pp_indirect pp_print_string pp_print_string
84	c226a3ba	Lélio Brun
85	8d2d6fa0	Lélio Brun	let pp_access pp_stru pp_field fmt (stru, field) =
86			fprintf fmt "%a.%a" pp_stru stru pp_field field
87	c226a3ba	Lélio Brun
88	8d2d6fa0	Lélio Brun	let pp_access' = pp_access pp_print_string pp_print_string
89	c226a3ba	Lélio Brun
90	ca7ff3f7	Lélio Brun	let pp_var_decl fmt v = pp_print_string fmt v.var_id
91	8d2d6fa0	Lélio Brun
92			let pp_reg self fmt field =
93			pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
94
95	ca7ff3f7	Lélio Brun	let pp_true fmt () = pp_print_string fmt "\\true"
96	c226a3ba	Lélio Brun
97	10131419	Lélio Brun	let pp_cast pp_ty pp fmt (ty, x) = fprintf fmt "(%a) %a" pp_ty ty pp x
98
99			let pp_bool_cast pp fmt x = pp_cast pp_print_string pp fmt ("_Bool", x)
100
101	81d69074	Lélio Brun	let pp_double_cast pp fmt x = pp_cast pp_print_string pp fmt ("double", x)
102
103	10131419	Lélio Brun	let pp_true_c_bool fmt () = pp_bool_cast pp_print_string fmt "1"
104	0988cb68	Lélio Brun
105	ca7ff3f7	Lélio Brun	let pp_false fmt () = pp_print_string fmt "\\false"
106	6d1693b9	Lélio Brun
107	18dada08	Lélio Brun	let pp_nothing fmt () = pp_print_string fmt "\\nothing"
108
109	f1518c7c	Lélio Brun	let pp_null fmt () = pp_print_string fmt "\\null"
110
111			let pp_stdout fmt () = pp_print_string fmt "stdout"
112
113	ca7ff3f7	Lélio Brun	let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l
114	8d2d6fa0	Lélio Brun
115	e164af45	Lélio Brun	let pp_at_pre pp_v fmt v = pp_at pp_v fmt (v, "Pre")
116
117	d29fbec5	Lélio Brun	let find_machine f = List.find (fun m -> m.mname.node_id = f)
118	5b98398a	Lélio Brun
119	8d2d6fa0	Lélio Brun	let instances machines m =
120			let open List in
121	6d1693b9	Lélio Brun	let grow paths i td mems =
122	8d2d6fa0	Lélio Brun	match paths with
123	ca7ff3f7	Lélio Brun	\| [] ->
124			[ [ i, (td, mems) ] ]
125			\| _ ->
126			map (cons (i, (td, mems))) paths
127	8d2d6fa0	Lélio Brun	in
128			let rec aux paths m =
129	ca7ff3f7	Lélio Brun	map
130			(fun (i, (td, _)) ->
131	8d2d6fa0	Lélio Brun	try
132	5b98398a	Lélio Brun	let m = find_machine (node_name td) machines in
133	6d1693b9	Lélio Brun	aux (grow paths i td m.mmemory) m
134			with Not_found -> grow paths i td [])
135	ca7ff3f7	Lélio Brun	m.minstances
136			\|> flatten
137	8d2d6fa0	Lélio Brun	in
138			aux [] m \|> map rev
139
140			let memories insts =
141	ca7ff3f7	Lélio Brun	List.(
142			map
143			(fun path ->
144			let _, (_, mems) = hd (rev path) in
145			map (fun mem -> path, mem) mems)
146			insts
147			\|> flatten)
148
149	18dada08	Lélio Brun	let pp_instance ?(indirect = true) pp ptr =
150	8d2d6fa0	Lélio Brun	pp_print_list
151	18dada08	Lélio Brun	~pp_prologue:(fun fmt () -> fprintf fmt "%a->" pp ptr)
152	6d1693b9	Lélio Brun	~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
153	8d2d6fa0	Lélio Brun	(fun fmt (i, _) -> pp_print_string fmt i)
154
155	ca7ff3f7	Lélio Brun	let pp_memory ?(indirect = true) ptr fmt (path, mem) =
156	6d1693b9	Lélio Brun	pp_access
157			((if indirect then pp_indirect else pp_access)
158	18dada08	Lélio Brun	(pp_instance ~indirect pp_print_string ptr)
159	ca7ff3f7	Lélio Brun	pp_print_string)
160	d978c46e	Lélio Brun	pp_var_decl
161			fmt
162	ca7ff3f7	Lélio Brun	((path, "_reg"), mem)
163	8d2d6fa0	Lélio Brun
164			let prefixes l =
165			let rec pref acc = function
166	ca7ff3f7	Lélio Brun	\| x :: l ->
167			pref ([ x ] :: List.map (List.cons x) acc) l
168			\| [] ->
169			acc
170	8d2d6fa0	Lélio Brun	in
171			pref [] (List.rev l)
172
173	18dada08	Lélio Brun	let powerset_instances paths =
174			List.map prefixes paths \|> List.flatten \|> remove_duplicates
175	8d2d6fa0	Lélio Brun
176	18dada08	Lélio Brun	let pp_separated pp_self pp_mem pp_ptr fmt (self, mem, paths, ptrs) =
177	d978c46e	Lélio Brun	fprintf
178			fmt
179	5b98398a	Lélio Brun	"\\separated(@[<v>%a, %a%a%a@])"
180	18dada08	Lélio Brun	pp_self
181	d978c46e	Lélio Brun	self
182	18dada08	Lélio Brun	pp_mem
183	d978c46e	Lélio Brun	mem
184	5b98398a	Lélio Brun	(pp_comma_list ~pp_prologue:pp_print_comma (pp_instance pp_self self))
185	8d2d6fa0	Lélio Brun	paths
186	5b98398a	Lélio Brun	(pp_comma_list ~pp_prologue:pp_print_comma pp_ptr)
187	8d2d6fa0	Lélio Brun	ptrs
188	c226a3ba	Lélio Brun
189	18dada08	Lélio Brun	let pp_separated' self mem fmt (paths, ptrs) =
190			pp_separated
191			pp_print_string
192			pp_print_string
193			pp_var_decl
194			fmt
195			(self, mem, paths, ptrs)
196
197			let pp_separated'' =
198	6d1693b9	Lélio Brun	pp_comma_list
199	9d693675	Lélio Brun	~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
200	d978c46e	Lélio Brun	~pp_epilogue:pp_print_cpar
201			pp_var_decl
202	9d693675	Lélio Brun
203	c226a3ba	Lélio Brun	let pp_forall pp_l pp_r fmt (l, r) =
204	dccec723	Lélio Brun	fprintf fmt "@[<v 2>\\forall @[<hov>%a@];@,%a@]" pp_l l pp_r r
205	c226a3ba	Lélio Brun
206	4b596770	Lélio Brun	let pp_exists pp_l pp_r fmt (l, r) =
207	ca7ff3f7	Lélio Brun	fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r
208	4b596770	Lélio Brun
209	ca7ff3f7	Lélio Brun	let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
210	c226a3ba	Lélio Brun
211	89fd79f0	Lélio Brun	let pp_gequal pp_l pp_r fmt (l, r) = fprintf fmt "%a >= %a" pp_l l pp_r r
212
213	c226a3ba	Lélio Brun	let pp_implies pp_l pp_r fmt (l, r) =
214	ca7ff3f7	Lélio Brun	fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
215	c226a3ba	Lélio Brun
216	ca7ff3f7	Lélio Brun	let pp_and pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ && %a@]" pp_l l pp_r r
217	c226a3ba	Lélio Brun
218			let pp_and_l pp_v fmt =
219	d978c46e	Lélio Brun	pp_print_list
220			~pp_open_box:pp_open_vbox0
221	c226a3ba	Lélio Brun	~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
222	f51926b8	Lélio Brun	~pp_nil:pp_true
223	d978c46e	Lélio Brun	pp_v
224			fmt
225	c226a3ba	Lélio Brun
226	f1518c7c	Lélio Brun	let pp_or pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ \|\| %a@]" pp_l l pp_r r
227
228	6d1693b9	Lélio Brun	let pp_or_l pp_v fmt =
229	d978c46e	Lélio Brun	pp_print_list
230			~pp_open_box:pp_open_vbox0
231	6d1693b9	Lélio Brun	~pp_sep:(fun fmt () -> fprintf fmt "@,\|\| ")
232	d978c46e	Lélio Brun	pp_v
233			fmt
234	6d1693b9	Lélio Brun
235	ca7ff3f7	Lélio Brun	let pp_not pp fmt = fprintf fmt "!%a" pp
236	6d1693b9	Lélio Brun
237	d0f26f04	Lélio Brun	let pp_valid pp = pp_and_l (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
238	186e1aef	Lélio Brun
239	f1518c7c	Lélio Brun	let pp_valid_read pp fmt = fprintf fmt "\\valid_read(%a)" pp
240
241	ca7ff3f7	Lélio Brun	let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
242	6d1693b9	Lélio Brun
243	15c3e4e7	Lélio Brun	let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
244	ca7ff3f7	Lélio Brun	fprintf fmt "(%a @[<hov>? %a@ : %a)@]" pp_c c pp_t t pp_f f
245	15c3e4e7	Lélio Brun
246	ca7ff3f7	Lélio Brun	let pp_paren pp fmt v = fprintf fmt "(%a)" pp v
247	4b596770	Lélio Brun
248	6d1693b9	Lélio Brun	let pp_initialization pp_mem fmt (name, mem) =
249	7f03f62d	Lélio Brun	fprintf fmt "%s_initialization(%a)" name pp_mem mem
250	15c3e4e7	Lélio Brun
251	d29fbec5	Lélio Brun	let pp_init pp_mem fmt (name, mem) = fprintf fmt "%s_init(%a)" name pp_mem mem
252	dccec723	Lélio Brun
253	6d1693b9	Lélio Brun	let pp_initialization' = pp_initialization pp_print_string
254	c226a3ba	Lélio Brun
255	aaa8e454	Lélio Brun	let pp_local m =
256			pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
257
258	6d1693b9	Lélio Brun	let pp_locals m =
259	ca7ff3f7	Lélio Brun	pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m)
260	4b596770	Lélio Brun
261	ca7ff3f7	Lélio Brun	let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
262	c226a3ba	Lélio Brun
263	89fd79f0	Lélio Brun	let pp_basic_assign_spec ?(pp_op=pp_equal) pp_l pp_r fmt typ var_name value =
264	ca7ff3f7	Lélio Brun	if Types.is_real_type typ && !Options.mpfr then assert false
265	7f03f62d	Lélio Brun	(* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
266	89fd79f0	Lélio Brun	else pp_op pp_l pp_r fmt (var_name, value)
267	7f03f62d	Lélio Brun
268	89fd79f0	Lélio Brun	let pp_assign_spec ?pp_op m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
269	6d1693b9	Lélio Brun	(var_type, var_name, value) =
270	7f03f62d	Lélio Brun	let depth = expansion_depth value in
271			let loop_vars = mk_loop_variables m var_type depth in
272			let reordered_loop_vars = reorder_loop_variables loop_vars in
273	aaa8e454	Lélio Brun	let aux typ fmt vars =
274	7f03f62d	Lélio Brun	match vars with
275			\| [] ->
276	89fd79f0	Lélio Brun	pp_basic_assign_spec ?pp_op
277	d978c46e	Lélio Brun	(pp_value_suffix
278			~indirect:indirect_l
279			m
280			self_l
281			var_type
282			loop_vars
283	ca7ff3f7	Lélio Brun	pp_var_l)
284	d978c46e	Lélio Brun	(pp_value_suffix
285			~indirect:indirect_r
286			m
287			self_r
288			var_type
289			loop_vars
290	ca7ff3f7	Lélio Brun	pp_var_r)
291	d978c46e	Lélio Brun	fmt
292			typ
293			var_name
294			value
295	9d693675	Lélio Brun	\| (_d, LVar _i) :: _q ->
296	7f03f62d	Lélio Brun	assert false
297	ca7ff3f7	Lélio Brun	(* let typ' = Types.array_element_type typ in
298			* fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
299			* i i i pp_c_dimension d i
300			* (aux typ') q *)
301	9d693675	Lélio Brun	\| (_d, LInt _r) :: _q ->
302	7f03f62d	Lélio Brun	assert false
303	ca7ff3f7	Lélio Brun	(* let typ' = Types.array_element_type typ in
304			* let szl = Utils.enumerate (Dimension.size_const_dimension d) in
305			* fprintf fmt "@[<v 2>{@,%a@]@,}"
306			* (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
307			\| _ ->
308			assert false
309	7f03f62d	Lélio Brun	in
310	ca7ff3f7	Lélio Brun	reset_loop_counter ();
311			aux var_type fmt reordered_loop_vars
312	7f03f62d	Lélio Brun
313	6d1693b9	Lélio Brun	let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
314	d978c46e	Lélio Brun	fprintf
315			fmt
316			"%s_pack%a(@[<hov>%a,@ %a@])"
317			name
318	ca7ff3f7	Lélio Brun	(pp_print_option pp_print_int)
319	d978c46e	Lélio Brun	i
320			pp_mem
321			mem
322			pp_self
323			self
324	6d1693b9	Lélio Brun
325			let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
326	d978c46e	Lélio Brun	pp_memory_pack_aux
327			?i:mp.mpindex
328			pp_mem
329			pp_self
330			fmt
331	6d1693b9	Lélio Brun	(mp.mpname.node_id, mem, self)
332
333	478edbed	Lélio Brun	let pp_transition_aux ?i stateless pp_mem_in pp_mem_out pp_var fmt
334	0406ab94	Lélio Brun	(name, vars, mem_in, mem_out) =
335	d978c46e	Lélio Brun	fprintf
336			fmt
337			"%s_transition%a(@[<hov>%t%a%t@])"
338			name
339	ca7ff3f7	Lélio Brun	(pp_print_option pp_print_int)
340			i
341	aaa8e454	Lélio Brun	(fun fmt -> if not stateless then pp_mem_in fmt mem_in)
342			(pp_comma_list
343			~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
344	0406ab94	Lélio Brun	pp_var)
345			vars
346	6d1693b9	Lélio Brun	(fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
347
348	d29fbec5	Lélio Brun	let pp_transition stateless pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out)
349			=
350	d978c46e	Lélio Brun	pp_transition_aux
351			?i:t.tindex
352	478edbed	Lélio Brun	stateless
353	d978c46e	Lélio Brun	pp_mem_in
354			pp_mem_out
355			pp_var
356			fmt
357	0406ab94	Lélio Brun	(t.tname.node_id, t.tvars, mem_in, mem_out)
358	6d1693b9	Lélio Brun
359			let pp_transition_aux' ?i m =
360	478edbed	Lélio Brun	let stateless = fst (get_stateless_status m) in
361			pp_transition_aux ?i stateless pp_print_string pp_print_string (fun fmt v ->
362	0406ab94	Lélio Brun	(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
363	ca7ff3f7	Lélio Brun
364	6d1693b9	Lélio Brun	let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
365	d978c46e	Lélio Brun	fprintf
366			fmt
367			"%s_reset_cleared(@[<hov>%a,@ %a@])"
368			name
369			pp_mem_in
370			mem_in
371			pp_mem_out
372			mem_out
373	6d1693b9	Lélio Brun
374			let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
375
376	27502d69	Lélio Brun	let pp_functional_update mems insts fmt mem =
377			let rec aux fmt = function
378	ca7ff3f7	Lélio Brun	\| [] ->
379			pp_print_string fmt mem
380	27502d69	Lélio Brun	\| (x, is_mem) :: fields ->
381	d978c46e	Lélio Brun	fprintf
382			fmt
383			"{ @[<hov>%a@ \\with .%s%s = %s@] }"
384			aux
385			fields
386	27502d69	Lélio Brun	(if is_mem then "_reg." else "")
387	d978c46e	Lélio Brun	x
388			x
389	aaa8e454	Lélio Brun	in
390	d978c46e	Lélio Brun	aux
391			fmt
392	27502d69	Lélio Brun	(List.map (fun (x, _) -> x, false) (Utils.IMap.bindings insts)
393			@ List.map (fun x -> x, true) (Utils.ISet.elements mems))
394	aaa8e454	Lélio Brun
395	6d1693b9	Lélio Brun	module PrintSpec = struct
396	aaa8e454	Lélio Brun	type mode =
397			\| MemoryPackMode
398			\| TransitionMode
399			\| TransitionFootprintMode
400			\| ResetIn
401			\| ResetOut
402			\| InstrMode of ident
403
404			let pp_reg mem fmt = function
405	6d1693b9	Lélio Brun	\| ResetFlag ->
406	aaa8e454	Lélio Brun	fprintf fmt "%s.%s" mem reset_flag_name
407	6d1693b9	Lélio Brun	\| StateVar x ->
408	aaa8e454	Lélio Brun	fprintf fmt "%s.%a" mem pp_var_decl x
409	6d1693b9	Lélio Brun
410	10131419	Lélio Brun	let not_var v = match v.value_desc with
411			\| Var _ -> false
412			\| _ -> true
413
414			let pp_expr ?(test_output = false) m mem fmt = function
415	ca7ff3f7	Lélio Brun	\| Val v ->
416	e77a0fa5	Lélio Brun	let pp = pp_c_val ~indirect:false m mem (pp_c_var_read ~test_output m) in
417	81d69074	Lélio Brun	(if not_var v
418			then if Types.is_bool_type v.value_type
419			then pp_bool_cast pp
420			else if Types.is_real_type v.value_type
421			then pp_double_cast pp
422			else pp
423			else pp) fmt v
424	ca7ff3f7	Lélio Brun	\| Tag t ->
425			pp_print_string fmt t
426			\| Var v ->
427			pp_var_decl fmt v
428			\| Memory r ->
429			pp_reg mem fmt r
430	6d1693b9	Lélio Brun
431	aaa8e454	Lélio Brun	let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
432	0406ab94	Lélio Brun	let test_output, mem_update =
433	ca7ff3f7	Lélio Brun	match mode with
434			\| InstrMode _ ->
435			true, false
436			\| TransitionFootprintMode ->
437			false, true
438			\| _ ->
439			false, false
440	aaa8e454	Lélio Brun	in
441	10131419	Lélio Brun	let pp_expr test_output fmt e = pp_expr ~test_output m mem_out fmt e in
442	6d1693b9	Lélio Brun	match p with
443	478edbed	Lélio Brun	\| Transition (stateless, f, inst, i, vars, r, mems, insts) ->
444	ca7ff3f7	Lélio Brun	let pp_mem_in, pp_mem_out =
445			match inst with
446	6d1693b9	Lélio Brun	\| None ->
447	ca7ff3f7	Lélio Brun	( pp_print_string,
448	27502d69	Lélio Brun	if mem_update then pp_functional_update mems insts
449			else pp_print_string )
450	6d1693b9	Lélio Brun	\| Some inst ->
451	ca7ff3f7	Lélio Brun	( (fun fmt mem_in ->
452			if r then pp_print_string fmt mem_in
453			else pp_access' fmt (mem_in, inst)),
454			fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
455	6d1693b9	Lélio Brun	in
456	d978c46e	Lélio Brun	pp_transition_aux
457			?i
458	478edbed	Lélio Brun	stateless
459	d978c46e	Lélio Brun	pp_mem_in
460			pp_mem_out
461			(pp_expr test_output)
462			fmt
463	0406ab94	Lélio Brun	(f, vars, mem_in', mem_out')
464	aaa8e454	Lélio Brun	\| Reset (_f, inst, r) ->
465			pp_ite
466			(pp_c_val m mem_in (pp_c_var_read m))
467			(pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
468			(pp_equal pp_print_string pp_access')
469			fmt
470			(r, (mem_out, 1), (mem_out, (mem_in, inst)))
471	6d1693b9	Lélio Brun	\| MemoryPack (f, inst, i) ->
472	ca7ff3f7	Lélio Brun	let pp_mem, pp_self =
473			match inst with
474	6d1693b9	Lélio Brun	\| None ->
475			pp_print_string, pp_print_string
476			\| Some inst ->
477	ca7ff3f7	Lélio Brun	( (fun fmt mem -> pp_access' fmt (mem, inst)),
478			fun fmt self -> pp_indirect' fmt (self, inst) )
479	6d1693b9	Lélio Brun	in
480			pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
481			\| ResetCleared f ->
482			pp_reset_cleared' fmt (f, mem_in, mem_out)
483	ca7ff3f7	Lélio Brun	(* fprintf fmt "ResetCleared_%a" pp_print_string f *)
484			\| Initialization ->
485			()
486	6d1693b9	Lélio Brun
487			let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
488
489	10131419	Lélio Brun	let val_of_expr = function
490	ca7ff3f7	Lélio Brun	\| Val v ->
491			v
492			\| Tag t ->
493			id_to_tag t
494			\| Var v ->
495			vdecl_to_val v
496			\| Memory (StateVar v) ->
497			vdecl_to_val v
498			\| Memory ResetFlag ->
499			vdecl_to_val reset_flag
500	6d1693b9	Lélio Brun
501	9c227bad	Lélio Brun	let find_arrow loc m =
502			match List.find_opt (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances with
503			\| Some (f, _) -> Some f
504			\| None ->
505			Error.pp_warning loc
506			(fun fmt -> pp_print_string fmt "Generating stateful spec for uninitialized state variables.");
507			None
508	6d1693b9	Lélio Brun
509	f51926b8	Lélio Brun	let rec has_memory_val m v =
510			let has_mem = has_memory_val m in
511			match v.value_desc with
512			\| Var v ->
513			is_memory m v
514	d29fbec5	Lélio Brun	\| Array vl \| Fun (_, vl) ->
515	f51926b8	Lélio Brun	List.exists has_mem vl
516	d29fbec5	Lélio Brun	\| Access (t, i) \| Power (t, i) ->
517	f51926b8	Lélio Brun	has_mem t \|\| has_mem i
518			\| _ ->
519			false
520
521	10131419	Lélio Brun	let has_memory m = function Val v -> has_memory_val m v \| _ -> false
522	f51926b8	Lélio Brun
523	27502d69	Lélio Brun	let pp_spec mode m =
524	6d1693b9	Lélio Brun	let rec pp_spec mode fmt f =
525			let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
526			let self = mk_self m in
527			let mem = mk_mem m in
528			let mem_in = mk_mem_in m in
529			let mem_out = mk_mem_out m in
530			let mem_reset = mk_mem_reset m in
531			match mode with
532			\| MemoryPackMode ->
533			self, self, true, mem, mem, false
534			\| TransitionMode ->
535			mem_in, mem_in, false, mem_out, mem_out, false
536	aaa8e454	Lélio Brun	\| TransitionFootprintMode ->
537			mem_in, mem_in, false, mem_out, mem_out, false
538	6d1693b9	Lélio Brun	\| ResetIn ->
539			mem_reset, mem_reset, false, mem_out, mem_out, false
540	aaa8e454	Lélio Brun	\| ResetOut ->
541			mem_in, mem_in, false, mem_reset, mem_reset, false
542	6d1693b9	Lélio Brun	\| InstrMode self ->
543			let mem = "*" ^ mem in
544			fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
545	ca7ff3f7	Lélio Brun	self, flush_str_formatter (), false, mem, mem, false
546	6d1693b9	Lélio Brun	in
547	10131419	Lélio Brun	let pp_expr fmt e = pp_expr m mem_out fmt e in
548	6d1693b9	Lélio Brun	let pp_spec' = pp_spec mode in
549			match f with
550			\| True ->
551			pp_true fmt ()
552			\| False ->
553			pp_false fmt ()
554			\| Equal (a, b) ->
555	f51926b8	Lélio Brun	let pp_eq fmt () =
556			pp_assign_spec
557			m
558			mem_out
559			(pp_c_var_read ~test_output:false m)
560			indirect_l
561			mem_in
562			(pp_c_var_read ~test_output:false m)
563			indirect_r
564			fmt
565	10131419	Lélio Brun	(Spec_common.type_of_l_value a, val_of_expr a, val_of_expr b)
566	f51926b8	Lélio Brun	in
567			if has_memory m b then
568	9c227bad	Lélio Brun	let inst = find_arrow Location.dummy m in
569			pp_print_option
570			~none:pp_eq
571			(fun fmt inst ->
572			pp_paren
573			(pp_implies (pp_not (pp_initialization pp_access')) pp_eq)
574			fmt
575			((Arrow.arrow_id, (mem_in, inst)), ()))
576			fmt inst
577	d29fbec5	Lélio Brun	else pp_eq fmt ()
578	89fd79f0	Lélio Brun	\| GEqual (a, b) ->
579			pp_assign_spec ~pp_op:pp_gequal
580			m
581			mem_out
582			(pp_c_var_read ~test_output:false m)
583			indirect_l
584			mem_in
585			(pp_c_var_read ~test_output:false m)
586			indirect_r
587			fmt
588	10131419	Lélio Brun	(Spec_common.type_of_l_value a, val_of_expr a, val_of_expr b)
589	6d1693b9	Lélio Brun	\| And fs ->
590			pp_and_l pp_spec' fmt fs
591			\| Or fs ->
592			pp_or_l pp_spec' fmt fs
593			\| Imply (a, b) ->
594	50a8778a	Lélio Brun	pp_paren (pp_implies pp_spec' pp_spec') fmt (a, b)
595	6d1693b9	Lélio Brun	\| Exists (xs, a) ->
596			pp_exists (pp_locals m) pp_spec' fmt (xs, a)
597			\| Forall (xs, a) ->
598			pp_forall (pp_locals m) pp_spec' fmt (xs, a)
599			\| Ternary (e, a, b) ->
600			pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
601			\| Predicate p ->
602	aaa8e454	Lélio Brun	pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
603	6d1693b9	Lélio Brun	\| StateVarPack ResetFlag ->
604			let r = vdecl_to_val reset_flag in
605	d978c46e	Lélio Brun	pp_assign_spec
606			m
607			mem_out
608	ca7ff3f7	Lélio Brun	(pp_c_var_read ~test_output:false m)
609	d978c46e	Lélio Brun	indirect_l
610			mem_in
611	ca7ff3f7	Lélio Brun	(pp_c_var_read ~test_output:false m)
612	d978c46e	Lélio Brun	indirect_r
613			fmt
614	6d1693b9	Lélio Brun	(Type_predef.type_bool, r, r)
615			\| StateVarPack (StateVar v) ->
616			let v' = vdecl_to_val v in
617	9c227bad	Lélio Brun	let pp_eq fmt () =
618			pp_assign_spec
619			m
620			mem_out
621			(pp_c_var_read ~test_output:false m)
622			indirect_l
623			mem_in
624			(pp_c_var_read ~test_output:false m)
625			indirect_r
626			fmt
627			(v.var_type, v', v')
628			in
629			let inst = find_arrow Location.dummy m in
630			pp_print_option
631			~none:pp_eq
632			(fun fmt inst ->
633			pp_paren
634			(pp_implies
635			(pp_not (pp_initialization pp_access'))
636			pp_eq)
637			fmt
638			((Arrow.arrow_id, (mem_out, inst)), ()))
639			fmt inst
640	aaa8e454	Lélio Brun	\| ExistsMem (f, rc, tr) ->
641	6d1693b9	Lélio Brun	pp_exists
642			(pp_machine_decl' ~ghost:true)
643	aaa8e454	Lélio Brun	(pp_and (pp_spec ResetOut) (pp_spec ResetIn))
644	6d1693b9	Lélio Brun	fmt
645	ca7ff3f7	Lélio Brun	((f, mk_mem_reset m), (rc, tr))
646	5b98398a	Lélio Brun	\| Value v ->
647	70710795	Lélio Brun	pp_c_val m mem_in (pp_c_var_read ~test_output:true m) fmt v
648	6d1693b9	Lélio Brun	in
649	d29fbec5	Lélio Brun
650	27502d69	Lélio Brun	pp_spec mode
651	6d1693b9	Lélio Brun	end
652	c226a3ba	Lélio Brun
653			let pp_predicate pp_l pp_r fmt (l, r) =
654	ca7ff3f7	Lélio Brun	fprintf fmt "@[<v 2>predicate %a =@,%a;@]" pp_l l pp_r r
655	c226a3ba	Lélio Brun
656	aaa8e454	Lélio Brun	let pp_lemma pp_l pp_r fmt (l, r) =
657	ca7ff3f7	Lélio Brun	fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r
658	aaa8e454	Lélio Brun
659	dccec723	Lélio Brun	let pp_axiomatic pp_l pp_r fmt (l, r) =
660			fprintf fmt "@[<v 2>axiomatic %a {@,%a@]@;}" pp_l l pp_r r
661
662			let pp_axiom pp_l pp_r fmt (l, r) =
663			fprintf fmt "@[<v 2>axiom %a:@,%a;@]" pp_l l pp_r r
664
665	aaa8e454	Lélio Brun	let pp_mem_valid_def fmt m =
666	4fef1a04	Lélio Brun	if not (fst (get_stateless_status m) \|\| m.mis_contract) then
667	c226a3ba	Lélio Brun	let name = m.mname.node_id in
668			let self = mk_self m in
669	6d1693b9	Lélio Brun	pp_acsl
670	c226a3ba	Lélio Brun	(pp_predicate
671	6d1693b9	Lélio Brun	(pp_mem_valid (pp_machine_decl pp_ptr))
672	c226a3ba	Lélio Brun	(pp_and
673	aaa8e454	Lélio Brun	(pp_and_l (fun fmt (inst, (td, _)) ->
674			if Arrow.td_is_arrow td then
675	ca7ff3f7	Lélio Brun	pp_valid pp_indirect' fmt [ self, inst ]
676			else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
677	c226a3ba	Lélio Brun	(pp_valid pp_print_string)))
678			fmt
679	ca7ff3f7	Lélio Brun	((name, (name, self)), (m.minstances, [ self ]))
680	c226a3ba	Lélio Brun
681	6d1693b9	Lélio Brun	let pp_memory_pack_def m fmt mp =
682	4fef1a04	Lélio Brun	if not (fst (get_stateless_status m) \|\| m.mis_contract) then
683			let name = mp.mpname.node_id in
684			let self = mk_self m in
685			let mem = mk_mem m in
686			pp_acsl_cut
687			(pp_predicate
688	d29fbec5	Lélio Brun	(pp_memory_pack
689			(pp_machine_decl' ~ghost:true)
690			(pp_machine_decl pp_ptr))
691	4fef1a04	Lélio Brun	(PrintSpec.pp_spec MemoryPackMode m))
692			fmt
693			((mp, (name, mem), (name, self)), mp.mpformula)
694	c226a3ba	Lélio Brun
695	d978c46e	Lélio Brun	let pp_machine_ghost_struct fmt m =
696	a7062da6	Lélio Brun	pp_acsl (pp_ghost (pp_machine_struct ~ghost:true)) fmt m
697	c226a3ba	Lélio Brun
698	6d1693b9	Lélio Brun	let pp_memory_pack_defs fmt m =
699	9d693675	Lélio Brun	if not (fst (get_stateless_status m)) then
700	d978c46e	Lélio Brun	fprintf
701			fmt
702			"%a@,%a"
703			pp_machine_ghost_struct
704			m
705			(pp_print_list
706	4fef1a04	Lélio Brun	~pp_sep:pp_print_nothing
707	d978c46e	Lélio Brun	~pp_epilogue:pp_print_cut
708			~pp_open_box:pp_open_vbox0
709	ca7ff3f7	Lélio Brun	(pp_memory_pack_def m))
710			m.mspec.mmemory_packs
711	6d1693b9	Lélio Brun
712			let pp_transition_def m fmt t =
713			let name = t.tname.node_id in
714	4b596770	Lélio Brun	let mem_in = mk_mem_in m in
715			let mem_out = mk_mem_out m in
716	478edbed	Lélio Brun	let stateless = fst (get_stateless_status m) in
717	6d1693b9	Lélio Brun	pp_acsl
718	4b596770	Lélio Brun	(pp_predicate
719	d978c46e	Lélio Brun	(pp_transition
720	478edbed	Lélio Brun	stateless
721	ca7ff3f7	Lélio Brun	(pp_machine_decl' ~ghost:true)
722			(pp_machine_decl' ~ghost:true)
723	0406ab94	Lélio Brun	(pp_local m))
724	6d1693b9	Lélio Brun	(PrintSpec.pp_spec TransitionMode m))
725	4b596770	Lélio Brun	fmt
726	ca7ff3f7	Lélio Brun	((t, (name, mem_in), (name, mem_out)), t.tformula)
727	6d1693b9	Lélio Brun
728			let pp_transition_defs fmt m =
729	d978c46e	Lélio Brun	pp_print_list
730			~pp_epilogue:pp_print_cut
731			~pp_open_box:pp_open_vbox0
732			(pp_transition_def m)
733			fmt
734			m.mspec.mtransitions
735	aaa8e454	Lélio Brun
736			let pp_transition_footprint fmt t =
737	d978c46e	Lélio Brun	fprintf
738			fmt
739			"%s_transition%a_footprint"
740			t.tname.node_id
741	ca7ff3f7	Lélio Brun	(pp_print_option pp_print_int)
742			t.tindex
743	aaa8e454	Lélio Brun
744			let pp_transition_footprint_lemma m fmt t =
745			let name = t.tname.node_id in
746	27502d69	Lélio Brun	let mem_in = mk_mem_in m in
747			let mem_out = mk_mem_out m in
748	478edbed	Lélio Brun	let stateless = fst (get_stateless_status m) in
749	ca7ff3f7	Lélio Brun	let mems =
750	27502d69	Lélio Brun	ISet.(
751			diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)
752			in
753			let insts =
754			IMap.(
755			diff
756			(of_list (List.map (fun (x, (td, _)) -> x, node_name td) m.minstances))
757			t.tinst_footprint)
758	ca7ff3f7	Lélio Brun	in
759			let memories =
760			List.map
761			(fun v -> { v with var_type = { v.var_type with tid = -1 } })
762	27502d69	Lélio Brun	(List.filter (fun v -> ISet.mem v.var_id mems) m.mmemory)
763			in
764			let mems_empty = ISet.is_empty mems in
765			let insts_empty = IMap.is_empty insts in
766			let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
767			let tr ?mems ?insts () =
768	d978c46e	Lélio Brun	Spec_common.mk_transition
769			?mems
770			?insts
771			?i:t.tindex
772	478edbed	Lélio Brun	stateless
773	d978c46e	Lélio Brun	name
774	0406ab94	Lélio Brun	(vdecls_to_vals t.tvars)
775	aaa8e454	Lélio Brun	in
776	4fef1a04	Lélio Brun	if not ((mems_empty && insts_empty) \|\| m.mis_contract) then
777			pp_acsl_cut
778	d978c46e	Lélio Brun	(pp_lemma
779			pp_transition_footprint
780	27502d69	Lélio Brun	(pp_forall
781			(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
782			((if insts_empty then fun pp fmt (_, x) -> pp fmt x
783			else pp_forall (pp_comma_list (pp_machine_decl' ~ghost:true)))
784			((if mems_empty then fun pp fmt (_, x) -> pp fmt x
785			else pp_forall (pp_locals m))
786			(PrintSpec.pp_spec TransitionFootprintMode m)))))
787	aaa8e454	Lélio Brun	fmt
788	ca7ff3f7	Lélio Brun	( t,
789	27502d69	Lélio Brun	( (m.mname.node_id, [ mem_in; mem_out ]),
790			( instances,
791	0406ab94	Lélio Brun	(memories, Forall (t.tvars, Imply (tr (), tr ~mems ~insts ()))) ) )
792			)
793	aaa8e454	Lélio Brun
794			let pp_transition_footprint_lemmas fmt m =
795	d978c46e	Lélio Brun	pp_print_list
796			~pp_epilogue:pp_print_cut
797			~pp_open_box:pp_open_vbox0
798	4fef1a04	Lélio Brun	~pp_sep:pp_print_nothing
799	ca7ff3f7	Lélio Brun	(pp_transition_footprint_lemma m)
800			fmt
801			(List.filter
802			(fun t -> match t.tindex with Some i when i > 0 -> true \| _ -> false)
803			m.mspec.mtransitions)
804	aaa8e454	Lélio Brun
805			let pp_initialization_def fmt m =
806	9d693675	Lélio Brun	if not (fst (get_stateless_status m)) then
807	7f03f62d	Lélio Brun	let name = m.mname.node_id in
808			let mem_in = mk_mem_in m in
809	6d1693b9	Lélio Brun	pp_acsl
810	7f03f62d	Lélio Brun	(pp_predicate
811	6d1693b9	Lélio Brun	(pp_initialization (pp_machine_decl' ~ghost:true))
812	7f03f62d	Lélio Brun	(pp_and_l (fun fmt (i, (td, _)) ->
813	aaa8e454	Lélio Brun	if Arrow.td_is_arrow td then
814			pp_initialization pp_access' fmt (node_name td, (mem_in, i))
815			else
816	ca7ff3f7	Lélio Brun	pp_equal
817			(pp_reset_flag ~indirect:false pp_access')
818	d978c46e	Lélio Brun	pp_print_int
819			fmt
820	aaa8e454	Lélio Brun	((mem_in, i), 1))))
821	7f03f62d	Lélio Brun	fmt
822	6d1693b9	Lélio Brun	((name, (name, mem_in)), m.minstances)
823	7f03f62d	Lélio Brun
824	aaa8e454	Lélio Brun	let pp_reset_cleared_def fmt m =
825			if not (fst (get_stateless_status m)) then
826			let name = m.mname.node_id in
827			let mem_in = mk_mem_in m in
828			let mem_out = mk_mem_out m in
829			pp_acsl
830			(pp_predicate
831			(pp_reset_cleared
832	ca7ff3f7	Lélio Brun	(pp_machine_decl' ~ghost:true)
833			(pp_machine_decl' ~ghost:true))
834	aaa8e454	Lélio Brun	(pp_ite
835			(pp_reset_flag' ~indirect:false)
836			(pp_and
837			(pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
838			pp_initialization')
839			(pp_equal pp_print_string pp_print_string)))
840			fmt
841	ca7ff3f7	Lélio Brun	( (name, (name, mem_in), (name, mem_out)),
842			(mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
843	aaa8e454	Lélio Brun
844	ca7ff3f7	Lélio Brun	let pp_register_chain ?(indirect = true) ptr =
845	efcc8d7f	Lélio Brun	pp_print_list
846	6d1693b9	Lélio Brun	~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
847	ca7ff3f7	Lélio Brun	~pp_epilogue:(fun fmt () ->
848			fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
849	6d1693b9	Lélio Brun	~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
850	efcc8d7f	Lélio Brun	(fun fmt (i, _) -> pp_print_string fmt i)
851
852	ca7ff3f7	Lélio Brun	let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
853	6d1693b9	Lélio Brun	pp_print_list
854			~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
855	aaa8e454	Lélio Brun	~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
856	6d1693b9	Lélio Brun	~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
857			(fun fmt (i, _) -> pp_print_string fmt i)
858	d978c46e	Lélio Brun	fmt
859			mems
860	6d1693b9	Lélio Brun
861	c4780a6a	Lélio Brun	let pp_arrow_reset_ghost mem fmt inst =
862			fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
863
864	ca7ff3f7	Lélio Brun	module GhostProto : MODIFIERS_GHOST_PROTO = struct
865			let pp_ghost_parameters ?(cut = true) fmt vs =
866	d978c46e	Lélio Brun	fprintf
867			fmt
868			"%a%a"
869	ca7ff3f7	Lélio Brun	(if cut then pp_print_cut else pp_print_nothing)
870			()
871	c4780a6a	Lélio Brun	(pp_acsl_line'
872	ca7ff3f7	Lélio Brun	(pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
873	6d1693b9	Lélio Brun	vs
874			end
875
876	efcc8d7f	Lélio Brun	module HdrMod = struct
877	6d1693b9	Lélio Brun	module GhostProto = GhostProto
878
879	d978c46e	Lélio Brun	let pp_machine_decl_prefix _ _ = ()
880	efcc8d7f	Lélio Brun
881	aaa8e454	Lélio Brun	let pp_import_arrow fmt () =
882	d978c46e	Lélio Brun	fprintf
883			fmt
884			"#include \"%s/arrow_spec.h%s\""
885	efcc8d7f	Lélio Brun	(Arrow.arrow_top_decl ()).top_decl_owner
886			(if !Options.cpp then "pp" else "")
887	d978c46e	Lélio Brun
888	18dada08	Lélio Brun	let pp_predicates fmt machines =
889			let pp_preds comment pp =
890			pp_print_list
891			~pp_open_box:pp_open_vbox0
892			~pp_prologue:(pp_print_endcut comment)
893			pp
894			~pp_epilogue:pp_print_cutcut
895			in
896			fprintf
897			fmt
898			"%a%a"
899			(pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
900			machines
901			(pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
902			machines
903	d978c46e	Lélio Brun
904			let pp_machine_alloc_decl fmt m =
905			pp_machine_decl_prefix fmt m;
906			if not (fst (get_stateless_status m)) then
907			if !Options.static_mem then
908			(* Static allocation *)
909			let macro = m, mk_attribute m, mk_instance m in
910			fprintf
911			fmt
912			"%a@,%a@,%a"
913			(pp_static_declare_macro ~ghost:true)
914			macro
915			(pp_static_link_macro ~ghost:true)
916			macro
917			(pp_static_alloc_macro ~ghost:true)
918			macro
919			else
920			(* Dynamic allocation *)
921			(* TODO: handle dynamic alloc *)
922			assert false
923			(* fprintf fmt "extern %a;@,extern %a" pp_alloc_prototype
924			* (m.mname.node_id, m.mstatic)
925			* pp_dealloc_prototype m.mname.node_id *)
926	efcc8d7f	Lélio Brun	end
927	15c3e4e7	Lélio Brun
928	c226a3ba	Lélio Brun	module SrcMod = struct
929	6d1693b9	Lélio Brun	module GhostProto = GhostProto
930
931	d978c46e	Lélio Brun	let pp_predicates fmt machines =
932	aaa8e454	Lélio Brun	let pp_preds comment pp =
933	d978c46e	Lélio Brun	pp_print_list
934			~pp_open_box:pp_open_vbox0
935			~pp_prologue:(pp_print_endcut comment)
936			pp
937			~pp_epilogue:pp_print_cutcut
938	ca7ff3f7	Lélio Brun	in
939	d978c46e	Lélio Brun	fprintf
940			fmt
941			"%a%a%a%a%a%a"
942	ca7ff3f7	Lélio Brun	(pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
943			machines
944			(pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
945			machines
946			(pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
947			machines
948			(pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
949			machines
950			(pp_preds "/* ACSL transition annotations */" pp_transition_defs)
951			machines
952	d978c46e	Lélio Brun	(pp_preds
953			"/* ACSL transition memory footprints lemmas */"
954	ca7ff3f7	Lélio Brun	pp_transition_footprint_lemmas)
955			machines
956	c226a3ba	Lélio Brun
957	c4780a6a	Lélio Brun	let pp_clear_reset_spec fmt self mem m =
958	c226a3ba	Lélio Brun	let name = m.mname.node_id in
959	ca7ff3f7	Lélio Brun	let arws, narws =
960			List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
961			in
962			let mk_insts = List.map (fun x -> [ x ]) in
963			pp_acsl_cut
964			(fun fmt () ->
965	d978c46e	Lélio Brun	fprintf
966			fmt
967	ca7ff3f7	Lélio Brun	"%a@,\
968			%a@,\
969			%a@,\
970			%a@,\
971			%a@,\
972			%a@,\
973			%a@,\
974			%a@,\
975			%a@,\
976			%a@,\
977			@[<v 2>behavior reset:@;\
978			%a@,\
979			%a@]@,\
980			@[<v 2>behavior no_reset:@;\
981			%a@,\
982			%a@]@,\
983			complete behaviors;@,\
984			disjoint behaviors;"
985			(pp_requires pp_mem_valid')
986			(name, self)
987	18dada08	Lélio Brun	(pp_requires (pp_separated' self mem))
988	ca7ff3f7	Lélio Brun	(mk_insts m.minstances, [])
989	c4780a6a	Lélio Brun	(pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
990			(name, mem, self)
991	ca7ff3f7	Lélio Brun	(pp_ensures
992			(pp_memory_pack_aux
993			~i:(List.length m.mspec.mmemory_packs - 2)
994	d978c46e	Lélio Brun	pp_ptr
995			pp_print_string))
996	6d1693b9	Lélio Brun	(name, mem, self)
997	ca7ff3f7	Lélio Brun	(pp_assigns pp_reset_flag')
998			[ self ]
999			(pp_assigns (pp_register_chain self))
1000			(mk_insts arws)
1001			(pp_assigns (pp_reset_flag_chain self))
1002			(mk_insts narws)
1003			(pp_assigns pp_reset_flag')
1004			[ mem ]
1005			(pp_assigns (pp_register_chain ~indirect:false mem))
1006			(mk_insts arws)
1007			(pp_assigns (pp_reset_flag_chain ~indirect:false mem))
1008			(mk_insts narws)
1009			(pp_assumes (pp_equal pp_reset_flag' pp_print_int))
1010			(mem, 1)
1011			(pp_ensures (pp_initialization pp_ptr))
1012			(name, mem)
1013			(pp_assumes (pp_equal pp_reset_flag' pp_print_int))
1014			(mem, 0)
1015			(pp_ensures (pp_equal pp_ptr (pp_old pp_ptr)))
1016			(mem, mem))
1017	d978c46e	Lélio Brun	fmt
1018			()
1019	c226a3ba	Lélio Brun
1020	6d1693b9	Lélio Brun	let pp_set_reset_spec fmt self mem m =
1021			let name = m.mname.node_id in
1022	ca7ff3f7	Lélio Brun	pp_acsl_cut
1023			(fun fmt () ->
1024	d978c46e	Lélio Brun	fprintf
1025			fmt
1026			"%a@,%a@,%a"
1027	ca7ff3f7	Lélio Brun	(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
1028			(name, mem, self)
1029			(pp_ensures (pp_equal pp_reset_flag' pp_print_int))
1030			(mem, 1)
1031			(pp_assigns pp_reset_flag')
1032			[ self; mem ])
1033	d978c46e	Lélio Brun	fmt
1034			()
1035	6d1693b9	Lélio Brun
1036	d29fbec5	Lélio Brun	let spec_from_contract c = Spec_common.red (Imply (c.mc_pre, c.mc_post))
1037	dccec723	Lélio Brun
1038			let pp_contract m fmt c =
1039			PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (spec_from_contract c)
1040
1041			let contract_of machines m =
1042			match m.mspec.mnode_spec with
1043	d29fbec5	Lélio Brun	\| Some spec -> (
1044			match spec with
1045			\| Contract c ->
1046			Some c, None
1047			\| NodeSpec f -> (
1048			let m_f = find_machine f machines in
1049			match m_f.mspec.mnode_spec with
1050			\| Some (Contract c) ->
1051			Some c, Some m_f
1052			\| _ ->
1053			None, None))
1054	dccec723	Lélio Brun	\| None ->
1055			None, None
1056
1057			let pp_init_def fmt m =
1058			let name = m.mname.node_id in
1059			let mem = mk_mem m in
1060			pp_predicate
1061			(pp_init (pp_machine_decl' ~ghost:true))
1062			(pp_and pp_initialization' (pp_reset_flag' ~indirect:false))
1063			fmt
1064			((name, (name, mem)), ((name, mem), mem))
1065
1066			let rename n x = sprintf "%s_%d" x n
1067
1068			let rename_var_decl n vd = { vd with var_id = rename n vd.var_id }
1069
1070			let rec rename_value n v =
1071	d29fbec5	Lélio Brun	{
1072			v with
1073			value_desc =
1074			(match v.value_desc with
1075			\| Machine_code_types.Var v ->
1076			Machine_code_types.Var (rename_var_decl n v)
1077			\| Fun (f, vs) ->
1078			Fun (f, List.map (rename_value n) vs)
1079			\| Array vs ->
1080			Array (List.map (rename_value n) vs)
1081			\| Access (v1, v2) ->
1082			Access (rename_value n v1, rename_value n v2)
1083			\| Power (v1, v2) ->
1084			Power (rename_value n v1, rename_value n v2)
1085			\| v ->
1086			v);
1087	dccec723	Lélio Brun	}
1088
1089	10131419	Lélio Brun	let rename_expression n = function
1090	d29fbec5	Lélio Brun	\| Val v ->
1091			Val (rename_value n v)
1092			\| Var v ->
1093			Var (rename_var_decl n v)
1094			\| e ->
1095			e
1096	dccec723	Lélio Brun
1097			let rename_predicate n = function
1098	478edbed	Lélio Brun	\| Transition (s, f, inst, i, es, r, mf, mif) ->
1099			Transition (s, f, inst, i, List.map (rename_expression n) es, r, mf, mif)
1100	d29fbec5	Lélio Brun	\| p ->
1101			p
1102	dccec723	Lélio Brun
1103			let rec rename_formula n = function
1104	d29fbec5	Lélio Brun	\| Equal (e1, e2) ->
1105			Equal (rename_expression n e1, rename_expression n e2)
1106			\| And fs ->
1107			And (List.map (rename_formula n) fs)
1108			\| Or fs ->
1109			Or (List.map (rename_formula n) fs)
1110			\| Imply (f1, f2) ->
1111			Imply (rename_formula n f1, rename_formula n f2)
1112			\| Exists (xs, f) ->
1113			Exists (List.map (rename_var_decl n) xs, rename_formula n f)
1114			\| Forall (xs, f) ->
1115			Forall (List.map (rename_var_decl n) xs, rename_formula n f)
1116			\| Ternary (e, t, f) ->
1117			Ternary (rename_expression n e, rename_formula n t, rename_formula n f)
1118			\| Predicate p ->
1119			Predicate (rename_predicate n p)
1120			\| ExistsMem (x, f1, f2) ->
1121			ExistsMem (rename n x, rename_formula n f1, rename_formula n f2)
1122			\| Value v ->
1123			Value (rename_value n v)
1124			\| f ->
1125			f
1126
1127	dccec723	Lélio Brun	let rename_contract n c =
1128	d29fbec5	Lélio Brun	{
1129			c with
1130	dccec723	Lélio Brun	mc_pre = rename_formula n c.mc_pre;
1131	d29fbec5	Lélio Brun	mc_post = rename_formula n c.mc_post;
1132			}
1133	dccec723	Lélio Brun
1134	d29fbec5	Lélio Brun	let but_last l = List.(rev (tl (rev l)))
1135	dccec723	Lélio Brun
1136	d29fbec5	Lélio Brun	let pp_k_induction_case case m pp_mem_in pp_mem_out pp_vars fmt
1137			(n, mem_in, mem_out) =
1138	dccec723	Lélio Brun	let name = m.mname.node_id in
1139			let inputs = m.mstep.step_inputs in
1140			let outputs = m.mstep.step_outputs in
1141	d29fbec5	Lélio Brun	fprintf
1142			fmt
1143			"%s_%s_%d(@[<hov>%a,@;%a,@;%a@])"
1144	dccec723	Lélio Brun	name
1145			case
1146			n
1147			pp_mem_in
1148			mem_in
1149			pp_vars
1150			(inputs @ outputs)
1151			pp_mem_out
1152			mem_out
1153
1154	d29fbec5	Lélio Brun	let pp_k_induction_base_case m = pp_k_induction_case "base" m
1155	dccec723	Lélio Brun
1156	d29fbec5	Lélio Brun	let pp_k_induction_inductive_case m = pp_k_induction_case "inductive" m
1157	dccec723	Lélio Brun
1158			let pp_base_cases m fmt (c, m_c, k) =
1159			let name = m.mname.node_id in
1160	d29fbec5	Lélio Brun	let name_c = m_c.mname.node_id in
1161	dccec723	Lélio Brun	let mem = mk_mem m in
1162	d29fbec5	Lélio Brun	let mem_c = mk_mem_c m in
1163	dccec723	Lélio Brun	let inputs = m.mstep.step_inputs in
1164			let outputs = m.mstep.step_outputs in
1165	478edbed	Lélio Brun	let stateless = fst (get_stateless_status m) in
1166			let stateless_c = fst (get_stateless_status m_c) in
1167	dccec723	Lélio Brun	let l = List.init (k - 1) (fun n -> n + 1) in
1168	d29fbec5	Lélio Brun	pp_print_list
1169			~pp_open_box:pp_open_vbox0
1170			~pp_sep:pp_print_cutcut
1171	dccec723	Lélio Brun	(fun fmt n ->
1172	d29fbec5	Lélio Brun	let l = List.init (n + 1) (fun n -> n) in
1173			let pp fmt =
1174			let pp =
1175			pp_implies
1176			(pp_and_l (fun fmt -> function
1177			\| 0 ->
1178			let pp = pp_init pp_print_string in
1179			(if stateless_c then fun fmt (x, _) -> pp fmt x
1180			else pp_and pp pp)
1181			fmt
1182			((name, rename 0 mem), (name_c, rename 0 mem_c))
1183			\| n' ->
1184			let pp_var_c fmt (out, vd) =
1185			if out && n' < n then pp_true_c_bool fmt ()
1186			else pp_var_decl fmt vd
1187			in
1188			let c_inputs =
1189			List.map
1190			(fun v -> false, rename_var_decl n' v)
1191			m_c.mstep.step_inputs
1192			in
1193			let c_outputs =
1194			List.map
1195			(fun v -> true, rename_var_decl n' v)
1196			m_c.mstep.step_outputs
1197			in
1198			let pp stateless pp_var =
1199			pp_transition_aux
1200			stateless
1201			pp_print_string
1202			pp_print_string
1203			pp_var
1204			in
1205			pp_and
1206			(pp stateless pp_var_decl)
1207			(pp stateless_c pp_var_c)
1208			fmt
1209			( ( name,
1210			List.map (rename_var_decl n') (inputs @ outputs),
1211			rename (n' - 1) mem,
1212			rename n' mem ),
1213			( name_c,
1214			c_inputs @ c_outputs,
1215			rename (n' - 1) mem_c,
1216			rename n' mem_c ) )))
1217			(pp_contract m)
1218			in
1219			if stateless_c then pp fmt
1220			else fun x ->
1221			pp_forall
1222			(pp_machine_decl
1223			~ghost:true
1224			(pp_comma_list (fun fmt n ->
1225			pp_print_string fmt (rename n mem_c))))
1226			pp
1227			fmt
1228			((name_c, l), x)
1229			in
1230			pp_predicate
1231			(pp_k_induction_base_case
1232			m
1233			(pp_machine_decl' ~ghost:true)
1234			(pp_machine_decl' ~ghost:true)
1235			(fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl n) xs)))
1236			(pp_forall
1237			(pp_locals m)
1238			(if n > 1 then
1239			pp_forall
1240			(fun fmt l ->
1241			fprintf
1242			fmt
1243			"%a@,%a"
1244			(pp_machine_decl
1245			~ghost:true
1246			(pp_comma_list ~pp_eol:pp_print_comma (fun fmt n ->
1247			pp_print_string fmt (rename n mem))))
1248			(name, but_last l)
1249			(pp_locals m)
1250			(List.flatten
1251			(List.map
1252			(fun n ->
1253			List.map (rename_var_decl n) (inputs @ outputs))
1254			(List.tl l))))
1255			pp
1256			else fun fmt (_, x) -> pp fmt x))
1257			fmt
1258			( (n, (name, rename (n - 1) mem), (name, rename n mem)),
1259			( List.map (rename_var_decl n) m_c.mstep.step_outputs,
1260			(but_last l, (l, rename_contract n c)) ) ))
1261			fmt
1262			l
1263	dccec723	Lélio Brun
1264			let pp_inductive_case m fmt (c, m_c, k) =
1265			let name = m.mname.node_id in
1266			let mem = mk_mem m in
1267	4fef1a04	Lélio Brun	let mem_c = mk_mem_c m_c in
1268	dccec723	Lélio Brun	let inputs = m.mstep.step_inputs in
1269			let outputs = m.mstep.step_outputs in
1270	478edbed	Lélio Brun	let stateless = fst (get_stateless_status m) in
1271			let stateless_c = fst (get_stateless_status m_c) in
1272	dccec723	Lélio Brun	let l = List.init k (fun n -> n + 1) in
1273	4fef1a04	Lélio Brun	let l' = 0 :: l in
1274			let pp fmt =
1275			let pp =
1276			pp_implies
1277			(pp_and_l (fun fmt n ->
1278	d29fbec5	Lélio Brun	let pp_var_c fmt (out, vd) =
1279			if out && n < k then pp_true_c_bool fmt ()
1280			else pp_var_decl fmt vd
1281			in
1282			let c_inputs =
1283			List.map
1284			(fun v -> false, rename_var_decl n v)
1285			m_c.mstep.step_inputs
1286			in
1287			let c_outputs =
1288			List.map
1289			(fun v -> true, rename_var_decl n v)
1290			m_c.mstep.step_outputs
1291	4fef1a04	Lélio Brun	in
1292			pp_and
1293	d29fbec5	Lélio Brun	(pp_transition_aux
1294			stateless
1295			pp_print_string
1296			pp_print_string
1297			pp_var_decl)
1298			(pp_transition_aux
1299			stateless_c
1300			pp_print_string
1301			pp_print_string
1302			pp_var_c)
1303	4fef1a04	Lélio Brun	fmt
1304	d29fbec5	Lélio Brun	( ( name,
1305			List.map (rename_var_decl n) (inputs @ outputs),
1306			rename (n - 1) mem,
1307			rename n mem ),
1308			( m_c.mname.node_id,
1309			c_inputs @ c_outputs,
1310			rename (n - 1) mem_c,
1311			rename n mem_c ) )))
1312	4fef1a04	Lélio Brun	(pp_contract m)
1313			in
1314			if stateless_c then pp fmt
1315			else fun x ->
1316			pp_forall
1317	d29fbec5	Lélio Brun	(pp_machine_decl
1318			~ghost:true
1319	4fef1a04	Lélio Brun	(pp_comma_list (fun fmt n -> pp_print_string fmt (rename n mem_c))))
1320			pp
1321			fmt
1322			((m_c.mname.node_id, l'), x)
1323	dccec723	Lélio Brun	in
1324			pp_predicate
1325			(pp_k_induction_inductive_case
1326			m
1327			(pp_machine_decl' ~ghost:true)
1328			(pp_machine_decl' ~ghost:true)
1329			(fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl k) xs)))
1330	d29fbec5	Lélio Brun	(pp_forall
1331			(pp_locals m)
1332	dccec723	Lélio Brun	(if k > 1 then
1333	d29fbec5	Lélio Brun	pp_forall
1334			(fun fmt l ->
1335			fprintf
1336			fmt
1337			"%a@,%a"
1338			(pp_machine_decl
1339			~ghost:true
1340			(pp_comma_list ~pp_eol:pp_print_comma (fun fmt n ->
1341			pp_print_string fmt (rename (n - 1) mem))))
1342			(name, but_last l)
1343			(pp_locals m)
1344			(List.flatten
1345			(List.map
1346			(fun n ->
1347			List.map (rename_var_decl (n - 1)) (inputs @ outputs))
1348			(List.tl l))))
1349			pp
1350			else fun fmt (_, x) -> pp fmt x))
1351	dccec723	Lélio Brun	fmt
1352	d29fbec5	Lélio Brun	( (k, (name, rename (k - 1) mem), (name, rename k mem)),
1353			( List.map (rename_var_decl k) m_c.mstep.step_outputs,
1354			(l, (l, rename_contract k c)) ) )
1355	dccec723	Lélio Brun
1356			let pp_k_induction_lemmas m fmt k =
1357			let name = m.mname.node_id in
1358			let mem_in = mk_mem_in m in
1359			let mem_out = mk_mem_out m in
1360			let inputs = m.mstep.step_inputs in
1361			let outputs = m.mstep.step_outputs in
1362			let l = List.init k (fun n -> n + 1) in
1363	d29fbec5	Lélio Brun	pp_print_list
1364			~pp_open_box:pp_open_vbox0
1365			~pp_sep:pp_print_cutcut
1366	dccec723	Lélio Brun	(fun fmt n ->
1367	d29fbec5	Lélio Brun	pp_lemma
1368			(fun fmt n -> fprintf fmt "%s_k_induction_%d" name n)
1369			(pp_forall
1370			(fun fmt () ->
1371			fprintf
1372			fmt
1373			"%a,@;%a"
1374			(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
1375			(name, [ mem_in; mem_out ])
1376			(pp_locals m)
1377			(inputs @ outputs))
1378			((if n = k then pp_k_induction_inductive_case
1379			else pp_k_induction_base_case)
1380			m
1381			pp_print_string
1382			pp_print_string
1383			(pp_comma_list pp_var_decl)))
1384			fmt
1385			(n, ((), (n, mem_in, mem_out))))
1386	dccec723	Lélio Brun	fmt
1387			l
1388
1389			let pp_k_induction_axiom m fmt (c, m_c, k) =
1390			let name = m.mname.node_id in
1391			let mem_in = mk_mem_in m in
1392			let mem_out = mk_mem_out m in
1393	4fef1a04	Lélio Brun	let mem_in_c = mk_mem_in_c m_c in
1394			let mem_out_c = mk_mem_out_c m_c in
1395	dccec723	Lélio Brun	let inputs = m.mstep.step_inputs in
1396			let outputs = m.mstep.step_outputs in
1397	d29fbec5	Lélio Brun	let stateless = fst (get_stateless_status m) in
1398	478edbed	Lélio Brun	let stateless_c = fst (get_stateless_status m_c) in
1399	dccec723	Lélio Brun	let l = List.init k (fun n -> n + 1) in
1400	4fef1a04	Lélio Brun	let pp =
1401			pp_implies
1402	d29fbec5	Lélio Brun	(pp_and_l (fun fmt n ->
1403			(if n = k then pp_k_induction_inductive_case
1404			else pp_k_induction_base_case)
1405			m
1406			pp_print_string
1407			pp_print_string
1408			(pp_comma_list pp_var_decl)
1409			fmt
1410			(n, mem_in, mem_out)))
1411			(pp_forall
1412			(pp_locals m)
1413			(pp_implies
1414			(pp_and
1415			(pp_transition_aux
1416			stateless
1417			pp_print_string
1418			pp_print_string
1419			pp_var_decl)
1420			(pp_transition_aux
1421			stateless_c
1422			pp_print_string
1423			pp_print_string
1424			pp_var_decl))
1425			(pp_contract m)))
1426	4fef1a04	Lélio Brun	in
1427	dccec723	Lélio Brun	pp_axiomatic
1428			(fun fmt () -> fprintf fmt "%s_k_Induction" name)
1429			(pp_axiom
1430			(fun fmt () -> fprintf fmt "%s_k_induction" name)
1431			(pp_forall
1432	d29fbec5	Lélio Brun	(fun fmt () ->
1433			fprintf
1434			fmt
1435			"%a,@;%a"
1436			(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
1437			(name, [ mem_in; mem_out ])
1438			(pp_locals m)
1439			(inputs @ outputs))
1440			(if stateless_c then pp
1441			else fun fmt x ->
1442			pp_forall
1443			(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
1444			pp
1445			fmt
1446			((m_c.mname.node_id, [ mem_in_c; mem_out_c ]), x))))
1447	dccec723	Lélio Brun	fmt
1448	d29fbec5	Lélio Brun	( (),
1449			( (),
1450			( (),
1451			( l,
1452			( m_c.mstep.step_outputs,
1453			( ( (name, inputs @ outputs, mem_in, mem_out),
1454			( m_c.mname.node_id,
1455			m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
1456			mem_in_c,
1457			mem_out_c ) ),
1458			c ) ) ) ) ) )
1459
1460			let pp_k_induction m fmt ((_, m_c, k) as c_m_k) =
1461			let stateless_c = fst (get_stateless_status m_c) in
1462	dccec723	Lélio Brun	pp_acsl_cut
1463	d29fbec5	Lélio Brun	(fun fmt () ->
1464			fprintf
1465			fmt
1466			"%a@,@,%a@,@,%a@,@,%a@,@,%a@,@,%a"
1467			pp_init_def
1468			m
1469			(if stateless_c then pp_print_nothing else pp_init_def)
1470			m_c
1471			(pp_base_cases m)
1472			c_m_k
1473			(pp_inductive_case m)
1474			c_m_k
1475			(pp_k_induction_lemmas m)
1476			k
1477			(pp_k_induction_axiom m)
1478			c_m_k)
1479	dccec723	Lélio Brun	fmt
1480			()
1481
1482			let pp_proof_annotation m m_c fmt c =
1483			let pp m_c fmt = function
1484			\| Kinduction k ->
1485			pp_k_induction m fmt (c, m_c, k)
1486			in
1487			match m_c with
1488			\| Some m_c ->
1489			pp_print_option (pp m_c) fmt c.mc_proof
1490	d29fbec5	Lélio Brun	\| None ->
1491			()
1492	5b98398a	Lélio Brun
1493	6d1693b9	Lélio Brun	let pp_step_spec fmt machines self mem m =
1494	c226a3ba	Lélio Brun	let name = m.mname.node_id in
1495	8d2d6fa0	Lélio Brun	let insts = instances machines m in
1496			let insts' = powerset_instances insts in
1497	ca7ff3f7	Lélio Brun	let insts'' =
1498			List.(
1499			filter
1500			(fun l -> l <> [])
1501			(map (filter (fun (_, (td, _)) -> not (Arrow.td_is_arrow td))) insts))
1502			in
1503	6d1693b9	Lélio Brun	let inputs = m.mstep.step_inputs in
1504			let outputs = m.mstep.step_outputs in
1505	478edbed	Lélio Brun	let stateless = fst (get_stateless_status m) in
1506	d29fbec5	Lélio Brun	let pp_if_outputs pp = if outputs = [] then pp_print_nothing else pp in
1507	dccec723	Lélio Brun	let c, m_c = contract_of machines m in
1508	d29fbec5	Lélio Brun	let pp_spec =
1509			pp_print_option
1510			(if m.mis_contract then pp_print_nothing
1511			else fun fmt c ->
1512			pp_print_option
1513			(fun fmt m_c ->
1514			let mem_in = mk_mem_in_c m_c in
1515			let mem_out = mk_mem_out_c m_c in
1516			let stateless_c = fst (get_stateless_status m_c) in
1517			pp_ensures
1518			(pp_implies
1519			(pp_transition_aux
1520			stateless_c
1521			pp_print_string
1522			pp_print_string
1523			(fun fmt v ->
1524			(if is_output m v then pp_ptr_decl else pp_var_decl)
1525			fmt
1526			v))
1527			(pp_contract m))
1528			fmt
1529			( ( m_c.mname.node_id,
1530			m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
1531			mem_in,
1532			mem_out ),
1533			c ))
1534			fmt
1535			m_c)
1536			in
1537			let pp_spec_vars =
1538			match m_c with
1539			\| Some m_c ->
1540			let mem_in = mk_mem_in_c m_c in
1541			let mem_out = mk_mem_out_c m_c in
1542			let stateless_c = fst (get_stateless_status m_c) in
1543	dccec723	Lélio Brun	pp_acsl_cut
1544	d29fbec5	Lélio Brun	(pp_ghost (fun fmt () ->
1545			fprintf
1546			fmt
1547			"@;<0 2>@[<v>%a%a@]"
1548			(pp_print_list
1549			~pp_open_box:pp_open_vbox0
1550			~pp_sep:pp_print_semicolon
1551			~pp_eol:pp_print_semicolon
1552			(pp_c_decl_local_var m))
1553			m_c.mstep.step_outputs
1554			(if stateless_c then pp_print_nothing
1555			else
1556			pp_machine_decl
1557			~ghost:true
1558			(pp_comma_list ~pp_eol:pp_print_semicolon pp_print_string))
1559			(m_c.mname.node_id, [ mem_in; mem_out ])))
1560			\| _ ->
1561			pp_print_nothing
1562	dccec723	Lélio Brun	in
1563			pp_print_option (pp_proof_annotation m m_c) fmt c;
1564			pp_spec_vars fmt ();
1565	ca7ff3f7	Lélio Brun	pp_acsl_cut
1566			(fun fmt () ->
1567	478edbed	Lélio Brun	if stateless then
1568	d978c46e	Lélio Brun	fprintf
1569			fmt
1570	d29fbec5	Lélio Brun	"%a@,%a@,%a@,%a@,%a"
1571	5b98398a	Lélio Brun	(pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
1572	ca7ff3f7	Lélio Brun	outputs
1573	5b98398a	Lélio Brun	(pp_if_outputs (pp_requires pp_separated''))
1574	d978c46e	Lélio Brun	outputs
1575			(pp_assigns pp_ptr_decl)
1576			outputs
1577	50a8778a	Lélio Brun	(pp_ensures (pp_transition_aux' m))
1578	0406ab94	Lélio Brun	(name, inputs @ outputs, "", "")
1579	70710795	Lélio Brun	pp_spec
1580	dccec723	Lélio Brun	c
1581	9d693675	Lélio Brun	else
1582	d978c46e	Lélio Brun	fprintf
1583			fmt
1584	d29fbec5	Lélio Brun	"%a@,\
1585			%a@,\
1586			%a@,\
1587			%a@,\
1588			%a@,\
1589			%a@,\
1590			%a@,\
1591			%a@,\
1592			%a@,\
1593			%a@,\
1594			%a@,\
1595			%a@,\
1596			%a@,\
1597			%a@,\
1598			%a@,\
1599			%a@,\
1600			%a@,\
1601			%a"
1602	5b98398a	Lélio Brun	(pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
1603	ca7ff3f7	Lélio Brun	outputs
1604			(pp_requires pp_mem_valid')
1605			(name, self)
1606	18dada08	Lélio Brun	(pp_requires (pp_separated' self mem))
1607	ca7ff3f7	Lélio Brun	(insts', outputs)
1608	6d1693b9	Lélio Brun	(pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
1609			(name, mem, self)
1610	aaa8e454	Lélio Brun	(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
1611			(name, mem, self)
1612	ca7ff3f7	Lélio Brun	(pp_ensures
1613	478edbed	Lélio Brun	(pp_transition_aux stateless (pp_old pp_ptr) pp_ptr (fun fmt v ->
1614	0406ab94	Lélio Brun	(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
1615			(name, inputs @ outputs, mem, mem)
1616	70710795	Lélio Brun	pp_spec
1617	dccec723	Lélio Brun	c
1618	d978c46e	Lélio Brun	(pp_assigns pp_ptr_decl)
1619			outputs
1620	ca7ff3f7	Lélio Brun	(pp_assigns (pp_reg self))
1621			m.mmemory
1622			(pp_assigns pp_reset_flag')
1623			[ self ]
1624			(pp_assigns (pp_memory self))
1625			(memories insts')
1626			(pp_assigns (pp_register_chain self))
1627			insts
1628			(pp_assigns (pp_reset_flag_chain self))
1629			insts''
1630			(pp_assigns (pp_reg mem))
1631			m.mmemory
1632			(pp_assigns pp_reset_flag')
1633			[ mem ]
1634			(pp_assigns (pp_memory ~indirect:false mem))
1635			(memories insts')
1636			(pp_assigns (pp_register_chain ~indirect:false mem))
1637			insts
1638			(pp_assigns (pp_reset_flag_chain ~indirect:false mem))
1639			insts'')
1640	d978c46e	Lélio Brun	fmt
1641			()
1642	c226a3ba	Lélio Brun
1643	ca7ff3f7	Lélio Brun	let pp_ghost_instr_code m self fmt instr =
1644			match instr.instr_desc with
1645	c4780a6a	Lélio Brun	\| MStateAssign (x, v) ->
1646	d978c46e	Lélio Brun	fprintf
1647			fmt
1648			"@,%a"
1649	ca7ff3f7	Lélio Brun	(pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m))))
1650	c4780a6a	Lélio Brun	(x, v)
1651			\| MResetAssign b ->
1652	ca7ff3f7	Lélio Brun	fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b
1653	c4780a6a	Lélio Brun	\| MSetReset inst ->
1654			let td, _ = List.assoc inst m.minstances in
1655			if Arrow.td_is_arrow td then
1656	d978c46e	Lélio Brun	fprintf
1657			fmt
1658			"@,%a;"
1659	ca7ff3f7	Lélio Brun	(pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self)))
1660			inst
1661			\| _ ->
1662			()
1663	c4780a6a	Lélio Brun
1664			let pp_step_instr_spec m self mem fmt instr =
1665	5b98398a	Lélio Brun	let ghost = m.mis_contract in
1666	d978c46e	Lélio Brun	fprintf
1667			fmt
1668			"%a%a"
1669	ca7ff3f7	Lélio Brun	(pp_ghost_instr_code m mem)
1670			instr
1671	d978c46e	Lélio Brun	(pp_print_list
1672			~pp_open_box:pp_open_vbox0
1673			~pp_prologue:pp_print_cut
1674	d29fbec5	Lélio Brun	(pp_acsl_line'
1675			~ghost
1676			(pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
1677	6d1693b9	Lélio Brun	instr.instr_spec
1678
1679	c4780a6a	Lélio Brun	let pp_ghost_parameter mem fmt inst =
1680	d978c46e	Lélio Brun	GhostProto.pp_ghost_parameters
1681			~cut:false
1682			fmt
1683	c4780a6a	Lélio Brun	(match inst with
1684	ca7ff3f7	Lélio Brun	\| Some inst ->
1685	d978c46e	Lélio Brun	[ (inst, fun fmt inst -> pp_ref pp_indirect' fmt (mem, inst)) ]
1686	ca7ff3f7	Lélio Brun	\| None ->
1687			[ mem, pp_print_string ])
1688	5b98398a	Lélio Brun
1689	e164af45	Lélio Brun	let pp_contract fmt machines _self mem m =
1690			let pp_vars ?pp_eol = pp_comma_list ?pp_eol (pp_c_var_read m) in
1691			match contract_of machines m with
1692	0988cb68	Lélio Brun	\| Some c, Some _ ->
1693	d29fbec5	Lélio Brun	pp_print_option
1694			(pp_acsl_cut (fun fmt -> function
1695			\| Kinduction k ->
1696			let l = List.init k (fun n -> n + 1) in
1697			let pp_mem_in = pp_at_pre pp_ptr in
1698			let pp_mem_out = pp_ptr in
1699			pp_assert
1700			(pp_and_l (fun fmt n ->
1701			(if n = k then pp_k_induction_inductive_case
1702			else pp_k_induction_base_case)
1703			m
1704			pp_mem_in
1705			pp_mem_out
1706			pp_vars
1707			fmt
1708			(n, mem, mem)))
1709			fmt
1710			l))
1711			fmt
1712			c.mc_proof
1713			\| _, _ ->
1714			()
1715	c226a3ba	Lélio Brun	end
1716
1717	d978c46e	Lélio Brun	module MainMod = struct
1718			let main_mem_ghost = "main_mem_ghost"
1719
1720			let pp_declare_ghost_state fmt name =
1721			pp_acsl_line'_cut
1722			(pp_ghost (fun fmt () ->
1723			fprintf
1724			fmt
1725			"%a(,%s);"
1726			(pp_machine_static_alloc_name ~ghost:true)
1727			name
1728			main_mem_ghost))
1729			fmt
1730			()
1731
1732			let pp_ghost_state_parameter fmt () =
1733			GhostProto.pp_ghost_parameters
1734			~cut:false
1735			fmt
1736			[ main_mem_ghost, pp_ref pp_print_string ]
1737
1738	18dada08	Lélio Brun	let pp_main_loop_invariants main_mem machines fmt m =
1739			let name = m.mname.node_id in
1740			let insts = powerset_instances (instances machines m) in
1741	d978c46e	Lélio Brun	pp_acsl_cut
1742			(fun fmt () ->
1743			fprintf
1744			fmt
1745	18dada08	Lélio Brun	"%a@,%a@,%a@,%a"
1746			(pp_loop_invariant pp_mem_valid')
1747			(name, main_mem)
1748			(pp_loop_invariant
1749			(pp_memory_pack_aux pp_print_string pp_print_string))
1750			(name, main_mem_ghost, main_mem)
1751			(pp_loop_invariant
1752			(pp_separated
1753			(pp_paren pp_print_string)
1754			pp_ref'
1755			(pp_ref pp_var_decl)))
1756			(main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
1757	f1518c7c	Lélio Brun	(pp_loop_invariant
1758	d29fbec5	Lélio Brun	(pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
1759	f1518c7c	Lélio Brun	((), ((), ())))
1760	18dada08	Lélio Brun	fmt
1761			()
1762
1763			let pp_main_spec fmt =
1764			pp_acsl_cut
1765			(fun fmt () ->
1766			fprintf
1767			fmt
1768			"%a@,%a@,%a@,%a"
1769	f1518c7c	Lélio Brun	(pp_requires
1770	d29fbec5	Lélio Brun	(pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
1771	f1518c7c	Lélio Brun	((), ((), ()))
1772	18dada08	Lélio Brun	(pp_terminates pp_false)
1773			()
1774	d978c46e	Lélio Brun	(pp_ensures pp_false)
1775			()
1776	18dada08	Lélio Brun	(pp_assigns pp_nothing)
1777			[ () ])
1778	d978c46e	Lélio Brun	fmt
1779			()
1780			end
1781
1782	d4107cf2	ploc	(**************************************************************************)
1783			(* MAKEFILE *)
1784			(**************************************************************************)
1785
1786	c226a3ba	Lélio Brun	module MakefileMod = struct
1787	b2ad5de3	Lélio Brun	let pp_print_dependencies = C_backend_makefile.fprintf_dependencies "_spec"
1788
1789			let pp_arrow_o fmt () = pp_print_string fmt "arrow_spec.o"
1790
1791	c226a3ba	Lélio Brun	let other_targets fmt basename _nodename dependencies =
1792			fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
1793			(* EACSL version of library file . c *)
1794			fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
1795	d978c46e	Lélio Brun	fprintf
1796			fmt
1797	ca7ff3f7	Lélio Brun	"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
1798			e-acsl -print -ocode %s_eacsl.c@."
1799	d978c46e	Lélio Brun	basename
1800			basename;
1801	c226a3ba	Lélio Brun	fprintf fmt "@.";
1802			fprintf fmt "@.";
1803
1804	ca7ff3f7	Lélio Brun	(* EACSL version of library file . c + main .c *)
1805	d978c46e	Lélio Brun	fprintf
1806			fmt
1807			"%s_main_eacsl.c: %s.c %s.h %s_main.c@."
1808			basename
1809			basename
1810			basename
1811			basename;
1812			fprintf
1813			fmt
1814	ca7ff3f7	Lélio Brun	"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \
1815			-then-on e-acsl -print -ocode %s_main_eacsl.i@."
1816	d978c46e	Lélio Brun	basename
1817			basename
1818			basename;
1819	c226a3ba	Lélio Brun	(* Ugly hack to deal with eacsl bugs *)
1820	d978c46e	Lélio Brun	fprintf
1821			fmt
1822			"\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c"
1823			basename
1824			basename;
1825	c226a3ba	Lélio Brun	fprintf fmt "@.";
1826			fprintf fmt "@.";
1827
1828			(* EACSL version of binary *)
1829			fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
1830	d978c46e	Lélio Brun	fprintf
1831			fmt
1832			"\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
1833	ca7ff3f7	Lélio Brun	basename;
1834			(* compiling instrumented lib + main *)
1835	b2ad5de3	Lélio Brun	pp_print_dependencies fmt dependencies;
1836	d978c46e	Lélio Brun	fprintf
1837			fmt
1838	ca7ff3f7	Lélio Brun	"\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
1839			%s_main_eacsl.o %a@."
1840	c226a3ba	Lélio Brun	basename
1841	a7062da6	Lélio Brun	(pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name))
1842	c226a3ba	Lélio Brun	(C_backend_makefile.compiled_dependencies dependencies)
1843			("${FRAMACEACSL}/e_acsl.c "
1844	ca7ff3f7	Lélio Brun	^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
1845			^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
1846	c226a3ba	Lélio Brun	basename
1847	a7062da6	Lélio Brun	(pp_print_list (fun fmt lib -> fprintf fmt "-l%s" lib))
1848	ca7ff3f7	Lélio Brun	(C_backend_makefile.lib_dependencies dependencies);
1849	c226a3ba	Lélio Brun	fprintf fmt "@."
1850	d4107cf2	ploc	end
1851
1852	13eb21df	ploc	(* Local Variables: *)
1853	cd670fe1	ploc	(* compile-command:"make -C ../../.." *)
1854	13eb21df	ploc	(* End: *)

Project

General

Profile

CristalCaveGem » LustreC