Project

General

Profile

Revision f4cba4b8

View differences:

TODO.org
141 141
** Development
142 142
*** Done
143 143
- (ploc) retirer le parser Kind2 et revenir à celui de lustrec
144

  
144 145
*** To be done
146

  
145 147
**** Court terme
146 148
- (CG) etendre la syntaxe pour coller à la definition donnée ci-dessus
147 149
  - lexeur/parseur lustreSpec + document latex de grammaire
src/arrow.ml
19 19
    node_dec_stateless = false;
20 20
    node_stateless = Some false;
21 21
    node_spec = None;
22
    node_annot = [];  }
22
    node_annot = [];
23
    node_iscontract = false;
24
}
23 25

  
24 26
let arrow_top_decl =
25 27
  {
src/automata.ml
162 162
    node_dec_stateless = false;
163 163
    node_stateless = None;
164 164
    node_spec = None;
165
    node_annot = []
165
    node_annot = [];
166
    node_iscontract = false;
166 167
  },
167 168
  mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset))
168 169

  
......
213 214
    node_dec_stateless = false;
214 215
    node_stateless = None;
215 216
    node_spec = None;
216
    node_annot = handler.hand_annots
217
    node_annot = handler.hand_annots;
218
    node_iscontract = false;
217 219
  },
218 220
  mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset))
219 221

  
src/backends/EMF/EMF_backend.ml
393 393
  fprintf fmt "\"contract\": \"%s\",@ "
394 394
    i.import_nodeid;
395 395
  fprintf fmt "\"inputs\": [%a],@ "
396
    pp_emf_exprs i.inputs;
396
    pp_emf_expr i.inputs;
397 397
  fprintf fmt "\"outputs\": [%a],@ "
398
    pp_emf_exprs i.outputs;
398
    pp_emf_expr i.outputs;
399 399
  fprintf fmt "@]}"
400 400
  
401 401
let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import
......
421 421
let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
422 422
let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list
423 423

  
424
let pp_emf_contract fmt nd =
425
  let c = Printers.node_as_contract nd in
426
  fprintf fmt "@[v 2>\"%a\": {@ "
427
    print_protect (fun fmt -> pp_print_string fmt nd.node_id);
428
  fprintf fmt "\"contract\": %a@ "
429
    pp_emf_spec c;
430
  fprintf fmt "@]@ }"
424 431
  
425
                                           
426 432
let pp_machine fmt m =
427 433
  let instrs = (*merge_branches*) m.mstep.step_instrs in
428 434
  try
......
445 451
    fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
446 452
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
447 453
      (pp_emf_instrs m) instrs;
448
    (match m.mspec with None -> () | Some spec -> fprintf fmt "\"spec\": %a,@ " pp_emf_spec spec);
454
    (match m.mspec with | None -> () 
455
                        | Some (Contract _) -> assert false 
456
                        | Some (NodeSpec id) -> fprintf fmt "\"coco_contract\": %s" id
457
    );
449 458
    fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
450 459
    fprintf fmt "@]@ }"
451 460
  with Unhandled msg -> (
......
455 464
    eprintf "node skipped - no output generated@ @]@."
456 465
  )
457 466

  
467
let pp_machine fmt m =                      
468
  match m.mspec with
469
  | None | Some (NodeSpec _) -> pp_machine fmt m
470
  | Some (Contract _) -> pp_emf_contract fmt m.mname 
471
                       
458 472
let pp_emf_imported_node fmt top =
459 473
  let ind = Corelang.imported_node_of_top top in
460
   try
474
  try
461 475
    fprintf fmt "@[<v 2>\"%a\": {@ "
462 476
      print_protect (fun fmt -> pp_print_string fmt ind.nodei_id);
463 477
    fprintf fmt "\"imported\": \"true\",@ ";
......
466 480
    fprintf fmt "\"outputs\": [%a],@ "
467 481
      pp_emf_vars_decl ind.nodei_outputs;
468 482
    fprintf fmt "\"original_name\": \"%s\",@ " ind.nodei_id;
469
    (match ind.nodei_spec with None -> () | Some spec -> fprintf fmt "\"spec\": %a" pp_emf_spec spec);
483
    (match ind.nodei_spec with None -> ()
484
                             | Some (Contract _) -> assert false (* should have been processed *)
485
                             | Some (NodeSpec id) -> fprintf fmt "\"coco_contract\": %s" id
486
    );
470 487
    fprintf fmt "@]@ }"
471 488
  with Unhandled msg -> (
472 489
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
src/causality.ml
148 148
    List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)
149 149

  
150 150
  let node_input_variables nd =
151
    List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty nd.node_inputs
151
    List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty 
152
      (if nd.node_iscontract then
153
         nd.node_inputs@nd.node_outputs
154
       else
155
         nd.node_inputs)
156
    
157
  let node_output_variables nd =
158
    List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty
159
      (if nd.node_iscontract then [] else nd.node_outputs)
152 160

  
153 161
  let node_local_variables nd =
154 162
    List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals
......
156 164
  let node_constant_variables nd =
157 165
    List.fold_left (fun locals v -> if v.var_dec_const then ISet.add v.var_id locals else locals) ISet.empty nd.node_locals
158 166

  
159
  let node_output_variables nd =
160
    List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs
161

  
162 167
  let node_auxiliary_variables nd =
163 168
    ISet.diff (node_local_variables nd) (node_memory_variables nd)
164 169

  
......
170 175
(* computes the equivalence relation relating variables 
171 176
   in the same equation lhs, under the form of a table 
172 177
   of class representatives *)
173
  let node_eq_equiv nd =
178
  let eqs_eq_equiv eqs =
174 179
    let eq_equiv = Hashtbl.create 23 in
175 180
    List.iter (fun eq ->
176 181
      let first = List.hd eq.eq_lhs in
177 182
      List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs
178 183
    )
179
      (get_node_eqs nd);
184
      eqs;
180 185
    eq_equiv
181

  
186
    
187
  let node_eq_equiv nd = eqs_eq_equiv  (get_node_eqs nd)
188
  
182 189
(* Create a tuple of right dimension, according to [expr] type, *)
183 190
(* filled with variable [v] *)
184 191
  let adjust_tuple v expr =
......
624 631
    ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems;
625 632
  end
626 633

  
634
(* Takes a node and return a pair (node', graph) where node' is node
635
   rebuilt with the equations enriched with new ones introduced to
636
   "break cycles" *)
627 637
let global_dependency node =
628 638
  let mems = ExprDep.node_memory_variables node in
629 639
  let inputs =
src/checks/stateless.ml
76 76
  List.iter (fun td -> ignore (force_node td)) decls
77 77

  
78 78
let check_compat_decl decl =
79
 match decl.top_decl_desc with
80
 | ImportedNode nd ->
81
   let td = Corelang.node_from_name nd.nodei_id in
82
   (match td.top_decl_desc with
83
   | Node nd' -> let stateless = check_node td in
84
		 if nd.nodei_stateless && (not stateless)
85
		 then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))
86
		 else nd'.node_dec_stateless <- nd.nodei_stateless
87
   | _        -> assert false)
88
 | Node _          -> assert false
89
 | _               -> ()
79
  match decl.top_decl_desc with
80
  | ImportedNode nd -> (* A node declared in the header (lusi) shall
81
                          be locally defined with compatible stateless
82
                          flag *)
83
     begin
84
       let td = Corelang.node_from_name nd.nodei_id in
85
       (match td.top_decl_desc with
86
        | Node nd' -> let stateless = check_node td in
87
		      if nd.nodei_stateless && (not stateless)
88
		      then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))
89
		      else nd'.node_dec_stateless <- nd.nodei_stateless
90
        | _        -> assert false)
91
     end
92
  | Node nd -> (
93
     match nd.node_spec with
94
       Some (Contract _) -> (* A contract element in a header does not
95
                               need to be provided in the associed lus
96
                               file *)
97
        ()
98
     | _ -> assert false)
99
             
100
  | _               -> ()
90 101

  
91 102
let check_compat header =
92 103
  List.iter check_compat_decl header
src/clock_calculus.ml
794 794

  
795 795
let check_env_compat header declared computed =
796 796
  uneval_prog_generics header;
797
  Env.iter declared (fun k decl_clock_k -> 
798
    let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
799
    try_semi_unify decl_clock_k computed_c Location.dummy_loc
800
  ) 
797
  Env.iter declared (fun k decl_clock_k ->
798
      try
799
        let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
800
        try_semi_unify decl_clock_k computed_c Location.dummy_loc
801
      with Not_found -> (* If the lookup failed then either an actual
802
                           required element should have been declared
803
                           and is missing but typing should have catch
804
                           it, or it was a contract and does not
805
                           require this additional check.  *)
806
          ()
807
    ) 
801 808
(* Local Variables: *)
802 809
(* compile-command:"make -C .." *)
803 810
(* End: *)
src/compiler_common.ml
187 187
      Location.pp_loc loc;
188 188
    raise exc
189 189

  
190
(* Process each node/imported node and introduce the associated contract node *)
191
let resolve_contracts prog =
192
  (* Bind a fresh node with a new name according to existing nodes and freshly binded contract node. Clean the contract to remove the stmts  *)
193
  let process_contract new_contracts prog c =
194
    (* Resolve first the imports *)
195
    let stmts, locals, c =
196
      List.fold_left (
197
          fun (stmts, locals, c) import ->
198
          (* Search for contract in prog.
199
             The node have to be processed already. Otherwise raise an error.
200
             Each stmts in injected with a fresh name
201
             Inputs are renamed and associated to the expression in1
202
             Same thing for outputs.
190 203

  
204
             Last the contracts elements are replaced with the renamed vars and merged with c contract.
205
           *)
206
          let name = import.import_nodeid in
207
          assert false; (* TODO: we do not handle imports yet.  The
208
                           algorithm is sketched below *)
209
        (*
210
          try
211
            let imp_nd = xxx in (* Get the contract node in prog *)
212
            (* checking that it's actually a (processed) contract *)
213
            let imp_c =
214
              match imp_nd.node_spec with
215
                Some (Contract imp_c) ->
216
                 if imp_c.imports = [] then
217
                   imp_c
218
                 else
219
                   assert false (* should be processed *)
220
              | _ -> assert false (* should be a contract *)
221
            in  
222
            (* Preparing vars: renaming them *)
223
            let imp_in = rename imp_nd.node_inputs in
224
            let imp_out = rename imp_nd.node_outputs in
225
            let imp_locals = rename imp_nd.node_locals in
226
            let locals = imp_in@imp_out@imp_locals@locals in
227
            (* Assinging in and out *)
228
            let in_assigns =
229
              xxx imp_in = import.inputs
230
            in
231
            let out_assigns =
232
              xxx imp_out = import.outputs
233
            in
234
            let stmts = stmts @ (rename imp_nd.stmts) in
235
            let imp_c = rename imp_c in
236
            let c = merge_contracts c imp_c in
237
            stmts, locals, c 
238
          with Not_found -> raise (Error.Unbound_symbol ("contract " ^ name))
239

  
240
                            *)
241
        ) ([], c.consts@c.locals, c) c.imports
242
    in
243
    (* Other contract elements will be normalized later *)
244
    let c = { c with
245
              locals = [];
246
              consts = [];
247
              stmts = [];
248
              imports = []
249
            }
250
    in
251
    stmts, locals, c
252
    
253
  in
254
  let process_contract_new_node accu_contracts prog top =
255
    let id, spec, inputs, outputs =
256
      match top.top_decl_desc with
257
      | Node nd -> nd.node_id, nd.node_spec, nd.node_inputs, nd.node_outputs
258
      | ImportedNode ind -> ind.nodei_id, ind.nodei_spec, ind.nodei_inputs, ind.nodei_outputs
259
      | _ -> assert false
260
    in
261
    let stmts, locals, c =
262
      match spec with
263
      | None | Some (NodeSpec _) -> assert false
264
      | Some (Contract c) ->
265
         process_contract accu_contracts prog c
266
    in
267
    (* Create a fresh name *)
268
    let used v = List.exists (fun top ->
269
                     match top.top_decl_desc with
270
                     | Node _
271
                       | ImportedNode _ ->
272
                        (node_name top) = v
273
                     | _ -> false
274
                   ) (accu_contracts@prog)
275
    in
276
    let new_nd_id = mk_new_name used (id ^ "_coco") in
277
    let new_nd =
278
      mktop_decl
279
        c.spec_loc
280
        top.top_decl_owner
281
        top.top_decl_itf
282
      (Node {
283
           node_id = new_nd_id;
284
	   node_type = Types.new_var ();
285
	   node_clock = Clocks.new_var true;
286
	   node_inputs = inputs;
287
	   node_outputs = outputs;
288
	   node_locals = locals;
289
	   node_gencalls = [];
290
	   node_checks = [];
291
	   node_asserts = []; 
292
	   node_stmts = stmts;
293
	   node_dec_stateless = false;
294
	   node_stateless = None;
295
	   node_spec = Some (Contract c);
296
	   node_annot = [];
297
	   node_iscontract = true;
298
      }) in
299
    new_nd
300
  in
301
  (* Processing nodes in order. Should have been sorted by now
302

  
303
     Each top level contract is processed: stmts pushed in node
304

  
305
     Each regular imported node or node associated with a contract is
306
     replaced with a simplidfied contract and its contract is bound to
307
     a fresh node.
308

  
309
   *)
310
  let new_contracts, prog =
311
    List.fold_left
312
      (
313
        fun (accu_contracts, accu_nodes) top ->
314
        match top.top_decl_desc with
315
          
316
        | Node nd when nd.node_iscontract -> (
317
          match nd.node_spec with
318
          | None | Some (NodeSpec _) -> assert false
319
          | Some (Contract c) ->
320
             let stmts, locals, c = process_contract accu_contracts prog c in
321
             let nd =
322
               { nd with
323
                 node_locals = nd.node_locals @ locals;
324
                 node_stmts = nd.node_stmts @ stmts;
325
                 node_spec = Some (Contract c);
326
               }
327
             in
328
             { top with top_decl_desc = Node nd }::accu_contracts,
329
             accu_nodes
330
             
331
        )
332
        | Node nd -> (
333
          match nd.node_spec with
334
          | None -> accu_contracts, top::accu_nodes (* A boring node: no contract *)
335
          | Some (NodeSpec id) -> (* shall not happen, its too early *)
336
             assert false
337
          | Some (Contract c) -> (* A contract: processing it *)
338
             (* we bind a fresh node *)
339
             let new_nd = process_contract_new_node accu_contracts prog top in
340
             Format.eprintf "Creating new contract node %s@." (node_name new_nd);
341
             let nd = { nd with node_spec = (Some (NodeSpec (node_name new_nd))) } in
342
             new_nd::accu_contracts,
343
             { top with top_decl_desc = Node nd }::accu_nodes
344
             
345
        )
346
                   
347
        | ImportedNode ind -> ( (* Similar treatment for imported nodes *)
348
          match ind.nodei_spec with
349
            None -> accu_contracts, top::accu_nodes (* A boring node: no contract *)
350
          | Some (NodeSpec id) -> (* shall not happen, its too early *)
351
             assert false
352
          | Some (Contract c) -> (* A contract: processing it *)
353
             (* we bind a fresh node *)
354
             let new_nd = process_contract_new_node accu_contracts prog top in
355
             let ind = { ind with nodei_spec = (Some (NodeSpec (node_name new_nd))) } in
356
             new_nd::accu_contracts,
357
             { top with top_decl_desc = ImportedNode ind }::accu_nodes
358
        )
359
        | _ -> accu_contracts, top::accu_nodes
360
      ) ([],[]) prog
361
  in
362
  (List.rev new_contracts) @ (List.rev prog)
363
         
364

  
365
  
191 366
let track_exception () =
192 367
  if !Options.track_exceptions
193 368
  then (Printexc.print_backtrace stdout; flush stdout)
src/compiler_stages.ml
78 78
  (* Sorting nodes *)
79 79
  let prog = SortProg.sort prog in
80 80

  
81
  (* Consolidating contracts *)
82
  let prog = resolve_contracts prog in
83
  
81 84
  (* Perform inlining before any analysis *)
82 85
  let orig, prog =
83 86
    if !Options.global_inline && !Options.main_node <> "" then
src/corelang.ml
324 324
  | ImportedNode nd -> true
325 325
  | _ -> assert false
326 326

  
327
let is_contract td =
328
  match td.top_decl_desc with 
329
  | Node nd -> (
330
    match nd.node_spec with
331
    | Some (Contract _) -> true
332
    | _ -> false
333
  )                     
334
  | _ -> false
335

  
327 336

  
328 337
(* alias and type definition table *)
329 338

  
......
855 864
     node_stateless = nd.node_stateless;
856 865
     node_spec = spec;
857 866
     node_annot = annot;
867
     node_iscontract = nd.node_iscontract;
858 868
   }
859 869

  
860 870

  
......
1255 1265
    in
1256 1266
    aux [] eqs
1257 1267

  
1268

  
1269

  
1270
       
1258 1271
(* Local Variables: *)
1259 1272
(* compile-command:"make -C .." *)
1260 1273
(* End: *)
src/corelang.mli
58 58
val update_node: ident -> top_decl -> unit
59 59
val is_generic_node: top_decl -> bool
60 60
val is_imported_node: top_decl -> bool
61

  
61
val is_contract: top_decl -> bool
62
  
62 63
val consts_table: (ident, top_decl) Hashtbl.t
63 64
val print_consts_table:  Format.formatter -> unit -> unit
64 65
val type_table: (type_dec_desc, top_decl) Hashtbl.t
......
167 168
val mk_contract_guarantees: eexpr -> contract_desc
168 169
val mk_contract_assume: eexpr -> contract_desc
169 170
val mk_contract_mode: ident -> eexpr list -> eexpr list -> Location.t -> contract_desc
170
val mk_contract_import: ident -> expr list -> expr list -> Location.t -> contract_desc
171
val mk_contract_import: ident -> expr -> expr -> Location.t -> contract_desc
171 172
val merge_contracts:  contract_desc -> contract_desc -> contract_desc 
172 173
val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr
173 174
val update_expr_annot: ident -> expr -> expr_annot -> expr
src/error.ml
24 24
  | AlgebraicLoop -> 9
25 25
  | LoadError _ -> 10
26 26

  
27

  
27 28
  let pp_error_msg fmt = function
28 29
  | Main_not_found ->
29 30
      fprintf fmt "Could not find the definition of main node %s.@."
src/inliner.ml
421 421
    node_dec_stateless = false;
422 422
    node_stateless = None;
423 423
    node_spec = Some 
424
      (mk_contract_guarantees (mkeexpr loc (mkexpr loc (Expr_ident ok_ident))));
425
      node_annot = [];
426
  }
424
                  (Contract
425
                     (mk_contract_guarantees
426
                        (mkeexpr loc (mkexpr loc (Expr_ident ok_ident)))
427
                     )
428
                  );
429
    node_annot = [];
430
    node_iscontract = true;
431
    }
427 432
  in
428 433
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
429 434
  let new_prog = others@nodes_origs@nodes_inlined@main in
src/lustre_types.ml
129 129
  { mode_id: ident; require: eexpr list; ensure: eexpr list; mode_loc: Location.t}
130 130

  
131 131
type contract_import =
132
  { import_nodeid: ident; inputs: expr list; outputs: expr list; import_loc: Location.t }
132
  { import_nodeid: ident;
133
    inputs: expr;
134
    outputs: expr;
135
    import_loc: Location.t }
133 136
    
134 137

  
135 138

  
......
174 177
    spec_loc: Location.t;
175 178
  }
176 179

  
180
type node_spec_t = Contract of contract_desc
181
                 | NodeSpec of ident
182

  
177 183
type node_desc =
178 184
    {node_id: ident;
179 185
     mutable node_type: Types.type_expr;
......
187 193
     node_stmts: statement list;
188 194
     mutable node_dec_stateless: bool;
189 195
     mutable node_stateless: bool option;
190
     node_spec: contract_desc option;
196
     node_spec: node_spec_t option;
191 197
     node_annot: expr_annot list;
198
     node_iscontract: bool;
192 199
    }
193 200

  
194 201
type imported_node_desc =
......
198 205
     nodei_inputs: var_decl list;
199 206
     nodei_outputs: var_decl list;
200 207
     nodei_stateless: bool;
201
     nodei_spec: contract_desc option;
208
     nodei_spec: node_spec_t option;
202 209
     (* nodei_annot: expr_annot list; *)
203 210
     nodei_prototype: string option;
204 211
     nodei_in_lib: string list;
......
213 220

  
214 221
  
215 222
type top_decl_desc =
216
| Node of node_desc
217
| Const of const_desc
218
| ImportedNode of imported_node_desc
219
| Open of bool * string (* the boolean set to true denotes a local
223
  | Node of node_desc
224
  | Const of const_desc
225
  | ImportedNode of imported_node_desc
226
  | Open of bool * string (* the boolean set to true denotes a local
220 227
			   lusi vs a lusi installed at system level *)
221
| Include of string (* the boolean set to true denotes a local
228
  | Include of string (* the boolean set to true denotes a local
222 229
			   lus vs a lus installed at system level *)
223
| TypeDef of typedef_desc
230
  | TypeDef of typedef_desc
224 231
    
225 232
type top_decl =
226 233
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
......
237 244
    is_stateful: bool
238 245
  }
239 246

  
247
type spec_types =
248
  | LocalContract of contract_desc
249
  | TopContract of top_decl list
250

  
240 251

  
241 252

  
242 253
(* Local Variables: *)
src/machine_code.ml
375 375
  
376 376
  ctx, ctx0.s
377 377

  
378
 
378 379
let translate_decl nd sch =
379 380
  (* Extracting eqs, variables ..  *)
380 381
  let eqs, auts = get_node_eqs nd in
......
395 396
  let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
396 397

  
397 398
  let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
398
(* CODE QUI MARCHE
399
  let constant_eqs = constant_equations locals in
400 399
  
401
  (* Compute constants' instructions  *)
402
  let ctx0 = translate_eqs env ctx_init constant_eqs in
403
  assert (VSet.is_empty ctx0.m);
404
  assert (ctx0.si = []);
405
  assert (Utils.IMap.is_empty ctx0.j);
406

  
407
  (* Compute ctx for all eqs *)
408
  let ctx = translate_eqs env ctx_init (assert_instrs@sorted_eqs) in
409
 *)
410 400
  
411
  (*
412
  (* Processing spec: locals would be actual locals of the spec while
413
     non locals would be inputs/ouptpus of the node. Locals of the
414
     node are not visible. *)
415
  let spec =
416
    match nd.node_spec with
417
    | None -> None
418
    | Some spec -> translate_spec inout_vars spec
419
  in
420

  
421

  
422
        inout_vars spec =
423
    let locals = VSet.of_list spec.locals in
424
    let spec_consts = VSet.of_list spec.consts in
425
    let other_spec_vars = VSet.union inout_vars spec_consts in
426
    let spec_env = build_env spec_locals other_spec_vars in
427
   *)             
401
 
428 402
  let mmap = Utils.IMap.elements ctx.j in
429 403
  {
430 404
    mname = nd;
......
454 428
        );
455 429
        step_asserts = List.map (translate_expr env) nd_node_asserts;
456 430
      };
431

  
432
    (* Processing spec: there is no processing performed here. Contract
433
     have been processed already. Either one of the other machine is a
434
     cocospec node, or the current one is a cocospec node. Contract do
435
     not contain any statement or import. *)
436
 
457 437
    mspec = nd.node_spec;
458 438
    mannot = nd.node_annot;
459 439
    msch = Some sch;
......
462 442
(** takes the global declarations and the scheduling associated to each node *)
463 443
let translate_prog decls node_schs =
464 444
  let nodes = get_nodes decls in
465
  List.map
445
  let machines =
446
    List.map
466 447
    (fun decl ->
467 448
     let node = node_of_top decl in
468 449
      let sch = Utils.IMap.find node.node_id node_schs in
469 450
      translate_decl node sch
470 451
    ) nodes
471

  
452
  in
453
  machines
472 454

  
473 455
(* Local Variables: *)
474 456
(* compile-command:"make -C .." *)
src/machine_code.mli
1
val translate_prog: Lustre_types.program_t -> Scheduling_type.schedule_report Utils.IMap.t  -> Machine_code_types.machine_t list
1
val translate_prog:
2
  Lustre_types.program_t ->
3
  Scheduling_type.schedule_report Utils.IMap.t  ->
4
  Machine_code_types.machine_t list
src/machine_code_common.ml
105 105
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.minit
106 106
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.mconst
107 107
    (pp_step m) m.mstep
108
    (fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec)
108
    (fun fmt -> match m.mspec with | None -> ()
109
                                   | Some (NodeSpec id) -> Format.fprintf fmt "cocospec: %s" id
110
                                   | Some (Contract spec) -> Printers.pp_spec fmt spec)
109 111
    (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
110 112

  
111 113
let pp_machines fmt ml =
......
190 192
    node_dec_stateless = true;
191 193
    node_stateless = Some true;
192 194
    node_spec = None;
193
    node_annot = [];  }
195
    node_annot = [];
196
    node_iscontract = false;
197
}
194 198

  
195 199
let empty_machine =
196 200
  {
src/machine_code_types.ml
30 30
  | MBranch of value_t * (label * instr_t list) list
31 31
  | MComment of string
32 32

  
33
      type step_t = {
34
  step_checks: (Location.t * value_t) list;
35
  step_inputs: var_decl list;
36
  step_outputs: var_decl list;
37
  step_locals: var_decl list;
38
  step_instrs: instr_t list;
39
  step_asserts: value_t list;
40
}
33
type step_t = {
34
    step_checks: (Location.t * value_t) list;
35
    step_inputs: var_decl list;
36
    step_outputs: var_decl list;
37
    step_locals: var_decl list;
38
    step_instrs: instr_t list;
39
    step_asserts: value_t list;
40
  }
41 41

  
42 42
type static_call = top_decl * (Dimension.dim_expr list)
43 43

  
44
                 
44
  
45 45
type machine_t = {
46 46
  mname: node_desc;
47 47
  mmemory: var_decl list;
......
51 51
  mstatic: var_decl list; (* static inputs only *)
52 52
  mconst: instr_t list; (* assignments of node constant locals *)
53 53
  mstep: step_t;
54
  mspec: contract_desc option;
54
  mspec: node_spec_t option;
55 55
  mannot: expr_annot list;
56 56
  msch: Scheduling_type.schedule_report option; (* Equations scheduling *)
57 57
}
src/modules.ml
49 49
    let itf = value.top_decl_itf in
50 50
    match value'.top_decl_desc, value.top_decl_desc with
51 51
    | ImportedNode _, Node _          when owner = owner' && itf' && (not itf) -> ()
52
    | Node _        , Node _                    -> raise (Error (value.top_decl_loc, Error.Already_bound_symbol ("node " ^ name)))
52
    | Node _        , Node _                    -> assert false; raise (Error (value.top_decl_loc, Error.Already_bound_symbol ("node " ^ name)))
53 53
    | _                                         -> assert false
54 54
  with
55 55
    Not_found                                   -> update_node name value
src/normalization.ml
554 554

  
555 555
(* We use node local vars to make sure we are creating fresh variables *) 
556 556
let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =  
557
  (* Original set of variables actually visible from here: iun/out and
557
  (* Original set of variables actually visible from here: in/out and
558 558
     spec locals (no node locals) *)
559 559
  let orig_vars = in_vars @ out_vars @ s.locals in
560 560
  let not_is_orig_var v =
......
593 593
  in
594 594
  
595 595
  let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
596
   
597
      
596
  new_locals, defs,      
598 597
  {s with
599 598
    locals = s.locals @ new_locals;
600
    stmts = List.map (fun eq -> Eq eq) defs;
599
    stmts = [];
601 600
    assume = assume';
602 601
    guarantees = guarantees';
603 602
    modes = modes'
......
644 643
      is_output = (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
645 644
    }
646 645
  in
647
  
646

  
647
  let eqs, auts = get_node_eqs node in
648
  if auts != [] then assert false; (* Automata should be expanded by now. *)
649
  let spec, new_vars, eqs =
650
    begin
651
      (* Update mutable fields of eexpr to perform normalization of
652
	 specification.
653

  
654
	 Careful: we do not normalize annotations, since they can have the form
655
	 x = (a, b, c) *)
656
      match node.node_spec with
657
      | None 
658
        | Some (NodeSpec _) -> node.node_spec, [], eqs
659
      | Some (Contract s) ->
660
         let new_locals, new_stmts, s' = normalize_spec
661
                    decls
662
                    node.node_id
663
                    (node.node_inputs, node.node_outputs, node.node_locals)
664
                    s
665
         in
666
         Some (Contract s'), new_locals, new_stmts@eqs
667
    end
668
  in
648 669
  let defs, vars =
649
    let eqs, auts = get_node_eqs node in
650
    if auts != [] then assert false; (* Automata should be expanded by now. *)
651
    List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in
670
    List.fold_left (normalize_eq norm_ctx) ([], new_vars@orig_vars) eqs in
652 671
  (* Normalize the asserts *)
653 672
  let vars, assert_defs, asserts =
654 673
    List.fold_left (
655
      fun (vars, def_accu, assert_accu) assert_ ->
674
        fun (vars, def_accu, assert_accu) assert_ ->
656 675
	let assert_expr = assert_.assert_expr in
657 676
	let (defs, vars'), expr = 
658 677
	  normalize_expr 
......
662 681
	    ([], vars) (* defvar only contains vars *)
663 682
	    assert_expr
664 683
	in
665
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
684
        (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
666 685
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
667
    ) (vars, [], []) node.node_asserts in
686
      ) (vars, [], []) node.node_asserts in
668 687
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
669 688
							  vars and initial locals ones *)
670 689
  
......
679 698
  (* Compute traceability info:
680 699
     - gather newly bound variables
681 700
     - compute the associated expression without aliases
682
  *)
701
   *)
683 702
  let new_annots =
684 703
    if !Options.traces then
685 704
      begin
686 705
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
687 706
	let norm_traceability = {
688
	  annots = List.map (fun v ->
689
	    let eq =
690
	      try
691
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
692
	      with Not_found -> 
693
		(
694
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
695
		  assert false
696
		) 
697
	    in
698
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
699
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
700
	    Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
701
	    (["traceability"], pair)
702
	  ) diff_vars;
703
	  annot_loc = Location.dummy_loc
704
	}
707
	    annots = List.map (fun v ->
708
	                 let eq =
709
	                   try
710
		             List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
711
	                   with Not_found -> 
712
		             (
713
		               Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
714
		               assert false
715
		             ) 
716
	                 in
717
	                 let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
718
	                 let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
719
	                 Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
720
	                 (["traceability"], pair)
721
	               ) diff_vars;
722
	    annot_loc = Location.dummy_loc
723
	  }
705 724
	in
706 725
	norm_traceability::node.node_annot
707 726
      end
......
711 730

  
712 731
  let new_annots =
713 732
    List.fold_left (fun annots v ->
714
      if Machine_types.is_active && Machine_types.is_exportable v then
715
	let typ = Machine_types.get_specified_type v in
716
  	let typ_name = Machine_types.type_name typ in
717

  
718
	let loc = v.var_loc in
719
	let typ_as_string =
720
	  mkexpr
721
	    loc
722
	    (Expr_const
723
	       (Const_string typ_name))
724
	in
725
	let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
726
	Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
727
	{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
728
      else
729
	annots
730
    ) new_annots new_locals
731
  in
732
  let spec =
733
    begin
734
      (* Update mutable fields of eexpr to perform normalization of
735
	 specification.
736

  
737
	 Careful: we do not normalize annotations, since they can have the form
738
	 x = (a, b, c) *)
739
      match node.node_spec with None -> None | Some s -> Some (normalize_spec decls node.node_id (node.node_inputs, node.node_outputs, node.node_locals) s) 
740
    end
733
        if Machine_types.is_active && Machine_types.is_exportable v then
734
	  let typ = Machine_types.get_specified_type v in
735
  	  let typ_name = Machine_types.type_name typ in
736

  
737
	  let loc = v.var_loc in
738
	  let typ_as_string =
739
	    mkexpr
740
	      loc
741
	      (Expr_const
742
	         (Const_string typ_name))
743
	  in
744
	  let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
745
	  Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
746
	  {annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
747
        else
748
	  annots
749
      ) new_annots new_locals
741 750
  in
742 751
  
743 752
  
......
750 759
      node_spec = spec;
751 760
    }
752 761
  in ((*Printers.pp_node Format.err_formatter node;*)
753
    node
754
  )
762
      node
763
    )
755 764

  
756 765
let normalize_inode decls nd =
757 766
  reset_cpt_fresh ();
758 767
  match nd.nodei_spec with
759
    None -> nd
760
  | Some s ->
761
     let s = normalize_spec decls nd.nodei_id (nd.nodei_inputs, nd.nodei_outputs, []) s in
762
     { nd with nodei_spec = Some s }
763
  
768
    None | Some (NodeSpec _) -> nd
769
    | Some (Contract _) -> assert false
770
                         
764 771
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
765 772
  match decl.top_decl_desc with
766 773
  | Node nd ->
src/parsers/lexerLustreSpec.mll
40 40
  "tel", TEL;
41 41
  "returns", RETURNS;
42 42
  "var", VAR;
43
  "import", IMPORT;
43 44
  "imported", IMPORTED;
44 45
  "int", TINT;
45 46
  "bool", TBOOL;
src/parsers/lexer_lustre.mll
41 41
  "returns", RETURNS;
42 42
  "var", VAR;
43 43
  "imported", IMPORTED;
44
  "import", IMPORT;
44 45
  "type", TYPE;
45 46
  "int", TINT;
46 47
  "bool", TBOOL;
src/parsers/parserLustreSpec.mly
95 95
    { Guarantees($2)::$4 }
96 96
| MODE ident LPAR mode_content RPAR SCOL contract
97 97
    { Mode($2,$4)::$7 }	
98
| IMPORT ident LPAR tuple_expr RPAR returns LPAR tuple_expr RPAR SCOL contract
98
| IMPORT ident LPAR expr RPAR returns LPAR expr RPAR SCOL contract
99 99
    { Import($2, $4, $8)::$11 }
100 100
	
101 101

  
src/parsers/parser_lustre.mly
49 49
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr)))
50 50
  else
51 51
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n-1) init))))
52
  
52

  
53
 
53 54
%}
54 55

  
55 56
%token <int> INT
......
62 63
%token <string> UIDENT
63 64
%token TRUE FALSE
64 65
%token <Lustre_types.expr_annot> ANNOT
65
%token <Lustre_types.contract_desc> NODESPEC
66
%token <Lustre_types.spec_types> NODESPEC
66 67
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
67 68
%token AMPERAMPER BARBAR NOT POWER
68 69
%token IF THEN ELSE
......
113 114
%type <Lustre_types.expr_annot> lustre_annot
114 115

  
115 116
%start lustre_spec
116
%type <Lustre_types.contract_desc> lustre_spec
117
%type <Lustre_types.spec_types> lustre_spec
117 118

  
118 119
%start signed_const
119 120
%type <Lustre_types.constant> signed_const
......
203 204

  
204 205
top_decl_header:
205 206
| CONST cdecl_list { List.rev ($2 true) }
206
| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR  prototype_opt in_lib_list SCOL
207
    {let nd = mktop_decl true (ImportedNode
207
| nodespecs state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR  prototype_opt in_lib_list SCOL
208
    {
209
      let inputs = List.rev $5 in
210
      let outputs = List.rev $10 in
211
      let nd = mktop_decl true (ImportedNode
208 212
				 {nodei_id = $3;
209 213
				  nodei_type = Types.new_var ();
210 214
				  nodei_clock = Clocks.new_var true;
211
				  nodei_inputs = List.rev $5;
212
				  nodei_outputs = List.rev $10;
215
				  nodei_inputs = inputs;
216
				  nodei_outputs = outputs;
213 217
				  nodei_stateless = $2;
214 218
				  nodei_spec = $1;
215 219
				  nodei_prototype = $13;
216 220
				  nodei_in_lib = $14;})
217 221
     in
218
     (*add_imported_node $3 nd;*) [nd] } 
219
| CONTRACT node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract TEL 
220
    {let nd = mktop_decl true (ImportedNode
221
				 {nodei_id = $2;
222
				  nodei_type = Types.new_var ();
223
				  nodei_clock = Clocks.new_var true;
224
				  nodei_inputs = List.rev $4;
225
				  nodei_outputs = List.rev $9;
226
				  nodei_stateless = false (* By default we assume contracts as stateful *);
227
				  nodei_spec = Some $14;
228
				  nodei_prototype = None;
229
				  nodei_in_lib = [];})
230
     in
231
     (*add_imported_node $3 nd;*) [nd] }
222
     pop_node ();
223
     [nd] } 
224
| top_contract { [$1] }
225

  
232 226

  
233 227
prototype_opt:
234 228
 { None }
......
240 234

  
241 235
top_decl:
242 236
| CONST cdecl_list { List.rev ($2 false) }
243
| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespec_list locals LET stmt_list TEL 
237
| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespecs locals LET stmt_list TEL 
244 238
    {
245 239
     let stmts, asserts, annots = $16 in
246 240
      (* Declaring eqs annots *)
......
249 243
	  Annotations.add_node_ann $2 key
250 244
	) ann.annots
251 245
      ) annots;
252
     (* Building the node *)
246
      (* Building the node *)
247
      let inputs = List.rev $4 in
248
      let outputs = List.rev $9 in
253 249
     let nd = mktop_decl false (Node
254 250
				  {node_id = $2;
255 251
				   node_type = Types.new_var ();
256 252
				   node_clock = Clocks.new_var true;
257
				   node_inputs = List.rev $4;
258
				   node_outputs = List.rev $9;
253
				   node_inputs = inputs;
254
				   node_outputs = outputs;
259 255
				   node_locals = List.rev $14;
260 256
				   node_gencalls = [];
261 257
				   node_checks = [];
......
264 260
				   node_dec_stateless = $1;
265 261
				   node_stateless = None;
266 262
				   node_spec = $13;
267
				   node_annot = annots})
263
				   node_annot = annots;
264
				   node_iscontract = false;
265
			       })
268 266
     in
269 267
     pop_node ();
270 268
     (*add_node $3 nd;*) [nd] }
271 269

  
272
| state_annot IMPORTED node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract TEL
273
    {let nd = mktop_decl true (ImportedNode
274
				 {nodei_id = $3;
275
				  nodei_type = Types.new_var ();
276
				  nodei_clock = Clocks.new_var true;
277
				  nodei_inputs = List.rev $5;
278
				  nodei_outputs = List.rev $10;
279
				  nodei_stateless = $1;
280
				  nodei_spec = Some $15;
281
				  nodei_prototype = None;
282
				  nodei_in_lib = [];})
283
     in
284
     pop_node ();
285
     (*add_imported_node $3 nd;*) [nd] } 
286
| state_annot IMPORTED node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
287
    {let nd = mktop_decl true (ImportedNode
288
				 {nodei_id = $3;
289
				  nodei_type = Types.new_var ();
290
				  nodei_clock = Clocks.new_var true;
291
				  nodei_inputs = List.rev $5;
292
				  nodei_outputs = List.rev $10;
293
				  nodei_stateless = $1;
294
				  nodei_spec = None;
295
				  nodei_prototype = None;
296
				  nodei_in_lib = [];})
297
     in
298
     pop_node ();
299
     (*add_imported_node $3 nd;*) [nd] } 
270

  
271
| NODESPEC
272
    { match $1 with
273
      | LocalContract c -> assert false
274
      | TopContract c   -> c
275
			 
276
    }
277

  
278
nodespecs:
279
nodespec_list {
280
  match $1 with
281
  | None -> None 
282
  | Some c -> Some (Contract c)
283
}
300 284

  
301 285
nodespec_list:
302 286
 { None }
303
| NODESPEC nodespec_list { 
304
  (function 
305
  | None    -> (fun s1 -> Some s1) 
306
  | Some s2 -> (fun s1 -> Some (merge_contracts s1 s2))) $2 $1 }
287
  | NODESPEC nodespec_list {
288
	       let extract x = match x with LocalContract c -> c | _ -> assert false in
289
	       let s1 = extract $1 in
290
	       match $2 with
291
	       | None -> Some s1
292
	       | Some s2 -> Some (merge_contracts s1 s2) }
307 293

  
308 294
typ_def_list:
309 295
    /* empty */             { (fun itf -> []) }
......
382 368
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
383 369

  
384 370
lustre_spec:
385
| contract EOF { $1 }
371
| top_contracts EOF     { TopContract $1 }
372
| contract_content EOF { LocalContract $1}
373

  
374
top_contracts:
375
| top_contract { [$1] }
376
| top_contract top_contracts { $1::$2 }
377

  
378
top_contract:
379
| CONTRACT node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract_content TEL 
380
    {
381
      let nd = mktop_decl true (Node
382
				 {node_id = $2;
383
				  node_type = Types.new_var ();
384
				  node_clock = Clocks.new_var true;
385
				  node_inputs = List.rev $4;
386
				  node_outputs = List.rev $9;
387
				  node_locals = []; (* will be filled later *)
388
				  node_gencalls = [];
389
				  node_checks = [];
390
				  node_asserts = [];
391
				  node_stmts = []; (* will be filled later *)
392
				  node_dec_stateless = false;
393
				  (* By default we assume contracts as stateful *)
394
				  node_stateless = None;
395
				  node_spec = Some (Contract $14);
396
				  node_annot = [];
397
				  node_iscontract = true;
398
				 }
399
			       )
400
     in
401
     pop_node ();
402
     (*add_imported_node $3 nd;*)
403
     nd }
386 404

  
387
contract:
405
contract_content:
388 406
{ empty_contract }
389
| CONTRACT contract { $2 }
390
| CONST IDENT EQ expr SCOL contract
407
| CONTRACT contract_content { $2 }
408
| CONST IDENT EQ expr SCOL contract_content
391 409
    { merge_contracts (mk_contract_var $2 true None $4 (get_loc())) $6 }
392
| CONST IDENT COL typeconst EQ expr SCOL contract
410
| CONST IDENT COL typeconst EQ expr SCOL contract_content
393 411
    { merge_contracts (mk_contract_var $2 true (Some(mktyp $4)) $6 (get_loc())) $8 }
394
| VAR IDENT COL typeconst EQ expr SCOL contract
412
| VAR IDENT COL typeconst EQ expr SCOL contract_content
395 413
    { merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 }
396
| ASSUME qexpr SCOL contract
414
| ASSUME qexpr SCOL contract_content
397 415
    { merge_contracts (mk_contract_assume $2) $4 }
398
| GUARANTEES qexpr SCOL contract	
416
| GUARANTEES qexpr SCOL contract_content	
399 417
    { merge_contracts (mk_contract_guarantees $2) $4 }
400
| MODE IDENT LPAR mode_content RPAR SCOL contract
418
| MODE IDENT LPAR mode_content RPAR SCOL contract_content
401 419
	{ merge_contracts (
402 420
	  let r, e = $4 in 
403 421
	  mk_contract_mode $2 r e (get_loc())) $7 }	
404
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract
422
| IMPORT IDENT LPAR expr RPAR RETURNS LPAR expr RPAR SCOL contract_content
405 423
    { merge_contracts (mk_contract_import $2  $4  $8 (get_loc())) $11 }
406 424

  
407 425
mode_content:
src/printers.ml
323 323
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt import ->
324 324
    fprintf fmt "import %s (%a) returns (%a);" 
325 325
      import.import_nodeid
326
      (fprintf_list ~sep:"@ " pp_expr) import.inputs
327
      (fprintf_list ~sep:"@ " pp_expr) import.outputs
326
      pp_expr import.inputs
327
      pp_expr import.outputs
328 328
  ) fmt spec.imports
329 329

  
330
let pp_spec_as_comment fmt spec =
331
  fprintf fmt "@[<hov 2>(*@@ ";
332
  pp_spec fmt spec;
333
  fprintf fmt "@]*)@ "
330

  
331
  let node_as_contract nd =
332
  match nd.node_spec with
333
  | None | Some (NodeSpec _) -> raise (Invalid_argument "Not a contract")
334
  | Some (Contract c) -> (
335
    assert (c.locals = []);
336
    assert (c.stmts = []);
337
    { c with
338
      locals = nd.node_locals;
339
      stmts = nd.node_stmts;
340
    }
341
  )
342

  
343
let pp_contract fmt nd =    
344
  let c = node_as_contract nd in
345
  let pp_l = fprintf_list ~sep:"," pp_var_name in
346
  fprintf fmt "@[<hov 2>(*@@ contract %s(%a) returns (%a);@ "
347
    nd.node_id
348
    pp_l nd.node_inputs
349
    pp_l nd.node_outputs;
350
  fprintf fmt "let@ ";
351
  pp_spec fmt c;
352
  fprintf fmt "tel@ @]*)@ "        
334 353
    
354
let pp_spec_as_comment fmt (inl, outl, spec) =
355
  match spec with
356
  | Contract c -> (* should have been processed by now *)
357
     fprintf fmt "@[<hov 2>(*@@ ";
358
     pp_spec fmt c;
359
     fprintf fmt "@]*)@ "
360
     
361
  | NodeSpec name -> (* Pushing stmts in contract. We update the
362
                      original information with the computed one in
363
                      nd. *)
364
     let pp_l = fprintf_list ~sep:"," pp_var_name in
365
     fprintf fmt "@[<hov 2>(*@@ contract import %s(%a) returns (%a)@]*)@ "
366
       name
367
       pp_l inl
368
       pp_l outl
369
     
370
              
335 371
let pp_node fmt nd =
336 372
  fprintf fmt "@[<v 0>";
337 373
  (* Prototype *)
......
342 378
    pp_node_args nd.node_outputs;
343 379
  (* Contracts *)
344 380
  fprintf fmt "%a%t"
345
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt s | _ -> ()) nd.node_spec
381
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s) | _ -> ()) nd.node_spec
346 382
    (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ");
347 383
  (* Locals *)
348 384
  fprintf fmt "%a" (fun fmt locals ->
......
375 411

  
376 412
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
377 413

  
414
let pp_node fmt nd =
415
  match nd.node_spec, nd.node_iscontract with
416
  | None, false
417
    | Some (NodeSpec _), false 
418
    -> pp_node fmt nd
419
  | Some (Contract _), false -> pp_node fmt nd (* may happen early in the compil process *)
420
  | Some (Contract _), true -> pp_contract fmt nd 
421
  | _ -> assert false
422
     
378 423
let pp_imported_node fmt ind = 
379 424
  fprintf fmt "@[<v 0>";
380 425
  (* Prototype *)
......
385 430
    pp_node_args ind.nodei_outputs;
386 431
  (* Contracts *)
387 432
  fprintf fmt "%a%t"
388
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt s | _ -> ()) ind.nodei_spec
433
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (ind.nodei_inputs, ind.nodei_outputs, s) | _ -> ()) ind.nodei_spec
389 434
    (fun fmt -> match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
390 435
  fprintf fmt "@]@ "
391 436
  
src/scheduling.ml
113 113
   let vdecl = get_node_var v n in
114 114
   if vdecl.var_orig then v :: res else res) vl []
115 115

  
116
let eq_equiv eq_equiv_hash =
117
  fun v1 v2 ->
118
  try
119
    Hashtbl.find eq_equiv_hash v1 = Hashtbl.find eq_equiv_hash v2
120
  with Not_found -> false
121

  
116 122
let schedule_node n =
117 123
  (* let node_vars = get_node_vars n in *)
118
  let eq_equiv = ExprDep.node_eq_equiv n in
119
  let eq_equiv v1 v2 =
120
    try
121
      Hashtbl.find eq_equiv v1 = Hashtbl.find eq_equiv v2
122
    with Not_found -> false in
124
  let eq_equiv = eq_equiv (ExprDep.node_eq_equiv n) in
123 125

  
124 126
  let n', g = global_dependency n in
125 127
  
......
135 137
  let fanin = Liveness.compute_fanin n gg in
136 138
  { node = n'; schedule = sort; unused_vars = unused; fanin_table = fanin; dep_graph = gg; }
137 139

  
140
(* let schedule_eqs eqs =
141
 *   let eq_equiv = eq_equiv (ExprDep.eqs_eq_equiv eqs) in
142
 *   assert false (\* TODO: continue to implement scheduling of eqs for spec *\) *)
138 143

  
139 144
let compute_node_reuse_table report =
140 145
  let disjoint = Disjunction.clock_disjoint_map (get_node_vars report.node) in
src/tools/stateflow/semantics/cPS_lustre_generator.ml
345 345
			   node_dec_stateless = false;
346 346
			   node_stateless = None;
347 347
			   node_spec = None;
348
			   node_annot = []}
348
			   node_annot = [];
349
                           node_iscontract = false}
349 350
      )  
350 351
	in
351 352
	[node]
......
400 401
			 node_dec_stateless = false;
401 402
			 node_stateless = None;
402 403
			 node_spec = None;
403
			 node_annot = []}
404
			 node_annot = [];
405
                         node_iscontract = false;}
404 406
      )  
405 407
    in
406 408
    node_principal
src/typing.ml
669 669
    let check_vd_env vd_env =
670 670
      ignore (List.fold_left add_vdecl [] vd_env)
671 671

  
672
    let type_spec env spec =
673
      let vd_env = spec.consts @ spec.locals in
672
    let type_contract env c =
673
      let vd_env = c.consts @ c.locals in
674 674
      check_vd_env vd_env;
675 675
      let env = type_var_decl_list ((* this argument seems useless to me, cf TODO at top of the file*) vd_env) env vd_env in
676 676
      (* typing stmts *)
677
      let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) spec.stmts  in
677
      let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) c.stmts  in
678 678
      let undefined_vars_init =
679 679
        List.fold_left
680 680
          (fun uvs v -> ISet.add v.var_id uvs)
681
          ISet.empty spec.locals
681
          ISet.empty c.locals
682 682
      in
683 683
      let _ =
684 684
        List.fold_left
......
692 692
      in
693 693
      List.iter type_pred_ee
694 694
        (
695
          spec.assume 
696
          @ spec.guarantees
697
          @ List.flatten (List.map (fun m -> m.ensure @ m.require) spec.modes) 
695
          c.assume 
696
          @ c.guarantees
697
          @ List.flatten (List.map (fun m -> m.ensure @ m.require) c.modes) 
698 698
        );
699 699
      (*TODO 
700 700
        enrich env locally with locals and consts
......
703 703
        For the moment, returning the provided env           
704 704
       *)
705 705
      env
706
      
706

  
707
    let rec type_spec env spec loc =
708
      match spec with
709
      | Contract c -> type_contract env c
710
      | NodeSpec id -> env
711
                     
707 712
    (** [type_node env nd loc] types node [nd] in environment env. The
708 713
    location is used for error reports. *)
709
    let type_node env nd loc =
714
    and type_node env nd loc =
710 715
      let is_main = nd.node_id = !Options.main_node in
711
      let vd_env_ol = nd.node_outputs@nd.node_locals in
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff