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]);
src/tools/seal/seal_verifier.ml
3 3
open Seal_utils
4 4

  
5 5
let active = ref false
6
let seal_export = ref None
6 7

  
8
let set_export s = match s with
9
  | "lustre" | "lus" | "m" | "matlab" -> seal_export := Some s
10
  | _ -> (Format.eprintf "Unrecognized seal export: %s@.@?" s; exit 1)
7 11
(* TODO
8 12

  
9 13
   - build the output function: for the moment we slice the node with
......
97 101
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "
98 102
        pp_res  sw_sys
99 103
    );
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
  let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in
103
  Format.eprintf "%s@." output_file;
104
  let new_top = Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node) in
105

  
106
  let out = open_out output_file in
107
  let fmt = Format.formatter_of_out_channel out in
108
  Format.fprintf fmt "%a@." 
109
    Printers.pp_prog  (prog@[new_top]);
104
  let _ = match !seal_export with
105
    | Some "lustre" | Some "lus" ->
106
       Seal_export.to_lustre basename prog m sw_init sw_sys init_out update_out  
107
    | Some "matlab" | Some "m" -> assert false (* TODO *)
108
    | Some _ -> assert false 
109
    | None -> ()
110
  in
110 111
  ()
111 112
  
112 113
module Verifier =
113 114
  (struct
114 115
    include VerifierType.Default
115 116
    let name = "seal"
116
    let options = []
117
    let options = ["-export", Arg.String set_export, "seal export option (lustre, matlab)"]
117 118
    let activate () =
118 119
      active := true;
119 120
      Options.global_inline := true

Also available in: Unified diff