Source file standard.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
open Cil_types
open Va_types
open Options
module List = Extends.List
module Typ = Extends.Typ
let pp_prototype name fmt tparams =
Format.fprintf fmt "%s(%a)"
name
(Pretty_utils.pp_list ~sep:", " Printer.pp_typ) tparams
let pp_overload name fmt l =
let prototypes = List.map fst l in
Pretty_utils.pp_list ~sep:"@\n" (pp_prototype name) fmt prototypes
module Fallback_counts =
State_builder.Hashtbl
(Datatype.String.Hashtbl)
(Datatype.Int)
(struct
let size = 17
let name = "fallback_counts"
let dependencies = [ Options.Enabled.self; Options.Strict.self ]
end)
exception Translate_call_exn of varinfo
let extended_integer_typenames =
["int8_t"; "uint8_t"; "int_least8_t"; "uint_least8_t";
"int_fast8_t"; "uint_fast8_t";
"int16_t"; "uint16_t"; "int_least16_t"; "uint_least16_t";
"int_fast16_t"; "uint_fast16_t";
"int32_t"; "uint32_t"; "int_least32_t"; "uint_least32_t";
"int_fast32_t"; "uint_fast32_t";
"int64_t"; "uint64_t"; "int_least64_t"; "uint_least64_t";
"int_fast64_t"; "uint_fast64_t"]
let is_extended_integer_type t =
match t with
| TNamed (ti, _) -> List.mem ti.tname extended_integer_typenames
| _ -> false
let integral_rep ikind =
Cil.bitsSizeOfInt ikind, Cil.isSigned ikind
let expose t =
Cil.type_remove_attributes_for_c_cast (Cil.unrollType t)
type castability = Strict
| Tolerated
| NonPortable
| NonStrict
| Never
let can_cast given expected =
match expose given, expose expected with
| t1, t2 when Cil_datatype.Typ.equal t1 t2 -> Strict
| (TInt (i1,a1) | TEnum({ekind=i1},a1)),
(TInt (i2,a2) | TEnum({ekind=i2},a2)) ->
if integral_rep i1 <> integral_rep i2 ||
not (Cil_datatype.Attributes.equal a1 a2) then
Never
else if is_extended_integer_type given then
Tolerated
else if i1 = i2 then
NonPortable
else
NonStrict
| TPtr _, TPtr _ -> Strict
| _, _ -> Never
let does_fit exp typ =
match Cil.constFoldToInt exp, Cil.unrollType typ with
| Some i, (TInt (ekind,_) | TEnum({ekind},_)) ->
Cil.fitsInInt ekind i
| _ -> false
let pretty_typ fmt t =
match Cil.unrollType t with
| TEnum (ei, _) ->
Format.fprintf fmt "%a (%a)" Printer.pp_typ t
Printer.pp_typ (TInt (ei.ekind, []))
| _ -> Printer.pp_typ fmt t
let cast_arg i paramtyp exp =
let argtyp = Cil.typeOf exp in
if not (does_fit exp paramtyp) then
begin match can_cast argtyp paramtyp with
| Strict | Tolerated -> ()
| (NonPortable | NonStrict) when not (Strict.get ()) -> ()
| NonPortable ->
Self.warning ~current:true ~wkey:wkey_typing
"Possible portability issues with enum type for argument %d \
(use -variadic-no-strict to avoid this warning)."
(i + 1)
| NonStrict | Never ->
Self.warning ~current:true ~wkey:wkey_typing
"Incorrect type for argument %d. \
The argument will be cast from %a to %a."
(i + 1)
pretty_typ argtyp pretty_typ paramtyp
end;
Cil.mkCast ~check:false ~force:false ~newt:paramtyp exp
let match_args ~callee tparams args =
let paramcount = List.length tparams
and argcount = List.length args in
if argcount > paramcount then
Self.warning ~current:true ~wkey:wkey_typing
"Too many arguments: expected %d, given %d. \
Superfluous arguments will be removed."
paramcount argcount
else if argcount < paramcount then (
Self.warning ~current:true ~wkey:wkey_typing
"Not enough arguments: expected %d, given %d."
paramcount argcount;
raise (Translate_call_exn callee)
);
let new_args, unused_args = List.break paramcount args in
List.mapi2 cast_arg tparams new_args, unused_args
let match_call ~builder new_callee new_tparams args =
let module Build = (val builder : Builder.S) in
let new_args, unused_args = match_args ~callee:new_callee new_tparams args in
Build.start_translation ();
Build.(List.iter pure (of_exp_list unused_args));
Build.(translated_call (var new_callee) (of_exp_list new_args))
let check_available_name env name =
not @@ Environment.mem_global env name
&& not @@ Environment.mem_function env name
let get_next_name env id name =
let rec aux id =
let next_name = name ^ (string_of_int id) in
if check_available_name env next_name then
next_name, id
else
aux (id + 1)
in
aux id
let fallback_fun_call ~builder ~callee env vf args =
let module Build = (val builder : Builder.S) in
let name = callee.vname in
let vorig_name = callee.vorig_name in
let count = try Fallback_counts.find name + 1 with Not_found -> 1 in
let new_name, new_count = get_next_name env count (name ^ "_fallback_") in
Fallback_counts.replace name new_count;
let loc = vf.vf_decl.vdecl in
let new_callee = Build.open_function ~loc ~vorig_name new_name in
let ret_typ, params, _, attrs = Cil.splitFunctionType vf.vf_original_type in
Build.set_return_type' ret_typ;
List.iter Build.add_attribute attrs;
Build.add_stdlib_generated ();
let fixed_params_count = Typ.params_count vf.vf_original_type in
let add_static_param (name,typ,attributes) =
ignore (Build.parameter ~attributes typ name)
and add_variadic_param i e =
let typ = Cil.typeOf e in
ignore (Build.parameter typ ("param" ^ string_of_int i))
in
List.iter add_static_param (Option.get params);
List.iteri add_variadic_param (List.drop fixed_params_count args);
Build.finish_declaration ();
Replacements.add (Build.cil_varinfo new_callee) vf.vf_decl;
Build.start_translation ();
Self.result ~current:true ~level:2
"Fallback translation of call %s to a call to the specialized version %a."
vf.vf_decl.vorig_name Build.pretty new_callee;
Build.(translated_call new_callee (List.map of_exp args))
let find_null exp_list =
List.ifind (fun e -> Cil.isZero (Cil.constFold false e)) exp_list
let aggregator_call ~builder aggregator vf args =
let module Build = (val builder : Builder.S) in
let {a_target; a_pos; a_type; a_param} = aggregator in
let name = vf.vf_decl.vorig_name
and tparams = Typ.params_types a_target.vtype
and pname, ptyp = a_param in
let argcount = List.length args
and paramcount = List.length tparams in
if argcount < paramcount then begin
Self.warning ~current:true ~wkey:wkey_typing
"Not enough arguments: expected %d, given %d."
paramcount argcount;
raise (Translate_call_exn vf.vf_decl);
end;
let size = match a_type with
| EndedByNull ->
begin try
find_null (List.drop a_pos args) + 1
with Not_found ->
Self.warning ~current:true
"Failed to find a sentinel (NULL pointer) in the argument list.";
raise (Translate_call_exn vf.vf_decl);
end
in
let tparams_left = List.take a_pos tparams in
let tparams_right = List.drop (a_pos + 1) tparams in
let new_tparams = tparams_left @ List.make size ptyp @ tparams_right in
let new_args, unused_args = match_args ~callee:vf.vf_decl new_tparams args in
let args_left, args_rem = List.break a_pos new_args in
let args_middle, args_right = List.break size args_rem in
Self.result ~current:true ~level:2
"Translating call to %s to a call to %s."
name a_target.vorig_name;
let pname = if pname = "" then "param" else pname in
Build.start_translation ();
let init = match args_middle with
| [] -> [Build.(of_init (Cil.makeZeroInit ~loc ptyp))]
| l -> List.map Build.of_exp l
in
let size = List.length init in
let vaggr = Build.(local (array ~size (of_ctyp ptyp)) pname ~init) in
let new_args = args_left @ [Build.(cil_exp ~loc (addr vaggr))] @ args_right in
let new_args,_ = match_args ~callee:vf.vf_decl tparams new_args in
Build.(List.iter pure (of_exp_list unused_args));
Build.(translated_call (var a_target) (of_exp_list new_args))
let rec check_arg_matching expected given =
match Cil.unrollType given, Cil.unrollType expected with
| (TInt _ | TEnum _), (TInt _ | TEnum _) -> true
| TPtr _, _ when Cil.isVoidPtrType expected -> true
| TPtr (t1, _), TPtr (t2, _) -> check_arg_matching t1 t2
| _, _ -> not (Cil.need_cast given expected)
let rec check_call_matching tparams targs =
match tparams, targs with
| [], [] -> true
| [], _
| _, [] -> false
| a1 :: l1, a2 :: l2 ->
check_arg_matching a1 a2 &&
check_call_matching l1 l2
let filter_matching_prototypes overload args =
let targs = List.map Cil.typeOf args in
let check (tparams, _vi) = check_call_matching tparams targs in
List.filter check overload
let overloaded_call ~builder overload vf args =
let name = vf.vf_decl.vorig_name in
let tparams, new_callee =
match filter_matching_prototypes overload args with
| [] ->
Self.warning ~current:true ~wkey:wkey_prototype
"@[No matching prototype found for this call to %s.@.\
Expected candidates:@.\
@[<v> %a@]@.\
Given arguments:@.\
@[<v> %a@]"
name (pp_overload name) overload
(pp_prototype name) (List.map Cil.typeOf args);
raise (Translate_call_exn vf.vf_decl);
| [(tparams,vi)] ->
tparams, vi
| l ->
Self.warning ~current:true ~wkey:wkey_prototype
"Ambiguous call to %s. Matching candidates are: \
%a"
name
(pp_overload name) l;
raise (Translate_call_exn vf.vf_decl);
in
Replacements.add new_callee vf.vf_decl;
Self.result ~current:true ~level:2
"Translating call to the specialized version %a."
(pp_prototype name) tparams;
match_call ~builder new_callee tparams args
let rec static_string a = match a.enode with
| Const (CStr s) -> Some (Format_string.String s)
| Const (CWStr s) -> Some (Format_string.WString s)
| CastE (_, e) -> static_string e
| _ -> None
let find_global env name =
try
Some (Environment.find_global env name)
with Not_found ->
Self.warning ~once:true ~wkey:wkey_libc_framac
"Unable to locate global %s which should be in the Frama-C LibC. \
Correct specifications can't be generated."
name;
None
let find_predicate name =
match Logic_env.find_all_logic_functions name with
| f :: _q -> f
| [] ->
Self.warning ~once:true ~wkey:wkey_libc_framac
"Unable to locate ACSL predicate %s which should be in the Frama-C LibC. \
Correct specifications can't be generated."
name;
raise Not_found
let find_field env structname fieldname =
try
let compinfo = Environment.find_struct env structname in
Cil.getCompField compinfo fieldname
with Not_found ->
Self.warning ~once:true
"Unable to locate %s field %s."
structname fieldname;
raise Not_found
let find_predicate_by_width typ narrow_name wide_name =
match Cil.unrollTypeDeep typ with
| TPtr (TInt(IChar, _), _) -> find_predicate narrow_name
| TPtr (t, _) when
Cil_datatype.Typ.equal
(Cil.typeDeepDropAllAttributes (Cil.unrollTypeDeep t))
(Machine.wchar_type ()) ->
find_predicate wide_name
| _ ->
Self.warning ~current:true ~wkey:wkey_typing
"expected single/wide character pointer type, got %a (%a, unrolled %a)"
Printer.pp_typ typ Cil_types_debug.pp_typ typ Cil_types_debug.pp_typ (Cil.unrollTypeDeep typ);
raise Not_found
let valid_read_string typ =
find_predicate_by_width typ "valid_read_string" "valid_read_wstring"
let valid_read_nstring typ =
find_predicate_by_width typ "valid_read_nstring" "valid_read_nwstring"
let format_length typ =
find_predicate_by_width typ "format_length" "wformat_length"
let build_specialized_fun ~builder env vf format_fun tvparams =
let open Format_types in
let module Build = (val builder : Builder.S) in
let name = vf.vf_decl.vorig_name in
let id = vf.vf_specialization_count + 1 in
let new_name, new_count = get_next_name env id (name ^ "_va_") in
vf.vf_specialization_count <- new_count;
let loc = vf.vf_decl.vdecl in
let funvar = Build.open_function ~loc ~vorig_name:name new_name in
let ret_typ, params, _, attrs = Cil.splitFunctionType vf.vf_original_type in
Build.set_return_type' ret_typ;
List.iter Build.add_attribute attrs;
Build.add_stdlib_generated ();
let fresh_param_name =
let counter = ref 0 in
fun () ->
let p = "param" ^ string_of_int !counter in
incr counter;
p
in
let add_static_param (name,typ,attributes) =
let name = if name = "" then fresh_param_name () else name in
Build.parameter ~attributes typ name
and add_variadic_param (typ,_dir) =
let typ = if Cil.isIntegralType typ then
Cil.integralPromotion typ
else
typ
in
Build.parameter typ (fresh_param_name ())
in
let sformals = List.map add_static_param (Option.get params)
and vformals = List.map add_variadic_param tvparams
in
let sources = ref [] and dests = ref [] in
let add_source ?(indirect=false) s =
let s = (s :> Build.source) in
sources := (if indirect then Build.indirect s else s) :: !sources
and add_dest d =
dests := (d :> Build.exp) :: !dests
in
let add_lval ~indirect lval = function
| (`ArgIn | `ArgInArray _) -> add_source ~indirect lval
| (`ArgOut | `ArgOutArray) -> add_dest lval
| `ArgInOut -> add_source ~indirect lval; add_dest lval
in
let add_var ?pos ~indirect (v : Build.var) dir =
let ty = Build.cil_typeof v in
let lval = match dir with
| `ArgIn -> (v :> Build.lval)
| (`ArgInArray _ | `ArgOutArray) -> Build.(index v whole_right)
| (`ArgOut | `ArgInOut) -> Build.(mem v)
in
add_lval ~indirect lval dir;
try match dir with
| `ArgInArray None ->
Build.(requires (app (valid_read_string ty) [here] [v]))
| `ArgInArray (Some precision) ->
let nterm = match precision with
| PStar ->
let size_arg = List.nth vformals (Option.get pos - 1) in
Build.(cast integer size_arg)
| PInt n ->
Build.of_int n
in
Build.(requires (app (valid_read_nstring ty) [here] [(v :> Build.exp) ; nterm]))
| `ArgOut ->
Build.(requires (valid v));
Build.(ensures (initialized v))
| _ -> ()
with Not_found -> ()
in
let l = List.combine vformals tvparams in
List.iteri (fun pos (v,(_,dir)) -> add_var ~indirect:false ~pos v dir) l;
let fmt = List.nth sformals format_fun.f_format_pos in
add_var ~indirect:true fmt (`ArgInArray None);
let add_stream v =
try
let f_data = find_field env "__fc_FILE" "__fc_FILE_data"
and f_id = find_field env "__fc_FILE" "__fc_FILE_id" in
add_lval ~indirect:false Build.(field v f_data) `ArgInOut;
add_lval ~indirect:true Build.(field v f_id) `ArgIn
with Not_found ->
add_var ~indirect:false v `ArgInOut
in
let add_buffer buffer size =
add_var ~indirect:true size `ArgIn;
let valid_range length =
Build.(valid (buffer + (zero -- (length - one))))
in
let left_pred = valid_range size in
try
let flen = format_length (Build.cil_typeof buffer) in
let right_pred = Build.(valid_range (app flen [here] [fmt])) in
Build.(requires (logor left_pred right_pred))
with
| Not_found -> Build.requires left_pred
| Build.NotAFunction li ->
Self.abort ~current:true
"%a should be a logic function, not a predicate"
Printer.pp_logic_var li.l_var_info
in
begin match format_fun.f_buffer, format_fun.f_kind with
| StdIO, ScanfLike ->
begin match find_global env "__fc_stdin" with
| Some vi -> add_stream (Build.var vi)
| None -> ()
end
| StdIO, PrintfLike ->
begin match find_global env "__fc_stdout" with
| Some vi -> add_stream (Build.var vi)
| None -> ()
end
| Arg (i, _), ScanfLike ->
add_var ~indirect:true (List.nth sformals i) (`ArgInArray None)
| Arg (i, size_pos), PrintfLike ->
add_var ~indirect:true (List.nth sformals i) (`ArgOutArray);
begin match size_pos with
| Some n ->
add_buffer (List.nth sformals i) (List.nth sformals n)
| None -> ()
end
| Stream i, _ ->
add_stream (List.nth sformals i)
| File i, _ ->
let file = List.nth sformals i in
add_var ~indirect:true file `ArgIn;
| Syslog, _ -> ()
end;
if not (Cil.isVoidType ret_typ) then
Build.(assigns [result] (List.map indirect !sources));
Build.assigns !dests !sources;
Build.finish_declaration ();
Build.cil_varinfo funvar
let format_of_ikind = function
| IBool -> Some `hh, `u
| IChar -> None, `c
| ISChar -> Some `hh, `d
| IUChar -> Some `hh, `u
| IInt -> None, `d
| IUInt -> None, `u
| IShort -> Some `h, `d
| IUShort -> Some `h, `u
| ILong -> Some `l, `d
| IULong -> Some `l, `u
| ILongLong -> Some `ll, `d
| IULongLong -> Some `ll, `u
let format_of_fkind k = function
| FFloat -> None, `f
| FDouble ->
(match k with
| Format_types.PrintfLike -> None, `f
| ScanfLike -> Some `l, `f)
| FLongDouble -> Some `L, `f
let rec format_of_type vf k t =
match t with
| TInt (ikind,_) | TEnum ({ekind = ikind},_) -> format_of_ikind ikind
| TFloat (fkind,_) -> format_of_fkind k fkind
| TPtr(_,_) ->
if Cil.isCharPtrType t then
None, `s
else
None, `p
| TNamed ({tname;ttype},_) ->
(match tname with
| "size_t" -> Some `z, `u
| "ptrdiff_t" -> Some `t, `d
| "intmax_t" -> Some `j, `d
| "uintmax_t" -> Some `j, `u
| "ssize_t" -> Some `z, `d
| _ -> format_of_type vf k ttype
)
| TVoid _ -> raise (Translate_call_exn vf.vf_decl)
| TComp _
| TFun _
| TArray _
| TBuiltin_va_list _ -> raise (Translate_call_exn vf.vf_decl)
let infer_format_from_args vf format_fun args =
let args = List.drop (format_fun.f_format_pos + 1) args in
let f_format (l,s) =
Format_types.(
Specification
{ f_flags = [];
f_field_width = None;
f_precision = None;
f_length_modifier = l;
f_conversion_specifier = s;
f_capitalize = false;
})
in
let s_format (l,s) =
Format_types.(
Specification
{ s_assignment_suppression = false;
s_field_width = None;
s_length_modifier = l;
s_conversion_specifier = s;
}
)
in
let treat_one_arg arg =
let t = Cil.typeOf arg in
let t =
match format_fun.f_kind with
| PrintfLike -> t
| ScanfLike ->
if not (Cil.isPointerType t) then begin
let source = fst arg.eloc in
Self.warning ~source ~wkey:wkey_typing
"Expecting pointer as parameter of scanf function. \
Argument %a has type %a"
Printer.pp_exp arg Printer.pp_typ t;
raise (Translate_call_exn vf.vf_decl);
end;
Cil.typeOf_pointed t
in
format_of_type vf format_fun.f_kind t
in
let format = List.map treat_one_arg args in
match format_fun.f_kind with
| PrintfLike -> Format_types.FFormat (List.map f_format format)
| ScanfLike -> Format_types.SFormat (List.map s_format format)
let format_fun_call ~builder env format_fun vf args =
let format =
try
let format_arg = List.nth args format_fun.f_format_pos in
match static_string format_arg with
| None ->
Self.warning ~current:true
"Call to function %s with non-static format argument: \
assuming that parameters are coherent with the format, and that \
no %%n specifiers are present in the actual string."
vf.vf_decl.vorig_name;
infer_format_from_args vf format_fun args
| Some s -> Format_parser.parse_format format_fun.f_kind s
with
| Format_parser.Invalid_format -> raise (Translate_call_exn vf.vf_decl)
in
let find_typedef = Environment.find_type env in
let tvparams =
try
Format_typer.type_format ~find_typedef format
with Format_typer.Type_not_found (type_name) ->
Self.warning ~current:true
"Unable to find type %s in the source code which should be used in \
this call:@ no specification will be generated.@ \
Note that due to cleanup, the type may have been defined in the \
original code but not used anywhere.@.\
Did you include <stdint.h> ?" type_name;
raise (Translate_call_exn vf.vf_decl)
in
let new_callee = build_specialized_fun ~builder env vf format_fun tvparams in
Replacements.add new_callee vf.vf_decl;
Self.result ~current:true ~level:2
"Translating call to %s to a call to the specialized version %s."
vf.vf_decl.vorig_name new_callee.vname;
let tparams = Typ.params_types new_callee.vtype in
match_call ~builder new_callee tparams args