1 (** This module gives utility functions for creating terms and
6 module Varinfo = Cil_datatype.Varinfo
7 module Stmt = Cil_datatype.Stmt
8 module Term = Cil_datatype.Term
9 module Logic_label = Cil_datatype.Logic_label
11 (** {Add needed logic function} *)
13 let get_max_logic_info, add_def_max_logic_info =
14 (* TODO the name can collide with other logic function *)
15 let module M = State_builder.Option_ref(Cil_datatype.Logic_info)
17 let name = "max_logic_fun"
18 let dependencies = [Annotations.self]
22 let x = Cil_const.make_logic_var "x" Linteger in
23 let y = Cil_const.make_logic_var "y" Linteger in
24 let tx = Logic_const.tvar x in let ty = Logic_const.tvar y in
26 let cond = Logic_const.term (TBinOp (Gt,tx,ty)) Linteger in
27 let term = Logic_const.term (Tif (cond,tx,ty)) Linteger in
29 let signature = Larrow ([Linteger;Linteger],Linteger) in
30 let li = { l_var_info = Cil_const.make_logic_var "__max" signature;
33 l_type = Some Linteger;
35 l_body = LBterm body } in
38 (fun () -> M.memo create),
40 match M.get_option () with
43 Globals.Annotations.add_generated
44 (Dfun_or_pred (li, Cil_datatype.Location.unknown)))
47 (** {2 Simplify casts} *)
48 (** Casts may get in the way when looking for a loop counter, just remove
51 let rec remove_casts e = match e.enode with
53 { e with enode = Lval (remove_casts_lval lval) }
55 { e with enode = SizeOfE (remove_casts e) }
57 { e with enode = AlignOfE (remove_casts e) }
58 | UnOp (unop, e, typ) ->
59 { e with enode = UnOp (unop, remove_casts e, typ) }
60 | BinOp (binop, e1, e2, typ) ->
62 BinOp (binop, remove_casts e1, remove_casts e2, typ) in
64 | CastE (_, e) -> remove_casts e
66 { e with enode = AddrOf (remove_casts_lval lval) }
68 { e with enode = StartOf (remove_casts_lval lval) }
70 { e with enode = Info (remove_casts e, info) }
73 and remove_casts_lval (lhost, offset) =
74 (remove_casts_lhost lhost, remove_casts_offset offset)
76 and remove_casts_lhost = function
77 | Mem e -> Mem (remove_casts e)
80 and remove_casts_offset = function
81 | Field (fieldinfo, offset) ->
82 Field (fieldinfo, remove_casts_offset offset)
83 | Index (e, offset) ->
84 Index (remove_casts e, remove_casts_offset offset)
88 (** {2 Simplify and convert terms} *)
92 exception Untranslatable_expr of exp
94 let print_exception_raise fmt = function
95 | Untranslatable_expr exp ->
96 Format.fprintf fmt "Can't convert exp %a to term.@."
97 Cil.defaultCilPrinter#pExp exp;
100 let print_exception fmt exn =
102 print_exception_raise fmt exn
103 with _ -> Format.fprintf fmt "%s" (Printexc.to_string exn)
106 (** raised when a function call contains something that can't be translated to
109 (** cost of incr_cost (cost of all the instruction until the next one) *)
110 let rec term_of_exp e =
111 let open Cil_types in
113 | Const (CInt64 _ as c) ->
114 Logic_const.term (TConst c) (Ctype (Cil.typeOf e))
115 | Lval (Var varinfo, offset) ->
116 let logic_var = Cil.cvar_to_lvar varinfo in
117 let offset = term_offset_of_offset offset in
118 Logic_const.term (TLval (TVar logic_var, offset)) (Ctype (Cil.typeOf e))
119 | Info (e, _) -> term_of_exp e
120 | UnOp (unop, e, typ) ->
121 Logic_const.term (TUnOp (unop, term_of_exp e)) (Ctype typ)
122 | BinOp (binop, e1, e2, typ) ->
123 Logic_const.term (TBinOp (binop, term_of_exp e1, term_of_exp e2))
126 Logic_const.term (TCastE (typ, term_of_exp e)) (Ctype typ)
127 | _ -> raise (Untranslatable_expr e)
129 and term_offset_of_offset = function
130 | NoOffset -> TNoOffset
131 | Field (fi, offset) ->
132 TField(fi, term_offset_of_offset offset)
133 | Index (exp, offset) ->
134 TIndex(term_of_exp exp, term_offset_of_offset offset)
137 let e = if remove_casts_in_annotations then remove_casts e else e in
140 (** Same as before but use integer for all the types *)
141 let term_of_cost_expr e =
143 | Const (CInt64 _ as c) ->
144 Logic_const.term (TConst c) Linteger
145 (** TODO: convert the other function use integer when needed *)
146 | _ -> raise (Untranslatable_expr e)
148 (** Operation simplifying (** same as termFoldConst ? *) *)
150 let make_at label x =
151 let open Cil_types in
152 match x.term_node with
153 | TConst (CInt64 (_,_,_)) -> x
154 | _ -> Logic_const.tat (x,label)
156 (** Use only for cost *)
160 | {term_node = TConst (CInt64 (xn,_,_))},
161 {term_node = TConst (CInt64 (yn,_,_))} ->
162 (Cil.lconstant (My_bigint.max xn yn))
163 (* (\** one null *\) *) (* correct but dangerous *)
164 (* | {term_node = TConst (CInt64 (zero,_,_))}, other *)
165 (* | other, {term_node = TConst (CInt64 (zero,_,_))} *)
166 (* when My_bigint.is_zero zero -> other *)
169 Logic_const.term (Tapp (get_max_logic_info (), [], [x;y])) Linteger
171 let make_max_opt x y =
173 (** one inaccessible *)
174 | None, other | other, None -> other
175 | Some x, Some y -> Some (make_max x y)
177 let make_sign = function
179 | {term_node = TConst (CInt64 (xn,_,_))} ->
180 if My_bigint.ge xn My_bigint.zero
181 then (Cil.lconstant (My_bigint.one))
182 else (Cil.lconstant (My_bigint.minus_one))
183 (* (\** one null *\) *) (* correct but dangerous *)
184 (* | {term_node = TConst (CInt64 (zero,_,_))}, other *)
185 (* | other, {term_node = TConst (CInt64 (zero,_,_))} *)
186 (* when My_bigint.is_zero zero -> other *)
189 let cond = Logic_const.term (TBinOp (Ge,x,Cil.lzero ())) Linteger in
190 let term = Logic_const.term (Tif (cond,
191 (Cil.lconstant (My_bigint.one)),
192 (Cil.lconstant (My_bigint.minus_one))))
196 let make_unop unop x =
197 match unop, x.term_node with
198 | Neg, TUnOp(Neg,y) -> y
199 | Neg, TConst (CInt64 (xn,_,_)) -> Cil.lconstant (My_bigint.neg xn)
200 | _ -> Logic_const.term (TUnOp (unop,x)) Linteger
202 let make_binop binop x y =
203 match binop, x.term_node, y.term_node with
204 | PlusA, TConst (CInt64 (xn,_,_)), TConst (CInt64 (yn,_,_)) ->
205 Cil.lconstant (My_bigint.add xn yn)
206 | PlusA, TConst (CInt64 (zero,_,_)), _ when My_bigint.is_zero zero -> y
207 | PlusA, _, TConst (CInt64 (zero,_,_)) when My_bigint.is_zero zero -> x
209 | MinusA, TConst (CInt64 (xn,_,_)), TConst (CInt64 (yn,_,_)) ->
210 Cil.lconstant (My_bigint.sub xn yn)
211 | MinusA, TConst (CInt64 (zero,_,_)), _ when My_bigint.is_zero zero ->
213 | MinusA, _, TConst (CInt64 (zero,_,_)) when My_bigint.is_zero zero -> x
214 | Mult, TConst (CInt64 (xn,_,_)), TConst (CInt64 (yn,_,_)) ->
215 Cil.lconstant (My_bigint.mul xn yn)
216 | Mult, TConst (CInt64 (zero,_,_)), _ when My_bigint.is_zero zero -> x
217 | Mult, _, TConst (CInt64 (zero,_,_)) when My_bigint.is_zero zero -> y
218 | Mult, TConst (CInt64 (one,_,_)), _ when My_bigint.is_one one -> y
219 | Mult, _, TConst (CInt64 (one,_,_)) when My_bigint.is_one one -> x
220 | Div, TConst (CInt64 (xn,_,_)), TConst (CInt64 (yn,_,_)) ->
221 Cil.lconstant (My_bigint.div xn yn)
222 (* | Div, TConst (CInt64 (zero,_,_)), _ when My_bigint.is_zero zero -> x *)
223 (* | Div, _, TConst (CInt64 (zero,_,_)) when My_bigint.is_zero zero -> y *)
224 | Div, _, TConst (CInt64 (one,_,_)) when My_bigint.is_one one -> x
225 | Div, _, TConst (CInt64 (minus_one,_,_))
226 when My_bigint.equal My_bigint.minus_one minus_one ->
228 | _ -> Logic_const.term (TBinOp (binop,x,y)) Linteger
230 let simplify_term_top t =
231 match t.term_node with
232 | TBinOp(binop,x,y) -> make_binop binop x y
233 | TUnOp(unop,x) -> make_unop unop x
235 TBinOp ((Lt|Le|Gt|Ge|Eq|Ne) as rel,
236 {term_node = TConst (CInt64 (xn,_,_))},
237 {term_node = TConst (CInt64 (yn,_,_))})},t1,t2) ->
238 let b = match rel with
239 | Lt -> My_bigint.lt xn yn
240 | Gt -> My_bigint.gt xn yn
241 | Le -> My_bigint.le xn yn
242 | Ge -> My_bigint.ge xn yn
243 | Eq -> My_bigint.equal xn yn
244 | Ne -> not (My_bigint.equal xn yn)
245 | _ -> assert false in
247 | Tapp(f, [], [{term_node = TConst (CInt64 (xn,_,_))} as xt;
248 {term_node = TConst (CInt64 (yn,_,_))} as yt]) when
249 Cil_datatype.Logic_info.equal f (get_max_logic_info ()) ->
250 if My_bigint.gt xn yn then xt else yt
253 class simplify_term prj =
254 object inherit Visitor.frama_c_copy prj as super
255 method vterm term = Cil.ChangeDoChildrenPost(term,simplify_term_top)
258 let rec top_const_form t =
259 match t.term_node with
260 | TConst _ -> t, (Cil.lzero ())
262 let cx,x = top_const_form x in
263 begin match unop with
264 | Neg -> make_unop unop cx, make_unop unop x
265 | _ -> (Cil.lzero ()),
266 Logic_const.term (TUnOp (unop,make_binop PlusA cx x)) Linteger end
267 | TBinOp(binop,x,y) ->
268 let cx,x = top_const_form x in
269 let cy,y = top_const_form y in
270 begin match binop with
271 | PlusA -> make_binop binop cx cy, make_binop binop x y
272 | MinusA -> make_binop binop cx cy, make_binop binop x y
273 | Mult -> make_binop binop cx cy,
274 make_binop PlusA (make_binop binop x y)
275 (make_binop PlusA (make_binop binop cx y)
276 (make_binop binop cy x))
277 | _ -> (Cil.lzero ()),
278 Logic_const.term (TBinOp (binop, make_binop PlusA cx x,
279 make_binop PlusA cy y)) Linteger end
281 let c1,t1 = top_const_form t1 in
282 let c2,t2 = top_const_form t2 in
283 let c3,t3 = top_const_form t3 in
285 Logic_const.term (Tif(make_binop PlusA c1 t1,
286 make_binop PlusA c2 t2,
287 make_binop PlusA c3 t3)) Linteger
288 | Tapp(f, labs, l) ->
291 (Tapp(f, labs, List.map (fun t -> let c,t = top_const_form t in
292 make_binop PlusA c t) l))
294 | _ -> (Cil.lzero ()),t
297 let top_const_form t =
298 let ct,t = top_const_form t in
299 make_binop PlusA ct t
301 let simplify_term term =
303 Visitor.visitFramacTerm (new simplify_term (Project.current ())) term in
304 if put_const_at_the_top_in_annotations then top_const_form term else term
307 (** {2 Simply labels} *)
309 class subst_lval subst prj =
310 object inherit Visitor.frama_c_copy prj as super
312 let open Cil_types in
313 match term.term_node with
314 | TLval (TVar {lv_origin = Some vi},TNoOffset)
315 when Varinfo.Map.mem vi subst ->
316 Cil.ChangeTo (Varinfo.Map.find vi subst)
317 | _ -> Cil.DoChildren
321 class subst_with_label stmt_label subst prj =
322 object inherit Visitor.frama_c_copy prj as super
324 let open Cil_types in
325 match term.term_node with
326 | TLval (TVar {lv_origin = Some vi},TNoOffset) (**TODO other offset *)
327 when Varinfo.Map.mem vi subst ->
328 Cil.ChangeTo (Varinfo.Map.find vi subst)
329 | Tat _ -> Cil.JustCopy (* don't touch if we don't see it *)
330 | _ -> Cil.ChangeDoChildrenPost(term,simplify_term_top)
334 class remove_stmt_label stmt_label prj =
335 object inherit Visitor.frama_c_copy prj as super
337 let open Cil_types in
338 match term.term_node with
339 | Tat(t, (LogicLabel (Some stmt,_)))
340 when Stmt.equal stmt stmt_label ->
343 let rec filter_label l =
346 (** TODO understand what the differences between la and lb *)
347 | (( LogicLabel(Some stmt,_),_) | (_,LogicLabel(Some stmt,_)))::ll
348 when Stmt.equal stmt stmt_label -> filter_label ll
350 let ll' = filter_label ll in
351 if ll == ll' then l else a::ll' in
352 let l' = filter_label l in
353 if l == l' then Cil.DoChildren
354 else Cil.ChangeDoChildrenPost
355 ({term with term_node = Tapp(li,l',t)},fun x -> x)
356 | _ -> Cil.DoChildren
360 class remove_logic_label lab prj =
361 object inherit Visitor.frama_c_copy prj as super
363 let open Cil_types in
364 match term.term_node with
366 when Logic_label.equal label lab ->
369 let rec filter_label l =
372 (** TODO understand what the differences between la and lb *)
373 | (label1,label2)::ll
374 when Logic_label.equal label1 lab ||
375 Logic_label.equal label2 lab -> filter_label ll
377 let ll' = filter_label ll in
378 if ll == ll' then l else a::ll' in
379 let l' = filter_label l in
380 if l == l' then Cil.DoChildren
381 else Cil.ChangeDoChildrenPost
382 ({term with term_node = Tapp(li,l',t)},fun x -> x)
383 | _ -> Cil.DoChildren
386 let remove_logic_label lab cost =
387 Visitor.visitFramacTerm
388 (new remove_logic_label lab (Project.current ()))
392 let rec freevar acc t =
393 match t.term_node with
395 | TUnOp(_,x) -> freevar acc x
396 | TBinOp(_,x,y) -> freevar (freevar acc x) y
397 | Tif(t1,t2,t3) -> freevar (freevar (freevar acc t1) t2) t3
398 | Tapp(_, _, l) -> List.fold_left freevar acc l
399 | Tat(t,_) -> freevar acc t
400 | (TLval(TVar lv,_)) -> Cil_datatype.Logic_var.Set.add lv acc
406 match lv.lv_type with
408 (** the main handle cases is t is an integer, lv an is int so we
409 need a cast (int)t *)
410 (* if Logic_utils.is_same_type lv.lv_type t.term_type *)
412 (* else *) Logic_const.term (TCastE(typ,t)) lv.lv_type
414 let args = List.map2 cast li.l_profile args in