Project

General

Profile

Revision d75eb6f1

View differences:

src/tools/seal/seal_export.ml
1
(* Multiple export channels for switched systems:
2
- lustre
3
- matlab
4
- text
5
 *)
6
open Lustre_types
7
open Machine_code_types
8

  
9
let verbose = false
10
            
11
let to_lustre m sw_init sw_step init_out update_out =
12
  let orig_nd = m.mname in
13
  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
14
  let vl = (* memories *)
15
    match sw_init with
16
    | [] -> assert false
17
    | (gl, up)::_ -> List.map (fun (v,_) -> v) up
18
  in
19
(*  let add_pre sw =
20
    List.map (fun (gl, up) ->
21
        List.map (fun (g,b) ->
22
            if not b then
23
              assert false (* should be guaranted by constrauction *)
24
            else
25
              add_pre_expr vl g) gl,
26
        List.map (fun (v,e) -> add_pre_expr vl e) up
27
      ) sw
28
  in
29
 *)
30
  
31
  let rec process_sw f_e sw =
32
    let process_branch g_opt up =
33
      let el = List.map (fun (v,e) -> f_e e) up in
34
      let loc = (List.hd el).expr_loc in
35
      let new_e = Corelang.mkexpr loc (Expr_tuple el) in
36
      match g_opt with
37
        None -> None, new_e, loc
38
      | Some g ->
39
         let g = f_e g in
40
         let ee = Corelang.mkeexpr loc g in
41
         let new_e = if verbose then
42
           {new_e with
43
             expr_annot =
44
               Some ({annots = [["seal";"guards"],ee];
45
                      annot_loc = loc})} else new_e 
46
         in
47
         Some g, new_e, loc
48
    in
49
    match sw with
50
    | [] -> assert false
51
    | [g_opt,up] -> ((* last case, no need to guard it *)
52
      let _, up_e, _ = process_branch g_opt up in
53
      up_e
54
    )
55
    | (g_opt,up)::tl ->
56
       let g_opt, up_e, loc = process_branch g_opt up in
57
       match g_opt with
58
       | None -> assert false (* How could this happen anyway ? *)
59
       | Some g ->
60
          let tl_e = process_sw f_e tl in
61
          Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)) 
62
  in
63
    
64
  let e_init = process_sw (fun x -> x) sw_init in
65
  let e_step = process_sw (Corelang.add_pre_expr vl) sw_step in
66
  let e_init_out = process_sw (fun x -> x) init_out in
67
  let e_update_out = process_sw (Corelang.add_pre_expr vl) update_out in
68
  let loc = Location.dummy_loc in 
69
  { copy_nd with
70
    node_id = copy_nd.node_id ^ "_seal";
71
    node_locals = m.mmemory;
72
    node_stmts = [Eq
73
                    { eq_loc = loc;
74
                      eq_lhs = vl; 
75
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step))
76
                    };
77
                 Eq
78
                    { eq_loc = loc;
79
                      eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; 
80
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))
81
                    };
82
                 ]
83
(*
84
                   il faut mettre un pre devant chaque memoire dans les updates comme dans les gardes par contre pas besoin de mettre de pre devant les entrees, ni dans les updates, ni dans les gardes
85

  
86

  
87
                                                                                                                                                                                        ecrire une expression
88

  
89
                                                                                                                                                                                        (mem1, mem2, mem3) = if garde1 then (e1,e2,e2) else if garde2 then (e1,e2,e3) else ...... else (* garde3 *) (e1,e2,e2)
90

  
91
                                                                                                                                                                                                                                                                                         Il faut aussi calculer la fonction de sortie
92

  
93
  out1,out2 = if garde1 then e1,e2 else if garde2 ....
94
   *)    
95
  }
src/tools/seal/seal_extract.ml
774 774
          prefix
775 775
        :
776 776
          ((expr * bool) list * (ident * expr) list ) list =
777
  Format.eprintf "Build_switch with %a@."
778
    (Utils.fprintf_list ~sep:",@ "
779
       (fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a@ ]@]"
780
                               id
781
                               pp_mdefs gel))
782
    mem_defs;
777 783
  (* if all mem_defs have empty guards, we are done, return prefix,
778 784
     mem_defs expr.
779 785

  
......
884 890
     Each assign is stored in a hash tbl as list of guarded
885 891
     expressions. The memory definition is also "rewritten" as such a
886 892
     list of guarded assigns.  *)
887
  let mem_defs =
888
    List.fold_left (fun accu eq ->
893
  let mem_defs, output_defs =
894
    List.fold_left (fun (accu_mems, accu_outputs) eq ->
889 895
        match eq.eq_lhs with
890 896
        | [vid] ->
891
           (* Only focus on non memory definitions *)
892
           if not (List.exists (fun v -> v.var_id = vid) mems) then (
893
             report ~level:3 (fun fmt ->
894
                 Format.fprintf fmt "Registering variable %s@." vid);
895
             add_def vid eq.eq_rhs;
896
             accu
897
           )
898
           else
897
           (* Only focus on memory definitions *)
898
           if List.exists (fun v -> v.var_id = vid) mems then 
899 899
             (
900 900
               match eq.eq_rhs.expr_desc with
901 901
               | Expr_pre def_m ->
902 902
                  report ~level:3 (fun fmt ->
903 903
                      Format.fprintf fmt "Preparing mem %s@." vid);
904
                  (vid, rewrite defs def_m)::accu
904
                  (vid, rewrite defs def_m)::accu_mems, accu_outputs
905 905
               | _ -> assert false
906
             )
906
             ) 
907
           else if List.exists (fun v -> v.var_id = vid) nd.node_outputs then (
908
             report ~level:3 (fun fmt ->
909
                 Format.fprintf fmt "Output variable %s@." vid);
910
             add_def vid eq.eq_rhs;
911
             accu_mems, (vid, rewrite defs eq.eq_rhs)::accu_outputs
912
          
913
           )
914
           else
915
             (
916
             report ~level:3 (fun fmt ->
917
                 Format.fprintf fmt "Registering variable %s@." vid);
918
             add_def vid eq.eq_rhs;
919
             accu_mems, accu_outputs
920
           )
907 921
        | _ -> assert false (* should have been removed by normalization *)
908
      ) [] sorted_eqs
922
      ) ([], []) sorted_eqs
909 923
  in
910 924

  
911 925
  
......
928 942
  let init_defs, update_defs =
929 943
    split_init mem_defs 
930 944
  in
945
  let init_out, update_out =
946
    split_init output_defs
947
  in
931 948
  report ~level:3
932 949
    (fun fmt ->
933 950
      Format.fprintf fmt
......
959 976
  let sw_sys =
960 977
    build_switch_sys update_defs []
961 978
  in
962
  let sw_init, sw_sys = clean_sys sw_init, clean_sys sw_sys in
963 979

  
980
  let init_out =
981
    build_switch_sys init_out []
982
  in
983
  let update_out =
984
    build_switch_sys update_out []
985
  in
986

  
987
  let sw_init = clean_sys sw_init in
988
  let sw_sys = clean_sys sw_sys in
989
  let init_out = clean_sys init_out in
990
  let update_out = clean_sys update_out in
964 991

  
965 992
  (* Some additional checks *)
966 993
  let pp_gl pp_expr =
......
1146 1173
      ) map []
1147 1174
    
1148 1175
  in
1149
  process sw_init, process sw_sys
1176
  process sw_init, process sw_sys, process init_out, process update_out
src/tools/seal/seal_verifier.ml
62 62
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
63 63

  
64 64
  let consts = Corelang.(List.map const_of_top (get_consts prog)) in
65
  let sw_init, sw_sys = node_as_switched_sys consts mems sliced_nd in
65
  let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in
66 66
  let pp_res pp_expr =
67 67
    (Utils.fprintf_list ~sep:"@ "
68 68
       (fun fmt (g, up) ->
......
97 97
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "
98 98
        pp_res  sw_sys
99 99
    );
100
  (* let new_node = Seal_export.to_lustre(m,sw_init, sw_sys) in  
101
   * Format.eprintf "%a@." Printer.pp_node new_node; *)
100
  let new_node = Seal_export.to_lustre m sw_init sw_sys init_out update_out in  
101
  Format.eprintf "%a@." Printers.pp_node new_node;
102 102
  ()
103 103
  
104 104
module Verifier =

Also available in: Unified diff