[2620] | 1 | (* Based on the prototype --- expect some obsolete definitions to be present *) |
---|
| 2 | |
---|
| 3 | open Printf |
---|
| 4 | |
---|
| 5 | open Cparser |
---|
| 6 | open Cparser.C |
---|
| 7 | open Cparser.Env |
---|
| 8 | |
---|
| 9 | open Extracted.Csyntax |
---|
| 10 | open Extracted.AST |
---|
| 11 | open Extracted.Vector |
---|
| 12 | open Extracted.BitVector |
---|
| 13 | |
---|
| 14 | (* Integer conversion *) |
---|
| 15 | |
---|
| 16 | let rec convertIntNat n = |
---|
| 17 | if n = 0 then Extracted.Nat.O else Extracted.Nat.S (convertIntNat (n-1)) |
---|
| 18 | |
---|
| 19 | let rec convertInt64Nat n = |
---|
| 20 | if n = Int64.zero then Extracted.Nat.O else Extracted.Nat.S (convertInt64Nat (Int64.pred n)) |
---|
| 21 | |
---|
| 22 | let convertBool = function |
---|
| 23 | | true -> Extracted.Bool.True |
---|
| 24 | | false -> Extracted.Bool.False |
---|
| 25 | |
---|
| 26 | let rec convertIntBV len n = |
---|
| 27 | match len with |
---|
| 28 | | 0 -> VEmpty |
---|
| 29 | | _ -> let l = len -1 in VCons (convertIntNat l, convertBool (Int64.logand n (Int64.shift_left Int64.one l) <> Int64.zero), convertIntBV l n) |
---|
| 30 | |
---|
| 31 | let convertInt sz n = |
---|
| 32 | convertIntBV (match sz with I8 -> 8 | I16 -> 16 | I32 -> 32) n |
---|
| 33 | |
---|
| 34 | (** Extract the type part of a type-annotated Clight expression. *) |
---|
| 35 | |
---|
| 36 | let typeof e = match e with Expr(_,te) -> te |
---|
| 37 | |
---|
| 38 | (** Natural alignment of a type, in bytes. *) |
---|
| 39 | let rec alignof = function |
---|
| 40 | | Tvoid -> 1 |
---|
| 41 | | Tint (I8,_) -> 1 |
---|
| 42 | | Tint (I16,_) -> 2 |
---|
| 43 | | Tint (I32,_) -> 4 |
---|
| 44 | (*| Tfloat F32 -> 4 |
---|
| 45 | | Tfloat F64 -> 8*) |
---|
| 46 | | Tpointer _ -> 4 |
---|
| 47 | | Tarray (t',n) -> alignof t' |
---|
| 48 | | Tfunction (_,_) -> 1 |
---|
| 49 | | Tstruct (_,fld) -> alignof_fields fld |
---|
| 50 | | Tunion (_,fld) -> alignof_fields fld |
---|
| 51 | | Tcomp_ptr _ -> 4 |
---|
| 52 | and alignof_fields = function |
---|
| 53 | | Fnil -> 1 |
---|
| 54 | | Fcons (id,t, f') -> max (alignof t) (alignof_fields f') |
---|
| 55 | |
---|
| 56 | (** Size of a type, in bytes. *) |
---|
| 57 | |
---|
| 58 | let align n amount = |
---|
| 59 | ((n + amount - 1) / amount) * amount |
---|
| 60 | |
---|
| 61 | let int_of_nat n = |
---|
| 62 | let rec aux n i = |
---|
| 63 | match n with |
---|
| 64 | | Extracted.Nat.O -> i |
---|
| 65 | | Extracted.Nat.S m -> aux m (i+1) |
---|
| 66 | in aux n 0 |
---|
| 67 | |
---|
| 68 | let rec sizeof t = |
---|
| 69 | match t with |
---|
| 70 | | Tvoid -> 1 |
---|
| 71 | | Tint (I8,_) -> 1 |
---|
| 72 | | Tint (I16,_) -> 2 |
---|
| 73 | | Tint (I32,_) -> 4 |
---|
| 74 | (* | Tfloat F32 -> 4 |
---|
| 75 | | Tfloat F64 -> 8*) |
---|
| 76 | | Tpointer _ -> 4 |
---|
| 77 | | Tarray (t',n) -> sizeof t' * max 1 (int_of_nat n) |
---|
| 78 | | Tfunction (_,_) -> 1 |
---|
| 79 | | Tstruct (_,fld) -> align (max 1 (sizeof_struct fld 0)) (alignof t) |
---|
| 80 | | Tunion (_,fld) -> align (max 1 (sizeof_union fld)) (alignof t) |
---|
| 81 | | Tcomp_ptr _ -> 4 |
---|
| 82 | and sizeof_struct fld pos = |
---|
| 83 | match fld with |
---|
| 84 | | Fnil -> pos |
---|
| 85 | | Fcons (id,t, fld') -> sizeof_struct fld' (align pos (alignof t) + sizeof t) |
---|
| 86 | and sizeof_union = function |
---|
| 87 | | Fnil -> 0 |
---|
| 88 | | Fcons (id,t, fld') -> max (sizeof t) (sizeof_union fld') |
---|
| 89 | |
---|
| 90 | (** Record the declarations of global variables and associate them |
---|
| 91 | with the corresponding atom. *) |
---|
| 92 | |
---|
| 93 | let decl_atom : (ident, Env.t * C.decl) Hashtbl.t = Hashtbl.create 103 |
---|
| 94 | |
---|
| 95 | (** Hooks -- overriden in machine-dependent CPragmas module *) |
---|
| 96 | |
---|
| 97 | let process_pragma_hook = ref (fun (s: string) -> false) |
---|
| 98 | let define_variable_hook = ref (fun (id: ident) (d: C.decl) -> ()) |
---|
| 99 | let define_function_hook = ref (fun (id: ident) (d: C.decl) -> ()) |
---|
| 100 | let define_stringlit_hook = ref (fun (id: ident) -> ()) |
---|
| 101 | |
---|
| 102 | (** ** Error handling *) |
---|
| 103 | |
---|
| 104 | let currentLocation = ref Cutil.no_loc |
---|
| 105 | |
---|
| 106 | let updateLoc l = currentLocation := l |
---|
| 107 | |
---|
| 108 | let numErrors = ref 0 |
---|
| 109 | |
---|
| 110 | let error msg = |
---|
| 111 | incr numErrors; |
---|
| 112 | eprintf "%aError: %s\n" Cutil.printloc !currentLocation msg |
---|
| 113 | |
---|
| 114 | let unsupported msg = |
---|
| 115 | incr numErrors; |
---|
| 116 | eprintf "%aUnsupported feature: %s\n" Cutil.printloc !currentLocation msg |
---|
| 117 | |
---|
| 118 | let warning msg = |
---|
| 119 | eprintf "%aWarning: %s\n" Cutil.printloc !currentLocation msg |
---|
| 120 | |
---|
| 121 | (** ** Identifier creation *) |
---|
| 122 | |
---|
| 123 | (* Rather than use the Matita name generators which have to be threaded |
---|
| 124 | throughout definitions, we'll use an imperative generator here. *) |
---|
| 125 | |
---|
[2648] | 126 | let idGenerator = ref (Extracted.Identifiers.new_universe Extracted.PreIdentifiers.SymbolTag) |
---|
[2620] | 127 | let idTable = Hashtbl.create 47 |
---|
[2758] | 128 | let symTable = Hashtbl.create 47 |
---|
[2620] | 129 | let make_id s = |
---|
| 130 | try |
---|
| 131 | Hashtbl.find idTable s |
---|
| 132 | with Not_found -> |
---|
[2648] | 133 | let { Extracted.Types.fst = id; Extracted.Types.snd = g} = Extracted.Identifiers.fresh Extracted.PreIdentifiers.SymbolTag !idGenerator in |
---|
[2620] | 134 | idGenerator := g; |
---|
| 135 | Hashtbl.add idTable s id; |
---|
[2758] | 136 | Hashtbl.add symTable id s; |
---|
[2620] | 137 | id |
---|
| 138 | |
---|
| 139 | (** ** Functions used to handle string literals *) |
---|
| 140 | |
---|
| 141 | let stringNum = ref 0 (* number of next global for string literals *) |
---|
| 142 | let stringTable = Hashtbl.create 47 |
---|
| 143 | |
---|
| 144 | let name_for_string_literal env s = |
---|
| 145 | try |
---|
| 146 | Hashtbl.find stringTable s |
---|
| 147 | with Not_found -> |
---|
| 148 | incr stringNum; |
---|
| 149 | let name = Printf.sprintf "__stringlit_%d" !stringNum in |
---|
| 150 | let id = make_id name in |
---|
| 151 | Hashtbl.add decl_atom id |
---|
| 152 | (env, (C.Storage_static, |
---|
| 153 | Env.fresh_ident name, |
---|
| 154 | C.TPtr(C.TInt(C.IChar,[C.AConst]),[]), |
---|
| 155 | None)); |
---|
| 156 | !define_stringlit_hook id; |
---|
| 157 | Hashtbl.add stringTable s id; |
---|
| 158 | id |
---|
| 159 | |
---|
| 160 | let typeStringLiteral s = |
---|
| 161 | Tarray(Tint(I8, Unsigned), convertIntNat (String.length s + 1)) |
---|
| 162 | |
---|
| 163 | let global_for_string s id = |
---|
| 164 | let init = ref [] in |
---|
| 165 | let add_char c = |
---|
| 166 | init := |
---|
| 167 | Init_int8(convertInt I8 (Int64.of_int (Char.code c))) |
---|
| 168 | :: !init in |
---|
| 169 | add_char '\000'; |
---|
| 170 | for i = String.length s - 1 downto 0 do add_char s.[i] done; |
---|
| 171 | ((id, !init), typeStringLiteral s) |
---|
| 172 | |
---|
| 173 | let globals_for_strings globs = |
---|
| 174 | Hashtbl.fold |
---|
| 175 | (fun s id l -> global_for_string s id :: l) |
---|
| 176 | stringTable globs |
---|
| 177 | |
---|
| 178 | (** ** Handling of stubs for variadic functions *) |
---|
| 179 | |
---|
| 180 | let stub_function_table = Hashtbl.create 47 |
---|
| 181 | |
---|
| 182 | let register_stub_function name tres targs = |
---|
| 183 | let rec letters_of_type = function |
---|
| 184 | | Tnil -> [] |
---|
| 185 | (*| Tfloat(_)::tl -> "f" :: letters_of_type tl*) |
---|
| 186 | | Tcons (_, tl) -> "i" :: letters_of_type tl in |
---|
| 187 | let stub_name = make_id |
---|
| 188 | (name ^ "$" ^ String.concat "" (letters_of_type targs)) in |
---|
| 189 | try |
---|
| 190 | (stub_name, Hashtbl.find stub_function_table stub_name) |
---|
| 191 | with Not_found -> |
---|
| 192 | let rec types_of_types = function |
---|
| 193 | | Tnil -> Tnil |
---|
| 194 | (*| Tfloat(_)::tl -> Tfloat(F64)::(types_of_types tl)*) |
---|
| 195 | | Tcons (_,tl) -> Tcons (Tpointer(Tvoid), types_of_types tl) in |
---|
| 196 | let stub_type = Tfunction (types_of_types targs, tres) in |
---|
| 197 | Hashtbl.add stub_function_table stub_name stub_type; |
---|
| 198 | (stub_name, stub_type) |
---|
| 199 | |
---|
| 200 | let declare_stub_function stub_name stub_type = |
---|
| 201 | match stub_type with |
---|
| 202 | | Tfunction(targs, tres) -> |
---|
| 203 | (stub_name, |
---|
| 204 | CL_External(stub_name, targs, tres)) |
---|
| 205 | | _ -> assert false |
---|
| 206 | |
---|
| 207 | let declare_stub_functions k = |
---|
| 208 | Hashtbl.fold |
---|
| 209 | (fun n i k -> declare_stub_function n i :: k) |
---|
| 210 | stub_function_table k |
---|
| 211 | |
---|
| 212 | (** ** Translation functions *) |
---|
| 213 | |
---|
| 214 | (** Constants *) |
---|
| 215 | |
---|
| 216 | |
---|
| 217 | |
---|
| 218 | (** Types *) |
---|
| 219 | |
---|
| 220 | let convertIkind = function |
---|
| 221 | | C.IBool -> unsupported "'_Bool' type"; (Unsigned, I8) |
---|
| 222 | | C.IChar -> (Unsigned, I8) |
---|
| 223 | | C.ISChar -> (Signed, I8) |
---|
| 224 | | C.IUChar -> (Unsigned, I8) |
---|
| 225 | | C.IInt -> (Signed, I32) |
---|
| 226 | | C.IUInt -> (Unsigned, I32) |
---|
| 227 | | C.IShort -> (Signed, I16) |
---|
| 228 | | C.IUShort -> (Unsigned, I16) |
---|
| 229 | | C.ILong -> (Signed, I32) |
---|
| 230 | | C.IULong -> (Unsigned, I32) |
---|
| 231 | | C.ILongLong -> |
---|
| 232 | (*if not !ClightFlags.option_flonglong then*) unsupported "'long long' type"; |
---|
| 233 | (Signed, I32) |
---|
| 234 | | C.IULongLong -> |
---|
| 235 | (*if not !ClightFlags.option_flonglong then*) unsupported "'unsigned long long' type"; |
---|
| 236 | (Unsigned, I32) |
---|
| 237 | |
---|
| 238 | (* |
---|
| 239 | let convertFkind = function |
---|
| 240 | | C.FFloat -> F32 |
---|
| 241 | | C.FDouble -> F64 |
---|
| 242 | | C.FLongDouble -> |
---|
| 243 | if not !ClightFlags.option_flonglong then unsupported "'long double' type"; |
---|
| 244 | F64 |
---|
| 245 | *) |
---|
| 246 | |
---|
| 247 | let convertTyp env t = |
---|
| 248 | |
---|
| 249 | let rec convertTyp seen t = |
---|
| 250 | match Cutil.unroll env t with |
---|
| 251 | | C.TVoid a -> Tvoid |
---|
| 252 | | C.TInt(ik, a) -> |
---|
| 253 | let (sg, sz) = convertIkind ik in Tint(sz, sg) |
---|
| 254 | | C.TFloat(fk, a) -> unsupported "float type"; Tvoid |
---|
| 255 | (*Tfloat(convertFkind fk)*) |
---|
| 256 | | C.TPtr(C.TStruct(id, _), _) when List.mem id seen -> |
---|
| 257 | Tcomp_ptr(make_id ("struct " ^ id.name)) |
---|
| 258 | | C.TPtr(C.TUnion(id, _), _) when List.mem id seen -> |
---|
| 259 | Tcomp_ptr(make_id ("union " ^ id.name)) |
---|
| 260 | | C.TPtr(ty, a) -> |
---|
| 261 | Tpointer(convertTyp seen ty) |
---|
| 262 | | C.TArray(ty, None, a) -> |
---|
| 263 | (* Cparser verified that the type ty[] occurs only in |
---|
| 264 | contexts that are safe for Clight, so just treat as ty[0]. *) |
---|
| 265 | (* warning "array type of unspecified size"; *) |
---|
| 266 | Tarray(convertTyp seen ty, Extracted.Nat.O) |
---|
| 267 | | C.TArray(ty, Some sz, a) -> |
---|
| 268 | Tarray(convertTyp seen ty, convertInt64Nat sz ) |
---|
| 269 | | C.TFun(tres, targs, va, a) -> |
---|
| 270 | if va then unsupported "variadic function type"; |
---|
| 271 | if Cutil.is_composite_type env tres then |
---|
| 272 | unsupported "return type is a struct or union"; |
---|
| 273 | Tfunction(begin match targs with |
---|
| 274 | | None -> warning "un-prototyped function type"; Tnil |
---|
| 275 | | Some tl -> convertParams seen tl |
---|
| 276 | end, |
---|
| 277 | convertTyp seen tres) |
---|
| 278 | | C.TNamed _ -> |
---|
| 279 | assert false |
---|
| 280 | | C.TStruct(id, a) -> |
---|
| 281 | let flds = |
---|
| 282 | try |
---|
| 283 | convertFields (id :: seen) (Env.find_struct env id) |
---|
| 284 | with Env.Error e -> |
---|
| 285 | error (Env.error_message e); Fnil in |
---|
| 286 | Tstruct(make_id ("struct " ^ id.name), flds) |
---|
| 287 | | C.TUnion(id, a) -> |
---|
| 288 | let flds = |
---|
| 289 | try |
---|
| 290 | convertFields (id :: seen) (Env.find_union env id) |
---|
| 291 | with Env.Error e -> |
---|
| 292 | error (Env.error_message e); Fnil in |
---|
| 293 | Tunion(make_id ("union " ^ id.name), flds) |
---|
| 294 | |
---|
| 295 | and convertParams seen = function |
---|
| 296 | | [] -> Tnil |
---|
| 297 | | (id, ty) :: rem -> |
---|
| 298 | if Cutil.is_composite_type env ty then |
---|
| 299 | unsupported "function parameter of struct or union type"; |
---|
| 300 | Tcons (convertTyp seen ty, convertParams seen rem) |
---|
| 301 | |
---|
| 302 | and convertFields seen ci = |
---|
| 303 | convertFieldList seen ci.Env.ci_members |
---|
| 304 | |
---|
| 305 | and convertFieldList seen = function |
---|
| 306 | | [] -> Fnil |
---|
| 307 | | f :: fl -> |
---|
| 308 | if f.fld_bitfield <> None then |
---|
| 309 | unsupported "bit field in struct or union"; |
---|
| 310 | Fcons (make_id f.fld_name, convertTyp seen f.fld_typ, |
---|
| 311 | convertFieldList seen fl) |
---|
| 312 | |
---|
| 313 | in convertTyp [] t |
---|
| 314 | |
---|
| 315 | let rec convertTypList env = function |
---|
| 316 | | [] -> Tnil |
---|
| 317 | | t1 :: tl -> Tcons (convertTyp env t1, convertTypList env tl) |
---|
| 318 | |
---|
| 319 | (** Expressions *) |
---|
| 320 | |
---|
| 321 | let ezero = Expr(Econst_int(I32, zero (convertIntNat 32)), Tint(I32, Signed)) |
---|
| 322 | |
---|
| 323 | let rec convertExpr env e = |
---|
| 324 | let ty = convertTyp env e.etyp in |
---|
| 325 | match e.edesc with |
---|
| 326 | | C.EConst(C.CInt(i, k, _)) -> |
---|
| 327 | let (_,sz) = convertIkind k in |
---|
| 328 | Expr(Econst_int(sz, convertInt sz i), ty) |
---|
| 329 | | C.EConst(C.CFloat(f, _, _)) -> unsupported "float constant"; ezero |
---|
| 330 | (*Expr(Econst_float f, ty)*) |
---|
| 331 | | C.EConst(C.CStr s) -> |
---|
| 332 | Expr(Evar(name_for_string_literal env s), typeStringLiteral s) |
---|
| 333 | | C.EConst(C.CWStr s) -> |
---|
| 334 | unsupported "wide string literal"; ezero |
---|
| 335 | | C.EConst(C.CEnum(id, i)) -> |
---|
| 336 | let sz = match ty with Tint (sz, _) -> sz | _ -> I32 in |
---|
| 337 | Expr(Econst_int(sz, convertInt sz i), ty) |
---|
| 338 | |
---|
| 339 | | C.ESizeof ty1 -> |
---|
| 340 | Expr(Esizeof(convertTyp env ty1), ty) |
---|
| 341 | | C.EVar id -> |
---|
| 342 | Expr(Evar(make_id id.name), ty) |
---|
| 343 | |
---|
| 344 | | C.EUnop(C.Oderef, e1) -> |
---|
| 345 | Expr(Ederef(convertExpr env e1), ty) |
---|
| 346 | | C.EUnop(C.Oaddrof, e1) -> |
---|
| 347 | Expr(Eaddrof(convertExpr env e1), ty) |
---|
| 348 | | C.EUnop(C.Odot id, e1) -> |
---|
| 349 | Expr(Efield(convertExpr env e1, make_id id), ty) |
---|
| 350 | | C.EUnop(C.Oarrow id, e1) -> |
---|
| 351 | let e1' = convertExpr env e1 in |
---|
| 352 | let ty1 = |
---|
| 353 | match typeof e1' with |
---|
| 354 | | Tpointer t -> t |
---|
| 355 | | _ -> error ("wrong type for ->" ^ id ^ " access"); Tvoid in |
---|
| 356 | Expr(Efield(Expr(Ederef(convertExpr env e1), ty1), |
---|
| 357 | make_id id), ty) |
---|
| 358 | | C.EUnop(C.Oplus, e1) -> |
---|
| 359 | convertExpr env e1 |
---|
| 360 | | C.EUnop(C.Ominus, e1) -> |
---|
| 361 | Expr(Eunop(Oneg, convertExpr env e1), ty) |
---|
| 362 | | C.EUnop(C.Olognot, e1) -> |
---|
| 363 | Expr(Eunop(Onotbool, convertExpr env e1), ty) |
---|
| 364 | | C.EUnop(C.Onot, e1) -> |
---|
| 365 | Expr(Eunop(Onotint, convertExpr env e1), ty) |
---|
| 366 | | C.EUnop(_, _) -> |
---|
| 367 | unsupported "pre/post increment/decrement operator"; ezero |
---|
| 368 | |
---|
| 369 | | C.EBinop(C.Oindex, e1, e2, _) -> |
---|
| 370 | Expr(Ederef(Expr(Ebinop(Oadd, convertExpr env e1, convertExpr env e2), |
---|
| 371 | Tpointer ty)), ty) |
---|
| 372 | | C.EBinop(C.Ologand, e1, e2, _) -> |
---|
| 373 | Expr(Eandbool(convertExpr env e1, convertExpr env e2), ty) |
---|
| 374 | | C.EBinop(C.Ologor, e1, e2, _) -> |
---|
| 375 | Expr(Eorbool(convertExpr env e1, convertExpr env e2), ty) |
---|
| 376 | | C.EBinop(op, e1, e2, _) -> |
---|
| 377 | let op' = |
---|
| 378 | match op with |
---|
| 379 | | C.Oadd -> Oadd |
---|
| 380 | | C.Osub -> Osub |
---|
| 381 | | C.Omul -> Omul |
---|
| 382 | | C.Odiv -> Odiv |
---|
| 383 | | C.Omod -> Omod |
---|
| 384 | | C.Oand -> Oand |
---|
| 385 | | C.Oor -> Oor |
---|
| 386 | | C.Oxor -> Oxor |
---|
| 387 | | C.Oshl -> Oshl |
---|
| 388 | | C.Oshr -> Oshr |
---|
| 389 | | C.Oeq -> Oeq |
---|
[2773] | 390 | | C.One -> One |
---|
[2620] | 391 | | C.Olt -> Olt |
---|
| 392 | | C.Ogt -> Ogt |
---|
| 393 | | C.Ole -> Ole |
---|
| 394 | | C.Oge -> Oge |
---|
| 395 | | C.Ocomma -> unsupported "sequence operator"; Oadd |
---|
| 396 | | _ -> unsupported "assignment operator"; Oadd in |
---|
| 397 | Expr(Ebinop(op', convertExpr env e1, convertExpr env e2), ty) |
---|
| 398 | | C.EConditional(e1, e2, e3) -> |
---|
| 399 | Expr(Econdition(convertExpr env e1, convertExpr env e2, convertExpr env e3), ty) |
---|
| 400 | | C.ECast(ty1, e1) -> |
---|
| 401 | Expr(Ecast(convertTyp env ty1, convertExpr env e1), ty) |
---|
| 402 | | C.ECall _ -> |
---|
| 403 | unsupported "function call within expression"; ezero |
---|
| 404 | |
---|
| 405 | (* Function calls *) |
---|
| 406 | |
---|
| 407 | let rec projFunType env ty = |
---|
| 408 | match Cutil.unroll env ty with |
---|
| 409 | | TFun(res, args, vararg, attr) -> Some(res, vararg) |
---|
| 410 | | TPtr(ty', attr) -> projFunType env ty' |
---|
| 411 | | _ -> None |
---|
| 412 | |
---|
| 413 | let rec convertList l = |
---|
| 414 | match l with |
---|
| 415 | | [] -> Extracted.List.Nil |
---|
| 416 | | h::t -> Extracted.List.Cons (h,convertList t) |
---|
| 417 | |
---|
| 418 | let convertFuncall env lhs fn args = |
---|
| 419 | match projFunType env fn.etyp with |
---|
| 420 | | None -> |
---|
| 421 | error "wrong type for function part of a call"; Sskip |
---|
| 422 | | Some(res, false) -> |
---|
| 423 | (* Non-variadic function *) |
---|
| 424 | Scall(lhs, convertExpr env fn, convertList (List.map (convertExpr env) args)) |
---|
| 425 | | Some(res, true) -> |
---|
| 426 | (* Variadic function: generate a call to a stub function with |
---|
| 427 | the appropriate number and types of arguments. Works only if |
---|
| 428 | the function expression e is a global variable. *) |
---|
| 429 | let fun_name = |
---|
| 430 | match fn with |
---|
| 431 | | {edesc = C.EVar id} when false (* FIXME? !ClightFlags.option_fvararg_calls *)-> |
---|
| 432 | (*warning "emulating call to variadic function"; *) |
---|
| 433 | id.name |
---|
| 434 | | _ -> |
---|
| 435 | unsupported "call to variadic function"; |
---|
| 436 | "<error>" in |
---|
| 437 | let targs = convertTypList env (List.map (fun e -> e.etyp) args) in |
---|
| 438 | let tres = convertTyp env res in |
---|
| 439 | let (stub_fun_name, stub_fun_typ) = |
---|
| 440 | register_stub_function fun_name tres targs in |
---|
| 441 | Scall(lhs, |
---|
| 442 | Expr(Evar(stub_fun_name), stub_fun_typ), |
---|
| 443 | convertList (List.map (convertExpr env) args)) |
---|
| 444 | |
---|
| 445 | (* Handling of volatile *) |
---|
| 446 | |
---|
| 447 | let is_volatile_access env e = |
---|
| 448 | List.mem C.AVolatile (Cutil.attributes_of_type env e.etyp) |
---|
| 449 | && Cutil.is_lvalue env e |
---|
| 450 | |
---|
| 451 | let volatile_fun_suffix_type ty = |
---|
| 452 | match ty with |
---|
| 453 | | Tint(I8, Unsigned) -> ("int8unsigned", ty) |
---|
| 454 | | Tint(I8, Signed) -> ("int8signed", ty) |
---|
| 455 | | Tint(I16, Unsigned) -> ("int16unsigned", ty) |
---|
| 456 | | Tint(I16, Signed) -> ("int16signed", ty) |
---|
| 457 | | Tint(I32, _) -> ("int32", Tint(I32, Signed)) |
---|
| 458 | (*| Tfloat F32 -> ("float32", ty) |
---|
| 459 | | Tfloat F64 -> ("float64", ty)*) |
---|
| 460 | | Tpointer _ | Tarray _ | Tfunction _ | Tcomp_ptr _ -> |
---|
| 461 | ("pointer", Tpointer Tvoid) |
---|
| 462 | | _ -> |
---|
| 463 | unsupported "operation on volatile struct or union"; ("", Tvoid) |
---|
| 464 | |
---|
| 465 | let volatile_read_fun ty = |
---|
| 466 | let (suffix, ty') = volatile_fun_suffix_type ty in |
---|
| 467 | Expr(Evar(make_id ("__builtin_volatile_read_" ^ suffix)), |
---|
| 468 | Tfunction(Tcons (Tpointer Tvoid, Tnil), ty')) |
---|
| 469 | |
---|
| 470 | let volatile_write_fun ty = |
---|
| 471 | let (suffix, ty') = volatile_fun_suffix_type ty in |
---|
| 472 | Expr(Evar(make_id ("__builtin_volatile_write_" ^ suffix)), |
---|
| 473 | Tfunction(Tcons (Tpointer Tvoid, Tcons (ty', Tnil)), Tvoid)) |
---|
| 474 | |
---|
| 475 | (* Toplevel expression, argument of an Sdo *) |
---|
| 476 | |
---|
| 477 | let convertTopExpr env e = |
---|
| 478 | match e.edesc with |
---|
| 479 | | C.EBinop(C.Oassign, lhs, {edesc = C.ECall(fn, args)}, _) -> |
---|
| 480 | convertFuncall env (Extracted.Types.Some (convertExpr env lhs)) fn args |
---|
| 481 | | C.EBinop(C.Oassign, lhs, rhs, _) -> |
---|
| 482 | if Cutil.is_composite_type env lhs.etyp then |
---|
| 483 | unsupported "assignment between structs or between unions"; |
---|
| 484 | let lhs' = convertExpr env lhs |
---|
| 485 | and rhs' = convertExpr env rhs in |
---|
| 486 | begin match (is_volatile_access env lhs, is_volatile_access env rhs) with |
---|
| 487 | | true, true -> (* should not happen *) |
---|
| 488 | unsupported "volatile-to-volatile assignment"; |
---|
| 489 | Sskip |
---|
| 490 | | false, true -> (* volatile read *) |
---|
| 491 | Scall(Extracted.Types.Some lhs', |
---|
| 492 | volatile_read_fun (typeof rhs'), |
---|
| 493 | convertList [ Expr (Eaddrof rhs', Tpointer (typeof rhs')) ]) |
---|
| 494 | | true, false -> (* volatile write *) |
---|
| 495 | Scall(Extracted.Types.None, |
---|
| 496 | volatile_write_fun (typeof lhs'), |
---|
| 497 | convertList [ Expr(Eaddrof lhs', Tpointer (typeof lhs')); rhs' ]) |
---|
| 498 | | false, false -> (* regular assignment *) |
---|
| 499 | Sassign(convertExpr env lhs, convertExpr env rhs) |
---|
| 500 | end |
---|
| 501 | | C.ECall(fn, args) -> |
---|
| 502 | convertFuncall env Extracted.Types.None fn args |
---|
| 503 | | _ -> |
---|
| 504 | unsupported "illegal toplevel expression"; Sskip |
---|
| 505 | |
---|
| 506 | (* Separate the cases of a switch statement body *) |
---|
| 507 | |
---|
| 508 | type switchlabel = |
---|
| 509 | | Case of C.exp |
---|
| 510 | | Default |
---|
| 511 | |
---|
| 512 | type switchbody = |
---|
| 513 | | Label of switchlabel |
---|
| 514 | | Stmt of C.stmt |
---|
| 515 | |
---|
| 516 | let rec flattenSwitch = function |
---|
| 517 | | {sdesc = C.Sseq(s1, s2)} -> |
---|
| 518 | flattenSwitch s1 @ flattenSwitch s2 |
---|
| 519 | | {sdesc = C.Slabeled(C.Scase e, s1)} -> |
---|
| 520 | Label(Case e) :: flattenSwitch s1 |
---|
| 521 | | {sdesc = C.Slabeled(C.Sdefault, s1)} -> |
---|
| 522 | Label Default :: flattenSwitch s1 |
---|
| 523 | | s -> |
---|
| 524 | [Stmt s] |
---|
| 525 | |
---|
| 526 | let rec groupSwitch = function |
---|
| 527 | | [] -> |
---|
| 528 | (Cutil.sskip, []) |
---|
| 529 | | Label case :: rem -> |
---|
| 530 | let (fst, cases) = groupSwitch rem in |
---|
| 531 | (Cutil.sskip, (case, fst) :: cases) |
---|
| 532 | | Stmt s :: rem -> |
---|
| 533 | let (fst, cases) = groupSwitch rem in |
---|
| 534 | (Cutil.sseq s.sloc s fst, cases) |
---|
| 535 | |
---|
| 536 | (* Statement *) |
---|
| 537 | |
---|
| 538 | let rec convertStmt env s = |
---|
| 539 | updateLoc s.sloc; |
---|
| 540 | match s.sdesc with |
---|
| 541 | | C.Sskip -> |
---|
| 542 | Sskip |
---|
| 543 | | C.Sdo e -> |
---|
| 544 | convertTopExpr env e |
---|
| 545 | | C.Sseq(s1, s2) -> |
---|
| 546 | Ssequence(convertStmt env s1, convertStmt env s2) |
---|
| 547 | | C.Sif(e, s1, s2) -> |
---|
| 548 | Sifthenelse(convertExpr env e, convertStmt env s1, convertStmt env s2) |
---|
| 549 | | C.Swhile(e, s1) -> |
---|
| 550 | Swhile(convertExpr env e, convertStmt env s1) |
---|
| 551 | | C.Sdowhile(s1, e) -> |
---|
| 552 | Sdowhile(convertExpr env e, convertStmt env s1) |
---|
| 553 | | C.Sfor(s1, e, s2, s3) -> |
---|
| 554 | Sfor(convertStmt env s1, convertExpr env e, convertStmt env s2, |
---|
| 555 | convertStmt env s3) |
---|
| 556 | | C.Sbreak -> |
---|
| 557 | Sbreak |
---|
| 558 | | C.Scontinue -> |
---|
| 559 | Scontinue |
---|
| 560 | | C.Sswitch(e, s1) -> |
---|
| 561 | let (init, cases) = groupSwitch (flattenSwitch s1) in |
---|
| 562 | if cases = [] then |
---|
| 563 | unsupported "ill-formed 'switch' statement"; |
---|
| 564 | if init.sdesc <> C.Sskip then |
---|
| 565 | warning "ignored code at beginning of 'switch'"; |
---|
| 566 | let e' = convertExpr env e in |
---|
| 567 | let sz = match typeof e' with Tint(sz,_) -> sz | _ -> I32 in |
---|
| 568 | Sswitch(e', convertSwitch env sz cases) |
---|
| 569 | | C.Slabeled(C.Slabel lbl, s1) -> |
---|
| 570 | Slabel(make_id lbl, convertStmt env s1) |
---|
| 571 | | C.Slabeled(C.Scase _, _) -> |
---|
| 572 | unsupported "'case' outside of 'switch'"; Sskip |
---|
| 573 | | C.Slabeled(C.Sdefault, _) -> |
---|
| 574 | unsupported "'default' outside of 'switch'"; Sskip |
---|
| 575 | | C.Sgoto lbl -> |
---|
| 576 | Sgoto(make_id lbl) |
---|
| 577 | | C.Sreturn None -> |
---|
| 578 | Sreturn Extracted.Types.None |
---|
| 579 | | C.Sreturn(Some e) -> |
---|
| 580 | Sreturn(Extracted.Types.Some(convertExpr env e)) |
---|
| 581 | | C.Sblock _ -> |
---|
| 582 | unsupported "nested blocks"; Sskip |
---|
| 583 | | C.Sdecl _ -> |
---|
| 584 | unsupported "inner declarations"; Sskip |
---|
| 585 | |
---|
| 586 | and convertSwitch env sz = function |
---|
| 587 | | [] -> |
---|
| 588 | LSdefault Sskip |
---|
| 589 | | [Default, s] -> |
---|
| 590 | LSdefault (convertStmt env s) |
---|
| 591 | | (Default, s) :: _ -> |
---|
| 592 | updateLoc s.sloc; |
---|
| 593 | unsupported "'default' case must occur last"; |
---|
| 594 | LSdefault Sskip |
---|
| 595 | | (Case e, s) :: rem -> |
---|
| 596 | updateLoc s.sloc; |
---|
| 597 | let v = |
---|
| 598 | match Ceval.integer_expr env e with |
---|
| 599 | | None -> unsupported "'case' label is not a compile-time integer"; 0L |
---|
| 600 | | Some v -> v in |
---|
| 601 | LScase(sz, |
---|
| 602 | convertInt sz v, |
---|
| 603 | convertStmt env s, |
---|
| 604 | convertSwitch env sz rem) |
---|
| 605 | |
---|
| 606 | (** Function definitions *) |
---|
| 607 | |
---|
| 608 | let convertProd (x,y) = {Extracted.Types.fst = x; Extracted.Types.snd = y} |
---|
| 609 | |
---|
| 610 | let convertFundef env fd = |
---|
| 611 | if Cutil.is_composite_type env fd.fd_ret then |
---|
| 612 | unsupported "function returning a struct or union"; |
---|
| 613 | let ret = |
---|
| 614 | convertTyp env fd.fd_ret in |
---|
| 615 | let params = |
---|
| 616 | List.map |
---|
| 617 | (fun (id, ty) -> |
---|
| 618 | if Cutil.is_composite_type env ty then |
---|
| 619 | unsupported "function parameter of struct or union type"; |
---|
| 620 | convertProd (make_id id.name, convertTyp env ty)) |
---|
| 621 | fd.fd_params in |
---|
| 622 | let vars = |
---|
| 623 | List.map |
---|
| 624 | (fun (sto, id, ty, init) -> |
---|
| 625 | if sto = Storage_extern || sto = Storage_static then |
---|
| 626 | unsupported "'static' or 'extern' local variable"; |
---|
| 627 | if init <> None then |
---|
| 628 | unsupported "initialized local variable"; |
---|
| 629 | convertProd (make_id id.name, convertTyp env ty)) |
---|
| 630 | fd.fd_locals in |
---|
| 631 | let body' = convertStmt env fd.fd_body in |
---|
| 632 | let id' = make_id fd.fd_name.name in |
---|
| 633 | let decl = |
---|
| 634 | (fd.fd_storage, fd.fd_name, Cutil.fundef_typ fd, None) in |
---|
| 635 | Hashtbl.add decl_atom id' (env, decl); |
---|
| 636 | !define_function_hook id' decl; |
---|
| 637 | (id', |
---|
| 638 | CL_Internal {fn_return = ret; fn_params = convertList params; |
---|
| 639 | fn_vars = convertList vars; fn_body = body'}) |
---|
| 640 | |
---|
| 641 | (** External function declaration *) |
---|
| 642 | |
---|
| 643 | let convertFundecl env (sto, id, ty, optinit) = |
---|
| 644 | match convertTyp env ty with |
---|
| 645 | | Tfunction(args, res) -> |
---|
| 646 | let id' = make_id id.name in |
---|
| 647 | (id', CL_External(id', args, res)) |
---|
| 648 | | _ -> |
---|
| 649 | assert false |
---|
| 650 | |
---|
| 651 | (** Initializers *) |
---|
| 652 | |
---|
| 653 | let init_data_of_string s = |
---|
| 654 | let id = ref [] in |
---|
| 655 | let enter_char c = |
---|
| 656 | let n = convertInt I8 (Int64.of_int (Char.code c)) in |
---|
| 657 | id := Init_int8 n :: !id in |
---|
| 658 | enter_char '\000'; |
---|
| 659 | for i = String.length s - 1 downto 0 do enter_char s.[i] done; |
---|
| 660 | !id |
---|
| 661 | |
---|
| 662 | let convertInit env ty init = |
---|
| 663 | |
---|
| 664 | let k = ref [] |
---|
| 665 | and pos = ref 0 in |
---|
| 666 | let emit size datum = |
---|
| 667 | k := datum :: !k; |
---|
| 668 | pos := !pos + size in |
---|
| 669 | let emit_space size = |
---|
| 670 | emit size (Init_space (convertIntNat size)) in |
---|
| 671 | let align size = |
---|
| 672 | let n = !pos land (size - 1) in |
---|
| 673 | if n > 0 then emit_space (size - n) in |
---|
| 674 | let check_align size = |
---|
| 675 | assert (!pos land (size - 1) = 0) in |
---|
| 676 | |
---|
| 677 | let rec reduceInitExpr = function |
---|
| 678 | | { edesc = C.EVar id; etyp = ty } -> |
---|
| 679 | begin match Cutil.unroll env ty with |
---|
| 680 | | C.TArray _ | C.TFun _ -> Some id |
---|
| 681 | | _ -> None |
---|
| 682 | end |
---|
| 683 | | {edesc = C.EUnop(C.Oaddrof, {edesc = C.EVar id})} -> Some id |
---|
| 684 | | {edesc = C.ECast(ty, e)} -> reduceInitExpr e |
---|
| 685 | | _ -> None in |
---|
| 686 | |
---|
| 687 | let rec cvtInit ty = function |
---|
| 688 | | Init_single e -> |
---|
| 689 | begin match reduceInitExpr e with |
---|
| 690 | | Some id -> |
---|
| 691 | check_align 4; |
---|
| 692 | emit 4 (Init_addrof(make_id id.name, convertIntNat 0)) |
---|
| 693 | | None -> |
---|
| 694 | match Ceval.constant_expr env ty e with |
---|
| 695 | | Some(C.CInt(v, ik, _)) -> |
---|
| 696 | begin match convertIkind ik with |
---|
| 697 | | (_, I8) -> |
---|
| 698 | emit 1 (Init_int8(convertInt I8 v)) |
---|
| 699 | | (_, I16) -> |
---|
| 700 | check_align 2; |
---|
| 701 | emit 2 (Init_int16(convertInt I16 v)) |
---|
| 702 | | (_, I32) -> |
---|
| 703 | check_align 4; |
---|
| 704 | emit 4 (Init_int32(convertInt I32 v)) |
---|
| 705 | end |
---|
| 706 | | Some(C.CFloat(v, fk, _)) -> |
---|
| 707 | unsupported "floats" |
---|
| 708 | (*begin match convertFkind fk with |
---|
| 709 | | F32 -> |
---|
| 710 | check_align 4; |
---|
| 711 | emit 4 (Init_float32 v) |
---|
| 712 | | F64 -> |
---|
| 713 | check_align 8; |
---|
| 714 | emit 8 (Init_float64 v) |
---|
| 715 | end*) |
---|
| 716 | | Some(C.CStr s) -> |
---|
| 717 | check_align 4; |
---|
| 718 | let id = name_for_string_literal env s in |
---|
| 719 | emit 4 (Init_addrof(id, convertIntNat 0)) |
---|
| 720 | | Some(C.CWStr _) -> |
---|
| 721 | unsupported "wide character strings" |
---|
| 722 | | Some(C.CEnum _) -> |
---|
| 723 | error "enum tag after constant folding" |
---|
| 724 | | None -> |
---|
| 725 | error "initializer is not a compile-time constant" |
---|
| 726 | end |
---|
| 727 | | Init_array il -> |
---|
| 728 | let ty_elt = |
---|
| 729 | match Cutil.unroll env ty with |
---|
| 730 | | C.TArray(t, _, _) -> t |
---|
| 731 | | _ -> error "array type expected in initializer"; C.TVoid [] in |
---|
| 732 | List.iter (cvtInit ty_elt) il |
---|
| 733 | | Init_struct(_, flds) -> |
---|
| 734 | cvtPadToSizeof ty (fun () -> List.iter cvtFieldInit flds) |
---|
| 735 | | Init_union(_, fld, i) -> |
---|
| 736 | cvtPadToSizeof ty (fun () -> cvtFieldInit (fld,i)) |
---|
| 737 | |
---|
| 738 | and cvtFieldInit (fld, i) = |
---|
| 739 | let ty' = convertTyp env fld.fld_typ in |
---|
| 740 | let al = alignof ty' in |
---|
| 741 | align al; |
---|
| 742 | cvtInit fld.fld_typ i |
---|
| 743 | |
---|
| 744 | and cvtPadToSizeof ty fn = |
---|
| 745 | let ty' = convertTyp env ty in |
---|
| 746 | let sz = sizeof ty' in |
---|
| 747 | let pos0 = !pos in |
---|
| 748 | fn(); |
---|
| 749 | let pos1 = !pos in |
---|
| 750 | assert (pos1 <= pos0 + sz); |
---|
| 751 | if pos1 < pos0 + sz then emit_space (pos0 + sz - pos1) |
---|
| 752 | |
---|
| 753 | in cvtInit ty init; List.rev !k |
---|
| 754 | |
---|
| 755 | (** Global variable *) |
---|
| 756 | |
---|
| 757 | let convertGlobvar env (sto, id, ty, optinit as decl) = |
---|
| 758 | let id' = make_id id.name in |
---|
| 759 | let ty' = convertTyp env ty in |
---|
| 760 | let init' = |
---|
| 761 | match optinit with |
---|
| 762 | | None -> |
---|
| 763 | if sto = C.Storage_extern then [] else [Init_space(convertIntNat (sizeof ty'))] |
---|
| 764 | | Some i -> |
---|
| 765 | convertInit env ty i in |
---|
| 766 | Hashtbl.add decl_atom id' (env, decl); |
---|
| 767 | !define_variable_hook id' decl; |
---|
| 768 | ((id', init'), ty') |
---|
| 769 | |
---|
| 770 | (** Convert a list of global declarations. |
---|
| 771 | Result is a pair [(funs, vars)] where [funs] are |
---|
| 772 | the function definitions (internal and external) |
---|
| 773 | and [vars] the variable declarations. *) |
---|
| 774 | |
---|
| 775 | let rec convertGlobdecls env funs vars gl = |
---|
| 776 | match gl with |
---|
| 777 | | [] -> (List.rev funs, List.rev vars) |
---|
| 778 | | g :: gl' -> |
---|
| 779 | updateLoc g.gloc; |
---|
| 780 | match g.gdesc with |
---|
| 781 | | C.Gdecl((sto, id, ty, optinit) as d) -> |
---|
| 782 | (* Prototyped functions become external declarations. |
---|
| 783 | Variadic functions are skipped. |
---|
| 784 | Other types become variable declarations. *) |
---|
| 785 | begin match Cutil.unroll env ty with |
---|
| 786 | | TFun(_, Some _, false, _) -> |
---|
| 787 | convertGlobdecls env (convertFundecl env d :: funs) vars gl' |
---|
| 788 | | TFun(_, None, false, _) -> |
---|
| 789 | error "function declaration without prototype"; |
---|
| 790 | convertGlobdecls env funs vars gl' |
---|
| 791 | | TFun(_, _, true, _) -> |
---|
| 792 | convertGlobdecls env funs vars gl' |
---|
| 793 | | _ -> |
---|
| 794 | convertGlobdecls env funs (convertGlobvar env d :: vars) gl' |
---|
| 795 | end |
---|
| 796 | | C.Gfundef fd -> |
---|
| 797 | convertGlobdecls env (convertFundef env fd :: funs) vars gl' |
---|
| 798 | | C.Gcompositedecl _ | C.Gcompositedef _ |
---|
| 799 | | C.Gtypedef _ | C.Genumdef _ -> |
---|
| 800 | (* typedefs are unrolled, structs are expanded inline, and |
---|
| 801 | enum tags are folded. So we just skip their declarations. *) |
---|
| 802 | convertGlobdecls env funs vars gl' |
---|
| 803 | | C.Gpragma s -> |
---|
| 804 | if not (!process_pragma_hook s) then |
---|
| 805 | warning ("'#pragma " ^ s ^ "' directive ignored"); |
---|
| 806 | convertGlobdecls env funs vars gl' |
---|
| 807 | |
---|
| 808 | (** Build environment of typedefs and structs *) |
---|
| 809 | |
---|
| 810 | let rec translEnv env = function |
---|
| 811 | | [] -> env |
---|
| 812 | | g :: gl -> |
---|
| 813 | let env' = |
---|
| 814 | match g.gdesc with |
---|
| 815 | | C.Gcompositedecl(su, id) -> |
---|
| 816 | Env.add_composite env id (Cutil.composite_info_decl env su) |
---|
| 817 | | C.Gcompositedef(su, id, fld) -> |
---|
| 818 | Env.add_composite env id (Cutil.composite_info_def env su fld) |
---|
| 819 | | C.Gtypedef(id, ty) -> |
---|
| 820 | Env.add_typedef env id ty |
---|
| 821 | | _ -> |
---|
| 822 | env in |
---|
| 823 | translEnv env' gl |
---|
| 824 | |
---|
| 825 | (** Eliminate forward declarations of globals that are defined later. *) |
---|
| 826 | |
---|
| 827 | module IdentSet = Set.Make(struct type t = C.ident let compare = compare end) |
---|
| 828 | |
---|
| 829 | let cleanupGlobals p = |
---|
| 830 | |
---|
| 831 | let rec clean defs accu = function |
---|
| 832 | | [] -> accu |
---|
| 833 | | g :: gl -> |
---|
| 834 | updateLoc g.gloc; |
---|
| 835 | match g.gdesc with |
---|
| 836 | | C.Gdecl(sto, id, ty, None) -> |
---|
| 837 | if IdentSet.mem id defs |
---|
| 838 | then clean defs accu gl |
---|
| 839 | else clean (IdentSet.add id defs) (g :: accu) gl |
---|
| 840 | | C.Gdecl(_, id, ty, _) -> |
---|
| 841 | if IdentSet.mem id defs then |
---|
| 842 | error ("multiple definitions of " ^ id.name); |
---|
| 843 | clean (IdentSet.add id defs) (g :: accu) gl |
---|
| 844 | | C.Gfundef fd -> |
---|
| 845 | if IdentSet.mem fd.fd_name defs then |
---|
| 846 | error ("multiple definitions of " ^ fd.fd_name.name); |
---|
| 847 | clean (IdentSet.add fd.fd_name defs) (g :: accu) gl |
---|
| 848 | | _ -> |
---|
| 849 | clean defs (g :: accu) gl |
---|
| 850 | |
---|
| 851 | in clean IdentSet.empty [] (List.rev p) |
---|
| 852 | |
---|
| 853 | (** Convert a [C.program] into a [Csyntax.program] *) |
---|
| 854 | |
---|
| 855 | let convertCLVar ((x,y),z) = |
---|
| 856 | {Extracted.Types.fst = {Extracted.Types.fst = x; Extracted.Types.snd = XData}; |
---|
| 857 | Extracted.Types.snd = {Extracted.Types.fst = convertList y; Extracted.Types.snd = z}} |
---|
| 858 | |
---|
| 859 | let convertProgram (p:C.program) : clight_program option = |
---|
| 860 | numErrors := 0; |
---|
[2648] | 861 | idGenerator := Extracted.Identifiers.new_universe Extracted.PreIdentifiers.SymbolTag; |
---|
[2620] | 862 | stringNum := 0; |
---|
| 863 | Hashtbl.clear decl_atom; |
---|
| 864 | Hashtbl.clear idTable; |
---|
| 865 | Hashtbl.clear stringTable; |
---|
| 866 | Hashtbl.clear stub_function_table; |
---|
| 867 | (* Hack: externals are problematic for Cerco. TODO *) |
---|
| 868 | let p = (* Builtins.declarations() @ *) p in |
---|
| 869 | try |
---|
| 870 | let (funs1, vars1) = |
---|
| 871 | convertGlobdecls (translEnv Env.empty p) [] [] (cleanupGlobals p) in |
---|
| 872 | let funs2 = declare_stub_functions funs1 in |
---|
| 873 | let main = make_id "main" in |
---|
| 874 | let vars2 = globals_for_strings vars1 in |
---|
| 875 | if !numErrors > 0 |
---|
| 876 | then None |
---|
| 877 | else Some { prog_funct = convertList (List.map convertProd funs2); |
---|
| 878 | prog_vars = convertList (List.map convertCLVar vars2); |
---|
| 879 | prog_main = main } |
---|
| 880 | with Env.Error msg -> |
---|
| 881 | error (Env.error_message msg); None |
---|
| 882 | |
---|
| 883 | (** ** Extracting information about global variables from their atom *) |
---|
| 884 | |
---|
| 885 | let rec type_is_readonly env t = |
---|
| 886 | let a = Cutil.attributes_of_type env t in |
---|
| 887 | if List.mem C.AVolatile a then false else |
---|
| 888 | if List.mem C.AConst a then true else |
---|
| 889 | match Cutil.unroll env t with |
---|
| 890 | | C.TArray(t', _, _) -> type_is_readonly env t' |
---|
| 891 | | _ -> false |
---|
| 892 | |
---|
| 893 | let atom_is_static a = |
---|
| 894 | try |
---|
| 895 | let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in |
---|
| 896 | sto = C.Storage_static |
---|
| 897 | with Not_found -> |
---|
| 898 | false |
---|
| 899 | |
---|
| 900 | let atom_is_readonly a = |
---|
| 901 | try |
---|
| 902 | let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in |
---|
| 903 | type_is_readonly env ty |
---|
| 904 | with Not_found -> |
---|
| 905 | false |
---|
| 906 | |
---|
| 907 | let atom_sizeof a = |
---|
| 908 | try |
---|
| 909 | let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in |
---|
| 910 | Cutil.sizeof env ty |
---|
| 911 | with Not_found -> |
---|
| 912 | None |
---|
| 913 | |
---|
| 914 | let atom_alignof a = |
---|
| 915 | try |
---|
| 916 | let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in |
---|
| 917 | Cutil.alignof env ty |
---|
| 918 | with Not_found -> |
---|
| 919 | None |
---|
| 920 | |
---|
| 921 | (** ** The builtin environment *) |
---|
| 922 | |
---|
| 923 | open Builtins |
---|
| 924 | |
---|
| 925 | let builtins_generic = { |
---|
| 926 | typedefs = [ |
---|
| 927 | (* keeps GCC-specific headers happy, harmless for others *) |
---|
| 928 | "__builtin_va_list", C.TPtr(C.TVoid [], []) |
---|
| 929 | ]; |
---|
| 930 | functions = [ |
---|
| 931 | (* The volatile read/volatile write functions *) |
---|
| 932 | "__builtin_volatile_read_int8unsigned", |
---|
| 933 | (TInt(IUChar, []), [TPtr(TVoid [], [])], false); |
---|
| 934 | "__builtin_volatile_read_int8signed", |
---|
| 935 | (TInt(ISChar, []), [TPtr(TVoid [], [])], false); |
---|
| 936 | "__builtin_volatile_read_int16unsigned", |
---|
| 937 | (TInt(IUShort, []), [TPtr(TVoid [], [])], false); |
---|
| 938 | "__builtin_volatile_read_int16signed", |
---|
| 939 | (TInt(IShort, []), [TPtr(TVoid [], [])], false); |
---|
| 940 | "__builtin_volatile_read_int32", |
---|
| 941 | (TInt(IInt, []), [TPtr(TVoid [], [])], false); |
---|
| 942 | "__builtin_volatile_read_float32", |
---|
| 943 | (TFloat(FFloat, []), [TPtr(TVoid [], [])], false); |
---|
| 944 | "__builtin_volatile_read_float64", |
---|
| 945 | (TFloat(FDouble, []), [TPtr(TVoid [], [])], false); |
---|
| 946 | "__builtin_volatile_read_pointer", |
---|
| 947 | (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false); |
---|
| 948 | "__builtin_volatile_write_int8unsigned", |
---|
| 949 | (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false); |
---|
| 950 | "__builtin_volatile_write_int8signed", |
---|
| 951 | (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false); |
---|
| 952 | "__builtin_volatile_write_int16unsigned", |
---|
| 953 | (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false); |
---|
| 954 | "__builtin_volatile_write_int16signed", |
---|
| 955 | (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false); |
---|
| 956 | "__builtin_volatile_write_int32", |
---|
| 957 | (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false); |
---|
| 958 | "__builtin_volatile_write_float32", |
---|
| 959 | (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false); |
---|
| 960 | "__builtin_volatile_write_float64", |
---|
| 961 | (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false); |
---|
| 962 | "__builtin_volatile_write_pointer", |
---|
| 963 | (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false) |
---|
| 964 | ] |
---|
| 965 | } |
---|
| 966 | |
---|
| 967 | (* Add processor-dependent builtins *) |
---|
| 968 | |
---|
| 969 | let builtins = |
---|
| 970 | { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; |
---|
| 971 | functions = builtins_generic.functions @ CBuiltins.builtins.functions |
---|
| 972 | } |
---|
| 973 | |
---|