From 8f444dec7112e5b125bf3ead8481ae0f698bbb96 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 2 Jun 2016 14:43:34 +0200 Subject: Pass the updated env through elab_expr. Since casts, sizeof, etc. expressions can introduce new types we also need to add these to the environment and pass it through. Bug 17814 --- cparser/Elab.ml | 315 +++++++++++++++++++++++++++++--------------------------- 1 file changed, 166 insertions(+), 149 deletions(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 91a795e9..cdae2fd9 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -94,7 +94,7 @@ let redef fn env arg = (* Forward declarations *) -let elab_expr_f : (cabsloc -> Env.t -> Cabs.expression -> C.exp) ref +let elab_expr_f : (cabsloc -> Env.t -> Cabs.expression -> C.exp * Env.t) ref = ref (fun _ _ _ -> assert false) let elab_funbody_f : (C.typ -> Env.t -> statement -> C.stmt) ref @@ -295,7 +295,7 @@ let elab_attr_arg loc env a = AIdent s end | _ -> - let b = !elab_expr_f loc env a in + let b,env = !elab_expr_f loc env a in match Ceval.constant_expr env b.etyp b with | Some(CInt(n, _, _)) -> AInt n | Some(CStr s) -> AString s @@ -530,7 +530,8 @@ and elab_type_declarator loc env ty kr_ok = function | None -> None | Some sz -> - match Ceval.integer_expr env (!elab_expr_f loc env sz) with + let expr,env = (!elab_expr_f loc env sz) in + match Ceval.integer_expr env expr with | Some n -> if n < 0L then error loc "array size is negative"; if n = 0L then warning loc "array of size 0"; @@ -679,7 +680,8 @@ and elab_field_group env (Field_group (spec, fieldlist, loc)) = no bigger than 'int'" id; None end else begin - match Ceval.integer_expr env' (!elab_expr_f loc env sz) with + let expr,env' =(!elab_expr_f loc env sz) in + match Ceval.integer_expr env' expr with | Some n -> if n < 0L then begin error loc "bit size of '%s' (%Ld) is negative" id n; @@ -790,7 +792,7 @@ and elab_enum_item env ((s, exp), loc) nextval = | None -> (nextval, None) | Some exp -> - let exp' = !elab_expr_f loc env exp in + let exp',env = !elab_expr_f loc env exp in match Ceval.integer_expr env exp' with | Some n -> (n, Some exp') | None -> @@ -1071,7 +1073,8 @@ let rec elab_designator loc env zi desig = raise Exit end | ATINDEX_INIT a :: desig' -> - begin match Ceval.integer_expr env (!elab_expr_f loc env a) with + let expr,env = (!elab_expr_f loc env a) in + begin match Ceval.integer_expr env expr with | None -> error loc "array element designator for %s is not a compile-time constant" (I.name zi); @@ -1152,7 +1155,7 @@ and elab_item zi item il = elab_list (I.set zi ini') il false (* Single expression *) | SINGLE_INIT a, _ -> - let a' = !elab_expr_f loc env a in + let a',_ = !elab_expr_f loc env a in elab_single zi a' il (* No initializer: can this happen? *) | NO_INIT, _ -> @@ -1231,35 +1234,36 @@ let elab_expr loc env a = let error fmt = fatal_error loc fmt in let warning fmt = warning loc fmt in - let rec elab = function + let rec elab env = function (* 6.5.1 Primary expressions *) | VARIABLE s -> begin match wrap Env.lookup_ident loc env s with | (id, II_ident(sto, ty)) -> - { edesc = EVar id; etyp = ty } + { edesc = EVar id; etyp = ty },env | (id, II_enum v) -> - { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) } + { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) },env end | CONSTANT cst -> let cst' = elab_constant loc cst in - { edesc = EConst cst'; etyp = type_of_constant cst' } + { edesc = EConst cst'; etyp = type_of_constant cst' },env (* 6.5.2 Postfix expressions *) | INDEX(a1, a2) -> (* e1[e2] *) - let b1 = elab a1 in let b2 = elab a2 in + let b1,env = elab env a1 in + let b2,env = elab env a2 in let tres = match (unroll env b1.etyp, unroll env b2.etyp) with | (TPtr(t, _) | TArray(t, _, _)), (TInt _ | TEnum _) -> t | (TInt _ | TEnum _), (TPtr(t, _) | TArray(t, _, _)) -> t | t1, t2 -> error "incorrect types for array subscripting" in - { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres } + { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres },env | MEMBEROF(a1, fieldname) -> - let b1 = elab a1 in + let b1,env = elab env a1 in let (fld, attrs) = match unroll env b1.etyp with | TStruct(id, attrs) -> @@ -1271,10 +1275,10 @@ let elab_expr loc env a = (* A field of a const/volatile struct or union is itself const/volatile *) { edesc = EUnop(Odot fieldname, b1); etyp = add_attributes_type (List.filter attr_inherited_by_members attrs) - (type_of_member env fld) } + (type_of_member env fld) },env | MEMBEROFPTR(a1, fieldname) -> - let b1 = elab a1 in + let b1,env = elab env a1 in let (fld, attrs) = match unroll env b1.etyp with | TPtr(t, _) | TArray(t,_,_) -> @@ -1290,7 +1294,7 @@ let elab_expr loc env a = error "left-hand side of '->' is not a pointer " in { edesc = EUnop(Oarrow fieldname, b1); etyp = add_attributes_type (List.filter attr_inherited_by_members attrs) - (type_of_member env fld) } + (type_of_member env fld) },env (* Hack to treat vararg.h functions the GCC way. Helps with testing. va_start(ap,n) @@ -1301,9 +1305,11 @@ let elab_expr loc env a = (elaboration) --> __builtin_va_arg(ap, sizeof(ty)) *) | CALL((VARIABLE "__builtin_va_start" as a1), [a2; a3]) -> - let b1 = elab a1 and b2 = elab a2 and _b3 = elab a3 in + let b1,env = elab env a1 in + let b2,env = elab env a2 in + let _b3,env = elab env a3 in { edesc = ECall(b1, [b2]); - etyp = TVoid [] } + etyp = TVoid [] },env | BUILTIN_VA_ARG (a2, a3) -> let ident = @@ -1311,17 +1317,18 @@ let elab_expr loc env a = | (id, II_ident(sto, ty)) -> { edesc = EVar id; etyp = ty } | _ -> assert false in - let b2 = elab a2 and b3 = elab (TYPE_SIZEOF a3) in + let b2,env = elab env a2 in + let b3,env = elab env (TYPE_SIZEOF a3) in let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in let ty' = default_argument_conversion env ty in if not (compatible_types AttrIgnoreTop env ty ty') then warning "'%a' is promoted to '%a' when passed through '...'.@ You should pass '%a', not '%a', to 'va_arg'" Cprint.typ ty Cprint.typ ty' Cprint.typ ty' Cprint.typ ty; - { edesc = ECall(ident, [b2; b3]); etyp = ty } + { edesc = ECall(ident, [b2; b3]); etyp = ty },env | CALL(a1, al) -> - let b1 = + let b1,env = (* Catch the old-style usage of calling a function without having declared it *) match a1 with @@ -1331,9 +1338,9 @@ let elab_expr loc env a = (* Emit an extern declaration for it *) let id = Env.fresh_ident n in emit_elab env loc (Gdecl(Storage_extern, id, ty, None)); - { edesc = EVar id; etyp = ty } - | _ -> elab a1 in - let bl = List.map elab al in + { edesc = EVar id; etyp = ty },env + | _ -> elab env a1 in + let bl = mmap elab env al in (* Extract type information *) let (res, args, vararg) = match unroll env b1.etyp with @@ -1346,11 +1353,11 @@ let elab_expr loc env a = | _ -> error "the function part of a call does not have a function type" in (* Type-check the arguments against the prototype *) - let bl' = + let bl',env = match args with | None -> bl | Some proto -> elab_arguments 1 bl proto vararg in - { edesc = ECall(b1, bl'); etyp = res } + { edesc = ECall(b1, bl'); etyp = res },env | UNARY(POSINCR, a1) -> elab_pre_post_incr_decr Opostincr "postfix '++'" a1 @@ -1361,24 +1368,24 @@ let elab_expr loc env a = | CAST ((spec, dcl), SINGLE_INIT a1) -> let (ty, _) = elab_type loc env spec dcl in - let b1 = elab a1 in + let b1,env = elab env a1 in if not (wrap2 valid_cast loc env b1.etyp ty) then err "illegal cast from %a@ to %a" Cprint.typ b1.etyp Cprint.typ ty; - { edesc = ECast(ty, b1); etyp = ty } + { edesc = ECast(ty, b1); etyp = ty },env (* 6.5.2.5 Compound literals *) | CAST ((spec, dcl), ie) -> let (ty, _) = elab_type loc env spec dcl in begin match elab_initializer loc env "" ty ie with - | (ty', Some i) -> { edesc = ECompound(ty', i); etyp = ty' } + | (ty', Some i) -> { edesc = ECompound(ty', i); etyp = ty' },env | (ty', None) -> error "ill-formed compound literal" end (* 6.5.3 Unary expressions *) | EXPR_SIZEOF a1 -> - let b1 = elab a1 in + let b1,env = elab env a1 in if wrap incomplete_type loc env b1.etyp then err "incomplete type %a" Cprint.typ b1.etyp; let bdesc = @@ -1392,52 +1399,52 @@ let elab_expr loc env a = EConst(CInt(Int64.of_int sz, size_t_ikind(), "")) | _ -> ESizeof b1.etyp in - { edesc = bdesc; etyp = TInt(size_t_ikind(), []) } + { edesc = bdesc; etyp = TInt(size_t_ikind(), []) },env | TYPE_SIZEOF (spec, dcl) -> let (ty, env') = elab_type loc env spec dcl in if wrap incomplete_type loc env' ty then err "incomplete type %a" Cprint.typ ty; - { edesc = ESizeof ty; etyp = TInt(size_t_ikind(), []) } + { edesc = ESizeof ty; etyp = TInt(size_t_ikind(), []) },env' | EXPR_ALIGNOF a1 -> - let b1 = elab a1 in + let b1,env = elab env a1 in if wrap incomplete_type loc env b1.etyp then err "incomplete type %a" Cprint.typ b1.etyp; - { edesc = EAlignof b1.etyp; etyp = TInt(size_t_ikind(), []) } + { edesc = EAlignof b1.etyp; etyp = TInt(size_t_ikind(), []) },env | TYPE_ALIGNOF (spec, dcl) -> let (ty, env') = elab_type loc env spec dcl in if wrap incomplete_type loc env' ty then err "incomplete type %a" Cprint.typ ty; - { edesc = EAlignof ty; etyp = TInt(size_t_ikind(), []) } + { edesc = EAlignof ty; etyp = TInt(size_t_ikind(), []) },env | UNARY(PLUS, a1) -> - let b1 = elab a1 in + let b1,env = elab env a1 in if not (is_arith_type env b1.etyp) then err "argument of unary '+' is not an arithmetic type"; - { edesc = EUnop(Oplus, b1); etyp = unary_conversion env b1.etyp } + { edesc = EUnop(Oplus, b1); etyp = unary_conversion env b1.etyp },env | UNARY(MINUS, a1) -> - let b1 = elab a1 in + let b1,env = elab env a1 in if not (is_arith_type env b1.etyp) then err "argument of unary '-' is not an arithmetic type"; - { edesc = EUnop(Ominus, b1); etyp = unary_conversion env b1.etyp } + { edesc = EUnop(Ominus, b1); etyp = unary_conversion env b1.etyp },env | UNARY(BNOT, a1) -> - let b1 = elab a1 in + let b1,env = elab env a1 in if not (is_integer_type env b1.etyp) then err "argument of '~' is not an integer type"; - { edesc = EUnop(Onot, b1); etyp = unary_conversion env b1.etyp } + { edesc = EUnop(Onot, b1); etyp = unary_conversion env b1.etyp },env | UNARY(NOT, a1) -> - let b1 = elab a1 in + let b1,env = elab env a1 in if not (is_scalar_type env b1.etyp) then err "argument of '!' is not a scalar type"; - { edesc = EUnop(Olognot, b1); etyp = TInt(IInt, []) } + { edesc = EUnop(Olognot, b1); etyp = TInt(IInt, []) },env | UNARY(ADDROF, a1) -> - let b1 = elab a1 in + let b1,env = elab env a1 in if not (is_lvalue b1 || is_function_type env b1.etyp) then err "argument of '&' is not an l-value"; begin match b1.edesc with @@ -1457,15 +1464,15 @@ let elab_expr loc env a = err "address of bit-field '%s' requested" f | _ -> () end; - { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.etyp, []) } + { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.etyp, []) },env | UNARY(MEMOF, a1) -> - let b1 = elab a1 in + let b1,env = elab env a1 in begin match unroll env b1.etyp with (* '*' applied to a function type has no effect *) - | TFun _ -> b1 + | TFun _ -> b1,env | TPtr(ty, _) | TArray(ty, _, _) -> - { edesc = EUnop(Oderef, b1); etyp = ty } + { edesc = EUnop(Oderef, b1); etyp = ty },env | _ -> error "argument of unary '*' is not a pointer" end @@ -1487,8 +1494,8 @@ let elab_expr loc env a = elab_binary_integer "/" Omod a1 a2 | BINARY(ADD, a1, a2) -> - let b1 = elab a1 in - let b2 = elab a2 in + let b1,env = elab env a1 in + let b2,env = elab env a2 in let tyres = if is_arith_type env b1.etyp && is_arith_type env b2.etyp then binary_conversion env b1.etyp b2.etyp @@ -1502,11 +1509,11 @@ let elab_expr loc env a = err "illegal pointer arithmetic in binary '+'"; TPtr(ty, []) end in - { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres } + { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres },env | BINARY(SUB, a1, a2) -> - let b1 = elab a1 in - let b2 = elab a2 in + let b1,env = elab env a1 in + let b2,env = elab env a2 in let (tyop, tyres) = if is_arith_type env b1.etyp && is_arith_type env b2.etyp then begin let tyres = binary_conversion env b1.etyp b2.etyp in @@ -1532,7 +1539,7 @@ let elab_expr loc env a = (TPtr(ty1, []), TInt(ptrdiff_t_ikind(), [])) | _, _ -> error "type error in binary '-'" end in - { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres } + { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres },env | BINARY(SHL, a1, a2) -> elab_shift "<<" Oshl a1 a2 @@ -1569,15 +1576,15 @@ let elab_expr loc env a = (* 6.5.15 Conditional expressions *) | QUESTION(a1, a2, a3) -> - let b1 = elab a1 in - let b2 = elab a2 in - let b3 = elab a3 in + let b1,env = elab env a1 in + let b2,env = elab env a2 in + let b3,env = elab env a3 in if not (is_scalar_type env b1.etyp) then err ("the first argument of '? :' is not a scalar type"); begin match pointer_decay env b2.etyp, pointer_decay env b3.etyp with | (TInt _ | TFloat _ | TEnum _), (TInt _ | TFloat _ | TEnum _) -> { edesc = EConditional(b1, b2, b3); - etyp = binary_conversion env b2.etyp b3.etyp } + etyp = binary_conversion env b2.etyp b3.etyp },env | TPtr(ty1, a1), TPtr(ty2, a2) -> let tyres = if is_void_type env ty1 || is_void_type env ty2 then @@ -1592,24 +1599,24 @@ let elab_expr loc env a = TPtr(TVoid (add_attributes a1 a2), []) | Some ty -> ty in - { edesc = EConditional(b1, b2, b3); etyp = tyres } + { edesc = EConditional(b1, b2, b3); etyp = tyres },env | TPtr(ty1, a1), TInt _ when is_literal_0 b3 -> - { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, []) } + { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, []) },env | TInt _, TPtr(ty2, a2) when is_literal_0 b2 -> - { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, []) } + { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, []) },env | ty1, ty2 -> match combine_types AttrIgnoreAll env ty1 ty2 with | None -> error ("the second and third arguments of '? :' have incompatible types") | Some tyres -> - { edesc = EConditional(b1, b2, b3); etyp = tyres } + { edesc = EConditional(b1, b2, b3); etyp = tyres },env end (* 6.5.16 Assignment expressions *) | BINARY(ASSIGN, a1, a2) -> - let b1 = elab a1 in - let b2 = elab a2 in + let b1,env = elab env a1 in + let b2,env = elab env a2 in if List.mem AConst (attributes_of_type env b1.etyp) then err "left-hand side of assignment has 'const' type"; if not (is_modifiable_lvalue env b1) then @@ -1622,7 +1629,7 @@ let elab_expr loc env a = err "assigning a value of type@ %a@ to a lvalue of type@ %a" Cprint.typ b2.etyp Cprint.typ b1.etyp; end; - { edesc = EBinop(Oassign, b1, b2, b1.etyp); etyp = b1.etyp } + { edesc = EBinop(Oassign, b1, b2, b1.etyp); etyp = b1.etyp },env | BINARY((ADD_ASSIGN | SUB_ASSIGN | MUL_ASSIGN | DIV_ASSIGN | MOD_ASSIGN | BAND_ASSIGN | BOR_ASSIGN | XOR_ASSIGN | SHL_ASSIGN | SHR_ASSIGN @@ -1640,8 +1647,8 @@ let elab_expr loc env a = | SHL_ASSIGN -> (SHL, Oshl_assign) | SHR_ASSIGN -> (SHR, Oshr_assign) | _ -> assert false in - begin match elab (BINARY(sop, a1, a2)) with - | { edesc = EBinop(_, b1, b2, _); etyp = ty } as b -> + begin match elab env (BINARY(sop, a1, a2)) with + | ({ edesc = EBinop(_, b1, b2, _); etyp = ty } as b),env -> if List.mem AConst (attributes_of_type env b1.etyp) then err "left-hand side of assignment has 'const' type"; if not (is_modifiable_lvalue env b1) then @@ -1654,63 +1661,63 @@ let elab_expr loc env a = err "assigning a value of type@ %a@ to a lvalue of type@ %a" Cprint.typ ty Cprint.typ b1.etyp; end; - { edesc = EBinop(top, b1, b2, ty); etyp = b1.etyp } + { edesc = EBinop(top, b1, b2, ty); etyp = b1.etyp },env | _ -> assert false end (* 6.5.17 Sequential expressions *) | BINARY(COMMA, a1, a2) -> - let b1 = elab a1 in - let b2 = elab a2 in - { edesc = EBinop (Ocomma, b1, b2, b2.etyp); etyp = b2.etyp } + let b1,env = elab env a1 in + let b2,env = elab env a2 in + { edesc = EBinop (Ocomma, b1, b2, b2.etyp); etyp = b2.etyp },env (* Elaboration of pre- or post- increment/decrement *) and elab_pre_post_incr_decr op msg a1 = - let b1 = elab a1 in + let b1,env = elab env a1 in if not (is_modifiable_lvalue env b1) then err "the argument of %s is not a modifiable l-value" msg; if not (is_scalar_type env b1.etyp) then err "the argument of %s must be an arithmetic or pointer type" msg; - { edesc = EUnop(op, b1); etyp = b1.etyp } + { edesc = EUnop(op, b1); etyp = b1.etyp },env (* Elaboration of binary operators over integers *) and elab_binary_integer msg op a1 a2 = - let b1 = elab a1 in + let b1,env = elab env a1 in if not (is_integer_type env b1.etyp) then error "the first argument of '%s' is not an integer type" msg; - let b2 = elab a2 in + let b2,env = elab env a2 in if not (is_integer_type env b2.etyp) then error "the second argument of '%s' is not an integer type" msg; let tyres = binary_conversion env b1.etyp b2.etyp in - { edesc = EBinop(op, b1, b2, tyres); etyp = tyres } + { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env (* Elaboration of binary operators over arithmetic types *) and elab_binary_arithmetic msg op a1 a2 = - let b1 = elab a1 in + let b1,env = elab env a1 in if not (is_arith_type env b1.etyp) then error "the first argument of '%s' is not an arithmetic type" msg; - let b2 = elab a2 in + let b2,env = elab env a2 in if not (is_arith_type env b2.etyp) then error "the second argument of '%s' is not an arithmetic type" msg; let tyres = binary_conversion env b1.etyp b2.etyp in - { edesc = EBinop(op, b1, b2, tyres); etyp = tyres } + { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env (* Elaboration of shift operators *) and elab_shift msg op a1 a2 = - let b1 = elab a1 in + let b1,env = elab env a1 in if not (is_integer_type env b1.etyp) then error "the first argument of '%s' is not an integer type" msg; - let b2 = elab a2 in + let b2,env = elab env a2 in if not (is_integer_type env b2.etyp) then error "the second argument of '%s' is not an integer type" msg; let tyres = unary_conversion env b1.etyp in - { edesc = EBinop(op, b1, b2, tyres); etyp = tyres } + { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env (* Elaboration of comparisons *) and elab_comparison op a1 a2 = - let b1 = elab a1 in - let b2 = elab a2 in + let b1,env = elab env a1 in + let b2,env = elab env a2 in let resdesc = match pointer_decay env b1.etyp, pointer_decay env b2.etyp with | (TInt _ | TFloat _ | TEnum _), (TInt _ | TFloat _ | TEnum _) -> @@ -1736,28 +1743,28 @@ let elab_expr loc env a = | _, _ -> error "illegal comparison between types@ %a@ and %a" Cprint.typ b1.etyp Cprint.typ b2.etyp in - { edesc = resdesc; etyp = TInt(IInt, []) } + { edesc = resdesc; etyp = TInt(IInt, []) },env (* Elaboration of && and || *) and elab_logical_operator msg op a1 a2 = - let b1 = elab a1 in + let b1,env = elab env a1 in if not (is_scalar_type env b1.etyp) then err "the first argument of '%s' is not a scalar type" msg; - let b2 = elab a2 in + let b2,env = elab env a2 in if not (is_scalar_type env b2.etyp) then err "the second argument of '%s' is not a scalar type" msg; - { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []) } + { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []) },env (* Type-checking of function arguments *) and elab_arguments argno args params vararg = match args, params with - | [], [] -> [] - | [], _::_ -> err "not enough arguments in function call"; [] - | _::_, [] -> + | ([],env), [] -> [],env + | ([],env), _::_ -> err "not enough arguments in function call"; [], env + | (_::_,env), [] -> if vararg - then args + then args else (err "too many arguments in function call"; args) - | arg1 :: argl, (_, ty_p) :: paraml -> + | (arg1 :: argl,env), (_, ty_p) :: paraml -> let ty_a = argument_conversion env arg1.etyp in if not (wrap2 valid_assignment loc env {arg1 with etyp = ty_a} ty_p) then begin @@ -1772,20 +1779,22 @@ let elab_expr loc env a = instead of the expected type@ %a" argno Cprint.typ ty_a Cprint.typ ty_p end; - arg1 :: elab_arguments (argno + 1) argl paraml vararg - - in elab a + let rest,env = elab_arguments (argno + 1) (argl,env) paraml vararg in + arg1 :: rest,env + in elab env a (* Filling in forward declaration *) let _ = elab_expr_f := elab_expr let elab_opt_expr loc env = function - | None -> None - | Some a -> Some (elab_expr loc env a) + | None -> None,env + | Some a -> let a,env = (elab_expr loc env a) in + Some a,env let elab_for_expr loc env = function - | None -> { sdesc = Sskip; sloc = elab_loc loc } - | Some a -> { sdesc = Sdo (elab_expr loc env a); sloc = elab_loc loc } + | None -> { sdesc = Sskip; sloc = elab_loc loc },env + | Some a -> let a,env = elab_expr loc env a in + { sdesc = Sdo a; sloc = elab_loc loc },env (* Handling of __func__ (section 6.4.2.2) *) @@ -2042,8 +2051,8 @@ and elab_definitions local env = function let elab_asm_operand loc env (ASMOPERAND(label, wide, chars, e)) = let s = elab_simple_string loc wide chars in - let e' = elab_expr loc env e in - (label, s, e') + let e',env = elab_expr loc env e in + (label, s, e'),env (* Contexts for elaborating statements *) @@ -2091,24 +2100,28 @@ let rec elab_stmt env ctx s = (* 6.8.3 Expression statements *) | COMPUTATION(a, loc) -> - { sdesc = Sdo (elab_expr loc env a); sloc = elab_loc loc } + let a,env = (elab_expr loc env a) in + { sdesc = Sdo a; sloc = elab_loc loc },env (* 6.8.1 Labeled statements *) | LABEL(lbl, s1, loc) -> - { sdesc = Slabeled(Slabel lbl, elab_stmt env ctx s1); sloc = elab_loc loc } + let s1,env = elab_stmt env ctx s1 in + { sdesc = Slabeled(Slabel lbl, s1); sloc = elab_loc loc },env | CASE(a, s1, loc) -> - let a' = elab_expr loc env a in + let a',env = elab_expr loc env a in begin match Ceval.integer_expr env a' with | None -> error loc "argument of 'case' must be an integer compile-time constant" | Some n -> () end; - { sdesc = Slabeled(Scase a', elab_stmt env ctx s1); sloc = elab_loc loc } + let s1,env = elab_stmt env ctx s1 in + { sdesc = Slabeled(Scase a', s1); sloc = elab_loc loc },env | DEFAULT(s1, loc) -> - { sdesc = Slabeled(Sdefault, elab_stmt env ctx s1); sloc = elab_loc loc } + let s1,env = elab_stmt env ctx s1 in + { sdesc = Slabeled(Sdefault, s1); sloc = elab_loc loc },env (* 6.8.2 Compound statements *) @@ -2118,81 +2131,83 @@ let rec elab_stmt env ctx s = (* 6.8.4 Conditional statements *) | If(a, s1, s2, loc) -> - let a' = elab_expr loc env a in + let a',env = elab_expr loc env a in if not (is_scalar_type env a'.etyp) then error loc "the condition of 'if' does not have scalar type"; - let s1' = elab_stmt env ctx s1 in - let s2' = + let s1',env = elab_stmt env ctx s1 in + let s2',env = match s2 with - | None -> sskip + | None -> sskip,env | Some s2 -> elab_stmt env ctx s2 in - { sdesc = Sif(a', s1', s2'); sloc = elab_loc loc } + { sdesc = Sif(a', s1', s2'); sloc = elab_loc loc },env (* 6.8.5 Iterative statements *) | WHILE(a, s1, loc) -> - let a' = elab_expr loc env a in + let a',env = elab_expr loc env a in if not (is_scalar_type env a'.etyp) then error loc "the condition of 'while' does not have scalar type"; - let s1' = elab_stmt env (ctx_loop ctx) s1 in - { sdesc = Swhile(a', s1'); sloc = elab_loc loc } + let s1',env = elab_stmt env (ctx_loop ctx) s1 in + { sdesc = Swhile(a', s1'); sloc = elab_loc loc },env | DOWHILE(a, s1, loc) -> - let s1' = elab_stmt env (ctx_loop ctx) s1 in - let a' = elab_expr loc env a in + let s1',env = elab_stmt env (ctx_loop ctx) s1 in + let a',env = elab_expr loc env a in if not (is_scalar_type env a'.etyp) then error loc "the condition of 'while' does not have scalar type"; - { sdesc = Sdowhile(s1', a'); sloc = elab_loc loc } + { sdesc = Sdowhile(s1', a'); sloc = elab_loc loc },env | FOR(fc, a2, a3, s1, loc) -> let (a1', env', decls') = match fc with | Some (FC_EXP a1) -> - (elab_for_expr loc env (Some a1), env, None) + let a1,env = elab_for_expr loc env (Some a1) in + (a1, env, None) | None -> - (elab_for_expr loc env None, env, None) + let a1,env = elab_for_expr loc env None in + (a1, env, None) | Some (FC_DECL def) -> let (dcl, env') = elab_definition true (Env.new_scope env) def in let loc = elab_loc (get_definitionloc def) in (sskip, env', Some(List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl)) in - let a2' = + let a2',env = match a2 with - | None -> intconst 1L IInt + | None -> intconst 1L IInt,env | Some a2 -> elab_expr loc env' a2 in if not (is_scalar_type env' a2'.etyp) then error loc "the condition of 'for' does not have scalar type"; - let a3' = elab_for_expr loc env' a3 in - let s1' = elab_stmt env' (ctx_loop ctx) s1 in + let a3',env' = elab_for_expr loc env' a3 in + let s1',env' = elab_stmt env' (ctx_loop ctx) s1 in let sfor = { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc } in begin match decls' with - | None -> sfor - | Some sl -> { sdesc = Sblock (sl @ [sfor]); sloc = elab_loc loc } + | None -> sfor,env + | Some sl -> { sdesc = Sblock (sl @ [sfor]); sloc = elab_loc loc },env end (* 6.8.4 Switch statement *) | SWITCH(a, s1, loc) -> - let a' = elab_expr loc env a in + let a',env = elab_expr loc env a in if not (is_integer_type env a'.etyp) then error loc "the argument of 'switch' is not an integer"; - let s1' = elab_stmt env (ctx_switch ctx) s1 in - { sdesc = Sswitch(a', s1'); sloc = elab_loc loc } + let s1',env = elab_stmt env (ctx_switch ctx) s1 in + { sdesc = Sswitch(a', s1'); sloc = elab_loc loc },env (* 6.8.6 Break and continue statements *) | BREAK loc -> if not ctx.ctx_break then error loc "'break' outside of a loop or a 'switch'"; - { sdesc = Sbreak; sloc = elab_loc loc } + { sdesc = Sbreak; sloc = elab_loc loc },env | CONTINUE loc -> if not ctx.ctx_continue then error loc "'continue' outside of a loop"; - { sdesc = Scontinue; sloc = elab_loc loc } + { sdesc = Scontinue; sloc = elab_loc loc },env (* 6.8.6 Return statements *) | RETURN(a, loc) -> - let a' = elab_opt_expr loc env a in + let a',env = elab_opt_expr loc env a in begin match (unroll env ctx.ctx_return_typ, a') with | TVoid _, None -> () | TVoid _, Some _ -> @@ -2217,51 +2232,53 @@ let rec elab_stmt env ctx s = Cprint.typ b.etyp Cprint.typ ctx.ctx_return_typ end end; - { sdesc = Sreturn a'; sloc = elab_loc loc } + { sdesc = Sreturn a'; sloc = elab_loc loc },env (* 6.8.6 Goto statements *) | GOTO(lbl, loc) -> if not (StringSet.mem lbl ctx.ctx_labels) then error loc "unknown 'goto' label %s" lbl; - { sdesc = Sgoto lbl; sloc = elab_loc loc } + { sdesc = Sgoto lbl; sloc = elab_loc loc },env (* 6.8.3 Null statements *) | NOP loc -> - { sdesc = Sskip; sloc = elab_loc loc } + { sdesc = Sskip; sloc = elab_loc loc },env (* Traditional extensions *) | ASM(cv_specs, wide, chars, outputs, inputs, flags, loc) -> let a = elab_cvspecs env cv_specs in let s = elab_simple_string loc wide chars in - let outputs = List.map (elab_asm_operand loc env) outputs in - let inputs = List.map (elab_asm_operand loc env) inputs in + let outputs,env = mmap (elab_asm_operand loc) env outputs in + let inputs ,env= mmap (elab_asm_operand loc) env inputs in let flags = List.map (fun (w,c) -> elab_simple_string loc w c) flags in { sdesc = Sasm(a, s, outputs, inputs, flags); - sloc = elab_loc loc } + sloc = elab_loc loc },env (* Unsupported *) | DEFINITION def -> error (get_definitionloc def) "ill-placed definition"; - sskip + sskip,env and elab_block loc env ctx b = - let b' = elab_block_body (Env.new_scope env) ctx b in - { sdesc = Sblock b'; sloc = elab_loc loc } + let b',_ = elab_block_body (Env.new_scope env) ctx b in + { sdesc = Sblock b'; sloc = elab_loc loc },env and elab_block_body env ctx sl = match sl with | [] -> - [] + [],env | DEFINITION def :: sl1 -> let (dcl, env') = elab_definition true env def in let loc = elab_loc (get_definitionloc def) in - List.map (fun ((sto,id,ty,_) as d) -> + let dcl = List.map (fun ((sto,id,ty,_) as d) -> Debug.insert_local_declaration sto id ty loc; - {sdesc = Sdecl d; sloc = loc}) dcl - @ elab_block_body env' ctx sl1 + {sdesc = Sdecl d; sloc = loc}) dcl in + let sl1',env' = elab_block_body env' ctx sl1 in + dcl @ sl1',env' | s :: sl1 -> - let s' = elab_stmt env ctx s in - s' :: elab_block_body env ctx sl1 + let s',env = elab_stmt env ctx s in + let sl1',env = elab_block_body env ctx sl1 in + s' :: sl1',env (* Elaboration of a function body. Return the corresponding C statement. *) @@ -2271,7 +2288,7 @@ let elab_funbody return_typ env b = ctx_labels = stmt_labels b; ctx_break = false; ctx_continue = false } in - elab_stmt env ctx b + fst(elab_stmt env ctx b) (* Filling in forward declaration *) let _ = elab_funbody_f := elab_funbody -- cgit