Revision 2196a0a6 src/machine_code.ml
src/machine_code.ml  

290  290 
(* s : step instructions *) 
291  291 
let translate_ident vars (m, si, j, d, s) id = 
292  292 
try (* id is a node var *) 
293 
Format.eprintf "translate ident: %s@.@?" id;


293 
(* Format.eprintf "translate ident: %s@.@?" id; *)


294  294 
let var_id = try List.find (fun v > v.var_id= id) vars with Not_found > assert false in 
295  295 
if ISet.exists (fun v > v.var_id = id) m 
296  296 
then StateVar var_id 
...  ...  
470  470 

471  471 
*) 
472  472 
let translate_eexpr nd eexpr = 
473 
Format.eprintf "Translating eexpr: %a" Printers.pp_eexpr eexpr;


473 
(* Format.eprintf "Translating eexpr: %a" Printers.pp_eexpr eexpr; *)


474  474 
let output_var, eqs, locals = match eexpr.eexpr_normalized with None > assert false  Some x > x in 
475  475 
(* both inputs and outputs are considered here as inputs for the specification *) 
476  476 
let inputs = nd.node_inputs @ nd.node_outputs in 
...  ...  
481  481 

482  482 
let sort_eqs inputs eqs = 
483  483 
let eqs_logic, new_locals_logic, sch_logic = Scheduling.schedule_eqs inputs visible_vars eqs in 
484 
Format.eprintf "sch: [%a]@;new locals: [%a]@;locals:[%a]@.eexpr local vars: [%a]@.@?"


485 
(Utils.fprintf_list ~sep:", " Format.pp_print_string) sch_logic


486 
(Utils.fprintf_list ~sep:", " Printers.pp_var) new_locals_logic


487 
(Utils.fprintf_list ~sep:", " Printers.pp_var) locals


488 
(Utils.fprintf_list ~sep:", " Printers.pp_var) eexpr_local_vars;


484 
(* Format.eprintf "sch: [%a]@;new locals: [%a]@;locals:[%a]@.eexpr local vars: [%a]@.@?" *)


485 
(* (Utils.fprintf_list ~sep:", " Format.pp_print_string) sch_logic *)


486 
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) new_locals_logic *)


487 
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) locals *)


488 
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) eexpr_local_vars; *)


489  489 
let locals = eexpr_local_vars @ new_locals_logic @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in 
490  490 
let sorted_eqs_rev_logic, remainder_logic = 
491  491 
List.fold_left 
...  ...  
493  493 
if List.exists (fun eq > List.mem v eq.eq_lhs) accu 
494  494 
then (* The variable was already handled by a previous selected eq. 
495  495 
Typically it is part of a tuple *) 
496 
(Format.eprintf "Case 1 for variable %s@." v;


496 
((* Format.eprintf "Case 1 for variable %s@." v; *)


497  497 
(accu, eqs_remainder) 
498  498 
) 
499  499 
else if List.exists (fun vdecl > vdecl.var_id = v) locals  output_var.var_id = v 
500  500 
then ((* Select the eq associated to v. *) 
501 
Format.eprintf "Case 2 for variable %s@." v;


501 
(* Format.eprintf "Case 2 for variable %s@." v; *)


502  502 
let eq_v, remainder = find_eq v eqs_remainder in 
503  503 
eq_v::accu, remainder 
504  504 
) 
505  505 
else ((* else it is a constant value, checked during typing phase *) 
506 
Format.eprintf "Case 3 for variable %s@." v;


506 
(* Format.eprintf "Case 3 for variable %s@." v; *)


507  507 
accu, eqs_remainder 
508  508 
) 
509  509 
) 
...  ...  
523  523 
(* Generating logic definition instructions *) 
524  524 
let sorted_eqs, locals = sort_eqs inputs_quantifiers eqs in 
525  525  
526 


527 
(* let eqs_logic, new_locals_logic, sch_logic = Scheduling.schedule_eqs inputs visible_vars eqs in *) 

528 
(* Format.eprintf "sch: [%a]@;new locals: [%a]@;locals:[%a]@.eexpr local vars: [%a]@.@?" *) 

529 
(* (Utils.fprintf_list ~sep:", " Format.pp_print_string) sch_logic *) 

530 
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) new_locals_logic *) 

531 
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) locals *) 

532 
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) eexpr_local_vars; *) 

533 
(* let split_eqs_logic = Splitting.tuple_split_eq_list eqs_logic in *) 

534 
(* let locals = eexpr_local_vars @ new_locals_logic @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in *) 

535 
(* let sorted_eqs_rev_logic, remainder_logic = *) 

536 
(* List.fold_left *) 

537 
(* (fun (accu, eqs_remainder) v > *) 

538 
(* if List.exists (fun eq > List.mem v eq.eq_lhs) accu *) 

539 
(* then (\* The variable was already handled by a previous selected eq. *) 

540 
(* Typically it is part of a tuple *\) *) 

541 
(* (Format.eprintf "Case 1 for variable %s@." v; *) 

542 
(* (accu, eqs_remainder) *) 

543 
(* ) *) 

544 
(* else if List.exists (fun vdecl > vdecl.var_id = v) locals  output_var.var_id = v *) 

545 
(* then ((\* Select the eq associated to v. *\) *) 

546 
(* Format.eprintf "Case 2 for variable %s@." v; *) 

547 
(* let eq_v, remainder = find_eq v eqs_remainder in *) 

548 
(* eq_v::accu, remainder *) 

549 
(* ) *) 

550 
(* else ((\* else it is a constant value, checked during typing phase *\) *) 

551 
(* Format.eprintf "Case 3 for variable %s@." v; *) 

552 
(* accu, eqs_remainder *) 

553 
(* ) *) 

554 
(* ) *) 

555 
(* ([], split_eqs_logic) *) 

556 
(* sch_logic *) 

557 
(* in *) 

558 
(* if List.length remainder_logic > 0 then ( *) 

559 
(* Format.eprintf "Spec equations not used are@.%a@.Full equation set is:@.%a@.@?" *) 

560 
(* Printers.pp_node_eqs remainder_logic *) 

561 
(* Printers.pp_node_eqs eqs_logic; *) 

562 
(* assert false ); *) 

563 


564  
565  
566  
567  526 
let init_args = 
568  527 
ISet.empty, 
569  528 
[], 
...  ...  
622  581 
 "C"  "java"  _ > join_guards_list s_side_effects 
623  582 
) 
624  583 
} 
625 
} 

626  
627 
(* { *) 

628 
(* step_inputs = inputs; *) 

629 
(* step_outputs = [output_var]; *) 

630 
(* step_locals = ISet.elements (ISet.diff locals_sideeffects m); *) 

631 
(* step_checks = [] (\* Not handled yet *\); *) 

632 
(* step_instrs = ( *) 

633 
(* (\* special treatment depending on the active backend. For horn backend, *) 

634 
(* common branches are not merged while they are in C or Java *) 

635 
(* backends. *\) *) 

636 
(* match !Options.output with *) 

637 
(*  "horn" > s *) 

638 
(*  "C"  "java"  _ > join_guards_list s *) 

639 
(* ); *) 

640 
(* } *) 

641 


584 
} 

642  585  
643  586  
644  587 
let translate_spec nd spec = 
...  ...  
662  605 
let nd = match top.top_decl_desc with Node nd > nd  _ > assert false in 
663  606 
(*Log.report ~level:1 (fun fmt > Printers.pp_node fmt nd);*) 
664  607 
let nd, sch = Scheduling.schedule_node nd in 
665 
Format.eprintf "node sch: [%a]@.@?"


666 
(Utils.fprintf_list ~sep:", " Format.pp_print_string) sch;


608 
(* Format.eprintf "node sch: [%a]@.@?" *)


609 
(* (Utils.fprintf_list ~sep:", " Format.pp_print_string) sch; *)


667  610  
668  611 
(* let split_eqs = Splitting.tuple_split_eq_list nd.node_eqs in *) 
669  612 
let sorted_eqs_rev, remainder = 
Also available in: Unified diff