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
open Cil_types
open Instantiator_builder
let base : (string, (module Instantiator)) Hashtbl.t = Hashtbl.create 17
let register (module G: Generator_sig) =
let module Instantiator = Make_instantiator(G) in
Hashtbl.add base G.function_name (module Instantiator)
let get_kfs () =
let get_kfs _ instantiator =
let module I = (val instantiator: Instantiator) in
let res = I.get_kfs () in
res
in
Hashtbl.fold (fun k v l -> (get_kfs k v) @ l) base []
let clear () =
Global_context.clear () ;
let clear _ instantiator =
let module I = (val instantiator: Instantiator) in
I.clear ()
in
Hashtbl.iter clear base
module VISet = Cil_datatype.Varinfo.Hptset
class transformer = object(self)
inherit Visitor.frama_c_inplace
val introduced_instantiators = ref VISet.empty
val used_instantiator_last_kf = Queue.create ()
method! vfile _ =
let post f =
f.globals <- (Global_context.globals (Current_loc.get())) @ f.globals ;
Ast.mark_as_changed () ;
Ast.mark_as_grown () ;
f
in
Cil.DoChildrenPost post
method! vglob_aux _ =
let post g =
let loc = Current_loc.get() in
let folding l fd =
if VISet.mem fd.svar !introduced_instantiators then l
else begin
introduced_instantiators := VISet.add fd.svar !introduced_instantiators ;
GFun (fd, loc) :: l
end
in
Queue.fold folding g used_instantiator_last_kf
in
Cil.DoChildrenPost post
method! vfunc f =
let kf = Globals.Functions.get f.svar in
if not (Options.Kfs.is_set ()) || Options.Kfs.mem kf then
Cil.DoChildren
else
Cil.SkipChildren
method private find_enabled_instantiator fct =
let instantiator = Hashtbl.find base fct.vname in
let module I = (val instantiator: Instantiator) in
if not (I.Enabled.get ()) then raise Not_found ;
instantiator
method private replace_call (lval, fct, args) =
try
let module I = (val (self#find_enabled_instantiator fct): Instantiator) in
if I.well_typed_call lval fct args then
let key = I.key_from_call lval fct args in
let fundec = I.get_override key in
let new_args = I.retype_args key args in
Queue.add fundec used_instantiator_last_kf ;
(fundec.svar), new_args
else begin
Options.warning
~current:true "%s instantiator cannot replace call" fct.vname ;
(fct, args)
end
with
| Not_found -> (fct, args)
method! vinst = function
| Call(_, Var _, _, _)
| Local_init(_, ConsInit(_ , _, Plain_func), _) ->
let change = function
| [ Call(r, Var f, args, loc) ] ->
let f, args = self#replace_call (r, f, args) in
[ Call(r, Var f, args, loc) ]
| [ Local_init(r, ConsInit(f, args, Plain_func), loc) ] ->
let f, args = self#replace_call (Some (Cil.var r), f, args) in
[ Local_init(r, ConsInit(f, args, Plain_func), loc) ]
| _ -> assert false
in
Cil.DoChildrenPost change
| _ -> Cil.DoChildren
end
let validate_property p =
Property_status.emit Options.emitter ~hyps:[] p Property_status.True
let compute_call_preconditions_statuses kf =
let stmt = Kernel_function.find_first_stmt kf in
let _ = Kernel_function.find_all_enclosing_blocks stmt in
match stmt.skind with
| Instr (Local_init(_, ConsInit(fct, _, Plain_func), _))
| Instr (Call(_, Var fct, _, _)) ->
let called_kf = Globals.Functions.get fct in
Statuses_by_call.setup_all_preconditions_proxies called_kf ;
let reqs = Statuses_by_call.all_call_preconditions_at
~warn_missing:true called_kf stmt
in
List.iter (fun (_, p) -> validate_property p) reqs ;
| _ ->
Options.fatal "Transformation: unexpected instruction kind on precondition"
let compute_postconditions_statuses kf =
let posts bhv =
List.iter validate_property
(Property.ip_post_cond_of_behavior kf ~active:[] Kglobal bhv)
in
Annotations.iter_behaviors posts kf
let compute_comp_disj_statuses kf =
let open Property in
let comps c = validate_property (ip_of_complete kf Kglobal ~active:[] c) in
let disjs d = validate_property (ip_of_disjoint kf Kglobal ~active:[] d) in
Annotations.iter_complete (fun _ -> comps) kf ;
Annotations.iter_disjoint (fun _ -> disjs) kf
let compute_statuses_all_kfs () =
let kfs = get_kfs () in
List.iter compute_call_preconditions_statuses kfs ;
List.iter compute_postconditions_statuses kfs ;
List.iter compute_comp_disj_statuses kfs
let transform file =
clear () ;
Visitor.visitFramacFile (new transformer) file ;
File.reorder_ast () ;
compute_statuses_all_kfs ()