Project

General

Profile

Download (5.02 KB) Statistics
| Branch: | Tag: | Revision:
1
(* TODO
2

    
3
   - build the output function: for the moment we slice the node with its
4
   memories, building the function updating the memory. We will need later the
5
   output function, using inputs and memories to compute the output. A way to do
6
   this would be to declared memories as input, remove their definitions, and
7
   slice the node with its outputs. This should clean up unnecessary internal
8
   variables and give us the output function.
9

    
10
   - compute the dimension of the node (nb of memories)
11

    
12
   - if the updates are all linear or affine, provide the update as a matrix
13
   rather then a polynomial. Check if this is simpler to do here or in matlab.
14

    
15
   - analyzes require bounds on inputs or sometimes target property over states.
16
   These could be specified as node annotations: eg -
17
   /seal/bounds/inputs/semialg/: (in1^4 + in2^3, 1) to specify that the inputs
18
   are constrained by a semialgebraic set (p,b) such as p(inputs) <= b -
19
   /seal/bounds/inputs/LMI/: (todo_describe_a_matrix) .... and so on. To be
20
   defined depending on needs. - /seal/prop/semialg/: (x3 - x5, 2) -- if x3 - x5
21
   <= 2 is the property to prove *)
22

    
23
open Seal_slice
24
open Seal_extract
25
open Seal_utils
26

    
27
let active = ref false
28

    
29
let seal_export = ref None
30

    
31
let set_export s =
32
  match s with
33
  | "lustre" | "lus" | "m" | "matlab" ->
34
    seal_export := Some s
35
  | _ ->
36
    Format.eprintf "Unrecognized seal export: %s@.@?" s;
37
    exit 1
38

    
39
(* Select the appropriate node, should have been inlined already and extract
40
   update/output functions. *)
41
let seal_run ~basename prog machines =
42
  let node_name =
43
    match !Options.main_node with
44
    | "" ->
45
      Format.eprintf "SEAL verifier requires a main node.@.";
46
      Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
47
        (Utils.fprintf_list ~sep:"@ " (fun fmt m ->
48
             Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id))
49
        machines;
50
      exit 1
51
    | s -> (
52
      (* should have been addessed before *)
53
      match Machine_code_common.get_machine_opt machines s with
54
      | None ->
55
        Global.main_node := s;
56
        Format.eprintf "Code generation error: %a@." Error.pp_error_msg
57
          Error.Main_not_found;
58
        raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
59
      | Some _ ->
60
        s)
61
  in
62
  let m = Machine_code_common.get_machine machines node_name in
63
  let nd = m.mname in
64
  let mems = m.mmemory in
65

    
66
  report ~level:1 (fun fmt ->
67
      Format.fprintf fmt "Node %s compiled: %i memories@." nd.node_id
68
        (List.length mems));
69

    
70
  (* Slicing node *)
71
  let msch = Utils.desome m.msch in
72
  let sliced_nd = slice_node (mems @ nd.node_outputs) msch nd in
73
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
74
  report ~level:10 (fun fmt ->
75
      Format.fprintf fmt "Sliced Node %a@." Printers.pp_node sliced_nd);
76

    
77
  let consts = Corelang.(List.map const_of_top (get_consts prog)) in
78

    
79
  let pp_sys = pp_sys Printers.pp_expr in
80
  if List.length mems = 0 then (
81
    (* A stateless node = a function ! *)
82
    let update_out = fun_as_switched_sys consts sliced_nd in
83

    
84
    report ~level:1 (fun fmt ->
85
        Format.fprintf fmt "Output (%i step switch cases):@ @[<v 0>%a@]@."
86
          (List.length update_out) pp_sys update_out);
87

    
88
    let _ =
89
      match !seal_export with
90
      | Some "lustre" | Some "lus" ->
91
        Seal_export.fun_to_lustre basename prog m update_out
92
      | Some "matlab" | Some "m" ->
93
        assert false (* TODO *)
94
      | Some _ ->
95
        assert false
96
      | None ->
97
        ()
98
    in
99
    ())
100
  else
101
    (* A stateful node *)
102
    let sw_init, sw_sys, init_out, update_out =
103
      node_as_switched_sys consts mems sliced_nd
104
    in
105

    
106
    report ~level:1 (fun fmt ->
107
        Format.fprintf fmt
108
          "DynSys: (%i memories, %i init, %i step switch cases)@ @[<v 0>@[<v \
109
           3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@."
110
          (List.length mems) (List.length sw_init) (List.length sw_sys) pp_sys
111
          sw_init pp_sys sw_sys);
112

    
113
    report ~level:1 (fun fmt ->
114
        Format.fprintf fmt
115
          "Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ \
116
           @[<v 3>Step:@ %a@]@]@."
117
          (List.length init_out) (List.length update_out) pp_sys init_out pp_sys
118
          update_out);
119

    
120
    let _ =
121
      match !seal_export with
122
      | Some "lustre" | Some "lus" ->
123
        Seal_export.node_to_lustre basename prog m sw_init sw_sys init_out
124
          update_out
125
      | Some "matlab" | Some "m" ->
126
        assert false (* TODO *)
127
      | Some _ ->
128
        assert false
129
      | None ->
130
        ()
131
    in
132
    ()
133

    
134
module Verifier : VerifierType.S = struct
135
  include VerifierType.Default
136

    
137
  let name = "seal"
138

    
139
  let options =
140
    [
141
      "-export", Arg.String set_export, "seal export option (lustre, matlab)";
142
      "-debug", Arg.Set seal_debug, "seal debug";
143
    ]
144

    
145
  let activate () =
146
    active := true;
147
    Options.global_inline := true;
148
    Options.optimization := 0;
149
    Options.const_unfold := true;
150
    ()
151

    
152
  let is_active () = !active
153

    
154
  let run = seal_run
155
end
156

    
157
let () =
158
  VerifierList.registered :=
159
    (module Verifier : VerifierType.S) :: !VerifierList.registered
(6-6/6)