Project

General

Profile

« Previous | Next » 

Revision 518951ed

Added by Pierre-Loïc Garoche over 5 years ago

Seal export lustre

View differences:

src/tools/seal/seal_export.ml
8 8

  
9 9
let verbose = true
10 10
            
11
let to_lustre m sw_init sw_step init_out update_out =
11
let sw_to_lustre m sw_init sw_step init_out update_out =
12 12
  let orig_nd = m.mname in
13 13
  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
14 14
  let vl = (* memories *)
......
66 66
  let e_init_out = process_sw (fun x -> x) init_out in
67 67
  let e_update_out = process_sw (Corelang.add_pre_expr vl) update_out in
68 68
  let loc = Location.dummy_loc in
69
  (* Build the contract: guarentee output = orig_node(input) *)
70
  let expr_of_vars vl = 
71
    Corelang.expr_of_expr_list loc
72
      (List.map Corelang.expr_of_vdecl vl)
73
  in
74
  let input_e = expr_of_vars  copy_nd.node_inputs in
75
  let output_e = expr_of_vars  copy_nd.node_outputs in
76
  let call_orig_e =
77
    Corelang.mkexpr loc (Expr_appl (orig_nd.node_id, input_e , None)) in 
78
  let args = Corelang.mkexpr loc (Expr_tuple([output_e; call_orig_e])) in
79
  let eq_expr = (Corelang.mkexpr loc (Expr_appl ("=", args, None))) in
80
  let contract = {
81
      consts = [];
82
      locals = [];
83
      stmts = [];
84
      assume = [];
85
      guarantees = [Corelang.mkeexpr loc eq_expr];
86
      modes = [];
87
      imports = [];
88
      spec_loc = loc;              
89
     
90
    }
91
  in
92
  { copy_nd with
69
  let new_nd =
70
    { copy_nd with
93 71
    node_id = copy_nd.node_id ^ "_seal";
94 72
    node_locals = m.mmemory;
95 73
    node_stmts = [Eq
......
103 81
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))
104 82
                    };
105 83
                 ];
106
    node_spec = Some (Contract contract);
84
    (*node_spec = Some (Contract contract);*)
107 85
                 
108 86
(*
109 87
                   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
......
117 95

  
118 96
  out1,out2 = if garde1 then e1,e2 else if garde2 ....
119 97
   *)    
120
  }
98
    }
99
  in
100
  new_nd, orig_nd
101

  
102
  
103
let to_lustre basename prog m sw_init sw_step init_out update_out =
104
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
105
  
106
  (* Format.eprintf "%a@." Printers.pp_node new_node; *)
107

  
108
  (* Main output *)
109
  let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in
110
  let new_top =
111
    Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node)
112
  in
113
let out = open_out output_file in
114
  let fmt = Format.formatter_of_out_channel out in
115
  Format.fprintf fmt "%a@." Printers.pp_prog  [new_top];
116

  
117
  (* Verif output *)
118
  let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in
119
  let out_verif = open_out output_file_verif in
120
  let fmt_verif = Format.formatter_of_out_channel out_verif in
121
  let check_nd = Lustre_utils.check_eq new_node orig_nd in
122
  let check_top =
123
    Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd)
124
  in
125
  Format.fprintf fmt_verif "%a@." Printers.pp_prog  (prog@[new_top;check_top]);

Also available in: Unified diff