misc.ml 7.8 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
Patrick Baudin's avatar
Patrick Baudin committed
3
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
4
(*                                                                        *)
5
(*  Copyright (C) 2012-2019                                               *)
Virgile Prevosto's avatar
Virgile Prevosto committed
6
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
Julien Signoles's avatar
Julien Signoles committed
7
(*         alternatives)                                                  *)
8
9
10
11
12
13
14
15
16
17
18
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
Virgile Prevosto's avatar
Virgile Prevosto committed
19
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
20
21
22
(*                                                                        *)
(**************************************************************************)

23
module RTL = Functions.RTL
24
25
26
open Cil_types
open Cil_datatype

27
28
29
30
(* ************************************************************************** *)
(** {2 Handling the E-ACSL's C-libraries, part I} *)
(* ************************************************************************** *)

31
let library_files () =
32
  List.map
33
34
    (fun d ->
       Filepath.Normalized.of_string (Options.Share.file ~error:true d))
35
    [ "e_acsl_gmp_api.h";
36
      "e_acsl.h" ]
37

38
let is_library_loc (loc, _) = List.mem loc.Filepath.pos_path (library_files ())
39

40
let library_functions = Datatype.String.Hashtbl.create 17
41
let register_library_function vi =
42
  Datatype.String.Hashtbl.add library_functions vi.vname vi
43

44
let reset () = Datatype.String.Hashtbl.clear library_functions
45

46
47
48
let is_fc_or_compiler_builtin vi =
  Cil.is_builtin vi
  ||
49
  (let prefix_length = 10 (* number of characters in "__builtin_" *) in
Julien Signoles's avatar
Julien Signoles committed
50
51
52
53
   String.length vi.vname > prefix_length
   &&
   let prefix = String.sub vi.vname 0 prefix_length in
   Datatype.String.equal prefix "__builtin_")
54

55
56
57
58
(* ************************************************************************** *)
(** {2 Builders} *)
(* ************************************************************************** *)

Julien Signoles's avatar
Julien Signoles committed
59
exception Unregistered_library_function of string
60
61
let get_lib_fun_vi fname =
  try Datatype.String.Hashtbl.find library_functions fname
Julien Signoles's avatar
Julien Signoles committed
62
63
64
65
66
67
  with Not_found ->
  try Builtins.find fname
  with Not_found ->
    (* should not happen in normal mode, but could be raised when E-ACSL is
       used as a library *)
    raise (Unregistered_library_function fname)
68

69
70
71
72
(* ************************************************************************** *)
(** {2 Handling \result} *)
(* ************************************************************************** *)

73
let result_lhost kf =
74
75
  let stmt =
    try Kernel_function.find_return kf
76
77
78
79
80
81
82
83
84
85
    with Kernel_function.No_Statement -> assert false
  in
  match stmt.skind with
  | Return(Some { enode = Lval (lhost, NoOffset) }, _) -> lhost
  | _ -> assert false

let result_vi kf = match result_lhost kf with
  | Var vi -> vi
  | Mem _ -> assert false

86
87
88
89
90
91
92
(* ************************************************************************** *)
(** {2 Other stuff} *)
(* ************************************************************************** *)

let term_addr_of ~loc tlv ty =
  Logic_const.taddrof ~loc tlv (Ctype (TPtr(ty, [])))

93
94
let reorder_ast () =
  let ast = Ast.get() in
95
  let is_from_library = function
96
    | GType(ti, _) when ti.tname = "size_t" || ti.tname = "FILE"
Julien Signoles's avatar
Julien Signoles committed
97
                        || RTL.is_rtl_name ti.tname -> true
98
    | GCompTag (ci, _) when RTL.is_rtl_name ci.cname -> true
99
100
    | GFunDecl(_, _, loc) | GVarDecl(_, loc) when is_library_loc loc -> true
    | _ -> false in
101
  let rtl, other = List.partition is_from_library ast.globals in
102
  ast.globals <- rtl @ other
103

Julien Signoles's avatar
Julien Signoles committed
104
105
106
107
let cty = function
  | Ctype ty -> ty
  | lty -> Options.fatal "Expecting a C type. Got %a" Printer.pp_logic_type lty

108
let rec ptr_index ?(loc=Location.unknown) ?(index=(Cil.zero loc)) exp =
Kostyantyn Vorobyov's avatar
Kostyantyn Vorobyov committed
109
110
111
112
113
  let arith_op = function
    | MinusPI -> MinusA
    | PlusPI -> PlusA
    | IndexPI -> PlusA
    | _ -> assert false in
114
115
116
  match exp.enode with
  | BinOp(op, lhs, rhs, _) ->
    (match op with
Julien Signoles's avatar
Julien Signoles committed
117
118
119
120
121
122
123
124
     (* Pointer arithmetic: split pointer and integer parts *)
     | MinusPI | PlusPI | IndexPI ->
       let index = Cil.mkBinOp exp.eloc (arith_op op) index rhs in
       ptr_index ~index lhs
     (* Other arithmetic: treat the whole expression as pointer address *)
     | MinusPP | PlusA | MinusA | Mult | Div | Mod
     | BAnd | BXor | BOr | Shiftlt | Shiftrt
     | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr -> (exp, index))
125
126
127
128
129
130
  | CastE _ -> ptr_index ~loc ~index (Cil.stripCasts exp)
  | Info (exp, _) -> ptr_index ~loc ~index exp
  | Const _ | StartOf _ | AddrOf _ | Lval _ | UnOp _ -> (exp, index)
  | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
    -> assert false

131
(* TODO: should not be in this file *)
132
let term_of_li li =  match li.l_body with
Julien Signoles's avatar
Julien Signoles committed
133
134
135
  | LBterm t -> t
  | LBnone | LBreads _ | LBpred _ | LBinductive _ ->
    Options.fatal "li.l_body does not match LBterm(t) in Misc.term_of_li"
136
137

let is_set_of_ptr_or_array lty =
138
  if Logic_const.is_set_type lty then
139
    let lty = Logic_const.type_of_element lty in
140
141
    Logic_utils.isLogicPointerType lty || Logic_utils.isLogicArrayType lty
  else
142
143
    false

144
exception Range_found_exception
145
let is_range_free t =
146
147
148
  try
    let has_range_visitor = object inherit Visitor.frama_c_inplace
      method !vterm t = match t.term_node with
Julien Signoles's avatar
Julien Signoles committed
149
150
        | Trange _ -> raise Range_found_exception
        | _ -> Cil.DoChildren
151
152
153
154
155
156
    end
    in
    ignore (Visitor.visitFramacTerm has_range_visitor t);
    true
  with Range_found_exception ->
    false
157

158
159
let is_bitfield_pointers lty =
  let is_bitfield_pointer = function
160
161
162
163
164
165
166
167
168
169
170
171
    | Ctype typ ->
      begin match Cil.unrollType typ with
        | TPtr(typ, _) ->
          let attrs = Cil.typeAttrs typ in
          Cil.hasAttribute Cil.bitfield_attribute_name attrs
        | _ ->
          false
      end
    | Ltype _ | Lvar _ | Linteger | Lreal | Larrow _ ->
      false
  in
  if Logic_const.is_set_type lty then
172
    is_bitfield_pointer (Logic_const.type_of_element lty)
173
  else
174
    is_bitfield_pointer lty
175

176
exception Lv_from_vi_found
177
let term_has_lv_from_vi t =
178
179
180
  try
    let o = object inherit Visitor.frama_c_inplace
      method !vlogic_var_use lv = match lv.lv_origin with
Julien Signoles's avatar
Julien Signoles committed
181
182
        | None -> Cil.DoChildren
        | Some _ -> raise Lv_from_vi_found
183
184
185
186
187
188
    end
    in
    ignore (Visitor.visitFramacTerm o t);
    false
  with Lv_from_vi_found ->
    true
189
190
191

type pred_or_term = PoT_pred of predicate | PoT_term of term

192
193
194
195
196
let mk_ptr_sizeof typ loc =
  match Cil.unrollType typ with
  | TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
  | _ -> assert false

197
198
199
200
let finite_min_and_max i = match Ival.min_and_max i with
  | Some min, Some max -> min, max
  | None, _ | _, None -> assert false

201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
let name_of_binop = function
  | Lt -> "lt"
  | Gt -> "gt"
  | Le -> "le"
  | Ge -> "ge"
  | Eq -> "eq"
  | Ne -> "ne"
  | LOr -> "or"
  | LAnd -> "and"
  | BOr -> "bor"
  | BXor -> "bxor"
  | BAnd -> "band"
  | Shiftrt -> "shiftr"
  | Shiftlt -> "shiftl"
  | Mod -> "mod"
  | Div -> "div"
  | Mult -> "mul"
  | PlusA -> "add"
  | MinusA -> "sub"
  | MinusPP | MinusPI | IndexPI | PlusPI -> assert false

222
223
(*
Local Variables:
224
compile-command: "make -C ../../../../.."
225
End:
226
*)