forked from cil-project/cil
-
Notifications
You must be signed in to change notification settings - Fork 24
Expand file tree
/
Copy pathcabs2cil.ml
More file actions
7251 lines (6643 loc) · 290 KB
/
cabs2cil.ml
File metadata and controls
7251 lines (6643 loc) · 290 KB
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
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
Copyright (c) 2001-2002,
George C. Necula <necula@cs.berkeley.edu>
Scott McPeak <smcpeak@cs.berkeley.edu>
Wes Weimer <weimer@cs.berkeley.edu>
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:
1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
3. The names of the contributors may not be used to endorse or promote
products derived from this software without specific prior written
permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)
(* Type check and elaborate ABS to CIL *)
(* The references to ISO means ANSI/ISO 9899-1999 *)
module A = Cabs
module C = Cabshelper
module V = Cabsvisit
module E = Errormsg
module H = Hashtbl
module IH = Inthash
module AL = Alpha
open Cabs
open Cabshelper
open Pretty
open Cil
open Cilint
open Trace
(* This exception is thrown if there is an attempt to transform Tauto into a CIL type *)
exception TautoEncountered
let debugGlobal = false
let continueOnError = true
(** Turn on tranformation that forces correct parameter evaluation order *)
let forceRLArgEval = ref false
(** By default, we warn as large constants cannot be appropriately represented as OCaml floats.
This can be set to true by tools that are aware of this problem and only use the string component of CReal
to avoid emitting warnings that are spurious in that context. *)
let silenceLongDoubleWarning = ref false
(** Leave a certain global alone. Use a negative number to disable. *)
let nocil: int ref = ref (-1)
(** Set to true to generate VarDecl "instructions" for all local variables
In some circumstances, it is unavoidable to generate VarDecls (namely
for variable length arrays (VLAs)). In these cases, we generate a VarDecl
even if alwaysGenerateVarDecl is false.
Under certain conditions (involving GNU computed gotos), it is not possible
to generate VarDecls for all locals, in these cases we do not generate them
*)
let alwaysGenerateVarDecl = false
(** Add an attribute to all variables which are not declared at the top scope,
so tools building on CIL can know which variables were pulled up.
Should be disabled when printing CIL code, as compilers will warn about this attribute.
*)
let addNestedScopeAttr = ref false
let addLoopConditionLabels = ref false
(** Indicates whether we're allowed to duplicate small chunks. *)
let allowDuplication: bool ref = ref true
(** If false, the destination of a Call instruction should always have the
same type as the function's return type. Where needed, CIL will insert
a temporary to make this happen.
If true, the destination type may differ from the return type, so there
is an implicit cast. This is useful for analyses involving [malloc],
because the instruction "T* x = malloc(...);" won't be broken into
two instructions, so it's easy to find the allocation type.
This is false by default. Set to true to replicate the behavior
of CIL 1.3.5 and earlier.
*)
let doCollapseCallCast: bool ref = ref false
(** Disables caching of globals during parsing. This is handy when we want
to parse additional source files without hearing about confclits. *)
let cacheGlobals: bool ref = ref true
(** A hook into the code for processing typeof. *)
let typeForTypeof: (Cil.typ -> Cil.typ) ref = ref (fun t -> t)
(** A hook into the code that creates temporary local vars. By default this
is the identity function, but you can overwrite it if you need to change the
types of cabs2cil-introduced temp variables. *)
let typeForInsertedVar: (Cil.typ -> Cil.typ) ref = ref (fun t -> t)
(** Like [typeForInsertedVar], but for casts.
Casts in the source code are exempt from this hook. *)
let typeForInsertedCast: (Cil.typ -> Cil.typ) ref = ref (fun t -> t)
(** A hook into the code that remaps argument names in the appropriate
attributes. *)
let typeForCombinedArg: ((string, string) H.t -> typ -> typ) ref =
ref (fun _ t -> t)
(** A hook into the code that remaps argument names in the appropriate
attributes. *)
let attrsForCombinedArg: ((string, string) H.t ->
attributes -> attributes) ref =
ref (fun _ t -> t)
(** Interface to the Cprint printer *)
let withCprint (f: 'a -> unit) (x: 'a) : unit =
Cprint.commit (); Cprint.flush ();
let old = (Whitetrack.getOutput()) in
Whitetrack.setOutput !E.logChannel;
f x;
Cprint.commit (); Cprint.flush ();
flush (Whitetrack.getOutput());
Whitetrack.setOutput old
(** Keep a list of the variable ID for the variables that were created to
hold the result of function calls *)
let callTempVars: unit IH.t = IH.create 13
let allTempVars: unit IH.t = IH.create 13
(* Keep a list of functions that were called without a prototype. *)
let noProtoFunctions : bool IH.t = IH.create 13
(* Check that s starts with the prefix p *)
let prefix p s =
let lp = String.length p in
let ls = String.length s in
lp <= ls && String.sub s 0 lp = p
(***** COMPUTED GOTO ************)
(* The address of labels are small integers (starting from 0). A computed
goto is replaced with a switch on the address of the label. We generate
only one such switch and we'll jump to it from all computed gotos. To
accomplish this we'll add a local variable to store the target of the
goto. *)
(* The local variable in which to put the destination of the goto and the
statement where to jump *)
let gotoTargetData: (varinfo * stmt) option ref = ref None
(* The "addresses" of labels *)
let gotoTargetHash: (string, int) H.t = H.create 13
let gotoTargetNextAddr: int ref = ref 0
(********** TRANSPARENT UNION ******)
(* Check if a type is a transparent union, and return the first field if it
is *)
let isTransparentUnion (t: typ) : fieldinfo option =
match unrollType t with
TComp (comp, _) when not comp.cstruct ->
(* Turn transparent unions into the type of their first field *)
if hasAttribute "transparent_union" (typeAttrs t) then begin
match comp.cfields with
f :: _ -> Some f
| _ -> E.s (unimp "Empty transparent union: %s" (compFullName comp))
end else
None
| _ -> None
(* When we process an argument list, remember the argument index which has a
transparent union type, along with the original type. We need this to
process function definitions *)
let transparentUnionArgs : (int * typ) list ref = ref []
let debugLoc = false
let convLoc (l : cabsloc) =
if debugLoc then
ignore (E.log "convLoc at %s: line %d, byte %d, column %d\n" l.filename l.lineno l.byteno l.columnno);
{line = l.lineno; file = l.filename; byte = l.byteno; column = l.columnno; endLine = l.endLineno; endByte = l.endByteno; endColumn = l.endColumnno; synthetic = false;}
let isOldStyleVarArgName n = n = "__builtin_va_alist"
let isOldStyleVarArgTypeName n = n = "__builtin_va_alist_t"
let isVariadicListType t =
match unrollType t with
| TBuiltin_va_list _ -> true
| _ -> false
(* Weimer
multi-character character constants
In MSCV, this code works:
long l1 = 'abcd'; // note single quotes
char * s = "dcba";
long * lptr = ( long * )s;
long l2 = *lptr;
assert(l1 == l2);
We need to change a multi-character character literal into the
appropriate integer constant. However, the plot sickens: we
must also be able to handle things like 'ab\nd' (value = * "d\nba")
and 'abc' (vale = *"cba").
First we convert 'AB\nD' into the list [ 65 ; 66 ; 10 ; 68 ], then we
multiply and add to get the desired value.
*)
(* Given a character constant (like 'a' or 'abc') as a list of 64-bit
values, turn it into a CIL constant. Multi-character constants are
treated as multi-digit numbers with radix given by the bit width of
the specified type (either char or wchar_t). *)
let reduce_multichar typ =
let radix = bitsSizeOf typ in
List.fold_left
(fun acc v -> add_cilint (shift_left_cilint acc radix) @@ (cilint_of_int64 v))
zero_cilint
let interpret_character_constant char_list =
let value = reduce_multichar charType char_list in
if compare_cilint value (cilint_of_int 256) < 0 then
(* ISO C 6.4.4.4.10: single-character constants have type int *)
(CChr(Char.chr (cilint_to_int value))), intType
else begin
let orig_rep = None (* Some("'" ^ (String.escaped str) ^ "'") *) in
if compare_cilint value (cilint_of_int64 (Int64.of_int32 Int32.max_int)) <= 0 then
(CInt(value,IULong,orig_rep)),(TInt(IULong,[]))
else
(CInt(value,IULongLong,orig_rep)),(TInt(IULongLong,[])) (* 128bit constants are only supported if long long is also 128bit wide *)
end
(*** EXPRESSIONS *************)
(* We collect here the program *)
let theFile : global list ref = ref []
let theFileTypes : global list ref = ref []
let initGlobals () = theFile := []; theFileTypes := []
let cabsPushGlobal (g: global) =
pushGlobal g ~types:theFileTypes ~variables:theFile
(* Keep track of some variable ids that must be turned into definitions. We
do this when we encounter what appears a definition of a global but
without initializer. We leave it a declaration because maybe down the road
we see another definition with an initializer. But if we don't see any
then we turn the last such declaration into a definition without
initializer *)
let mustTurnIntoDef: bool IH.t = IH.create 117
(* Globals that have already been defined. Indexed by the variable name. *)
let alreadyDefined: (string, location) H.t = H.create 117
(* Globals that were created due to static local variables. We chose their
names to be distinct from any global encountered at the time. But we might
see a global with conflicting name later in the file. *)
let staticLocals: (string, varinfo) H.t = H.create 13
(* Typedefs. We chose their names to be distinct from any global encountered
at the time. But we might see a global with conflicting name later in the
file *)
let typedefs: (string, typeinfo) H.t = H.create 13
let popGlobals () =
let rec revonto (tail: global list) = function
[] -> tail
| GVarDecl (vi, l) :: rest
when vi.vstorage != Extern && IH.mem mustTurnIntoDef vi.vid ->
IH.remove mustTurnIntoDef vi.vid;
if vi.vinit.init != None then
E.s (E.bug "GVarDecl %s should have empty initializer" vi.vname);
revonto (GVar (vi, vi.vinit, l) :: tail) rest
| x :: rest -> revonto (x :: tail) rest
in
revonto (revonto [] !theFile) !theFileTypes
(* Like Cil.mkCastT, but it calls typeForInsertedCast *)
let makeCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) =
Cil.mkCastT ~e:e ~oldt:oldt ~newt:(!typeForInsertedCast newt)
let makeCast ~(e: exp) ~(newt: typ) =
makeCastT ~e:e ~oldt:(typeOf e) ~newt:newt
(********* ENVIRONMENTS ***************)
(* The environment is kept in two distinct data structures. A hash table maps
each original variable name into a varinfo (for variables, or an
enumeration tag, or a type). (Note that the varinfo might contain an
alpha-converted name different from that of the lookup name.) The Ocaml
hash tables can keep multiple mappings for a single key. Each time the
last mapping is returned and upon deletion the old mapping is restored. To
keep track of local scopes we also maintain a list of scopes (represented
as lists). *)
type envdata =
EnvVar of varinfo (* The name refers to a variable
(which could also be a function) *)
| EnvEnum of exp * typ (* The name refers to an enumeration
tag for which we know the value
and the host type *)
| EnvTyp of typ (* The name is of the form "struct
foo", or "union foo" or "enum foo"
and refers to a type. Note that
the name of the actual type might
be different from foo due to alpha
conversion *)
| EnvLabel of string (* The name refers to a label. This
is useful for GCC's locally
declared labels. The lookup name
for this category is "label foo" *)
let env : (string, envdata * location) H.t = H.create 307
(* Just like env, except that it simply collects all the information (i.e. entries
are never removed and it is also not emptied after every file). *)
let environment : (string, envdata * location) H.t = H.create 307
let genvironment : (string, envdata * location) H.t = H.create 307
(* We also keep a global environment. This is always a subset of the env *)
let genv : (string, envdata * location) H.t = H.create 307
(* In the scope we keep the original name, so we can remove them from the
hash table easily *)
type undoScope =
UndoRemoveFromEnv of string
| UndoResetAlphaCounter of location AL.alphaTableData ref *
location AL.alphaTableData
| UndoRemoveFromAlphaTable of string
let scopes : undoScope list ref list ref = ref []
(* When you add to env, you also add it to the current scope *)
let addLocalToEnv (n: string) (d: envdata) =
(* ignore (E.log "%a: adding local %s to env\n" d_loc !currentLoc n); *)
H.add env n (d, !currentLoc);
H.add environment n (d, !currentLoc);
(* If we are in a scope, then it means we are not at top level. Add the
name to the scope *)
(match !scopes with
[] -> begin
match d with
EnvVar _ ->
E.s (E.bug "addLocalToEnv: not in a scope when adding %s!" n)
| _ -> () (* We might add types *)
end
| s :: _ ->
s := (UndoRemoveFromEnv n) :: !s)
let addGlobalToEnv (k: string) (d: envdata) : unit =
(* ignore (E.log "%a: adding global %s to env\n" d_loc !currentLoc k); *)
H.add env k (d, !currentLoc);
H.add environment k (d, !currentLoc);
(* Also add it to the global environment *)
H.add genv k (d, !currentLoc);
H.add genvironment k (d, !currentLoc)
(* Create a new name based on a given name. The new name is formed from a
prefix (obtained from the given name as the longest prefix that ends with
a non-digit), followed by a '_' and then by a positive integer suffix. The
first argument is a table mapping name prefixes with the largest suffix
used so far for that prefix. The largest suffix is one when only the
version without suffix has been used. *)
let alphaTable : (string, location AL.alphaTableData ref) H.t = H.create 307
(* vars and enum tags. For composite types we have names like "struct
foo" or "union bar" *)
(* To keep different name scopes different, we add prefixes to names
specifying the kind of name: the kind can be one of "" for variables or
enum tags, "struct" for structures and unions (they share the name space),
"enum" for enumerations, or "type" for types *)
let kindPlusName (kind: string)
(origname: string) : string =
if kind = "" then origname else
kind ^ " " ^ origname
let stripKind (kind: string) (kindplusname: string) : string =
let l = 1 + String.length kind in
if l > 1 then
String.sub kindplusname l (String.length kindplusname - l)
else
kindplusname
let newAlphaName (globalscope: bool) (* The name should have global scope *)
(kind: string)
(origname: string) : string * location =
let lookupname = kindPlusName kind origname in
(* If we are in a scope then it means that we are alpha-converting a local
name. Go and add stuff to reset the state of the alpha table but only to
the top-most scope (that of the enclosing function) *)
let rec findEnclosingFun = function
[] -> (* At global scope *)()
| [s] -> begin
let prefix = AL.getAlphaPrefix ~lookupname:lookupname in
try
let countref = H.find alphaTable prefix in
s := (UndoResetAlphaCounter (countref, !countref)) :: !s
with Not_found ->
s := (UndoRemoveFromAlphaTable prefix) :: !s
end
| _ :: rest -> findEnclosingFun rest
in
if not globalscope then
findEnclosingFun !scopes;
let newname, oldloc =
AL.newAlphaName ~alphaTable:alphaTable ~undolist:None ~lookupname:lookupname ~data:!currentLoc in
stripKind kind newname, oldloc
(*** In order to process GNU_BODY expressions we must record that a given
*** COMPUTATION is interesting *)
let gnu_body_result : (A.statement * ((exp * typ) option ref)) ref
= ref (A.NOP cabslu, ref None)
(*** When we do statements we need to know the current return type *)
let currentReturnType : typ ref = ref (TVoid([]))
let currentFunctionFDEC: fundec ref = ref dummyFunDec
(* Generate unique ids for structs, with a best-effort to base them on the
structure of the type, so that the same anonymous struct in different
compilation units gets the same name - this is important to preserve
compatible types. This is not bullet-proof because we do not
normalize the context at all. *)
let structIds = ref []
let newStructId id =
assert(id >= 0);
let rec find_fresh id max_id = function
| [] -> id
| x :: xs ->
let max' = max x max_id in
find_fresh (if id = x then max' + 1 else id) max' xs in
let id' = find_fresh id (-1) !structIds in
assert(id' >= 0);
assert(List.for_all ((<>) id') !structIds);
structIds := id' :: !structIds ;
id'
let anonStructName (k: string) (suggested: string) (context: 'a) =
let id = newStructId (Hashtbl.hash_param 100 1000 context) in
"__anon" ^ k ^ (if suggested <> "" then "_" ^ suggested else "")
^ "_" ^ (string_of_int id)
let constrExprId = ref 0
let startFile () =
H.clear env;
H.clear genv;
H.clear alphaTable;
structIds := [];
constrExprId := 0
let enterScope () =
scopes := (ref []) :: !scopes
(* Exit a scope and clean the environment. We do not yet delete from
the name table *)
let exitScope () =
let this, rest =
match !scopes with
car :: cdr -> car, cdr
| [] -> E.s (error "Not in a scope")
in
scopes := rest;
let rec loop = function
[] -> ()
| UndoRemoveFromEnv n :: t ->
H.remove env n; loop t
| UndoRemoveFromAlphaTable n :: t -> H.remove alphaTable n; loop t
| UndoResetAlphaCounter (vref, oldv) :: t ->
vref := oldv;
loop t
in
loop !this
(* Lookup a variable name. Return also the location of the definition. Might
raise Not_found *)
let lookupVar (n: string) : varinfo * location =
match H.find env n with
(EnvVar vi), loc -> vi, loc
| _ -> raise Not_found
let lookupGlobalVar (n: string) : varinfo * location =
match H.find genv n with
(EnvVar vi), loc -> vi, loc
| _ -> raise Not_found
(* Add a new variable. Do alpha-conversion if necessary *)
let alphaConvertVarAndAddToEnv (addtoenv: bool) (vi: varinfo) : varinfo =
(*
ignore (E.log "%t: alphaConvert(addtoenv=%b) %s" d_thisloc addtoenv vi.vname);
*)
(* Announce the name to the alpha conversion table *)
let newname, oldloc = newAlphaName (addtoenv && vi.vglob) "" vi.vname in
(* Make a copy of the vi if the name has changed. Never change the name for
global variables *)
let newvi =
if vi.vname = newname then
vi
else begin
if vi.vglob then begin
(* Perhaps this is because we have seen a static local which happened
to get the name that we later want to use for a global. *)
try
let static_local_vi = H.find staticLocals vi.vname in
H.remove staticLocals vi.vname;
(* Use the new name for the static local *)
static_local_vi.vname <- newname;
(* And continue using the last one *)
vi
with Not_found -> begin
(* Or perhaps we have seen a typedef which stole our name. This is
possible because typedefs use the same name space *)
try
let typedef_ti = H.find typedefs vi.vname in
H.remove typedefs vi.vname;
(* Use the new name for the typedef instead *)
typedef_ti.tname <- newname;
(* And continue using the last name *)
vi
with Not_found ->
E.s (E.error "It seems that we would need to rename global %s (to %s) because of previous occurrence at %a"
vi.vname newname d_loc oldloc);
end
end else begin
(* We have changed the name of a local variable. Can we try to detect
if the other variable was also local in the same scope? Not for
now. *)
copyVarinfo vi newname
end
end
in
(* Store all locals in the slocals (in reversed order). We'll reverse them
and take out the formals at the end of the function *)
if not vi.vglob then (
(if !addNestedScopeAttr then
(* two scopes implies top-level scope in the function, one is created for the FUNDEF (includes formals etc),
one for the body which is a block *)
match !scopes with
| _::_::_::_ ->
(* i.e. List.length scopes > 2 *)
newvi.vattr <- Attr("goblint_cil_nested", []) :: newvi.vattr
| _ -> ()
);
!currentFunctionFDEC.slocals <- newvi :: !currentFunctionFDEC.slocals
)
;
(if addtoenv then
if vi.vglob then
addGlobalToEnv vi.vname (EnvVar newvi)
else
addLocalToEnv vi.vname (EnvVar newvi));
(*
ignore (E.log " new=%s\n" newvi.vname);
*)
(* ignore (E.log "After adding %s alpha table is: %a\n"
newvi.vname docAlphaTable alphaTable); *)
newvi
(* Strip the "const" from the type. It is unfortunate that const variables
can only be set in initialization. Once we decided to move all
declarations to the top of the functions, we have no way of setting a
"const" variable. Furthermore, if the type of the variable is an array or
a struct we must recursively strip the "const" from fields and array
elements. *)
let rec stripConstLocalType (t: typ) : typ =
let dc = dropAttribute "pconst" in
match t with
| TPtr (bt, a) ->
(* We want to be able to detect by pointer equality if the type has
changed. So, don't realloc the type unless necessary. *)
let a' = dc a in if a != a' then TPtr(bt, a') else t
| TInt (ik, a) ->
let a' = dc a in if a != a' then TInt(ik, a') else t
| TFloat(fk, a) ->
let a' = dc a in if a != a' then TFloat(fk, a') else t
| TNamed (ti, a) ->
(* We must go and drop the consts from the typeinfo as well ! *)
let t' = stripConstLocalType ti.ttype in
if t != t' then begin
(* ignore (warn "Stripping \"const\" from typedef %s" ti.tname); *)
ti.ttype <- t'
end;
let a' = dc a in if a != a' then TNamed(ti, a') else t
| TEnum (ei, a) ->
let a' = dc a in if a != a' then TEnum(ei, a') else t
| TArray(bt, leno, a) ->
(* We never assign to the array. So, no need to change the const. But
we must change it on the base type *)
let bt' = stripConstLocalType bt in
if bt' != bt then TArray(bt', leno, a) else t
| TComp(ci, a) ->
(* Must change both this structure as well as its fields *)
List.iter
(fun f ->
let t' = stripConstLocalType f.ftype in
if t' != f.ftype then begin
ignore (warnOpt "Stripping \"const\" from field %s of %s"
f.fname (compFullName ci));
f.ftype <- t'
end)
ci.cfields;
let a' = dc a in if a != a' then TComp(ci, a') else t
(* We never assign functions either *)
| TFun(rt, args, va, a) -> t
| TVoid a ->
let a' = dc a in if a != a' then TVoid a' else t
| TBuiltin_va_list a ->
let a' = dc a in if a != a' then TBuiltin_va_list a' else t
let constFoldTypeVisitor = object (self)
inherit nopCilVisitor
method! vtype t: typ visitAction =
match t with
TArray(bt, Some len, a) ->
let len' = constFold true len in
ChangeDoChildrenPost (
TArray(bt, Some len', a),
(fun x -> x)
)
| _ -> DoChildren
end
(* Const-fold any expressions that appear as array lengths in this type *)
let constFoldType (t:typ) : typ =
visitCilType constFoldTypeVisitor t
let typeSigNoAttrs: typ -> typsig = typeSigWithAttrs (fun _ -> [])
(* Create a new temporary variable *)
let newTempVar (descr:doc) (descrpure:bool) typ =
if !currentFunctionFDEC == dummyFunDec then
E.s (bug "newTempVar called outside a function");
(* ignore (E.log "stripConstLocalType(%a) for temporary\n" d_type typ); *)
let t' = (!typeForInsertedVar) (stripConstLocalType typ) in
(* Start with the name "tmp". The alpha converter will fix it *)
let vi = makeVarinfo false "tmp" t' in
vi.vdescr <- descr;
vi.vdescrpure <- descrpure;
alphaConvertVarAndAddToEnv false vi (* Do not add to the environment *)
(*
{ vname = "tmp"; (* addNewVar will make the name fresh *)
vid = newVarId "tmp" false;
vglob = false;
vtype = t';
vdecl = locUnknown;
vinline = false;
vattr = [];
vaddrof = false;
vreferenced = false; (* sm *)
vstorage = NoStorage;
}
*)
let mkAddrOfAndMark ((b, off) as lval) : exp =
(* Mark the vaddrof flag if b is a variable *)
(match b with
Var vi -> vi.vaddrof <- true
| _ -> ());
mkAddrOf lval
(* Call only on arrays *)
let mkStartOfAndMark ((b, off) as lval) : exp =
(* Mark the vaddrof flag if b is a variable *)
(match b with
Var vi -> vi.vaddrof <- true
| _ -> ());
let res = StartOf lval in
res
(* Keep a set of self compinfo for composite types *)
let compInfoNameEnv : (string, compinfo) H.t = H.create 113
let enumInfoNameEnv : (string, enuminfo) H.t = H.create 113
let lookupTypeNoError (kind: string)
(n: string) : typ * location =
let kn = kindPlusName kind n in
match H.find env kn with
EnvTyp t, l -> t, l
| _ -> raise Not_found
let lookupType (kind: string)
(n: string) : (typ * location) option =
try
Some (lookupTypeNoError kind n)
with Not_found -> None
(* E.s (error "Cannot find type %s (kind:%s)" n kind) *)
(* Create the self ref cell and add it to the map. Return also an indication
if this is a new one. *)
let createCompInfo (iss: bool) (n: string) : compinfo * bool =
(* Add to the self cell set *)
let key = (if iss then "struct " else "union ") ^ n in
try
H.find compInfoNameEnv key, false (* Only if not already in *)
with Not_found -> begin
(* Create a compinfo. This will have "cdefined" false. *)
let res = mkCompInfo iss n (fun _ -> []) [] in
H.add compInfoNameEnv key res;
res, true
end
(* Create the self ref cell and add it to the map. Return an indication
whether this is a new one. *)
let createEnumInfo (n: string) : enuminfo * bool =
(* Add to the self cell set *)
try
H.find enumInfoNameEnv n, false (* Only if not already in *)
with Not_found -> begin
(* Create a enuminfo *)
let enum = { ename = n; eitems = [];
eattr = []; ereferenced = false; ekind = IInt; } in
H.add enumInfoNameEnv n enum;
enum, true
end
(* kind is either "struct" or "union" or "enum" and n is a name *)
let findCompType (kind: string) (n: string) (a: attributes) =
let makeForward () =
(* This is a forward reference, either because we have not seen this
struct already or because we want to create a version with different
attributes *)
if kind = "enum" then
let enum, isnew = createEnumInfo n in
if isnew then
cabsPushGlobal (GEnumTagDecl (enum, !currentLoc));
TEnum (enum, a)
else
let iss = if kind = "struct" then true else false in
let self, isnew = createCompInfo iss n in
if isnew then
cabsPushGlobal (GCompTagDecl (self, !currentLoc));
TComp (self, a)
in
try
let old, _ = lookupTypeNoError kind n in (* already defined *)
let olda = typeAttrs old in
if Util.equals olda a then old else makeForward ()
with Not_found -> makeForward ()
(* A simple visitor that searchs a statement for labels *)
class canDropStmtClass pRes = object
inherit nopCilVisitor
method! vstmt s =
if s.labels != [] then
(pRes := false; SkipChildren)
else
if !pRes then DoChildren else SkipChildren
method! vinst _ = SkipChildren
method! vexpr _ = SkipChildren
end
let canDropStatement (s: stmt) : bool =
let pRes = ref true in
let vis = new canDropStmtClass pRes in
ignore (visitCilStmt vis s);
!pRes
(**** Occasionally we see structs with no name and no fields *)
module BlockChunk =
struct
type chunk = {
stmts: stmt list;
postins: instr list; (* Some instructions to append at
the ends of statements (in
reverse order) *)
cases: stmt list; (* A list of case statements
(statements with Case labels)
visible at the outer level *)
}
let d_chunk () (c: chunk) =
dprintf "@[{ @[%a@] };@?%a@]"
(docList ~sep:(chr ';') (d_stmt ())) c.stmts
(docList ~sep:(chr ';') (d_instr ())) (List.rev c.postins)
let empty =
{ stmts = []; postins = []; cases = []; }
let isEmpty (c: chunk) =
c.postins == [] && c.stmts == []
let isNotEmpty (c: chunk) = not (isEmpty c)
module SynthetizeLoc =
struct
let doLoc l =
(* ignore (Pretty.eprintf "synthesizeLoc %a in %a\n" d_loc l d_chunk c); *)
{l with synthetic = true}
let doInstr: instr -> instr = function
| Set (l, e, loc, eloc) -> Set (l, e, doLoc loc, doLoc eloc)
| VarDecl (v, loc) -> VarDecl (v, doLoc loc)
| Call (l, f, a, loc, eloc) -> Call (l, f, a, doLoc loc, doLoc eloc)
| Asm (a, b, c, d, e, loc) -> Asm (a, b, c, d, e, doLoc loc)
(** Change all stmt and instr locs to synthetic, except the first one.
Expressions/initializers that expand to multiple instructions cannot have intermediate locations referenced. *)
let doChunkTail (c: chunk): chunk =
(* ignore (Pretty.eprintf "synthesizeLocs %a\n" d_chunk c); *)
let doInstrs ~first = function
| [] -> []
| x :: xs when first -> x :: List.map doInstr xs
| xs -> List.map doInstr xs
in
(* must mutate stmts in order to not break refs (for gotos) *)
let rec doStmt ~first s: unit =
let doLoc = if first then fun x -> x else doLoc in
s.skind <- match s.skind with
| Instr xs -> Instr (doInstrs ~first xs)
| Return (e, loc, eloc) -> Return (e, doLoc loc, doLoc eloc)
| Goto (s, loc) -> Goto (s, doLoc loc)
| ComputedGoto (e, loc) -> ComputedGoto (e, doLoc loc)
| Break loc -> Break (doLoc loc)
| Continue loc -> Continue (doLoc loc)
| If (c, t, f, loc, eloc) ->
doBlock ~first:false t;
doBlock ~first:false f;
If (c, t, f, doLoc loc, doLoc eloc)
| Switch (e, b, s, loc, eloc) ->
doBlock ~first:false b;
doStmts ~first:false s;
Switch (e, b, s, doLoc loc, doLoc eloc)
| Loop (b, loc, eloc, s1, s2) ->
doBlock ~first:false b;
let option_iter f = function Some v -> f v | None -> () in (* Option.iter for older OCaml versions *)
option_iter (doStmt ~first:false) s1;
option_iter (doStmt ~first:false) s2;
Loop (b, doLoc loc, doLoc eloc, s1, s2)
| Block b ->
doBlock ~first b;
s.skind
and doBlock ~first b =
doStmts ~first b.bstmts
and doStmts ~first = function
| [] -> ()
| x :: xs ->
doStmt ~first x;
List.iter (doStmt ~first:false) xs
in
match c.stmts, c.postins with
| [], [] -> c
| [], postins -> {c with postins = List.rev (doInstrs ~first:true (List.rev postins))}
| stmts, postins ->
doStmts ~first:true stmts;
{c with postins = List.rev (doInstrs ~first:false (List.rev postins))}
(** Change first stmt or instr loc to synthetic. *)
let doChunkHead (c: chunk): chunk =
(* ignore (Pretty.eprintf "synthesizeFirstLoc %a\n" d_chunk c); *)
let doInstrs = function
| [] -> []
| x :: xs -> doInstr x :: xs
in
(* must mutate stmts in order to not break refs (for gotos) *)
let rec doStmt s: unit =
s.skind <- match s.skind with
| Instr xs -> Instr (doInstrs xs)
| Return (e, loc, eloc) -> Return (e, doLoc loc, doLoc eloc)
| Goto (s, loc) -> Goto (s, doLoc loc)
| ComputedGoto (e, loc) -> ComputedGoto (e, doLoc loc)
| Break loc -> Break (doLoc loc)
| Continue loc -> Continue (doLoc loc)
| If _
| Switch _
| Loop _ ->
s.skind
| Block b ->
doBlock b;
s.skind
and doBlock b =
doStmts b.bstmts
and doStmts = function
| [] -> ()
| x :: xs ->
doStmt x
in
match c.stmts, c.postins with
| [], [] -> c
| [], postins -> {c with postins = List.rev (doInstrs (List.rev postins))}
| stmts, postins ->
doStmts stmts;
c
let eDoInstr: instr -> instr = function
| Set (l, e, loc, eloc) -> Set (l, e, loc, doLoc eloc)
| VarDecl (v, loc) -> VarDecl (v, loc)
| Call (l, f, a, loc, eloc) -> Call (l, f, a, loc, doLoc eloc)
| Asm (a, b, c, d, e, loc) -> Asm (a, b, c, d, e, loc)
(** Change first stmt or instr eloc to synthetic. *)
let eDoChunkHead (c: chunk): chunk =
(* ignore (Pretty.eprintf "synthesizeFirstLoc %a\n" d_chunk c); *)
let doInstrs = function
| [] -> []
| x :: xs -> eDoInstr x :: xs
in
(* must mutate stmts in order to not break refs (for gotos) *)
let rec doStmt s: unit =
s.skind <- match s.skind with
| Instr xs -> Instr (doInstrs xs)
| Return (e, loc, eloc) -> Return (e, loc, doLoc eloc)
| Goto (s, loc) -> Goto (s, doLoc loc)
| ComputedGoto (e, loc) -> ComputedGoto (e, doLoc loc)
| Break loc -> Break (doLoc loc)
| Continue loc -> Continue (doLoc loc)
| If _
| Switch _
| Loop _ ->
s.skind
| Block b ->
doBlock b;
s.skind
and doBlock b =
doStmts b.bstmts
and doStmts = function
| [] -> ()
| x :: xs ->
doStmt x
in
match c.stmts, c.postins with
| [], [] -> c
| [], postins -> {c with postins = List.rev (doInstrs (List.rev postins))}
| stmts, postins ->
doStmts stmts;
c
end
let i2c (i: instr) =
{ empty with postins = [i] }
(* Occasionally, we'll have to push postins into the statements *)
let pushPostIns (c: chunk) : stmt list =
if c.postins = [] then c.stmts
else
let rec toLast = function
[{skind=Instr il; _} as s] as stmts ->
s.skind <- Instr (il @ (List.rev c.postins));
stmts
| [] -> [mkStmt (Instr (List.rev c.postins))]
| a :: rest -> a :: toLast rest
in
compactStmts (toLast c.stmts)