Source file ast_const.ml

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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's Lannotate plug-in.                 *)
(*                                                                        *)
(*  Copyright (C) 2012-2025                                               *)
(*    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 LICENSE)                       *)
(*                                                                        *)
(**************************************************************************)

open Cil_types

let unk_loc = Cil_datatype.Location.unknown

module Exp_builder = struct
  let mk ?(loc=unk_loc) =
    Cil.new_exp ~loc

  let zero ?(loc=unk_loc) () =
    Cil.zero ~loc

  let one ?(loc=unk_loc) () =
    Cil.one ~loc

  let integer ?(loc=unk_loc) =
    Cil.integer ~loc

  let kinteger ?(loc=unk_loc) =
    Cil.kinteger ~loc

  let kinteger64 ?(loc=unk_loc) kind =
    Cil.kinteger64 ~loc ~kind

  let float ?(loc=unk_loc) =
    Cil.kfloat ~loc FDouble

  let string ?(loc=unk_loc) =
    Cil.mkString ~loc

  let var ?(loc=unk_loc) varinfo =
    Cil.evar ~loc varinfo

  let lval ?(loc=Cil_datatype.Location.unknown) lval =
    Cil.new_exp ~loc (Lval lval)

  let mem ?(loc=unk_loc) addr off =
    Cil.new_exp ~loc (Lval (Cil.mkMem ~addr ~off))

  let lnot ?(loc=unk_loc) e =
    Cil.new_exp ~loc (UnOp (LNot, e, Cil_const.intType))

  let neg ?(loc=unk_loc) e =
    let oldt = Cil.typeOf e in
    let newt = Cil.integralPromotion oldt in
    (* make integral promotion explicit *)
    let e' = Cil.mkCastT ~oldt ~newt e in
    Cil.new_exp ~loc (UnOp (Neg, e', newt))

  let binop ?(loc=unk_loc) op left right =
    Cil.mkBinOp ~loc op left right

  let implies ?(loc=unk_loc) l r =
    let n_l = lnot ~loc l in
    Cil.mkBinOp ~loc LOr n_l r

  let iff ?(loc=unk_loc) l r =
    let l_imp_r = implies ~loc l r in
    let r_imp_l = implies ~loc r l in
    Cil.mkBinOp ~loc LAnd l_imp_r r_imp_l

  let niff ?(loc=unk_loc) l r =
    let nl_and_r = Cil.mkBinOp ~loc LAnd (lnot ~loc l) r in
    let l_and_nr = Cil.mkBinOp ~loc LAnd l (lnot ~loc r) in
    Cil.mkBinOp ~loc LOr nl_and_r l_and_nr

  let rec replace ~whole ~part ~(repl: exp) : exp=
    if part == whole then repl
    else
      match whole.enode with
      | UnOp (op, e, typ) ->
        let e' = replace ~whole:e ~part ~repl in
        if e == e' then whole else mk ~loc:whole.eloc (UnOp (op, e', typ))
      | BinOp (op, e1, e2, typ) ->
        let e1' = replace ~whole:e1 ~part ~repl in
        let e2' = replace ~whole:e2 ~part ~repl in
        if e1 == e1' && e2 == e2' then whole else mk ~loc:whole.eloc (BinOp (op, e1', e2', typ))
      | _ -> whole

  (** Joins some expressions (at least one) with a binary operator. *)
  let rev_join ?(loc=Cil_datatype.Location.unknown) op l =
    match l with
    | [] -> invalid_arg "join"
    | head :: tail ->
      List.fold_left (fun acc e -> Cil.mkBinOp ~loc op e acc) head tail

  let join ?(loc=Cil_datatype.Location.unknown) op l =
    rev_join ~loc op (List.rev l)
end

module Stmt_builder = struct
  let mk = Cil.mkStmt ~valid_sid:true
  let instr = Cil.mkStmtOneInstr ~valid_sid:true
  let block stmts = mk (Block (Cil.mkBlock stmts))
end