Project

General

Profile

Revision f4cba4b8 src/compiler_common.ml

View differences:

src/compiler_common.ml
187 187
      Location.pp_loc loc;
188 188
    raise exc
189 189

  
190
(* Process each node/imported node and introduce the associated contract node *)
191
let resolve_contracts prog =
192
  (* Bind a fresh node with a new name according to existing nodes and freshly binded contract node. Clean the contract to remove the stmts  *)
193
  let process_contract new_contracts prog c =
194
    (* Resolve first the imports *)
195
    let stmts, locals, c =
196
      List.fold_left (
197
          fun (stmts, locals, c) import ->
198
          (* Search for contract in prog.
199
             The node have to be processed already. Otherwise raise an error.
200
             Each stmts in injected with a fresh name
201
             Inputs are renamed and associated to the expression in1
202
             Same thing for outputs.
190 203

  
204
             Last the contracts elements are replaced with the renamed vars and merged with c contract.
205
           *)
206
          let name = import.import_nodeid in
207
          assert false; (* TODO: we do not handle imports yet.  The
208
                           algorithm is sketched below *)
209
        (*
210
          try
211
            let imp_nd = xxx in (* Get the contract node in prog *)
212
            (* checking that it's actually a (processed) contract *)
213
            let imp_c =
214
              match imp_nd.node_spec with
215
                Some (Contract imp_c) ->
216
                 if imp_c.imports = [] then
217
                   imp_c
218
                 else
219
                   assert false (* should be processed *)
220
              | _ -> assert false (* should be a contract *)
221
            in  
222
            (* Preparing vars: renaming them *)
223
            let imp_in = rename imp_nd.node_inputs in
224
            let imp_out = rename imp_nd.node_outputs in
225
            let imp_locals = rename imp_nd.node_locals in
226
            let locals = imp_in@imp_out@imp_locals@locals in
227
            (* Assinging in and out *)
228
            let in_assigns =
229
              xxx imp_in = import.inputs
230
            in
231
            let out_assigns =
232
              xxx imp_out = import.outputs
233
            in
234
            let stmts = stmts @ (rename imp_nd.stmts) in
235
            let imp_c = rename imp_c in
236
            let c = merge_contracts c imp_c in
237
            stmts, locals, c 
238
          with Not_found -> raise (Error.Unbound_symbol ("contract " ^ name))
239

  
240
                            *)
241
        ) ([], c.consts@c.locals, c) c.imports
242
    in
243
    (* Other contract elements will be normalized later *)
244
    let c = { c with
245
              locals = [];
246
              consts = [];
247
              stmts = [];
248
              imports = []
249
            }
250
    in
251
    stmts, locals, c
252
    
253
  in
254
  let process_contract_new_node accu_contracts prog top =
255
    let id, spec, inputs, outputs =
256
      match top.top_decl_desc with
257
      | Node nd -> nd.node_id, nd.node_spec, nd.node_inputs, nd.node_outputs
258
      | ImportedNode ind -> ind.nodei_id, ind.nodei_spec, ind.nodei_inputs, ind.nodei_outputs
259
      | _ -> assert false
260
    in
261
    let stmts, locals, c =
262
      match spec with
263
      | None | Some (NodeSpec _) -> assert false
264
      | Some (Contract c) ->
265
         process_contract accu_contracts prog c
266
    in
267
    (* Create a fresh name *)
268
    let used v = List.exists (fun top ->
269
                     match top.top_decl_desc with
270
                     | Node _
271
                       | ImportedNode _ ->
272
                        (node_name top) = v
273
                     | _ -> false
274
                   ) (accu_contracts@prog)
275
    in
276
    let new_nd_id = mk_new_name used (id ^ "_coco") in
277
    let new_nd =
278
      mktop_decl
279
        c.spec_loc
280
        top.top_decl_owner
281
        top.top_decl_itf
282
      (Node {
283
           node_id = new_nd_id;
284
	   node_type = Types.new_var ();
285
	   node_clock = Clocks.new_var true;
286
	   node_inputs = inputs;
287
	   node_outputs = outputs;
288
	   node_locals = locals;
289
	   node_gencalls = [];
290
	   node_checks = [];
291
	   node_asserts = []; 
292
	   node_stmts = stmts;
293
	   node_dec_stateless = false;
294
	   node_stateless = None;
295
	   node_spec = Some (Contract c);
296
	   node_annot = [];
297
	   node_iscontract = true;
298
      }) in
299
    new_nd
300
  in
301
  (* Processing nodes in order. Should have been sorted by now
302

  
303
     Each top level contract is processed: stmts pushed in node
304

  
305
     Each regular imported node or node associated with a contract is
306
     replaced with a simplidfied contract and its contract is bound to
307
     a fresh node.
308

  
309
   *)
310
  let new_contracts, prog =
311
    List.fold_left
312
      (
313
        fun (accu_contracts, accu_nodes) top ->
314
        match top.top_decl_desc with
315
          
316
        | Node nd when nd.node_iscontract -> (
317
          match nd.node_spec with
318
          | None | Some (NodeSpec _) -> assert false
319
          | Some (Contract c) ->
320
             let stmts, locals, c = process_contract accu_contracts prog c in
321
             let nd =
322
               { nd with
323
                 node_locals = nd.node_locals @ locals;
324
                 node_stmts = nd.node_stmts @ stmts;
325
                 node_spec = Some (Contract c);
326
               }
327
             in
328
             { top with top_decl_desc = Node nd }::accu_contracts,
329
             accu_nodes
330
             
331
        )
332
        | Node nd -> (
333
          match nd.node_spec with
334
          | None -> accu_contracts, top::accu_nodes (* A boring node: no contract *)
335
          | Some (NodeSpec id) -> (* shall not happen, its too early *)
336
             assert false
337
          | Some (Contract c) -> (* A contract: processing it *)
338
             (* we bind a fresh node *)
339
             let new_nd = process_contract_new_node accu_contracts prog top in
340
             Format.eprintf "Creating new contract node %s@." (node_name new_nd);
341
             let nd = { nd with node_spec = (Some (NodeSpec (node_name new_nd))) } in
342
             new_nd::accu_contracts,
343
             { top with top_decl_desc = Node nd }::accu_nodes
344
             
345
        )
346
                   
347
        | ImportedNode ind -> ( (* Similar treatment for imported nodes *)
348
          match ind.nodei_spec with
349
            None -> accu_contracts, top::accu_nodes (* A boring node: no contract *)
350
          | Some (NodeSpec id) -> (* shall not happen, its too early *)
351
             assert false
352
          | Some (Contract c) -> (* A contract: processing it *)
353
             (* we bind a fresh node *)
354
             let new_nd = process_contract_new_node accu_contracts prog top in
355
             let ind = { ind with nodei_spec = (Some (NodeSpec (node_name new_nd))) } in
356
             new_nd::accu_contracts,
357
             { top with top_decl_desc = ImportedNode ind }::accu_nodes
358
        )
359
        | _ -> accu_contracts, top::accu_nodes
360
      ) ([],[]) prog
361
  in
362
  (List.rev new_contracts) @ (List.rev prog)
363
         
364

  
365
  
191 366
let track_exception () =
192 367
  if !Options.track_exceptions
193 368
  then (Printexc.print_backtrace stdout; flush stdout)

Also available in: Unified diff