model_parser.mli 10.8 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12
(*
13
***************************************************************
14 15 16
**  Counter-example model values
****************************************************************
*)
17 18 19 20 21 22 23 24

type float_type =
  | Plus_infinity
  | Minus_infinity
  | Plus_zero
  | Minus_zero
  | Not_a_number
  | Float_value of string * string * string
25
    (* Float_value (sign, exponent, mantissa) *)
26
  | Float_hexa of string * float
27

28
val interp_float: ?interp:bool -> string -> string -> string -> float_type
29

30 31
type model_value =
 | Integer of string
32
 | Decimal of (string * string)
33
 | Fraction of (string * string)
34
 | Float of float_type
35
 | Boolean of bool
36
 | Array of model_array
37
 | Record of model_record
38
 | Proj of model_proj
39
 | Bitvector of string
40
 | Apply of string * model_value list
41
 | Unparsed of string
42
and  arr_index = {
43
  arr_index_key : string;
44 45 46 47 48 49
  arr_index_value : model_value;
}
and model_array = {
  arr_others  : model_value;
  arr_indices : arr_index list;
}
50 51
and model_proj = (proj_name * model_value)
and proj_name = string
52 53
and model_record = (field_name * model_value) list
and field_name = string
54

55 56
val array_create_constant :
  value : model_value ->
57 58 59
  model_array
(** Creates constant array with all indices equal to the parameter value. *)

60 61
val array_add_element :
  array : model_array ->
62
  index : string      ->
63
  value : model_value ->
64
  model_array
65
(** Adds an element to the array.
66
    @param array : the array to that the element will be added
67

68 69 70 71 72 73 74 75
    @param index : the index on which the element will be added.
    Note that the index must be of value model_value.Integer

    @param value : the value of the element to be added
*)

val print_model_value : Format.formatter -> model_value -> unit

76 77

(*
78
***************************************************************
79 80 81
**  Model elements
***************************************************************
*)
82

83
type model_element_kind =
84 85 86
| Result
  (* Result of a function call (if the counter-example is for postcondition)  *)
| Old
87 88 89 90
  (* Old value of function argument (if the counter-example is for postcondition) *)
| Error_message
  (* The model element represents error message, not source-code element.
     The error message is saved in the name of the model element.*)
91 92
| Other

93 94 95 96 97 98
(** Information about the name of the model element *)
type model_element_name = {
  men_name   : string;
    (** The name of the source-code element.  *)
  men_kind   : model_element_kind;
    (** The kind of model element. *)
99
  men_attrs : Ident.Sattr.t;
100
}
101

102 103
(** Counter-example model elements. Each element represents
    a counter-example for a single source-code element.*)
104
type model_element = {
105
  me_name       : model_element_name;
106
    (** Information about the name of the model element  *)
107
  me_value      : model_value;
108
    (** Counter-example value for the element. *)
109
  me_location   : Loc.position option;
110
    (** Source-code location of the element. *)
111
  me_term       : Term.term option;
112
    (** Why term corresponding to the element.  *)
113 114
}

115
val create_model_element :
116 117
  name      : string ->
  value     : model_value ->
118
  attrs     : Ident.Sattr.t ->
119
  ?location : Loc.position ->
120 121
  ?term     : Term.term ->
  unit ->
122
  model_element
123
(** Creates a counter-example model element.
124 125 126 127
    @param name : the name of the source-code element

    @param value  : counter-example value for the element

128 129
    @param location : source-code location of the element

130 131
    @param term : why term corresponding to the element
*)
132

133
(*
134
***************************************************************
135 136
**  Model definitions
***************************************************************
137 138
*)
type model
139

140 141
val is_model_empty : model -> bool
val default_model : model
142 143

(*
144
***************************************************************
145 146 147
**  Quering the model
***************************************************************
*)
148

149
val print_model :
150
  ?me_name_trans:(model_element_name -> string) ->
151
  print_attrs:bool ->
152
  Format.formatter ->
153
  model ->
154 155 156 157
  unit
(** Prints the counter-example model

    @param me_name_trans the transformation of the model elements
158 159
      names. The input is information about model element name. The
      output is the name of the model element that should be displayed.
160
    @param model the counter-example model to print
161 162
    @param print_attrs: when set to true, the name is printed together with the
    attrs associated to the specific ident.
163 164
*)

165 166 167 168
val print_model_human :
  ?me_name_trans:(model_element_name -> string) ->
  Format.formatter ->
  model ->
169
  print_attrs:bool ->
170 171 172 173 174
  unit
(** Same as print_model but is intended to be human readable.

*)

175
val print_model_json :
176
  ?me_name_trans:(model_element_name -> string) ->
177
  ?vc_line_trans:(int -> string) ->
178
  Format.formatter ->
179
  model ->
180 181
  unit
(** Prints counter-example model to json format.
182

183
    @param me_name_trans see print_model
184 185 186 187 188 189 190 191 192 193
    @param vc_line_trans the transformation from the line number corresponding
      to the term that triggers VC before splitting VC to the name of JSON field
      storing counterexample information related to this term. By default, this
      information is stored in JSON field corresponding to this line, i.e.,
      the transformation is string_of_int.
      Note that the exact line of the construct that triggers VC may not be
      known. This can happen if the term that triggers VC spans multiple lines
      and it is splitted.
      This transformation can be used to store the counterexample information
      related to this term in dedicated JSON field.
194
    @param model the counter-example model to print.
195
    @param print_attrs if set to true, add attrs associated to the name id to
196
      the counterexample output
197

198 199 200 201 202 203 204 205 206 207 208 209
    The format is the following:
    - counterexample is JSON object with fields indexed by names of files
      storing values of counterexample_file
    - counterexample_file is JSON object with fields indexed by line numbers
      storing values of counterexample_line
    - counterexample_line is JSON array (ordered list) with elements
      corresponding to counterexample_element
    - counterexample_element is JSON object with following fields
      - "name": name of counterexample element
      - "value": value of counterexample element
      - "kind": kind of counterexample element:
        - "result": Result of a function call (if the counter-example is for postcondition)
210
        - "old": Old value of function argument (if the counter-example is for postcondition)
211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231
        - "error_message": The model element represents error message, not source-code element.
            The error message is saved in the name of the model element
        - "other"

    Example:
    {
      "records.adb": {
          "84": [
            {
              "name": "A.A",
              "value": "255",
              "kind": "other"
            },
            {
              "name": "B.B",
              "value": "0",
              "kind": "other"
            }
          ]
      }
    }
232
*)
233

234
val interleave_with_source :
235
  print_attrs:bool ->
236 237
  ?start_comment:string ->
  ?end_comment:string ->
238
  ?me_name_trans:(model_element_name -> string) ->
239
  model ->
240
  rel_filename:string ->
241
  source_code:string ->
242 243
  locations:(Loc.position * 'a) list ->
  string * (Loc.position * 'a) list
244 245 246 247 248 249 250 251 252 253
(** Given a source code and a counter-example model interleaves
    the source code with information in about the counter-example.
    That is, for each location in counter-example trace creates
    a comment in the output source code with information about
    values of counter-example model elements.

    @param start_comment the string that starts a comment
    @param end_comment the string that ends a comment
    @param me_name_trans see print_model
    @param model counter-example model
254
    @param rel_filename the file name of the source relative to the session
255
    @param source_code the input source code
256
    @param locations the source locations that are found in the code
257 258

    @return the source code with added comments with information
259 260 261
    about counter-example model. The second part of the pair are
    locations modified so that it takes into account that counterexamples
    were added.
262
*)
263 264

(*
265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284
***************************************************************
**  Filtering the model
***************************************************************
*)
val model_for_positions_and_decls : model ->
  positions: Loc.position list -> model
(** Given a model and a list of source-code positions returns model
    that contains only elements from the input model that are on these
    positions plus for every file in the model, elements that are
    in the positions of function declarations. Elements with other
    positions are filtered out.

    Assumes that for each file the element on the first line of the model
    has position of function declaration.

    Only filename and line number is used to identify positions.
*)

(*
***************************************************************
285 286 287 288
** Registering model parser
***************************************************************
*)
type model_parser =  string -> Printer.printer_mapping -> model
289 290
(** Parses the input string into model elements, estabilishes
    a mapping between these elements and mapping from printer
291 292
    and builds model data structure.
*)
293

294
type raw_model_parser =
DAILLER Sylvain's avatar
DAILLER Sylvain committed
295
  Ident.ident Wstdlib.Mstr.t -> Ident.ident Wstdlib.Mstr.t -> ((string * string) list) Wstdlib.Mstr.t ->
296
    string list -> Ident.Sattr.t Wstdlib.Mstr.t -> string -> model_element list
297 298 299
(** Parses the input string into model elements.
    [raw_model_parser: proj->record_map->noarg_cons->s->mel]
    [proj]: is the list of projections
DAILLER Sylvain's avatar
DAILLER Sylvain committed
300
    [list_field]: is the list of field function definition
301 302 303 304 305 306
    [record_map]: is a map associating the name of printed projections to the
      fields (couple of printed field and model_trace name).
    [noarg_cons]: List of constructors with no arguments (collected to avoid
      confusion between variable and constructors)
    [s]: model
    [mel]: collected model
307
 *)
308

309 310
val register_remove_field:
  (Ident.Sattr.t * model_value -> Ident.Sattr.t * model_value) -> unit
311

312
val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit
313 314 315 316

val lookup_model_parser : string -> model_parser

val list_model_parsers : unit -> (string * Pp.formatted) list