Source file `callstack_tracking.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
(****************************************************************************)
(*                                                                          *)
(* This file is part of MOPSA, a Modular Open Platform for Static Analysis. *)
(*                                                                          *)
(* Copyright (C) 2017-2022 The MOPSA Project.                               *)
(*                                                                          *)
(* This program is free software: 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, either version 3 of the License, or     *)
(* (at your option) any later version.                                      *)
(*                                                                          *)
(* This program 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.                      *)
(*                                                                          *)
(* You should have received a copy of the GNU Lesser General Public License *)
(* along with this program.  If not, see <http://www.gnu.org/licenses/>.    *)
(*                                                                          *)
(****************************************************************************)

open Mopsa
open Sig.Abstraction.Domain
open Universal.Ast
open C.Ast
open C.Common.Points_to
open Top

type ('a, _) query += Q_cpython_attached_callstack : addr -> ('a, Callstack.callstack) query

let () = register_query {
             join = (let f: type a r. query_pool -> (a, r) query -> r -> r -> r =
                       fun next query a b ->
                       match query with
                       | Q_cpython_attached_callstack _ -> assert false
                       | _ -> next.pool_join query a b in
                     f);
             meet = (let f: type a r. query_pool -> (a, r) query -> r -> r -> r =
                       fun next query a b ->
                       match query with
                       | Q_cpython_attached_callstack _ -> assert false
                       | _ -> next.pool_meet query a b in
                     f)
           }

module Domain =
  struct

    module Callstacks = struct
      module CallstackSet = Framework.Lattices.Powerset.Make
                            (struct
                              type t = Callstack.callstack
                              let compare = Callstack.compare_callstack
                              let print = unformat pp_callstack
                            end)

      include CallstackSet

      let max_size = 1
      let bound (x:t) : t =
        match x with
        | Nt s when Set.cardinal s <= max_size -> x
        | _ -> TOP

      let join a1 a2 = CallstackSet.join a1 a2 |> bound

      let add v t =
        add v t |> bound
    end


    module CallstackMap = Framework.Lattices.Partial_map.Make(Addr)(Callstacks)

    include CallstackMap

    include Framework.Core.Id.GenDomainId(
                struct
                  type nonrec t = t
                  let name = "cpython.callstack_tracking"
                end)

    let checks = []

    let init _ man flow =
      Hashtbl.add C.Common.Builtins.builtin_functions "_mopsa_pyerr_bind_cs_to" ();
      set_env T_cur empty man flow |>
      Option.some

    let eval exp man flow =
      let range = erange exp in
      match ekind exp with
      | E_c_builtin_call ("_mopsa_pyerr_bind_cs_to", [exc]) ->
         resolve_pointer exc man flow >>$ (fun pt flow ->
          match pt with
          | P_block({base_kind = Addr a}, _, _) ->
             get_env T_cur man flow >>$ fun cur flow ->
             set_env T_cur
               (add a (Callstacks.singleton (Flow.get_callstack flow)) cur)
               man flow
             >>% fun flow ->
             Eval.singleton (mk_one range) flow
          | _ -> assert false
        ) |> OptionExt.return

      | _ -> None

    let exec stmt man flow =
      match skind stmt with
      | S_free addr ->
        get_env T_cur man flow >>$? fun cur flow ->
         let post =
           if mem addr cur then
             set_env T_cur (remove addr cur) man flow
           else Post.return flow in
         post >>% man.exec ~route:(Below name) stmt
         |> OptionExt.return
      | _ -> None

    let ask : type r. ('a, r) query -> ('a, t) man -> 'a flow -> ('a, r) cases option =
      fun query man flow ->
      match query with
      | Q_cpython_attached_callstack a ->
         get_env T_cur man flow >>$? fun cur flow ->
         OptionExt.lift (fun cs ->
             assert(Callstacks.cardinal cs = 1);
             Cases.singleton (Callstacks.choose cs) flow)
           (find_opt a cur)

      | _ -> None

    let print_expr _ _ _ _ = ()
    let print_state printer a =
      pprint ~path:[Key "C/Python callstack tracking"] printer (pbox CallstackMap.print a)

    let merge _ _ _ = assert false
  end

let () = register_standard_domain(module Domain)