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/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;

Also available in: Unified diff