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