Merge pull request #162 from AbsInt/return-analysis-2

Improved warnings related to function returns

5 files changed, 290 insertions, 32 deletions

diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml
new file mode 100644
index 00000000..f5408c15
--- /dev/null
+++ b/cparser/Cflow.ml
@@ -0,0 +1,248 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 non-void functions that fall through,
+   and for _Noreturn functions that can return. *)
+
+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 = 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 ->
+  { 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 ->
+  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 ->
+  join (s1 i) (s2 i)
+
+(* 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 ->
+  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 ->
+  let o = s i in
+  { o with onormal = o.onormal || o.obreak; obreak = false}
+
+(* Statements labeled with a goto label *)
+
+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 ->
+  s { i with inormal = i.inormal || i.iswitch }
+
+let switch (s: flow) : flow = fun i ->
+  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. *)
+
+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 { 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. *)
+     { 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]. *)
+
+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 lbl, s) ->
+      label lbl (outcomes env s)
+  | Slabeled((Scase _ | Sdefault), s) ->
+      case (outcomes env s)
+  | Sgoto lbl ->
+      goto lbl
+  | 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 =
+  (* 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 *)
+  (o.onormal || o.oreturn, o.onormal)
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 2334966c..18088be7 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -1179,24 +1179,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 9d053717..a1b9cd26 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 ea85ad04..eb9ff560 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 =