Project

General

Profile

« Previous | Next » 

Revision 7ee5f69e

Added by LĂ©lio Brun 9 months ago

corrections on loggers + spec in AST

View differences:

src/machine_code.ml
15 15
open Corelang
16 16
open Clocks
17 17
open Causality
18
  
18

  
19 19
exception NormalizationError
20 20

  
21 21
(* Questions:
22 22

  
23 23
   - where are used the mconst. They contain initialization of
24
   constant in nodes. But they do not seem to be used by c_backend *)
24
     constant in nodes. But they do not seem to be used by c_backend *)
25

  
25 26

  
26
       
27 27
(* translate_<foo> : vars -> context -> <foo> -> machine code/expression *)
28 28
(* the context contains  m : state aka memory variables  *)
29 29
(*                      si : initialization instructions *)
......
34 34
(* Machine processing requires knowledge about variables and local
35 35
   variables. Local could be memories while other could not.  *)
36 36
type machine_env = {
37
    is_local: string -> bool;
38
    get_var: string -> var_decl
39
  }
37
  is_local: string -> bool;
38
  get_var: string -> var_decl
39
}
40

  
40 41

  
41
                 
42 42
let build_env locals non_locals =
43 43
  let all = VSet.union locals non_locals in
44 44
  {
45 45
    is_local = (fun id -> VSet.exists (fun v -> v.var_id = id) locals);
46
    get_var = (fun id -> try
47
                  VSet.get id all
48
                with Not_found -> (
49
                  (* Format.eprintf "Impossible to find variable %s in set %a@.@?"
50
                   *   id
51
                   *   VSet.pp all; *)
52
                  raise Not_found
53
                )
54
              )  
46
    get_var = (fun id -> try VSet.get id all with Not_found ->
47
        (* Format.eprintf "Impossible to find variable %s in set %a@.@?"
48
         *   id
49
         *   VSet.pp all; *)
50
        raise Not_found)
55 51
  }
56 52

  
57
  
53

  
58 54

  
59 55
(****************************************************************)
60 56
(* Basic functions to translate to machine values, instructions *) 
......
66 62
    let var_id = env.get_var id in
67 63
    mk_val (Var var_id) var_id.var_type
68 64
  with Not_found ->
69
    try (* id is a constant *)
70
      let vdecl = (Corelang.var_decl_of_const
71
                     (const_of_top (Hashtbl.find Corelang.consts_table id)))
72
      in
73
      mk_val (Var vdecl) vdecl.var_type
74
    with Not_found ->
75
      (* id is a tag, getting its type in the list of declared enums *)
76
      try
77
        let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
78
        mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
79
      with Not_found -> (Format.eprintf
80
                           "internal error: Machine_code.translate_ident %s@.@?"
81
                           id;
82
                         assert false)
65
  try (* id is a constant *)
66
    let vdecl = (Corelang.var_decl_of_const
67
                   (const_of_top (Hashtbl.find Corelang.consts_table id)))
68
    in
69
    mk_val (Var vdecl) vdecl.var_type
70
  with Not_found ->
71
  (* id is a tag, getting its type in the list of declared enums *)
72
  try
73
    let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
74
    mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
75
  with Not_found ->
76
    Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;
77
    assert false
83 78

  
84 79
let rec control_on_clock env ck inst =
85
 match (Clocks.repr ck).cdesc with
86
 | Con    (ck1, cr, l) ->
87
   let id  = Clocks.const_of_carrier cr in
88
   control_on_clock env ck1
89
     (mkinstr
90
	(MBranch (translate_ident env id,
91
		  [l, [inst]] )))
92
 | _                   -> inst
80
  match (Clocks.repr ck).cdesc with
81
  | Con (ck1, cr, l) ->
82
    let id = Clocks.const_of_carrier cr in
83
    control_on_clock env ck1
84
      (mkinstr (MBranch (translate_ident env id, [l, [inst]])))
85
  | _ -> inst
93 86

  
94 87

  
95 88
(* specialize predefined (polymorphic) operators wrt their instances,
96 89
   so that the C semantics is preserved *)
97 90
let specialize_to_c expr =
98
 match expr.expr_desc with
99
 | Expr_appl (id, e, r) ->
100
   if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e)
101
   then let id =
102
	  match id with
103
	  | "="  -> "equi"
104
	  | "!=" -> "xor"
105
	  | _    -> id in
106
	{ expr with expr_desc = Expr_appl (id, e, r) }
107
   else expr
108
 | _ -> expr
91
  match expr.expr_desc with
92
  | Expr_appl (id, e, r) ->
93
    if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e)
94
    then let id =
95
           match id with
96
           | "="  -> "equi"
97
           | "!=" -> "xor"
98
           | _    -> id in
99
      { expr with expr_desc = Expr_appl (id, e, r) }
100
    else expr
101
  | _ -> expr
109 102

  
110 103
let specialize_op expr =
111 104
  match !Options.output with
......
117 110
  let translate_expr = translate_expr env in
118 111
  let value_desc = 
119 112
    match expr.expr_desc with
120
    | Expr_const v                     -> Cst v
121
    | Expr_ident x                     -> (translate_ident env x).value_desc
122
    | Expr_array el                    -> Array (List.map translate_expr el)
123
    | Expr_access (t, i)               -> Access (translate_expr t,
124
                                                  translate_expr 
125
                                                    (expr_of_dimension i))
126
    | Expr_power  (e, n)               -> Power  (translate_expr e,
127
                                                  translate_expr
128
                                                    (expr_of_dimension n))
129
    | Expr_tuple _
130
      | Expr_arrow _ 
131
      | Expr_fby _
132
      | Expr_pre _                       -> (Printers.pp_expr
133
                                               Format.err_formatter expr;
134
                                             Format.pp_print_flush
135
                                               Format.err_formatter ();
136
                                             raise NormalizationError)
137
                                          
138
    | Expr_when    (e1, _, _)          -> (translate_expr e1).value_desc
139
    | Expr_merge   _                   -> raise NormalizationError
113
    | Expr_const v ->
114
      Cst v
115
    | Expr_ident x ->
116
      (translate_ident env x).value_desc
117
    | Expr_array el ->
118
      Array (List.map translate_expr el)
119
    | Expr_access (t, i) ->
120
      Access (translate_expr t, translate_expr (expr_of_dimension i))
121
    | Expr_power  (e, n) ->
122
      Power (translate_expr e, translate_expr (expr_of_dimension n))
123
    | Expr_when (e1, _, _) ->
124
      (translate_expr e1).value_desc
140 125
    | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
141
       let nd = node_from_name id in
142
       Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
143
    | Expr_ite (g,t,e) -> (
126
      let nd = node_from_name id in
127
      Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
128
    | Expr_ite (g,t,e) when Backends.is_functional () ->
144 129
      (* special treatment depending on the active backend. For
145 130
         functional ones, like horn backend, ite are preserved in
146 131
         expression. While they are removed for C or Java backends. *)
147
      if Backends.is_functional () then
148
	Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
149
      else 
150
	(Format.eprintf "Normalization error for backend %s: %a@."
151
	   !Options.output
152
	   Printers.pp_expr expr;
153
	 raise NormalizationError)
154
    )
155
    | _                   -> raise NormalizationError
132
      Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
133
    | _ ->
134
      Format.eprintf "Normalization error for backend %s: %a@."
135
        !Options.output
136
        Printers.pp_expr expr;
137
      raise NormalizationError
156 138
  in
157 139
  mk_val value_desc expr.expr_type
158 140

  
159 141
let translate_guard env expr =
160 142
  match expr.expr_desc with
161
  | Expr_ident x  -> translate_ident env x
162
  | _ -> (Format.eprintf "internal error: translate_guard %a@."
163
            Printers.pp_expr expr;
164
          assert false)
143
  | Expr_ident x -> translate_ident env x
144
  | _ ->
145
    Format.eprintf "internal error: translate_guard %a@." Printers.pp_expr expr;
146
    assert false
165 147

  
166 148
let rec translate_act env (y, expr) =
167 149
  let translate_act = translate_act env in
168 150
  let translate_guard = translate_guard env in
169 151
  let translate_ident = translate_ident env in
170 152
  let translate_expr = translate_expr env in
171
  let eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
153
  let lustre_eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
172 154
  match expr.expr_desc with
173
  | Expr_ite   (c, t, e) -> let g = translate_guard c in
174
			    mk_conditional ?lustre_eq:(Some eq) g
175
                              [translate_act (y, t)]
176
                              [translate_act (y, e)]
177
  | Expr_merge (x, hl)   -> mkinstr ?lustre_eq:(Some eq)
178
                              (MBranch (translate_ident x,
179
                                        List.map (fun (t,  h) ->
180
                                            t, [translate_act (y, h)])
181
                                          hl))
182
  | _                    -> mkinstr ?lustre_eq:(Some eq)
183
                              (MLocalAssign (y, translate_expr expr))
155
  | Expr_ite (c, t, e) ->
156
    mk_conditional ~lustre_eq
157
      (translate_guard c)
158
      [translate_act (y, t)]
159
      [translate_act (y, e)]
160
  | Expr_merge (x, hl) ->
161
    mkinstr ~lustre_eq
162
      (MBranch (translate_ident x,
163
                List.map (fun (t,  h) -> t, [translate_act (y, h)]) hl))
164
  | _ -> mkinstr ~lustre_eq (MLocalAssign (y, translate_expr expr))
184 165

  
185 166
let reset_instance env i r c =
186 167
  match r with
187
  | None        -> []
188
  | Some r      -> let g = translate_guard env r in
189
                   [control_on_clock
190
                      env
191
                      c
192
                      (mk_conditional
193
                         g
194
                         [mkinstr (MReset i)]
195
                         [mkinstr (MNoReset i)])
196
                   ]
168
  | Some r ->
169
    [control_on_clock env c
170
       (mk_conditional
171
          (translate_guard env r)
172
          [mkinstr (MReset i)]
173
          [mkinstr (MNoReset i)])]
174
  | None -> []
197 175

  
198 176

  
199 177
(* Datastructure updated while visiting equations *)
200 178
type machine_ctx = {
201
    m: VSet.t; (* Memories *)
202
    si: instr_t list;
203
    j: (Lustre_types.top_decl * Dimension.dim_expr list) Utils.IMap.t;
204
    s: instr_t list;
205
  }
179
  m: VSet.t; (* Memories *)
180
  si: instr_t list;
181
  j: (Lustre_types.top_decl * Dimension.dim_expr list) Utils.IMap.t;
182
  s: instr_t list;
183
}
206 184

  
207 185
let ctx_init = { m = VSet.empty; (* memories *)
208 186
                 si = []; (* init instr *)
209 187
                 j = Utils.IMap.empty;
210 188
                 s = [] }
211
             
189

  
212 190
(****************************************************************)
213 191
(* Main function to translate equations into this machine context we
214 192
   are building *) 
215 193
(****************************************************************)
216 194

  
217
                   
195

  
218 196

  
219 197
let translate_eq env ctx eq =
220 198
  let translate_expr = translate_expr env in
221 199
  let translate_act = translate_act env in
222 200
  let control_on_clock = control_on_clock env in
223 201
  let reset_instance = reset_instance env in
202
  let mkinstr' = mkinstr ~lustre_eq:eq in
203
  let ctl ?(ck=eq.eq_rhs.expr_clock) instr =
204
    control_on_clock ck (mkinstr' instr) in
224 205

  
225 206
  (* Format.eprintf "translate_eq %a with clock %a@." 
226 207
     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
227 208
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
228 209
  | [x], Expr_arrow (e1, e2)                     ->
229
     let var_x = env.get_var x in
230
     let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
231
     let c1 = translate_expr e1 in
232
     let c2 = translate_expr e2 in
233
     { ctx with
234
       si = mkinstr (MReset o) :: ctx.si;
235
       j = Utils.IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
236
       s = (control_on_clock
237
              eq.eq_rhs.expr_clock
238
              (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))
239
           ) :: ctx.s
240
     }
210
    let var_x = env.get_var x in
211
    let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
212
    let c1 = translate_expr e1 in
213
    let c2 = translate_expr e2 in
214
    { ctx with
215
      si = mkinstr (MReset o) :: ctx.si;
216
      j = Utils.IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
217
      s = ctl (MStep ([var_x], o, [c1;c2])) :: ctx.s
218
    }
241 219
  | [x], Expr_pre e1 when env.is_local x    ->
242
     let var_x = env.get_var x in
243
     
244
      { ctx with
245
        m = VSet.add var_x ctx.m;
246
        s = control_on_clock
247
              eq.eq_rhs.expr_clock
248
              (mkinstr ?lustre_eq:(Some eq)
249
                 (MStateAssign (var_x, translate_expr e1)))
250
            :: ctx.s
251
      }
220
    let var_x = env.get_var x in
221
    { ctx with
222
      m = VSet.add var_x ctx.m;
223
      s = ctl (MStateAssign (var_x, translate_expr e1)) :: ctx.s
224
    }
252 225
  | [x], Expr_fby (e1, e2) when env.is_local x ->
253
     let var_x = env.get_var x in
254
     { ctx with
255
       m = VSet.add var_x ctx.m;
256
       si = mkinstr ?lustre_eq:(Some eq)
257
              (MStateAssign (var_x, translate_expr e1))
258
            :: ctx.si;
259
       s = control_on_clock
260
             eq.eq_rhs.expr_clock
261
             (mkinstr ?lustre_eq:(Some eq)
262
                (MStateAssign (var_x, translate_expr e2)))
263
           :: ctx.s
264
     }
265

  
266
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
267
     let var_p = List.map (fun v -> env.get_var v) p in
268
     let el = expr_list_of_expr arg in
269
     let vl = List.map translate_expr el in
270
     let node_f = node_from_name f in
271
     let call_f =
272
       node_f,
273
       NodeDep.filter_static_inputs (node_inputs node_f) el in
274
     let o = new_instance node_f eq.eq_rhs.expr_tag in
275
     let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in
276
     let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in
277
     (*Clocks.new_var true in
278
       Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
279
       Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
280
     { ctx with
281
       si = 
282
         (if Stateless.check_node node_f then ctx.si else mkinstr (MReset o) :: ctx.si);
226
    let var_x = env.get_var x in
227
    { ctx with
228
      m = VSet.add var_x ctx.m;
229
      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
230
      s = ctl (MStateAssign (var_x, translate_expr e2)) :: ctx.s
231
    }
232
  | p, Expr_appl (f, arg, r)
233
    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
234
    let var_p = List.map (fun v -> env.get_var v) p in
235
    let el = expr_list_of_expr arg in
236
    let vl = List.map translate_expr el in
237
    let node_f = node_from_name f in
238
    let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in
239
    let o = new_instance node_f eq.eq_rhs.expr_tag in
240
    let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks)
241
        el [eq.eq_rhs.expr_clock] in
242
    let call_ck = Clock_calculus.compute_root_clock
243
        (Clock_predef.ck_tuple env_cks) in
244
    (*Clocks.new_var true in
245
      Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
246
      Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
247
    { ctx with
248
      si = if Stateless.check_node node_f
249
        then ctx.si else mkinstr (MReset o) :: ctx.si;
283 250
      j = Utils.IMap.add o call_f ctx.j;
284 251
      s = (if Stateless.check_node node_f
285
           then []
286
           else reset_instance o r call_ck) @
287
	    (control_on_clock call_ck
288
               (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl))))
289
            :: ctx.s
290
     }
291

  
292
  | [x], _                                       -> (
252
           then [] else reset_instance o r call_ck)
253
          @ ctl ~ck:call_ck (MStep (var_p, o, vl))
254
          :: ctx.s
255
    }
256
  | [x], _ ->
293 257
    let var_x = env.get_var x in
294 258
    { ctx with
295
      s = 
296
     control_on_clock 
297
       eq.eq_rhs.expr_clock
298
       (translate_act (var_x, eq.eq_rhs)) :: ctx.s
299
    }
300
  )
301
  | _                                            ->
302
     begin
303
       Format.eprintf "internal error: Machine_code.translate_eq %a@?"
304
         Printers.pp_node_eq eq;
305
       assert false
306
     end
307

  
308

  
259
      s = control_on_clock eq.eq_rhs.expr_clock
260
          (translate_act (var_x, eq.eq_rhs))
261
          :: ctx.s
262
      }
263
  | _ ->
264
    Format.eprintf "internal error: Machine_code.translate_eq %a@?"
265
      Printers.pp_node_eq eq;
266
    assert false
309 267

  
310 268
let constant_equations locals =
311
 VSet.fold (fun vdecl eqs ->
312
   if vdecl.var_dec_const
313
   then
314
     { eq_lhs = [vdecl.var_id];
315
       eq_rhs = Utils.desome vdecl.var_dec_value;
316
       eq_loc = vdecl.var_loc
317
     } :: eqs
318
   else eqs)
319
   locals []
269
  VSet.fold (fun vdecl eqs ->
270
      if vdecl.var_dec_const
271
      then
272
        { eq_lhs = [vdecl.var_id];
273
          eq_rhs = Utils.desome vdecl.var_dec_value;
274
          eq_loc = vdecl.var_loc
275
        } :: eqs
276
      else eqs)
277
    locals []
320 278

  
321 279
let translate_eqs env ctx eqs =
322
  List.fold_right (fun eq ctx -> translate_eq env ctx eq) eqs ctx;;
280
  List.fold_right (fun eq ctx -> translate_eq env ctx eq) eqs ctx
323 281

  
324 282

  
325 283
(****************************************************************)
......
327 285
(****************************************************************)
328 286

  
329 287
let process_asserts nd =
330
  
331
    let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
332
    if Backends.is_functional () then
333
      [], [], exprl  
334
    else (* Each assert(e) is associated to a fresh variable v and declared as
335
	    v=e; assert (v); *)
336
      let _, vars, eql, assertl =
337
	List.fold_left (fun (i, vars, eqlist, assertlist) expr ->
338
	  let loc = expr.expr_loc in
339
	  let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in
340
	  let assert_var =
341
	    mkvar_decl
342
	      loc
343
	      ~orig:false (* fresh var *)
344
	      (var_id,
345
	       mktyp loc Tydec_bool,
346
	       mkclock loc Ckdec_any,
347
	       false, (* not a constant *)
348
	       None, (* no default value *)
349
	       Some nd.node_id
350
	      )
351
	  in
352
	  assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *); 
353
	  let eq = mkeq loc ([var_id], expr) in
288

  
289
  let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
290
  if Backends.is_functional () then
291
    [], [], exprl
292
  else (* Each assert(e) is associated to a fresh variable v and declared as
293
          v=e; assert (v); *)
294
    let _, vars, eql, assertl =
295
      List.fold_left (fun (i, vars, eqlist, assertlist) expr ->
296
          let loc = expr.expr_loc in
297
          let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in
298
          let assert_var =
299
            mkvar_decl
300
              loc
301
              ~orig:false (* fresh var *)
302
              (var_id,
303
               mktyp loc Tydec_bool,
304
               mkclock loc Ckdec_any,
305
               false, (* not a constant *)
306
               None, (* no default value *)
307
               Some nd.node_id
308
              )
309
          in
310
          assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *);
311
          let eq = mkeq loc ([var_id], expr) in
354 312
          (i+1,
355 313
           assert_var::vars,
356 314
           eq::eqlist,
357 315
           {expr with expr_desc = Expr_ident var_id}::assertlist)
358
	) (1, [], [], []) exprl
359
      in
360
      vars, eql, assertl
316
        ) (1, [], [], []) exprl
317
    in
318
    vars, eql, assertl
361 319

  
362 320
let translate_core sorted_eqs locals other_vars =
363 321
  let constant_eqs = constant_equations locals in
364
  
322

  
365 323
  let env = build_env locals other_vars  in
366
  
324

  
367 325
  (* Compute constants' instructions  *)
368 326
  let ctx0 = translate_eqs env ctx_init constant_eqs in
369 327
  assert (VSet.is_empty ctx0.m);
370 328
  assert (ctx0.si = []);
371 329
  assert (Utils.IMap.is_empty ctx0.j);
372
  
330

  
373 331
  (* Compute ctx for all eqs *)
374 332
  let ctx = translate_eqs env ctx_init sorted_eqs in
375
  
333

  
376 334
  ctx, ctx0.s
377 335

  
378
 
336

  
379 337
let translate_decl nd sch =
380 338
  (* Format.eprintf "Translating node %s@." nd.node_id; *)
381 339
  (* Extracting eqs, variables ..  *)
382 340
  let eqs, auts = get_node_eqs nd in
383 341
  assert (auts = []); (* Automata should be expanded by now *)
384
  
342

  
385 343
  (* In case of non functional backend (eg. C), additional local variables have
386 344
     to be declared for each assert *)
387 345
  let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
......
393 351
  let env = build_env locals inout_vars  in 
394 352

  
395 353
  (* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)
396
  
354

  
397 355
  (* Computing main content *)
398 356
  (* Format.eprintf "ok1@.@?"; *)
399 357
  let schedule = sch.Scheduling_type.schedule in
......
403 361
   *   VSet.pp locals
404 362
   *   VSet.pp inout_vars
405 363
   * ; *)
406
  
364

  
407 365
  let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
408
  
366

  
409 367
  (* Format.eprintf "ok4@.@?"; *)
410 368

  
411 369
  (* Removing computed memories from locals. We also removed unused variables. *)
......
423 381
    mconst = ctx0_s;
424 382
    mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
425 383
    mstep = {
426
        step_inputs = nd.node_inputs;
427
        step_outputs = nd.node_outputs;
428
        step_locals = updated_locals;
429
        step_checks = List.map (fun d -> d.Dimension.dim_loc,
430
                                         translate_expr env 
431
                                           (expr_of_dimension d))
432
                        nd.node_checks;
433
        step_instrs = (
434
	  (* special treatment depending on the active backend. For horn backend,
435
	   common branches are not merged while they are in C or Java
436
	   backends. *)
437
	  if !Backends.join_guards then
438
	    join_guards_list ctx.s
439
	  else
440
	    ctx.s
441
        );
442
        step_asserts = List.map (translate_expr env) nd_node_asserts;
443
      };
384
      step_inputs = nd.node_inputs;
385
      step_outputs = nd.node_outputs;
386
      step_locals = updated_locals;
387
      step_checks = List.map (fun d -> d.Dimension.dim_loc,
388
                                       translate_expr env
389
                                         (expr_of_dimension d))
390
          nd.node_checks;
391
      step_instrs = (
392
        (* special treatment depending on the active backend. For horn backend,
393
           common branches are not merged while they are in C or Java
394
           backends. *)
395
        if !Backends.join_guards then
396
          join_guards_list ctx.s
397
        else
398
          ctx.s
399
      );
400
      step_asserts = List.map (translate_expr env) nd_node_asserts;
401
    };
444 402

  
445 403
    (* Processing spec: there is no processing performed here. Contract
446
     have been processed already. Either one of the other machine is a
447
     cocospec node, or the current one is a cocospec node. Contract do
448
     not contain any statement or import. *)
449
 
450
    mspec = nd.node_spec;
404
       have been processed already. Either one of the other machine is a
405
       cocospec node, or the current one is a cocospec node. Contract do
406
       not contain any statement or import. *)
407

  
408
    mspec = { mnode_spec = nd.node_spec; mtransitions = [] };
451 409
    mannot = nd.node_annot;
452 410
    msch = Some sch;
453 411
  }
......
457 415
  let nodes = get_nodes decls in
458 416
  let machines =
459 417
    List.map
460
    (fun decl ->
461
     let node = node_of_top decl in
462
      let sch = Utils.IMap.find node.node_id node_schs in
463
      translate_decl node sch
464
    ) nodes
418
      (fun decl ->
419
         let node = node_of_top decl in
420
         let sch = Utils.IMap.find node.node_id node_schs in
421
         translate_decl node sch
422
      ) nodes
465 423
  in
466 424
  machines
467 425

  
468
    (* Local Variables: *)
469
    (* compile-command:"make -C .." *)
470
    (* End: *)
426
(* Local Variables: *)
427
(* compile-command:"make -C .." *)
428
(* End: *)

Also available in: Unified diff