Revision 59020713 src/normalization.ml
src/normalization.ml  

170  170 
then 
171  171 
let new_aliases = 
172  172 
List.map2 
173 
(mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) expr.expr_loc)


173 
(mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc)


174  174 
(Types.type_list_of_type expr.expr_type) 
175  175 
(Clocks.clock_list_of_clock expr.expr_clock) in 
176  176 
let new_def = 
177  177 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
178  178 
in 
179  179 
(* Typing and Registering machine type *) 
180 
let _ = if Machine_types.is_active then Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr in 

180 
let _ = if Machine_types.is_active then 

181 
Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr 

182 
in 

181  183 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
182  184 
else 
183  185 
(defs, vars), expr 
...  ...  
400  402 
let normalize_eq_split norm_ctx defvars eq = 
401  403 
try 
402  404 
let defs, vars = normalize_eq norm_ctx defvars eq in 
403 
List.fold_right (fun eq (def, vars) > 

404 
let eq_defs = Splitting.tuple_split_eq eq in 

405 
if eq_defs = [eq] then 

406 
eq::def, vars 

407 
else 

408 
List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs 

409 
) defs ([], vars) 

410  
411 
with _ > (


405 
List.fold_right (fun eq (def, vars) >


406 
let eq_defs = Splitting.tuple_split_eq eq in


407 
if eq_defs = [eq] then


408 
eq::def, vars


409 
else


410 
List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs


411 
) defs ([], vars)


412 


413 
with ex > (


412  414 
Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq; 
413 
assert false


415 
raise ex


414  416 
) 
415  417  
416 
let normalize_eexpr decls norm_ctx vars ee = ee (* 

417 
(* New output variable *) 

418 
let output_id = "spec" ^ string_of_int ee.eexpr_tag in 

419 
let output_var = 

420 
mkvar_decl 

421 
ee.eexpr_loc 

422 
(output_id, 

423 
mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *) 

424 
mkclock ee.eexpr_loc Ckdec_any, 

425 
false (* not a constant *), 

426 
None, 

427 
None 

428 
) 

418 
(* Projecting an eexpr to an eexpr associated to a single 

419 
variable. Returns the updated ee, the bounded variable and the 

420 
associated statement *) 

421 
let normalize_pred_eexpr decls norm_ctx (def,vars) ee = 

422 
assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *) 

423 
(* don't do anything is eexpr is just a variable *) 

424 
let skip = 

425 
match ee.eexpr_qfexpr.expr_desc with 

426 
 Expr_ident _  Expr_const _ > true 

427 
 _ > false 

429  428 
in 
429 
if skip then 

430 
ee, (def, vars) 

431 
else ( 

432 
(* New output variable *) 

433 
let output_id = "spec" ^ string_of_int ee.eexpr_tag in 

434 
let output_var = 

435 
mkvar_decl 

436 
ee.eexpr_loc 

437 
(output_id, 

438 
mktyp ee.eexpr_loc Tydec_bool, (* It is a predicate, hence a bool *) 

439 
mkclock ee.eexpr_loc Ckdec_any, 

440 
false (* not a constant *), 

441 
None, 

442 
None 

443 
) 

444 
in 

445 
let output_expr = expr_of_vdecl output_var in 

446 
(* Rebuilding an eexpr with a silly expression, just a variable *) 

447 
let ee' = { ee with eexpr_qfexpr = output_expr } in 

448  
449 
(* Now processing a fresh equation output_id = eexpr_qfexpr. We 

450 
inline possible calls within, normalize it and type/clock the 

451 
result. *) 

452 
let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in 

453 
(* Inlining any calls *) 

454 
let nodes = get_nodes decls in 

455 
let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in 

456 
let vars, eqs = 

457 
if calls = [] && not (eq_has_arrows eq) then 

458 
vars, [eq] 

459 
else 

460 
assert false (* TODO *) 

461 
in 

462 


463 
(* Normalizing expr and eqs *) 

464 
let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) eqs in 

465 
(* let todefine = 

466 
List.fold_left 

467 
(fun m x> if List.exists (fun y> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m) 

468 
(ISet.add output_id ISet.empty) vars in 

469 
*) 

470  
471 
(* Typing / Clocking *) 

472 
try 

473 
ignore (Typing.type_var_decl_list vars !Global.type_env vars); 

474 
(* 

475 
let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *) 

476 
(* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *) 

477 
let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in 

478 
(*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*) 

479 
let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in 

480 
(* check that table is empty *) 

481 
if (not (ISet.is_empty undefined_vars)) then 

482 
raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars)); 

483 


484 
(*Format.eprintf "normalized eqs %a@.@?" 

485 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *) 

486 
*) 

487  
488 
ee', (defs, vars) 

489 


490 
with (Types.Error (loc,err)) as exc > 

491 
eprintf "Typing error for eexpr %a: %a%a%a@." 

492 
Printers.pp_eexpr ee 

493 
Types.pp_error err 

494 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs 

495 
Location.pp_loc loc 

496 


497 


498 
; 

499 
raise exc 

500 


501 
) 

502 


503 
(* 

430  504 

431  505 
let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in 
432  506 
(* Calls are first inlined *) 
433 
let nodes = get_nodes decls in 

434 
let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in 

435 
(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes 

436 
let calls = List.map 

437 
(fun called_nd > List.find (fun nd2 > nd2.node_id = called_nd) nodes) calls 

438 
in 

439 
*) 

507 


440  508 
(*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; *) 
441 
let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in 

442 
let locals = node.node_locals @ (List.fold_left (fun accu (_, q) > q@accu) [] ee.eexpr_quantifiers) in 

443  509 
let (new_locals, eqs) = 
444  510 
if calls = [] && not (eq_has_arrows eq) then 
445  511 
(locals, [eq]) 
...  ...  
485  551 
raise exc 
486  552 
*) 
487  553 

488 


489 
let normalize_spec decls iovars s = s (* 

490 
(* Each stmt is normalized *) 

491 
let orig_vars = iovars @ s.locals in 

554  
555 
(* We use node local vars to make sure we are creating fresh variables *) 

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 

558 
spec locals (no node locals) *) 

559 
let orig_vars = in_vars @ out_vars @ s.locals in 

492  560 
let not_is_orig_var v = 
493  561 
List.for_all ((!=) v) orig_vars in 
494 
let defs, vars = 

495 
let eqs, auts = List.fold_right (fun (el,al) s > match s with Eq e > e::el, al  Aut a > el, a::al) s.stmts ([], []) in 

496 
if auts != [] then assert false; (* Automata should be expanded by now. *) 

497 
List.fold_left (normalize_eq node) ([], orig_vars) eqs 

562 
let norm_ctx = { 

563 
parentid = parentid; 

564 
vars = in_vars @ out_vars @ l_vars; 

565 
is_output = (fun _ > false) (* no need to introduce fresh variables for outputs *); 

566 
} 

567 
in 

568 
(* Normalizing existing stmts *) 

569 
let eqs, auts = List.fold_right (fun s (el,al) > match s with Eq e > e::el, al  Aut a > el, a::al) s.stmts ([], []) in 

570 
if auts != [] then assert false; (* Automata should be expanded by now. *) 

571 
let defsvars = 

572 
List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs 

573 
in 

574 
(* Iterate through predicates and normalize them on the go, creating 

575 
fresh variables for any guarantees/assumes/require/ensure *) 

576 
let process_predicates l defvars = 

577 
List.fold_right (fun ee (accu, defvars) > 

578 
let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in 

579 
ee'::accu, defvars 

580 
) l ([], defvars) 

498  581 
in 
499 
let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *) 

500  582  
501 
(* 

583 


584 
let assume', defsvars = process_predicates s.assume defsvars in 

585 
let guarantees', defsvars = process_predicates s.guarantees defsvars in 

586 
let modes', (defs, vars) = 

587 
List.fold_right ( 

588 
fun m (accu_m, defsvars) > 

589 
let require', defsvars = process_predicates m.require defsvars in 

590 
let ensure', defsvars = process_predicates m.ensure defsvars in 

591 
{ m with require = require'; ensure = ensure' }:: accu_m, defsvars 

592 
) s.modes ([], defsvars) 

593 
in 

594 


595 
let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *) 

596 


502  597 

503  598 
{s with 
504  599 
locals = s.locals @ new_locals; 
505  600 
stmts = List.map (fun eq > Eq eq) defs; 
506 
let nee _ = () in 

507 
(*normalize_eexpr decls iovars in *) 

508 
List.iter nee s.assume; 

509 
List.iter nee s.guarantees; 

510 
List.iter (fun m > 

511 
List.iter nee m.require; 

512 
List.iter nee m.ensure 

513 
) s.modes; 

514 
*) 

515 
s 

516 
*) 

601 
assume = assume'; 

602 
guarantees = guarantees'; 

603 
modes = modes' 

604 
} 

605 
(* let nee _ = () in 

606 
* (\*normalize_eexpr decls iovars in *\) 

607 
* List.iter nee s.assume; 

608 
* List.iter nee s.guarantees; 

609 
* List.iter (fun m > 

610 
* List.iter nee m.require; 

611 
* List.iter nee m.ensure 

612 
* ) s.modes; *) 

613 


614  
615 


616 


617 


517  618 

518  619 
(* The normalization phase introduces new local variables 
519  620 
 output cannot be memories. If this happen, new local variables acting as 
...  ...  
534  635 
*) 
535  636 
let normalize_node decls node = 
536  637 
reset_cpt_fresh (); 
537 
let inputs_outputs = node.node_inputs@node.node_outputs in 

538 
let orig_vars = inputs_outputs@node.node_locals in 

638 
let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in 

539  639 
let not_is_orig_var v = 
540  640 
List.for_all ((!=) v) orig_vars in 
541  641 
let norm_ctx = { 
...  ...  
636  736  
637  737 
Careful: we do not normalize annotations, since they can have the form 
638  738 
x = (a, b, c) *) 
639 
match node.node_spec with None > None  Some s > Some (normalize_spec decls inputs_outputs s)


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)


640  740 
end 
641  741 
in 
642  742 

...  ...  
658  758 
match nd.nodei_spec with 
659  759 
None > nd 
660  760 
 Some s > 
661 
let inputs_outputs = nd.nodei_inputs@nd.nodei_outputs in 

662 
let s = normalize_spec decls inputs_outputs s in 

761 
let s = normalize_spec decls nd.nodei_id (nd.nodei_inputs, nd.nodei_outputs, []) s in 

663  762 
{ nd with nodei_spec = Some s } 
664  763 

665  764 
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl = 
Also available in: Unified diff