plugin/normAtLabels.ml

   1 (**************************************************************************)
   2 (*                                                                        *)
   3 (*  This file is part of WP plug-in of Frama-C.                           *)
   4 (*                                                                        *)
   5 (*  Copyright (C) 2007-2011                                               *)
   6 (*    CEA (Commissariat a l'énergie atomique et aux énergies              *)
   7 (*         alternatives)                                                  *)
   8 (*                                                                        *)
   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.                                              *)
  12 (*                                                                        *)
  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.                   *)
  17 (*                                                                        *)
  18 (*  See the GNU Lesser General Public License version 2.1                 *)
  19 (*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
  20 (*                                                                        *)
  21 (**************************************************************************)
  22
  23
  24 open Cil_types
  25
  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))
  30
  31
  32 type label_mapping = Cil_types.logic_label -> Cil_types.logic_label
  33
  34
  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.
  41 * *)
  42 class norm_at label_map = object(self)
  43   inherit Visitor.generic_frama_c_visitor (Project.current()) (Cil.copy_visit())
  44
  45   val mutable current_label = None
  46
  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
  51
  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
  56       | _ -> assert false
  57     in x
  58
  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
  63       | _ -> assert false
  64     in x
  65
  66
  67   method vterm t =
  68     match t.term_node with
  69       | Tat (t, l) ->
  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
  77             | _ -> old_label
  78           in
  79             current_label <- None;
  80           let post t =
  81             current_label <- old_label;
  82             match at_label with
  83             | Some label -> {t with term_node = Tat (t, label)}
  84             | None -> t
  85           in Cil.ChangeDoChildrenPost (t, post)
  86       (** logic function without label *)
  87       | Tapp ({l_labels=[]},[],_) -> Cil.DoChildren
  88       | Tapp (_,[],_) ->
  89         begin match current_label with
  90         | None -> Cil.DoChildren
  91         | Some lab ->
  92           let post = function
  93             | {term_node=Tapp(predicate,[],args)} as t ->
  94               { t with term_node=Tapp(predicate,[lab,lab],args) }
  95             | _ -> assert false
  96           in
  97           Cil.ChangeDoChildrenPost (t,post)
  98         end
  99       | Tapp _ ->
 100           let post = function
 101             | {term_node=Tapp(predicate,labels,args)} as t ->
 102                 let new_labels =
 103                   List.map
 104                     (fun (logic_lab, stmt_lab) -> logic_lab, label_map stmt_lab)
 105                     labels
 106                 in { t with term_node=Tapp(predicate,new_labels,args) }
 107             | _ -> assert false
 108           in
 109           Cil.ChangeDoChildrenPost (t,post)
 110       | _ -> Cil.DoChildren
 111
 112   method vpredicate_named p = match p.content with
 113     | Pat (p, l) ->
 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
 119     | Papp (_,[],_) ->
 120         begin match current_label with
 121         | None -> Cil.DoChildren
 122         | Some lab ->
 123           let post = function
 124             | {content=Papp(predicate,[],args)} as p ->
 125               { p with content=Papp(predicate,[lab,lab],args) }
 126             | _ -> assert false
 127           in
 128           Cil.ChangeDoChildrenPost (p,post)
 129         end
 130     | Papp _ ->
 131         let post = function
 132           | {content=Papp(predicate,labels,args)} as p ->
 133               let new_labels =
 134                 List.map
 135                   (fun (logic,stmt) -> logic, label_map stmt)
 136                   labels
 137               in { p with content=Papp(predicate,new_labels,args) }
 138           | _ -> assert false
 139         in
 140         Cil.ChangeDoChildrenPost (p,post)
 141     | _ -> Cil.DoChildren
 142 end
 143
 144 exception LabelError of logic_label
 145
 146 let labels_empty l = raise (LabelError l)
 147
 148 (* -------------------------------------------------------------------------- *)
 149 (* --- Function Contracts                                                 --- *)
 150 (* -------------------------------------------------------------------------- *)
 151
 152 let labels_fct_pre = function
 153   | LogicLabel (None, ("Pre" | "Here")) -> Logic_const.pre_label
 154   | l -> raise (LabelError l)
 155
 156
 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)
 161
 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)
 166
 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)
 176
 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)
 183       end
 184   | LogicLabel (Some s, _) -> mk_logic_label s
 185   | StmtLabel rs -> mk_logic_label !rs
 186   | l -> raise (LabelError l)
 187
 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 *)
 191       mk_logic_label s
 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)
 196
 197 (* -------------------------------------------------------------------------- *)
 198 (* --- User Assertions in Functions Code                                  --- *)
 199 (* -------------------------------------------------------------------------- *)
 200
 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)
 207
 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)
 215
 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)
 220   | l -> l
 221
 222 let labels_loop_assigns s l = labels_loop_inv s l
 223
 224 (* -------------------------------------------------------------------------- *)
 225 (* --- User Defined Predicates                                            --- *)
 226 (* -------------------------------------------------------------------------- *)
 227
 228 let labels_predicate lab_pairs = fun l ->
 229   try List.assoc l lab_pairs
 230   with Not_found -> l
 231
 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)
 236
 237 (* -------------------------------------------------------------------------- *)
 238 (* --- Apply Normalization                                                --- *)
 239 (* -------------------------------------------------------------------------- *)
 240
 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
 246
 247 let preproc_annot_term labels t =
 248   let visitor = new norm_at labels in
 249   Visitor.visitFramacTerm visitor t
 250
 251
 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
 257
 258 let preproc_label labels l = labels l