Project

General

Profile

Download (12.5 KB) Statistics
| Branch: | Tag: | Revision:
1 2863281f ploc
open Lustre_types
2
open Machine_code_types
3 75c459f4 Lélio Brun
open Spec_types
4
open Spec_common
5 2863281f ploc
open Corelang
6
  
7
let print_statelocaltag = true
8
9 c35de73b ploc
let is_memory m id =
10 70be4acf ploc
  (List.exists (fun o -> o.var_id = id.var_id) m.mmemory) 
11 c35de73b ploc
12
let rec pp_val m fmt v =
13
  let pp_val = pp_val m in
14 2863281f ploc
  match v.value_desc with
15 c35de73b ploc
  | Cst c         -> Printers.pp_const fmt c 
16
  | Var v    ->
17
     if is_memory m v then
18 2863281f ploc
       if print_statelocaltag then
19 c35de73b ploc
	 Format.fprintf fmt "%s(S)" v.var_id
20 2863281f ploc
       else
21 c35de73b ploc
	 Format.pp_print_string fmt v.var_id 
22
     else     
23 2863281f ploc
       if print_statelocaltag then
24 c35de73b ploc
	 Format.fprintf fmt "%s(L)" v.var_id
25 2863281f ploc
       else
26
	 Format.pp_print_string fmt v.var_id
27 c35de73b ploc
  | Array vl      -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val)  vl
28
  | Access (t, i) -> Format.fprintf fmt "%a[%a]" pp_val t pp_val i
29
  | Power (v, n)  -> Format.fprintf fmt "(%a^%a)" pp_val v pp_val n
30
  | Fun (n, vl)   -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val)  vl
31 2863281f ploc
32 c35de73b ploc
let rec  pp_instr m fmt i =
33
 let     pp_val = pp_val m and
34
      pp_branch = pp_branch m in
35 2863281f ploc
  let _ =
36
    match i.instr_desc with
37
    | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
38
    | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
39
    | MReset i           -> Format.fprintf fmt "reset %s" i
40
    | MNoReset i         -> Format.fprintf fmt "noreset %s" i
41
    | MStep (il, i, vl)  ->
42
       Format.fprintf fmt "%a = %s (%a)"
43
	 (Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
44
	 i
45
	 (Utils.fprintf_list ~sep:", " pp_val) vl
46
    | MBranch (g,hl)     ->
47
       Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
48
	 pp_val g
49
	 (Utils.fprintf_list ~sep:"@," pp_branch) hl
50
    | MComment s -> Format.pp_print_string fmt s
51 1fd3d002 ploc
    | MSpec s -> Format.pp_print_string fmt ("@" ^ s)
52 2863281f ploc
       
53
  in
54
  (* Annotation *)
55
  (* let _ = *)
56
  (*   match i.lustre_expr with None -> () | Some e -> Format.fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
57
  (* in *)
58
  let _ = 
59
    match i.lustre_eq with None -> () | Some eq -> Format.fprintf fmt " -- original eq: %a" Printers.pp_node_eq eq
60
  in
61
  ()
62
    
63 c35de73b ploc
and pp_branch m fmt (t, h) =
64
  Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," (pp_instr m)) h
65 2863281f ploc
66 c35de73b ploc
and pp_instrs m fmt il =
67
  Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," (pp_instr m)) il
68 2863281f ploc
69
70
(* merge log: get_node_def was in c0f8 *)
71
(* Returns the node/machine associated to id in m calls *)
72
let get_node_def id m =
73
  try
74
    let (decl, _) = List.assoc id m.mcalls in
75
    Corelang.node_of_top decl
76
  with Not_found -> ( 
77
    (* Format.eprintf "Unable to find node %s in list [%a]@.@?" *)
78
    (*   id *)
79
    (*   (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> Format.fprintf fmt "%s" n)) m.mcalls *)
80
    (* ; *)
81
    raise Not_found
82
  )
83
    
84
(* merge log: machine_vars was in 44686 *)
85
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
86
87 c35de73b ploc
let pp_step m fmt s =
88 2863281f ploc
  Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
89
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs
90
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs
91
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals
92 c35de73b ploc
    (Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val m fmt c)) s.step_checks
93
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) s.step_instrs
94
    (Utils.fprintf_list ~sep:", " (pp_val m)) s.step_asserts
95 2863281f ploc
96
97
let pp_static_call fmt (node, args) =
98
 Format.fprintf fmt "%s<%a>"
99
   (node_name node)
100
   (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args
101
102
let pp_machine fmt m =
103
  Format.fprintf fmt
104 7ee5f69e Lélio Brun
    "@[<v 2>machine %s@ \
105
     mem      : %a@ \
106
     instances: %a@ \
107
     init     : %a@ \
108
     const    : %a@ \
109
     step     :@   \
110
     @[<v 2>%a@]@ \
111
     spec     : @[%t@]@ \
112
     annot    : @[%a@]@]@ "
113 2863281f ploc
    m.mname.node_id
114
    (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
115
    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
116 c35de73b ploc
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.minit
117
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.mconst
118
    (pp_step m) m.mstep
119 7ee5f69e Lélio Brun
    (fun fmt -> match m.mspec.mnode_spec with
120
       | None -> ()
121
       | Some (NodeSpec id) -> Format.fprintf fmt "cocospec: %s" id
122
       | Some (Contract spec) -> Printers.pp_spec fmt spec)
123 2863281f ploc
    (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
124
125
let pp_machines fmt ml =
126
  Format.fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml
127
128
  
129
let rec is_const_value v =
130
  match v.value_desc with
131
  | Cst _          -> true
132 ca7e8027 Lélio Brun
  | Fun (_, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args
133 2863281f ploc
  | _              -> false
134
135
(* Returns the declared stateless status and the computed one. *)
136 9d693675 Lélio Brun
let get_stateless_status_node n =
137
  (n.node_dec_stateless,
138 1fd3d002 ploc
   try
139 9d693675 Lélio Brun
     Utils.desome n.node_stateless
140
   with _ -> failwith ("stateless status of machine " ^ n.node_id ^ " not computed"))
141
142
let get_stateless_status_top_decl td = match td.top_decl_desc with
143
  | Node n -> get_stateless_status_node n
144
  | ImportedNode n -> n.nodei_stateless, false
145
  | _ -> true, false
146
147
let get_stateless_status m =
148
  get_stateless_status_node m.mname
149 2863281f ploc
150 e4edf171 ploc
let is_stateless m = m.minstances = [] && m.mmemory = []
151
152 ca7e8027 Lélio Brun
(* let is_input m id =
153
 *   List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs *)
154 2863281f ploc
155
let is_output m id =
156
  List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
157
158 75c459f4 Lélio Brun
let get_instr_spec i = i.instr_spec
159 2863281f ploc
160
let mk_conditional ?lustre_eq c t e =
161 75c459f4 Lélio Brun
  mkinstr ?lustre_eq
162
    (Ternary (Val c,
163
              And (List.map get_instr_spec t),
164
              And (List.map get_instr_spec e)))
165
    (MBranch(c, [
166
         (tag_true, t);
167
         (tag_false, e) ]))
168
169
let mk_branch ?lustre_eq c br =
170
  mkinstr ?lustre_eq
171
    (And (List.map (fun (l, instrs) ->
172
         Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
173
         br))
174
    (MBranch (c, br))
175
176
let mk_assign ?lustre_eq x v =
177
  mkinstr ?lustre_eq
178
    (Equal (Var x, Val v))
179
    (MLocalAssign (x, v))
180 2863281f ploc
181
let mk_val v t =
182
  { value_desc = v; 
183
    value_type = t; 
184
    value_annot = None }
185
    
186
let arrow_machine =
187
  let state = "_first" in
188
  let var_state = dummy_var_decl state Type_predef.type_bool(* (Types.new_ty Types.Tbool) *) in
189
  let var_input1 = List.nth Arrow.arrow_desc.node_inputs 0 in
190
  let var_input2 = List.nth Arrow.arrow_desc.node_inputs 1 in
191
  let var_output = List.nth Arrow.arrow_desc.node_outputs 0 in
192
  let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in
193 867276c9 Guillaume DAVY
  assert(var_input1.var_type = var_input2.var_type);
194
  let t_arg = var_input1.var_type in (* TODO Xavier: c'est bien la bonne def ? Guillaume: Bof preferable de reprendre le type des variables non ? *)
195 2863281f ploc
  {
196
    mname = Arrow.arrow_desc;
197
    mmemory = [var_state];
198
    mcalls = [];
199
    minstances = [];
200 75c459f4 Lélio Brun
    minit = [mkinstr True (MStateAssign(var_state, cst true))];
201 2863281f ploc
    mstatic = [];
202
    mconst = [];
203
    mstep = {
204
      step_inputs = Arrow.arrow_desc.node_inputs;
205
      step_outputs = Arrow.arrow_desc.node_outputs;
206
      step_locals = [];
207
      step_checks = [];
208 c35de73b ploc
      step_instrs = [mk_conditional (mk_val (Var var_state) Type_predef.type_bool)
209 75c459f4 Lélio Brun
			(List.map (mkinstr True)
210 2863281f ploc
			[MStateAssign(var_state, cst false);
211 c35de73b ploc
			 MLocalAssign(var_output, mk_val (Var var_input1) t_arg)])
212 75c459f4 Lélio Brun
                        (List.map (mkinstr True)
213 c35de73b ploc
			[MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];
214 2863281f ploc
      step_asserts = [];
215
    };
216 7ee5f69e Lélio Brun
    mspec = { mnode_spec = None; mtransitions = [] };
217 2863281f ploc
    mannot = [];
218 95fb046e ploc
    msch = None
219 2863281f ploc
  }
220
221
let empty_desc =
222
  {
223
    node_id = Arrow.arrow_id;
224
    node_type = Types.bottom;
225
    node_clock = Clocks.bottom;
226
    node_inputs= [];
227
    node_outputs= [];
228
    node_locals= [];
229
    node_gencalls = [];
230
    node_checks = [];
231
    node_asserts = [];
232
    node_stmts= [];
233
    node_dec_stateless = true;
234
    node_stateless = Some true;
235
    node_spec = None;
236 f4cba4b8 ploc
    node_annot = [];
237
    node_iscontract = false;
238
}
239 2863281f ploc
240
let empty_machine =
241
  {
242
    mname = empty_desc;
243
    mmemory = [];
244
    mcalls = [];
245
    minstances = [];
246
    minit = [];
247
    mstatic = [];
248
    mconst = [];
249
    mstep = {
250
      step_inputs = [];
251
      step_outputs = [];
252
      step_locals = [];
253
      step_checks = [];
254
      step_instrs = [];
255
      step_asserts = [];
256
    };
257 7ee5f69e Lélio Brun
    mspec = { mnode_spec = None; mtransitions = [] };
258 2863281f ploc
    mannot = [];
259 95fb046e ploc
    msch = None
260 2863281f ploc
  }
261
262
let new_instance =
263
  let cpt = ref (-1) in
264 59020713 ploc
  fun callee tag ->
265 2863281f ploc
    begin
266
      let o =
267
	if Stateless.check_node callee then
268
	  node_name callee
269
	else
270
	  Printf.sprintf "ni_%d" (incr cpt; !cpt) in
271
      let o =
272
	if !Options.ansi && is_generic_node callee
273 59020713 ploc
	then Printf.sprintf "%s_inst_%d"
274
               o
275
               (incr cpt; !cpt)
276 2863281f ploc
	else o in
277
      o
278
    end
279
280
281 e4edf171 ploc
let get_machine_opt machines name =
282 2863281f ploc
  List.fold_left
283
    (fun res m ->
284
      match res with
285
      | Some _ -> res
286
      | None -> if m.mname.node_id = name then Some m else None)
287
    None machines
288
289 e4edf171 ploc
let get_machine machines node_name =
290
 try
291 c3b0a8c9 ploc
    Utils.desome (get_machine_opt machines node_name) 
292
 with Utils.DeSome ->
293
   Format.eprintf "Unable to find machine %s in machines %a@.@?"
294
     node_name
295
     (Utils.fprintf_list ~sep:", " (fun fmt m -> Format.pp_print_string fmt m.mname.node_id)) machines
296
      ; assert false
297 e4edf171 ploc
     
298 2863281f ploc
let get_const_assign m id =
299
  try
300
    match get_instr_desc (List.find
301
	     (fun instr -> match get_instr_desc instr with
302
	     | MLocalAssign (v, _) -> v == id
303
	     | _ -> false)
304
	     m.mconst
305
    ) with
306
    | MLocalAssign (_, e) -> e
307
    | _                   -> assert false
308
  with Not_found -> assert false
309
310
311
let value_of_ident loc m id =
312
  (* is is a state var *)
313
  try
314
    let v = List.find (fun v -> v.var_id = id) m.mmemory
315 c35de73b ploc
    in mk_val (Var v) v.var_type 
316 2863281f ploc
  with Not_found ->
317
    try (* id is a node var *)
318
      let v = get_node_var id m.mname
319 c35de73b ploc
      in mk_val (Var v) v.var_type
320 2863281f ploc
  with Not_found ->
321
    try (* id is a constant *)
322
      let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))
323 c35de73b ploc
      in mk_val (Var c) c.var_type
324 2863281f ploc
    with Not_found ->
325
      (* id is a tag *)
326
      let t = Const_tag id
327
      in mk_val (Cst t) (Typing.type_const loc t)
328
329
(* type of internal fun used in dimension expression *)
330
let type_of_value_appl f args =
331
  if List.mem f Basic_library.arith_funs
332
  then (List.hd args).value_type
333
  else Type_predef.type_bool
334
335
let rec value_of_dimension m dim =
336
  match dim.Dimension.dim_desc with
337
  | Dimension.Dbool b         ->
338 e8f55c25 ploc
     mk_val (Cst (Const_tag (if b then tag_true else tag_false))) Type_predef.type_bool
339 2863281f ploc
  | Dimension.Dint i          ->
340
     mk_val (Cst (Const_int i)) Type_predef.type_int
341
  | Dimension.Dident v        -> value_of_ident dim.Dimension.dim_loc m v
342
  | Dimension.Dappl (f, args) ->
343
     let vargs = List.map (value_of_dimension m) args
344
     in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) 
345
  | Dimension.Dite (i, t, e)  ->
346
     (match List.map (value_of_dimension m) [i; t; e] with
347
     | [vi; vt; ve] -> mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type
348
     | _            -> assert false)
349
  | Dimension.Dlink dim'      -> value_of_dimension m dim'
350
  | _                         -> assert false
351
352
let rec dimension_of_value value =
353
  match value.value_desc with
354 e8f55c25 ploc
  | Cst (Const_tag t) when t = tag_true  -> Dimension.mkdim_bool  Location.dummy_loc true
355
  | Cst (Const_tag t) when t = tag_false -> Dimension.mkdim_bool  Location.dummy_loc false
356 2863281f ploc
  | Cst (Const_int i)                             -> Dimension.mkdim_int   Location.dummy_loc i
357 c35de73b ploc
  | Var v                                         -> Dimension.mkdim_ident Location.dummy_loc v.var_id
358 2863281f ploc
  | Fun (f, args)                                 -> Dimension.mkdim_appl  Location.dummy_loc f (List.map dimension_of_value args)
359
  | _                                             -> assert false
360
361
362
     let rec join_branches hl1 hl2 =
363
 match hl1, hl2 with
364
 | []          , _            -> hl2
365
 | _           , []           -> hl1
366
 | (t1, h1)::q1, (t2, h2)::q2 ->
367
   if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else
368
   if t1 > t2 then (t2, h2) :: join_branches hl1 q2
369
   else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
370
371
and join_guards inst1 insts2 =
372
 match get_instr_desc inst1, List.map get_instr_desc insts2 with
373
 | _                   , []                               ->
374
   [inst1]
375 ca7e8027 Lélio Brun
 | MBranch (x1, hl1), MBranch (x2, hl2) :: _ when x1 = x2 ->
376 75c459f4 Lélio Brun
    mkinstr True
377 2863281f ploc
      (* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
378
      (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
379
   :: (List.tl insts2)
380
 | _ -> inst1 :: insts2
381
382
let join_guards_list insts =
383
 List.fold_right join_guards insts []