Project

General

Profile

Download (33.1 KB) Statistics
| Branch: | Tag: | Revision:
1
open Format
2
open LustreSpec
3
open Machine_code
4
open Corelang
5
open C_backend_common
6
open C_backend_spec
7
open Utils
8
open Types
9

    
10
let fullExists () = !Options.acsl_spec_fullExists 
11

    
12
let rec list_to_partial l = match l with
13
  | []   -> [[]]
14
  | _::q -> l::(list_to_partial q)
15

    
16

    
17
(* Print a function call/declaration in acsl *) 
18
let pp_acsl_fun name fmt args =
19
    fprintf fmt "%s(@[<v>%a@])"
20
      name
21
      (Utils.fprintf_list ~sep:",@ " (fun fmt f-> f fmt)) args
22

    
23
(* Print an invariant call/decl in acsl *)
24
let pp_acsl_fun_init name self inst fmt mem =
25
  let arg = fun fmt-> (match inst, mem with
26
    | x,  None    -> fprintf fmt "%a %s" pp_machine_memtype_name name self
27
    | "", Some "" -> fprintf fmt "%s" self
28
    | "", Some m  -> fprintf fmt "\\at(*%s, %s)" self m
29
    | x,  Some "" -> fprintf fmt "%s.%s" self inst
30
    | x,  Some m  -> fprintf fmt "\\at(%s->%s, %s)" self inst m)
31
  in
32
  pp_acsl_fun ("init_"^name) fmt [arg]
33

    
34

    
35
let preprocess_acsl_instr calls outputs instr =
36
  match instr with 
37
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i && (not (List.mem i0 outputs)) ->
38
      Some (i0, Fun (i, vl))
39
    | MStep ([i0], i, vl) when (not (Basic_library.is_internal_fun i)) && (node_name (fst (List.assoc i calls)) = "_arrow") && (not (List.mem i0 outputs)) ->
40
      assert (List.length vl == 2);
41
      Some (i0, Fun ("arrow_"^i, vl))
42
    | MLocalAssign (i,v) when not (List.mem i outputs) ->
43
      Some (i, v)
44
    | _ -> None
45

    
46

    
47
let pp_cast fmt = function
48
  | Types.Tbool           -> fprintf fmt "(_Bool)"
49
  | Types.Treal           -> fprintf fmt "(double)"
50
  | Types.Tint            -> fprintf fmt "(int)"
51
  | _ -> assert false
52

    
53
let getFunType i args =
54
  match i, args with
55
  | "ite", [v1; v2; v3] -> v2
56
  | "uminus", [v] -> v
57
  | "not", [v] -> v
58
  | "impl", [v1; v2] -> v1
59
  | "=", [v1; v2] -> Types.Tbool
60
  | "mod", [v1; v2] -> v1
61
  | "xor", [v1; v2] -> v1
62
  | _, [v1; v2] -> v1
63
  | _ -> assert false
64

    
65
let rec get_val_type v =
66
match v with 
67
| Cst _
68
| LocalVar _ 
69
| StateVar _-> Machine_code.get_val_type v
70
| Fun (n, vl) -> getFunType n (List.map get_val_type vl)
71
| Array _
72
| Access _
73
| Power _ -> assert false
74

    
75
let get_var_type t = (Types.repr t.var_type).Types.tdesc
76

    
77
(* Print a machine instruction in acsl for transition lemma *) 
78
let rec pp_acsl_instr init vars instances calls self pointer fmt instr =
79
  let mem1 = if init then self else (self^"1") in
80
  let mem2 = if init then self else (self^"2") in
81
  match instr with 
82
    | MReset i ->
83
      let (node, static) = List.assoc i calls in
84
      assert (List.length static == 0);
85
      if node_name node = "_arrow" then
86
        fprintf fmt "(%s.%s._reg._first==1)" self i
87
      else
88
        pp_acsl_fun_init (node_name node) self i fmt (Some "")
89
    | MLocalAssign (i,v) -> 
90
      (match i.var_type.tdesc with Tbool -> fprintf fmt "((!%a) == (!%a))" | _ -> fprintf fmt "(%a == %a)")
91
      (pp_acsl_var_read "" pointer) i
92
      (pp_acsl_val mem1 (pp_acsl_var_read "" pointer)) v
93
    | MStateAssign (i,v) ->
94
      (match i.var_type.tdesc with Tbool -> fprintf fmt "((!%a) == (!%a))" | _ -> fprintf fmt "(%a == %a)")
95
      (pp_acsl_val mem2 (fun fmt v-> fprintf fmt "%s" v.var_id)) (StateVar i)
96
      (pp_acsl_val mem1 (pp_acsl_var_read "" pointer)) v
97
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
98
      pp_acsl_instr init vars calls instances self pointer fmt (MLocalAssign (i0, Fun (i, vl)))
99
    | MStep ([i0], i, [x;y]) when (not (Basic_library.is_internal_fun i)) && (node_name (fst (List.assoc i calls)) = "_arrow") ->
100
      fprintf fmt "(%a==(%s1.%s._reg._first?(%a):(%a))) && (%s2.%s._reg._first==0)"
101
        (pp_acsl_var_read "" pointer) i0
102
        self i
103
        (pp_acsl_val mem1 (pp_acsl_var_read "" [])) x
104
        (pp_acsl_val mem1 (pp_acsl_var_read "" [])) y
105
        self i
106
    | MStep (il, i, vl) ->
107
      let pp_val fmt x = (match get_val_type x with Types.Tbool -> fprintf fmt "%a" | _ -> fprintf fmt "%a") (pp_acsl_val mem1 (pp_acsl_var_read "" [])) x in
108
      pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i calls)))) fmt
109
      ((List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_val_type x)*) pp_val x) vl)@
110
      (List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read "" []) x) il)@
111
        (try ignore(List.assoc i instances);[(fun fmt->fprintf fmt "%s1.%s" self i);(fun fmt->fprintf fmt "%s2.%s" self i)] with Not_found -> []))
112
    | MBranch (g,hl) -> assert false (*TODO: useless : ????
113
      let t = fst (List.hd hl) in
114
      if hl <> [] && (t = tag_true || t = tag_false) then
115
        let tl = try List.assoc tag_true  hl with Not_found -> [] in
116
        let el = try List.assoc tag_false hl with Not_found -> [] in
117
        fprintf fmt "((%a)?(%a%s):(%a%s))"
118
          (pp_acsl_val mem1 (pp_acsl_var_read pointer)) g
119
          (Utils.fprintf_list ~sep:"&& " (pp_acsl_instr init vars calls self pointer)) tl
120
          (if List.length tl == 0 then "1" else "")
121
          (Utils.fprintf_list ~sep:"&& " (pp_acsl_instr init vars calls self pointer)) el
122
          (if List.length el == 0 then "1" else "")
123
      else assert false*)
124

    
125
(* Print all machine instructions in acsl for transition lemma *) 
126
let pp_acsl_instrs init outputs self pointer instances calls vars fmt instrs =
127
  if List.length instrs == 0 then fprintf fmt "\\true" else
128
  let handle (locals, instrs) i =
129
    match preprocess_acsl_instr calls outputs i with
130
      | None    -> (locals, i::instrs)
131
      | Some l  -> (l::locals, instrs)
132
  in
133
  let pp_let fmt (i, v) =
134
    match v with
135
      | Fun (s, [x;y]) when String.length s >= 6 && String.sub s 0 6 = "arrow_" ->
136
        let var = String.sub s 6 (String.length s - 6) in
137
        fprintf fmt "\\let %s = %s1.%s._reg._first?%a:%a; (%s2.%s._reg._first==0) &&"
138
          i.var_id
139
          self var
140
          (pp_acsl_val (self^"1") (pp_acsl_var_read "" [])) x
141
          (pp_acsl_val (self^"1") (pp_acsl_var_read "" [])) y
142
          self var
143
      | _ ->
144
        fprintf fmt "\\let %s = %a;"
145
          i.var_id
146
          (pp_acsl_val (self^"1") (pp_acsl_var_read "" pointer)) v
147
  in
148
  let (locals, instrs) = if fullExists () then ([], instrs) else List.fold_left handle ([], []) instrs in
149
  fprintf fmt "%a@,%a"
150
    (Utils.fprintf_list ~sep:"@," pp_let)
151
    (List.rev locals)
152
    (Utils.fprintf_list ~sep:" &&@," (pp_acsl_instr init vars instances calls self pointer))
153
    instrs
154

    
155
(* Take a dependance and print it for invariant predicate *)
156
(*
157
let pp_acsl_dep self instances fmt = function
158
  | Dep_Var s -> fprintf fmt "%s2._reg.%s == %s1._reg.%s" self s self s
159
  | Dep_Node s ->
160
    pp_acsl_fun ("inv_"^(node_name (fst (List.assoc s instances)))) fmt [fun fmt->fprintf fmt "%s1.%s" self i];
161
    fprintf fmt "&&@, %t == %t" (pp_acsl_at self s)
162
      (pp_acsl_at self s)
163
*)
164

    
165
(*
166
Require Why3.
167
intros.
168
unfold P_trans_AltitudeControl.
169
repeat split.
170
why3 "Z3" timelimit 10.
171
why3 "Z3" timelimit 10.
172
why3 "Z3" timelimit 10.
173
why3 "Z3" timelimit 10.
174
why3 "Z3" timelimit 10.
175
why3 "Z3" timelimit 10.
176
why3 "Z3" timelimit 10.
177
why3 "Z3" timelimit 10.
178
why3 "Z3" timelimit 10.
179
why3 "Z3" timelimit 10.
180
why3 "Z3" timelimit 10.
181
why3 "Z3" timelimit 10.
182
why3 "Z3" timelimit 10.
183
why3 "Z3" timelimit 10.
184
why3 "Z3" timelimit 10.
185
why3 "Z3" timelimit 10.
186
why3 "Z3" timelimit 10.
187
why3 "Z3" timelimit 10.
188
assert (a_9 = F_AltitudeControl_mem_ni_1 a_6).
189
why3 "Z3" timelimit 10.
190
assert (a_10 = F_AltitudeControl_mem_ni_1 a_7).
191
unfold F_AltitudeControl_mem_ni_1.
192
unfold a_7.
193
unfold Load_S_AltitudeControl_mem.
194
unfold a_10.
195
unfold a_8.
196
unfold havoc in H36.
197
unfold get.
198
clear.
199
rewrite <- H48.
200
rewrite <- H49.
201
apply H47.
202
*)
203

    
204
(* Print a transition call/decl in acsl *)
205
let pp_acsl_fun_trans infos pre name inputs outputs suffix flag_output self flag_mem locals fmt existential =
206
  let (locals, existential) = (*([], match existential with None -> None | Some x -> Some []) else*)
207
  match infos with
208
    | None -> (locals, existential)
209
    | Some (instrs, calls) ->
210
      let nonlocals = List.fold_left (fun l x-> match preprocess_acsl_instr calls outputs x with | Some (i, _) -> i::l | None -> l) [] instrs in
211
      (
212
        (if not (fullExists ()) then List.filter (fun x-> not (List.mem x nonlocals)) else fun x -> x) locals,
213
        match existential with None -> None | Some existential -> Some ((if not (fullExists ()) then List.filter (fun x-> not (List.mem x nonlocals)) else fun x -> x) existential)
214
      )
215
  in
216
  let mems = function 1 -> "Pre" | 2 -> "Here" | _ -> assert false in
217
  let pp_self_read =
218
    if flag_mem then fun i fmt-> (match i with 1 -> fprintf fmt "\\at(*%s, Pre)" self | 2 -> fprintf fmt "(*%s)" self | _ -> assert false)
219
    else fun i fmt-> fprintf fmt "%s%i" self (match suffix with None -> i | Some s -> s+i-1)
220
  in
221
  let (pp_var, pp_self) =
222
    match existential with
223
      | None    -> ((fun i -> pp_acsl_var_decl), (fun i fmt-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i))
224
      | Some ex -> (if List.length ex != 0 then fprintf fmt "\\exists %a;@," (Utils.fprintf_list ~sep:";@,\\exists " pp_acsl_var_decl) ex);
225
                   ((fun i -> pp_acsl_var_read i (if flag_output then outputs else [])), pp_self_read)
226
  in
227
  let pp_vars = List.map (fun x fmt-> match suffix with None-> pp_var "" fmt x | Some i -> fprintf fmt "%a" (pp_var (string_of_int (i+1))) x) in
228
    (pp_acsl_fun (pre^"trans_"^name)) fmt
229
    ((pp_vars (inputs@outputs))@(if not (self = "") then [pp_self 1;pp_self 2] else [])@(pp_vars locals))
230

    
231
(* Print an invariant call/decl in acsl *)
232
let pp_acsl_fun_inv depth name self fmt mem =
233
  let arg = fun fmt-> (match mem with
234
    | None -> fprintf fmt "%a %s%i" pp_machine_memtype_name name self depth
235
    | Some "" -> fprintf fmt "%s" self
236
    | Some "Here" -> fprintf fmt "*%s" self
237
    | Some m -> fprintf fmt "\\at(*%s, %s)" self m)
238
  in
239
  pp_acsl_fun ("inv_"^name) fmt [arg]
240

    
241
(* Print an invariant call/decl in acsl *)
242
let pp_acsl_inv depth name inputs outputs self fmt spec =
243
  let rec iter base x = function
244
    | i when i = base-1 -> []
245
    | i -> (i, x)::(iter base x (i-1))
246
  in
247
  let rec iterList base = function
248
    | []   -> []
249
    | t::q -> (iter base t depth)@(iterList base q)
250
  in
251
  let trans_pred fmt i =
252
    fprintf fmt "%a" (pp_acsl_fun_trans  None "C" name inputs outputs (Some i) false self false []) (Some [])
253
  in
254
  let pp_eexpr_expr self i j fmt ee = 
255
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read (string_of_int j) [])) ee.mmstep_logic.step_inputs self i
256
  in
257
  let spec_pred cor preds fmt i =
258
    let j = if cor then i + 1 else i in
259
    if List.length preds != 0 then
260
        fprintf fmt "(%a)%s" (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self i j)) preds (if cor then " &&@," else "")
261
    else ()
262
  in
263
  let aux fmt base =
264
    let selfs = iter base self (depth-1) in
265
    let ios = iterList (base + 1) (inputs@outputs) in
266
    (if List.length selfs == 0 && List.length ios == 0 then 
267
      fprintf fmt "(%a%t%a%t)"
268
     else
269
      fprintf fmt "(\\exists %a%t%a;@,%a%t%a%t)"
270
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i)) selfs
271
        (Utils.pp_final_char_if_non_empty ", " (iter base self (depth-1)))
272
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a%i" pp_acsl_var_decl x i)) ios
273
    )
274
      (Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i)) (iter base trans_pred (depth-1))
275
      (Utils.pp_final_char_if_non_empty "&&@," (iter base trans_pred (depth-1))) 
276
      (Utils.fprintf_list ~sep:"" (fun fmt (i, f)-> fprintf fmt "%a" f i)) (iter base (spec_pred true spec.m_requires) (depth-1))
277
      (fun fmt->
278
        if base == 0 then
279
          Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i) fmt (iter (base+1) (spec_pred false spec.m_ensures) depth)
280
        else
281
          pp_acsl_fun_init name (self^(string_of_int base)) "" fmt (Some "")
282
      )
283
  in
284
  Utils.fprintf_list ~sep:"||@," (fun fmt (i, f)-> fprintf fmt "%a" f i) fmt (iter 0 aux depth)
285

    
286
(* Print the invariant lemma *)
287
let pp_acsl_lem_inv depth name inputs outputs self fmt spec =
288
  let pp_eexpr_expr self j fmt ee =
289
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read "" [])) ee.mmstep_logic.step_inputs self j
290
  in
291
  fprintf fmt "\\forall %a %s1, %s2, %a;@,%a==>@,%a==>@,%a%t%a"
292
    pp_machine_memtype_name name self self
293
    (Utils.fprintf_list ~sep:", " pp_acsl_var_decl) (inputs@outputs)
294
    (pp_acsl_fun_inv depth name (self^"1")) (Some "")
295
    (pp_acsl_fun_trans None "C" name inputs outputs None false self false []) (Some [])
296
    (Utils.fprintf_list ~sep:"==>@," (pp_eexpr_expr self 1)) spec.m_requires
297
    (Utils.pp_final_char_if_non_empty "==>@," spec.m_requires)
298
    (pp_acsl_fun_inv depth name (self^"2")) (Some "")
299

    
300
(* Print lemma init *)
301
let pp_acsl_lem_init k depth name inputs outputs self fmt spec =
302
  let rec iter base x = function
303
    | i when i = base-1 -> []
304
    | i -> (i, x)::(iter base x (i-1))
305
  in
306
  let rec iterList base = function
307
    | []   -> []
308
    | t::q -> (iter base t depth)@(iterList base q)
309
  in
310
  let trans_pred fmt i =
311
    fprintf fmt "%a" (pp_acsl_fun_trans  None "C" name inputs outputs (Some i) false self false []) (Some [])
312
  in
313
  let spec_pred fmt i =
314
    let pp_eexpr_expr self j fmt ee = 
315
      fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read (string_of_int i) [])) ee.mmstep_logic.step_inputs self j
316
    in
317
    fprintf fmt "%a(%a)"
318
    (Utils.fprintf_list ~sep:"" ((fun fmt (w, x)-> fprintf fmt "%a%t"
319
      (Utils.fprintf_list ~sep:"==>@," (pp_eexpr_expr self (w))) spec.m_requires
320
      (Utils.pp_final_char_if_non_empty "==>@," spec.m_requires)
321
    ))) (iter k None (depth -1))
322
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self (i))) spec.m_ensures
323
  in
324
  let aux fmt base =
325
    let selfs = iter base self (depth) in
326
    let ios = iterList (base + 1) (inputs@outputs) in
327
    (if List.length selfs == 0 && List.length ios == 0 then 
328
      fprintf fmt "(%a%t%t)"
329
     else
330
      fprintf fmt "\\forall %a%t%a;@,%a%t%t"
331
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i)) selfs
332
        (Utils.pp_final_char_if_non_empty ", " (iter base self (depth-1)))
333
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a%i" pp_acsl_var_decl x i)) ios
334
    )
335
      (Utils.fprintf_list ~sep:"==>@," (fun fmt (i, f)-> fprintf fmt "%a" f i)) (iter base trans_pred (depth-1))
336
      (Utils.pp_final_char_if_non_empty "==>@," (iter base trans_pred (depth-1))) 
337
      (fun fmt->
338
          pp_acsl_fun_init name (self^(string_of_int base)) "" fmt (Some "")
339
      )
340
  in
341
  fprintf fmt "%a ==> %a" aux k spec_pred depth
342

    
343
(* Print the spec lemma *)
344
let pp_acsl_lem_spec depth name inputs outputs self fmt spec =
345
  let pp_eexpr_expr self j fmt ee =
346
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read "" [])) ee.mmstep_logic.step_inputs self j
347
  in
348
  fprintf fmt "\\forall %a %s1, %s2, %a;@,%a==>@,%a==>@,%a%t%a"
349
    pp_machine_memtype_name name self self
350
    (Utils.fprintf_list ~sep:", " pp_acsl_var_decl) (inputs@outputs)
351
    (pp_acsl_fun_inv depth name (self^"1")) (Some "")
352
    (pp_acsl_fun_trans None "C" name inputs outputs None false self false []) (Some [])
353
    (Utils.fprintf_list ~sep:"==>@," (pp_eexpr_expr self 1)) spec.m_requires
354
    (Utils.pp_final_char_if_non_empty "==>@," spec.m_requires)
355
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self 2)) spec.m_ensures
356

    
357
let getDepth m =
358
  try (
359
    match (List.assoc ["k"] (List.flatten (List.map (fun x-> x.annots) m.mannot))).eexpr_qfexpr.expr_desc with
360
      | (Expr_const (Const_int k)) -> k
361
      | _ -> 0
362
  ) with Not_found -> 0
363

    
364
(* Get the instructions from acsl spec effect *)
365
let get_instrs_effect spec =
366
  let effects = spec.m_requires@spec.m_ensures@
367
    (List.fold_left 
368
       (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
369
      [] spec.m_behaviors)
370
  in
371
  let effects = List.filter (fun ee -> ee.mmstep_effects.step_instrs <> []) effects in
372
  List.flatten (List.map (fun e -> e.mmstep_effects.step_instrs) effects)
373

    
374
let get_instrs_effect_init spec =
375
  let effects = spec.m_requires@spec.m_ensures@
376
    (List.fold_left 
377
       (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
378
       [] spec.m_behaviors)
379
  in
380
  
381
  let effects = List.filter (fun ee -> ee.mminit <> []) effects in
382
  List.flatten (List.map (fun e -> e.mminit) effects)
383

    
384
module Make = 
385
  functor (SpecArg: SPECARG) -> 
386
struct
387
  
388
  open SpecArg
389

    
390
  module Spec = Make(SpecArg)
391

    
392
  let init m = Spec.init m
393

    
394
  module HdrMod = struct
395

    
396
    (* Print all the proof stuff *)
397
    let pp_acsl_def_trans stateless fmt m =
398
      let name = m.mname.node_id in
399
      let inputs = m.mstep.step_inputs in
400
      let outputs = m.mstep.step_outputs in
401
      let locals = m.mstep.step_locals in
402
      let memory = m.mmemory in
403
      let vars = inputs@outputs@locals@memory in
404
      let depth = getDepth m in
405
      let instrs = match m.mspec with None -> [] | Some spec -> get_instrs_effect (Spec.get_spec m.mname) in
406
      let instrs_init =  match m.mspec with None -> [] | Some spec -> get_instrs_effect_init (Spec.get_spec m.mname) in
407
      let induction = (not stateless) && (getDepth m != 0) in
408
      if m.mname.node_id <> arrow_id then (
409
        let self = if stateless then "" else mk_self m in
410
        fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
411
          (pp_acsl_fun_trans (Some (m.mstep.step_instrs, m.mcalls)) "" name inputs outputs None false self false locals) None
412
            (pp_acsl_instrs false outputs self [] m.minstances m.mcalls vars) (m.mstep.step_instrs@instrs);
413
        fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
414
          (pp_acsl_fun_trans None "C" name inputs outputs None false self false []) None
415
            (pp_acsl_fun_trans (Some (m.mstep.step_instrs, m.mcalls)) "" name inputs outputs None false self false locals) (Some locals);
416
        (if not stateless then fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
417
          (pp_acsl_fun_init name self "") None
418
            (pp_acsl_instrs true [] self [] m.minstances m.mcalls vars) (m.minit@instrs_init));
419
        if induction then (
420
        match m.mspec with None -> () | Some spec -> (
421
          let spec = (Spec.get_spec m.mname) in
422
          fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@." (pp_acsl_fun_inv depth name self) None (pp_acsl_inv depth name inputs outputs self) spec;
423
          for i = 0 to depth-1 do
424
            fprintf fmt "/*@@ @[<v 3>lemma inv_init_%i_%s : @;%a;@]@;*/@." (depth-i) name (pp_acsl_lem_init i depth name inputs outputs self) spec;
425
          done;
426
          fprintf fmt "/*@@ @[<v 3>lemma inv_spec_%s : @;%a;@]@;*/@." name (pp_acsl_lem_spec depth name inputs outputs self) spec;
427
          fprintf fmt "/*@@ @[<v 3>lemma inv_inv_%s : @;%a;@]@;*/@." name (pp_acsl_lem_inv depth name inputs outputs self) spec
428
        )
429
      ))
430
    let _print_machine_decl_step_fun_prefix stateless fmt m =
431
      let self = mk_self m in
432
      let induction = (not stateless) && (getDepth m != 0) in
433
      let pre_inv = fun fmt -> fprintf fmt "requires %a;@," (pp_acsl_fun_inv (getDepth m) m.mname.node_id self) (Some "Here") in
434
      let post_inv = fun fmt -> fprintf fmt "ensures %a;@," (pp_acsl_fun_inv (getDepth m) m.mname.node_id self) (Some "Here") in
435
        let post_trans = fun fmt -> fprintf fmt "ensures %a;@," (pp_acsl_fun_trans None "C" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true (if stateless then "" else self) true []) (Some []) in
436
      let pre = match m.mspec with
437
        | Some _ when induction -> pre_inv
438
        | _ -> fun fmt -> ()
439
      in
440
      let post = match m.mspec with
441
        | Some _ when induction -> fun fmt -> fprintf fmt "%t%t" post_inv post_trans
442
        | _ -> post_trans
443
      in
444
      Spec.HdrMod._print_machine_decl_step_fun_prefix stateless pre post fmt m
445

    
446
    let has_spec_mem m = Spec.HdrMod.has_spec_mem m
447
    let pp_registers_struct fmt m = Spec.HdrMod.pp_registers_struct fmt m
448
    let print_machine_decl_prefix fmt m =
449
        let mems = Machine_code.get_mems m machines in
450
        fprintf fmt "%a%a"
451
          Spec.HdrMod.print_machine_decl_prefix m
452
          (pp_acsl_def_trans (List.length mems == 0)) m
453
    let print_machine_decl_step_fun_prefix fmt m = _print_machine_decl_step_fun_prefix false fmt m
454
    
455
    let print_machine_decl_init_fun_prefix fmt m =
456
      let self = mk_self m in
457
      let post fmt = 
458
          fprintf fmt "ensures %a;@." (pp_acsl_fun_init m.mname.node_id self "") (Some "Here");
459
        match m.mspec with
460
        | Some _ when getDepth m != 0 ->
461
            fprintf fmt "ensures %a;@." (pp_acsl_fun_inv (getDepth m) m.mname.node_id self) (Some "Here")
462
        | _ -> ()
463
          
464
      in
465
      Spec.HdrMod._print_machine_decl_init_fun_prefix (fun fmt-> ()) post fmt m
466
    
467
    let print_machine_decl_stateless_fun_prefix fmt m = _print_machine_decl_step_fun_prefix true fmt m
468
    
469
    let print_global_decl fmt = fprintf fmt "/*@@ @[<v 3>lemma missing: \\forall _Bool x; (x != 0) <==> (((int) x) != 0);*/@."
470
  end
471

    
472
  module SrcMod =
473
  struct
474
    let print_step_code_prefix pp_machine_instr stateless fmt m =
475
      let inputs = m.mstep.step_inputs in
476
      let outputs = m.mstep.step_outputs in
477
      let locals = m.mstep.step_locals in
478
      let mems = Machine_code.get_mems m machines in
479
      let self = if List.length mems == 0 then "" else mk_self m in
480
      fprintf fmt "/*@@ensures %a;@,%a*/@,{@," 
481
        (pp_acsl_fun_trans None "C" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true (if stateless then "" else self) true []) (Some [])
482
        (C_backend_spec.pp_assigns [] stateless machines) m
483
    let print_step_code_midfix pp_machine_instr stateless fmt m =
484
      let inputs = m.mstep.step_inputs in
485
      let outputs = m.mstep.step_outputs in
486
      let locals = m.mstep.step_locals in
487
      let mems = Machine_code.get_mems m machines in
488
      let self = if List.length mems == 0 then "" else mk_self m in
489
      let instrs = match m.mspec with None -> [] | Some spec -> get_instrs_effect (Spec.get_spec m.mname) in
490
      let memory = m.mmemory in
491
      let vars = inputs@outputs@locals@memory in
492
      let filtered_existencials = (if (fullExists ()) then 
493
        let nonlocals = List.fold_left (fun l x-> match preprocess_acsl_instr m.mcalls outputs x with | Some (i, _) -> i::l | None -> l) [] m.mstep.step_instrs in
494
        List.filter (fun x-> not (List.mem x nonlocals))else fun x -> x) locals
495
      in
496
      Format.fprintf fmt "@,/* Asserting trans predicate: locals are [%a] */@,"
497
        (fprintf_list ~sep:", " Printers.pp_var) filtered_existencials;
498
      (Utils.fprintf_list ~sep:"@," 
499
        (fun fmt x -> 
500
          fprintf fmt "/*@@ensures %a;@,%a*/@,{@," 
501
        (pp_acsl_fun_trans 
502
           (Some (m.mstep.step_instrs, m.mcalls)) 
503
           "" (* no predicate prefix *)
504
           m.mname.node_id
505
           inputs 
506
           outputs 
507
           None 
508
           true
509
           self
510
           true
511
           locals
512
        ) 
513
        (Some x) 
514
        (C_backend_spec.pp_assigns (List.map (fun x fmt-> Printers.pp_var_name fmt x) locals) stateless machines) m)
515
     )
516
    fmt (list_to_partial filtered_existencials)
517
    
518
    let print_step_code_postfix pp_machine_instr stateless fmt m =
519
      let inputs = m.mstep.step_inputs in
520
      let outputs = m.mstep.step_outputs in
521
      let locals = m.mstep.step_locals in
522
      let memory = m.mmemory in
523
      let vars = inputs@outputs@locals@memory in
524
      let mems = Machine_code.get_mems m machines in
525
      let self = if List.length mems == 0 then "" else mk_self m in
526
      Spec.SrcMod.print_step_code_postfix pp_machine_instr stateless fmt m;
527
      
528
      let filtered_existencials = (if (fullExists ()) then 
529
        let nonlocals = List.fold_left (fun l x-> match preprocess_acsl_instr m.mcalls outputs x with | Some (i, _) -> i::l | None -> l) [] m.mstep.step_instrs in
530
        List.filter (fun x-> not (List.mem x nonlocals)) else fun x -> x) locals
531
      in
532
      
533
      for i = 0 to List.length filtered_existencials + 1 (*+ 1*) do
534
        fprintf fmt "}"
535
      done (*;
536
    fprintf fmt "/*@@%a@,%a*/ {"
537
      (pp_acsl_instrs_assert false outputs self m.minstances m.mcalls vars) (m.mstep.step_instrs@instrs)
538
      (C_backend_spec.pp_assigns (List.map (fun x fmt-> Printers.pp_var_name fmt x) locals) stateless machines) m*)
539
    
540
    let print_instr_prefix m fmt instr =
541
      let inputs = m.mstep.step_inputs in
542
      let outputs = m.mstep.step_outputs in
543
      let locals = m.mstep.step_locals in
544
      let memory = m.mmemory in
545
      let mems = Machine_code.get_mems m machines in
546
      let pointer = outputs in
547
      let self = if List.length mems == 0 then "" else mk_self m in
548
      let mem1 = "\\at(*"^self^", Pre)" in
549
      let mem2 = "(*"^self^")" in
550
      let rec pp_instr fmt = function
551
        | MReset i ->
552
          let (node, static) = List.assoc i m.mcalls in
553
          assert (List.length static == 0);
554
          if node_name node = "_arrow" then
555
            fprintf fmt "(%s.%s._reg._first==1)" mem2 i
556
          else
557
            pp_acsl_fun_init (node_name node) mem2 i fmt (Some "")
558
        | MLocalAssign (i,v) -> 
559
          (match i.var_type.tdesc with Tbool -> fprintf fmt "((!%a) == (!%a))" | _ -> fprintf fmt "(%a == %a)")
560
          (pp_acsl_var_read "" pointer) i
561
          (pp_acsl_val mem1 (pp_acsl_var_read "" pointer)) v
562
        | MStateAssign (i,v) ->
563
          (match i.var_type.tdesc with Tbool -> fprintf fmt "((!%a) == (!%a))" | _ -> fprintf fmt "(%a == %a)")
564
          (pp_acsl_val mem2 (pp_acsl_var_read "" pointer)) (StateVar i)
565
          (pp_acsl_val mem1 (pp_acsl_var_read "" pointer)) v
566
        | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
567
          pp_instr fmt (MLocalAssign (i0, Fun (i, vl)))
568
        | MStep ([i0], i, [x;y]) when (not (Basic_library.is_internal_fun i)) && (node_name (fst (List.assoc i m.mcalls)) = "_arrow") ->
569
          fprintf fmt "(%a==(%s.%s._reg._first?(%a):(%a))) && (%s.%s._reg._first==0)"
570
            (pp_acsl_var_read "" pointer) i0
571
            mem1 i
572
            (pp_acsl_val mem1 (pp_acsl_var_read "" [])) x
573
            (pp_acsl_val mem1 (pp_acsl_var_read "" [])) y
574
            mem2 i
575
        | MStep (il, i, vl) ->
576
          let pp_val fmt x = (match get_val_type x with Types.Tbool -> fprintf fmt "%a" | _ -> fprintf fmt "%a") (pp_acsl_val mem1 (pp_acsl_var_read "" [])) x in
577
          pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i m.mcalls)))) fmt
578
          ((List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_val_type x)*) pp_val x) vl)@
579
          (List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read "" []) x) il)@
580
            (try ignore(List.assoc i m.minstances);[(fun fmt->fprintf fmt "%s.%s" mem1 i);(fun fmt->fprintf fmt "%s.%s" mem2 i)] with Not_found -> []))
581
        | MBranch (g,hl) -> assert false
582
      in
583
      let mods = match instr with
584
        | MReset i -> [fun fmt -> fprintf fmt "%s.%s" mem2 i]
585
        | MLocalAssign (i,v) -> [fun fmt -> if List.exists (fun o -> o.var_id = i.var_id) pointer
586
    then fprintf fmt "*%s" i.var_id
587
    else fprintf fmt "%s" i.var_id]
588
        | MStateAssign (i,v) -> [fun fmt -> fprintf fmt "%a" (pp_acsl_val mem2 (pp_acsl_var_read "" pointer)) (StateVar i)]
589
        | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> [fun fmt -> fprintf fmt "%a" (pp_acsl_var_read "" pointer) i0]
590
        | MStep ([i0], i, [x;y]) when (not (Basic_library.is_internal_fun i)) && (node_name (fst (List.assoc i m.mcalls)) = "_arrow") ->
591
          [fun fmt-> fprintf fmt "%t, %s.%s" (fun fmt -> if List.exists (fun o -> o.var_id = i0.var_id) pointer
592
    then fprintf fmt "*%s" i0.var_id
593
    else fprintf fmt "%s" i0.var_id) mem2 i]
594
        | MStep (il, i, vl) -> (List.map (fun x fmt-> if List.exists (fun o -> o.var_id = x.var_id) pointer
595
    then fprintf fmt "*%s" x.var_id
596
    else fprintf fmt "%s" x.var_id) il)@
597
            (try ignore(List.assoc i m.minstances);[(fun fmt->fprintf fmt "%s.%s" mem1 i);(fun fmt->fprintf fmt "%s.%s" mem2 i)] with Not_found -> [])
598
        | MBranch (g,hl) -> assert false
599
      in
600
      fprintf fmt "/*@@@,ensures %a;@,assigns %a;@,*/@,{@," pp_instr instr (fprintf_list ~sep:", " (fun fmt x-> x fmt)) mods
601
        
602
    let print_instr_postfix m fmt instr =
603
      fprintf fmt "@,}"
604
    
605
    let print_init_code_postfix pp_machine_instr fmt m = Spec.SrcMod.print_init_code_postfix pp_machine_instr fmt m
606
  end
607

    
608
  module MakefileMod =
609
  struct
610
    let other_targets fmt basename nodename dependencies = Spec.MakefileMod.other_targets fmt basename nodename dependencies
611
  end
612

    
613
  module MainMod =
614
  struct
615
    let print_while_prefix fmt m =
616
  (match m.mspec with
617
      | Some _ when getDepth m != 0 -> fprintf fmt "/*@@ loop invariant %a;*/@," (pp_acsl_fun_inv (getDepth m) m.mname.node_id "main_mem") (Some "")
618
      | _ -> ()
619
  );
620
  end
621

    
622
  module CoqMod =
623
  struct
624

    
625
    let repeat n fmt x =
626
        for i = 0 to n - 1 do
627
            fprintf fmt "%s" x
628
        done
629

    
630
    let pp_intro_hyp fmt k =
631
      fprintf fmt "(*nb: %i*)\nintros " k;
632
      repeat (k-1) fmt "[? ";
633
      fprintf fmt "?";
634
      repeat (k-1) fmt "]";
635
      fprintf fmt ".\n"
636

    
637
    let pp_choose nbcase fmt k =
638
      fprintf fmt "(*choose case %i/%i*)\n" (k+1) nbcase;
639
      repeat k fmt "right.\n";
640
      (if k != nbcase - 1 then fprintf fmt "left.\n")
641

    
642
    let pp_intros_exists fmt =
643
        fprintf fmt "repeat eapply ex_intro.\n"
644

    
645
    let pp_split fmt k =
646
      fprintf fmt "(*nb goals: %i(split one less)*)\n" k;
647
      repeat (k-1) fmt "split.\nFocus 2.\n"
648

    
649
    let pp_eassumption fmt k =
650
      repeat k fmt "eassumption.\n"
651

    
652

    
653
    let pp_apply_lem_init fmt k =
654
      fprintf fmt "eapply (Q_inv_init_%i_AltitudeControl).\n" k;
655
      let nbgoals = k+1+k+2 in
656
      for i = 0 to k-1 do
657
        fprintf fmt "Focus %i.\n" (nbgoals-i);
658
        fprintf fmt "eassumption.\n";
659
      done;
660
      for i = 1 to nbgoals-k do
661
        fprintf fmt "eassumption.\n";
662
      done
663

    
664
    let pp_apply_inv_spec fmt name =
665
      fprintf fmt "eapply Q_inv_spec_%s.\n" name;
666
      fprintf fmt "Focus 5.\n";
667
      for i = 1 to 5 do
668
        fprintf fmt "eassumption.\n"
669
      done
670

    
671
    let pp_case nbgoals1 nbgoals2 nbgoals3 nbintro nbcase case_hyp case_goal fmt name =
672
      let nbgoals = nbgoals1 + nbgoals2 + nbgoals3 in
673
      if case_hyp != nbcase - 1 then (
674
        fprintf fmt "intros h.\n";
675
        fprintf fmt "elim h;clear h.\n"
676
      );
677
      pp_intro_hyp fmt nbintro;
678
      pp_choose nbcase fmt case_goal;
679
      pp_intros_exists fmt;
680
      pp_split fmt nbgoals;
681
      pp_eassumption fmt nbgoals3;
682
      (
683
      if case_hyp == nbcase -2 then
684
        for i = 0 to case_goal - 1 do
685
          pp_apply_lem_init fmt (case_goal - i)
686
        done
687
      else (if case_hyp == nbcase -1 then
688
        (pp_apply_inv_spec fmt name;
689
        for i = 1 to nbgoals2 - 1 do
690
          fprintf fmt "eassumption.\n"
691
        done)
692
      else
693
        ())
694
      );
695
      pp_eassumption fmt nbgoals1
696
    
697
    let pp_code_inv_inv m fmt name =
698
      let inputs = m.mstep.step_inputs in
699
      let outputs = m.mstep.step_outputs in
700
      let locals = m.mstep.step_locals in
701
      let memory = m.mmemory in
702
      let vars = inputs@outputs@locals@memory in
703
      let depth = getDepth m in
704
      let nbcase = depth + 1 in
705
      let spec = (Spec.get_spec m.mname) in
706
      fprintf fmt "intros.\n";
707
      fprintf fmt "generalize H2.\n";
708
      fprintf fmt "unfold P_inv_%s.\n" name;
709
      let computeAnd k = (
710
        1*k + (*mems*)
711
        (List.length spec.m_requires)*k + (*pre*)
712
        (if k == nbcase -1 then 0 else 1), (*init*)
713
        (if k == nbcase -1 then (List.length spec.m_ensures) else 0)*k, (*post*)
714
        1*k (*trans*)
715
      ) in
716
      for case_hyp = 0 to nbcase - 1 do
717
        let case_goal = min (case_hyp+1) (nbcase -1) in
718
        let (nbgoals1, nbgoals2, nbgoals3) = computeAnd case_goal in
719
        let (nbhyp1, nbhyp2, nbhyp3) = computeAnd case_hyp in
720
        let vars = ((List.length inputs) + (List.length outputs) + 1)*case_hyp in
721
        let nbintro = vars + nbhyp1 + nbhyp2 + nbhyp3 in
722
        fprintf fmt "(*Case %i/%i -> %i/%i*)\n" (case_hyp+1) nbcase (case_goal+1) nbcase;
723
        fprintf fmt "(*nb var and hyps in case hyp: %i+%i+%i+%i*)\n" vars nbhyp1 nbhyp2 nbhyp3;
724
        fprintf fmt "(*nb goals in case goal : %i+%i+%i*)\n" nbgoals1 nbgoals2 nbgoals3;
725
        pp_case nbgoals1 nbgoals2 nbgoals3 nbintro  nbcase case_hyp case_goal fmt name
726
      done
727

    
728
    let pp_code_inv fmt name =
729
      fprintf fmt "intros.\n";
730
      fprintf fmt "eapply Q_inv_inv_%s.\n" name;
731
      fprintf fmt "Focus 4.\n";
732
      fprintf fmt "eassumption.\n";
733
      fprintf fmt "eassumption.\n";
734
      fprintf fmt "eassumption.\n";
735
      fprintf fmt "eassumption.\n"
736

    
737
    (*
738
      fprintf fmt "intros;\n";
739
      fprintf fmt "eapply Q_inv_inv_%s;" name;
740
      fprintf fmt "match goal with | |- context [P_Ctrans_%s]=> eassumption | _ => idtac end;\n" name;
741
      fprintf fmt "intuition;\n";
742
      fprintf fmt "(match goal with";
743
      fprintf fmt "  | |- context [if ?t then _ else _] => destruct t\n";
744
      fprintf fmt "  | _ => idtac\n";
745
      fprintf fmt "  end);hnf;try omega;intuition.\n"
746
    *)
747

    
748
    let pp_coq_goal name goalname code fmt =
749
        fprintf fmt "Goal %t.\nProof.\n%aQed.\n\n" (fun fmt-> fprintf fmt goalname name) code name
750

    
751
    let pp_coq stateless fmt m =
752
      match m.mspec with
753
        | Some _ ->
754
          let name = m.mname.node_id in
755
          if name <> arrow_id then (
756
            pp_coq_goal name "typed_%s_step_post" pp_code_inv fmt;
757
            pp_coq_goal name "typed_ref_%s_step_post" pp_code_inv fmt;
758
            pp_coq_goal name "typed_lemma_inv_inv_%s" (pp_code_inv_inv m) fmt
759
          )
760
        | _ -> ()
761

    
762
end
763

    
764
end
765
(* Local Variables: *)
766
(* compile-command:"make -C ../../.." *)
767
(* End: *)
(7-7/9)