Project

General

Profile

Revision 0d065e73

View differences:

src/compiler_common.ml
239 239
    deps
240 240
  end
241 241

  
242

  
src/machine_code.ml
81 81
}
82 82

  
83 83
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
84

  
84 85
let pp_step fmt s =
85 86
  Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
86 87
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs
......
318 319
      (* special treatment depending on the active backend. For horn backend, ite
319 320
	 are preserved in expression. While they are removed for C or Java
320 321
	 backends. *)
321
      match !Options.output with | "horn" -> 
322
	Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
322
      match !Options.output with
323
      | "horn" -> 
324
	 Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
323 325
      | "C" | "java" | _ -> 
324
	(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
326
	 (Format.eprintf "Normalization error for backend %s: %a@."
327
	    !Options.output
328
	    Printers.pp_expr expr;
329
	  raise NormalizationError)
325 330
    )
326 331
    | _                   -> raise NormalizationError
327 332
  in
......
488 493

  
489 494
  let sorted_eqs = sort_equations_from_schedule nd sch in
490 495
  let constant_eqs = constant_equations nd in
491
  
492
  let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in
496

  
497
  (* In case of non functional backend (eg. C), additional local variables have
498
     to be declared for each assert *)
499
  let new_locals, assert_instrs, nd_node_asserts =
500
    let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
501
    if Corelang.functional_backend () then
502
      [], [], exprl  
503
    else (* Each assert(e) is associated to a fresh variable v and declared as
504
	    v=e; assert (v); *)
505
      let _, vars, eql, assertl =
506
	List.fold_left (fun (i, vars, eqlist, assertlist) expr ->
507
	  let loc = expr.expr_loc in
508
	  let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in
509
	  let assert_var =
510
	    mkvar_decl
511
	      loc
512
	      ~orig:false (* fresh var *)
513
	      (var_id,
514
	       mktyp loc Tydec_bool,
515
	       mkclock loc Ckdec_any,
516
	       false, (* not a constant *)
517
	       None (* no default value *)
518
	      )
519
	  in
520
	  assert_var.var_type <- Types.new_ty (Types.Tbool); 
521
	  let eq = mkeq loc ([var_id], expr) in
522
	  (i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist)
523
	) (1, [], [], []) exprl
524
      in
525
      vars, eql, assertl
526
  in
527
  let locals_list = nd.node_locals @ new_locals in
528

  
529
  let nd = { nd with node_locals = locals_list } in
530
  let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) locals_list ISet.empty, [] in
493 531
  (* memories, init instructions, node calls, local variables (including memories), step instrs *)
494 532
  let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in
495 533
  assert (ISet.is_empty m0);
496 534
  assert (init0 = []);
497 535
  assert (Utils.IMap.is_empty j0);
498
  let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, []) sorted_eqs in
536
  let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, []) (sorted_eqs@assert_instrs) in
499 537
  let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
500 538
  {
501 539
    mname = nd;
......
518 556
	(* | "horn" -> s TODO 16/12 *)
519 557
	| "C" | "java" | _ -> join_guards_list s
520 558
      );
521
      step_asserts = 
522
	let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
523
	List.map (translate_expr nd init_args) exprl
524
	;
559
      step_asserts = List.map (translate_expr nd init_args) nd_node_asserts;
525 560
    };
526 561
    mspec = nd.node_spec;
527 562
    mannot = nd.node_annot;
......
578 613
  | Dimension.Dident v        -> value_of_ident m v
579 614
  | Dimension.Dappl (f, args) -> let typ = if Basic_library.is_numeric_operator f then Type_predef.type_int else Type_predef.type_bool
580 615
                                 in mk_val (Fun (f, List.map (value_of_dimension m) args)) typ
581
  | Dimension.Dite (i, t, e)  -> let [vi; vt; ve] = List.map (value_of_dimension m) [i; t; e] in
582
				 mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type
616
  | Dimension.Dite (i, t, e)  -> (
617
    match List.map (value_of_dimension m) [i; t; e] with
618
    | [vi; vt; ve] ->  mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type
619
    | _ -> assert false (* could not happen *)
620
  )
583 621
  | Dimension.Dlink dim'      -> value_of_dimension m dim'
584 622
  | _                         -> assert false
585 623

  

Also available in: Unified diff