Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/checks/stateless.ml
13 13
open Corelang
14 14

  
15 15
type error =
16
| Stateful_kwd   of ident
17
| Stateful_imp   of ident
18
| Stateful_ext_C of ident
16
  | Stateful_kwd of ident
17
  | Stateful_imp of ident
18
  | Stateful_ext_C of ident
19 19

  
20 20
exception Error of Location.t * error
21 21

  
22 22
let rec check_expr expr =
23 23
  match expr.expr_desc with
24
  | Expr_const _ 
25
    | Expr_ident _ -> true
26
  | Expr_tuple el
27
    | Expr_array el -> List.for_all check_expr el
28
  | Expr_access (e1, _)
29
    | Expr_power (e1, _) -> check_expr e1
30
  | Expr_ite (c, t, e) -> check_expr c && check_expr t && check_expr e
31
  | Expr_arrow _
32
    | Expr_fby _
33
    | Expr_pre _ -> false
34
  | Expr_when (e', _, _)-> check_expr e'
35
  | Expr_merge (_, hl) -> List.for_all (fun (_, h) -> check_expr h) hl
24
  | Expr_const _ | Expr_ident _ ->
25
    true
26
  | Expr_tuple el | Expr_array el ->
27
    List.for_all check_expr el
28
  | Expr_access (e1, _) | Expr_power (e1, _) ->
29
    check_expr e1
30
  | Expr_ite (c, t, e) ->
31
    check_expr c && check_expr t && check_expr e
32
  | Expr_arrow _ | Expr_fby _ | Expr_pre _ ->
33
    false
34
  | Expr_when (e', _, _) ->
35
    check_expr e'
36
  | Expr_merge (_, hl) ->
37
    List.for_all (fun (_, h) -> check_expr h) hl
36 38
  | Expr_appl (i, e', i') ->
37
     let reset_opt = (match i' with None -> true | Some e'' -> check_expr e'') in
38
     let stateless_node =
39
       (Basic_library.is_stateless_fun i || (
40
          try
41
            check_node (node_from_name i)
42
          with Not_found ->
43
            let loc = expr.expr_loc in
44
            Error.pp_error loc (fun fmt -> Format.fprintf fmt "Unable to find node %s in expression %a" i Printers.pp_expr expr);
45
            raise (Error.Error (loc, Error.Unbound_symbol i))
46
       ))
47
     in
48
     (* Warning message when trying to reset a stateless node *)
49
     if stateless_node && not reset_opt then
50
       Error.pp_warning expr.expr_loc (fun fmt -> Format.fprintf fmt "Trying to reset call the stateless node or op %s" i)
51
     ;
52
     check_expr e' && reset_opt && stateless_node
53
     
54
and compute_node nd = (* returns true iff the node is stateless.*)
39
    let reset_opt = match i' with None -> true | Some e'' -> check_expr e'' in
40
    let stateless_node =
41
      Basic_library.is_stateless_fun i
42
      ||
43
      try check_node (node_from_name i)
44
      with Not_found ->
45
        let loc = expr.expr_loc in
46
        Error.pp_error loc (fun fmt ->
47
            Format.fprintf fmt "Unable to find node %s in expression %a" i
48
              Printers.pp_expr expr);
49
        raise (Error.Error (loc, Error.Unbound_symbol i))
50
    in
51
    (* Warning message when trying to reset a stateless node *)
52
    if stateless_node && not reset_opt then
53
      Error.pp_warning expr.expr_loc (fun fmt ->
54
          Format.fprintf fmt "Trying to reset call the stateless node or op %s"
55
            i);
56
    check_expr e' && reset_opt && stateless_node
57

  
58
and compute_node nd =
59
  (* returns true iff the node is stateless.*)
55 60
  let eqs, aut = get_node_eqs nd in
56
  aut = [] && (* A node containinig an automaton will be stateful *)
57
    List.for_all (fun eq -> check_expr eq.eq_rhs) eqs
61
  aut = []
62
  && (* A node containinig an automaton will be stateful *)
63
  List.for_all (fun eq -> check_expr eq.eq_rhs) eqs
64

  
58 65
and check_node td =
59
  match td.top_decl_desc with 
60
  | Node nd         -> (
66
  match td.top_decl_desc with
67
  | Node nd -> (
61 68
    match nd.node_stateless with
62
    | None     -> 
63
       begin
64
	 let stateless = compute_node nd in
65
	 nd.node_stateless <- Some stateless;
66
	 if nd.node_dec_stateless && (not stateless)
67
	 then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id))
68
	 else (nd.node_dec_stateless <- stateless; stateless)
69
       end
70
    | Some stl -> stl)
69
    | None ->
70
      let stateless = compute_node nd in
71
      nd.node_stateless <- Some stateless;
72
      if nd.node_dec_stateless && not stateless then
73
        raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id))
74
      else (
75
        nd.node_dec_stateless <- stateless;
76
        stateless)
77
    | Some stl ->
78
      stl)
71 79
  | ImportedNode nd ->
72
     begin
73
       (if nd.nodei_prototype = Some "C" && not nd.nodei_stateless
74
	then raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id)));
75
       nd.nodei_stateless
76
     end
77
  | _ -> true
78

  
79
let check_prog decls =
80
  List.iter (fun td -> ignore (check_node td)) decls
80
    if nd.nodei_prototype = Some "C" && not nd.nodei_stateless then
81
      raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id));
82
    nd.nodei_stateless
83
  | _ ->
84
    true
81 85

  
86
let check_prog decls = List.iter (fun td -> ignore (check_node td)) decls
82 87

  
83 88
let force_prog decls =
84 89
  let force_node td =
85
    match td.top_decl_desc with 
86
    | Node nd         -> (
90
    match td.top_decl_desc with
91
    | Node nd ->
87 92
      nd.node_dec_stateless <- false;
88
      nd.node_stateless <- Some false)
89
    | _ -> ()
93
      nd.node_stateless <- Some false
94
    | _ ->
95
      ()
90 96
  in
91 97
  List.iter (fun td -> ignore (force_node td)) decls
92 98

  
93 99
let check_compat_decl decl =
94 100
  match decl.top_decl_desc with
95
  | ImportedNode nd -> (* A node declared in the header (lusi) shall
96
                          be locally defined with compatible stateless
97
                          flag *)
98
     begin
99
       let td = Corelang.node_from_name nd.nodei_id in
100
       (match td.top_decl_desc with
101
        | Node nd' -> let stateless = check_node td in
102
		      if nd.nodei_stateless && (not stateless)
103
		      then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))
104
		      else nd'.node_dec_stateless <- nd.nodei_stateless
105
        | _        -> assert false)
106
     end
101
  | ImportedNode nd -> (
102
    (* A node declared in the header (lusi) shall be locally defined with
103
       compatible stateless flag *)
104
    let td = Corelang.node_from_name nd.nodei_id in
105
    match td.top_decl_desc with
106
    | Node nd' ->
107
      let stateless = check_node td in
108
      if nd.nodei_stateless && not stateless then
109
        raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))
110
      else nd'.node_dec_stateless <- nd.nodei_stateless
111
    | _ ->
112
      assert false)
107 113
  | Node nd -> (
108
     match nd.node_spec with
109
       Some (Contract _) -> (* A contract element in a header does not
110
                               need to be provided in the associed lus
111
                               file *)
112
        ()
113
     | _ -> assert false)
114
             
115
  | _               -> ()
114
    match nd.node_spec with
115
    | Some (Contract _) ->
116
      (* A contract element in a header does not need to be provided in the
117
         associed lus file *)
118
      ()
119
    | _ ->
120
      assert false)
121
  | _ ->
122
    ()
116 123

  
117
let check_compat header =
118
  List.iter check_compat_decl header
124
let check_compat header = List.iter check_compat_decl header
119 125

  
120 126
let pp_error fmt err =
121 127
  match err with
122 128
  | Stateful_kwd nd ->
123
     Format.fprintf fmt
124
       "node %s should be stateless but is actually stateful.@."
125
       nd
129
    Format.fprintf fmt "node %s should be stateless but is actually stateful.@."
130
      nd
126 131
  | Stateful_imp nd ->
127
     Format.fprintf fmt
128
       "node %s is declared stateless but is actually stateful.@."
129
       nd
132
    Format.fprintf fmt
133
      "node %s is declared stateless but is actually stateful.@." nd
130 134
  | Stateful_ext_C nd ->
131
     Format.fprintf fmt
132
       "node %s with declared prototype C cannot be stateful, it has to be a function.@."
133
       nd
135
    Format.fprintf fmt
136
      "node %s with declared prototype C cannot be stateful, it has to be a \
137
       function.@."
138
      nd
134 139

  
135 140
(* Local Variables: *)
136 141
(* compile-command:"make -C .." *)

Also available in: Unified diff