Project

General

Profile

« Previous | Next » 

Revision 36454535

Added by Pierre-Loïc Garoche over 10 years ago

Merged horn_traces branch

View differences:

src/inliner.ml
7 7
  | _ -> false) 
8 8

  
9 9

  
10
let rename_expr rename expr = expr_replace_var rename expr
11
let rename_eq rename eq = 
12
  { eq with
13
    eq_lhs = List.map rename eq.eq_lhs; 
14
    eq_rhs = rename_expr rename eq.eq_rhs
15
  }
16

  
10 17
(* 
11 18
    expr, locals', eqs = inline_call id args' reset locals nodes
12 19

  
......
27 34
      node.node_id uid v;
28 35
    Format.flush_str_formatter ()
29 36
  in
30
  let eqs' = List.map 
31
    (fun eq -> { eq with
32
      eq_lhs = List.map rename eq.eq_lhs; 
33
      eq_rhs = expr_replace_var rename eq.eq_rhs
34
    } ) node.node_eqs
37
  let eqs' = List.map (rename_eq rename) node.node_eqs
35 38
  in
36 39
  let rename_var v = { v with var_id = rename v.var_id } in
37 40
  let inputs' = List.map rename_var node.node_inputs in
......
51 54
    loc 
52 55
    (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs')
53 56
  in
54
  expr , inputs'@outputs'@locals'@locals, assign_inputs::eqs'
57
  let asserts' = (* We rename variables in assert expressions *)
58
    List.map 
59
      (fun a -> 
60
	{a with assert_expr = 
61
	    let expr = a.assert_expr in
62
	    rename_expr rename expr
63
      })
64
      node.node_asserts 
65
  in
66
  expr, 
67
  inputs'@outputs'@locals'@locals, 
68
  assign_inputs::eqs',
69
  asserts'
55 70

  
56 71

  
57 72

  
......
65 80
*)
66 81
let rec inline_expr expr locals nodes =
67 82
  let inline_tuple el = 
68
    List.fold_right (fun e (el_tail, locals, eqs) -> 
69
      let e', locals', eqs' = inline_expr e locals nodes in
70
      e'::el_tail, locals', eqs'@eqs
71
    ) el ([], locals, [])
83
    List.fold_right (fun e (el_tail, locals, eqs, asserts) -> 
84
      let e', locals', eqs', asserts' = inline_expr e locals nodes in
85
      e'::el_tail, locals', eqs'@eqs, asserts@asserts'
86
    ) el ([], locals, [], [])
72 87
  in
73 88
  let inline_pair e1 e2 = 
74
    let el', l', eqs' = inline_tuple [e1;e2] in
89
    let el', l', eqs', asserts' = inline_tuple [e1;e2] in
75 90
    match el' with
76
    | [e1'; e2'] -> e1', e2', l', eqs'
91
    | [e1'; e2'] -> e1', e2', l', eqs', asserts'
77 92
    | _ -> assert false
78 93
  in
79 94
  let inline_triple e1 e2 e3 = 
80
    let el', l', eqs' = inline_tuple [e1;e2;e3] in
95
    let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
81 96
    match el' with
82
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs'
97
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
83 98
    | _ -> assert false
84 99
  in
85 100
    
86 101
  match expr.expr_desc with
87 102
  | Expr_appl (id, args, reset) ->
88
    let args', locals', eqs' = inline_expr args locals nodes in 
103
    let args', locals', eqs', asserts' = inline_expr args locals nodes in 
89 104
    if List.exists (check_node_name id) nodes then 
90 105
      (* The node should be inlined *)
91
(*      let _ =     Format.eprintf "Inlining call to %s@." id in
92
  *)    let node = try List.find (check_node_name id) nodes 
106
      (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
107
      let node = try List.find (check_node_name id) nodes 
93 108
	with Not_found -> (assert false) in
94
      let node = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
109
      let node = 
110
	match node.top_decl_desc with Node nd -> nd | _ -> assert false in
95 111
      let node = inline_node node nodes in
96
      let expr, locals', eqs'' = 
112
      let expr, locals', eqs'', asserts'' = 
97 113
	inline_call expr args' reset locals' node in
98
      expr, locals', eqs'@eqs''
114
      expr, locals', eqs'@eqs'', asserts'@asserts''
99 115
    else 
100 116
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
101
      { expr with expr_desc = Expr_appl(id, args', reset)}, locals', eqs'
117
      { expr with expr_desc = Expr_appl(id, args', reset)}, 
118
      locals', 
119
      eqs', 
120
      asserts'
102 121

  
103 122
  (* For other cases, we just keep the structure, but convert sub-expressions *)
104 123
  | Expr_const _ 
105
  | Expr_ident _ -> expr, locals, []
124
  | Expr_ident _ -> expr, locals, [], []
106 125
  | Expr_tuple el -> 
107
    let el', l', eqs' = inline_tuple el in
108
    { expr with expr_desc = Expr_tuple el' }, l', eqs'
126
    let el', l', eqs', asserts' = inline_tuple el in
127
    { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts'
109 128
  | Expr_ite (g, t, e) ->
110
    let g', t', e', l', eqs' = inline_triple g t e in
111
    { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs'
129
    let g', t', e', l', eqs', asserts' = inline_triple g t e in
130
    { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts'
112 131
  | Expr_arrow (e1, e2) ->
113
    let e1', e2', l', eqs' = inline_pair e1 e2 in
114
    { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs'
132
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
133
    { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts'
115 134
  | Expr_fby (e1, e2) ->
116
    let e1', e2', l', eqs' = inline_pair e1 e2 in
117
    { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs'
135
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
136
    { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts'
118 137
  | Expr_array el ->
119
    let el', l', eqs' = inline_tuple el in
120
    { expr with expr_desc = Expr_array el' }, l', eqs'
138
    let el', l', eqs', asserts' = inline_tuple el in
139
    { expr with expr_desc = Expr_array el' }, l', eqs', asserts'
121 140
  | Expr_access (e, dim) ->
122
    let e', l', eqs' = inline_expr e locals nodes in 
123
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs'
141
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
142
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
124 143
  | Expr_power (e, dim) ->
125
    let e', l', eqs' = inline_expr e locals nodes in 
126
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs'
144
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
145
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
127 146
  | Expr_pre e ->
128
    let e', l', eqs' = inline_expr e locals nodes in 
129
    { expr with expr_desc = Expr_pre e' }, l', eqs'
147
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
148
    { expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
130 149
  | Expr_when (e, id, label) ->
131
    let e', l', eqs' = inline_expr e locals nodes in 
132
    { expr with expr_desc = Expr_when (e', id, label) }, l', eqs'
150
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
151
    { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
133 152
  | Expr_merge (id, branches) ->
134
    let el, l', eqs' = inline_tuple (List.map snd branches) in
153
    let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
135 154
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
136
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs'
155
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
137 156
and inline_node nd nodes = 
138
  let new_locals, eqs = 
139
    List.fold_left (fun (locals, eqs) eq ->
140
      let eq_rhs', locals', new_eqs' = 
157
  let new_locals, eqs, asserts = 
158
    List.fold_left (fun (locals, eqs, asserts) eq ->
159
      let eq_rhs', locals', new_eqs', asserts' = 
141 160
	inline_expr eq.eq_rhs locals nodes 
142 161
      in
143
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs 
144
    ) (nd.node_locals, []) nd.node_eqs
162
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
163
    ) (nd.node_locals, [], nd.node_asserts) nd.node_eqs
145 164
  in
146 165
  { nd with
147 166
    node_locals = new_locals;
148
    node_eqs = eqs
167
    node_eqs = eqs;
168
    node_asserts = asserts;
149 169
  }
150 170

  
151 171
let inline_all_calls node nodes =

Also available in: Unified diff