From 5a7fc8637ae82d9aaf71c0053078a950ddee3b89 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 7 Feb 2017 09:57:45 +0100 Subject: More precise warnings about function returns This commit introduces a control-flow static analysis over C abstract syntax (file cparser/Cflow.ml) and uses it to - warn for non-void functions that can return by falling through the body - warn more precisely for _Noreturn functions that can return - introduce the "return 0" in "main" functions less often (cosmetic). For the control-flow analysis, the following conservative approximations are made: - any "goto" label is reachable - all cases of a "switch" statement are reachable as soon as the "switch" is reachable (i.e. the switch expression takes all values needed to reach every case) - the boolean expressions in "if", "while", "do"-"while" and "for" can take true and false values, unless they are compile-time constants. --- cparser/Cflow.ml | 195 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ cparser/Cflow.mli | 24 +++++++ cparser/Cutil.ml | 21 ------ cparser/Cutil.mli | 5 -- cparser/Elab.ml | 24 +++++-- 5 files changed, 237 insertions(+), 32 deletions(-) create mode 100644 cparser/Cflow.ml create mode 100644 cparser/Cflow.mli (limited to 'cparser') diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml new file mode 100644 index 00000000..49a85332 --- /dev/null +++ b/cparser/Cflow.ml @@ -0,0 +1,195 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* A simple control flow analysis for C statements. + Main purpose: emit warnings for _Noreturn functions. *) + +open C +open Cutil + +(* Statements are abstracted as "flow transformers": + functions from possible inputs to possible outcomes. + Possible inputs are: + - start normally at the beginning of the statement + - start at a "case" or "default" label because of an enclosing switch + Possible outputs are: + - terminate normally and fall through + - terminate early on "break" + - terminate early on "continue" + - terminate early on "return" +*) + +type flow = bool -> (* start normally at beginning of statement *) + bool -> (* start at "case"/"default" label *) + int +(* Outputs are encoded as bit masks in an integer *) + +let _None = 0 +let _Fallthrough = 1 +let _Break = 2 +let _Continue = 4 +let _Return = 8 +let can flag out = out land flag <> 0 +let add flag out = out lor flag +let remove flag out = out land (lnot flag) +let join out1 out2 = out1 lor out2 + +(* Some elementary flows *) + +let normal : flow = fun i is -> if i then _Fallthrough else _None +let break : flow = fun i is -> if i then _Break else _None +let continue : flow = fun i is -> if i then _Continue else _None +let return : flow = fun i is -> if i then _Return else _None +let noflow : flow = fun i is -> _None + +(* Some flow transformers *) + +(* Sequential composition *) + +let seq (s1: flow) (s2: flow) : flow = fun i is -> + let o1 = s1 i is in + let o2 = s2 (can _Fallthrough o1) is in + join (remove _Fallthrough o1) o2 + +(* Nondeterministic choice *) + +let either (s1: flow) (s2: flow) : flow = fun i is -> + join (s1 i is) (s2 i is) + +(* If-then-else, with special cases for conditions that are always true + or always false. *) + +let resolve_test env e = + match Ceval.integer_expr env e with + | None -> None + | Some n -> Some (n <> 0L) + +let if_ env e (s1: flow) (s2: flow) : flow = + match resolve_test env e with + | Some true -> s1 + | Some false -> s2 + | None -> either s1 s2 + +(* Convert "continue" into "fallthrough". Typically applied to a loop body. *) + +let catch_continue (s: flow) : flow = fun i is -> + let o = s i is in + if can _Continue o then add _Fallthrough (remove _Continue o) else o + +(* Convert "continue" into "fallthrough". Typically applied to a loop. *) + +let catch_break (s: flow) : flow = fun i is -> + let o = s i is in + if can _Break o then add _Fallthrough (remove _Break o) else o + +(* For goto-labeled statements we assume they can always be entered normally. *) + +let label (s: flow) : flow = fun i is -> s true is + +(* For "case" and "default" labeled statements, we assume they can be entered + normally as soon as the nearest enclosing "switch" can be entered normally. *) + +let case (s: flow) : flow = fun i is -> s is is + +let switch (s: flow) : flow = fun i is -> s false i + +(* This is the flow for an infinite loop with body [s]. + There is no fallthrough exit, but all other exits from [s] are preserved. *) + +let loop (s: flow) : flow = fun i is -> + let o = s i is in + if (not i) && can _Fallthrough o then + (* Corner case: on the first iteration, [s] was not entered normally, + but it exits by fallthrough. Then on the next iteration [s] is + entered normally. So, we need to recompute the flow of [s] + assuming it is entered normally. *) + s true is + else + (* In all other cases, iterating [s] once more does not produce new + exits that we did not compute on the first iteration. Just remove + the fallthrough exit. *) + remove _Fallthrough o + +(* This is the main analysis function. Given a C statement [s] it returns + a flow that overapproximates the behavior of [s]. *) + +let rec outcomes env s : flow = + match s.sdesc with + | Sskip -> + normal + | Sdo {edesc = ECall(fn, args)} -> + if find_custom_attributes ["noreturn"; "__noreturn__"] + (attributes_of_type env fn.etyp) = [] + then normal else noflow + | Sdo e -> + normal + | Sseq(s1, s2) -> + seq (outcomes env s1) (outcomes env s2) + | Sif(e, s1, s2) -> + if_ env e (outcomes env s1) (outcomes env s2) + | Swhile(e, s) -> + catch_break ( + loop ( + if_ env e + (catch_continue (outcomes env s)) (* e is true: execute body [s] *) + break)) (* e is false: exit loop *) + | Sdowhile(s, e) -> + catch_break ( + loop ( + seq (catch_continue (outcomes env s)) (* do the body *) + (if_ env e normal break))) (* then continue or break *) + | Sfor(s1, e, s2, s3) -> + seq (outcomes env s1) (* initialization, runs once *) + (catch_break ( + loop ( + if_ env e (* e is true: do body, do next *) + (seq (catch_continue (outcomes env s2)) (outcomes env s3)) + break))) (* e is false: exit loop *) + | Sbreak -> + break + | Scontinue -> + continue + | Sswitch(e, s) -> + catch_break (switch (outcomes env s)) + | Slabeled(Slabel _, s) -> + label (outcomes env s) + | Slabeled((Scase _ | Sdefault), s) -> + case (outcomes env s) + | Sgoto _ -> + noflow + | Sreturn opte -> + return + | Sblock sl -> + outcomes_block env sl + | Sdecl dcl -> + normal + | Sasm _ -> + normal + +and outcomes_block env sl = + match sl with + | [] -> + normal + | s1 :: sl -> + seq (outcomes env s1) (outcomes_block env sl) + +(* This is the entry point in this module. Given the body of a function, + estimate if and how this function can return. *) + +let function_returns env body = + let o = outcomes env body true false in + (* First boolean is: function can return + Second boolean is: function can return by fall-through *) + (can _Fallthrough o || can _Return o, can _Fallthrough o) diff --git a/cparser/Cflow.mli b/cparser/Cflow.mli new file mode 100644 index 00000000..0de245ae --- /dev/null +++ b/cparser/Cflow.mli @@ -0,0 +1,24 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* A simple control flow analysis for C statements. + Main purpose: emit warnings for _Noreturn functions. *) + +val function_returns: Env.t -> C.stmt -> bool * bool + (** Given a function body, returns two Booleans: + - the first says whether the function can return + - the second says whether the function can return by falling through + the end of its body. + Both are over-approximations. *) diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 8a59c147..735dd99b 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -1183,24 +1183,3 @@ let rec subst_stmt phi s = List.map subst_asm_operand inputs, clob) } - -let contains_return s = - let rec aux s = - match s.sdesc with - | Sskip - | Sbreak - | Scontinue - | Sdo _ - | Sdecl _ - | Sasm _ - | Sgoto _ -> false - | Sif(_, s1, s2) - | Sseq(s1, s2) -> aux s1 || aux s2 - | Sswitch (_, s) - | Slabeled (_, s) - | Swhile (_, s) - | Sdowhile(s, _ ) -> aux s - | Sfor(s1, _ , s2, s3) -> aux s1 || aux s2 || aux s3 - | Sreturn _ -> true - | Sblock sl -> List.fold_left (fun acc s -> acc || aux s) false sl in - aux s diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 4eaa9e4a..bd5a2c3e 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -285,8 +285,3 @@ val subst_expr: exp IdentMap.t -> exp -> exp val subst_init: exp IdentMap.t -> init -> init val subst_decl: exp IdentMap.t -> decl -> decl val subst_stmt: exp IdentMap.t -> stmt -> stmt - -(* Statement properties *) - -val contains_return: stmt -> bool - (* Does the stmt contain a return. *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 69830122..76f0c998 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2329,18 +2329,30 @@ let elab_fundef env spec name defs body loc = (Gdecl(Storage_static, func_id, func_ty, Some func_init)); (* Elaborate function body *) let body1 = !elab_funbody_f ty_ret vararg env3 body in - (* Special treatment of the "main" function *) + (* Analyse it for returns *) + let (can_return, can_fallthrough) = Cflow.function_returns env3 body1 in + (* Special treatment of the "main" function. *) let body2 = if s = "main" then begin match unroll env ty_ret with | TInt(IInt, []) -> - (* Add implicit "return 0;" at end of function body *) - sseq no_loc body1 - {sdesc = Sreturn(Some(intconst 0L IInt)); sloc = no_loc} + (* Add implicit "return 0;" at end of function body, unless + this control point is unreachable, e.g. function already + returns in all cases. *) + if can_fallthrough then + sseq no_loc body1 + {sdesc = Sreturn(Some(intconst 0L IInt)); sloc = no_loc} + else body1 | _ -> warning loc Main_return_type "return type of 'main' should be 'int'"; body1 - end else body1 in + end else begin + (* For non-"main" functions, warn if the body can fall through + and the return type is not "void". *) + if can_fallthrough && not (is_void_type env ty_ret) then + warning loc Return_type "control reaches end of non-void function"; + body1 + end in (* Add the extra declarations if any *) let body3 = if extra_decls = [] then body2 else begin @@ -2352,7 +2364,7 @@ let elab_fundef env spec name defs body loc = if noret then warning loc Celeven_extension "_Noreturn functions are a C11 extension"; if (noret || find_custom_attributes ["noreturn"; "__noreturn__"] attr <> []) - && contains_return body1 then + && can_return then warning loc Invalid_noreturn "function '%s' declared 'noreturn' should not return" s; (* Build and emit function definition *) let fn = -- cgit From 178e71c74a034d7ea13645ab843f4dd0e23a3255 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 7 Feb 2017 10:29:58 +0100 Subject: Control-flow analysis: wrong flow for "case"/"default" statements Those labeled statements can be entered either by fall-through or by the enclosing switch. --- cparser/Cflow.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'cparser') diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml index 49a85332..dfa6ad72 100644 --- a/cparser/Cflow.ml +++ b/cparser/Cflow.ml @@ -94,14 +94,16 @@ let catch_break (s: flow) : flow = fun i is -> let o = s i is in if can _Break o then add _Fallthrough (remove _Break o) else o -(* For goto-labeled statements we assume they can always be entered normally. *) +(* For goto-labeled statements we assume they can always be entered by + a goto. *) let label (s: flow) : flow = fun i is -> s true is -(* For "case" and "default" labeled statements, we assume they can be entered - normally as soon as the nearest enclosing "switch" can be entered normally. *) +(* For "case" and "default" labeled statements, we assume they can be + entered normally as soon as the nearest enclosing "switch" can be + entered normally. *) -let case (s: flow) : flow = fun i is -> s is is +let case (s: flow) : flow = fun i is -> s (i || is) is let switch (s: flow) : flow = fun i is -> s false i -- cgit From 65103cdcf96b8c0411c9a7fec62a00daf6b5cb2e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 7 Feb 2017 14:33:29 +0100 Subject: Revised, more precise implementation of control-flow analysis The new implementation keeps track of goto labels that are actually branched to. It is less optimized than the previous implementation (no bit vectors) but perhaps easier to read. --- cparser/Cflow.ml | 146 +++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 98 insertions(+), 48 deletions(-) (limited to 'cparser') diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml index dfa6ad72..7de5cf59 100644 --- a/cparser/Cflow.ml +++ b/cparser/Cflow.ml @@ -19,54 +19,95 @@ open C open Cutil +module StringSet = Set.Make(String) + (* Statements are abstracted as "flow transformers": functions from possible inputs to possible outcomes. Possible inputs are: - start normally at the beginning of the statement - start at a "case" or "default" label because of an enclosing switch + - start at a named label because of a "goto" Possible outputs are: - terminate normally and fall through - terminate early on "break" - terminate early on "continue" - terminate early on "return" + - terminate early on "goto" to a label *) -type flow = bool -> (* start normally at beginning of statement *) - bool -> (* start at "case"/"default" label *) - int -(* Outputs are encoded as bit masks in an integer *) - -let _None = 0 -let _Fallthrough = 1 -let _Break = 2 -let _Continue = 4 -let _Return = 8 -let can flag out = out land flag <> 0 -let add flag out = out lor flag -let remove flag out = out land (lnot flag) -let join out1 out2 = out1 lor out2 +type flow = inflow -> outflow + +and inflow = { + inormal: bool; (* start normally at beginning of statement *) + iswitch: bool; (* start at any "case" or "default" label *) + igoto: StringSet.t; (* start at one of the goto labels in the set *) +} + +and outflow = { + onormal: bool; (* terminates normally by falling through *) + obreak: bool; (* terminates early by "break" *) + ocontinue: bool; (* terminates early by "continue" *) + oreturn: bool; (* terminates early by "return" *) + ogoto: StringSet.t (* terminates early by "goto" *) + (* to one of the labels in the set *) +} + +(* The l.u.b. of two out flows *) + +let join o1 o2 = + { onormal = o1.onormal || o2.onormal; + obreak = o1.obreak || o2.obreak; + ocontinue = o1.ocontinue || o2.ocontinue; + oreturn = o1.oreturn || o2.oreturn; + ogoto = StringSet.union o1.ogoto o2.ogoto } (* Some elementary flows *) -let normal : flow = fun i is -> if i then _Fallthrough else _None -let break : flow = fun i is -> if i then _Break else _None -let continue : flow = fun i is -> if i then _Continue else _None -let return : flow = fun i is -> if i then _Return else _None -let noflow : flow = fun i is -> _None +let normal : flow = fun i -> + { onormal = i.inormal; + obreak = false; ocontinue = false; oreturn = false; + ogoto = StringSet.empty } + +let break : flow = fun i -> + { obreak = i.inormal; + onormal = false; ocontinue = false; oreturn = false; + ogoto = StringSet.empty } + +let continue : flow = fun i -> + { ocontinue = i.inormal; + onormal = false; obreak = false; oreturn = false; + ogoto = StringSet.empty } + +let return : flow = fun i -> + { oreturn = i.inormal; + onormal = false; obreak = false; ocontinue = false; + ogoto = StringSet.empty } + +let goto lbl : flow = fun i -> + { onormal = false; obreak = false; ocontinue = false; oreturn = false; + ogoto = if i.inormal then StringSet.singleton lbl else StringSet.empty } + +let noflow : flow = fun i -> + { onormal = false; obreak = false; ocontinue = false; oreturn = false; + ogoto = StringSet.empty } (* Some flow transformers *) (* Sequential composition *) -let seq (s1: flow) (s2: flow) : flow = fun i is -> - let o1 = s1 i is in - let o2 = s2 (can _Fallthrough o1) is in - join (remove _Fallthrough o1) o2 +let seq (s1: flow) (s2: flow) : flow = fun i -> + let o1 = s1 i in + let o2 = s2 {i with inormal = o1.onormal} in + { onormal = o2.onormal; + obreak = o1.obreak || o2.obreak; + ocontinue = o1.ocontinue || o2.ocontinue; + oreturn = o1.oreturn || o2.oreturn; + ogoto = StringSet.union o1.ogoto o2.ogoto } (* Nondeterministic choice *) -let either (s1: flow) (s2: flow) : flow = fun i is -> - join (s1 i is) (s2 i is) +let either (s1: flow) (s2: flow) : flow = fun i -> + join (s1 i) (s2 i) (* If-then-else, with special cases for conditions that are always true or always false. *) @@ -84,45 +125,47 @@ let if_ env e (s1: flow) (s2: flow) : flow = (* Convert "continue" into "fallthrough". Typically applied to a loop body. *) -let catch_continue (s: flow) : flow = fun i is -> - let o = s i is in - if can _Continue o then add _Fallthrough (remove _Continue o) else o +let catch_continue (s: flow) : flow = fun i -> + let o = s i in + { o with onormal = o.onormal || o.ocontinue; ocontinue = false} (* Convert "continue" into "fallthrough". Typically applied to a loop. *) -let catch_break (s: flow) : flow = fun i is -> - let o = s i is in - if can _Break o then add _Fallthrough (remove _Break o) else o +let catch_break (s: flow) : flow = fun i -> + let o = s i in + { o with onormal = o.onormal || o.obreak; obreak = false} -(* For goto-labeled statements we assume they can always be entered by - a goto. *) +(* Statements labeled with a goto label *) -let label (s: flow) : flow = fun i is -> s true is +let label lbl (s: flow) : flow = fun i -> + s { i with inormal = i.inormal || StringSet.mem lbl i.igoto } (* For "case" and "default" labeled statements, we assume they can be entered normally as soon as the nearest enclosing "switch" can be entered normally. *) -let case (s: flow) : flow = fun i is -> s (i || is) is - -let switch (s: flow) : flow = fun i is -> s false i +let case (s: flow) : flow = fun i -> + s { i with inormal = i.inormal || i.iswitch } +let switch (s: flow) : flow = fun i -> + s { i with inormal = false; iswitch = true } + (* This is the flow for an infinite loop with body [s]. There is no fallthrough exit, but all other exits from [s] are preserved. *) -let loop (s: flow) : flow = fun i is -> - let o = s i is in - if (not i) && can _Fallthrough o then +let loop (s: flow) : flow = fun i -> + let o = s i in + if o.onormal && not i.inormal then (* Corner case: on the first iteration, [s] was not entered normally, but it exits by fallthrough. Then on the next iteration [s] is entered normally. So, we need to recompute the flow of [s] assuming it is entered normally. *) - s true is + s { i with inormal = true} else (* In all other cases, iterating [s] once more does not produce new exits that we did not compute on the first iteration. Just remove the fallthrough exit. *) - remove _Fallthrough o + { o with onormal = false } (* This is the main analysis function. Given a C statement [s] it returns a flow that overapproximates the behavior of [s]. *) @@ -165,12 +208,12 @@ let rec outcomes env s : flow = continue | Sswitch(e, s) -> catch_break (switch (outcomes env s)) - | Slabeled(Slabel _, s) -> - label (outcomes env s) + | Slabeled(Slabel lbl, s) -> + label lbl (outcomes env s) | Slabeled((Scase _ | Sdefault), s) -> case (outcomes env s) - | Sgoto _ -> - noflow + | Sgoto lbl -> + goto lbl | Sreturn opte -> return | Sblock sl -> @@ -191,7 +234,14 @@ and outcomes_block env sl = estimate if and how this function can return. *) let function_returns env body = - let o = outcomes env body true false in + (* Iterate [outcomes] until all gotos are accounted for *) + let rec fixpoint i = + let o = outcomes env body i in + if StringSet.subset o.ogoto i.igoto + then o + else fixpoint { i with igoto = StringSet.union i.igoto o.ogoto } in + let o = + fixpoint { inormal = true; iswitch = false; igoto = StringSet.empty } in (* First boolean is: function can return Second boolean is: function can return by fall-through *) - (can _Fallthrough o || can _Return o, can _Fallthrough o) + (o.onormal || o.oreturn, o.onormal) -- cgit From 6805bcf7b3ddd78bcbe0e25618ccaf0429ff78ec Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 7 Feb 2017 16:53:47 +0100 Subject: Cflow: analysis of "switch" was too imprecise Plus: updated comments. --- cparser/Cflow.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'cparser') diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml index 7de5cf59..f5408c15 100644 --- a/cparser/Cflow.ml +++ b/cparser/Cflow.ml @@ -14,7 +14,8 @@ (* *********************************************************************) (* A simple control flow analysis for C statements. - Main purpose: emit warnings for _Noreturn functions. *) + Main purpose: emit warnings for non-void functions that fall through, + and for _Noreturn functions that can return. *) open C open Cutil @@ -148,7 +149,7 @@ let case (s: flow) : flow = fun i -> s { i with inormal = i.inormal || i.iswitch } let switch (s: flow) : flow = fun i -> - s { i with inormal = false; iswitch = true } + s { i with inormal = false; iswitch = i.inormal } (* This is the flow for an infinite loop with body [s]. There is no fallthrough exit, but all other exits from [s] are preserved. *) -- cgit