Project

General

Profile

« Previous | Next » 

Revision 3d1f9d9f

Added by LĂ©lio Brun over 2 years ago

more agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)

View differences:

src/backends/C/c_backend_spec.ml
421 421
         then pp_double_cast pp
422 422
         else pp
423 423
       else pp) fmt v
424
    | Tag t ->
424
    | Tag (t, _) ->
425 425
      pp_print_string fmt t
426 426
    | Var v ->
427 427
      pp_var_decl fmt v
......
489 489
  let val_of_expr = function
490 490
    | Val v ->
491 491
      v
492
    | Tag t ->
492
    | Tag (t, _) ->
493 493
      id_to_tag t
494 494
    | Var v ->
495 495
      vdecl_to_val v
......
520 520

  
521 521
  let has_memory m = function Val v -> has_memory_val m v | _ -> false
522 522

  
523
  let pp_spec mode m =
523
  let pp_spec mode m fmt f =
524 524
    let rec pp_spec mode fmt f =
525 525
      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
526 526
        let self = mk_self m in
......
562 562
            (pp_c_var_read ~test_output:false m)
563 563
            indirect_r
564 564
            fmt
565
            (Spec_common.type_of_l_value a, val_of_expr a, val_of_expr b)
565
            (Spec_common.type_of_value a, val_of_expr a, val_of_expr b)
566 566
        in
567 567
        if has_memory m b then
568 568
          let inst = find_arrow Location.dummy m in
......
585 585
          (pp_c_var_read ~test_output:false m)
586 586
          indirect_r
587 587
          fmt
588
          (Spec_common.type_of_l_value a, val_of_expr a, val_of_expr b)
588
          (Spec_common.type_of_value a, val_of_expr a, val_of_expr b)
589 589
      | And fs ->
590 590
        pp_and_l pp_spec' fmt fs
591 591
      | Or fs ->
......
647 647
        pp_c_val m mem_in (pp_c_var_read ~test_output:true m) fmt v
648 648
    in
649 649

  
650
    pp_spec mode
650
    pp_spec mode fmt (Spec_common.red f)
651 651
end
652 652

  
653 653
let pp_predicate pp_l pp_r fmt (l, r) =
src/machine_code.ml
215 215
      let id = Clocks.const_of_carrier cr in
216 216
      let v = env.get_var id in
217 217
      aux
218
        ( (fun spec -> Imply (Equal (Var v, Tag l), fspec spec)),
218
        ( (fun spec -> Imply (Equal (Var v, Tag (l, v.var_type)), fspec spec)),
219 219
          mk_control v l inst )
220 220
        ck
221 221
    | _ ->
src/machine_code_common.ml
45 45
  let pp_expr m fmt = function
46 46
    | Val v ->
47 47
      pp_val m fmt v
48
    | Tag t ->
48
    | Tag (t, _) ->
49 49
      pp_print_string fmt t
50 50
    | Var v ->
51 51
      pp_vdecl fmt v
src/optimize_machine.ml
21 21
let pp_elim m fmt elim =
22 22
  IMap.pp ~comment:"/* elim table: */" (pp_val m) fmt elim
23 23

  
24
let eliminate_var_decl elim m v f a =
25
  if is_memory m v then a
26
  else try
27
      f (IMap.find v.var_id elim)
28
    with Not_found -> a
29

  
24 30
let rec eliminate_val m elim expr =
25 31
  let eliminate_val = eliminate_val m in
26 32
  match expr.value_desc with
27
  | Var v -> (
28
    if is_memory m v then expr
29
    else try IMap.find v.var_id elim with Not_found -> expr)
33
  | Var v ->
34
    eliminate_var_decl elim m v (fun x -> x) expr
30 35
  | Fun (id, vl) ->
31 36
    { expr with value_desc = Fun (id, List.map (eliminate_val elim) vl) }
32 37
  | Array vl ->
......
48 53
  let e_val = eliminate_val m elim in
49 54
  match e with
50 55
  | Val v -> Val (e_val v)
51
  | Var v -> begin try Val (IMap.find v.var_id elim) with Not_found -> e end
56
  | Var v -> eliminate_var_decl elim m v (fun x -> Val x) e
52 57
  | _ -> e
53 58

  
54 59
let eliminate_pred m elim = function
55 60
  | Transition (s, f, inst, i, vars, r, mems, insts) ->
56
    Transition
57
      (s, f, inst, i, List.map (eliminate_expr m elim) vars, r, mems, insts)
61
    let vars = List.filter_map (function
62
        | Spec_types.Val v ->
63
          begin match v.value_desc with
64
            | Var vd when IMap.mem vd.var_id elim -> None
65
            | _ -> Some (Val v)
66
          end
67
        | Spec_types.Var vd when IMap.mem vd.var_id elim -> None
68
        | e -> Some (eliminate_expr m elim e)) vars
69
    in
70
    Transition (s, f, inst, i, vars, r, mems, insts)
58 71
  | p ->
59 72
    p
60 73

  
61
let rec eliminate_instr_spec m elim =
74
let rec eliminate_formula m elim =
62 75
  let e_expr = eliminate_expr m elim in
63
  let e_instr i = eliminate_instr_spec m elim i in
76
  let e_instr i = eliminate_formula m elim i in
64 77
  let e_pred = eliminate_pred m elim in
65 78
  function
66 79
  | Equal (e1, e2) ->
......
72 85
  | Imply (a, b) ->
73 86
    Imply (e_instr a, e_instr b)
74 87
  | Exists (xs, a) ->
75
    let elim = IMap.filter (fun v _ -> not (List.exists (fun v' -> v = v'.var_id) xs)) elim in
76
    Exists (xs, eliminate_instr_spec m elim a)
88
    let xs = List.filter (fun vd -> not (IMap.mem vd.var_id elim)) xs in
89
    Exists (xs, eliminate_formula m elim a)
77 90
  | Forall (xs, a) ->
78
    let elim = IMap.filter (fun v _ -> not (List.exists (fun v' -> v = v'.var_id) xs)) elim in
79
    Forall (xs, eliminate_instr_spec m elim a)
91
    let xs = List.filter (fun vd -> not (IMap.mem vd.var_id elim)) xs in
92
    Forall (xs, eliminate_formula m elim a)
80 93
  | Ternary (e, a, b) ->
81 94
    Ternary (e_expr e, e_instr a, e_instr b)
82 95
  | Predicate p ->
......
88 101

  
89 102
let rec eliminate m elim instr =
90 103
  let e_val = eliminate_val m elim in
91
  let instr = { instr with instr_spec = List.map (eliminate_instr_spec m elim) instr.instr_spec } in
104
  let instr = { instr with instr_spec = List.map (eliminate_formula m elim) instr.instr_spec } in
92 105
  match get_instr_desc instr with
93 106
  | MLocalAssign (i, v) ->
94 107
    update_instr_desc instr (MLocalAssign (i, e_val v))
......
110 123
         ( e_val g,
111 124
           List.map (fun (l, il) -> l, List.map (eliminate m elim) il) hl ))
112 125

  
126
let eliminate_transition m elim t =
127
  { t with
128
    tvars = List.filter (fun vd -> not (IMap.mem vd.var_id elim)) t.tvars;
129
    tformula = eliminate_formula m elim t.tformula }
113 130

  
114 131
(* XXX: UNUSED *)
115 132
(* let eliminate_dim elim dim =
......
375 392
  let elim_vars, instrs =
376 393
    instrs_unfold machine fanin elim_consts machine.mstep.step_instrs
377 394
  in
378
  let instrs = simplify_instrs_offset machine instrs in
379
  let checks =
395
  let step_instrs = simplify_instrs_offset machine instrs in
396
  let step_checks =
380 397
    List.map
381 398
      (fun (loc, check) ->
382 399
        loc, eliminate_val machine (IMap.map fst elim_vars) check)
383 400
      machine.mstep.step_checks
384 401
  in
385
  let locals =
402
  let step_locals =
386 403
    List.filter
387 404
      (fun v -> not (IMap.mem v.var_id elim_vars))
388 405
      machine.mstep.step_locals
389 406
  in
407
  let mtransitions = List.map (eliminate_transition machine (IMap.map fst elim_vars)) machine.mspec.mtransitions in
390 408
  let elim_consts = IMap.map fst elim_consts in
391 409
  let minstances =
392 410
    List.map (static_call_unfold elim_consts) machine.minstances
......
397 415
      mstep =
398 416
        {
399 417
          machine.mstep with
400
          step_locals = locals;
401
          step_instrs = instrs;
402
          step_checks = checks;
418
          step_locals;
419
          step_instrs;
420
          step_checks;
421
        };
422
      mspec =
423
        {
424
          machine.mspec with
425
          mtransitions
403 426
        };
404 427
      mconst;
405 428
      minstances;
src/spec_common.ml
6 6

  
7 7
let is_false = function False -> true | _ -> false
8 8

  
9
let type_of_l_value = function
9
let type_of_value = function
10
  | Val v -> v.Machine_code_types.value_type
11
  | Tag (_, t) -> t
10 12
  | Var v ->
11 13
    v.var_type
12 14
  | Memory ResetFlag ->
13 15
    Type_predef.type_bool
14 16
  | Memory (StateVar v) ->
15 17
    v.var_type
16
  | _ -> assert false
17 18

  
18
let expr_eq a b =
19
  match a, b with
20
  | Var x, Var y ->
21
    x = y
22
  | Memory r1, Memory r2 ->
23
    r1 = r2
24
  | _ ->
25
    false
19
let expr_eq a b = a = b
20
  (* match a, b with *)
21
  (* | Var x, Var y -> *)
22
  (*   x = y *)
23
  (* | Memory r1, Memory r2 -> *)
24
  (*   r1 = r2 *)
25
  (* | _ -> *)
26
  (*   false *)
26 27

  
27 28
let rec red = function
28 29
  | Equal (a, b) when expr_eq a b ->
......
124 125
  | hl ->
125 126
    let n = List.length hl in
126 127
    And (List.mapi (fun k (t, spec) ->
127
        let c = if k = n - 1 then GEqual (Var x, Tag t) else Equal (Var x, Tag t) in
128
        let tag = Tag (t, x.var_type) in
129
        let x = Var x in
130
        let c = if k = n - 1 then GEqual (x, tag) else Equal (x, tag) in
128 131
        Imply (c, spec)) hl)
129 132

  
130 133
let mk_assign_tr x v = Equal (Var x, Val v)
src/spec_common.mli
2 2
open Lustre_types
3 3
open Spec_types
4 4

  
5
val type_of_l_value : 'a expression_t -> Types.t
5
val type_of_value : Machine_code_types.value_t expression_t -> Types.t
6 6

  
7 7
val mk_conditional_tr : 'a -> 'a formula_t -> 'a formula_t -> 'a formula_t
8 8

  
src/spec_types.ml
5 5

  
6 6
type 'a expression_t =
7 7
  | Val of 'a
8
  | Tag of ident
8
  | Tag of ident * Types.t
9 9
  | Var of var_decl
10 10
  | Memory of register_t
11 11

  
src/spec_types.mli
5 5

  
6 6
type 'a expression_t =
7 7
  | Val of 'a
8
  | Tag of ident
8
  | Tag of ident * Types.t
9 9
  | Var of var_decl
10 10
  | Memory of register_t
11 11

  

Also available in: Unified diff