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.

5 files changed, 237 insertions, 32 deletions

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 =