plugin/simplify_terms.ml

   1 (** This module gives utility functions for creating terms and
   2      simplifying them *)
   3
   4 open Parameters
   5 open Cil_types
   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
  10
  11 (** {Add needed logic function} *)
  12
  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)
  16         (struct
  17           let name = "max_logic_fun"
  18           let dependencies = [Annotations.self]
  19           let kind = `Internal
  20          end) in
  21   let create () =
  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
  25     let body =
  26       let cond = Logic_const.term (TBinOp (Gt,tx,ty)) Linteger in
  27       let term = Logic_const.term (Tif (cond,tx,ty)) Linteger in
  28       term in
  29     let signature = Larrow ([Linteger;Linteger],Linteger) in
  30     let li = { l_var_info = Cil_const.make_logic_var "__max" signature;
  31                l_labels = [];
  32                l_tparams = [];
  33                l_type = Some Linteger;
  34                l_profile = [x;y];
  35                l_body = LBterm body } in
  36     li
  37   in
  38   (fun () -> M.memo create),
  39   (fun () ->
  40     match M.get_option () with
  41     | None -> ()
  42     | Some li ->
  43       Globals.Annotations.add_generated
  44         (Dfun_or_pred (li, Cil_datatype.Location.unknown)))
  45
  46
  47 (** {2 Simplify casts} *)
  48 (** Casts may get in the way when looking for a loop counter, just remove
  49     them. *)
  50
  51 let rec remove_casts e = match e.enode with
  52   | Lval lval ->
  53     { e with enode = Lval (remove_casts_lval lval) }
  54   | SizeOfE e ->
  55     { e with enode = SizeOfE (remove_casts e) }
  56   | AlignOfE 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) ->
  61     let enode =
  62       BinOp (binop, remove_casts e1, remove_casts e2, typ) in
  63     { e with enode }
  64   | CastE (_, e) -> remove_casts e
  65   | AddrOf lval ->
  66     { e with enode = AddrOf (remove_casts_lval lval) }
  67   | StartOf lval ->
  68     { e with enode = StartOf (remove_casts_lval lval) }
  69   | Info (e, info) ->
  70     { e with enode = Info (remove_casts e, info) }
  71   | _ -> e
  72
  73 and remove_casts_lval (lhost, offset) =
  74   (remove_casts_lhost lhost, remove_casts_offset offset)
  75
  76 and remove_casts_lhost = function
  77   | Mem e -> Mem (remove_casts e)
  78   | lhost -> lhost
  79
  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)
  85   | offset -> offset
  86
  87
  88 (** {2 Simplify and convert terms} *)
  89
  90
  91 (*** Exceptions ***)
  92 exception Untranslatable_expr of exp
  93
  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;
  98   | e -> raise e
  99
 100 let print_exception fmt exn =
 101   try
 102     print_exception_raise fmt exn
 103   with _ -> Format.fprintf fmt "%s" (Printexc.to_string exn)
 104
 105
 106 (** raised when a function call contains something that can't be translated to
 107     term *)
 108
 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
 112   match e.enode with
 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))
 124       (Ctype typ)
 125   | CastE (typ, e) ->
 126     Logic_const.term (TCastE (typ, term_of_exp e)) (Ctype typ)
 127   | _ -> raise (Untranslatable_expr e)
 128
 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)
 135
 136 let term_of_exp e =
 137   let e = if remove_casts_in_annotations then remove_casts e else e in
 138   term_of_exp e
 139
 140 (** Same as before but use integer for all the types *)
 141 let term_of_cost_expr e =
 142   match e.enode with
 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)
 147
 148 (** Operation simplifying (** same as termFoldConst ? *) *)
 149
 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)
 155
 156 (** Use only for cost *)
 157 let make_max x y =
 158   match x, y with
 159     (** two constants *)
 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 *)
 167     (** generic case *)
 168   | x, y ->
 169     Logic_const.term (Tapp (get_max_logic_info (), [], [x;y])) Linteger
 170
 171 let make_max_opt x y =
 172   match x, y with
 173     (** one inaccessible *)
 174   | None, other | other, None -> other
 175   | Some x, Some y -> Some (make_max x y)
 176
 177 let make_sign = function
 178     (** two constants *)
 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 *)
 187     (** generic case *)
 188   | x ->
 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))))
 193       Linteger in
 194     term
 195
 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
 201
 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
 208
 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 ->
 212     make_unop Neg y
 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 ->
 227     make_unop Neg x
 228   | _ -> Logic_const.term (TBinOp (binop,x,y)) Linteger
 229
 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
 234   | Tif({term_node =
 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
 246     if b then t1 else t2
 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
 251   | _ -> t
 252
 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)
 256 end
 257
 258 let rec top_const_form t =
 259   match t.term_node with
 260   | TConst _ -> t, (Cil.lzero ())
 261   | TUnOp(unop,x) ->
 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
 280   | Tif(t1,t2,t3) ->
 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
 284     Cil.lzero (),
 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) ->
 289     Cil.lzero (),
 290     Logic_const.term
 291       (Tapp(f, labs, List.map (fun t -> let c,t = top_const_form t in
 292                                         make_binop PlusA c t) l))
 293       Linteger
 294   | _ -> (Cil.lzero ()),t
 295
 296
 297 let top_const_form t =
 298   let ct,t = top_const_form t in
 299   make_binop PlusA ct t
 300
 301 let simplify_term term =
 302   let 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
 305
 306
 307 (** {2 Simply labels} *)
 308
 309 class subst_lval subst prj =
 310 object inherit Visitor.frama_c_copy prj as super
 311        method vterm term =
 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
 318
 319 end
 320
 321 class subst_with_label stmt_label subst prj  =
 322 object inherit Visitor.frama_c_copy prj as super
 323        method vterm term =
 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)
 331
 332 end
 333
 334 class remove_stmt_label stmt_label prj  =
 335 object inherit Visitor.frama_c_copy prj as super
 336        method vterm term =
 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 ->
 341            Cil.ChangeTo t
 342          | Tapp(li,l,t) ->
 343            let rec filter_label l =
 344              match l with
 345              | [] -> 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
 349              | a::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
 357 end
 358
 359
 360 class remove_logic_label lab prj  =
 361 object inherit Visitor.frama_c_copy prj as super
 362        method vterm term =
 363          let open Cil_types in
 364          match term.term_node with
 365          | Tat(t, label)
 366              when Logic_label.equal label lab ->
 367            Cil.ChangeTo t
 368          | Tapp(li,l,t) ->
 369            let rec filter_label l =
 370              match l with
 371              | [] -> 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
 376              | a::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
 384 end
 385
 386 let remove_logic_label lab cost =
 387   Visitor.visitFramacTerm
 388     (new remove_logic_label lab (Project.current ()))
 389     cost
 390
 391
 392 let rec freevar acc t =
 393   match t.term_node with
 394   | TConst _ -> acc
 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
 401   | _ -> assert false
 402
 403
 404 let tapp li args =
 405   let cast lv t =
 406     match lv.lv_type with
 407     | Ctype typ ->
 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 *)
 411       (* then t *)
 412       (* else *) Logic_const.term (TCastE(typ,t)) lv.lv_type
 413     | _  -> t  in
 414   let args = List.map2 cast li.l_profile args in
 415   Tapp(li,[],args)