Project

General

Profile

« Previous | Next » 

Revision 97602f7c

Added by Guillaume Davy over 9 years ago

Correct bug when there is no precondition and change reprensentation
of boolean in ACSL

View differences:

src/backends/C/c_backend_proof.ml
88 88
        pp_acsl_fun_init (node_name node) self i fmt (Some "")
89 89
    | MLocalAssign (i,v) -> 
90 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
91
      (pp_acsl_var_read "" pointer) i
92
      (pp_acsl_val mem1 (pp_acsl_var_read "" pointer)) v
93 93
    | MStateAssign (i,v) ->
94 94
      (match i.var_type.tdesc with Tbool -> fprintf fmt "((!%a) == (!%a))" | _ -> fprintf fmt "(%a == %a)")
95
      (pp_acsl_val mem2 (pp_acsl_var_read pointer)) (StateVar i)
96
      (pp_acsl_val mem1 (pp_acsl_var_read pointer)) v
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 97
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
98 98
      pp_acsl_instr init vars calls instances self pointer fmt (MLocalAssign (i0, Fun (i, vl)))
99 99
    | MStep ([i0], i, [x;y]) when (not (Basic_library.is_internal_fun i)) && (node_name (fst (List.assoc i calls)) = "_arrow") ->
100 100
      fprintf fmt "(%a==(%s1.%s._reg._first?(%a):(%a))) && (%s2.%s._reg._first==0)"
101
        (pp_acsl_var_read pointer) i0
101
        (pp_acsl_var_read "" pointer) i0
102 102
        self i
103
        (pp_acsl_val mem1 (pp_acsl_var_read [])) x
104
        (pp_acsl_val mem1 (pp_acsl_var_read [])) y
103
        (pp_acsl_val mem1 (pp_acsl_var_read "" [])) x
104
        (pp_acsl_val mem1 (pp_acsl_var_read "" [])) y
105 105
        self i
106 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
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 108
      pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i calls)))) fmt
109
      ((List.map (fun x fmt-> fprintf fmt "%a %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)@
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 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 112
    | MBranch (g,hl) -> assert false (*TODO: useless : ????
113 113
      let t = fst (List.hd hl) in
......
134 134
    match v with
135 135
      | Fun (s, [x;y]) when String.length s >= 6 && String.sub s 0 6 = "arrow_" ->
136 136
        let var = String.sub s 6 (String.length s - 6) in
137
        fprintf fmt "\\let %a = %s1.%s._reg._first?%a:%a; (%s2.%s._reg._first==0) &&"
138
          (pp_acsl_var_read pointer) i
137
        fprintf fmt "\\let %s = %s1.%s._reg._first?%a:%a; (%s2.%s._reg._first==0) &&"
138
          i.var_id
139 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
140
          (pp_acsl_val (self^"1") (pp_acsl_var_read "" [])) x
141
          (pp_acsl_val (self^"1") (pp_acsl_var_read "" [])) y
142 142
          self var
143 143
      | _ ->
144
        fprintf fmt "\\let %a = %a;"
145
          (pp_acsl_var_read pointer) i
146
          (pp_acsl_val (self^"1") (pp_acsl_var_read pointer)) v
144
        fprintf fmt "\\let %s = %a;"
145
          i.var_id
146
          (pp_acsl_val (self^"1") (pp_acsl_var_read "" pointer)) v
147 147
  in
148 148
  let (locals, instrs) = if fullExists () then ([], instrs) else List.fold_left handle ([], []) instrs in
149 149
  fprintf fmt "%a@,%a"
......
220 220
  in
221 221
  let (pp_var, pp_self) =
222 222
    match existential with
223
      | None    -> (pp_acsl_var_decl, (fun i fmt-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i))
223
      | None    -> ((fun i -> pp_acsl_var_decl), (fun i fmt-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i))
224 224
      | Some ex -> (if List.length ex != 0 then fprintf fmt "\\exists %a;@," (Utils.fprintf_list ~sep:";@,\\exists " pp_acsl_var_decl) ex);
225
                   (pp_acsl_var_read (if flag_output then outputs else []), pp_self_read)
225
                   ((fun i -> pp_acsl_var_read i (if flag_output then outputs else [])), pp_self_read)
226 226
  in
227
  let pp_vars = List.map (fun x fmt-> match suffix with None-> pp_var fmt x | Some i -> fprintf fmt "%a%i" pp_var x (i+1)) 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 228
    (pp_acsl_fun (pre^"trans_"^name)) fmt
229 229
    ((pp_vars (inputs@outputs))@(if not (self = "") then [pp_self 1;pp_self 2] else [])@(pp_vars locals))
230 230

  
......
252 252
    fprintf fmt "%a" (pp_acsl_fun_trans  None "C" name inputs outputs (Some i) false self false []) (Some [])
253 253
  in
254 254
  let pp_eexpr_expr self i j fmt ee = 
255
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (fun fmt x-> fprintf fmt "%a%i" (pp_acsl_var_read []) x j)) ee.mmstep_logic.step_inputs self i
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 256
  in
257 257
  let spec_pred cor preds fmt i =
258 258
    let j = if cor then i + 1 else i in
259
    fprintf fmt "(%a)" (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self i j)) preds
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 ()
260 262
  in
261 263
  let aux fmt base =
262 264
    let selfs = iter base self (depth-1) in
263 265
    let ios = iterList (base + 1) (inputs@outputs) in
264 266
    (if List.length selfs == 0 && List.length ios == 0 then 
265
      fprintf fmt "(%a%t%a%t%t)"
267
      fprintf fmt "(%a%t%a%t)"
266 268
     else
267
      fprintf fmt "(\\exists %a%t%a;@,%a%t%a%t%t)"
269
      fprintf fmt "(\\exists %a%t%a;@,%a%t%a%t)"
268 270
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i)) selfs
269 271
        (Utils.pp_final_char_if_non_empty ", " (iter base self (depth-1)))
270 272
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a%i" pp_acsl_var_decl x i)) ios
271 273
    )
272 274
      (Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i)) (iter base trans_pred (depth-1))
273 275
      (Utils.pp_final_char_if_non_empty "&&@," (iter base trans_pred (depth-1))) 
274
      (Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i)) (iter base (spec_pred true spec.m_requires) (depth-1))
275
      (Utils.pp_final_char_if_non_empty "&&@," (iter base (spec_pred true spec.m_requires) (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))
276 277
      (fun fmt->
277 278
        if base == 0 then
278 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)
......
285 286
(* Print the invariant lemma *)
286 287
let pp_acsl_lem_inv depth name inputs outputs self fmt spec =
287 288
  let pp_eexpr_expr self j fmt ee =
288
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [])) ee.mmstep_logic.step_inputs self j
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
289 290
  in
290 291
  fprintf fmt "\\forall %a %s1, %s2, %a;@,%a==>@,%a==>@,%a%t%a"
291 292
    pp_machine_memtype_name name self self
......
311 312
  in
312 313
  let spec_pred fmt i =
313 314
    let pp_eexpr_expr self j fmt ee = 
314
      fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (fun fmt x-> fprintf fmt "%a%i" (pp_acsl_var_read []) x i)) ee.mmstep_logic.step_inputs self j
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
315 316
    in
316
    fprintf fmt "%a%t(%a)"
317
    (Utils.fprintf_list ~sep:"==>@," ((fun fmt (w, x)-> fprintf fmt "%a"
317
    fprintf fmt "%a(%a)"
318
    (Utils.fprintf_list ~sep:"" ((fun fmt (w, x)-> fprintf fmt "%a%t"
318 319
      (Utils.fprintf_list ~sep:"==>@," (pp_eexpr_expr self (w))) spec.m_requires
320
      (Utils.pp_final_char_if_non_empty "==>@," spec.m_requires)
319 321
    ))) (iter k None (depth -1))
320
    (Utils.pp_final_char_if_non_empty "==>@," spec.m_requires)
321 322
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self (i))) spec.m_ensures
322 323
  in
323 324
  let aux fmt base =
......
342 343
(* Print the spec lemma *)
343 344
let pp_acsl_lem_spec depth name inputs outputs self fmt spec =
344 345
  let pp_eexpr_expr self j fmt ee =
345
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [])) ee.mmstep_logic.step_inputs self j
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
346 347
  in
347 348
  fprintf fmt "\\forall %a %s1, %s2, %a;@,%a==>@,%a==>@,%a%t%a"
348 349
    pp_machine_memtype_name name self self
......
556 557
            pp_acsl_fun_init (node_name node) mem2 i fmt (Some "")
557 558
        | MLocalAssign (i,v) -> 
558 559
          (match i.var_type.tdesc with Tbool -> fprintf fmt "((!%a) == (!%a))" | _ -> fprintf fmt "(%a == %a)")
559
          (pp_acsl_var_read pointer) i
560
          (pp_acsl_val mem1 (pp_acsl_var_read pointer)) v
560
          (pp_acsl_var_read "" pointer) i
561
          (pp_acsl_val mem1 (pp_acsl_var_read "" pointer)) v
561 562
        | MStateAssign (i,v) ->
562 563
          (match i.var_type.tdesc with Tbool -> fprintf fmt "((!%a) == (!%a))" | _ -> fprintf fmt "(%a == %a)")
563
          (pp_acsl_val mem2 (pp_acsl_var_read pointer)) (StateVar i)
564
          (pp_acsl_val mem1 (pp_acsl_var_read pointer)) v
564
          (pp_acsl_val mem2 (pp_acsl_var_read "" pointer)) (StateVar i)
565
          (pp_acsl_val mem1 (pp_acsl_var_read "" pointer)) v
565 566
        | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
566 567
          pp_instr fmt (MLocalAssign (i0, Fun (i, vl)))
567 568
        | MStep ([i0], i, [x;y]) when (not (Basic_library.is_internal_fun i)) && (node_name (fst (List.assoc i m.mcalls)) = "_arrow") ->
568 569
          fprintf fmt "(%a==(%s.%s._reg._first?(%a):(%a))) && (%s.%s._reg._first==0)"
569
            (pp_acsl_var_read pointer) i0
570
            (pp_acsl_var_read "" pointer) i0
570 571
            mem1 i
571
            (pp_acsl_val mem1 (pp_acsl_var_read [])) x
572
            (pp_acsl_val mem1 (pp_acsl_var_read [])) y
572
            (pp_acsl_val mem1 (pp_acsl_var_read "" [])) x
573
            (pp_acsl_val mem1 (pp_acsl_var_read "" [])) y
573 574
            mem2 i
574 575
        | MStep (il, i, vl) ->
575
          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
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
576 577
          pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i m.mcalls)))) fmt
577
          ((List.map (fun x fmt-> fprintf fmt "%a %a" pp_cast (get_val_type x) pp_val x) vl)@
578
          (List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read []) x) il)@
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)@
579 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 -> []))
580 581
        | MBranch (g,hl) -> assert false
581 582
      in
582 583
      let mods = match instr with
583 584
        | MReset i -> [fun fmt -> fprintf fmt "%s.%s" mem2 i]
584
        | MLocalAssign (i,v) -> [fun fmt -> fprintf fmt "%a" (pp_acsl_var_read pointer) i]
585
        | MStateAssign (i,v) -> [fun fmt -> fprintf fmt "%a" (pp_acsl_val mem2 (pp_acsl_var_read pointer)) (StateVar i)]
586
        | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> [fun fmt -> fprintf fmt "%a" (pp_acsl_var_read pointer) i0]
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]
587 590
        | MStep ([i0], i, [x;y]) when (not (Basic_library.is_internal_fun i)) && (node_name (fst (List.assoc i m.mcalls)) = "_arrow") ->
588
          [fun fmt-> fprintf fmt "%a, %s.%s" (pp_acsl_var_read pointer) i0 mem2 i]
589
        | MStep (il, i, vl) -> (List.map (fun x fmt-> fprintf fmt "%a" (pp_acsl_var_read []) x) il)@
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)@
590 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 -> [])
591 598
        | MBranch (g,hl) -> assert false
592 599
      in

Also available in: Unified diff