Project

General

Profile

Revision 2196a0a6

View differences:

src/c_backend.ml
197 197
  then
198 198
    fprintf fmt "%s" id.var_id
199 199
  else (
200
    Format.eprintf "pp_c_var_write: %s , outputs are %a@.@?" id.var_id (Utils.fprintf_list ~sep:", " Printers.pp_var) outputs;
200
    (* Format.eprintf "pp_c_var_write: %s , outputs are %a@.@?" id.var_id (Utils.fprintf_list ~sep:", " Printers.pp_var) outputs; *)
201 201
    if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
202 202
    then
203 203
      fprintf fmt "%s" id.var_id
......
387 387
  
388 388
 try (* stateful node instance *)
389 389
   let (n,_) = List.assoc i instances in
390
  Format.eprintf "pp_instance_call: %s , outputs are %a@.@?" (node_name n) (Utils.fprintf_list ~sep:", " Printers.pp_var) outputs;
390
  (* Format.eprintf "pp_instance_call: %s , outputs are %a@.@?" (node_name n) (Utils.fprintf_list ~sep:", " Printers.pp_var) outputs; *)
391 391
 fprintf fmt "%s_step (%a%t%a%t%s->%s);"
392 392
     (node_name n)
393 393
     (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read machine_outputs))) inputs
......
399 399
 with Not_found -> ((* stateless node instance *)
400 400
  try 
401 401
    let (n,_) = List.assoc i calls in
402
  Format.eprintf "pp_instance_call: %s , outputs are %a@.@?" (node_name n) (Utils.fprintf_list ~sep:", " Printers.pp_var) outputs;
402
  (* Format.eprintf "pp_instance_call: %s , outputs are %a@.@?" (node_name n) (Utils.fprintf_list ~sep:", " Printers.pp_var) outputs; *)
403 403
    fprintf fmt "%s (%a%t%a);"
404 404
      (node_name n)
405 405
      (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read machine_outputs))) inputs
......
583 583
    pp_eexpr_logic_instr m self fmt (MLocalAssign (i0, Fun (i, vl)))
584 584
  | MStep ([i0], "ite", vl) ->
585 585
    pp_eexpr_logic_instr m self fmt (MLocalAssign (i0, Fun ("ite", vl)))
586
  | MStep (il, i, vl) ->Format.eprintf "Illegal function call %s@.%a@.@?" i pp_instr instr; assert false (* should not happen, calls were inlined *)
586
  | MStep (il, i, vl) ->
587
    Format.eprintf "Illegal function call %s@.%a@.@?" i pp_instr instr; 
588
    assert false (* should not happen, calls were inlined *)
587 589
  | MBranch (g,hl) -> assert false (* should not happen. Oder ??? TODO *)
588 590

  
589 591

  
src/causality.ml
415 415

  
416 416
let global_dependency_eqs inputs vars eqs =
417 417
  
418
  Format.eprintf "@.%a@." (Utils.fprintf_list ~sep:"@." Printers.pp_node_eq) eqs;
419
  Format.eprintf "inputs: %a@." (Utils.fprintf_list ~sep:"@." Printers.pp_var) inputs;
418
  (* Format.eprintf "@.%a@." (Utils.fprintf_list ~sep:"@." Printers.pp_node_eq) eqs; *)
419
  (* Format.eprintf "inputs: %a@." (Utils.fprintf_list ~sep:"@." Printers.pp_var) inputs; *)
420 420
  let mems = ExprDep.eqs_memory_variables eqs in
421
  Format.eprintf "@.global dep; mems: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) (ISet.elements mems); 
421
  (* Format.eprintf "@.global dep; mems: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) (ISet.elements mems);  *)
422 422
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs eqs in
423
  Format.eprintf "g_non_mems: %a@.@?" pp_dep_graph g_non_mems;
424
  Format.eprintf "g_mems: %a@.@?" pp_dep_graph g_mems;
423
  (* Format.eprintf "g_non_mems: %a@.@?" pp_dep_graph g_non_mems; *)
424
  (* Format.eprintf "g_mems: %a@.@?" pp_dep_graph g_mems; *)
425 425
  CycleDetection.check_cycles g_non_mems;
426 426
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles vars eqs mems g_mems in
427 427
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
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 = 
src/normalization.ml
318 318
  let nodes = get_nodes decls in
319 319
  let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
320 320
  let calls = List.map (fun called_nd -> List.find (fun nd2 -> node_name nd2 = called_nd) nodes) calls in
321
  Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd -> pp_print_string fmt (node_name nd))) calls;
321
  (* Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd -> pp_print_string fmt (node_name nd))) calls; *)
322 322
  let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
323 323
  if calls = [] then
324 324
    let defs, vars = normalize_eq_split node ([], vars) eq in
src/splitting.ml
36 36
  | Expr_ident _ -> [expr]
37 37
  | Expr_tuple elist -> elist
38 38
  | Expr_appl ("=", args, r) -> ( (* Specific treatment of tuple equalities *)
39
    Format.eprintf "splitting equality: %a@." Printers.pp_expr expr;
40 39
    let args_list = List.map tuple_split_expr (expr_list_of_expr args) in
41
    Format.eprintf "splitting equality: %a@.%i elements" Printers.pp_expr expr (List.length args_list);
42 40
    let (eqs : expr list)=
43 41
      List.map
44 42
	(fun arg -> 
......
52 50
    | [] -> assert false 
53 51
    | [e] -> [e]
54 52
    | hd::tl -> 
55
      Format.eprintf "obtained eqs:@.%a@.@." (Utils.fprintf_list ~sep:"@." Printers.pp_expr) eqs;
56 53
      let res = List.fold_left (fun accu eq ->
57 54
	mkpredef_call args.expr_loc "&&" [accu; eq]
58 55
      ) hd tl
59 56
      in
60
      Format.eprintf "Result: %a@." Printers.pp_expr res;
61 57
      [res]
62 58
  )
63 59
  | Expr_appl (id, args, r) ->
src/typing.ml
412 412
*)
413 413
and type_appl env in_main loc const f args =
414 414
  let tfun = type_ident env in_main loc const f in
415
  Format.eprintf "Typing function call %s: %a@.@?" f print_ty tfun ;
415
  (* Format.eprintf "Typing function call %s: %a@.@?" f print_ty tfun ; *)
416 416
  let tins, touts = split_arrow tfun in
417 417
  let tins = type_list_of_type tins in
418 418
  let args = expr_list_of_expr args in
......
422 422
(** [type_expr env in_main expr] types expression [expr] in environment
423 423
    [env], expecting it to be [const] or not. *)
424 424
and type_expr env in_main const expr =
425
  Format.eprintf "Typing expr: %a@.@?" Printers.pp_expr expr;
425
  (* Format.eprintf "Typing expr: %a@.@?" Printers.pp_expr expr; *)
426 426
  let res = 
427 427
  match expr.expr_desc with
428 428
  | Expr_const c ->
429
    Format.eprintf "const@.@?";
429
    (* Format.eprintf "const@.@?"; *)
430 430
    let ty = type_const expr.expr_loc c in
431 431
    let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in
432 432
    expr.expr_type <- ty;
433 433
    ty
434 434
  | Expr_ident v ->
435
    Format.eprintf "ident@.@?";
435
    (* Format.eprintf "ident@.@?"; *)
436 436
    let tyv =
437 437
      try
438 438
        Env.lookup_value (fst env) v
......
470 470
    expr.expr_type <- ty;
471 471
    ty
472 472
  | Expr_tuple elist ->
473
    Format.eprintf "const@.@?";
473
    (* Format.eprintf "const@.@?"; *)
474 474
    let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in
475 475
    expr.expr_type <- ty;
476 476
    ty
......
480 480
    expr.expr_type <- ty;
481 481
    ty
482 482
  | Expr_appl (id, args, r) ->
483
    Format.eprintf "app %s@.@?" id;
483
    (* Format.eprintf "app %s@.@?" id; *)
484 484
    (* application of non internal function is not legal in a constant
485 485
       expression *)
486 486
    (match r with
......
682 682
    match nd.node_spec with
683 683
    | Some ns -> (
684 684
      try
685
	Format.eprintf "Typing specification: %a@.@?"
686
	  Printers.pp_spec ns;
687
	type_spec (delta_env, vd_env) ns;
688
	Format.eprintf "Typing ok@.@?";
685
	(* Format.eprintf "Typing specification: %a@.@?" *)
686
	(*   Printers.pp_spec ns; *)
687
	type_spec (delta_env, vd_env) ns
689 688
      with _ as exc -> (
690 689
	Format.eprintf "Error typing specification: %a@."
691 690
	  Printers.pp_spec ns;
......
720 719
  generalize ty_node;
721 720
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
722 721
  nd.node_type <- ty_node;
723
  Format.eprintf "Node %s type is %a@." nd.node_id Types.print_ty ty_node;
722
  (* Format.eprintf "Node %s type is %a@." nd.node_id Types.print_ty ty_node; *)
724 723
  Env.add_value env nd.node_id ty_node
725 724

  
726 725
let type_imported_node env nd loc =

Also available in: Unified diff