diff options
| -rw-r--r-- | cparser/Cflow.ml | 146 |
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) |