Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / stateless.ml @ e135421f

History | View | Annotate | Download (3.26 KB)

1
(* ----------------------------------------------------------------------------
2
 * SchedMCore - A MultiCore Scheduling Framework
3
 * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4
 *
5
 * This file is part of Prelude
6
 *
7
 * Prelude is free software; you can redistribute it and/or
8
 * modify it under the terms of the GNU Lesser General Public License
9
 * as published by the Free Software Foundation ; either version 2 of
10
 * the License, or (at your option) any later version.
11
 *
12
 * Prelude is distributed in the hope that it will be useful, but
13
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15
 * Lesser General Public License for more details.
16
 *
17
 * You should have received a copy of the GNU Lesser General Public
18
 * License along with this program ; if not, write to the Free Software
19
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
20
 * USA
21
 *---------------------------------------------------------------------------- *)
22
open Corelang
23

    
24
type error =
25
| Stateful_kwd of ident
26
| Stateful_imp of ident
27

    
28
exception Error of Location.t * error
29

    
30
let rec check_expr expr =
31
  match expr.expr_desc with
32
  | Expr_const _ 
33
  | Expr_ident _ -> true
34
  | Expr_tuple el
35
  | Expr_array el -> List.for_all check_expr el
36
  | Expr_access (e1, _)
37
  | Expr_power (e1, _) -> check_expr e1
38
  | Expr_ite (c, t, e) -> check_expr c && check_expr t && check_expr e
39
  | Expr_arrow _
40
  | Expr_fby _
41
  | Expr_pre _ -> false
42
  | Expr_when (e', i, l)-> check_expr e'
43
  | Expr_merge (i, hl) -> List.for_all (fun (t, h) -> check_expr h) hl 
44
  | Expr_appl (i, e', i') ->
45
    check_expr e' &&
46
      (Basic_library.is_internal_fun i || check_node (node_from_name i))
47
  | Expr_uclock _
48
  | Expr_dclock _
49
  | Expr_phclock _ -> assert false
50
and compute_node nd =
51
 List.for_all (fun eq -> check_expr eq.eq_rhs) nd.node_eqs
52
and check_node td =
53
  match td.top_decl_desc with 
54
  | Node nd         -> (
55
    match nd.node_stateless with
56
    | None     -> 
57
      begin
58
	let stateless = compute_node nd in
59
	nd.node_stateless <- Some stateless;
60
	if nd.node_dec_stateless && (not stateless)
61
	then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id))
62
	else (nd.node_dec_stateless <- stateless; stateless)
63
      end
64
    | Some stl -> stl)
65
  | ImportedNode nd -> nd.nodei_stateless
66
  | _ -> true
67

    
68
let check_prog decls =
69
  List.iter (fun td -> ignore (check_node td)) decls
70

    
71
let check_compat_decl decl =
72
 match decl.top_decl_desc with
73
 | ImportedNode nd ->
74
   let td = Corelang.node_from_name nd.nodei_id in
75
   (match td.top_decl_desc with
76
   | Node nd' -> let stateless = check_node td in
77
		 if nd.nodei_stateless && (not stateless)
78
		 then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))
79
		 else nd'.node_dec_stateless <- nd.nodei_stateless
80
   | _        -> assert false)
81
 | Node _          -> assert false
82
 | _               -> ()
83

    
84
let check_compat header =
85
  List.iter check_compat_decl header
86

    
87
let pp_error fmt err =
88
  match err with
89
  | Stateful_kwd nd ->
90
    Format.fprintf fmt
91
      "node %s should be stateless but is actually stateful.@."
92
      nd
93
  | Stateful_imp nd ->
94
    Format.fprintf fmt
95
      "node %s is declared stateless but is actually stateful.@."
96
      nd
97

    
98
(* Local Variables: *)
99
(* compile-command:"make -C .." *)
100
(* End: *)