constructor.ml 5.86 KB
Newer Older
1
2
3
4
5
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
50
51
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
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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
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
163
164
165
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
(*                                                                        *)
(*  Copyright (C) 2012-2018                                               *)
(*    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
    | Assertion -> "Assertion"
    | Precondition -> "Precondition"
    | Postcondition -> "Postcondition"
    | Invariant -> "Invariant"
    | RTE -> "RTE")

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 ->
        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)
      ty_params
      args
  in
  let args = match vi.vtype with
    | 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 ->
    store [ Cil.evar ~loc vi ; Cil.sizeOf ~loc ty ]
  | TPtr(TInt(IChar, _), _), Some size -> store [ Cil.evar ~loc vi ; size ]
  | _, None -> store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
  | _, Some _ -> assert false

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 =
    if reverse then e else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
  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:
compile-command: "make -C ../.."
End:
*)