Project

General

Profile

« Previous | Next » 

Revision 0406ab94

Added by LĂ©lio Brun 7 months ago

implement optimization on spec: IT WORKS

View differences:

include/arrow_spec.h
37 37
 */
38 38

  
39 39
/*@ predicate _arrow_transition(struct _arrow_mem_ghost mem_in,
40
                                struct _arrow_mem_ghost mem_out,
41
                                _Bool out) =
40
                                _Bool out,
41
                                struct _arrow_mem_ghost mem_out) =
42 42
      out == mem_in._reg._first
43 43
      && (mem_in._reg._first ? (mem_out._reg._first == 0)
44 44
                             : (mem_out._reg._first == mem_in._reg._first));
src/backends/C/c_backend_spec.ml
258 258

  
259 259
let pp_memory_pack' fmt = pp_memory_pack pp_print_string pp_print_string fmt
260 260

  
261
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_input pp_output fmt
262
    (name, inputs, locals, outputs, mem_in, mem_out) =
261
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_var fmt
262
    (name, vars, mem_in, mem_out) =
263 263
  let stateless = fst (get_stateless_status m) in
264
  fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])" name
264
  fprintf fmt "%s_transition%a(@[<hov>%t%a%t@])" name
265 265
    (pp_print_option pp_print_int)
266 266
    i
267 267
    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)
268 268
    (pp_comma_list
269 269
       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
270
       pp_input)
271
    inputs
272
    (pp_print_option (fun fmt _ ->
273
         pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals))
274
    i
270
       pp_var)
271
    vars
275 272
    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
276
    (pp_comma_list ~pp_prologue:pp_print_comma pp_output)
277
    outputs
278 273

  
279
let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt
280
    (t, mem_in, mem_out) =
281
  pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_input pp_output fmt
282
    (t.tname.node_id, t.tinputs, t.tlocals, t.toutputs, mem_in, mem_out)
274
let pp_transition m pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
275
  pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_var fmt
276
    (t.tname.node_id, t.tvars, mem_in, mem_out)
283 277

  
284 278
let pp_transition_aux' ?i m =
285
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl
279
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl
286 280

  
287 281
let pp_transition_aux'' ?i m =
288
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
282
  pp_transition_aux ?i m pp_print_string pp_print_string (fun fmt v ->
283
      (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
289 284

  
290 285
let pp_transition' m =
291
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl
292

  
293
let pp_transition'' m =
294
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
286
  pp_transition m pp_print_string pp_print_string pp_var_decl
295 287

  
296 288
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
297 289
  fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" name pp_mem_in mem_in
......
329 321

  
330 322
  let pp_expr :
331 323
      type a.
332
      ?output:bool ->
324
      ?test_output:bool ->
333 325
      machine_t ->
334 326
      ident ->
335 327
      formatter ->
336 328
      (value_t, a) expression_t ->
337 329
      unit =
338
   fun ?(output = false) m mem fmt -> function
330
   fun ?(test_output = false) m mem fmt -> function
339 331
    | Val v ->
340
      pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v
332
      pp_c_val m mem (pp_c_var_read ~test_output m) fmt v
341 333
    | Tag t ->
342 334
      pp_print_string fmt t
343 335
    | Var v ->
......
346 338
      pp_reg mem fmt r
347 339

  
348 340
  let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
349
    let output, mem_update =
341
    let test_output, mem_update =
350 342
      match mode with
351 343
      | InstrMode _ ->
352 344
        true, false
......
355 347
      | _ ->
356 348
        false, false
357 349
    in
358
    let pp_expr :
359
        type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit =
360
     fun ?output fmt e -> pp_expr ?output m mem_out fmt e
350
    let pp_expr : type a. bool -> formatter -> (value_t, a) expression_t -> unit
351
        =
352
     fun test_output fmt e -> pp_expr ~test_output m mem_out fmt e
361 353
    in
362 354
    match p with
363
    | Transition (f, inst, i, inputs, locals, outputs, r, mems, insts) ->
355
    | Transition (f, inst, i, vars, r, mems, insts) ->
364 356
      let pp_mem_in, pp_mem_out =
365 357
        match inst with
366 358
        | None ->
......
373 365
              else pp_access' fmt (mem_in, inst)),
374 366
            fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
375 367
      in
376
      pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output) fmt
377
        (f, inputs, locals, outputs, mem_in', mem_out')
368
      pp_transition_aux ?i m pp_mem_in pp_mem_out (pp_expr test_output) fmt
369
        (f, vars, mem_in', mem_out')
378 370
    | Reset (_f, inst, r) ->
379 371
      pp_ite
380 372
        (pp_c_val m mem_in (pp_c_var_read m))
......
555 547
       (pp_transition m
556 548
          (pp_machine_decl' ~ghost:true)
557 549
          (pp_machine_decl' ~ghost:true)
558
          (pp_local m) (pp_local m))
550
          (pp_local m))
559 551
       (PrintSpec.pp_spec TransitionMode m))
560 552
    fmt
561 553
    ((t, (name, mem_in), (name, mem_out)), t.tformula)
......
593 585
  let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
594 586
  let tr ?mems ?insts () =
595 587
    Spec_common.mk_transition ?mems ?insts ?i:t.tindex name
596
      (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
597
      (vdecls_to_vals t.toutputs)
588
      (vdecls_to_vals t.tvars)
598 589
  in
599 590
  if not (mems_empty && insts_empty) then
600 591
    pp_acsl
......
610 601
      ( t,
611 602
        ( (m.mname.node_id, [ mem_in; mem_out ]),
612 603
          ( instances,
613
            ( memories,
614
              Forall
615
                ( t.tinputs @ t.tlocals @ t.toutputs,
616
                  Imply (tr (), tr ~mems ~insts ()) ) ) ) ) )
604
            (memories, Forall (t.tvars, Imply (tr (), tr ~mems ~insts ()))) ) )
605
      )
617 606

  
618 607
let pp_transition_footprint_lemmas fmt m =
619 608
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
......
824 813
            (pp_requires pp_separated')
825 814
            outputs (pp_assigns pp_ptr_decl) outputs
826 815
            (pp_ensures (pp_transition_aux'' m))
827
            (name, inputs, [], outputs, "", "")
816
            (name, inputs @ outputs, "", "")
828 817
        else
829 818
          fprintf fmt
830 819
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
......
839 828
            (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
840 829
            (name, mem, self)
841 830
            (pp_ensures
842
               (pp_transition_aux m (pp_old pp_ptr) pp_ptr pp_var_decl
843
                  pp_ptr_decl))
844
            (name, inputs, [], outputs, mem, mem)
831
               (pp_transition_aux m (pp_old pp_ptr) pp_ptr (fun fmt v ->
832
                    (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
833
            (name, inputs @ outputs, mem, mem)
845 834
            (pp_assigns pp_ptr_decl) outputs
846 835
            (pp_assigns (pp_reg self))
847 836
            m.mmemory
src/machine_code.ml
186 186
  (* Transition spec *)
187 187
  t :
188 188
    (var_decl list
189
    (* inputs *)
190
    * var_decl list
191
    (* locals *)
192
    * var_decl list
193
    (* outputs *)
189
    (* vars *)
194 190
    * ISet.t (* memory footprint *)
195 191
    * ident IMap.t
196 192
    (* memory instances footprint *)
......
247 243
  let outputs_i = Lustre_live.inter_live_i_with id i outputs in
248 244
  let pred_mp ctx a = And [ mk_memory_pack ~i:(i - 1) id; a ] :: ctx.mp in
249 245
  let pred_t ctx a =
250
    ( inputs,
251
      locals_i,
252
      outputs_i,
246
    ( inputs @ locals_i @ outputs_i,
253 247
      ctx.m,
254 248
      IMap.map (fun (td, _) -> node_name td) ctx.j,
255 249
      Exists
256 250
        ( Lustre_live.existential_vars id i eq (locals @ outputs),
257 251
          And
258 252
            [
259
              mk_transition ~i:(i - 1) id (vdecls_to_vals inputs)
260
                (vdecls_to_vals locals_pi)
261
                (vdecls_to_vals outputs_pi);
253
              mk_transition ~i:(i - 1) id
254
                (vdecls_to_vals (inputs @ locals_pi @ outputs_pi));
262 255
              a;
263 256
            ] ) )
264 257
    :: ctx.t
......
274 267
            (if fst (get_stateless_status_node nd) then []
275 268
            else [ mk_memory_pack ~i id ])
276 269
            @ [
277
                mk_transition ~i id (vdecls_to_vals inputs)
278
                  (vdecls_to_vals locals_i) (vdecls_to_vals outputs_i);
270
                mk_transition ~i id
271
                  (vdecls_to_vals (inputs @ locals_i @ outputs_i));
279 272
              ];
280 273
        }
281 274
        :: ctx.s;
......
304 297
      ctl
305 298
        (MStep ([ var_x ], inst, [ c1; c2 ]))
306 299
        (mk_memory_pack ~inst (node_name td))
307
        (mk_transition ~inst (node_name td) [] [] [ vdecl_to_val var_x ])
300
        (mk_transition ~inst (node_name td) [ vdecl_to_val var_x ])
308 301
        { ctx with j = IMap.add inst (td, []) ctx.j }
309 302
    in
310 303
    { ctx with si = mkinstr (MSetReset inst) :: ctx.si }
......
332 325
    }
333 326
  | p, Expr_appl (f, arg, r)
334 327
    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
335
    let var_p = List.map (fun v -> env.get_var v) p in
328
    let var_p = List.map env.get_var p in
336 329
    let el = expr_list_of_expr arg in
337 330
    let vl = List.map translate_expr el in
338 331
    let node_f = node_from_name f in
......
351 344
      ctl ~ck:call_ck
352 345
        (MStep (var_p, inst, vl))
353 346
        (mk_memory_pack ~inst (node_name node_f))
354
        (mk_transition ?r ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))
347
        (mk_transition ?r ~inst (node_name node_f) (vl @ vdecls_to_vals var_p))
355 348
        {
356 349
          ctx with
357 350
          j = IMap.add inst call_f ctx.j;
......
472 465
  {
473 466
    tname = nd;
474 467
    tindex = Some 0;
475
    tinputs = nd.node_inputs;
476
    tlocals = [];
477
    toutputs = [];
468
    tvars = nd.node_inputs;
478 469
    tformula = True;
479 470
    tmem_footprint = ISet.empty;
480 471
    tinst_footprint = IMap.empty;
......
483 474
let transition_toplevel nd i =
484 475
  let tr =
485 476
    mk_transition nd.node_id ~i
486
      (vdecls_to_vals nd.node_inputs)
487
      []
488
      (vdecls_to_vals nd.node_outputs)
477
      (vdecls_to_vals (nd.node_inputs @ nd.node_outputs))
489 478
  in
490 479
  {
491 480
    tname = nd;
492 481
    tindex = None;
493
    tinputs = nd.node_inputs;
494
    tlocals = [];
495
    toutputs = nd.node_outputs;
482
    tvars = nd.node_inputs @ nd.node_outputs;
496 483
    tformula =
497 484
      (if fst (get_stateless_status_node nd) then tr
498 485
      else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));
......
564 551
    transition_0 nd
565 552
    ::
566 553
    List.mapi
567
      (fun i (tinputs, tlocals, toutputs, tmem_footprint, tinst_footprint, f) ->
554
      (fun i (tvars, tmem_footprint, tinst_footprint, f) ->
568 555
        {
569 556
          tname = nd;
570 557
          tindex = Some (i + 1);
571
          tinputs;
572
          tlocals;
573
          toutputs;
558
          tvars;
574 559
          tformula = red f;
575 560
          tmem_footprint;
576 561
          tinst_footprint;
......
583 568
      ~instr_spec:
584 569
        ((if fst (get_stateless_status_node nd) then []
585 570
         else [ mk_memory_pack ~i:0 nd.node_id ])
586
        @ [
587
            mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] [];
588
          ])
571
        @ [ mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) ])
589 572
      MClearReset
590 573
  in
591 574
  {
src/machine_code_common.ml
58 58
     fun fmt e -> pp_expr m fmt e
59 59
    in
60 60
    match p with
61
    | Transition (f, inst, i, inputs, locals, outputs, _r, _mems, _insts) ->
61
    | Transition (f, inst, i, vars, _r, _mems, _insts) ->
62 62
      fprintf fmt "Transition_%a<%a>%a%a" pp_print_string f
63 63
        (pp_print_option
64 64
           ~none:(fun fmt () -> pp_print_string fmt "SELF")
......
67 67
        (pp_print_option pp_print_int)
68 68
        i
69 69
        (pp_print_parenthesized pp_expr)
70
        (inputs @ locals @ outputs)
70
        vars
71 71
    | Reset (f, inst, r) ->
72 72
      fprintf fmt "Reset_%a<%a> on %a" pp_print_string f pp_print_string inst
73 73
        (pp_val m) r
......
239 239
    (pp_print_option pp_print_int)
240 240
    t.tindex
241 241
    (pp_print_parenthesized pp_vdecl)
242
    (t.tinputs @ t.tlocals @ t.toutputs)
243
    (PrintSpec.pp_spec m) t.tformula
242
    t.tvars (PrintSpec.pp_spec m) t.tformula
244 243

  
245 244
let pp_transitions m fmt =
246 245
  if !Options.spec <> "no" then
src/optimize_machine.ml
11 11

  
12 12
open Utils
13 13
open Lustre_types
14
open Spec_types
14 15
open Machine_code_types
15 16
open Corelang
16 17
open Causality
......
597 598
  | Power (v, n) ->
598 599
    { value with value_desc = Power (value_replace_var fvar v, n) }
599 600

  
600
let rec instr_replace_var fvar instr cont =
601
  match get_instr_desc instr with
602
  | MLocalAssign (i, v) ->
603
    instr_cons
604
      (update_instr_desc instr
605
         (MLocalAssign (fvar i, value_replace_var fvar v)))
606
      cont
607
  | MStateAssign (i, v) ->
608
    instr_cons
609
      (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v)))
610
      cont
611
  | MSetReset _
612
  | MNoReset _
613
  | MClearReset
614
  | MResetAssign _
615
  | MSpec _
616
  | MComment _ ->
617
    instr_cons instr cont
618
  | MStep (il, i, vl) ->
619
    instr_cons
620
      (update_instr_desc instr
621
         (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)))
622
      cont
623
  | MBranch (g, hl) ->
624
    instr_cons
625
      (update_instr_desc instr
626
         (MBranch
627
            ( value_replace_var fvar g,
628
              List.map (fun (h, il) -> h, instrs_replace_var fvar il []) hl )))
629
      cont
601
let expr_spec_replace :
602
    type a.
603
    (var_decl -> var_decl) ->
604
    (value_t, a) expression_t ->
605
    (value_t, a) expression_t =
606
 fun fvar -> function
607
  | Val v ->
608
    Val (value_replace_var fvar v)
609
  | Var v ->
610
    Var (fvar v)
611
  | e ->
612
    e
613

  
614
let predicate_spec_replace fvar = function
615
  | Transition (f, inst, i, vars, r, mems, insts) ->
616
    Transition
617
      (f, inst, i, List.map (expr_spec_replace fvar) vars, r, mems, insts)
618
  | p ->
619
    p
620

  
621
let rec instr_spec_replace fvar =
622
  let aux instr = instr_spec_replace fvar instr in
623
  function
624
  | Equal (e1, e2) ->
625
    Equal (expr_spec_replace fvar e1, expr_spec_replace fvar e2)
626
  | And f ->
627
    And (List.map aux f)
628
  | Or f ->
629
    Or (List.map aux f)
630
  | Imply (a, b) ->
631
    Imply (aux a, aux b)
632
  | Exists (xs, a) ->
633
    let fvar v = if List.mem v xs then v else fvar v in
634
    Exists (xs, instr_spec_replace fvar a)
635
  | Forall (xs, a) ->
636
    let fvar v = if List.mem v xs then v else fvar v in
637
    Forall (xs, instr_spec_replace fvar a)
638
  | Ternary (e, a, b) ->
639
    Ternary (expr_spec_replace fvar e, aux a, aux b)
640
  | Predicate p ->
641
    Predicate (predicate_spec_replace fvar p)
642
  | ExistsMem (f, a, b) ->
643
    ExistsMem (f, aux a, aux b)
644
  | f ->
645
    f
646

  
647
let rec instr_replace_var fvar instr =
648
  let instr_desc =
649
    match instr.instr_desc with
650
    | MLocalAssign (i, v) ->
651
      MLocalAssign (fvar i, value_replace_var fvar v)
652
    | MStateAssign (i, v) ->
653
      MStateAssign (i, value_replace_var fvar v)
654
    | MStep (il, i, vl) ->
655
      MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)
656
    | MBranch (g, hl) ->
657
      MBranch
658
        ( value_replace_var fvar g,
659
          List.map (fun (h, il) -> h, instrs_replace_var fvar il []) hl )
660
    | MSetReset _
661
    | MNoReset _
662
    | MClearReset
663
    | MResetAssign _
664
    | MSpec _
665
    | MComment _ ->
666
      instr.instr_desc
667
  in
668
  let instr_spec = List.map (instr_spec_replace fvar) instr.instr_spec in
669
  instr_cons { instr with instr_desc; instr_spec }
630 670

  
631 671
and instrs_replace_var fvar instrs cont =
632 672
  List.fold_right (instr_replace_var fvar) instrs cont
......
657 697
let machine_replace_variables fvar m =
658 698
  { m with mstep = step_replace_var fvar m.mstep }
659 699

  
660
let machine_reuse_variables m reuse =
700
let machine_reuse_variables reuse m =
661 701
  let fvar v = try Hashtbl.find reuse v.var_id with Not_found -> v in
662 702
  machine_replace_variables fvar m
663 703

  
664
let machines_reuse_variables prog reuse_tables =
665
  List.map
666
    (fun m ->
667
      machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables))
668
    prog
704
let machines_reuse_variables reuse_tables =
705
  List.map (fun m ->
706
      machine_reuse_variables (Utils.IMap.find m.mname.node_id reuse_tables) m)
669 707

  
670 708
let rec instr_assign res instr =
671 709
  match get_instr_desc instr with
......
723 761
    i1 :: instrs_reduce branches (i2 :: q) cont
724 762

  
725 763
let rec instrs_fusion instrs =
726
  match instrs, List.map get_instr_desc instrs with
727
  | [], [] | [ _ ], [ _ ] ->
764
  match instrs with
765
  | [] | [ _ ] ->
728 766
    instrs
729
  | i1 :: _ :: q, _ :: MBranch ({ value_desc = Var v; _ }, hl) :: _
730
    when instr_constant_assign v i1 ->
731
    instr_reduce
732
      (List.map (fun (h, b) -> h, instrs_fusion b) hl)
733
      i1 (instrs_fusion q)
734
  | i1 :: i2 :: q, _ ->
735
    i1 :: instrs_fusion (i2 :: q)
736
  | _ ->
737
    assert false
738
(* Other cases should not happen since both lists are of same size *)
767
  | i1 :: i2 :: q -> (
768
    match i2.instr_desc with
769
    | MBranch ({ value_desc = Var v; _ }, hl) when instr_constant_assign v i1 ->
770
      instr_reduce
771
        (List.map (fun (h, b) -> h, instrs_fusion b) hl)
772
        { i1 with instr_spec = i1.instr_spec @ i2.instr_spec }
773
        (instrs_fusion q)
774
    | _ ->
775
      i1 :: instrs_fusion (i2 :: q))
739 776

  
740 777
let step_fusion step =
741 778
  { step with step_instrs = instrs_fusion step.step_instrs }
......
897 934
        Scheduling.remove_prog_inlined_locals removed_table node_schs
898 935
      in
899 936
      let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
900
      machines_fusion (machines_reuse_variables machine_code reuse_tables))
937
      machines_fusion (machines_reuse_variables reuse_tables machine_code))
901 938
    else machine_code
902 939
  in
903 940

  
src/spec_common.ml
79 79

  
80 80
let mk_pred_call pred = Predicate pred
81 81

  
82
let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst id
83
    inputs locals outputs =
82
let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst id vars
83
    =
84 84
  let tr =
85 85
    mk_pred_call
86 86
      (Transition
87 87
         ( id,
88 88
           inst,
89 89
           i,
90
           vals inputs,
91
           vals locals,
92
           vals outputs,
90
           vals vars,
93 91
           (match r with Some _ -> true | None -> false),
94 92
           mems,
95 93
           insts ))
src/spec_types.ml
22 22
  | Memory (StateVar v) ->
23 23
    v.var_type
24 24

  
25
type ('a, 'b) expressions_t = ('a, 'b) expression_t list
26

  
27 25
type 'a predicate_t =
28 26
  | Transition :
29 27
      ident (* node name *)
......
31 29
      (* instance *)
32 30
      * int option
33 31
      (* transition index *)
34
      * ('a, 'b) expressions_t
35
      (* inputs *)
36
      * ('a, 'b) expressions_t
37
      (* locals *)
38
      * ('a, 'b) expressions_t
39
      (* outputs *)
32
      * ('a, 'b) expression_t list
33
      (* variables *)
40 34
      * bool (* reset *)
41 35
      * Utils.ISet.t (* memory footprint *)
42 36
      * ident Utils.IMap.t
......
78 72
type 'a transition_t = {
79 73
  tname : node_desc;
80 74
  tindex : int option;
81
  tinputs : var_decl list;
82
  tlocals : var_decl list;
83
  toutputs : var_decl list;
75
  tvars : var_decl list;
84 76
  tformula : 'a formula_t;
85 77
  tmem_footprint : Utils.ISet.t;
86 78
  tinst_footprint : ident Utils.IMap.t;

Also available in: Unified diff