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.

1 files changed, 98 insertions, 48 deletions

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)