Source file `mt_ids.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-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 licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Mt_memory.Types

type id_type = IdThread | IdMutex | IdQueue

let to_string = function
  | IdThread -> "thread"
  | IdMutex -> "mutex"
  | IdQueue -> "queue"

type raw_id = id_type * int

let pretty_raw_id fmt (idt, offset) =
  Format.fprintf fmt "%s_%d" (to_string idt) offset


(* YYY cache this per project *)
let array_threads = Mt_cil.mthread_global_var "__fc_mthread_threads"
let array_mutexes = Mt_cil.mthread_global_var "__fc_mthread_mutexes"
let array_queues = Mt_cil.mthread_global_var "__fc_mthread_queues"

let array_of_idt = function
  | IdThread -> array_threads ()
  | IdMutex -> array_mutexes ()
  | IdQueue -> array_queues ()

let pointer_of_id ((idt, offset): raw_id) : pointer =
  assert (offset > 0);
  let array = array_of_idt idt
  and offset = (offset - 1) * (Machine.sizeof_int ())
  (* Let us not lose the first cell of the array *)
  in
  array, offset


let read_id_state state raw_id =
  let p = pointer_of_id raw_id in
  Mt_memory.read_int_pointer p state

let read_id_state_enumerate card state raw_id : _ Mt_lib.conversion =
  let value = read_id_state state raw_id in
  let failure fmt = Format.fprintf fmt "Id %a contains garbled state %a"
      pretty_raw_id raw_id Cvalue.V.pretty value
  in
  try
    match Locations.Location_Bytes.fold_i (fun b i l -> (b,i) :: l) value []
    with
    | [Base.Null,i]  -> begin
        try
          ignore (Ival.cardinal_less_than i card);
          `Success (Ival.fold_int (fun i l -> Abstract_interp.Int.to_int_exn i :: l) i [])
        with Abstract_interp.Not_less_than -> `Failure failure
      end

    | _ -> `Failure failure
  with Not_found -> `Failure failure


let write_id_state state raw_id v =
  let p = pointer_of_id raw_id in
  Mt_memory.write_int_pointer p v state

let replace_id_value state raw_id ~before ~after =
  let p = pointer_of_id raw_id in
  Mt_memory.replace_value_at_int_pointer p ~before ~after state

let of_thread th = IdThread, Thread.id th
let of_mutex m = IdMutex, Mutex.id m
let of_queue q = IdQueue, Mqueue.id q