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