constructor.ml 6.25 KB
Newer Older
1
2
3
4
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
(*                                                                        *)
5
(*  Copyright (C) 2012-2019                                               *)
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
(*    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

(* ********************************************************************** *)
(* Expressions *)
(* ********************************************************************** *)

let mk_deref ~loc lv = Cil.new_exp ~loc (Lval(Mem(lv), NoOffset))

(* ********************************************************************** *)
(* Statements *)
(* ********************************************************************** *)

let mk_stmt sk = Cil.mkStmt ~valid_sid:true sk
let mk_instr i = mk_stmt (Instr i)
let mk_call ~loc ?result e args = mk_instr (Call(result, e, args, loc))

type annotation_kind =
  | Assertion
  | Precondition
  | Postcondition
  | Invariant
  | RTE

let kind_to_string loc k =
  Cil.mkString
    ~loc
    (match k with
Julien Signoles's avatar
Julien Signoles committed
50
51
52
53
54
     | Assertion -> "Assertion"
     | Precondition -> "Precondition"
     | Postcondition -> "Postcondition"
     | Invariant -> "Invariant"
     | RTE -> "RTE")
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

let mk_block stmt b = match b.bstmts with
  | [] ->
    (match stmt.skind with
     | Instr(Skip _) -> stmt
     | _ -> assert false)
  | [ s ] -> s
  |  _ :: _ -> mk_stmt (Block b)

(* ********************************************************************** *)
(* E-ACSL specific code *)
(* ********************************************************************** *)

let mk_lib_call ~loc ?result fname args =
  let vi = Misc.get_lib_fun_vi fname in
  let f = Cil.evar ~loc vi in
  vi.vreferenced <- true;
  let make_args args ty_params =
    List.map2
      (fun (_, ty, _) arg ->
Julien Signoles's avatar
Julien Signoles committed
75
76
77
78
79
80
81
         let e =
           match ty, Cil.unrollType (Cil.typeOf arg), arg.enode with
           | TPtr _, TArray _, Lval lv -> Cil.new_exp ~loc (StartOf lv)
           | TPtr _, TArray _, _ -> assert false
           | _, _, _ -> arg
         in
         Cil.mkCast ~force:false ~newt:ty ~e)
82
83
84
      ty_params
      args
  in
85
  let args = match Cil.unrollType vi.vtype with
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
    | TFun(_, Some params, _, _) -> make_args args params
    | TFun(_, None, _, _) -> []
    | _ -> assert false
  in
  mk_call ~loc ?result f args

let mk_rtl_call ~loc ?result fname args =
  mk_lib_call ~loc ?result (Functions.RTL.mk_api_name fname) args

(* ************************************************************************** *)
(** {2 Handling the E-ACSL's C-libraries, part II} *)
(* ************************************************************************** *)

let mk_full_init_stmt ?(addr=true) vi =
  let loc = vi.vdecl in
  let mk = mk_rtl_call ~loc "full_init" in
  match addr, Cil.unrollType vi.vtype with
  | _, TArray(_,Some _, _, _) | false, _ -> mk [ Cil.evar ~loc vi ]
  | _ -> mk [ Cil.mkAddrOfVi vi ]

let mk_initialize ~loc (host, offset as lv) = match host, offset with
  | Var _, NoOffset ->
    mk_rtl_call ~loc "full_init" [ Cil.mkAddrOf ~loc lv ]
  | _ ->
    let typ = Cil.typeOfLval lv in
    mk_rtl_call ~loc
      "initialize"
      [ Cil.mkAddrOf ~loc lv; Cil.new_exp loc (SizeOf typ) ]

let mk_named_store_stmt name ?str_size vi =
  let ty = Cil.unrollType vi.vtype in
  let loc = vi.vdecl in
  let store = mk_rtl_call ~loc name in
  match ty, str_size with
  | TArray(_, Some _,_,_), None ->
121
122
123
124
    store [ Cil.evar ~loc vi; Cil.sizeOf ~loc ty ]
  | TPtr(TInt(IChar, _), _), Some size ->
    store [ Cil.evar ~loc vi ; size ]
  | TPtr _, Some size ->
125
    (* a VLA that has been converted into a pointer by the kernel *)
126
127
128
    store [ Cil.evar ~loc vi; size ]
  | _, None ->
    store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
129
130
131
  | _, Some size ->
    Options.fatal
      "unexpected types for arguments of function '%s': \
Julien Signoles's avatar
Julien Signoles committed
132
       %s got type %a, while representing a memory block of %a bytes"
133
134
135
136
      name
      vi.vname
      Printer.pp_typ ty
      Printer.pp_exp size
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162

let mk_store_stmt ?str_size vi =
  mk_named_store_stmt "store_block" ?str_size vi

let mk_duplicate_store_stmt ?str_size vi =
  mk_named_store_stmt "store_block_duplicate" ?str_size vi

let mk_delete_stmt vi =
  let loc = vi.vdecl in
  let mk = mk_rtl_call ~loc "delete_block" in
  match Cil.unrollType vi.vtype with
  | TArray(_, Some _, _, _) -> mk [ Cil.evar ~loc vi ]
  | _ -> mk [ Cil.mkAddrOfVi vi ]

let mk_mark_readonly vi =
  let loc = vi.vdecl in
  mk_rtl_call ~loc "mark_readonly" [ Cil.evar ~loc vi ]

let mk_runtime_check ?(reverse=false) kind kf e p =
  let loc = p.pred_loc in
  let msg =
    Kernel.Unicode.without_unicode
      (Format.asprintf "%a@?" Printer.pp_predicate) p
  in
  let line = (fst loc).Filepath.pos_lnum in
  let e =
163
164
165
    if reverse
    then e
    else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
166
167
168
169
170
171
172
173
174
175
176
  in
  mk_rtl_call ~loc
    "assert"
    [ e;
      kind_to_string loc kind;
      Cil.mkString ~loc (Functions.RTL.get_original_name kf);
      Cil.mkString ~loc msg;
      Cil.integer loc line ]

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