Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / access.ml @ 22fe1c93

History | View | Annotate | Download (3.92 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

    
23
(** Access checking module. Done after typing. Generates dimension constraints stored in nodes *)
24

    
25
let debug fmt args = () (* Format.eprintf "%a"  *)
26
(* Though it shares similarities with the clock calculus module, no code
27
    is shared.  Simple environments, very limited identifier scoping, no
28
    identifier redefinition allowed. *)
29

    
30
open Utils
31
(* Yes, opening both modules is dirty as some type names will be
32
   overwritten, yet this makes notations far lighter.*)
33
open LustreSpec
34
open Corelang
35
open Types
36
open Format
37

    
38
module ConstraintModule =
39
struct (* bool dimension module *)
40
  type t = Dimension.dim_expr
41
  let equal d1 d2 = Dimension.is_eq_dimension d1 d2
42
  let compare d1 d2 = if equal d1 d2 then 0 else compare d1.Dimension.dim_id d2.Dimension.dim_id
43
  let hash n = Hashtbl.hash n
44
end
45

    
46
module CSet = Set.Make(ConstraintModule)
47

    
48
(** [check_expr env expr] checks expression [expr] and gathers constraints 
49
    in set [checks]. *)
50
let rec check_expr checks expr =
51
  (*Format.eprintf "check_expr %a with type %a@." Printers.pp_expr expr Types.print_ty expr.expr_type;*)
52
  let res = 
53
  match expr.expr_desc with
54
  | Expr_const _
55
  | Expr_ident _ -> checks
56
  | Expr_array elist -> List.fold_left check_expr checks elist
57
  | Expr_access (e1, d) -> check_expr (CSet.add (Dimension.check_access expr.expr_loc (Types.array_type_dimension e1.expr_type) d) checks) e1
58
    (* TODO: check dimensions *)
59
 
60
  | Expr_power (e1, _) -> check_expr checks e1
61
 
62
  | Expr_tuple elist -> List.fold_left check_expr checks elist
63

    
64
  | Expr_ite (c, t, e) -> List.fold_left check_expr checks [c; t; e]
65
 
66
  | Expr_appl (_, args, _) -> check_expr checks args
67
 
68
  | Expr_fby (e1,e2)
69
  | Expr_arrow (e1,e2) -> check_expr (check_expr checks e1) e2
70
  | Expr_pre e1
71
  | Expr_when (e1,_,_) -> check_expr checks e1
72
 
73
  | Expr_merge (_,hl) -> List.fold_left (fun checks (l, h) -> check_expr checks h) checks hl
74
  | _ -> assert false
75
  in (*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr Location.pp_loc expr.expr_loc Types.print_ty res;*) res
76

    
77
let rec check_var_decl_type loc checks ty =
78
  if Types.is_array_type ty
79
  then
80
    check_var_decl_type loc
81
      (CSet.add (Dimension.check_bound loc (Types.array_type_dimension ty)) checks)
82
      (Types.array_element_type ty) 
83
  else checks
84

    
85
let check_var_decl checks vdecl =
86
  check_var_decl_type vdecl.var_loc checks vdecl.var_type
87

    
88
(** [check_node nd] checks node [nd]. 
89
    The resulting constraints are stored in nodes. *)
90
let check_node nd =
91
  let checks = CSet.empty in
92
  let checks =
93
    List.fold_left check_var_decl checks (node_vars nd) in
94
  let checks =
95
    List.fold_left (fun checks eq -> check_expr checks eq.eq_rhs) checks nd.node_eqs in
96
  nd.node_checks <- CSet.elements checks
97

    
98
let check_top_decl decl =
99
  match decl.top_decl_desc with
100
  | Node nd -> check_node nd
101
  | _ -> ()
102

    
103
let check_prog decls =
104
  List.iter check_top_decl decls
105

    
106

    
107
(* Local Variables: *)
108
(* compile-command:"make -C .." *)
109
(* End: *)