package mopsa

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file query.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
(****************************************************************************)
(*                                                                          *)
(* This file is part of MOPSA, a Modular Open Platform for Static Analysis. *)
(*                                                                          *)
(* Copyright (C) 2017-2021 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/>.    *)
(*                                                                          *)
(****************************************************************************)

(** Queries to retrieve variable values during an interactive session *)

open Mopsa_utils
open Core.All
open Format
open Location
open Callstack


(** {2 Debug queries} *)
(** ***************** *)

(* In order to retrieve structured information from the abstract environment,
   each language should implement a handler for the query [Q_debug_variable_value].
   The query [Q_debug_variable_value] retrieves the value of a given
   variable as a [var_value] record, containing a textual representation of
   the value, and a structural encoding of the eventual sub-values.
*)

(** Value of a variable *)
type var_value = {
  var_value: string option;            (** Direct value of the variable *)
  var_value_type : typ;                (** Type of the value *)
  var_sub_value: var_sub_value option; (** Sub-values of the variable *)
}


(** Sub-value of a variable *)
and var_sub_value =
  | Named_sub_value   of (string (** key *) * var_value (** value *)) list
  (** Named sub-values are maps from field names to values *)

  | Indexed_sub_value of var_value list
  (** Indexed sub-values are arrays of values *)


(** Query to retrieve the value of a given variable *)
type ('a,_) query += Q_debug_variable_value : var -> ('a,var_value) query

type ('a,_) query += Q_debug_addr_value : addr -> ('a,var_value) query

let () =
  register_query {
      join = (let doit : type a r. query_pool -> (a,r) query -> r -> r -> r =
          fun next query a b ->
          match query with
          | Q_debug_addr_value addr ->
             assert (a.var_value = None && b.var_value = None);
             let var_sub_value = begin match a.var_sub_value, b.var_sub_value with
                                 | None, Some sb -> Some sb
                                 | Some sa, None -> Some sa
                                 | Some Indexed_sub_value la, Some Indexed_sub_value lb -> Some (Indexed_sub_value (la @ lb))
                                 | Some Named_sub_value ma, Some Named_sub_value mb -> Some (Named_sub_value (ma @ mb))
                                 | _, _ -> assert false
                                 end in
             {var_value=None; var_value_type = T_any; var_sub_value}

          | _ -> next.pool_join query a b
        in doit
      );
      meet = (fun next q a b -> next.pool_meet q a b);
    }


(** Compare two var values *)
let rec compare_var_value v1 v2 =
  Compare.compose [
    (fun () -> Compare.option compare v1.var_value v2.var_value);
    (fun () -> Compare.option compare_var_sub_value v1.var_sub_value v2.var_sub_value);
  ]


(** Compare two var sub-values *)
and compare_var_sub_value sv1 sv2 =
  match sv1, sv2 with
  | Named_sub_value m1, Named_sub_value m2 ->
    Compare.list (fun x1 x2 -> Compare.pair compare compare_var_value x1 x2) m1 m2

  | Indexed_sub_value l1, Indexed_sub_value l2 ->
    Compare.list compare_var_value l1 l2

  | _ -> compare sv1 sv2



(** Print a key with its type *)
let pp_key_with_type fmt (k,t) =
  match t with
  | T_any -> pp_print_string fmt k
  | _      ->Format.fprintf fmt "%s : %a" k pp_typ t


(** Print a variable with its type *)
let pp_var_with_type fmt (v,t) =
  match t with
  | T_any -> pp_var fmt v
  | _      ->Format.fprintf fmt "%a : %a" pp_var v pp_typ t


(** Print the value of a variable *)
let rec pp_var_value fmt v =
  pp_print_option (Debug.color_str Debug.blue) fmt v.var_value;
  match v.var_sub_value with
  | None -> ()
  | Some sv -> fprintf fmt "@,@[<v2>  %a@]" pp_var_sub_value sv


(** Print the values of sub-variables *)
and pp_var_sub_value fmt = function
  | Named_sub_value l ->
    fprintf fmt "%a"
      (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@,")
         (fun fmt (k,v) -> fprintf fmt "%a = %a" pp_key_with_type (k,v.var_value_type) pp_var_value v)
      ) l

  | Indexed_sub_value l ->
    (* Group consecutive elements with the same value *)
    let rec group_by_value = function
      | []        -> []
      | (i,v)::tl ->
        match group_by_value tl with
        | [] -> [(i,i,v)]
        | (a,b,w)::tl ->
          if compare_var_value v w = 0
          then (i,b,v)::tl
          else (i,i,v)::(a,b,w)::tl
    in
    List.mapi (fun i v -> (i,v)) l |>
    group_by_value |>
    fprintf fmt "%a"
      (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@,")
         (fun fmt (i,j,v) ->
            if i = j
            then fprintf fmt "[%d] = %a" i pp_var_value v
            else fprintf fmt "[%d-%d] = %a" i j pp_var_value v
         )
      )
OCaml

Innovation. Community. Security.