From da54bd2b37839c7461c0fff11c2e64ac6417c680 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 17 Jul 2011 17:12:03 +0000 Subject: More precise typechecking of statements git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1686 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cparser/Elab.ml | 108 +++++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 75 insertions(+), 33 deletions(-) (limited to 'cparser/Elab.ml') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index b52299a..d42fcb4 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -94,7 +94,7 @@ let redef fn env arg = let elab_expr_f : (cabsloc -> Env.t -> Cabs.expression -> C.exp) ref = ref (fun _ _ _ -> assert false) -let elab_block_f : (cabsloc -> C.typ -> Env.t -> Cabs.block -> C.stmt) ref +let elab_funbody_f : (cabsloc -> C.typ -> Env.t -> Cabs.block -> C.stmt) ref = ref (fun _ _ _ _ -> assert false) @@ -1544,7 +1544,7 @@ let elab_fundef env (spec, name) body loc1 loc2 = List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty) (Env.new_scope env1) params in (* Elaborate function body *) - let body' = !elab_block_f loc2 ty_ret env2 body in + let body' = !elab_funbody_f loc2 ty_ret env2 body in (* Build and emit function definition *) let fn = { fd_storage = sto; @@ -1607,7 +1607,36 @@ and elab_definitions local env = function (decl1 @ decl2, env2) -(* Elaboration of statements *) +(* Contexts for elaborating statements *) + +module StringSet = Set.Make(String) + +type stmt_context = { + ctx_return_typ: typ; + ctx_labels: StringSet.t; + ctx_break: bool; + ctx_continue: bool +} + +let block_labels b = + let lbls = ref StringSet.empty in + let rec do_stmt = function + | BLOCK(b, _) -> do_block b + | IF(_, s1, s2, _) -> do_stmt s1; do_stmt s2 + | WHILE(_, s1, _) -> do_stmt s1 + | DOWHILE(_, s1, _) -> do_stmt s1 + | FOR(_, _, _, s1, _) -> do_stmt s1 + | SWITCH(_, s1, _) -> do_stmt s1 + | CASE(_, s1, _) -> do_stmt s1 + | DEFAULT(s1, _) -> do_stmt s1 + | LABEL(lbl, s1, _) -> lbls := StringSet.add lbl !lbls; do_stmt s1 + | _ -> () + and do_block b = List.iter do_stmt b.bstmts + in do_block b; !lbls + +let ctx_loop ctx = { ctx with ctx_break = true; ctx_continue = true } + +let ctx_switch ctx = { ctx with ctx_break = true } (* Extract list of Cabs statements from a Cabs block *) @@ -1618,11 +1647,10 @@ let block_body loc b = warning loc "ignoring attributes on this block"; b.bstmts -(* Elaboration of a block. Return the corresponding C statement. *) - -let elab_block loc return_typ env b = + +(* Elaboration of statements *) -let rec elab_stmt env s = +let rec elab_stmt env ctx s = match s with @@ -1634,7 +1662,7 @@ let rec elab_stmt env s = (* 8.3 Labeled statements *) | LABEL(lbl, s1, loc) -> - { sdesc = Slabeled(Slabel lbl, elab_stmt env s1); sloc = elab_loc loc } + { sdesc = Slabeled(Slabel lbl, elab_stmt env ctx s1); sloc = elab_loc loc } | CASE(a, s1, loc) -> let a' = elab_expr loc env a in @@ -1643,19 +1671,19 @@ let rec elab_stmt env s = error loc "argument of 'case' must be an integer compile-time constant" | Some n -> () end; - { sdesc = Slabeled(Scase a', elab_stmt env s1); sloc = elab_loc loc } + { sdesc = Slabeled(Scase a', elab_stmt env ctx s1); sloc = elab_loc loc } | CASERANGE(_, _, _, loc) -> error loc "GCC's 'case' with range of values is not supported"; sskip | DEFAULT(s1, loc) -> - { sdesc = Slabeled(Sdefault, elab_stmt env s1); sloc = elab_loc loc } + { sdesc = Slabeled(Sdefault, elab_stmt env ctx s1); sloc = elab_loc loc } (* 8.4 Compound statements *) | BLOCK(b, loc) -> - elab_blk loc env b + elab_block loc env ctx b (* 8.5 Conditional statements *) @@ -1663,8 +1691,8 @@ let rec elab_stmt env s = let a' = 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 s1 in - let s2' = elab_stmt env s2 in + let s1' = elab_stmt env ctx s1 in + let s2' = elab_stmt env ctx s2 in { sdesc = Sif(a', s1', s2'); sloc = elab_loc loc } (* 8.6 Iterative statements *) @@ -1673,11 +1701,11 @@ let rec elab_stmt env s = let a' = 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 s1 in + let s1' = elab_stmt env (ctx_loop ctx) s1 in { sdesc = Swhile(a', s1'); sloc = elab_loc loc } | DOWHILE(a, s1, loc) -> - let s1' = elab_stmt env s1 in + let s1' = elab_stmt env (ctx_loop ctx) s1 in let a' = 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"; @@ -1698,27 +1726,31 @@ let rec elab_stmt env s = 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 s1 in + let s1' = elab_stmt env (ctx_loop ctx) s1 in { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc } (* 8.7 Switch statement *) | SWITCH(a, s1, loc) -> let a' = elab_expr loc env a in - if not (is_arith_type env a'.etyp) then - error loc "the argument of 'switch' does not have arithmetic type"; - let s1' = elab_stmt env s1 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 } (* 8,8 Break and continue statements *) | BREAK loc -> + if not ctx.ctx_break then + error loc "'break' outside a loop or a 'switch'"; { sdesc = Sbreak; sloc = elab_loc loc } | CONTINUE loc -> + if not ctx.ctx_continue then + error loc "'continue' outside a loop"; { sdesc = Scontinue; sloc = elab_loc loc } (* 8.9 Return statements *) | RETURN(a, loc) -> let a' = elab_opt_expr loc env a in - begin match (unroll env return_typ, a') with + begin match (unroll env ctx.ctx_return_typ, a') with | TVoid _, None -> () | TVoid _, Some _ -> error loc @@ -1726,25 +1758,27 @@ let rec elab_stmt env s = | _, None -> warning loc "'return' without a value in a function of return type@ %a" - Cprint.typ return_typ + Cprint.typ ctx.ctx_return_typ | _, Some b -> - if not (valid_assignment env b return_typ) then begin - if valid_cast env b.etyp return_typ then + if not (valid_assignment env b ctx.ctx_return_typ) then begin + if valid_cast env b.etyp ctx.ctx_return_typ then warning loc "return value has type@ %a@ \ instead of the expected type@ %a" - Cprint.typ b.etyp Cprint.typ return_typ + Cprint.typ b.etyp Cprint.typ ctx.ctx_return_typ else error loc "return value has type@ %a@ \ instead of the expected type@ %a" - Cprint.typ b.etyp Cprint.typ return_typ + Cprint.typ b.etyp Cprint.typ ctx.ctx_return_typ end end; { sdesc = Sreturn a'; sloc = elab_loc loc } (* 8.10 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 } (* 8.11 Null statements *) @@ -1768,11 +1802,11 @@ let rec elab_stmt env s = error loc "'try ... finally' statement is not supported"; sskip -and elab_blk loc env b = - let b' = elab_blk_body (Env.new_scope env) (block_body loc b) in +and elab_block loc env ctx b = + let b' = elab_block_body (Env.new_scope env) ctx (block_body loc b) in { sdesc = Sblock b'; sloc = elab_loc loc } -and elab_blk_body env sl = +and elab_block_body env ctx sl = match sl with | [] -> [] @@ -1780,15 +1814,23 @@ and elab_blk_body env sl = let (dcl, env') = elab_definition true env def in let loc = elab_loc (get_definitionloc def) in List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl - @ elab_blk_body env' sl1 + @ elab_block_body env' ctx sl1 | s :: sl1 -> - let s' = elab_stmt env s in - s' :: elab_blk_body env sl1 + let s' = elab_stmt env ctx s in + s' :: elab_block_body env ctx sl1 + +(* Elaboration of a function body. Return the corresponding C statement. *) -in elab_blk loc env b +let elab_funbody loc return_typ env b = + let ctx = + { ctx_return_typ = return_typ; + ctx_labels = block_labels b; + ctx_break = false; + ctx_continue = false } in + elab_block loc env ctx b (* Filling in forward declaration *) -let _ = elab_block_f := elab_block +let _ = elab_funbody_f := elab_funbody (** * Entry point *) -- cgit v1.2.3