logic_functions.ml 13.4 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
3
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
4
(*                                                                        *)
5
(*  Copyright (C) 2012-2019                                               *)
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  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                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
24
open Cil_datatype
25
26
27
28
29

(**************************************************************************)
(********************** Forward references ********************************)
(**************************************************************************)

30
let named_predicate_to_exp_ref
31
32
33
34
35
36
37
  : (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
  = Extlib.mk_fun "named_predicate_to_exp_ref"

let term_to_exp_ref
  : (kernel_function -> Env.t -> term -> exp * Env.t) ref
  = Extlib.mk_fun "term_to_exp_ref"

38
39
40
41
42
43
(*****************************************************************************)
(************************** Auxiliary  functions* ****************************)
(*****************************************************************************)

(* @return true iff the result of the function is provided by reference as the
   first extra argument at each call *)
44
let result_as_extra_argument = Gmp_types.Z.is_t
45
46
(* TODO: to be extended to any compound type? E.g. returning a struct is not
   good practice... *)
47
48
49
50
51

(*****************************************************************************)
(****************** Generation of function bodies ****************************)
(*****************************************************************************)

52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
(* Generate the block of code containing the statement assigning [e] to [ret_vi]
   (the result). *)
let generate_return_block ~loc env ret_vi e = match e.enode with
  | Lval (Var _, NoOffset) ->
    (* the returned value is a variable: Cil invariant preserved;
       no need of [ret_vi] *)
    let return_retres = Cil.mkStmt ~valid_sid:true (Return (Some e, loc)) in
    let b, env =
      Env.pop_and_get env return_retres ~global_clear:false Env.After
    in
    b.blocals <- b.blocals;
    b.bscoping <- true;
    b, env
  | _ ->
    (* the returned value is _not_ a variable: restore the invariant *)
    let init = AssignInit (SingleInit e) in
    let set =
      Cil.mkStmtOneInstr ~valid_sid:true (Local_init (ret_vi, init, loc))
    in
    let return =
      Cil.mkStmt ~valid_sid:true (Return (Some (Cil.evar ~loc ret_vi), loc))
    in
    let b, env = Env.pop_and_get env set ~global_clear:false Env.Middle in
    ret_vi.vdefined <- true;
    b.blocals <- ret_vi :: b.blocals;
    b.bstmts <- b.bstmts @ [ return ];
    b.bscoping <- true;
    b, env

(* Generate the function's body for predicates. *)
let pred_to_block ~loc kf env ret_vi p =
  Typing.type_named_predicate ~must_clear:false p;
  let e, env = !named_predicate_to_exp_ref kf env p in
  (* for predicate, since the result is either 0 or 1, return it directly (it
     cannot be provided as extra argument *)
  generate_return_block ~loc env ret_vi e
88

89
90
(* Generate the function's body for terms. *)
let term_to_block ~loc kf env ret_ty ret_vi t =
91
  Typing.type_term ~use_gmp_opt:false ~ctx:(Typing.number_ty_of_typ ret_ty) t;
92
93
94
95
96
97
98
  let e, env = !term_to_exp_ref kf env t in
  if Cil.isVoidType ret_ty then
    (* if the function's result is a GMP, it is the first parameter of the
       function (by reference). *)
    let set =
      let lv_star_ret = Cil.mkMem ~addr:(Cil.evar ~loc ret_vi) ~off:NoOffset in
      let star_ret = Cil.new_exp ~loc (Lval lv_star_ret) in
99
      Gmp.init_set ~loc lv_star_ret star_ret e
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
    in
    let return_void = Cil.mkStmt ~valid_sid:true (Return (None, loc)) in
    let b, env = Env.pop_and_get env set ~global_clear:false Env.Middle in
    b.bstmts <- b.bstmts @ [ return_void ];
    b.bscoping <- true;
    b, env
  else
    generate_return_block ~loc env ret_vi e

let generate_body ~loc kf env ret_ty ret_vi = function
  | LBnone | LBreads _ ->
    Options.abort
      "logic function or predicate without explicit definition are not part of \
       E-ACSL"
  | LBterm t -> term_to_block ~loc kf env ret_ty ret_vi t
  | LBpred p -> pred_to_block ~loc kf env ret_vi p
  | LBinductive _ -> Error.not_yet "inductive definition"
117

118
119
120
121
122
123
124
(* Generate a kernel function from a given logic info [li] *)
let generate_kf ~loc fname env ret_ty params_ty li =
  (* build the formal parameters *)
  let params, params_ty =
    List.fold_right2
      (fun lvi pty (params, params_ty) ->
        let ty = match pty with
125
          | Typing.Gmpz ->
126
127
            (* GMP's integer are arrays: consider them as pointers in function's
               parameters *)
128
            Gmp_types.Z.t_as_ptr ()
129
130
131
          | Typing.C_integer ik -> TInt(ik, [])
          | Typing.C_float ik -> TFloat(ik, [])
          (* for the time being, no reals but rationals instead *)
132
          | Typing.Rational -> Gmp_types.Q.t ()
133
          | Typing.Real -> Error.not_yet "real number"
134
          | Typing.Nan -> Typing.typ_of_lty lvi.lv_type
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
        in
        (* build the formals: cannot use [Cil.makeFormal] since the function
           does not yet exist *)
        let vi = Cil.makeVarinfo false true lvi.lv_name ty in
        vi :: params, (lvi.lv_name, ty, []) :: params_ty)
      li.l_profile
      params_ty
      ([], [])
  in
  (* build the varinfo storing the result *)
  let ret_vi, ret_ty, params_with_ret, params_ty_with_ret =
    let vname = "__retres" in
    if result_as_extra_argument ret_ty then
      let ret_ty_ptr = TPtr(ret_ty, []) (* call by reference *) in
      let vname = vname ^ "_arg" in
      let vi = Cil.makeVarinfo false true vname ret_ty_ptr in
      vi, Cil.voidType, vi :: params, (vname, ret_ty_ptr, []) :: params_ty
    else
      Cil.makeVarinfo false false vname ret_ty, ret_ty, params, params_ty
154
  in
155
156
157
158
159
160
161
162
163
  (* build the function's varinfo *)
  let vi =
    Cil.makeGlobalVar
      fname
      (TFun
         (ret_ty,
          Some params_ty_with_ret,
          false,
          li.l_var_info.lv_attr))
164
  in
165
166
  vi.vdefined <- true;
  (* create the fundec *)
167
  let fundec =
168
169
170
171
    { svar = vi;
      sformals = params_with_ret;
      slocals = []; (* filled later to break mutual dependencies between
                       creating this list and creating the kf *)
172
      smaxid = 0;
173
      sbody = Cil.mkBlock []; (* filled later; same as above *)
174
175
      smaxstmtid = None;
      sallstmts = [];
176
      sspec = Cil.empty_funspec () }
177
  in
178
179
  Cil.setMaxId fundec;
  let spec = Cil.empty_funspec () in
Julien Signoles's avatar
Julien Signoles committed
180
181
  (* register the definition *)
  Globals.Functions.replace_by_definition spec fundec loc;
182
183
184
185
186
187
188
189
190
191
192
  (* create the kernel function itself *)
  let kf = { fundec = Definition(fundec, loc); spec } in
  (* closure generating the function's body.
     Delay its generation after filling the memoisation table (for termination
     of recursive function calls) *)
  let gen_body () =
    let env = Env.push env in
    (* fill the typing environment with the function's parameters
       before generating the code (code generation invokes typing) *)
    let env =
      let add env lvi vi =
193
        let i = Interval.interv_of_typ vi.vtype in
194
        Interval.Env.add lvi i;
195
196
197
        Env.Logic_binding.add_binding env lvi vi
      in
      List.fold_left2 add env li.l_profile params
198
    in
199
200
201
202
203
204
205
206
    let b, env = generate_body ~loc kf env ret_ty ret_vi li.l_body in
    fundec.sbody <- b;
    (* add the generated variables in the necessary lists *)
    (* TODO: factorized the code below that add the generated vars with method
       [add_generated_variables_in_function] in the main visitor *)
    let vars =
      let l = Env.get_generated_variables env in
      if ret_vi.vdefined then (ret_vi, Env.LFunction kf) :: l else l
207
    in
208
209
210
211
212
213
214
215
216
217
    let locals, blocks =
      List.fold_left
        (fun (local_vars, block_vars as acc) (v, scope) -> match scope with
        | Env.LFunction kf' when Kernel_function.equal kf kf' ->
          v :: local_vars, block_vars
        | Env.LLocal_block kf' when Kernel_function.equal kf kf' ->
          v :: local_vars, block_vars
        | _ -> acc)
        (fundec.slocals, fundec.sbody.blocals)
        vars
218
    in
219
220
221
222
223
224
    fundec.slocals <- locals;
    fundec.sbody.blocals <- blocks;
    List.iter
      (fun lvi ->
         Interval.Env.remove lvi;
         ignore (Env.Logic_binding.remove env lvi))
225
      li.l_profile
226
  in
227
  vi, kf, gen_body
228
229
230
231
232

(**************************************************************************)
(***************************** Memoization ********************************)
(**************************************************************************)

233
234
235
236
module Params_ty =
  Datatype.List_with_collections
    (Typing.Datatype)
    (struct let module_name = "E_ACSL.Logic_functions.Params_ty" end)
237

238
239
240
241
242
(* for each logic_info, associate its possible profiles, i.e. the types of its
   parameters + the generated varinfo for the function *)
let memo_tbl:
    kernel_function Params_ty.Hashtbl.t Logic_info.Hashtbl.t
  = Logic_info.Hashtbl.create 7
243

244
let reset () = Logic_info.Hashtbl.clear memo_tbl
245

246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
let add_generated_functions globals =
  let rec aux acc = function
    | [] ->
      acc
    | GAnnot(Dfun_or_pred(li, loc), _) as g :: l ->
      let acc = g :: acc in
      (try
         (* add the declarations close to its corresponding logic function or
            predicate *)
         let params = Logic_info.Hashtbl.find memo_tbl li in
         let add_fundecl kf acc =
           GFunDecl(Cil.empty_funspec (), Kernel_function.get_vi kf, loc)
           :: acc
         in
         aux (Params_ty.Hashtbl.fold (fun _ -> add_fundecl) params acc) l
       with Not_found ->
         aux acc l)
    | g :: l ->
      aux (g :: acc) l
265
  in
266
267
268
269
270
271
  let rev_globals = aux [] globals in
  (* add the definitions at the end of [globals] *)
  let add_fundec kf globals =
    let fundec =
      try Kernel_function.get_definition kf
      with Kernel_function.No_Definition -> assert false
272
    in
273
274
275
276
277
278
279
280
281
    GFun(fundec, Location.unknown) :: globals
  in
  let rev_globals =
    Logic_info.Hashtbl.fold
      (fun _ -> Params_ty.Hashtbl.fold (fun _ -> add_fundec))
      memo_tbl
      rev_globals
  in
  List.rev rev_globals
282

283
let tapp_to_exp ~loc fname env kf t li params_ty args =
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
  let ret_ty = Typing.get_typ t in
  let gen tbl =
    let vi, kf, gen_body = generate_kf fname ~loc env ret_ty params_ty li in
    Params_ty.Hashtbl.add tbl params_ty kf;
    vi, gen_body
  in
  (* memoise the function's varinfo *)
  let fvi, gen_body =
    try
      let h = Logic_info.Hashtbl.find memo_tbl li in
      try
        let kf = Params_ty.Hashtbl.find h params_ty in
        Kernel_function.get_vi kf,
        (fun () -> ()) (* body generation already planified *)
      with Not_found -> gen h
    with Not_found ->
      let h = Params_ty.Hashtbl.create 7 in
      Logic_info.Hashtbl.add memo_tbl li h;
      gen h
  in
  (* the generation of the function body must be performed after memoizing the
     kernel function in order to handle recursive calls in finite time :-) *)
  gen_body ();
  (* create the function call for the tapp *)
  let mkcall vi =
    let mk_args types args =
      match types (* generated by E-ACSL: no need to unroll *) with
      | TFun(_, Some params, _, _) ->
        (* additional casts are necessary whenever the argument is GMP and the
           parameter is a (small) integralType: after handling the context in
           [Translate] through [add_cast], the GMP has been translated into a
           [long] (that is what provided the GMP API). This [long] must now be
           translated to the parameter's type. It cannot be done before since
           the exact type of the parameter is only computed when the function is
           generated *)
        List.map2
          (fun (_, newt, _) e -> Cil.mkCast ~force:false ~newt ~e)
          params
          args
      | _ -> assert false
    in
    if result_as_extra_argument ret_ty then
      let args = mk_args fvi.vtype (Cil.mkAddrOf ~loc (Cil.var vi) :: args) in
      Call(None, Cil.evar fvi, args, loc)
    else
      let args = mk_args fvi.vtype args in
      Call(Some (Cil.var vi), Cil.evar fvi, args, loc)
  in
  (* generate the varinfo storing the result of the call *)
  Env.new_var
    ~loc
    ~name:li.l_var_info.lv_name
    env
337
    kf
338
339
340
    (Some t)
    ret_ty
    (fun vi _ -> [ Cil.mkStmtOneInstr ~valid_sid:true (mkcall vi) ])
341
342
343
344
345
346

(*
Local Variables:
compile-command: "make -C ../.."
End:
*)