package frama-c

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

Source file pretty_source.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
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
(**************************************************************************)
(*                                                                        *)
(*  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 Gtk_helper
open Printer_tag

type localizable = Printer_tag.localizable
let kf_of_localizable = Printer_tag.kf_of_localizable
let ki_of_localizable = Printer_tag.ki_of_localizable
let varinfo_of_localizable = Printer_tag.varinfo_of_localizable

module Locs:sig
  type state
  val add: state -> int * int -> localizable -> unit
  val iter : state -> (int * int -> localizable -> unit) -> unit
  val create : unit -> state
  val clear : state -> unit
  val find : state -> int -> (int * int) * localizable
  val hilite : state -> unit
  val set_hilite : state -> (unit -> unit) -> unit
  val add_finalizer: state -> (unit -> unit) -> unit
  val size : state -> int
  val stmt_start: state -> stmt -> int
end
=
struct
  type state = { table : (int*int,localizable) Hashtbl.t;
                 mutable hiliter : unit -> unit;
                 mutable finalizers: (unit -> unit) list;
                 stmt_start: int Datatype.Int.Hashtbl.t
               (* mapping from sid to their offset in the buffer *);
               }

  let create () =
    {table = Hashtbl.create 97;
     hiliter = (fun () -> ());
     finalizers = [];
     stmt_start = Datatype.Int.Hashtbl.create 16;
    }

  let hilite state = state.hiliter ()

  let set_hilite state f =
    state.hiliter <- f

  let add_finalizer state f =
    state.finalizers <- f :: state.finalizers

  let finalize state =
    List.iter (fun f -> f ()) (List.rev state.finalizers)

  let clear state =
    finalize state;
    state.finalizers <- [];
    state.hiliter <- (fun () -> ());
    Hashtbl.clear state.table;
    Datatype.Int.Hashtbl.clear state.stmt_start;
  ;;

  (* Add a location range only if it is not already there.
     Visually only the innermost pretty printed entity is kept.
     For example: 'loop assigns x;' will be indexed as an assigns
     and not as a code annotation.
  *)
  let add state range = function
    | Printer_tag.PStmtStart(_,st) ->
      Datatype.Int.Hashtbl.add state.stmt_start st.sid (fst range)
    | localizable ->
      if not (Hashtbl.mem state.table range) then
        Hashtbl.add state.table range localizable

  let stmt_start state s =
    Datatype.Int.Hashtbl.find state.stmt_start s.sid

  let find state p =
    let best = ref None in
    let update ((b,e) as loc) sid =
      if b <= p && p <= e then
        match !best with
        | None -> best := Some (loc, sid)
        | Some ((b',e'),_) -> if e-b < e'-b' then best := Some (loc, sid)
    in
    Hashtbl.iter update state.table ;
    match !best with None -> raise Not_found | Some (loc,sid) -> loc, sid

  let iter state f =
    Hashtbl.iter f state.table

  let size state = Hashtbl.length state.table

end

let hilite state = Locs.hilite state
let stmt_start state = Locs.stmt_start state

module LocsArray:sig
  type t
  val create: Locs.state -> t
  val length : t -> int
  val get : t -> int -> (int * int) * localizable
  val find_next : t -> int -> (localizable -> bool) -> int
end
=
struct
  (* computes an ordered array containing all the elements of a Locs.state,
     the order (<) being such that loc1 < loc2 if either loc1 starts
     before loc2, or loc1 and loc2 start at the same position but
     loc1 spawns further than loc2.
  *)

  type t = ((int*int) * localizable option) array

  let create state =
    let arr = Array.make (Locs.size state) ((0,0), None) in
    let index = ref 0 in
    Locs.iter
      state
      (fun (pb,pe) v ->
         Array.set arr !index ((pb,pe), Some v) ;
         incr index
      )
    ;
    Array.sort
      (fun ((pb1,pe1),_) ((pb2,pe2),_) ->
         if (pb1 = pb2) then
           if (pe1 = pe2) then 0
           else
             (* most englobing comes first *)
             Stdlib.compare pe2 pe1
         else Stdlib.compare pb1 pb2
      ) arr
    ;
    arr

  let length arr = Array.length arr

  (* get loc at index i;
     raises Not_found if none exists *)
  let get arr i =
    if i >= Array.length arr then raise Not_found
    else
      match Array.get arr i with
      | ((_,_),None) -> raise Not_found
      | ((pb,pe),Some v) -> ((pb,pe),v)

  (* find the next loc in array starting at index i
     which satisfies the predicate;
     raises Not_found if none exists *)
  let find_next arr i predicate =
    let rec fnext i =
      let ((pb',_pe'),v) = get arr i in
      if predicate v then pb'
      else fnext (i+1)
    in fnext i

end

(* Set of callsite statements where preconditions must be unfolded. *)
let unfold_preconds = Cil_datatype.Stmt.Hashtbl.create 8

(* Fold or unfold the preconditions at callsite [stmt]. *)
let fold_preconds_at_callsite stmt =
  if Cil_datatype.Stmt.Hashtbl.mem unfold_preconds stmt
  then Cil_datatype.Stmt.Hashtbl.remove unfold_preconds stmt
  else Cil_datatype.Stmt.Hashtbl.replace unfold_preconds stmt ()

let are_preconds_unfolded stmt =
  Cil_datatype.Stmt.Hashtbl.mem unfold_preconds stmt

module Tag =
struct

  let hashtbl = Hashtbl.create 0
  let current = ref 0
  let charcode = function
    | PStmt _ -> 's'
    | PStmtStart _ -> 'k'
    | PLval _ -> 'l'
    | PExp _ -> 'e'
    | PTermLval _ -> 't'
    | PVDecl _ -> 'd'
    | PGlobal _ -> 'g'
    | PIP _ -> 'i'
    | PType _ -> 'y'

  let tag loc =
    incr current ;
    let tag = Printf.sprintf "guitag:%c%x" (charcode loc) !current in
    Hashtbl.replace hashtbl tag loc ; tag

  let find = Hashtbl.find hashtbl

end

module Printer = Printer_tag.Make(Tag)

exception Found of int*int

(* This function identifies two distinct localizable that happen to have
   the same location in the source code, typically because one of them
   is not printed. Feel free to add other heuristics if needed. *)
let equal_or_same_loc loc1 loc2 =
  let open Property in
  Localizable.equal loc1 loc2 ||
  match loc1, loc2 with
  | PIP (IPReachable {ir_kinstr=Kstmt s}), PStmt (_, s')
  | PStmt (_, s'), PIP (IPReachable {ir_kinstr=Kstmt s})
  | PIP (IPPropertyInstance {ii_stmt=s}), PStmt (_, s')
  | PStmt (_, s'), PIP (IPPropertyInstance {ii_stmt=s})
    when
      Cil_datatype.Stmt.equal s s' -> true
  | PIP (IPReachable {ir_kf=Some kf; ir_kinstr=Kglobal}),
    (PVDecl (_, _, vi) | PGlobal (GFun ({ svar = vi }, _)))
  | (PVDecl (_, _, vi) | PGlobal (GFun ({ svar = vi }, _))),
    PIP (IPReachable {ir_kf=Some kf;ir_kinstr=Kglobal})
    when Kernel_function.get_vi kf = vi
    -> true
  | _ -> false

let locate_localizable state loc =
  try
    Locs.iter
      state
      (fun (b,e) v -> if equal_or_same_loc v loc then raise (Found(b,e)));
    None
  with Found (b,e) -> Some (b,e)

let localizable_from_locs state ~file ~line =
  let r = ref [] in
  Locs.iter
    state
    (fun _ v ->
       let loc,_ = loc_of_localizable v in
       if line = loc.Filepath.pos_lnum && loc.Filepath.pos_path = file then
         r := v::!r);
  !r

let buffer_formatter state source =
  let starts = Stack.create () in
  let emit_open_tag s =
    let s = Extlib.format_string_of_stag s in
    (* Ignore tags that are not ours *)
    if String.starts_with ~prefix:"guitag:" s then
      Stack.push (source#end_iter#offset, Tag.find s) starts ;
    ""
  in
  let emit_close_tag s =
    let s = Extlib.format_string_of_stag s in
    (try
       if String.starts_with ~prefix:"guitag:" s then
         let (p,sid) = Stack.pop starts in
         Locs.add state (p, source#end_iter#offset) sid
     with Stack.Empty -> (* This should probably be a hard error *)
       Gui_parameters.error "empty stack in emit_tag");
    ""
  in
  let gtk_fmt = Gtk_helper.make_formatter source in
  Format.pp_set_tags gtk_fmt true;
  Format.pp_set_print_tags gtk_fmt false;
  Format.pp_set_mark_tags gtk_fmt true;
  let open Format in
  pp_set_formatter_stag_functions
    gtk_fmt {(pp_get_formatter_stag_functions gtk_fmt ())
             with
              mark_open_stag = emit_open_tag;
              mark_close_stag = emit_close_tag;};

  Format.pp_set_margin gtk_fmt 79;
  gtk_fmt

let display_source globals
    (source:GSourceView.source_buffer) ~(host:Gtk_helper.host)
    ~highlighter ~selector state =
  Locs.clear state;
  host#protect
    ~cancelable:false
    (fun () ->
       source#set_text "";
       source#remove_source_marks
         ~start:source#start_iter ~stop:source#end_iter ();
       let hiliter () =
         let event_tag = Gtk_helper.make_tag source ~name:"events" [] in
         Gtk_helper.cleanup_all_tags source;
         let locs_array = LocsArray.create state in
         let index_max =  LocsArray.length locs_array in
         let index = ref 0 in
         while(!index < index_max) do (
           try
             let ((pb,pe),v) = LocsArray.get locs_array !index in
             match v with
             | PStmt (_,ki) ->
               (try
                  let pb,pe = match ki with
                    | {skind = Instr _ | Return _ | Goto _
                               | Break _ | Continue _ | Throw _ } -> pb,pe
                    | {skind = If _ | Loop _
                               | Switch _ } ->
                      (* These statements contain other statements.
                         We highlight only until the start of the first
                         included statement. *)
                      pb,
                      (try LocsArray.find_next locs_array (!index+1)
                             (fun p -> match p with
                                | PStmt _ -> true
                                | _ -> false (* Do not stop on expressions*))
                       with Not_found -> pb+1)
                    | {skind = Block _ | TryExcept _ | TryFinally _
                               | UnspecifiedSequence _ | TryCatch _ } ->
                      pb,
                      (try LocsArray.find_next locs_array (!index+1) (fun _ -> true)
                       with Not_found -> pb+1)
                  in
                  highlighter v ~start:pb ~stop:pe
                with Not_found -> ())
             | PStmtStart _
             | PTermLval _ | PLval _ | PVDecl _ | PGlobal _
             | PIP _ | PExp _ | PType _ ->
               highlighter v  ~start:pb ~stop:pe
           with Not_found -> () ) ;
           incr index
         done;
         (* React to events on the text *)
         source#apply_tag ~start:source#start_iter ~stop:source#end_iter event_tag;
       in
       Locs.set_hilite state hiliter;
       let gtk_fmt = buffer_formatter state (source:>GText.buffer) in
       let display_global g =
         Printer.with_unfold_precond
           are_preconds_unfolded
           Printer.pp_global gtk_fmt g ;
         Format.pp_print_flush gtk_fmt ()
       in
       let counter = ref 0 in
       begin try
           List.iter
             (fun g ->
                incr counter;
                if !counter > 20 then raise Exit;
                display_global g)
             globals;
         with Exit ->
           Format.fprintf
             gtk_fmt
             "@./* Cannot display more than %d globals at a time. Skipping end \
              of file.@   \
              Use the filetree in 'Flat mode' to navigate the remainder. */@."
             (!counter-1);
           (*let ca = source#create_child_anchor source#end_iter in
             source_view#add_child_at_anchor (GButton.button
             ~text:"See 10 more globals"
             ~callback:(fun _ -> call_cc next_10)
             ()) ca *)
       end;
       source#place_cursor ~where:source#start_iter;
       let last_shown_area =
         Gtk_helper.make_tag source ~name:"last_shown_area"
           [`BACKGROUND "light green"]
       in
       let event_tag = Gtk_helper.make_tag source ~name:"events" [] in
       let id = event_tag#connect#event ~callback:
           (fun ~origin:_ ev it ->
              if !Gtk_helper.gui_unlocked then
                if GdkEvent.get_type ev = `BUTTON_PRESS then begin
                  let coords = GtkText.Iter.get_offset it in
                  try
                    let ((pb,pe), selected) = Locs.find state coords in
                    (* Highlight the pointed term *)
                    source#remove_tag
                      ~start:source#start_iter
                      ~stop:source#end_iter
                      last_shown_area;
                    apply_tag source last_shown_area pb pe;
                    let event_button = GdkEvent.Button.cast ev in
                    let button = GdkEvent.Button.button event_button in
                    host#protect ~cancelable:false
                      (fun () -> selector ~button selected);
                  with Not_found -> () (* no statement at this offset *)
                end;
              false)
       in
       Locs.add_finalizer state
         (fun () -> GtkSignal.disconnect event_tag#as_tag id);
    )

(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)
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