1 (**************************************************************************)
3 (* This file is part of WP plug-in of Frama-C. *)
5 (* Copyright (C) 2007-2011 *)
6 (* CEA (Commissariat a l'énergie atomique et aux énergies *)
9 (* you can redistribute it and/or modify it under the terms of the GNU *)
10 (* Lesser General Public License as published by the Free Software *)
11 (* Foundation, version 2.1. *)
13 (* It is distributed in the hope that it will be useful, *)
14 (* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
15 (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
16 (* GNU Lesser General Public License for more details. *)
18 (* See the GNU Lesser General Public License version 2.1 *)
19 (* for more details (enclosed in the file licenses/LGPLv2.1). *)
21 (**************************************************************************)
26 (** Copied from clabels.ml *)
27 (*TODO [LC] : Use extension of Clabels instead *)
28 let mk_logic_label s =
29 LogicLabel (Some s, "cost!stmt_"^(string_of_int s.sid))
32 type label_mapping = Cil_types.logic_label -> Cil_types.logic_label
35 (** push the Tat down to the 'data' operations.
36 * This can be useful in cases like \at (x + \at(y, Ly), Lx) because
37 * it gives \at(x, Lx) + \at(y, Ly) so there is no more \at imbrications.
38 * Also try to "normalize" label :
39 * - remove Here because its meaning change when propagating,
40 * - remove Old because its meaning depend on where it comes from.
42 class norm_at label_map = object(self)
43 inherit Visitor.generic_frama_c_visitor (Project.current()) (Cil.copy_visit())
45 val mutable current_label = None
47 method private change_label label =
48 let label = label_map label in
49 let old_label = current_label in
50 current_label <- Some label; old_label
52 method private restore_term old_label x =
53 current_label <- old_label;
54 let x = match x.term_node with
55 | Ttypeof x -> (* Ttypeof is used as a dummy unary construct *) x
59 method private restore_pred old_label x =
60 current_label <- old_label;
61 let x = match x.content with
62 | Pnot x -> (* Pnot is used as a dummy unary construct *) x
68 match t.term_node with
70 let old_label = self#change_label l in
71 let new_t = {t with term_node = Ttypeof t} in
72 Cil.ChangeDoChildrenPost (new_t, self#restore_term old_label)
73 | TAddrOf (h, _) | TLval (h, _) | TStartOf (h, _) ->
74 let old_label = current_label in
75 let at_label = match h with
76 | TResult _ -> Some Logic_const.post_label
79 current_label <- None;
81 current_label <- old_label;
83 | Some label -> {t with term_node = Tat (t, label)}
85 in Cil.ChangeDoChildrenPost (t, post)
86 (** logic function without label *)
87 | Tapp ({l_labels=[]},[],_) -> Cil.DoChildren
89 begin match current_label with
90 | None -> Cil.DoChildren
93 | {term_node=Tapp(predicate,[],args)} as t ->
94 { t with term_node=Tapp(predicate,[lab,lab],args) }
97 Cil.ChangeDoChildrenPost (t,post)
101 | {term_node=Tapp(predicate,labels,args)} as t ->
104 (fun (logic_lab, stmt_lab) -> logic_lab, label_map stmt_lab)
106 in { t with term_node=Tapp(predicate,new_labels,args) }
109 Cil.ChangeDoChildrenPost (t,post)
110 | _ -> Cil.DoChildren
112 method vpredicate_named p = match p.content with
114 let old_label = self#change_label l in
115 let new_p = {p with content = Pnot p} in
116 Cil.ChangeDoChildrenPost (new_p, self#restore_pred old_label)
117 (** logic function without label *)
118 | Papp ({l_labels=[]},[],_) -> Cil.DoChildren
120 begin match current_label with
121 | None -> Cil.DoChildren
124 | {content=Papp(predicate,[],args)} as p ->
125 { p with content=Papp(predicate,[lab,lab],args) }
128 Cil.ChangeDoChildrenPost (p,post)
132 | {content=Papp(predicate,labels,args)} as p ->
135 (fun (logic,stmt) -> logic, label_map stmt)
137 in { p with content=Papp(predicate,new_labels,args) }
140 Cil.ChangeDoChildrenPost (p,post)
141 | _ -> Cil.DoChildren
144 exception LabelError of logic_label
146 let labels_empty l = raise (LabelError l)
148 (* -------------------------------------------------------------------------- *)
149 (* --- Function Contracts --- *)
150 (* -------------------------------------------------------------------------- *)
152 let labels_fct_pre = function
153 | LogicLabel (None, ("Pre" | "Here")) -> Logic_const.pre_label
154 | l -> raise (LabelError l)
157 let labels_fct_post = function
158 | LogicLabel (None, ("Pre" | "Old")) -> Logic_const.pre_label
159 | LogicLabel (None, ("Post" | "Here")) -> Logic_const.post_label
160 | l -> raise (LabelError l)
162 let labels_fct_assigns = function
163 | LogicLabel (None, "Post") -> Logic_const.post_label
164 | LogicLabel (None, ("Pre" | "Old")) -> Logic_const.pre_label
165 | l -> raise (LabelError l)
167 (* -------------------------------------------------------------------------- *)
168 (* --- Statements Contracts --- *)
169 (* -------------------------------------------------------------------------- *)
170 let labels_stmt_pre s = function
171 | LogicLabel (None, "Pre") -> Logic_const.pre_label (* fct pre-state *)
172 | LogicLabel (None, "Here") -> mk_logic_label s
173 | LogicLabel (Some s, _) -> mk_logic_label s
174 | StmtLabel rs -> mk_logic_label !rs
175 | l -> raise (LabelError l)
177 let labels_stmt_post s l_post = function
178 | LogicLabel (None, "Pre") -> Logic_const.pre_label (* fct pre-state *)
179 | LogicLabel (None, "Old") -> mk_logic_label s (* contract pre-state *)
180 | LogicLabel (None, ("Here" | "Post")) as l ->
181 begin match l_post with Some l -> l
182 | None -> (* TODO ? *) raise (LabelError l)
184 | LogicLabel (Some s, _) -> mk_logic_label s
185 | StmtLabel rs -> mk_logic_label !rs
186 | l -> raise (LabelError l)
188 let labels_stmt_assigns s l_post = function
189 | LogicLabel (None, "Pre") -> Logic_const.pre_label (* fct pre-state *)
190 | LogicLabel (None, ("Here" | "Old")) -> (* contract pre-state *)
192 | LogicLabel (None, "Post") -> labels_stmt_post s l_post Logic_const.post_label
193 | LogicLabel (Some s, _) -> mk_logic_label s
194 | StmtLabel rs -> mk_logic_label !rs
195 | l -> raise (LabelError l)
197 (* -------------------------------------------------------------------------- *)
198 (* --- User Assertions in Functions Code --- *)
199 (* -------------------------------------------------------------------------- *)
201 let labels_assert_before s = function
202 | LogicLabel (None, "Pre") -> Logic_const.pre_label
203 | LogicLabel (None, "Here") -> mk_logic_label s
204 | LogicLabel (Some s, _) -> mk_logic_label s
205 | StmtLabel rs -> mk_logic_label !rs
206 | l -> raise (LabelError l)
208 let labels_assert_after s l_post = function
209 | LogicLabel (None, "Pre") -> Logic_const.pre_label
210 | LogicLabel (None, "Here") ->
211 labels_stmt_post s l_post Logic_const.post_label
212 | LogicLabel (Some s, _) -> mk_logic_label s
213 | StmtLabel rs -> mk_logic_label !rs
214 | l -> raise (LabelError l)
216 let labels_loop_inv _s = function
217 | LogicLabel (None, "Pre") -> Logic_const.pre_label
218 | LogicLabel (None, "Here") -> Logic_const.here_label
219 | LogicLabel (None, ("Old" | "Post")) as l -> raise (LabelError l)
222 let labels_loop_assigns s l = labels_loop_inv s l
224 (* -------------------------------------------------------------------------- *)
225 (* --- User Defined Predicates --- *)
226 (* -------------------------------------------------------------------------- *)
228 let labels_predicate lab_pairs = fun l ->
229 try List.assoc l lab_pairs
232 let labels_axiom = function
233 | LogicLabel (None, ("Pre"|"Old"|"Post")) as l -> raise (LabelError l)
234 | LogicLabel (None, _) as l -> l
235 | l -> raise (LabelError l)
237 (* -------------------------------------------------------------------------- *)
238 (* --- Apply Normalization --- *)
239 (* -------------------------------------------------------------------------- *)
241 (** @raise LabelError if there is a label in [p] that is incompatible
242 * with the [labels] translation *)
243 let preproc_annot labels p =
244 let visitor = new norm_at labels in
245 Visitor.visitFramacPredicateNamed visitor p
247 let preproc_annot_term labels t =
248 let visitor = new norm_at labels in
249 Visitor.visitFramacTerm visitor t
252 (** @raise LabelError if there is a label in [p] that is incompatible
253 * with the [labels] translation *)
254 let preproc_assigns labels asgns =
255 let visitor = new norm_at labels in
256 List.map (Visitor.visitFramacFrom visitor) asgns
258 let preproc_label labels l = labels l