Project

General

Profile

Revision 2196a0a6 src/machine_code.ml

View differences:

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