package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file nonterm_run.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Cil_datatype

module Self = Plugin.Register
    (struct
      let name = "nonterm"
      let shortname = "nonterm"
      let help =
        "Warns when definitively non-terminating functions/loops are \
         detected (e.g. reachable functions with unreachable returns)."
    end)

module Enabled =
  Self.WithOutput
    (struct
      let option_name = "-nonterm"
      let help = "when on (off by default), \
                  warns about non-terminating functions/loops"
      let output_by_default = false
    end)

let () = Parameter_customize.argument_may_be_fundecl ()
module Ignore =
  Self.Filled_string_set
    (struct
      let option_name = "-nonterm-ignore"
      let arg_name = "f1,..,fn"
      let help = "ignore functions f1,..,fn and direct calls to them. \
                  Functions prefixed with '-' are removed from the ignore \
                  list. Calls via function pointers are never ignored. \
                  By default, the following functions are ignored: \
                  abort, exit"
      let default = Datatype.String.Set.of_list ["abort"; "exit"]
    end)

module DeadCode =
  Self.False
    (struct
      let option_name = "-nonterm-dead-code"
      let help = "warns about syntactically unreachable code. \
                  Note that this may emit a substantial amount of warnings."
    end)

let pretty_stmt_kind fmt stmt =
  match stmt.skind with
  | Break _ ->
    let implicit =
      try
        let kf = Kernel_function.find_englobing_kf stmt in
        let loop = Kernel_function.find_enclosing_loop kf stmt in
        (* heuristic: if both statements have the same location, then
           the break was implicitly generated *)
        Location.equal (Stmt.loc stmt) (Stmt.loc loop)
      with Not_found -> false
    in
    Format.fprintf fmt "%sbreak" (if implicit then "implicit " else "")
  | Return _ ->
    (* heuristic: if the return statement has no predecessors, then
       it is implicitly generated (and dead code) *)
    let implicit = stmt.preds = [] in
    Format.fprintf fmt "%sreturn" (if implicit then "implicit " else "")
  | Loop _ -> Format.fprintf fmt "loop"
  | Switch _ -> Format.fprintf fmt "switch"
  | Instr (Call _) -> Format.fprintf fmt "function call"
  | Instr (Local_init(_,ConsInit _,_)) ->
    Format.fprintf fmt "function call (initializer)"
  | _ -> Format.fprintf fmt "statement"

let pp_numbered_stacks fmt callstacks =
  if List.length callstacks < 2 then
    Format.fprintf fmt "stack: %a"
      (Pretty_utils.pp_list ~sep:": " Eva.Callstack.pretty) callstacks
  else
    (* number callstacks *)
    let numbered_callstacks =
      List.mapi (fun i cs -> (i+1, cs)) callstacks
    in
    Format.fprintf fmt "%a"
      (Pretty_utils.pp_list ~sep:"@\n"
         (Pretty_utils.pp_pair ~pre:"stack " ~sep:": "
            Format.pp_print_int Eva.Callstack.pretty))
      numbered_callstacks

let wkey_stmt = Self.register_warn_category "stmt"

let warn_nonterminating_statement stmt callstacks =
  Self.warning ~wkey:wkey_stmt ~source:(fst (Stmt.loc stmt))
    "non-terminating %a@\n%a"
    pretty_stmt_kind stmt pp_numbered_stacks callstacks

let wkey_dead = Self.register_warn_category "dead-code"

let warn_dead_code stmt =
  Self.warning ~wkey:wkey_dead ~source:(fst (Stmt.loc stmt))
    "%a is syntactically unreachable" pretty_stmt_kind stmt

class dead_cc_collector kf = object
  inherit Visitor.frama_c_inplace

  val reachable =
    let first = Kernel_function.find_first_stmt kf in
    let initial_reachable = Stmt.Hptset.add first (Stmts_graph.reachable_stmts kf first) in
    ref initial_reachable

  val dead_ccs = ref []
  val cur_cc = ref []

  method get =
    (* the last cc may not have been finalized *)
    if !cur_cc <> [] then begin
      dead_ccs := !cur_cc :: !dead_ccs;
      cur_cc := []
    end;
    !dead_ccs

  method! vstmt stmt =
    let new_succs cc s = List.filter (fun s' -> not (List.mem s' cc)) s.succs in
    if not (Stmt.Hptset.mem stmt !reachable) then begin
      (* add [stmt] and its successors to a connected component; if there is
         already one with [stmt], remain there, otherwise create a new one *)
      begin
        if !cur_cc = [] then begin
          let cc = stmt :: new_succs [] stmt in
          cur_cc := cc
        end else
        if List.mem stmt !cur_cc then begin
          (* part of same cc: update cc in previous list *)
          cur_cc := !cur_cc @ new_succs !cur_cc stmt;
        end else (* new cc *) begin
          dead_ccs := !cur_cc :: !dead_ccs;
          cur_cc := stmt :: new_succs [] stmt;
        end
      end;
      reachable := Stmt.Hptset.add stmt !reachable
    end;
    Cil.DoChildren
end

let wkey_unreachable = Self.register_warn_category "unreachable"

let warn_unreachable_statement stmt =
  Self.warning ~wkey:wkey_unreachable ~source:(fst (Stmt.loc stmt))
    "unreachable %a" pretty_stmt_kind stmt

class unreachable_stmt_visitor kf to_ignore = object
  inherit Visitor.frama_c_inplace

  val semantically_unreachable : stmt list ref = ref []

  method get : stmt list = !semantically_unreachable

  val syntactically_reachable =
    let first = Kernel_function.find_first_stmt kf in
    let initial_reachable = Stmt.Hptset.add first (Stmts_graph.reachable_stmts kf first) in
    initial_reachable

  val semantically_considered = ref to_ignore

  method! vstmt stmt =
    if Stmt.Hptset.mem stmt syntactically_reachable &&
       not (Eva.Results.is_reachable stmt) &&
       not (Stmt.Hptset.mem stmt !semantically_considered)
    then begin
      (* add node and its reachable successors to the considered statements *)
      let cc = Stmt.Hptset.add stmt (Stmts_graph.reachable_stmts kf stmt) in
      semantically_considered :=
        Stmt.Hptset.union !semantically_considered cc;
      semantically_unreachable := stmt :: !semantically_unreachable
    end;
    Cil.DoChildren
end

(* Unreachable returns only need to be checked if:
   1. SyntacticallyUnreachable is disabled (otherwise it already checks them);
   2. No warnings were emitted for the function (otherwise it may be redundant). *)
let check_unreachable_returns kf =
  try
    let ret_stmt = Kernel_function.find_return kf in
    if not (Eva.Results.is_reachable ret_stmt) then
      warn_unreachable_statement ret_stmt
  with
  | Kernel_function.No_Statement -> (* should never happen *)
    Self.error "function %a has no return statement, skipping"
      Kernel_function.pretty kf

(* Checks [kf] for unreachable statements (ignoring those in [to_ignore])
   and emits warnings. [warned_kfs] indicates functions which already had
   warnings emitted, to minimize the amount of redundant ones. *)
let check_unreachable_statements kf ~to_ignore ~dead_code ~warned_kfs =
  match Eva.Analysis.status kf with
  | Unreachable | Analyzed NoResults -> ()
  | SpecUsed | Builtin _ ->
    (* TODO: consider as non-terminating if spec has
       \terminates(false) or \ensures(false) *)
    Self.debug "not analyzing function %a@ \
                (using specification instead of definition),@ \
                considered as always terminating"
      Kernel_function.pretty kf
  | Analyzed _ ->
    try
      let vis = new unreachable_stmt_visitor kf to_ignore in
      ignore (Visitor.visitFramacKf (vis :> Visitor.frama_c_visitor) kf);
      if dead_code then begin
        (* compute syntactically unreachable statements *)
        let vis = new dead_cc_collector kf in
        ignore (Visitor.visitFramacKf (vis :> Visitor.frama_c_visitor) kf);
        let cc_heads = List.map List.hd vis#get in
        Stmt.Hptset.iter (fun h -> warn_dead_code h) (Stmt.Hptset.of_list cc_heads)
      end
      else if not (Kernel_function.Set.mem kf warned_kfs) then
        check_unreachable_returns kf
    with
    | Kernel_function.No_Statement -> (* should never happen *)
      Self.error "function %a has no return statement, skipping"
        Kernel_function.pretty kf

(* To avoid redundant warnings, calls to possibly non-terminating functions
   are ignored if:
   1. the function is in the list of functions to be ignored;
   2. or Eva results are available for the function.
   In case 2, the call is ignored because non-terminating statements inside
   it will already be reported. *)
let ignore_kf name =
  try
    let kf = Globals.Functions.find_by_name name in
    Ignore.mem name || Eva.Results.are_available kf
  with Not_found -> false

(* simple statement collector: accumulates a list of all
   statements, except calls to functions in [to_ignore]. *)
class stmt_collector = object
  inherit Visitor.frama_c_inplace
  val instr_stmts = ref []
  method! vstmt stmt =
    begin
      match stmt.skind with
      | (Instr (Call (_, {enode = Lval (Var vi, _)}, _, _))
        | Instr (Local_init (_, ConsInit(vi,_,_), _))) when
          (ignore_kf vi.vname) -> ()
      | _ -> instr_stmts := stmt :: !instr_stmts
    end;
    Cil.DoChildren
  method get_instr_stmts = List.rev !instr_stmts
end

(* collects the list of non-terminating instructions *)
let collect_nonterminating_statements fd nonterm_stacks =
  let vis = new stmt_collector in
  ignore (Visitor.visitFramacFunction (vis :> Visitor.frama_c_visitor) fd);
  let new_nonterm_stmts = ref Stmt.Hptset.empty in
  let add_stack stmt cs =
    new_nonterm_stmts := Stmt.Hptset.add stmt !new_nonterm_stmts;
    let prev_stack_list =
      try
        Hashtbl.find nonterm_stacks stmt
      with Not_found -> []
    in
    Hashtbl.replace nonterm_stacks stmt (cs :: prev_stack_list)
  in
  List.iter (fun stmt ->
      match stmt.skind with
      | Block _ -> (* do not compute; already done for the block stmts *) ()
      | _ ->
        let source = fst (Stmt.loc stmt) in
        Self.debug ~source "processing stmt:@ %a" Printer.pp_stmt stmt;
        let process_callstack cs =
          if Eva.Results.(after stmt |> in_callstack cs |> is_empty) then
            add_stack stmt cs
          else if match stmt.skind with Loop _ -> true | _ -> false then begin
            (* special treatment for loops: even if their after state
                is reachable, we must check that at least one outgoing
                edge is reachable *)
            let out_edges = Stmts_graph.get_all_stmt_out_edges stmt in
            let all_out_edges_unreachable =
              List.for_all (fun (_, out_stmt) ->
                  Eva.Results.(before out_stmt |> in_callstack cs |> is_empty)
                ) out_edges
            in
            if all_out_edges_unreachable then add_stack stmt cs
          end
        in
        List.iter process_callstack Eva.Results.(before stmt |> callstacks)
    ) vis#get_instr_stmts;
  !new_nonterm_stmts

let run () =
  if not (Ast.is_computed ()) then
    Self.abort "nonterm requires a computed AST";
  if not (Eva.Analysis.is_computed ()) then
    Self.abort "nonterm requires a computed value analysis";
  Self.debug "Starting analysis...";
  let file = Ast.get () in
  let globals = file.globals in
  let nonterm_stacks = Hashtbl.create 13 in
  List.iter (fun glob ->
      match glob with
      | GFun (fd, _loc) ->
        let fname = fd.svar.vorig_name in
        if Ignore.mem fname then
          Self.debug "ignoring function: %s" fname
        else begin
          Self.debug "considering function: %s" fname;
          let new_nonterm_stmts =
            collect_nonterminating_statements fd nonterm_stacks
          in
          let warned_kfs =
            Stmt.Hptset.fold (fun stmt acc ->
                let cs = Hashtbl.find nonterm_stacks stmt in
                let cs = List.sort Eva.Callstack.compare_lex cs in
                warn_nonterminating_statement stmt cs;
                Kernel_function.Set.add (Kernel_function.find_englobing_kf stmt) acc
              ) new_nonterm_stmts Kernel_function.Set.empty
          in
          let kf = Globals.Functions.get fd.svar in
          check_unreachable_statements kf ~to_ignore:new_nonterm_stmts ~warned_kfs
            ~dead_code:(DeadCode.get());
        end
      | _ -> ()
    ) globals;
  Self.feedback ~level:2 "Analysis done."
;;

let run_once, _ = State_builder.apply_once "Nonterm.run" [Eva.Analysis.self] run

let main () =
  if Enabled.get () then run_once ()

let () =
  Boot.Main.extend main
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct