1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11structure StmtDeclDatatype =
12struct
13
14type expr = Expr.expr
15type initializer = Expr.initializer
16type 'a ctype = 'a CType.ctype
17type 'a wrap = 'a RegionExtras.wrap
18datatype gcc_attribute = GCC_AttribID of string
19                       | GCC_AttribFn of string * expr list
20                       | OWNED_BY of string
21
22datatype fnspec = fnspec of string wrap
23                | relspec of string wrap
24                | fn_modifies of string list
25                | didnt_translate
26                | gcc_attribs of gcc_attribute list
27
28datatype storage_class =
29         SC_EXTERN | SC_STATIC | SC_AUTO | SC_REGISTER | SC_THRD_LOCAL
30
31datatype declaration =
32         VarDecl of (expr ctype *
33                     string wrap *
34                     storage_class list *
35                     initializer option *
36                     gcc_attribute list)
37         (* VarDecl's bool is true if the declaration is not an extern;
38            if the declaration is "genuine".
39            The accompanying optional initialiser is only used to calculate the
40            size of an array when a declaration like
41              int a[] = {...}
42            is made.
43            Initialisers are translated into subsequent assignment statements
44            by the parser. *)
45       | StructDecl of string wrap * (expr ctype * string wrap) list
46       | TypeDecl of (expr ctype * string wrap) list
47       | ExtFnDecl of {rettype : expr ctype, name : string wrap,
48                       params : (expr ctype * string option) list,
49                       specs : fnspec list}
50       | EnumDecl of string option wrap * (string wrap * expr option) list
51
52type namedstringexp = string option * string * expr
53
54type asmblock = {head : string,
55                 mod1 : namedstringexp list,
56                 mod2 : namedstringexp list,
57                 mod3 : string list}
58(* if mod_i is empty, then so too are all mod_j for j > i *)
59
60datatype trappable = BreakT | ContinueT
61
62
63datatype statement_node =
64         Assign of expr * expr
65       | AssignFnCall of expr option * expr * expr list (* lval, fn, args *)
66       | Chaos of expr
67       | EmbFnCall of expr * expr * expr list (* lval, fn, args *)
68       | Block of block_item list
69       | While of expr * string wrap option * statement
70       | Trap of trappable * statement
71       | Return of expr option
72       | ReturnFnCall of expr * expr list
73       | Break | Continue
74       | IfStmt of expr * statement * statement
75       | Switch of expr * (expr option list * block_item list) list
76       | EmptyStmt
77       | Auxupd of string
78       | Ghostupd of string
79       | Spec of ((string * string) * statement list * string)
80       | AsmStmt of {volatilep : bool, asmblock : asmblock}
81       | LocalInit of expr
82and statement = Stmt of statement_node Region.Wrap.t
83and block_item =
84    BI_Stmt of statement
85  | BI_Decl of declaration wrap
86
87type body = block_item list wrap
88
89datatype ext_decl =
90         FnDefn of (expr ctype * string wrap) * (expr ctype * string wrap) list *
91                   fnspec list (* fnspec *) * body
92       | Decl of declaration wrap
93
94end
95
96signature STMT_DECL =
97sig
98  datatype gcc_attribute = datatype StmtDeclDatatype.gcc_attribute
99  datatype storage_class = datatype StmtDeclDatatype.storage_class
100  datatype fnspec = datatype StmtDeclDatatype.fnspec
101  datatype declaration = datatype StmtDeclDatatype.declaration
102  datatype trappable = datatype StmtDeclDatatype.trappable
103  datatype statement_node = datatype StmtDeclDatatype.statement_node
104  type statement
105  type asmblock = StmtDeclDatatype.asmblock
106  type namedstringexp = StmtDeclDatatype.namedstringexp
107  datatype block_item = datatype StmtDeclDatatype.block_item
108  datatype ext_decl = datatype StmtDeclDatatype.ext_decl
109
110  val merge_specs : fnspec list -> fnspec list -> fnspec list
111  val has_IDattribute : (string -> bool) -> fnspec list -> string option
112  val all_IDattributes : fnspec list -> string Binaryset.set
113  val get_owned_by : gcc_attribute list -> string option
114  val fnspec2string : fnspec -> string
115
116  val snode : statement -> statement_node
117  val swrap : statement_node * SourcePos.t * SourcePos.t -> statement
118  val sbogwrap : statement_node -> statement
119  val sleft : statement -> SourcePos.t
120  val sright : statement -> SourcePos.t
121
122  val stmt_type : statement -> string
123
124  val stmt_fail : statement * string -> exn
125
126  val is_extern : storage_class list -> bool
127  val is_static : storage_class list -> bool
128
129  val sub_stmts : statement -> statement list
130
131end
132
133structure StmtDecl : STMT_DECL =
134struct
135
136open StmtDeclDatatype RegionExtras Expr
137
138fun attr2string (GCC_AttribID s) = s
139  | attr2string (GCC_AttribFn(s, _)) = s ^ "(...)"
140  | attr2string (OWNED_BY s) = "[OWNED_BY "^s^"]"
141
142fun has_IDattribute P fspecs = let
143  val search_gccattrs = get_first
144                            (fn GCC_AttribID s => if P s then SOME s else NONE
145                              | _ => NONE)
146  fun oneP fspec =
147      case fspec of
148        gcc_attribs attrs => search_gccattrs attrs
149      | _ => NONE
150in
151  get_first oneP fspecs
152end
153
154fun all_IDattributes fspecs = let
155  fun getID (GCC_AttribID s, acc) = Binaryset.add(acc,s) | getID (_,acc) = acc
156  fun getGCCs (gcc_attribs attrs, acc) = List.foldl getID acc attrs
157    | getGCCs (_,acc) = acc
158in
159  List.foldl getGCCs (Binaryset.empty String.compare) fspecs
160end
161
162fun get_owned_by gattrs =
163    case gattrs of
164        [] => NONE
165      | OWNED_BY s :: _ => SOME s
166      | _ :: rest => get_owned_by rest
167
168
169
170val commas = String.concat o separate ","
171fun fnspec2string fs =
172    case fs of
173      fnspec s => "fnspec: "^node s
174    | fn_modifies slist => "MODIFIES: "^String.concat (separate " " slist)
175    | didnt_translate => "DONT_TRANSLATE"
176    | gcc_attribs attrs => "__attribute__((" ^ commas (map attr2string attrs) ^
177                           "))"
178    | relspec s => "relspec: "^node s
179
180
181fun collapse_mod_attribs sp = let
182  local
183    open Binaryset
184  in
185  fun IL (NONE, slist) = SOME (addList(empty String.compare, slist))
186    | IL (SOME s, slist) = SOME (addList(s, slist))
187  end
188  fun recurse (acc as (mods, attribs, specs)) sp =
189      case sp of
190        [] => acc
191      | s :: rest => let
192        in
193          case s of
194            fn_modifies slist => recurse (IL (mods, slist), attribs, specs) rest
195          | gcc_attribs gs => recurse (mods, Library.union op= gs attribs,
196                                       specs)
197                                      rest
198          | _ => recurse (mods, attribs, s::specs) rest
199        end
200  val (mods, attribs, specs) = recurse (NONE, [], []) sp
201  val mods = Option.map Binaryset.listItems mods
202  val mods' = case mods of NONE => [] | SOME l => [fn_modifies l]
203  val attribs' = case attribs of [] => [] | _ => [gcc_attribs attribs]
204in
205  mods' @ attribs' @ specs
206end
207
208fun merge_specs sp1 sp2 = collapse_mod_attribs (sp1 @ sp2)
209
210
211fun sleft (Stmt w) = left w
212fun sright (Stmt w) = right w
213fun swrap (s, l, r) = Stmt(wrap(s,l,r))
214fun snode (Stmt w) = node w
215fun sbogwrap s = Stmt(wrap(s,bogus,bogus))
216
217fun stmt_type s =
218    case snode s of
219      Assign _ => "Assign"
220    | AssignFnCall _ => "AssignFnCall"
221    | EmbFnCall _ => "EmbFnCall"
222    | Block _ => "Block"
223    | Chaos _ => "Chaos"
224    | While _ => "While"
225    | Trap _ => "Trap"
226    | Return _ => "Return"
227    | ReturnFnCall _ => "ReturnFnCall"
228    | Break => "Break"
229    | Continue => "Continue"
230    | IfStmt _ => "IfStmt"
231    | Switch _ => "Switch"
232    | EmptyStmt => "EmptyStmt"
233    | Auxupd _ => "Auxupd"
234    | Spec _ => "Spec"
235    | AsmStmt _ => "AsmStmt"
236    | LocalInit _ => "LocalInit"
237    | _ => "[whoa!  Unknown stmt type]"
238
239fun map_concat f ss = map f ss |> List.concat
240
241fun sub_stmts s =
242    case snode s of
243      Block bis => map_concat bi_stmts bis
244    | While (_, _, s) => [s]
245    | Trap (_, s) => [s]
246    | IfStmt (_, l, r) => [l, r]
247    | Switch (_, sws) => map_concat (map_concat bi_stmts o snd) sws
248    | Spec (_, ss, _) => ss
249    | _ => []
250and bi_stmts (BI_Stmt s) = sub_stmts s
251  | bi_stmts _ = []
252
253fun stmt_fail (Stmt w, msg) =
254    Fail (Region.toString (Region.Wrap.region w) ^ ": " ^ msg)
255
256val is_extern = List.exists (fn x => x = SC_EXTERN)
257val is_static = List.exists (fn x => x = SC_STATIC)
258
259end
260