Project

General

Profile

Revision 949b2e1e src/normalization.ml

View differences:

src/normalization.ml
369 369
    let norm_eq = { eq with eq_rhs = norm_rhs } in
370 370
    norm_eq::defs', vars'
371 371

  
372
(** normalize_node node returns a normalized node,
373
    ie.
372
let normalize_eq_split node defvars eq =
373
  
374
  let defs, vars = normalize_eq node defvars eq in
375
  List.fold_right (fun eq (def, vars) -> 
376
    let eq_defs = Splitting.tuple_split_eq eq in
377
    if eq_defs = [eq] then
378
      eq::def, vars 
379
    else
380
      List.fold_left (normalize_eq node) (def, vars) eq_defs
381
  ) defs ([], vars)  
382

  
383
let normalize_eexpr decls node vars ee =
384
  (* New output variable *)
385
  let output_id = "spec" ^ string_of_int ee.eexpr_tag in
386
  let output_var = 
387
    mkvar_decl 
388
      ee.eexpr_loc 
389
      (output_id, 
390
       mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)
391
       mkclock ee.eexpr_loc Ckdec_any, 
392
       false (* not a constant *),
393
       None,
394
       None
395
      ) 
396
  in
397
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
398
  (* Calls are first inlined *)
399
  let nodes = get_nodes decls in
400
  let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
401
(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes
402
   let calls = List.map 
403
    (fun called_nd -> List.find (fun nd2 -> nd2.node_id = called_nd) nodes) calls 
404
  in
405
*)
406
  (*Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd -> pp_print_string fmt nd.node_id)) calls;  *)
407
  let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
408
  let locals = node.node_locals @ (List.fold_left (fun accu (_, q) -> q@accu) [] ee.eexpr_quantifiers) in  
409
  let (new_locals, eqs) =
410
    if calls = [] && not (eq_has_arrows eq) then
411
      (locals, [eq])     
412
    else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
413
(*      let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
414
      (*Format.eprintf "eqs %a@.@?" 
415
	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
416
      (new_locals, eqs)
417
*)
418
           (locals, [eq])     
419
 
420
    ) in
421
  (* Normalizing expr and eqs *)
422
  let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
423
  let todefine = List.fold_left
424
    (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
425
    (ISet.add output_id ISet.empty) vars in
426
  try
427
    let env = Typing.type_var_decl_list quant_vars Basic_library.type_env quant_vars in
428
    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
429
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
430
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
431
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
432
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
433
  (* check that table is empty *)
434
    if (not (ISet.is_empty undefined_vars)) then
435
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
436
    
437
    (*Format.eprintf "normalized eqs %a@.@?" 
438
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
439
    ee.eexpr_normalized <- Some (output_var, defs, vars)
440
  with (Types.Error (loc,err)) as exc ->
441
    eprintf "Typing error for eexpr %a: %a%a%a@."
442
      Printers.pp_eexpr ee
443
      Types.pp_error err
444
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
445
      Location.pp_loc loc
446
      
447
;
448
    raise exc
449

  
450
let normalize_spec decls node vars s =
451
  let nee = normalize_eexpr decls node vars in
452
  List.iter nee s.requires;
453
  List.iter nee s.ensures;
454
  List.iter (fun (_, assumes, ensures, _) -> 
455
      List.iter nee assumes;
456
    List.iter nee ensures
457
  ) s.behaviors
458
  
459
    
460
(* The normalization phase introduces new local variables
461
   - output cannot be memories. If this happen, new local variables acting as
462
   memories are introduced. 
463
   - array constants, pre, arrow, fby, ite, merge, calls to node with index
464
   access
465
   Thoses values are shared, ie. no duplicate expressions are introduced.
466

  
467
   Concerning specification, a similar process is applied, replacing an
468
   expression by a list of local variables and definitions
469
*)
470

  
471
(** normalize_node node returns a normalized node, 
472
    ie. 
374 473
    - updated locals
375 474
    - new equations
376 475
    -
377 476
*)
378
let normalize_node node =
477
let normalize_node decls node =
379 478
  reset_cpt_fresh ();
380 479
  let inputs_outputs = node.node_inputs@node.node_outputs in
480
  let is_local v =
481
    List.for_all ((<>) v) inputs_outputs in
381 482
  let orig_vars = inputs_outputs@node.node_locals in
382 483
  let not_is_orig_var v =
383 484
    List.for_all ((!=) v) orig_vars in
......
465 566
	annots
466 567
    ) new_annots new_locals
467 568
  in
569
  if !Options.spec <> "no" then 
570
    begin
571
      (* Update mutable fields of eexpr to perform normalization of specification/annotations *)
572
      List.iter 
573
	(fun a -> 
574
	  List.iter 
575
	    (fun (_, ann) -> normalize_eexpr decls node inputs_outputs ann) 
576
	    a.annots
577
	)
578
	node.node_annot;
579
      match node.node_spec with None -> () | Some s -> normalize_spec decls node [] s 
580
    end;
581
  
582
 
583
 let new_locals = List.filter is_local vars in (* TODO a quoi ca sert ? *)
468 584
  let node =
469 585
    { node with
470 586
      node_locals = all_locals;
......
477 593
  )
478 594

  
479 595

  
480
let normalize_decl decl =
596
let normalize_decl (decls: program) (decl: top_decl) : top_decl =
481 597
  match decl.top_decl_desc with
482 598
  | Node nd ->
483
    let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in
599
    let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
484 600
    Hashtbl.replace Corelang.node_table nd.node_id decl';
485 601
    decl'
486 602
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
487 603

  
488
let normalize_prog ?(backend="C") decls =
604
let normalize_prog ?(backend="C") decls : program =
489 605
  let old_unfold_arrow_active = !unfold_arrow_active in
490 606
  let old_force_alias_ite = !force_alias_ite in
491 607
  let old_force_alias_internal_fun = !force_alias_internal_fun in
......
505 621
  in
506 622

  
507 623
  (* Main algorithm: iterates over nodes *)
508
  let res = List.map normalize_decl decls in
624
  let res = List.map (normalize_decl decls) decls in
509 625
  
510 626
  (* Restoring previous settings *)
511 627
  unfold_arrow_active := old_unfold_arrow_active;

Also available in: Unified diff