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