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 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