Project

General

Profile

Revision df647a81 src/c_backend.ml

View differences:

src/c_backend.ml
208 208
  let rec aux t pp_suffix =
209 209
  match (Types.repr t).Types.tdesc with
210 210
  | Types.Tclock t'       -> aux t' pp_suffix
211
  | Types.Tbool           -> fprintf fmt "int %s%a" var pp_suffix ()
212
  | Types.Treal           -> fprintf fmt "real %s%a" var pp_suffix ()
211
  | Types.Tbool           -> fprintf fmt "_Bool %s%a" var pp_suffix ()
212
  | Types.Treal           -> fprintf fmt "double %s%a" var pp_suffix ()
213 213
  | Types.Tint            -> fprintf fmt "int %s%a" var pp_suffix ()
214 214
  | Types.Tarray (d, t')  ->
215 215
    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
......
225 225

  
226 226

  
227 227
let pp_c_decl_instance_var fmt (name, (node, static)) = 
228
  fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
228
  fprintf fmt "%a %s" pp_machine_memtype_name (node_name node) name
229 229

  
230 230
let pp_c_tag fmt t =
231 231
 pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
......
256 256
      if Types.is_array_type v.var_type
257 257
      then fprintf fmt "*%a" pp_var v
258 258
      else fprintf fmt "%s->_reg.%a" self pp_var v
259
    | Fun (n, vl)   -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl
259
    | Fun (n, vl)   -> Basic_library.pp_c n Machine_code.get_val_type (pp_c_val self pp_var) fmt vl
260 260

  
261 261
let pp_c_checks self outputs fmt checks =
262 262
  Utils.fprintf_list ~sep:"" 
......
326 326
 | _           :: q, Power (v, n) ->
327 327
   pp_value_suffix self loop_vars pp_value fmt v
328 328
 | _               , Fun (n, vl)  ->
329
   Basic_library.pp_c n (pp_value_suffix self loop_vars pp_value) fmt vl
329
   Basic_library.pp_c n Machine_code.get_val_type (pp_value_suffix self loop_vars pp_value) fmt vl
330 330
 | _               , _            ->
331 331
   let pp_var_suffix fmt v = fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in
332 332
   pp_c_val self pp_var_suffix fmt value
......
344 344
  let reordered_loop_vars = reorder_loop_variables loop_vars in
345 345
  let rec aux fmt vars =
346 346
    match vars with
347
    | [] ->
348
      fprintf fmt "%a = %a;" 
349
	(pp_value_suffix self loop_vars pp_var) var_name
350
	(pp_value_suffix self loop_vars pp_var) value
347
    | [] -> fprintf fmt "%a = %a;" (pp_value_suffix self loop_vars pp_var) var_name
348
      (pp_value_suffix self loop_vars pp_var) value
351 349
    | (d, LVar i) :: q ->
352 350
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
353 351
      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
......
388 386
 try (* stateful node instance *)
389 387
   let (n,_) = List.assoc i instances in
390 388
  (* Format.eprintf "pp_instance_call: %s , outputs are %a@.@?" (node_name n) (Utils.fprintf_list ~sep:", " Printers.pp_var) outputs; *)
391
 fprintf fmt "%s_step (%a%t%a%t%s->%s);"
389
 fprintf fmt "%s_step (%a%t%a%t&(%s->%s));"
392 390
     (node_name n)
393 391
     (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read machine_outputs))) inputs
394 392
     (Utils.pp_final_char_if_non_empty ", " inputs) 
......
419 417
 )
420 418
let pp_machine_reset instances self fmt inst =
421 419
  let (node, static) = List.assoc inst instances in
422
  fprintf fmt "%a(%a%t%s->%s);"
420
  fprintf fmt "%a(%a%t&(%s->%s));"
423 421
    pp_machine_reset_name (node_name node)
424 422
    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
425 423
    (Utils.pp_final_char_if_non_empty ", " static)
......
468 466

  
469 467
(**************************************************************************)
470 468
(*     Printing spec for c *)
471

  
472 469
(**************************************************************************)
473 470

  
474 471
let pp_ident is_output fmt id =
......
555 552
    | Array _      
556 553
    | Access _       -> assert false (* no arrays *)
557 554
    | Power (v, n)  -> assert false
558
    | LocalVar v    -> pp_var fmt v
555
    | LocalVar v    -> pp_var "" fmt v
559 556
    | StateVar v    ->     
560 557
      if Types.is_array_type v.var_type
561 558
      then assert false
562
      else fprintf fmt "%s->_reg.%a" self pp_var v
559
      else fprintf fmt "%a" (pp_var (self^"._reg.")) v
563 560
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_acsl n Machine_code.get_val_type (pp_acsl_val self pp_var)) vl
564 561

  
562
(* Access to the value of a variable:
563
   - if it's not a scalar output, then its name is enough
564
   - otherwise, dereference it (it has been declared as a pointer,
565
     despite its scalar Lustre type)
566
   - moreover, cast arrays variables into their original array type.
567
*)
568
let pp_acsl_var_read outputs pre fmt id =
569
  if Types.is_array_type id.var_type
570
  then
571
    assert false (* no array *)
572
  else ( (* Hack to cast boolean variables as int for ACSL predicates *)
573
    (* This hack doesn't work because of int equality != bool equality and _Bool
574
        is supported now*)
575
    (*if (Types.repr id.var_type).Types.tdesc = Types.Tbool then
576
      fprintf fmt "(int)" 
577
    ;*)
578
    if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
579
    then fprintf fmt "%s*%s" pre id.var_id
580
    else fprintf fmt "%s%s" pre id.var_id
581
  )
565 582

  
566 583
let rec pp_eexpr_logic_instr 
567 584
    ((node_id, inputs, outputs, locals, memory) as m) self fmt instr =
......
570 587
  | MLocalAssign (i,v) -> (
571 588
    match outputs with 
572 589
    | [o] -> if i = o then
573
	fprintf fmt "%a;" (pp_acsl_val self (pp_c_var_read outputs)) v
590
	fprintf fmt "%a;" (pp_acsl_val self (pp_acsl_var_read outputs)) v
574 591
      else
575 592
	fprintf fmt "\\let %a = %a;" 
576 593
	  (pp_c_var_read outputs (* TODO no variable shold be treated as output *)) i
577
	  (pp_acsl_val self (pp_c_var_read outputs)) v
594
	  (pp_acsl_val self (pp_acsl_var_read outputs)) v
578 595

  
579 596
    | _ -> assert false (* should not happen: only a single output *)
580 597
)
......
601 618
  let self = mk_self m in
602 619
  let pp_expr_def fmt ee =
603 620
    match ee.mmstep_logic.step_instrs with
604
    | [MStep([o], i, vl)] -> () (* We do nothing, the expression is simple and 
605
				   was introduced directly in the contract *)
621
    (*| [MStep([o], i, vl)] -> () (* We do nothing, the expression is simple and 
622
				   was introduced directly in the contract *) *)
606 623
    | _ -> ((* We define a new ACSL predicate *)
607
      fprintf fmt "/*@@ @[<v 3>predicate spec_%i(%a%t%a *%s) =@;%a@]@;*/@." 
624
      fprintf fmt "/*@@ @[<v 3>predicate spec_%i(%a%t%a %s) =@;%a@]@;*/@." 
608 625
	ee.muid   
609 626
	(Utils.fprintf_list ~sep:", " pp_acsl_var_decl) ee.mmstep_logic.step_inputs
610 627
	(Utils.pp_final_char_if_non_empty ", " ee.mmstep_logic.step_inputs)
......
622 639
	  [] spec.m_behaviors)
623 640
    )
624 641

  
625
(* Access to the value of a variable:
626
   - if it's not a scalar output, then its name is enough
627
   - otherwise, dereference it (it has been declared as a pointer,
628
     despite its scalar Lustre type)
629
   - moreover, cast arrays variables into their original array type.
630
*)
631
let pp_acsl_var_read outputs fmt id =
632
  if Types.is_array_type id.var_type
633
  then
634
    assert false (* no array *)
635
  else ( (* Hack to cast boolean variables as int for ACSL predicates *)
636
    if (Types.repr id.var_type).Types.tdesc = Types.Tbool then
637
      fprintf fmt "(int)" 
638
    ;
639
    if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
640
    then fprintf fmt "*%s" id.var_id
641
    else fprintf fmt "%s" id.var_id
642
  )
643

  
644
    
645 642
let pp_requires_mem machines fmt m =
646 643
  let self = mk_self m in
647 644
  List.iter (fun v -> fprintf fmt "requires \\valid(%s);@;" v.var_id) m.mstep.step_outputs;
648 645
  fprintf fmt "requires \\valid(%s);@;" self;
649 646
  let mems = Machine_code.get_mems m machines in
650
  List.iter (fun prefix -> fprintf fmt "requires \\valid(%s%a);@;" self
647
  (*List.iter (fun prefix -> fprintf fmt "requires \\valid(%s%a);@;" self
651 648
    (Utils.fprintf_list ~sep:"" (fun fmt s -> fprintf fmt "->%s" s)) prefix
652 649
  )
653
    (Machine_code.get_instances m machines);
650
    (Machine_code.get_instances m machines);*)
654 651
  if List.length mems + List.length m.mstep.step_outputs > 1 then
655
    fprintf fmt "requires \\separated(@[<hov>%a%t%a@]);@;" 
652
    fprintf fmt "requires \\separated(@[<hov>%a%t%s@]);@;" 
656 653
      (Utils.fprintf_list ~sep:",@ " 
657 654
	 (fun fmt v -> pp_print_string fmt v.var_id))
658 655
      m.mstep.step_outputs 
659
      (Utils.pp_final_char_if_non_empty ",@ " mems)
660
      (Utils.fprintf_list ~sep:",@ " 
656
      (Utils.pp_final_char_if_non_empty ",@ " m.mstep.step_outputs)
657
      self
658

  
659
      (*(Utils.fprintf_list ~sep:",@ " 
661 660
	 (fun fmt (prefix, var) -> fprintf fmt "&%s%a->_reg.%s"
662 661
	   self 
663 662
	   (Utils.fprintf_list ~sep:"" (fun fmt s -> fprintf fmt "->%s" s)) prefix
664 663
	   var.var_id	 
665 664
	 ))
666
      mems
665
      mems*)
667 666

  
668 667
let pp_assigns machines fmt m =
669 668
  let self = mk_self m in
670 669
  let mems = Machine_code.get_mems m machines in
671
  fprintf fmt "assigns @[<hov>%a%t%a@];@;" 
670
  fprintf fmt "assigns @[<hov>%a%t*%s@];@;" 
672 671
    (Utils.fprintf_list ~sep:",@ " 
673 672
       (fun fmt v -> fprintf fmt "*%s" v.var_id))
674 673
    m.mstep.step_outputs 
675
    (Utils.pp_final_char_if_non_empty ",@ " mems)
674
    (Utils.pp_final_char_if_non_empty ",@ " m.mstep.step_outputs)
675
    self
676
(*
676 677
    (Utils.fprintf_list ~sep:",@ " 
677 678
       (fun fmt (prefix, var) -> fprintf fmt "%s%a->_reg.%s"
678 679
	 self 
......
680 681
	    (fun fmt s -> fprintf fmt "->%s" s)) prefix
681 682
	 var.var_id	 
682 683
       ))
683
    mems
684
    mems*)
685

  
686
(*TODO: BEGIN*)
687

  
688
(* concat two lists and remove duplicates *)
689
let rec concat_uniq l1 l2 =
690
  match l1 with
691
    | [] -> l2
692
    | t::q -> let l = concat_uniq q l2 in
693
      if List.mem t l2 then l else t::l
694

  
695
(* A type for dependance, it can be a node or a variable *)
696
type dep_t = Dep_Var of string | Dep_Node of string
697

  
698
(* Take a machine and output the list of all dependance *)
699
let gen_dep instrs =
700
  let rec gen_dep_val = function
701
    | Cst c         -> []
702
    | Array vl      -> assert false
703
    | Access (t, i) -> assert false
704
    | Power (v, n)  -> assert false
705
    | LocalVar v    -> []
706
    | StateVar v    -> [Dep_Var v.var_id]
707
    | Fun (n, vl)   -> List.fold_left (fun l x-> concat_uniq (gen_dep_val x) l) [] vl
708
  and gen_dep_instr = function
709
    | MReset i -> assert false
710
    | MLocalAssign (i,v) -> gen_dep_val v
711
    | MStateAssign (i,v) -> concat_uniq (gen_dep_val (StateVar i)) (gen_dep_val v)
712
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> gen_dep_instr (MLocalAssign (i0, Fun (i, vl)))
713
    | MStep (il, i, vl) -> List.fold_left (fun l x-> concat_uniq (gen_dep_val x) l) [Dep_Node i] vl
714
    | MBranch (g,hl) -> List.fold_left (fun l (x, y)-> concat_uniq (gen_dep_instrs y) l) (gen_dep_val g) hl
715
  and gen_dep_instrs instrs =
716
    List.fold_left (fun l x-> concat_uniq (gen_dep_instr x) l) [] instrs
717
  in
718
  gen_dep_instrs instrs
719

  
720
(* Print a function call/declaration in acsl *) 
721
let pp_acsl_fun name fmt args =
722
    fprintf fmt "%s(@[<v>%a@])"
723
      name
724
      (Utils.fprintf_list ~sep:",@ " (fun fmt f-> f fmt)) args
725

  
726
(* Print an invariant call/decl in acsl *)
727
let pp_acsl_fun_init name self inst fmt mem =
728
  let arg = fun fmt-> (match inst, mem with
729
    | x,  None    -> fprintf fmt "%a %s" pp_machine_memtype_name name self
730
    | "", Some "" -> fprintf fmt "%s" self
731
    | "", Some m  -> fprintf fmt "\\at(*%s, %s)" self m
732
    | x,  Some "" -> fprintf fmt "%s.%s" self inst
733
    | x,  Some m  -> fprintf fmt "\\at(%s->%s, %s)" self inst m)
734
  in
735
  pp_acsl_fun ("init_"^name) fmt [arg]
684 736

  
685 737

  
738
(* Print a machine instruction in acsl for transition lemma *) 
739
let preprocess_acsl_instr instances outputs instr =
740
  match instr with 
741
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i && (not (List.mem i0 outputs)) ->
742
      Some (i0, Fun (i, vl))
743
    | MStep ([i0], i, vl) when (not (Basic_library.is_internal_fun i)) && node_name (fst (List.assoc i instances)) = "_arrow" ->
744
      assert (List.length vl == 2);
745
      Some (i0, Fun ("arrow_"^i, vl))
746
    | MLocalAssign (i,v) when not (List.mem i outputs) ->
747
      Some (i, v)
748
    | _ -> None
749

  
750

  
751
let pp_cast fmt = function
752
  | Types.Tbool           -> fprintf fmt "(_Bool)"
753
  | Types.Treal           -> fprintf fmt "(double)"
754
  | Types.Tint            -> fprintf fmt "(int)"
755
  | _ -> assert false
756

  
757
let getFunType i args =
758
  match i, args with
759
  | "ite", [v1; v2; v3] -> v2
760
  | "uminus", [v] -> v
761
  | "not", [v] -> v
762
  | "impl", [v1; v2] -> v1
763
  | "=", [v1; v2] -> Types.Tbool
764
  | "mod", [v1; v2] -> v1
765
  | "xor", [v1; v2] -> v1
766
  | _, [v1; v2] -> v1
767
  | _ -> assert false
768

  
769
let rec get_val_type v =
770
match v with 
771
| Cst _
772
| LocalVar _ 
773
| StateVar _-> Machine_code.get_val_type v
774
| Fun (n, vl) -> getFunType n (List.map get_val_type vl)
775
| Array _
776
| Access _
777
| Power _ -> assert false
778

  
779
let get_var_type t = (Types.repr t.var_type).Types.tdesc
780

  
781
(* Print a machine instruction in acsl for transition lemma *) 
782
let rec pp_acsl_instr vars instances self pointer fmt instr =
783
  match instr with 
784
    | MReset i ->
785
      let (node, static) = List.assoc i instances in
786
      assert (List.length static == 0);
787
      if node_name node = "_arrow" then
788
        fprintf fmt "%s.%s._reg._first==1" self i
789
      else
790
        pp_acsl_fun_init (node_name node) self i fmt (Some "")
791
    | MLocalAssign (i,v) -> fprintf fmt "%a == %a"
792
      (pp_acsl_var_read pointer "") i
793
      (pp_acsl_val (self^"1") (pp_acsl_var_read pointer)) v
794
    | MStateAssign (i,v) -> fprintf fmt "%a == %a"
795
      (pp_acsl_val (self^"2") (pp_acsl_var_read pointer)) (StateVar i)
796
      (pp_acsl_val (self^"1") (pp_acsl_var_read pointer)) v
797
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
798
      pp_acsl_instr vars instances self pointer fmt (MLocalAssign (i0, Fun (i, vl)))
799
    | MStep (il, i, vl) ->
800
      let pp_val fmt x = (match get_val_type x with Types.Tbool -> fprintf fmt "((%a)?1:0)" | _ -> fprintf fmt "%a") (pp_acsl_val (self^"1") (pp_acsl_var_read [])) x in
801
      pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i instances)))) fmt
802
      ((List.map (fun x fmt-> fprintf fmt "%a %a" pp_cast (get_val_type x) pp_val x) vl)@
803
      (List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read [] "") x) il)@
804
        [(fun fmt->fprintf fmt "%s1.%s" self i);(fun fmt->fprintf fmt "%s2.%s" self i)])
805
    | MBranch (g,hl) ->
806
      let t = fst (List.hd hl) in
807
      if hl <> [] && (t = tag_true || t = tag_false) then
808
        let tl = try List.assoc tag_true  hl with Not_found -> [] in
809
        let el = try List.assoc tag_false hl with Not_found -> [] in
810
        fprintf fmt "(%a)?(%a):(%a)"
811
          (pp_acsl_val self (pp_acsl_var_read pointer)) g
812
          (Utils.fprintf_list ~sep:"&& " (pp_acsl_instr vars instances self pointer)) tl
813
          (Utils.fprintf_list ~sep:"&& " (pp_acsl_instr vars instances self pointer)) el
814
      else assert false
815

  
816
(* Print all machine instructions in acsl for transition lemma *) 
817
let pp_acsl_instrs outputs self pointer instances vars fmt instrs =
818
  if List.length instrs == 0 then fprintf fmt "\\true" else
819
  let handle (locals, instrs) i =
820
    match preprocess_acsl_instr instances outputs i with
821
      | None    -> (locals, i::instrs)
822
      | Some l  -> (l::locals, instrs)
823
  in
824
  let pp_let fmt (i, v) =
825
    match v with
826
      | Fun (s, [x;y]) when String.length s >= 6 && String.sub s 0 6 = "arrow_" ->
827
        let var = String.sub s 6 (String.length s - 6) in
828
        fprintf fmt "\\let %a = %s1.%s._reg._first?%a:%a; (%s2.%s._reg._first==0) &&"
829
          (pp_acsl_var_read pointer "") i
830
          self var
831
          (pp_acsl_val (self^"1") (pp_acsl_var_read [])) x
832
          (pp_acsl_val (self^"1") (pp_acsl_var_read [])) y
833
          self var
834
      | _ ->
835
        fprintf fmt "\\let %a = %a;"
836
          (pp_acsl_var_read pointer "") i
837
          (pp_acsl_val (self^"1") (pp_acsl_var_read pointer)) v
838
  in
839
  let (locals, instrs) = List.fold_left handle ([], []) instrs in
840
  fprintf fmt "%a@,%a"
841
    (Utils.fprintf_list ~sep:"@," pp_let)
842
    (List.rev locals)
843
    (Utils.fprintf_list ~sep:" &&@," (pp_acsl_instr vars instances self pointer))
844
    instrs
845

  
846
(* Take a dependance and print it for invariant predicate *)
847
(*
848
let pp_acsl_dep self instances fmt = function
849
  | Dep_Var s -> fprintf fmt "%s2._reg.%s == %s1._reg.%s" self s self s
850
  | Dep_Node s ->
851
    pp_acsl_fun ("inv_"^(node_name (fst (List.assoc s instances)))) fmt [fun fmt->fprintf fmt "%s1.%s" self i];
852
    fprintf fmt "&&@, %t == %t" (pp_acsl_at self s)
853
      (pp_acsl_at self s)
854
*)
855

  
856
(* Print a transition call/decl in acsl *)
857
let pp_acsl_fun_trans infos pre name inputs outputs suffix flag_output self flag_mem locals fmt existential =
858
  let (locals, existential) = (*([], match existential with None -> None | Some x -> Some []) in*)
859
  match infos with
860
    | None -> (locals, existential)
861
    | Some (instrs, instances) ->
862
      let nonlocals = List.fold_left (fun l x-> match preprocess_acsl_instr instances outputs x with | Some (i, _) -> i::l | None -> l) [] instrs in
863
      (
864
        List.filter (fun x-> not (List.mem x nonlocals)) locals,
865
        match existential with None -> None | Some existential -> Some (List.filter (fun x-> not (List.mem x nonlocals)) existential)
866
      )
867
  in
868
  let mems = function 1 -> "Pre" | 2 -> "Here" | _ -> assert false in
869
  let pp_self_read =
870
    if flag_mem then fun i fmt-> fprintf fmt "\\at(*%s, %s)" self (mems i)
871
    else fun i fmt-> fprintf fmt "%s%i" self (match suffix with None -> i | Some s -> s+i-1)
872
  in
873
  let (pp_var, pp_self) =
874
    match existential with
875
      | None    -> (pp_acsl_var_decl, (fun i fmt-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i))
876
      | Some ex -> (if List.length ex != 0 then fprintf fmt "\\exists %a;@," (Utils.fprintf_list ~sep:";@,\\exists " pp_acsl_var_decl) ex);
877
                   (pp_acsl_var_read (if flag_output then outputs else []) "", pp_self_read)
878
  in
879
  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
880
    (pp_acsl_fun (pre^"trans_"^name)) fmt
881
    ((pp_vars (inputs@outputs))@[pp_self 1;pp_self 2]@(pp_vars locals))
882

  
883
let depth = 1
884

  
885
(* Print an invariant call/decl in acsl *)
886
let pp_acsl_fun_inv name self fmt mem =
887
  let arg = fun fmt-> (match mem with
888
    | None -> fprintf fmt "%a %s%i" pp_machine_memtype_name name self depth
889
    | Some "" -> fprintf fmt "%s" self
890
    | Some "Here" -> fprintf fmt "*%s" self
891
    | Some m -> fprintf fmt "\\at(*%s, %s)" self m)
892
  in
893
  pp_acsl_fun ("inv_"^name) fmt [arg]
894

  
895
(* Print an invariant call/decl in acsl *)
896
let pp_acsl_inv name inputs outputs self fmt spec =
897
  let rec iter base x = function
898
    | i when i = base-1 -> []
899
    | i -> (i, x)::(iter base x (i-1))
900
  in
901
  let rec iterList base = function
902
    | []   -> []
903
    | t::q -> (iter base t depth)@(iterList base q)
904
  in
905
  let trans_pred fmt i =
906
    fprintf fmt "%a" (pp_acsl_fun_trans  None "C" name inputs outputs (Some i) false self false []) (Some [])
907
  in
908
  let spec_pred fmt i =
909
    let pp_eexpr_expr self j fmt ee = 
910
      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
911
    in
912
    fprintf fmt "%a%t%a"
913
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self (i))) spec.m_requires
914
    (Utils.pp_final_char_if_non_empty "&&@," spec.m_requires)
915
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self (i))) spec.m_ensures
916
  in
917
  let aux fmt base =
918
    let selfs = iter base self (depth-1) in
919
    let ios = iterList (if base == 0 then 0 else base + 1) (inputs@outputs) in
920
    (if List.length selfs == 0 && List.length ios == 0 then 
921
      fprintf fmt "(%a%t%t)"
922
     else
923
      fprintf fmt "(\\exists %a%t%a;@,%a%t%t)"
924
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i)) selfs
925
        (Utils.pp_final_char_if_non_empty ", " (iter base self (depth-1)))
926
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a%i" pp_acsl_var_decl x i)) ios
927
    )
928
      (Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i)) (iter base trans_pred (depth-1))
929
      (Utils.pp_final_char_if_non_empty "&&@," (iter base trans_pred (depth-1))) 
930
      (fun fmt->
931
        if base == 0 then
932
          Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i) fmt (iter base spec_pred depth)
933
        else
934
          pp_acsl_fun_init name (self^(string_of_int base)) "" fmt (Some "")
935
      )
936
  in
937
  Utils.fprintf_list ~sep:"||@," (fun fmt (i, f)-> fprintf fmt "%a" f i) fmt (iter 0 aux depth)
938

  
939
(* Print an invariant call/decl in acsl *)
940
let pp_acsl_lem_inv name inputs outputs fmt self =
941
  fprintf fmt "\\forall %a %s1, %s2, %a;@,%a==>@,%a==>@,%a"
942
    pp_machine_memtype_name name self self
943
    (Utils.fprintf_list ~sep:", " pp_acsl_var_decl) (inputs@outputs)
944
    (pp_acsl_fun_inv name (self^"1")) (Some "")
945
    (pp_acsl_fun_trans None "C" name inputs outputs None false self false []) (Some [])
946
    (pp_acsl_fun_inv name (self^"2")) (Some "")
947

  
948
(* Print an invariant call/decl in acsl *)
949
let pp_acsl_lem_spec name inputs outputs self fmt spec =
950
  let pp_eexpr_expr self j fmt ee =
951
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) ee.mmstep_logic.step_inputs self j
952
  in
953
  fprintf fmt "\\forall %a %s1, %s2, %a;@,%a==>@,%a==>@,%a%t%a"
954
    pp_machine_memtype_name name self self
955
    (Utils.fprintf_list ~sep:", " pp_acsl_var_decl) (inputs@outputs)
956
    (pp_acsl_fun_inv name (self^"1")) (Some "")
957
    (pp_acsl_fun_trans None "C" name inputs outputs None false self false []) (Some [])
958
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self 1)) spec.m_requires
959
    (Utils.pp_final_char_if_non_empty "&&@," spec.m_requires)
960
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self 2)) spec.m_ensures
961

  
962
(* Print the definition of the transition in acsl *)
963
let pp_acsl_def_trans fmt m =
964
  let name = m.mname.node_id in
965
  let inputs = m.mstep.step_inputs in
966
  let outputs = m.mstep.step_outputs in
967
  let locals = m.mstep.step_locals in
968
  let memory = m.mmemory in
969
  let vars = inputs@outputs@locals@memory in
970
  if m.mname.node_id <> arrow_id then (
971
    let self = mk_self m in
972
    fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
973
      (pp_acsl_fun_trans (Some (m.mstep.step_instrs, m.minstances)) "" name inputs outputs None false self false locals) None
974
	    (pp_acsl_instrs outputs self [] m.minstances vars) m.mstep.step_instrs;
975
    fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
976
      (pp_acsl_fun_init name self "") None
977
	    (pp_acsl_instrs [] self [] m.minstances vars) m.minit;
978
    fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
979
      (pp_acsl_fun_trans None "C" name inputs outputs None false self false []) None
980
	    (pp_acsl_fun_trans (Some (m.mstep.step_instrs, m.minstances)) "" name inputs outputs None false self false locals) (Some locals);
981
    match m.mspec with None -> () | Some spec -> fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
982
      (pp_acsl_fun_inv name self) None (pp_acsl_inv name inputs outputs self) spec;
983
    fprintf fmt "/*@@ @[<v 3>lemma inv_spec_%s : @;%a;@]@;*/@." name (pp_acsl_lem_spec name inputs outputs self) spec;
984
    fprintf fmt "/*@@ @[<v 3>lemma inv_inv_%s : @;%a;@]@;*/@." name (pp_acsl_lem_inv name inputs outputs) self
985
  )
986

  
987
(*;
988
  fprintf fmt "/*@@ @[<v 3>predicate inv_%s{L1, L2}(@[<v>@[%a *%s@]@]) =@;%a;@]@;*/@."
989
    m.mname.node_id
990
	  pp_machine_memtype_name m.mname.node_id
991
	  self
992
    (Utils.fprintf_list ~sep:" &&@," (printDep self "L1" "L2" m.minstances)) (gen_dep m.mstep.step_instrs);
993
  fprintf fmt "/*@@ @[<v 3>lemma transitivity_%s{L1, L2, L3, L4} :@, \forall @[<v>@[%a%t@]@,@[%a@]%t@[%a *%s@]@];@, %t;@]@;*/@."
994
    m.mname.node_id
995
    (Utils.fprintf_list ~sep:",@ " pp_acsl_var_decl) m.mstep.step_inputs
996
    (Utils.pp_final_char_if_non_empty ",@ " m.mstep.step_inputs) 
997
    (Utils.fprintf_list ~sep:",@ " pp_acsl_var_decl) m.mstep.step_outputs
998
    (Utils.pp_final_char_if_non_empty ",@," m.mstep.step_outputs)
999
	pp_machine_memtype_name m.mname.node_id
1000
	self
1001
  (fun fmt->
1002
    fprintf fmt "inv_%s{L1, L2}(%s) ==>@," m.mname.node_id self;
1003
    fprintf fmt "inv_%s{L3, L4}(%s) ==>@," m.mname.node_id self;
1004
    fprintf fmt "trans_%s{L2, L3}(%a%t%a%t\\at(%s, L2)) ==>@,"
1005
      m.mname.node_id
1006
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) m.mstep.step_inputs
1007
      (Utils.pp_final_char_if_non_empty ", " m.mstep.step_inputs) 
1008
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) m.mstep.step_outputs
1009
      (Utils.pp_final_char_if_non_empty ", " m.mstep.step_outputs)
1010
      self;
1011
    fprintf fmt "trans_%s{L1, L4}(%a%t%a%t\\at(%s, L1)@]@])"
1012
      m.mname.node_id
1013
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) m.mstep.step_inputs
1014
      (Utils.pp_final_char_if_non_empty ", " m.mstep.step_inputs) 
1015
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) m.mstep.step_outputs
1016
      (Utils.pp_final_char_if_non_empty ", " m.mstep.step_outputs)
1017
      self)
1018
*)
1019

  
1020
(*
1021
    (print_reset_prototype self) (m.mname.node_id, m.mstatic)
1022
    (Utils.fprintf_list ~sep:"@," 
1023
       (pp_machine_instr 
1024
	  (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, m.mstep.step_locals, m.mmemory, m.minstances, m.mcalls) self)) 
1025
    m.minit
1026
    (Utils.pp_newline_if_non_empty m.minit)
1027
    (* Print specification if any: insert side effect at the end of the function body  *)
1028
    (fun fmt -> match m.mspec with
1029
    | None -> ()
1030
    | Some spec -> pp_acsl_spec_init_side_effects m m.mstep.step_outputs fmt spec
1031
    )*)
1032

  
1033
(*TODO: END*)
1034

  
686 1035
let pp_acsl_mem_valid machines fmt m =
1036
  let self = mk_self m in
687 1037
  fprintf fmt "@[<v 2>/*@@ ";
688 1038
  pp_requires_mem machines fmt m;
1039
	fprintf fmt "ensures %a;@," (pp_acsl_fun_trans None "C" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true self true []) (Some []);
689 1040
  pp_assigns machines fmt m;
690 1041
  fprintf fmt "@]*/@.";
691 1042
  ()
......
697 1048
      (* If the eexpr contains a single definition we use it directly. Otherwise,
698 1049
	 we rely on an external predicate *)
699 1050
    match ee.mmstep_logic.step_instrs with
700
    | [MStep([o], i, vl)] -> 
1051
    (*| [MStep([o], i, vl)] -> 
701 1052
      fprintf fmt "%a %t"
702 1053
	(Utils.fprintf_list ~sep:" " pp_quantifiers) ee.mquantifiers
703 1054
	(fun fmt ->
......
706 1057
	    ee.mmstep_logic.step_inputs@ee.mmstep_logic.step_outputs@ee.mmstep_logic.step_locals@ee.mmmemory 
707 1058
	  in 
708 1059
	  pp_expr_rhs vars self (pp_c_var_read outputs) fmt o.var_type value 
709
	)
710
    | _ -> fprintf fmt "spec_%i(%a, %s);" 
1060
	)*)
1061
    | _ -> fprintf fmt "spec_%i(%a, *%s);" 
711 1062
      ee.muid   
712
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read outputs)) ee.mmstep_logic.step_inputs
1063
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read outputs "")) ee.mmstep_logic.step_inputs
713 1064
      self
714 1065
  in
715 1066
  fprintf fmt "@[<v 2>/*@@ ";
716 1067
  (* Valid pointers *)
717 1068
  pp_requires_mem machines fmt m;
718
  
719 1069
  (* Spec requires *)
720 1070
  Utils.fprintf_list ~sep:"" 
721 1071
    (fun fmt r -> fprintf fmt "requires %a@ " pp_eexpr_expr r) 
722 1072
    fmt 
723 1073
    spec.m_requires;
1074
  fprintf fmt "requires %a;@," (pp_acsl_fun_inv m.mname.node_id self) (Some "Here");
724 1075
  Utils.fprintf_list ~sep:"" 
725 1076
    (fun fmt r -> fprintf fmt "ensures %a@ " pp_eexpr_expr r) 
726 1077
    fmt 
727 1078
    spec.m_ensures;
1079
  fprintf fmt "ensures %a;@," (pp_acsl_fun_inv m.mname.node_id self) (Some "Here");
1080
	fprintf fmt "ensures %a;@," (pp_acsl_fun_trans None "C" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true self true []) (Some []);
728 1081
  fprintf fmt "@ ";
729 1082
    (* TODO assigns + separated *)
730 1083
    (* fprintf fmt "assigns *self%t%a;@ "  *)
......
997 1350
    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
998 1351
    pp_machine_static_link_name m.mname.node_id
999 1352

  
1000
let print_machine_decl machines fmt m =
1353
let print_machine_spec machines fmt m =
1001 1354
  if m.mname.node_id <> arrow_id then 
1002 1355
    (
1003 1356
      (* We don't print arrow function *)
1004
      
1357

  
1005 1358
      (* Print specification if any: insert logic definition before the function  *)
1006
      (match m.mspec with
1359
      match m.mspec with
1007 1360
      | None -> ()
1008 1361
      | Some spec -> 
1009 1362
	pp_acsl_spec_logics m m.mstep.step_outputs fmt spec
1010
      );
1011
      
1363
    )
1364

  
1365
let print_machine_decl machines fmt m =
1366
  if m.mname.node_id <> arrow_id then 
1367
    (
1368
   (*   (* We don't print arrow function *)
1369

  
1012 1370
      (* Static allocation *)
1013 1371
      if !Options.static_mem
1014 1372
      then (
......
1021 1379
      (* Dynamic allocation *)
1022 1380
	fprintf fmt "extern %a;@.@."
1023 1381
	  print_alloc_prototype (m.mname.node_id, m.mstatic)
1024
      );
1382
      );*)
1025 1383
      let self = mk_self m in
1384
	    fprintf fmt "/*@@ensures %a;@." (pp_acsl_fun_init m.mname.node_id self "") (Some "Here");
1385
	    fprintf fmt "assigns *%s;*/@." self;
1026 1386
      fprintf fmt "extern %a;@.@."
1027 1387
	(print_reset_prototype self) (m.mname.node_id, m.mstatic);
1028 1388
    (* Print specification contracts if any *)
1029 1389
      (match m.mspec with
1030 1390
      | None -> pp_acsl_mem_valid machines fmt m
1031
      | Some spec -> 
1032
	pp_acsl_spec_contracts machines m m.mstep.step_outputs fmt spec
1391
      | Some spec -> pp_acsl_spec_contracts machines m m.mstep.step_outputs fmt spec
1033 1392
      );
1034 1393
      fprintf fmt "extern %a;@.@."
1035 1394
	(print_step_prototype self)
......
1064 1423
    (pp_c_type "") base_type
1065 1424
    vdecl.var_id
1066 1425

  
1426
let rec list_to_partial l = match l with
1427
  | []   -> [[]]
1428
  | _::q -> l::(list_to_partial q)
1429

  
1067 1430
let print_alloc_code fmt m =
1068 1431
  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
1069 1432
  fprintf fmt "%a *_alloc;@,_alloc = (%a *) malloc(sizeof(%a));@,assert(_alloc);@,%a%areturn _alloc;"
......
1079 1442
  then
1080 1443
    (* C99 code *)
1081 1444
    let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
1082
    fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%t%t@]@,}@.@."
1445
    fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%t%a%t%t%t@]@,}@.@."
1083 1446
      (print_step_prototype self) (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
1084 1447
      (* locals *)
1085 1448
      (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals
......
1097 1460
      | None -> ()
1098 1461
      | Some spec -> pp_acsl_spec_side_effects m m.mstep.step_outputs fmt spec
1099 1462
      )
1463
      (let f = fun fmt x-> fprintf fmt "/*@@assert (%a);*/@," (pp_acsl_fun_trans (Some (m.mstep.step_instrs, m.minstances)) "" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true self true m.mstep.step_locals) (Some x) in
1464
      (Utils.fprintf_list ~sep:"@," f)) (List.rev (list_to_partial m.mstep.step_locals))
1465
      (fun fmt-> fprintf fmt "/*@@assert (%a);*/@," (pp_acsl_fun_trans None "C" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true self true []) (Some []))
1466
      (let pp_eexpr_expr fmt ee = 
1467
        fprintf fmt "spec_%i(%a, *%s)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read m.mstep.step_outputs "")) ee.mmstep_logic.step_inputs self
1468
       in
1469
       fun fmt -> match m.mspec with
1470
        | Some spec when 0 < List.length spec.m_ensures-> fprintf fmt "/*@@assert (%a);*/@," (Utils.fprintf_list ~sep:"&&@," pp_eexpr_expr) spec.m_ensures
1471
        | None ->fprintf fmt ""
1472
      )
1100 1473
      (fun fmt -> fprintf fmt "return;")
1101 1474
  else
1102 1475
    (* C90 code *)
......
1193 1566
    ) m.mstep.step_outputs;
1194 1567
  fprintf fmt "@ /* Main memory allocation */@ ";
1195 1568
  if (!Options.static_mem && !Options.main_node <> "")
1196
  then (fprintf fmt "%a(static,main_mem);@ " pp_machine_static_alloc_name mname)
1569
  then (*(fprintf fmt "%a(static,main_mem);@ " pp_machine_static_alloc_name mname)*) (fprintf fmt "%a main_mem;@ " pp_machine_memtype_name mname)
1197 1570
  else (fprintf fmt "%a *main_mem = %a();@ " pp_machine_memtype_name mname pp_machine_alloc_name mname);
1198 1571
  fprintf fmt "@ /* Initialize the main memory */@ ";
1199 1572
  fprintf fmt "%a(%s);@ " pp_machine_reset_name mname main_mem;
1200 1573
  fprintf fmt "@ ISATTY = isatty(0);@ ";
1201 1574
  fprintf fmt "@ /* Infinite loop */@ ";
1575
  (match m.mspec with
1576
      | None -> ()
1577
      | Some spec -> fprintf fmt "/*@@ loop invariant %a;*/@," (pp_acsl_fun_inv m.mname.node_id "main_mem") (Some "")
1578
  );
1202 1579
  fprintf fmt "@[<v 2>while(1){@ ";
1203
  fprintf fmt  "fflush(stdout);@ ";
1580
  (*fprintf fmt  "fflush(stdout);@ ";*)
1204 1581
  List.iter 
1205 1582
    (fun v -> fprintf fmt "%s = %a;@ "
1206 1583
      v.var_id
......
1373 1750
  fprintf header_fmt "/* Global constant (declarations, definitions are in C file) */@.";
1374 1751
  List.iter (fun c -> print_const_decl header_fmt c) (get_consts prog);
1375 1752
  pp_print_newline header_fmt ();
1753

  
1376 1754
  (* Print the struct declarations of all machines. *)
1377 1755
  fprintf header_fmt "/* Struct declarations */@.";
1378
  List.iter (print_machine_struct header_fmt) machines;
1756
  List.iter (print_machine_struct header_fmt) (List.rev machines);
1757
  pp_print_newline header_fmt ();
1758

  
1759
  (* Print the spec of all machines *)
1760
  fprintf header_fmt "/* Spec declarations */@.";
1761
  List.iter (print_machine_spec machines header_fmt) machines;
1379 1762
  pp_print_newline header_fmt ();
1763

  
1764
  (* Print the transition of all machines *)
1765
  fprintf header_fmt "/* Transitions declarations */@.";
1766
  List.iter (pp_acsl_def_trans header_fmt) (List.rev machines);
1767
  pp_print_newline header_fmt ();
1768

  
1380 1769
  (* Print the prototypes of all machines *)
1381 1770
  fprintf header_fmt "/* Nodes declarations */@.";
1382 1771
  List.iter (print_machine_decl machines header_fmt) machines;

Also available in: Unified diff