package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file slicingTypes.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
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
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(** Slicing module types. *)

open Pdg_types

exception Slicing_Internal_Error of string
exception ChangeCallErr of string
exception PtrCallExpr
exception CantRemoveCalledFf
exception WrongSlicingLevel

(** raised when someone tries to build more than one slice for the entry point.
 * *)
exception OnlyOneEntryPointSlice

(** raised when one tries to select something in a function where we are not
 * able to compute the Pdg. *)
exception NoPdg

(** {2 Public types}
  * These types are the only one that should be used by the API functions.
  * Public type definitions should be hidden to the outside world,
  * but it is not really possible to have abstract types since Slicing has to
  * use Db.Slicing functions...  So, it is up to the user of this module to use
  * only this public part.
*)

(** contains global things that has been computed so far
    for the slicing project.
    This includes :
    - the slices of the functions,
    - and the queue of actions to be applied.
*)
type sl_project   = SlicingInternals.project

(** Type of the selections
 * (we store the varinfo because we cannot use the kernel_function in this file)
 * *)
type sl_select = Cil_types.varinfo * SlicingInternals.fct_user_crit

module Fct_user_crit =
  Datatype.Make
    (struct
      include Datatype.Undefined (* TODO: unmarshal *)
      type t = SlicingInternals.fct_user_crit
      let reprs = [ SlicingInternals.dummy_fct_user_crit ]
      let name = "SlicingTypes.Fct_user_crit"
      let mem_project = Datatype.never_any_project
    end)

(** Function slice *)
type sl_fct_slice = SlicingInternals.fct_slice

(** Marks : used to put 'colors' in the result *)
type sl_mark = SlicingInternals.pdg_mark

let pp_sl_project p_caller fmt _p =
  let pp fmt =
    Format.fprintf fmt
      "@[<hv 2>Extlib.the@;~exn:Db.Slicing.No_Project@;@[<hv 2>(!Db.Slicing.Project.get_project@;())@]@]"
  in
  Type.par p_caller Type.Call fmt pp

module Sl_project =
  Datatype.Make
    (struct
      include Datatype.Undefined (* TODO: unmarshal *)
      type t = sl_project
      let reprs = [ SlicingInternals.dummy_project ]
      let name = "SlicingTypes.Sl_project"
      let mem_project = Datatype.never_any_project
    end)

module Sl_select =
  Datatype.Make
    (struct
      include Datatype.Undefined (* TODO: unmarshal *)
      type t = sl_select
      let reprs =
        List.map
          (fun v -> v, SlicingInternals.dummy_fct_user_crit)
          Cil_datatype.Varinfo.reprs
      let name = "SlicingTypes.Sl_select"
      let mem_project = Datatype.never_any_project
    end)

let pp_sl_fct_slice p_caller fmt ff =
  let pp fmt =
    Format.fprintf fmt
      "@[<hv 2>!Db.Slicing.Slice.from_num_id@;%a@;%d@]"
      Kernel_function.pretty
      ff.SlicingInternals.ff_fct.SlicingInternals.fi_kf
      ff.SlicingInternals.ff_id
  in
  Type.par p_caller Type.Call fmt pp

module Sl_fct_slice =
  Datatype.Make
    (struct
      include Datatype.Undefined (* TODO: unmarshal *)
      open SlicingInternals
      type t = fct_slice
      let name = "SlicingTypes.Sl_fct_slice"
      let reprs = [ dummy_fct_slice ]
      let mem_project = Datatype.never_any_project
    end)

let dyn_sl_fct_slice = Sl_fct_slice.ty

let pp_sl_mark fmt m =
  let pp = match m.SlicingInternals.m1, m.SlicingInternals.m2 with
    | SlicingInternals.Spare, _ -> None
    | _, SlicingInternals.Spare -> None
    | SlicingInternals.Cav mark1, SlicingInternals.Cav mark2 ->
      if (PdgTypes.Dpd.is_bottom mark2) then
        (* use [!Db.Slicing.Mark.make] constructor *)
        Some (fun fmt ->
            Format.fprintf fmt "@[<hv 2>!Db.Slicing.Mark.make@;~addr:%b@;~data:%b@;~ctrl:%b@]"
              (PdgTypes.Dpd.is_addr mark1)
              (PdgTypes.Dpd.is_data mark1)
              (PdgTypes.Dpd.is_ctrl mark1))
      else
        None
  in
  let pp = match pp with
    | Some pp -> pp
    | None ->
      let pp fmt sub_m = match sub_m with
        (* use internals constructors *)
        | SlicingInternals.Spare -> Format.fprintf fmt "SlicingInternals.Spare"
        | SlicingInternals.Cav pdg_m -> Format.fprintf fmt
                                          "@[<hv 2>(SlicingInternals.Cav@;@[<hv 2>(PdgTypes.Dpd.make@;~a:%b@;~d:%b@;~c:%b@;())@])@]"
                                          (PdgTypes.Dpd.is_addr pdg_m)
                                          (PdgTypes.Dpd.is_data pdg_m)
                                          (PdgTypes.Dpd.is_ctrl pdg_m)
      in
      fun fmt ->
        Format.fprintf fmt "@[<hv 2>SlicingInternals.create_sl_mark@;~m1:%a@;~m2:%a@]"
          pp m.SlicingInternals.m1 pp m.SlicingInternals.m2
  in pp fmt

module Sl_mark =
  Datatype.Make_with_collections
    (struct
      type t = SlicingInternals.pdg_mark
      let name = "SlicingTypes.Sl_mark"
      let structural_descr = Structural_descr.t_unknown
      let reprs = [ SlicingInternals.dummy_pdg_mark ]
      let compare = SlicingInternals.compare_pdg_mark
      let equal : t -> t -> bool = ( = )
      let hash = Hashtbl.hash
      let copy = Datatype.undefined
      let rehash = Datatype.undefined
      let pretty = pp_sl_mark
      let mem_project = Datatype.never_any_project
    end)

let dyn_sl_mark = Sl_mark.ty

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