Source file metrics_cilast.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
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
module Kernel_file = File
open Cil_datatype
open Cil_types
open Metrics_base
;;
type cilast_metrics = {
fundecl_calls: int Metrics_base.VInfoMap.t;
funspec_calls: int Metrics_base.VInfoMap.t;
fundef_calls: int Metrics_base.VInfoMap.t;
extern_global_vars: Metrics_base.VInfoSet.t;
basic_global_metrics: BasicMetrics.t
}
(** Syntactic metrics
=================
The goal is to collect various (syntactic) information about the source code
(slocs, assignments, loops, ...).
From those one can compute McCabe's cyclomatic complexity.
*)
class type sloc_visitor = object
inherit Visitor.generic_frama_c_visitor
method fundecl_calls: int Metrics_base.VInfoMap.t
method funspec_calls: int Metrics_base.VInfoMap.t
method fundef_calls: int Metrics_base.VInfoMap.t
method extern_global_vars: Metrics_base.VInfoSet.t
method get_global_metrics: BasicMetrics.t
method pp_file_metrics: Format.formatter -> Datatype.Filepath.t -> unit
method pp_detailed_text_metrics: Format.formatter -> unit
(** Print results of all file and functions to the given formatter as text *)
method print_stats: Format.formatter -> unit
(** Print computed metrics to a formatter *)
method get_metrics_map:
(BasicMetrics.t OptionKf.Map.t) Datatype.Filepath.Map.t
(** Compute and return per-function metrics *)
end
open BasicMetrics ;;
class slocVisitor ~libc : sloc_visitor = object(self)
inherit Visitor.frama_c_inplace
val global_metrics = ref BasicMetrics.empty_metrics
val local_metrics = ref BasicMetrics.empty_metrics
val mutable metrics_map:
(BasicMetrics.t OptionKf.Map.t) Datatype.Filepath.Map.t =
Datatype.Filepath.Map.empty
val mutable seen_vars = Varinfo.Set.empty;
val fundecl_calls: int VInfoMap.t ref = ref VInfoMap.empty;
val funspec_calls: int VInfoMap.t ref = ref VInfoMap.empty;
val fundef_calls: int VInfoMap.t ref = ref VInfoMap.empty;
val extern_global_vars = ref VInfoSet.empty
method fundecl_calls = !fundecl_calls
method funspec_calls = !funspec_calls
method fundef_calls = !fundef_calls
method extern_global_vars = !extern_global_vars
method get_global_metrics = !global_metrics
method get_metrics_map = metrics_map
method private update_metrics_map filename kfmap =
metrics_map <- Datatype.Filepath.Map.add filename kfmap metrics_map
method private incr_both_metrics f =
apply_then_set f global_metrics;
apply_then_set f local_metrics
method private add_map map vinfo value =
map := VInfoMap.add vinfo value !map
method private stats_of_filename filename =
try Datatype.Filepath.Map.find filename metrics_map
with
| Not_found ->
Metrics_parameters.fatal "Metrics for file %a not_found@."
Datatype.Filepath.pretty filename
method pp_file_metrics fmt filename =
Format.fprintf fmt "@[<v 0>%a@]"
(fun fmt filename ->
let fun_tbl = self#stats_of_filename filename in
OptionKf.Map.iter (fun _fun_name fmetrics ->
Format.fprintf fmt "@ %a" pp_base_metrics fmetrics)
fun_tbl;
) filename
method pp_detailed_text_metrics fmt =
Datatype.Filepath.Map.iter
(fun filename _func_tbl ->
Format.fprintf fmt "%a" self#pp_file_metrics filename) metrics_map
method print_stats fmt =
Format.pp_set_formatter_stag_functions fmt Metrics_base.html_stag_functions;
Format.pp_set_tags fmt true;
let pr_hdr fmt hdr_name =
Format.fprintf fmt "@{<th>%s@}" hdr_name in
Datatype.Filepath.Map.iter
(fun filename func_tbl ->
Metrics_parameters.result ~level:2 "%a" self#pp_file_metrics filename;
if func_tbl <> OptionKf.Map.empty then
begin
Format.fprintf fmt
"@[<v 0>@{<h3>%a@}<br/>@ \
@{<table>\
@[<v 2>@ \
@[<v 2>@{<tbody>@ \
@{<tr>@[<v 2>@ \
%a@ %a@ %a@ %a@ %a@ %a@ %a@ %a@ %a@ @]@}@ \
%a@ \
@}@]@]@ @} \
@]@ "
Datatype.Filepath.pretty filename
pr_hdr "Function" pr_hdr "#If stmts" pr_hdr "#Assignments"
pr_hdr "#Loops" pr_hdr "#Calls" pr_hdr "#Gotos"
pr_hdr "#Pointer dereferencing" pr_hdr "#Exits"
pr_hdr "Cyclomatic value"
(fun fmt fun_tbl ->
OptionKf.Map.iter
(fun _fname fmetrics ->
Format.fprintf fmt "%a"
pp_base_metrics_as_html_row fmetrics;
) fun_tbl
) func_tbl;
end
else
Metrics_parameters.warning
"Filename <%a> has no functions@."
Datatype.Filepath.pretty filename)
metrics_map
method private record_and_clear_function_metrics metrics =
let filename = metrics.cfile_name in
let funcname = metrics.cfunc in
local_metrics := BasicMetrics.set_cyclo !local_metrics
(BasicMetrics.compute_cyclo !local_metrics);
global_metrics := BasicMetrics.set_cyclo !global_metrics
(!global_metrics.ccyclo + !local_metrics.ccyclo);
(try
let fun_tbl = Datatype.Filepath.Map.find filename metrics_map in
self#update_metrics_map filename
(OptionKf.Map.add funcname !local_metrics fun_tbl);
with
| Not_found ->
let new_kfmap =
OptionKf.Map.add funcname !local_metrics
OptionKf.Map.empty
in self#update_metrics_map filename new_kfmap;
);
local_metrics := empty_metrics;
method! vvdec vi =
if not (Varinfo.Set.mem vi seen_vars) then (
if Cil.isFunctionType vi.vtype then (
if consider_function ~libc vi then begin
global_metrics := incr_funcs !global_metrics;
self#update_call_maps vi 0;
end
) else (
if vi.vglob && not vi.vtemp &&
Metrics_base.consider_variable ~libc vi
then (
global_metrics:= incr_glob_vars !global_metrics;
if vi.vstorage = Extern then
extern_global_vars := VInfoSet.add vi !extern_global_vars
)
);
seen_vars <- Varinfo.Set.add vi seen_vars;
);
Cil.SkipChildren
method! vfunc fdec =
if consider_function ~libc fdec.svar then
begin
local_metrics :=
{!local_metrics with
cfile_name = file_of_fundef fdec;
cfunc = Some (Globals.Functions.get fdec.svar);
cfuncs = 1; };
let fvinfo = fdec.svar in
(if not (VInfoMap.mem fvinfo !fundef_calls) then
self#add_map fundef_calls fvinfo 0);
Cil.ChangeDoChildrenPost
(fdec,
fun _ ->
begin
if !local_metrics <> empty_metrics
then self#record_and_clear_function_metrics !local_metrics;
fdec;
end
);
end
else Cil.SkipChildren
method! vlval (host, _) =
begin
match host with
| Mem _ -> self#incr_both_metrics incr_ptrs;
| _ -> ()
end;
Cil.DoChildren
method! vstmt s =
self#incr_both_metrics incr_slocs;
let do_children =
match s.skind with
| If _ ->
self#incr_both_metrics incr_ifs;
self#incr_both_metrics incr_dpoints;
true
| Loop _ -> self#incr_both_metrics incr_loops; true
| Goto _ -> self#incr_both_metrics incr_gotos; true
| Return _ -> self#incr_both_metrics incr_exits; true
| Switch (_, _, _slist, _) -> true
| TryFinally _
| TryExcept _ -> self#incr_both_metrics incr_dpoints; true
| UnspecifiedSequence l ->
List.iter
(fun (s,_,_,_,_) ->
ignore
(Visitor.visitFramacStmt (self:>Visitor.frama_c_visitor) s))
l;
false
| _ -> true
in
let rec has_case_label labels =
match labels with
| (Case _) :: _->
self#incr_both_metrics incr_dpoints;
| _ :: labels -> has_case_label labels
| [] -> ()
in has_case_label s.labels;
if do_children then Cil.DoChildren else Cil.SkipChildren
method! vexpr e =
begin
match e.enode with
| BinOp ((LAnd | LOr), _, _, _) ->
self#incr_both_metrics incr_dpoints;
| _ -> ()
end;
Cil.DoChildren
method private image (glob:global) =
match glob with
| GVar (v, _, _) -> v.vname ^ " (GVar) "
| GVarDecl (v, _) -> v.vname ^ " (GVarDecl) "
| GFunDecl (_, v, _) -> v.vname ^ " (GFunDecl) "
| GFun (fdec, _) -> fdec.svar.vname ^ " (GFun) "
| GType (ty, _) -> ty.tname
| GCompTag (ci, _) | GCompTagDecl (ci, _) -> ci.cname
| GEnumTagDecl (ei, _) | GEnumTag (ei, _) -> ei.ename
| GAsm (_, _) | GPragma _ | GText _ -> ""
| GAnnot (an,_) ->
begin
match an with
| Dfun_or_pred (li, _) -> li.l_var_info.lv_name
| Dvolatile (_, _, _, _, _) -> " (Volatile) "
| Daxiomatic (s, _, _, _) -> s
| Dtype (lti, _) -> lti.lt_name
| Dlemma (ln, _, _, _, _, _) -> ln
| Dinvariant (toto, _) -> toto.l_var_info.lv_name
| Dtype_annot (ta, _) -> ta.l_var_info.lv_name
| Dmodel_annot (mi, _) -> mi.mi_name
| Dextended ({ext_name}, _, _) -> " (Extension " ^ ext_name ^ ")"
end
method private images (globs:global list) =
let les_images = List.map self#image globs in
String.concat "," les_images
method private update_call_maps vinfo increment =
if consider_function ~libc vinfo then
let update_call_map funcmap =
self#add_map funcmap vinfo
(increment + try VInfoMap.find vinfo !funcmap with Not_found-> 0)
in
if vinfo.vdefined
then update_call_map fundef_calls
else if Annotations.has_funspec (Globals.Functions.get vinfo)
then update_call_map funspec_calls
else update_call_map fundecl_calls
method! vinst i =
begin match i with
| Call(v, e, _, _) ->
self#incr_both_metrics incr_calls;
(match e.enode with
| Lval(Var vinfo, NoOffset) -> self#update_call_maps vinfo 1
| _ -> ());
(match v with
| Some _ -> self#incr_both_metrics incr_assigns
| None -> ());
| Set _ -> self#incr_both_metrics incr_assigns;
| Local_init (_, AssignInit _, _) -> self#incr_both_metrics incr_assigns
| Local_init (_, ConsInit(f,_, k),_) ->
(match k with
| Plain_func -> self#incr_both_metrics incr_assigns
| Constructor -> ());
self#incr_both_metrics incr_calls;
self#update_call_maps f 1
| Asm _ | Skip _ | Code_annot _ -> ()
end;
Cil.DoChildren
end
let dkey = Metrics_parameters.register_category "used-files"
class reachable_from_main visited_vardefs = object
inherit Visitor.frama_c_inplace
val visited_vardefs = ref visited_vardefs
method get_visited_vardefs = !visited_vardefs
method! vvrbl vi =
if vi.vglob && not (Varinfo.Set.mem vi !visited_vardefs) then begin
Metrics_parameters.feedback ~dkey "visiting %a" Printer.pp_varinfo vi;
visited_vardefs := Varinfo.Set.add vi !visited_vardefs;
try
let kf = Globals.Functions.get vi in
try
let fd = Kernel_function.get_definition kf in
let vis = new reachable_from_main !visited_vardefs in
ignore (Visitor.visitFramacFunction (vis :> Visitor.frama_c_visitor) fd);
visited_vardefs :=
Varinfo.Set.union !visited_vardefs vis#get_visited_vardefs
with Kernel_function.No_Definition -> ()
with Not_found ->
let def = Ast.def_or_last_decl vi in
let vis = new reachable_from_main !visited_vardefs in
ignore (Visitor.visitFramacGlobal (vis :> Visitor.frama_c_visitor) def);
visited_vardefs :=
Varinfo.Set.union !visited_vardefs vis#get_visited_vardefs
end;
Cil.SkipChildren
end
let reachable_from_main () =
try
let (kf, _) = Globals.entry_point () in
Metrics_parameters.feedback ~dkey "compute_reachable_from_main: %a"
Kernel_function.pretty kf;
try
let main_fd = Kernel_function.get_definition kf in
let vis = new reachable_from_main (Varinfo.Set.singleton main_fd.svar) in
ignore (Visitor.visitFramacFunction (vis :> Visitor.frama_c_visitor) main_fd);
Some (Varinfo.Set.elements vis#get_visited_vardefs)
with Kernel_function.No_Definition -> None
with Globals.No_such_entry_point _ -> None
let compute_files_defining_globals gvars =
List.fold_left (fun acc vi ->
Metrics_parameters.feedback ~dkey "looking for global: %a"
Printer.pp_varinfo vi;
let def = Ast.def_or_last_decl vi in
let is_def =
match def with
| GVar _ | GFun _ -> true
| _ -> false
in
if is_def then
let loc = Cil_datatype.Global.loc def in
if Location.equal loc Location.unknown then acc
else begin
Metrics_parameters.feedback ~dkey "found %s at: %a"
(if is_def then "definition" else "declaration")
Printer.pp_location loc;
Datatype.Filepath.Set.add ((fst loc).Filepath.pos_path) acc
end
else acc
) (Datatype.Filepath.Set.empty) gvars
class logic_loc_visitor = object
inherit Visitor.frama_c_inplace
val locs = ref Location.Set.empty
method get_locs = !locs
method! vterm t =
locs := Cil_datatype.Location.Set.add t.term_loc !locs;
Cil.DoChildren
method! vpredicate p =
locs := Cil_datatype.Location.Set.add p.pred_loc !locs;
Cil.DoChildren
end
let get_filenames_in_funspec kf =
try
let spec = Annotations.funspec kf in
Metrics_parameters.feedback ~dkey "looking for files in the spec of: %a"
Kernel_function.pretty kf;
List.fold_left (fun acc b ->
let visitor = new logic_loc_visitor in
ignore
(Visitor.visitFramacBehavior (visitor :> Visitor.frama_c_visitor) b);
let locs = visitor#get_locs in
Cil_datatype.Location.Set.fold (fun loc acc' ->
let path = (fst loc).Filepath.pos_path in
Metrics_parameters.feedback ~dkey ~once:true
"found annotation in: %a"
Datatype.Filepath.pretty path;
Datatype.Filepath.Set.add path acc'
) locs acc
) Datatype.Filepath.Set.empty spec.spec_behavior
with Annotations.No_funspec _ -> Datatype.Filepath.Set.empty
let compute_files_defining_funspecs gvars =
List.fold_left
(fun acc vi ->
try
let kf = Globals.Functions.get vi in
let fs = get_filenames_in_funspec kf in
Datatype.Filepath.Set.union acc fs
with Not_found -> acc
) Datatype.Filepath.Set.empty gvars
let used_files () =
match reachable_from_main () with
| None -> Metrics_parameters.abort
"'%s' requires an entry point (-main) with a body"
Metrics_parameters.UsedFiles.option_name
| Some reachable_gvars ->
let used_for_defs = compute_files_defining_globals reachable_gvars in
let used_for_specs = compute_files_defining_funspecs reachable_gvars in
Datatype.Filepath.Set.union used_for_defs used_for_specs
let pretty_used_files used_files =
let cmdline_files = List.fold_left (fun acc file ->
Datatype.Filepath.Set.add (
Datatype.Filepath.of_string (Kernel_file.get_name file)
) acc
) Datatype.Filepath.Set.empty (Kernel_file.get_all ())
in
let used_cmdline_files, used_included_files =
Datatype.Filepath.Set.partition (fun path ->
Datatype.Filepath.Set.mem path cmdline_files
) used_files
in
let is_c_file s = String.ends_with ~suffix:".c" s && s <> ".c" in
let used_included_c_files =
Datatype.Filepath.Set.filter
(fun f -> is_c_file (f : Filepath.Normalized.t :> string))
used_included_files
in
let used_implicitly_included_c_files =
Datatype.Filepath.Set.diff used_included_c_files cmdline_files
in
let unused_cmdline_files =
Datatype.Filepath.Set.diff cmdline_files used_cmdline_files
in
let nb s = Datatype.Filepath.Set.cardinal s in
let pp_filepaths title fmt paths =
let n = nb paths in
if n = 0 then Format.ifprintf fmt ""
else
let title_len = String.length title in
Format.fprintf fmt
"@\n%s (%d)\
@\n%s\
@\n%a@\n"
title n (String.make (title_len + 4) '=')
(Pretty_utils.pp_list ~sep:" \\@\n" ~suf:" \\" Datatype.Filepath.pretty)
(Datatype.Filepath.Set.elements paths)
in
Metrics_parameters.result
"Used files starting at function '%a':@\n\
- command line has %d out of %d file(s) being used@\n\
- %d used file(s) inside #include directives, of which %d '.c' file(s).@\n\
%a%a%a"
Kernel_function.pretty (fst (Globals.entry_point ()))
(nb used_cmdline_files) (nb cmdline_files)
(nb used_included_files) (nb used_included_c_files)
(pp_filepaths "Used command-line files") used_cmdline_files
(pp_filepaths "Unused command-line files") unused_cmdline_files
(pp_filepaths "Used, but implicitly included C files")
used_implicitly_included_c_files
let dump_html fmt cil_visitor =
Format.pp_set_formatter_stag_functions fmt html_stag_functions;
Format.pp_set_tags fmt true;
let pr_row s fmt n =
Format.fprintf fmt
"@{<tr>@[<v 1>@ \
@{<td class=\"entry\">%s@}@ \
@{<td class=\"stat\">%d@}@]@ @} " s n
in
let pr_stats fmt visitor =
let metrics = visitor#get_global_metrics in
Format.fprintf fmt "@[<v 0>@{<table>%a@}@]"
(fun fmt metrics ->
List.iter2 (fun text value -> pr_row text fmt value)
["SLOC"; "Number of if statements"; "Number of assignments";
"Number of loops"; "Number of calls"; "Number of gotos";
"Number of pointer accesses";]
[metrics.cslocs; metrics.cifs; metrics.cassigns;
metrics.cloops; metrics.ccalls; metrics.cgotos;
metrics.cptrs;]) metrics
in
let pr_prelude fmt cil_visitor =
Format.fprintf fmt "@[<v 0>\
@{<div>@ \
@{<h1>@{<span>Metrics@}@}@ \
@{<h2>Synthetic results@}@ <br/>@ \
@{<span>Defined function(s)@} (%d): <br/>@ \
@[ %a@]@ <br/>@ <br/>@ \
@{<span>Specified-only function(s)@} (%d):@ <br/>@ \
@[ %a@]@ <br>@ <br/>@ \
@{<span>Undefined and unspecified function(s)@} (%d):@ <br/>@ \
@[ %a@]@ <br>@ <br/>@ \
@{<span>'Extern' global variable(s)@} (%d):@ <br/>@ \
@[ %a@]@ <br>@ <br/>@ \
@{<span>Potential entry point(s)@} (%d):@ <br/>@ \
@[ %a@]@ <br/>@ <br/>@ \
@}@]"
(VInfoMap.cardinal cil_visitor#fundef_calls)
Metrics_base.pretty_set cil_visitor#fundef_calls
(VInfoMap.cardinal cil_visitor#funspec_calls)
Metrics_base.pretty_set cil_visitor#funspec_calls
(VInfoMap.cardinal cil_visitor#fundecl_calls)
Metrics_base.pretty_set cil_visitor#fundecl_calls
(VInfoSet.cardinal cil_visitor#extern_global_vars)
Metrics_base.pretty_extern_vars cil_visitor#extern_global_vars
(Metrics_base.number_entry_points cil_visitor#fundef_calls)
Metrics_base.pretty_entry_points cil_visitor#fundef_calls
in
let pr_detailed_results fmt cil_visitor =
Format.fprintf fmt "@[<v 0>\
@{<div style=\"text-align: left;\">\
@[<v 2>@ \
@{<h2>Detailed results@}@ \
@[<v 0>%a@ @]\
@]@}"
(fun fmt cil_visitor -> cil_visitor#print_stats fmt) cil_visitor
in
Format.fprintf fmt "@[<v 0>\
<!DOCTYPE html>@ \
@{<html>@ \
@{<head>@ \
@{<title>%s@}@ \
<meta charset=\"utf-8\">@ \
@{<style type=\"text/css\">%s@}@ \
@}@ \
@{<body>\
@[<v 2>@ \
%a@ \
%a@ \
%a@ \
@]@}@}@]@?"
"Metrics"
Css_html.css
pr_prelude cil_visitor
pr_stats cil_visitor
pr_detailed_results cil_visitor
;;
let pp_funinfo fmt vis =
let nfundef = VInfoMap.cardinal vis#fundef_calls in
let nfunspec = VInfoMap.cardinal vis#funspec_calls in
let nfundecl = VInfoMap.cardinal vis#fundecl_calls in
let nextern = VInfoSet.cardinal vis#extern_global_vars in
let fundef_hdr = Format.sprintf "Defined functions (%d)" nfundef
and funspec_hdr = Format.sprintf "Specified-only functions (%d)" nfunspec
and fundecl_hdr = Format.sprintf "Undefined and unspecified functions (%d)" nfundecl
and extern_hdr = Format.sprintf "'Extern' global variables (%d)" nextern
and entry_pts_hdr = Format.sprintf "Potential entry points (%d)"
(Metrics_base.number_entry_points vis#fundef_calls) in
Format.fprintf fmt
"@[<v 0>@[<v 1>%a@ @[%a@]@]@ @ \
@[<v 1>%a@ @[%a@]@]@ @ \
@[<v 1>%a@ @[%a@]@]@ @ \
@[<v 1>%a@ @[%a@]@]@ @ \
@[<v 1>%a@ @[%a@]@]@ \
@]"
(Metrics_base.mk_hdr 1) fundef_hdr
Metrics_base.pretty_set vis#fundef_calls
(Metrics_base.mk_hdr 1) funspec_hdr
Metrics_base.pretty_set vis#funspec_calls
(Metrics_base.mk_hdr 1) fundecl_hdr
Metrics_base.pretty_set vis#fundecl_calls
(Metrics_base.mk_hdr 1) extern_hdr
Metrics_base.pretty_extern_vars vis#extern_global_vars
(Metrics_base.mk_hdr 1) entry_pts_hdr
Metrics_base.pretty_entry_points vis#fundef_calls
;;
let json_of_funinfo vis =
let fundef =
("defined-functions", json_of_varinfo_map vis#fundef_calls)
in
let funspec =
("specified-only-functions", json_of_varinfo_map vis#funspec_calls)
in
let fundecl =
("undefined-functions", json_of_varinfo_map vis#fundecl_calls)
in
let extern_vars =
VInfoSet.fold (fun vi acc -> `String vi.vname :: acc)
vis#extern_global_vars []
in
let extern =
("extern-global-vars", `List (List.rev extern_vars))
in
let entry_points =
("entry-points", json_of_entry_points vis#fundef_calls)
in
`Assoc [fundef; funspec; fundecl; extern; entry_points]
let pp_with_funinfo fmt cil_visitor =
Format.fprintf fmt "@[<v 0>%a@ %a@]"
pp_funinfo cil_visitor
pp_base_metrics cil_visitor#get_global_metrics
;;
let get_global_metrics ~libc =
let file = Ast.get () in
let cil_visitor = new slocVisitor ~libc in
Visitor.visitFramacFileSameGlobals
(cil_visitor:>Visitor.frama_c_visitor) file;
cil_visitor#get_global_metrics
;;
let get_metrics_map ~libc =
let file = Ast.get () in
let cil_visitor = new slocVisitor ~libc in
Visitor.visitFramacFileSameGlobals
(cil_visitor:>Visitor.frama_c_visitor) file;
cil_visitor#get_metrics_map
;;
let get_cilast_metrics ~libc =
let file = Ast.get () in
let cil_visitor = new slocVisitor ~libc in
Visitor.visitFramacFileSameGlobals
(cil_visitor:>Visitor.frama_c_visitor) file;
{
fundecl_calls = cil_visitor#fundecl_calls;
funspec_calls = cil_visitor#funspec_calls;
fundef_calls = cil_visitor#fundef_calls;
extern_global_vars = cil_visitor#extern_global_vars;
basic_global_metrics = cil_visitor#get_global_metrics;
}
;;
let compute_on_cilast ~libc =
let file = Ast.get () in
let cil_visitor = new slocVisitor ~libc in
Visitor.visitFramacFileSameGlobals
(cil_visitor:>Visitor.frama_c_visitor) file;
if Metrics_parameters.ByFunction.get () then
Metrics_parameters.result
"@[<v 0>Cil AST@ %t@]" cil_visitor#pp_detailed_text_metrics;
if not (Metrics_parameters.OutputFile.is_empty ()) then begin
let out_fname = Metrics_parameters.OutputFile.get () in
try
let oc = open_out_bin (out_fname:>string) in
let fmt = Format.formatter_of_out_channel oc in
(match Metrics_base.get_file_type out_fname with
| Html -> dump_html fmt cil_visitor
| Text -> pp_with_funinfo fmt cil_visitor
| Json ->
let json = json_of_funinfo cil_visitor in
Yojson.pretty_print fmt json;
Format.fprintf fmt "@."
);
close_out oc;
with Sys_error s ->
Metrics_parameters.abort "Cannot open file %a (%s)."
Filepath.Normalized.pretty out_fname s
end
else Metrics_parameters.result "%a" pp_with_funinfo cil_visitor
class locals_size_visitor kf callstack = object
val mutable locals_size_no_temps = Integer.zero
method get_locals_size_no_temps = locals_size_no_temps
val mutable locals_size_temps = Integer.zero
method get_locals_size_temps = locals_size_temps
val mutable max_size_calls_no_temps = Integer.zero
method get_max_size_calls_no_temps = max_size_calls_no_temps
val mutable max_size_calls_temps = Integer.zero
method get_max_size_calls_temps = max_size_calls_temps
inherit Visitor.frama_c_inplace
method! vinst i = match i with
| Call (_, { enode = Lval(Var vi, NoOffset) }, _, _)
| Local_init(_, ConsInit(vi,_,_),_) ->
begin
try
let kf' = Globals.Functions.find_by_name vi.vname in
Metrics_parameters.debug
"@[function %a:@;computing call to function %a@]"
Kernel_function.pretty kf Kernel_function.pretty kf';
let new_cs = kf' :: callstack in
if List.mem kf' callstack then
Metrics_parameters.abort
"@[unsupported recursive call detected:@;%a@]"
(Pretty_utils.pp_list ~sep:"@ <-@ " Kernel_function.pretty)
(List.rev new_cs);
let new_vis = new locals_size_visitor kf' new_cs in
ignore (Visitor.visitFramacKf
(new_vis :> Visitor.frama_c_visitor) kf');
let call_size_no_temps =
Integer.add new_vis#get_max_size_calls_no_temps
new_vis#get_locals_size_no_temps
in
let call_size_temps =
Integer.add new_vis#get_max_size_calls_temps
new_vis#get_locals_size_temps
in
max_size_calls_no_temps <-
Integer.max max_size_calls_no_temps call_size_no_temps;
max_size_calls_temps <-
Integer.max max_size_calls_temps call_size_temps
with Not_found ->
Metrics_parameters.fatal ~current:true
"@[function not found:@;%s@]" vi.vname;
end;
Cil.DoChildren
| _ -> Cil.DoChildren
method! vvdec vi =
if not vi.vglob && not vi.vghost && vi.vstorage = NoStorage then
begin
let size_exp = Cil.sizeOf ~loc:vi.vdecl vi.vtype in
match Cil.constFoldToInt size_exp with
| None -> Metrics_parameters.error
"@[in function %a,@;cannot compute sizeof %a (type %a)@]"
Kernel_function.pretty kf Printer.pp_varinfo vi
Printer.pp_typ vi.vtype
| Some size ->
Metrics_parameters.debug "@[function %a:@;sizeof(%a) = %a (%s)@]"
Kernel_function.pretty kf
Printer.pp_varinfo vi Integer.pretty size
(if vi.vtemp then "temp" else "non-temp");
if vi.vtemp then
locals_size_temps <- Integer.add locals_size_temps size
else
locals_size_no_temps <- Integer.add locals_size_no_temps size
end;
Cil.DoChildren
end
let compute_locals_size kf =
let vis = new locals_size_visitor kf [kf] in
ignore (Visitor.visitFramacKf (vis :> Visitor.frama_c_visitor) kf);
Metrics_parameters.result "@[%a\t%a\t%a\t%a\t%a@]"
Kernel_function.pretty kf
Integer.pretty vis#get_locals_size_no_temps
Integer.pretty
(Integer.add vis#get_locals_size_no_temps vis#get_locals_size_temps)
Integer.pretty vis#get_max_size_calls_no_temps
Integer.pretty
(Integer.add vis#get_max_size_calls_no_temps vis#get_max_size_calls_temps)
;;