Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/backends/C/c_backend_spec.ml | ||
---|---|---|
1 |
|
|
2 | 1 |
(********************************************************************) |
3 | 2 |
(* *) |
4 | 3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
... | ... | |
23 | 22 |
|
24 | 23 |
(**************************************************************************) |
25 | 24 |
|
26 |
(* TODO ACSL |
|
27 |
Return updates machines (eg with local annotations) and acsl preamble *)
|
|
25 |
(* TODO ACSL Return updates machines (eg with local annotations) and acsl
|
|
26 |
preamble *) |
|
28 | 27 |
let preprocess_acsl machines = machines, [] |
29 |
|
|
28 |
|
|
30 | 29 |
let pp_acsl_basic_type_desc t_desc = |
31 | 30 |
if Types.is_bool_type t_desc then |
32 | 31 |
(* if !Options.cpp then "bool" else "_Bool" *) |
... | ... | |
36 | 35 |
if t_desc.tid = -1 then "int" else "integer" |
37 | 36 |
else if Types.is_real_type t_desc then |
38 | 37 |
if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type |
39 |
else |
|
40 |
assert false (* Not a basic C type. Do not handle arrays or pointers *)
|
|
38 |
else assert false
|
|
39 |
(* Not a basic C type. Do not handle arrays or pointers *) |
|
41 | 40 |
|
42 |
let pp_acsl pp fmt = |
|
43 |
fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp |
|
41 |
let pp_acsl pp fmt = fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp |
|
44 | 42 |
|
45 |
let pp_acsl_cut pp fmt = |
|
46 |
fprintf fmt "%a@," (pp_acsl pp) |
|
43 |
let pp_acsl_cut pp fmt = fprintf fmt "%a@," (pp_acsl pp) |
|
47 | 44 |
|
48 |
let pp_acsl_line pp fmt = |
|
49 |
fprintf fmt "//%@ @[<h>%a@]" pp |
|
45 |
let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp |
|
50 | 46 |
|
51 |
let pp_acsl_line' pp fmt = |
|
52 |
fprintf fmt "/*%@ @[<h>%a@] */" pp |
|
47 |
let pp_acsl_line' pp fmt = fprintf fmt "/*%@ @[<h>%a@] */" pp |
|
53 | 48 |
|
54 |
let pp_acsl_line_cut pp fmt = |
|
55 |
fprintf fmt "%a@," (pp_acsl_line pp) |
|
49 |
let pp_acsl_line_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line pp) |
|
56 | 50 |
|
57 |
let pp_requires pp_req fmt = |
|
58 |
fprintf fmt "requires %a;" pp_req |
|
51 |
let pp_requires pp_req fmt = fprintf fmt "requires %a;" pp_req |
|
59 | 52 |
|
60 |
let pp_ensures pp_ens fmt = |
|
61 |
fprintf fmt "ensures %a;" pp_ens |
|
53 |
let pp_ensures pp_ens fmt = fprintf fmt "ensures %a;" pp_ens |
|
62 | 54 |
|
63 |
let pp_assumes pp_asm fmt = |
|
64 |
fprintf fmt "assumes %a;" pp_asm |
|
55 |
let pp_assumes pp_asm fmt = fprintf fmt "assumes %a;" pp_asm |
|
65 | 56 |
|
66 | 57 |
let pp_assigns pp = |
67 | 58 |
pp_comma_list |
68 | 59 |
~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ") |
69 |
~pp_epilogue:pp_print_semicolon' |
|
70 |
pp |
|
60 |
~pp_epilogue:pp_print_semicolon' pp |
|
71 | 61 |
|
72 |
let pp_ghost pp_gho fmt = |
|
73 |
fprintf fmt "ghost %a" pp_gho |
|
62 |
let pp_ghost pp_gho fmt = fprintf fmt "ghost %a" pp_gho |
|
74 | 63 |
|
75 |
let pp_assert pp_ast fmt = |
|
76 |
fprintf fmt "assert %a;" pp_ast |
|
64 |
let pp_assert pp_ast fmt = fprintf fmt "assert %a;" pp_ast |
|
77 | 65 |
|
78 | 66 |
let pp_mem_valid pp_var fmt (name, var) = |
79 | 67 |
fprintf fmt "%s_valid(%a)" name pp_var var |
... | ... | |
90 | 78 |
|
91 | 79 |
let pp_access' = pp_access pp_print_string pp_print_string |
92 | 80 |
|
93 |
let pp_var_decl fmt v = |
|
94 |
pp_print_string fmt v.var_id |
|
81 |
let pp_var_decl fmt v = pp_print_string fmt v.var_id |
|
95 | 82 |
|
96 | 83 |
let pp_reg self fmt field = |
97 | 84 |
pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field) |
98 | 85 |
|
99 |
let pp_true fmt () = |
|
100 |
pp_print_string fmt "\\true" |
|
86 |
let pp_true fmt () = pp_print_string fmt "\\true" |
|
101 | 87 |
|
102 |
let pp_false fmt () = |
|
103 |
pp_print_string fmt "\\false" |
|
88 |
let pp_false fmt () = pp_print_string fmt "\\false" |
|
104 | 89 |
|
105 |
let pp_at pp_v fmt (v, l) = |
|
106 |
fprintf fmt "\\at(%a, %s)" pp_v v l |
|
90 |
let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l |
|
107 | 91 |
|
108 | 92 |
let instances machines m = |
109 | 93 |
let open List in |
110 | 94 |
let grow paths i td mems = |
111 | 95 |
match paths with |
112 |
| [] -> [[i, (td, mems)]] |
|
113 |
| _ -> map (cons (i, (td, mems))) paths |
|
96 |
| [] -> |
|
97 |
[ [ i, (td, mems) ] ] |
|
98 |
| _ -> |
|
99 |
map (cons (i, (td, mems))) paths |
|
114 | 100 |
in |
115 | 101 |
let rec aux paths m = |
116 |
map (fun (i, (td, _)) -> |
|
102 |
map |
|
103 |
(fun (i, (td, _)) -> |
|
117 | 104 |
try |
118 | 105 |
let m = find (fun m -> m.mname.node_id = node_name td) machines in |
119 | 106 |
aux (grow paths i td m.mmemory) m |
120 | 107 |
with Not_found -> grow paths i td []) |
121 |
m.minstances |> flatten |
|
108 |
m.minstances |
|
109 |
|> flatten |
|
122 | 110 |
in |
123 | 111 |
aux [] m |> map rev |
124 | 112 |
|
125 | 113 |
let memories insts = |
126 |
List.(map (fun path -> |
|
127 |
let _, (_, mems) = hd (rev path) in |
|
128 |
map (fun mem -> path, mem) mems) insts |> flatten) |
|
129 |
|
|
130 |
let pp_instance ?(indirect=true) ptr = |
|
114 |
List.( |
|
115 |
map |
|
116 |
(fun path -> |
|
117 |
let _, (_, mems) = hd (rev path) in |
|
118 |
map (fun mem -> path, mem) mems) |
|
119 |
insts |
|
120 |
|> flatten) |
|
121 |
|
|
122 |
let pp_instance ?(indirect = true) ptr = |
|
131 | 123 |
pp_print_list |
132 | 124 |
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr) |
133 | 125 |
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else ".")) |
134 | 126 |
(fun fmt (i, _) -> pp_print_string fmt i) |
135 | 127 |
|
136 |
let pp_memory ?(indirect=true) ptr fmt (path, mem) =
|
|
128 |
let pp_memory ?(indirect = true) ptr fmt (path, mem) =
|
|
137 | 129 |
pp_access |
138 | 130 |
((if indirect then pp_indirect else pp_access) |
139 |
(pp_instance ~indirect ptr) pp_print_string) |
|
140 |
pp_var_decl |
|
141 |
fmt ((path, "_reg"), mem) |
|
131 |
(pp_instance ~indirect ptr) |
|
132 |
pp_print_string) |
|
133 |
pp_var_decl fmt |
|
134 |
((path, "_reg"), mem) |
|
142 | 135 |
|
143 | 136 |
let prefixes l = |
144 | 137 |
let rec pref acc = function |
145 |
| x :: l -> pref ([x] :: List.map (List.cons x) acc) l |
|
146 |
| [] -> acc |
|
138 |
| x :: l -> |
|
139 |
pref ([ x ] :: List.map (List.cons x) acc) l |
|
140 |
| [] -> |
|
141 |
acc |
|
147 | 142 |
in |
148 | 143 |
pref [] (List.rev l) |
149 | 144 |
|
150 |
let powerset_instances paths = |
|
151 |
List.map prefixes paths |> List.flatten |
|
145 |
let powerset_instances paths = List.map prefixes paths |> List.flatten |
|
152 | 146 |
|
153 | 147 |
let pp_separated self mem fmt (paths, ptrs) = |
154 |
fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])" |
|
155 |
self |
|
156 |
mem |
|
157 |
(pp_comma_list |
|
158 |
~pp_prologue:pp_print_comma' |
|
159 |
(pp_instance self)) |
|
148 |
fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])" self mem |
|
149 |
(pp_comma_list ~pp_prologue:pp_print_comma' (pp_instance self)) |
|
160 | 150 |
paths |
161 |
(pp_comma_list |
|
162 |
~pp_prologue:pp_print_comma' |
|
163 |
pp_var_decl) |
|
151 |
(pp_comma_list ~pp_prologue:pp_print_comma' pp_var_decl) |
|
164 | 152 |
ptrs |
165 | 153 |
|
166 | 154 |
let pp_separated' = |
167 | 155 |
pp_comma_list |
168 | 156 |
~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(") |
169 |
~pp_epilogue:pp_print_cpar |
|
170 |
pp_var_decl |
|
157 |
~pp_epilogue:pp_print_cpar pp_var_decl |
|
171 | 158 |
|
172 |
let pp_par pp fmt = |
|
173 |
fprintf fmt "(%a)" pp |
|
159 |
let pp_par pp fmt = fprintf fmt "(%a)" pp |
|
174 | 160 |
|
175 | 161 |
let pp_forall pp_l pp_r fmt (l, r) = |
176 |
fprintf fmt "@[<v 2>\\forall %a;@,%a@]" |
|
177 |
pp_l l |
|
178 |
pp_r r |
|
162 |
fprintf fmt "@[<v 2>\\forall %a;@,%a@]" pp_l l pp_r r |
|
179 | 163 |
|
180 | 164 |
let pp_exists pp_l pp_r fmt (l, r) = |
181 |
fprintf fmt "@[<v 2>\\exists %a;@,%a@]" |
|
182 |
pp_l l |
|
183 |
pp_r r |
|
165 |
fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r |
|
184 | 166 |
|
185 |
let pp_equal pp_l pp_r fmt (l, r) = |
|
186 |
fprintf fmt "%a == %a" |
|
187 |
pp_l l |
|
188 |
pp_r r |
|
167 |
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r |
|
189 | 168 |
|
190 |
let pp_different pp_l pp_r fmt (l, r) = |
|
191 |
fprintf fmt "%a != %a" |
|
192 |
pp_l l |
|
193 |
pp_r r |
|
169 |
let pp_different pp_l pp_r fmt (l, r) = fprintf fmt "%a != %a" pp_l l pp_r r |
|
194 | 170 |
|
195 | 171 |
let pp_implies pp_l pp_r fmt (l, r) = |
196 |
fprintf fmt "@[<v>%a ==>@ %a@]" |
|
197 |
pp_l l |
|
198 |
pp_r r |
|
172 |
fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r |
|
199 | 173 |
|
200 |
let pp_and pp_l pp_r fmt (l, r) = |
|
201 |
fprintf fmt "@[<v>%a @ && %a@]" |
|
202 |
pp_l l |
|
203 |
pp_r r |
|
174 |
let pp_and pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ && %a@]" pp_l l pp_r r |
|
204 | 175 |
|
205 | 176 |
let pp_and_l pp_v fmt = |
206 |
pp_print_list |
|
207 |
~pp_open_box:pp_open_vbox0 |
|
177 |
pp_print_list ~pp_open_box:pp_open_vbox0 |
|
208 | 178 |
~pp_sep:(fun fmt () -> fprintf fmt "@,&& ") |
209 |
pp_v |
|
210 |
fmt |
|
179 |
pp_v fmt |
|
211 | 180 |
|
212 |
let pp_or pp_l pp_r fmt (l, r) = |
|
213 |
fprintf fmt "@[<v>%a @ || %a@]" |
|
214 |
pp_l l |
|
215 |
pp_r r |
|
181 |
let pp_or pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ || %a@]" pp_l l pp_r r |
|
216 | 182 |
|
217 | 183 |
let pp_or_l pp_v fmt = |
218 |
pp_print_list |
|
219 |
~pp_open_box:pp_open_vbox0 |
|
184 |
pp_print_list ~pp_open_box:pp_open_vbox0 |
|
220 | 185 |
~pp_sep:(fun fmt () -> fprintf fmt "@,|| ") |
221 |
pp_v |
|
222 |
fmt |
|
186 |
pp_v fmt |
|
223 | 187 |
|
224 |
let pp_not pp fmt = |
|
225 |
fprintf fmt "!%a" pp |
|
188 |
let pp_not pp fmt = fprintf fmt "!%a" pp |
|
226 | 189 |
|
227 | 190 |
let pp_valid pp = |
228 | 191 |
pp_and_l |
229 |
(* pp_print_list *) |
|
192 |
(* pp_print_list *)
|
|
230 | 193 |
(* ~pp_sep:pp_print_cut *) |
231 | 194 |
(fun fmt x -> fprintf fmt "\\valid(%a)" pp x) |
232 | 195 |
|
233 |
let pp_old pp fmt = |
|
234 |
fprintf fmt "\\old(%a)" pp |
|
196 |
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp |
|
235 | 197 |
|
236 | 198 |
let pp_ite pp_c pp_t pp_f fmt (c, t, f) = |
237 |
fprintf fmt "(%a @[<hov>? %a@ : %a)@]" |
|
238 |
pp_c c |
|
239 |
pp_t t |
|
240 |
pp_f f |
|
199 |
fprintf fmt "(%a @[<hov>? %a@ : %a)@]" pp_c c pp_t t pp_f f |
|
241 | 200 |
|
242 |
let pp_paren pp fmt v = |
|
243 |
fprintf fmt "(%a)" pp v |
|
201 |
let pp_paren pp fmt v = fprintf fmt "(%a)" pp v |
|
244 | 202 |
|
245 | 203 |
let pp_initialization pp_mem fmt (name, mem) = |
246 | 204 |
fprintf fmt "%s_initialization(%a)" name pp_mem mem |
... | ... | |
251 | 209 |
pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m |
252 | 210 |
|
253 | 211 |
let pp_locals m = |
254 |
pp_comma_list |
|
255 |
~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) |
|
256 |
(pp_local m) |
|
212 |
pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m) |
|
257 | 213 |
|
258 |
let pp_ptr_decl fmt v = |
|
259 |
pp_ptr fmt v.var_id |
|
214 |
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id |
|
260 | 215 |
|
261 | 216 |
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value = |
262 |
if Types.is_real_type typ && !Options.mpfr |
|
263 |
then |
|
264 |
assert false |
|
217 |
if Types.is_real_type typ && !Options.mpfr then assert false |
|
265 | 218 |
(* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *) |
266 |
else |
|
267 |
pp_equal pp_l pp_r fmt (var_name, value) |
|
219 |
else pp_equal pp_l pp_r fmt (var_name, value) |
|
268 | 220 |
|
269 | 221 |
let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt |
270 | 222 |
(var_type, var_name, value) = |
... | ... | |
275 | 227 |
match vars with |
276 | 228 |
| [] -> |
277 | 229 |
pp_basic_assign_spec |
278 |
(pp_value_suffix ~indirect:indirect_l m self_l var_type loop_vars pp_var_l) |
|
279 |
(pp_value_suffix ~indirect:indirect_r m self_r var_type loop_vars pp_var_r) |
|
230 |
(pp_value_suffix ~indirect:indirect_l m self_l var_type loop_vars |
|
231 |
pp_var_l) |
|
232 |
(pp_value_suffix ~indirect:indirect_r m self_r var_type loop_vars |
|
233 |
pp_var_r) |
|
280 | 234 |
fmt typ var_name value |
281 | 235 |
| (_d, LVar _i) :: _q -> |
282 | 236 |
assert false |
283 |
(* let typ' = Types.array_element_type typ in
|
|
284 |
* fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
|
|
285 |
* i i i pp_c_dimension d i
|
|
286 |
* (aux typ') q *)
|
|
237 |
(* let typ' = Types.array_element_type typ in |
|
238 |
* fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}" |
|
239 |
* i i i pp_c_dimension d i |
|
240 |
* (aux typ') q *) |
|
287 | 241 |
| (_d, LInt _r) :: _q -> |
288 | 242 |
assert false |
289 |
(* let typ' = Types.array_element_type typ in |
|
290 |
* let szl = Utils.enumerate (Dimension.size_const_dimension d) in |
|
291 |
* fprintf fmt "@[<v 2>{@,%a@]@,}" |
|
292 |
* (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *) |
|
293 |
| _ -> assert false |
|
243 |
(* let typ' = Types.array_element_type typ in |
|
244 |
* let szl = Utils.enumerate (Dimension.size_const_dimension d) in |
|
245 |
* fprintf fmt "@[<v 2>{@,%a@]@,}" |
|
246 |
* (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *) |
|
247 |
| _ -> |
|
248 |
assert false |
|
294 | 249 |
in |
295 |
begin |
|
296 |
reset_loop_counter (); |
|
297 |
aux var_type fmt reordered_loop_vars; |
|
298 |
end |
|
250 |
reset_loop_counter (); |
|
251 |
aux var_type fmt reordered_loop_vars |
|
299 | 252 |
|
300 |
let pp_nothing fmt () = |
|
301 |
pp_print_string fmt "\\nothing" |
|
253 |
let pp_nothing fmt () = pp_print_string fmt "\\nothing" |
|
302 | 254 |
|
303 | 255 |
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) = |
304 |
fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])" |
|
305 |
name |
|
306 |
(pp_print_option pp_print_int) i |
|
307 |
pp_mem mem |
|
308 |
pp_self self |
|
256 |
fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])" name |
|
257 |
(pp_print_option pp_print_int) |
|
258 |
i pp_mem mem pp_self self |
|
309 | 259 |
|
310 | 260 |
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) = |
311 | 261 |
pp_memory_pack_aux ?i:mp.mpindex pp_mem pp_self fmt |
... | ... | |
313 | 263 |
|
314 | 264 |
let pp_memory_pack_aux' ?i fmt = |
315 | 265 |
pp_memory_pack_aux ?i pp_print_string pp_print_string fmt |
316 |
let pp_memory_pack' fmt = |
|
317 |
pp_memory_pack pp_print_string pp_print_string fmt
|
|
266 |
|
|
267 |
let pp_memory_pack' fmt = pp_memory_pack pp_print_string pp_print_string fmt
|
|
318 | 268 |
|
319 | 269 |
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_input pp_output fmt |
320 | 270 |
(name, inputs, locals, outputs, mem_in, mem_out) = |
321 | 271 |
let stateless = fst (get_stateless_status m) in |
322 |
fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])" |
|
323 |
name
|
|
324 |
(pp_print_option pp_print_int) i
|
|
272 |
fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])" name
|
|
273 |
(pp_print_option pp_print_int)
|
|
274 |
i |
|
325 | 275 |
(fun fmt -> if not stateless then pp_mem_in fmt mem_in) |
326 | 276 |
(pp_comma_list |
327 | 277 |
~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ()) |
328 |
pp_input) inputs |
|
278 |
pp_input) |
|
279 |
inputs |
|
329 | 280 |
(pp_print_option (fun fmt _ -> |
330 | 281 |
pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals)) |
331 | 282 |
i |
332 | 283 |
(fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out) |
333 |
(pp_comma_list ~pp_prologue:pp_print_comma pp_output) outputs |
|
284 |
(pp_comma_list ~pp_prologue:pp_print_comma pp_output) |
|
285 |
outputs |
|
334 | 286 |
|
335 | 287 |
let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt |
336 | 288 |
(t, mem_in, mem_out) = |
... | ... | |
339 | 291 |
|
340 | 292 |
let pp_transition_aux' ?i m = |
341 | 293 |
pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl |
294 |
|
|
342 | 295 |
let pp_transition_aux'' ?i m = |
343 | 296 |
pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl |
297 |
|
|
344 | 298 |
let pp_transition' m = |
345 | 299 |
pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl |
300 |
|
|
346 | 301 |
let pp_transition'' m = |
347 | 302 |
pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl |
348 | 303 |
|
349 | 304 |
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) = |
350 |
fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" |
|
351 |
name |
|
352 |
pp_mem_in mem_in |
|
305 |
fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" name pp_mem_in mem_in |
|
353 | 306 |
pp_mem_out mem_out |
354 | 307 |
|
355 | 308 |
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string |
... | ... | |
357 | 310 |
let pp_functional_update mems fmt mem = |
358 | 311 |
let rec aux fmt mems = |
359 | 312 |
match mems with |
360 |
| [] -> pp_print_string fmt mem |
|
313 |
| [] -> |
|
314 |
pp_print_string fmt mem |
|
361 | 315 |
| x :: mems -> |
362 | 316 |
fprintf fmt "{ @[<hov>%a@ \\with ._reg.%s = %s@] }" aux mems x x |
363 | 317 |
in |
364 | 318 |
aux fmt |
365 |
(* if Utils.ISet.is_empty mems then |
|
366 |
* pp_print_string fmt mem |
|
367 |
* else |
|
368 |
* fprintf fmt "{ %s @[<hov>\\with %a@] }" |
|
369 |
* mem |
|
370 |
* (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ") |
|
371 |
* (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *) |
|
372 |
(Utils.ISet.elements mems)
|
|
319 |
(* if Utils.ISet.is_empty mems then
|
|
320 |
* pp_print_string fmt mem
|
|
321 |
* else
|
|
322 |
* fprintf fmt "{ %s @[<hov>\\with %a@] }"
|
|
323 |
* mem
|
|
324 |
* (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ")
|
|
325 |
* (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *)
|
|
326 |
(Utils.ISet.elements mems) |
|
373 | 327 |
|
374 | 328 |
module PrintSpec = struct |
375 |
|
|
376 | 329 |
type mode = |
377 | 330 |
| MemoryPackMode |
378 | 331 |
| TransitionMode |
... | ... | |
387 | 340 |
| StateVar x -> |
388 | 341 |
fprintf fmt "%s.%a" mem pp_var_decl x |
389 | 342 |
|
390 |
let pp_expr: |
|
391 |
type a. ?output:bool -> machine_t -> ident -> formatter |
|
392 |
-> (value_t, a) expression_t -> unit = |
|
393 |
fun ?(output=false) m mem fmt -> function |
|
394 |
| Val v -> pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v |
|
395 |
| Tag t -> pp_print_string fmt t |
|
396 |
| Var v -> pp_var_decl fmt v |
|
397 |
| Memory r -> pp_reg mem fmt r |
|
343 |
let pp_expr : |
|
344 |
type a. |
|
345 |
?output:bool -> |
|
346 |
machine_t -> |
|
347 |
ident -> |
|
348 |
formatter -> |
|
349 |
(value_t, a) expression_t -> |
|
350 |
unit = |
|
351 |
fun ?(output = false) m mem fmt -> function |
|
352 |
| Val v -> |
|
353 |
pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v |
|
354 |
| Tag t -> |
|
355 |
pp_print_string fmt t |
|
356 |
| Var v -> |
|
357 |
pp_var_decl fmt v |
|
358 |
| Memory r -> |
|
359 |
pp_reg mem fmt r |
|
398 | 360 |
|
399 | 361 |
let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p = |
400 |
let output, mem_update = match mode with |
|
401 |
| InstrMode _ -> true, false |
|
402 |
| TransitionFootprintMode -> false, true |
|
403 |
| _ -> false, false |
|
362 |
let output, mem_update = |
|
363 |
match mode with |
|
364 |
| InstrMode _ -> |
|
365 |
true, false |
|
366 |
| TransitionFootprintMode -> |
|
367 |
false, true |
|
368 |
| _ -> |
|
369 |
false, false |
|
404 | 370 |
in |
405 |
let pp_expr: |
|
406 |
type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit = |
|
407 |
fun ?output fmt e -> pp_expr ?output m mem_out fmt e
|
|
371 |
let pp_expr :
|
|
372 |
type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit =
|
|
373 |
fun ?output fmt e -> pp_expr ?output m mem_out fmt e |
|
408 | 374 |
in |
409 | 375 |
match p with |
410 | 376 |
| Transition (f, inst, i, inputs, locals, outputs, r, mems) -> |
411 |
let pp_mem_in, pp_mem_out = match inst with |
|
377 |
let pp_mem_in, pp_mem_out = |
|
378 |
match inst with |
|
412 | 379 |
| None -> |
413 |
pp_print_string, |
|
414 |
if mem_update then pp_functional_update mems else pp_print_string
|
|
380 |
( pp_print_string,
|
|
381 |
if mem_update then pp_functional_update mems else pp_print_string )
|
|
415 | 382 |
| Some inst -> |
416 |
(fun fmt mem_in -> |
|
417 |
if r then pp_print_string fmt mem_in |
|
418 |
else pp_access' fmt (mem_in, inst)), |
|
419 |
(fun fmt mem_out -> pp_access' fmt (mem_out, inst))
|
|
383 |
( (fun fmt mem_in ->
|
|
384 |
if r then pp_print_string fmt mem_in
|
|
385 |
else pp_access' fmt (mem_in, inst)),
|
|
386 |
fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
|
|
420 | 387 |
in |
421 |
pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output) |
|
422 |
fmt |
|
388 |
pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output) fmt |
|
423 | 389 |
(f, inputs, locals, outputs, mem_in', mem_out') |
424 | 390 |
| Reset (_f, inst, r) -> |
425 | 391 |
pp_ite |
... | ... | |
429 | 395 |
fmt |
430 | 396 |
(r, (mem_out, 1), (mem_out, (mem_in, inst))) |
431 | 397 |
| MemoryPack (f, inst, i) -> |
432 |
let pp_mem, pp_self = match inst with |
|
398 |
let pp_mem, pp_self = |
|
399 |
match inst with |
|
433 | 400 |
| None -> |
434 | 401 |
pp_print_string, pp_print_string |
435 | 402 |
| Some inst -> |
436 |
(fun fmt mem -> pp_access' fmt (mem, inst)), |
|
437 |
(fun fmt self -> pp_indirect' fmt (self, inst))
|
|
403 |
( (fun fmt mem -> pp_access' fmt (mem, inst)),
|
|
404 |
fun fmt self -> pp_indirect' fmt (self, inst) )
|
|
438 | 405 |
in |
439 | 406 |
pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in) |
440 | 407 |
| ResetCleared f -> |
441 | 408 |
pp_reset_cleared' fmt (f, mem_in, mem_out) |
442 |
(* fprintf fmt "ResetCleared_%a" pp_print_string f *) |
|
443 |
| Initialization -> () |
|
409 |
(* fprintf fmt "ResetCleared_%a" pp_print_string f *) |
|
410 |
| Initialization -> |
|
411 |
() |
|
444 | 412 |
|
445 | 413 |
let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool |
446 | 414 |
|
447 |
let val_of_expr: type a. (value_t, a) expression_t -> value_t = function |
|
448 |
| Val v -> v |
|
449 |
| Tag t -> id_to_tag t |
|
450 |
| Var v -> vdecl_to_val v |
|
451 |
| Memory (StateVar v) -> vdecl_to_val v |
|
452 |
| Memory ResetFlag -> vdecl_to_val reset_flag |
|
415 |
let val_of_expr : type a. (value_t, a) expression_t -> value_t = function |
|
416 |
| Val v -> |
|
417 |
v |
|
418 |
| Tag t -> |
|
419 |
id_to_tag t |
|
420 |
| Var v -> |
|
421 |
vdecl_to_val v |
|
422 |
| Memory (StateVar v) -> |
|
423 |
vdecl_to_val v |
|
424 |
| Memory ResetFlag -> |
|
425 |
vdecl_to_val reset_flag |
|
453 | 426 |
|
454 | 427 |
let find_arrow m = |
455 |
try |
|
456 |
List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
|
|
457 |
|> fst
|
|
458 |
with Not_found -> eprintf "Internal error: arrow not found"; raise Not_found
|
|
428 |
try List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |> fst
|
|
429 |
with Not_found ->
|
|
430 |
eprintf "Internal error: arrow not found";
|
|
431 |
raise Not_found
|
|
459 | 432 |
|
460 | 433 |
let pp_spec mode m fmt f = |
461 | 434 |
let rec pp_spec mode fmt f = |
... | ... | |
479 | 452 |
| InstrMode self -> |
480 | 453 |
let mem = "*" ^ mem in |
481 | 454 |
fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label); |
482 |
self, flush_str_formatter (), false, |
|
483 |
mem, mem, false |
|
455 |
self, flush_str_formatter (), false, mem, mem, false |
|
484 | 456 |
in |
485 |
let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit = |
|
486 |
fun fmt e -> pp_expr m mem_out fmt e
|
|
457 |
let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
|
|
458 |
fun fmt e -> pp_expr m mem_out fmt e |
|
487 | 459 |
in |
488 | 460 |
let pp_spec' = pp_spec mode in |
489 | 461 |
match f with |
... | ... | |
492 | 464 |
| False -> |
493 | 465 |
pp_false fmt () |
494 | 466 |
| Equal (a, b) -> |
495 |
pp_assign_spec m |
|
496 |
mem_out (pp_c_var_read ~test_output:false m) indirect_l |
|
497 |
mem_in (pp_c_var_read ~test_output:false m) indirect_r |
|
498 |
fmt |
|
467 |
pp_assign_spec m mem_out |
|
468 |
(pp_c_var_read ~test_output:false m) |
|
469 |
indirect_l mem_in |
|
470 |
(pp_c_var_read ~test_output:false m) |
|
471 |
indirect_r fmt |
|
499 | 472 |
(type_of_l_value a, val_of_expr a, val_of_expr b) |
500 | 473 |
| And fs -> |
501 | 474 |
pp_and_l pp_spec' fmt fs |
... | ... | |
513 | 486 |
pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p |
514 | 487 |
| StateVarPack ResetFlag -> |
515 | 488 |
let r = vdecl_to_val reset_flag in |
516 |
pp_assign_spec m |
|
517 |
mem_out (pp_c_var_read ~test_output:false m) indirect_l |
|
518 |
mem_in (pp_c_var_read ~test_output:false m) indirect_r |
|
519 |
fmt |
|
489 |
pp_assign_spec m mem_out |
|
490 |
(pp_c_var_read ~test_output:false m) |
|
491 |
indirect_l mem_in |
|
492 |
(pp_c_var_read ~test_output:false m) |
|
493 |
indirect_r fmt |
|
520 | 494 |
(Type_predef.type_bool, r, r) |
521 | 495 |
| StateVarPack (StateVar v) -> |
522 | 496 |
let v' = vdecl_to_val v in |
523 | 497 |
let inst = find_arrow m in |
524 |
pp_par (pp_implies |
|
525 |
(pp_not (pp_initialization pp_access')) |
|
526 |
(pp_assign_spec m |
|
527 |
mem_out (pp_c_var_read ~test_output:false m) indirect_l |
|
528 |
mem_in (pp_c_var_read ~test_output:false m) indirect_r)) |
|
498 |
pp_par |
|
499 |
(pp_implies |
|
500 |
(pp_not (pp_initialization pp_access')) |
|
501 |
(pp_assign_spec m mem_out |
|
502 |
(pp_c_var_read ~test_output:false m) |
|
503 |
indirect_l mem_in |
|
504 |
(pp_c_var_read ~test_output:false m) |
|
505 |
indirect_r)) |
|
529 | 506 |
fmt |
530 |
((Arrow.arrow_id, (mem_out, inst)), |
|
531 |
(v.var_type, v', v')) |
|
507 |
((Arrow.arrow_id, (mem_out, inst)), (v.var_type, v', v')) |
|
532 | 508 |
| ExistsMem (f, rc, tr) -> |
533 | 509 |
pp_exists |
534 | 510 |
(pp_machine_decl' ~ghost:true) |
535 | 511 |
(pp_and (pp_spec ResetOut) (pp_spec ResetIn)) |
536 | 512 |
fmt |
537 |
((f, mk_mem_reset m), |
|
538 |
(rc, tr)) |
|
513 |
((f, mk_mem_reset m), (rc, tr)) |
|
539 | 514 |
in |
540 | 515 |
match mode with |
541 | 516 |
| TransitionFootprintMode -> |
... | ... | |
543 | 518 |
let mem_out = mk_mem_out m in |
544 | 519 |
pp_forall |
545 | 520 |
(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string)) |
546 |
(pp_spec mode) |
|
547 |
fmt ((m.mname.node_id, [mem_in; mem_out]), f)
|
|
521 |
(pp_spec mode) fmt
|
|
522 |
((m.mname.node_id, [ mem_in; mem_out ]), f)
|
|
548 | 523 |
| _ -> |
549 | 524 |
pp_spec mode fmt f |
550 |
|
|
551 | 525 |
end |
552 | 526 |
|
553 | 527 |
let pp_predicate pp_l pp_r fmt (l, r) = |
554 |
fprintf fmt "@[<v 2>predicate %a =@,%a;@]" |
|
555 |
pp_l l |
|
556 |
pp_r r |
|
528 |
fprintf fmt "@[<v 2>predicate %a =@,%a;@]" pp_l l pp_r r |
|
557 | 529 |
|
558 | 530 |
let pp_lemma pp_l pp_r fmt (l, r) = |
559 |
fprintf fmt "@[<v 2>lemma %a:@,%a;@]" |
|
560 |
pp_l l |
|
561 |
pp_r r |
|
531 |
fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r |
|
562 | 532 |
|
563 | 533 |
let pp_mem_valid_def fmt m = |
564 | 534 |
if not (fst (get_stateless_status m)) then |
... | ... | |
570 | 540 |
(pp_and |
571 | 541 |
(pp_and_l (fun fmt (inst, (td, _)) -> |
572 | 542 |
if Arrow.td_is_arrow td then |
573 |
pp_valid pp_indirect' fmt [self, inst] |
|
574 |
else |
|
575 |
pp_mem_valid pp_indirect' fmt (node_name td, (self, inst)))) |
|
543 |
pp_valid pp_indirect' fmt [ self, inst ] |
|
544 |
else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst)))) |
|
576 | 545 |
(pp_valid pp_print_string))) |
577 | 546 |
fmt |
578 |
((name, (name, self)), |
|
579 |
(m.minstances, [self])) |
|
547 |
((name, (name, self)), (m.minstances, [ self ])) |
|
580 | 548 |
|
581 | 549 |
let pp_memory_pack_def m fmt mp = |
582 | 550 |
let name = mp.mpname.node_id in |
... | ... | |
587 | 555 |
(pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr)) |
588 | 556 |
(PrintSpec.pp_spec MemoryPackMode m)) |
589 | 557 |
fmt |
590 |
((mp, (name, mem), (name, self)), |
|
591 |
mp.mpformula) |
|
558 |
((mp, (name, mem), (name, self)), mp.mpformula) |
|
592 | 559 |
|
593 | 560 |
let print_machine_ghost_struct fmt m = |
594 | 561 |
pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m |
595 | 562 |
|
596 | 563 |
let pp_memory_pack_defs fmt m = |
597 | 564 |
if not (fst (get_stateless_status m)) then |
598 |
fprintf fmt "%a@,%a" |
|
599 |
print_machine_ghost_struct m |
|
600 |
(pp_print_list |
|
601 |
~pp_epilogue:pp_print_cut |
|
602 |
~pp_open_box:pp_open_vbox0 |
|
603 |
(pp_memory_pack_def m)) m.mspec.mmemory_packs |
|
565 |
fprintf fmt "%a@,%a" print_machine_ghost_struct m |
|
566 |
(pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0 |
|
567 |
(pp_memory_pack_def m)) |
|
568 |
m.mspec.mmemory_packs |
|
604 | 569 |
|
605 | 570 |
let pp_transition_def m fmt t = |
606 | 571 |
let name = t.tname.node_id in |
... | ... | |
609 | 574 |
pp_acsl |
610 | 575 |
(pp_predicate |
611 | 576 |
(pp_transition m |
612 |
(pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true)
|
|
613 |
(pp_local m)
|
|
614 |
(pp_local m)) |
|
577 |
(pp_machine_decl' ~ghost:true) |
|
578 |
(pp_machine_decl' ~ghost:true)
|
|
579 |
(pp_local m) (pp_local m))
|
|
615 | 580 |
(PrintSpec.pp_spec TransitionMode m)) |
616 | 581 |
fmt |
617 |
((t, (name, mem_in), (name, mem_out)), |
|
618 |
t.tformula) |
|
582 |
((t, (name, mem_in), (name, mem_out)), t.tformula) |
|
619 | 583 |
|
620 | 584 |
let pp_transition_defs fmt m = |
621 |
pp_print_list |
|
622 |
~pp_epilogue:pp_print_cut |
|
623 |
~pp_open_box:pp_open_vbox0 |
|
585 |
pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0 |
|
624 | 586 |
(pp_transition_def m) fmt m.mspec.mtransitions |
625 | 587 |
|
626 | 588 |
let pp_transition_footprint fmt t = |
627 |
fprintf fmt "%s_transition%a_footprint" |
|
628 |
t.tname.node_id
|
|
629 |
(pp_print_option pp_print_int) t.tindex
|
|
589 |
fprintf fmt "%s_transition%a_footprint" t.tname.node_id
|
|
590 |
(pp_print_option pp_print_int)
|
|
591 |
t.tindex |
|
630 | 592 |
|
631 | 593 |
let pp_transition_footprint_lemma m fmt t = |
632 | 594 |
let open Utils.ISet in |
633 | 595 |
let name = t.tname.node_id in |
634 |
let mems = diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint in |
|
635 |
let memories = List.map (fun v -> |
|
636 |
{ v with var_type = { v.var_type with tid = -1 }}) |
|
596 |
let mems = |
|
597 |
diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint |
|
598 |
in |
|
599 |
let memories = |
|
600 |
List.map |
|
601 |
(fun v -> { v with var_type = { v.var_type with tid = -1 } }) |
|
637 | 602 |
(List.filter (fun v -> not (mem v.var_id t.tfootprint)) m.mmemory) |
638 | 603 |
in |
639 | 604 |
if not (is_empty mems) then |
640 | 605 |
pp_acsl |
641 |
(pp_lemma |
|
642 |
pp_transition_footprint |
|
606 |
(pp_lemma pp_transition_footprint |
|
643 | 607 |
(PrintSpec.pp_spec TransitionFootprintMode m)) |
644 | 608 |
fmt |
645 |
(t, |
|
646 |
Forall (
|
|
647 |
memories @ t.tinputs @ t.tlocals @ t.toutputs, |
|
648 |
Imply (Spec_common.mk_transition ?i:t.tindex name
|
|
649 |
(vdecls_to_vals t.tinputs)
|
|
650 |
(vdecls_to_vals t.tlocals) |
|
609 |
( t,
|
|
610 |
Forall
|
|
611 |
( memories @ t.tinputs @ t.tlocals @ t.toutputs,
|
|
612 |
Imply
|
|
613 |
( Spec_common.mk_transition ?i:t.tindex name
|
|
614 |
(vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
|
|
651 | 615 |
(vdecls_to_vals t.toutputs), |
652 | 616 |
Spec_common.mk_transition ~mems ?i:t.tindex name |
653 |
(vdecls_to_vals t.tinputs) |
|
654 |
(vdecls_to_vals t.tlocals) |
|
655 |
(vdecls_to_vals t.toutputs)))) |
|
617 |
(vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals) |
|
618 |
(vdecls_to_vals t.toutputs) ) ) ) |
|
656 | 619 |
|
657 | 620 |
let pp_transition_footprint_lemmas fmt m = |
658 |
pp_print_list |
|
659 |
~pp_epilogue:pp_print_cut
|
|
660 |
~pp_open_box:pp_open_vbox0
|
|
661 |
(pp_transition_footprint_lemma m) fmt
|
|
662 |
(List.filter (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
|
|
663 |
m.mspec.mtransitions)
|
|
621 |
pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
|
|
622 |
(pp_transition_footprint_lemma m)
|
|
623 |
fmt
|
|
624 |
(List.filter
|
|
625 |
(fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
|
|
626 |
m.mspec.mtransitions) |
|
664 | 627 |
|
665 | 628 |
let pp_initialization_def fmt m = |
666 | 629 |
if not (fst (get_stateless_status m)) then |
... | ... | |
673 | 636 |
if Arrow.td_is_arrow td then |
674 | 637 |
pp_initialization pp_access' fmt (node_name td, (mem_in, i)) |
675 | 638 |
else |
676 |
pp_equal (pp_reset_flag ~indirect:false pp_access') pp_print_int |
|
677 |
fmt |
|
639 |
pp_equal |
|
640 |
(pp_reset_flag ~indirect:false pp_access') |
|
641 |
pp_print_int fmt |
|
678 | 642 |
((mem_in, i), 1)))) |
679 | 643 |
fmt |
680 | 644 |
((name, (name, mem_in)), m.minstances) |
... | ... | |
687 | 651 |
pp_acsl |
688 | 652 |
(pp_predicate |
689 | 653 |
(pp_reset_cleared |
690 |
(pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true)) |
|
654 |
(pp_machine_decl' ~ghost:true) |
|
655 |
(pp_machine_decl' ~ghost:true)) |
|
691 | 656 |
(pp_ite |
692 | 657 |
(pp_reset_flag' ~indirect:false) |
693 | 658 |
(pp_and |
... | ... | |
695 | 660 |
pp_initialization') |
696 | 661 |
(pp_equal pp_print_string pp_print_string))) |
697 | 662 |
fmt |
698 |
((name, (name, mem_in), (name, mem_out)), |
|
699 |
(mem_in, |
|
700 |
((mem_out, 0), (name, mem_out)), |
|
701 |
(mem_out, mem_in))) |
|
663 |
( (name, (name, mem_in), (name, mem_out)), |
|
664 |
(mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) ) |
|
702 | 665 |
|
703 |
let pp_at pp_p fmt (p, l) = |
|
704 |
fprintf fmt "\\at(%a, %s)" pp_p p l |
|
666 |
let pp_at pp_p fmt (p, l) = fprintf fmt "\\at(%a, %s)" pp_p p l |
|
705 | 667 |
|
706 | 668 |
let label_pre = "Pre" |
707 | 669 |
|
708 |
let pp_at_pre pp_p fmt p = |
|
709 |
pp_at pp_p fmt (p, label_pre) |
|
670 |
let pp_at_pre pp_p fmt p = pp_at pp_p fmt (p, label_pre) |
|
710 | 671 |
|
711 |
let pp_register_chain ?(indirect=true) ptr =
|
|
672 |
let pp_register_chain ?(indirect = true) ptr =
|
|
712 | 673 |
pp_print_list |
713 | 674 |
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr) |
714 |
~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reg._first"
|
|
715 |
(if indirect then "->" else "."))
|
|
675 |
~pp_epilogue:(fun fmt () -> |
|
676 |
fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
|
|
716 | 677 |
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else ".")) |
717 | 678 |
(fun fmt (i, _) -> pp_print_string fmt i) |
718 | 679 |
|
719 |
let pp_reset_flag_chain ?(indirect=true) ptr fmt mems =
|
|
680 |
let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
|
|
720 | 681 |
pp_print_list |
721 | 682 |
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr) |
722 | 683 |
~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "") |
... | ... | |
727 | 688 |
let pp_arrow_reset_ghost mem fmt inst = |
728 | 689 |
fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst) |
729 | 690 |
|
730 |
module GhostProto: MODIFIERS_GHOST_PROTO = struct |
|
731 |
let pp_ghost_parameters ?(cut=true) fmt vs =
|
|
691 |
module GhostProto : MODIFIERS_GHOST_PROTO = struct
|
|
692 |
let pp_ghost_parameters ?(cut = true) fmt vs =
|
|
732 | 693 |
fprintf fmt "%a%a" |
733 |
(if cut then pp_print_cut else pp_print_nothing) () |
|
694 |
(if cut then pp_print_cut else pp_print_nothing) |
|
695 |
() |
|
734 | 696 |
(pp_acsl_line' |
735 |
(pp_ghost |
|
736 |
(pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x)))) |
|
697 |
(pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x)))) |
|
737 | 698 |
vs |
738 | 699 |
end |
739 | 700 |
|
740 | 701 |
module HdrMod = struct |
741 |
|
|
742 | 702 |
module GhostProto = GhostProto |
743 | 703 |
|
744 |
let print_machine_decl_prefix = fun _ _ -> ()
|
|
704 |
let print_machine_decl_prefix _ _ = ()
|
|
745 | 705 |
|
746 | 706 |
let pp_import_arrow fmt () = |
747 | 707 |
fprintf fmt "#include \"%s/arrow_spec.h%s\"" |
748 | 708 |
(Arrow.arrow_top_decl ()).top_decl_owner |
749 | 709 |
(if !Options.cpp then "pp" else "") |
750 |
|
|
751 | 710 |
end |
752 | 711 |
|
753 | 712 |
module SrcMod = struct |
754 |
|
|
755 | 713 |
module GhostProto = GhostProto |
756 | 714 |
|
757 | 715 |
let pp_predicates (* dependencies *) fmt machines = |
758 | 716 |
let pp_preds comment pp = |
759 |
pp_print_list |
|
760 |
~pp_open_box:pp_open_vbox0 |
|
761 |
~pp_prologue:(pp_print_endcut comment) |
|
762 |
pp |
|
763 |
~pp_epilogue:pp_print_cutcut in |
|
764 |
fprintf fmt |
|
765 |
"%a%a%a%a%a%a" |
|
766 |
(pp_preds "/* ACSL `valid` predicates */" |
|
767 |
pp_mem_valid_def) machines |
|
768 |
(pp_preds "/* ACSL `memory pack` simulations */" |
|
769 |
pp_memory_pack_defs) machines |
|
770 |
(pp_preds "/* ACSL initialization annotations */" |
|
771 |
pp_initialization_def) machines |
|
772 |
(pp_preds "/* ACSL reset cleared annotations */" |
|
773 |
pp_reset_cleared_def) machines |
|
774 |
(pp_preds "/* ACSL transition annotations */" |
|
775 |
pp_transition_defs) machines |
|
717 |
pp_print_list ~pp_open_box:pp_open_vbox0 |
|
718 |
~pp_prologue:(pp_print_endcut comment) pp ~pp_epilogue:pp_print_cutcut |
|
719 |
in |
|
720 |
fprintf fmt "%a%a%a%a%a%a" |
|
721 |
(pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def) |
|
722 |
machines |
|
723 |
(pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs) |
|
724 |
machines |
|
725 |
(pp_preds "/* ACSL initialization annotations */" pp_initialization_def) |
|
726 |
machines |
|
727 |
(pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def) |
|
728 |
machines |
|
729 |
(pp_preds "/* ACSL transition annotations */" pp_transition_defs) |
|
730 |
machines |
|
776 | 731 |
(pp_preds "/* ACSL transition memory footprints lemmas */" |
777 |
pp_transition_footprint_lemmas) machines |
|
732 |
pp_transition_footprint_lemmas) |
|
733 |
machines |
|
778 | 734 |
|
779 | 735 |
let pp_clear_reset_spec fmt self mem m = |
780 | 736 |
let name = m.mname.node_id in |
781 |
let arws, narws = List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) |
|
782 |
m.minstances in |
|
783 |
let mk_insts = List.map (fun x -> [x]) in |
|
784 |
pp_acsl_cut (fun fmt () -> |
|
737 |
let arws, narws = |
|
738 |
List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |
|
739 |
in |
|
740 |
let mk_insts = List.map (fun x -> [ x ]) in |
|
741 |
pp_acsl_cut |
|
742 |
(fun fmt () -> |
|
785 | 743 |
fprintf fmt |
786 |
"%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,\ |
|
787 |
@[<v 2>behavior reset:@;\ |
|
788 |
%a@,%a@]@,\ |
|
789 |
@[<v 2>behavior no_reset:@;\ |
|
790 |
%a@,%a@]@,\ |
|
791 |
complete behaviors;@,\ |
|
792 |
disjoint behaviors;" |
|
793 |
(pp_requires pp_mem_valid') (name, self) |
|
794 |
(pp_requires (pp_separated self mem)) (mk_insts m.minstances, []) |
|
744 |
"%a@,\ |
|
745 |
%a@,\ |
|
746 |
%a@,\ |
|
747 |
%a@,\ |
|
748 |
%a@,\ |
|
749 |
%a@,\ |
|
750 |
%a@,\ |
|
751 |
%a@,\ |
|
752 |
%a@,\ |
|
753 |
%a@,\ |
|
754 |
@[<v 2>behavior reset:@;\ |
|
755 |
%a@,\ |
|
756 |
%a@]@,\ |
|
757 |
@[<v 2>behavior no_reset:@;\ |
|
758 |
%a@,\ |
|
759 |
%a@]@,\ |
|
760 |
complete behaviors;@,\ |
|
761 |
disjoint behaviors;" |
|
762 |
(pp_requires pp_mem_valid') |
|
763 |
(name, self) |
|
764 |
(pp_requires (pp_separated self mem)) |
|
765 |
(mk_insts m.minstances, []) |
|
795 | 766 |
(pp_requires (pp_memory_pack_aux pp_ptr pp_print_string)) |
796 | 767 |
(name, mem, self) |
797 |
(pp_ensures (pp_memory_pack_aux |
|
798 |
~i:(List.length m.mspec.mmemory_packs - 2) |
|
799 |
pp_ptr pp_print_string)) |
|
768 |
(pp_ensures |
|
769 |
(pp_memory_pack_aux |
|
770 |
~i:(List.length m.mspec.mmemory_packs - 2) |
|
771 |
pp_ptr pp_print_string)) |
|
800 | 772 |
(name, mem, self) |
801 |
(pp_assigns pp_reset_flag') [self] |
|
802 |
(pp_assigns (pp_register_chain self)) (mk_insts arws) |
|
803 |
(pp_assigns (pp_reset_flag_chain self)) (mk_insts narws) |
|
804 |
(pp_assigns pp_reset_flag') [mem] |
|
805 |
(pp_assigns (pp_register_chain ~indirect:false mem)) (mk_insts arws) |
|
806 |
(pp_assigns (pp_reset_flag_chain ~indirect:false mem)) (mk_insts narws) |
|
807 |
(pp_assumes (pp_equal pp_reset_flag' pp_print_int)) (mem, 1) |
|
808 |
(pp_ensures (pp_initialization pp_ptr)) (name, mem) |
|
809 |
(pp_assumes (pp_equal pp_reset_flag' pp_print_int)) (mem, 0) |
|
810 |
(pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) (mem, mem) |
|
811 |
) |
|
773 |
(pp_assigns pp_reset_flag') |
|
774 |
[ self ] |
|
775 |
(pp_assigns (pp_register_chain self)) |
|
776 |
(mk_insts arws) |
|
777 |
(pp_assigns (pp_reset_flag_chain self)) |
|
778 |
(mk_insts narws) |
|
779 |
(pp_assigns pp_reset_flag') |
|
780 |
[ mem ] |
|
781 |
(pp_assigns (pp_register_chain ~indirect:false mem)) |
|
782 |
(mk_insts arws) |
|
783 |
(pp_assigns (pp_reset_flag_chain ~indirect:false mem)) |
|
784 |
(mk_insts narws) |
|
785 |
(pp_assumes (pp_equal pp_reset_flag' pp_print_int)) |
|
786 |
(mem, 1) |
|
787 |
(pp_ensures (pp_initialization pp_ptr)) |
|
788 |
(name, mem) |
|
789 |
(pp_assumes (pp_equal pp_reset_flag' pp_print_int)) |
|
790 |
(mem, 0) |
|
791 |
(pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) |
|
792 |
(mem, mem)) |
|
812 | 793 |
fmt () |
813 | 794 |
|
814 | 795 |
let pp_set_reset_spec fmt self mem m = |
815 | 796 |
let name = m.mname.node_id in |
816 |
pp_acsl_cut (fun fmt () -> |
|
817 |
fprintf fmt |
|
818 |
"%a@,%a@,%a" |
|
819 |
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) (name, mem, self) |
|
820 |
(pp_ensures (pp_equal pp_reset_flag' pp_print_int)) (mem, 1) |
|
821 |
(pp_assigns pp_reset_flag') [self; mem]) |
|
797 |
pp_acsl_cut |
|
798 |
(fun fmt () -> |
|
799 |
fprintf fmt "%a@,%a@,%a" |
|
800 |
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) |
|
801 |
(name, mem, self) |
|
802 |
(pp_ensures (pp_equal pp_reset_flag' pp_print_int)) |
|
803 |
(mem, 1) |
|
804 |
(pp_assigns pp_reset_flag') |
|
805 |
[ self; mem ]) |
|
822 | 806 |
fmt () |
823 | 807 |
|
824 | 808 |
let pp_step_spec fmt machines self mem m = |
825 | 809 |
let name = m.mname.node_id in |
826 | 810 |
let insts = instances machines m in |
827 | 811 |
let insts' = powerset_instances insts in |
828 |
let insts'' = List.(filter (fun l -> l <> []) |
|
829 |
(map (filter (fun (_, (td, _)) -> |
|
830 |
not (Arrow.td_is_arrow td))) insts)) in |
|
812 |
let insts'' = |
|
813 |
List.( |
|
814 |
filter |
|
815 |
(fun l -> l <> []) |
|
816 |
(map (filter (fun (_, (td, _)) -> not (Arrow.td_is_arrow td))) insts)) |
|
817 |
in |
|
831 | 818 |
let inputs = m.mstep.step_inputs in |
832 | 819 |
let outputs = m.mstep.step_outputs in |
833 |
pp_acsl_cut (fun fmt () -> |
|
820 |
pp_acsl_cut |
|
821 |
(fun fmt () -> |
|
834 | 822 |
if fst (get_stateless_status m) then |
835 |
fprintf fmt |
|
836 |
"%a@,%a@,%a@,%a"
|
|
837 |
(pp_requires (pp_valid pp_var_decl)) outputs
|
|
838 |
(pp_requires pp_separated') outputs
|
|
839 |
(pp_assigns pp_ptr_decl) outputs |
|
823 |
fprintf fmt "%a@,%a@,%a@,%a"
|
|
824 |
(pp_requires (pp_valid pp_var_decl))
|
|
825 |
outputs |
|
826 |
(pp_requires pp_separated') |
|
827 |
outputs (pp_assigns pp_ptr_decl) outputs
|
|
840 | 828 |
(pp_ensures (pp_transition_aux'' m)) |
841 | 829 |
(name, inputs, [], outputs, "", "") |
842 | 830 |
else |
843 | 831 |
fprintf fmt |
844 | 832 |
"%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a" |
845 |
(pp_requires (pp_valid pp_var_decl)) outputs |
|
846 |
(pp_requires pp_mem_valid') (name, self) |
|
847 |
(pp_requires (pp_separated self mem)) (insts', outputs) |
|
833 |
(pp_requires (pp_valid pp_var_decl)) |
|
834 |
outputs |
|
835 |
(pp_requires pp_mem_valid') |
|
836 |
(name, self) |
|
837 |
(pp_requires (pp_separated self mem)) |
|
838 |
(insts', outputs) |
|
848 | 839 |
(pp_requires (pp_memory_pack_aux pp_ptr pp_print_string)) |
849 | 840 |
(name, mem, self) |
850 | 841 |
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) |
851 | 842 |
(name, mem, self) |
852 |
(pp_ensures (pp_transition_aux m (pp_old pp_ptr) |
|
853 |
pp_ptr pp_var_decl pp_ptr_decl)) |
|
843 |
(pp_ensures |
|
844 |
(pp_transition_aux m (pp_old pp_ptr) pp_ptr pp_var_decl |
|
845 |
pp_ptr_decl)) |
|
854 | 846 |
(name, inputs, [], outputs, mem, mem) |
855 | 847 |
(pp_assigns pp_ptr_decl) outputs |
856 |
(pp_assigns (pp_reg self)) m.mmemory |
|
857 |
(pp_assigns pp_reset_flag') [self] |
|
858 |
(pp_assigns (pp_memory self)) (memories insts') |
|
859 |
(pp_assigns (pp_register_chain self)) insts |
|
860 |
(pp_assigns (pp_reset_flag_chain self)) insts'' |
|
861 |
(pp_assigns (pp_reg mem)) m.mmemory |
|
862 |
(pp_assigns pp_reset_flag') [mem] |
|
863 |
(pp_assigns (pp_memory ~indirect:false mem)) (memories insts') |
|
864 |
(pp_assigns (pp_register_chain ~indirect:false mem)) insts |
|
865 |
(pp_assigns (pp_reset_flag_chain ~indirect:false mem)) insts'' |
|
866 |
) |
|
848 |
(pp_assigns (pp_reg self)) |
|
849 |
m.mmemory |
|
850 |
(pp_assigns pp_reset_flag') |
|
851 |
[ self ] |
|
852 |
(pp_assigns (pp_memory self)) |
|
853 |
(memories insts') |
|
854 |
(pp_assigns (pp_register_chain self)) |
|
855 |
insts |
|
856 |
(pp_assigns (pp_reset_flag_chain self)) |
|
857 |
insts'' |
|
858 |
(pp_assigns (pp_reg mem)) |
|
859 |
m.mmemory |
|
860 |
(pp_assigns pp_reset_flag') |
|
861 |
[ mem ] |
|
862 |
(pp_assigns (pp_memory ~indirect:false mem)) |
|
863 |
(memories insts') |
|
864 |
(pp_assigns (pp_register_chain ~indirect:false mem)) |
|
865 |
insts |
|
866 |
(pp_assigns (pp_reset_flag_chain ~indirect:false mem)) |
|
867 |
insts'') |
|
867 | 868 |
fmt () |
868 | 869 |
|
869 |
let pp_ghost_instr_code m self fmt instr = match instr.instr_desc with |
|
870 |
let pp_ghost_instr_code m self fmt instr = |
|
871 |
match instr.instr_desc with |
|
870 | 872 |
| MStateAssign (x, v) -> |
871 | 873 |
fprintf fmt "@,%a" |
872 |
(pp_acsl_line |
|
873 |
(pp_ghost |
|
874 |
(pp_assign m self (pp_c_var_read m)))) |
|
874 |
(pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m)))) |
|
875 | 875 |
(x, v) |
876 | 876 |
| MResetAssign b -> |
877 |
fprintf fmt "@,%a" |
|
878 |
(pp_acsl_line |
|
879 |
(pp_ghost |
|
880 |
(pp_reset_assign self))) |
|
881 |
b |
|
877 |
fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b |
|
882 | 878 |
| MSetReset inst -> |
883 | 879 |
let td, _ = List.assoc inst m.minstances in |
884 | 880 |
if Arrow.td_is_arrow td then |
885 |
fprintf fmt "@,%a;" |
|
886 |
(pp_acsl_line |
|
887 |
(pp_ghost |
|
888 |
(pp_arrow_reset_ghost self))) |
|
889 |
inst |
|
890 |
| _ -> () |
|
881 |
fprintf fmt "@,%a;" |
|
882 |
(pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self))) |
|
883 |
inst |
|
884 |
| _ -> |
|
885 |
() |
|
891 | 886 |
|
892 | 887 |
let pp_step_instr_spec m self mem fmt instr = |
893 | 888 |
fprintf fmt "%a%a" |
894 |
(pp_ghost_instr_code m mem) instr |
|
889 |
(pp_ghost_instr_code m mem) |
|
890 |
instr |
|
895 | 891 |
(pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut |
896 | 892 |
(pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m)))) |
897 | 893 |
instr.instr_spec |
... | ... | |
899 | 895 |
let pp_ghost_parameter mem fmt inst = |
900 | 896 |
GhostProto.pp_ghost_parameters ~cut:false fmt |
901 | 897 |
(match inst with |
902 |
| Some inst -> |
|
903 |
[inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)] |
|
904 |
| None -> |
|
905 |
[mem, pp_print_string]) |
|
906 |
|
|
898 |
| Some inst -> |
|
899 |
[ (inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)) ] |
|
900 |
| None -> |
|
901 |
[ mem, pp_print_string ]) |
|
907 | 902 |
end |
908 | 903 |
|
909 | 904 |
(**************************************************************************) |
... | ... | |
911 | 906 |
(**************************************************************************) |
912 | 907 |
|
913 | 908 |
module MakefileMod = struct |
914 |
|
|
915 | 909 |
let other_targets fmt basename _nodename dependencies = |
916 | 910 |
fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@."; |
917 | 911 |
(* EACSL version of library file . c *) |
918 | 912 |
fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename; |
919 | 913 |
fprintf fmt |
920 |
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@." |
|
914 |
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \ |
|
915 |
e-acsl -print -ocode %s_eacsl.c@." |
|
921 | 916 |
basename basename; |
922 | 917 |
fprintf fmt "@."; |
923 | 918 |
fprintf fmt "@."; |
924 | 919 |
|
925 |
(* EACSL version of library file . c + main .c *) |
|
926 |
fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename; |
|
927 |
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@." |
|
920 |
(* EACSL version of library file . c + main .c *) |
|
921 |
fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename |
|
922 |
basename basename; |
|
923 |
fprintf fmt |
|
924 |
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \ |
|
925 |
-then-on e-acsl -print -ocode %s_main_eacsl.i@." |
|
928 | 926 |
basename basename basename; |
929 | 927 |
(* Ugly hack to deal with eacsl bugs *) |
930 |
fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename; |
|
928 |
fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" |
|
929 |
basename basename; |
|
931 | 930 |
fprintf fmt "@."; |
932 | 931 |
fprintf fmt "@."; |
933 | 932 |
|
934 | 933 |
(* EACSL version of binary *) |
935 | 934 |
fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename; |
936 |
fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *) |
|
935 |
fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." |
|
936 |
basename; |
|
937 |
(* compiling instrumented lib + main *) |
|
937 | 938 |
C_backend_makefile.fprintf_dependencies fmt dependencies; |
938 |
fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@." |
|
939 |
fprintf fmt |
|
940 |
"\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \ |
|
941 |
%s_main_eacsl.o %a@." |
|
939 | 942 |
basename |
940 |
(Utils.fprintf_list ~sep:" " (fun fmt dep -> Format.fprintf fmt "%s.o" dep.name)) |
|
943 |
(Utils.fprintf_list ~sep:" " (fun fmt dep -> |
|
944 |
Format.fprintf fmt "%s.o" dep.name)) |
|
941 | 945 |
(C_backend_makefile.compiled_dependencies dependencies) |
942 | 946 |
("${FRAMACEACSL}/e_acsl.c " |
943 |
^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
|
|
944 |
^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
|
|
947 |
^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c " |
|
948 |
^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c") |
|
945 | 949 |
basename |
946 | 950 |
(Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib)) |
947 |
(C_backend_makefile.lib_dependencies dependencies) |
|
948 |
; |
|
951 |
(C_backend_makefile.lib_dependencies dependencies); |
|
949 | 952 |
fprintf fmt "@." |
950 |
|
|
951 | 953 |
end |
952 | 954 |
|
953 | 955 |
(* Local Variables: *) |
Also available in: Unified diff
reformatting