package mopsa
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation
Install
Dune Dependency
Authors
Maintainers
Sources
mopsa-analyzer-v1.1.tar.gz
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500
doc/src/interactive/query.ml.html
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 ) )
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>