model_parser.mli 10.1 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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 25

type float_type =
  | Plus_infinity
  | Minus_infinity
  | Plus_zero
  | Minus_zero
  | Not_a_number
  | Float_value of string * string * string

26 27
type model_value =
 | Integer of string
28
 | Decimal of (string * string)
29
 | Fraction of (string * string)
30
 | Float of float_type
31
 | Boolean of bool
32
 | Array of model_array
33
 | Record of model_record
34
 | Bitvector of string
35
 | Unparsed of string
36
and  arr_index = {
37
  arr_index_key : string;
38 39 40 41 42 43
  arr_index_value : model_value;
}
and model_array = {
  arr_others  : model_value;
  arr_indices : arr_index list;
}
44 45 46 47
and model_record ={
  discrs : model_value list;
  fields : model_value list;
}
48

49 50
val array_create_constant :
  value : model_value ->
51 52 53
  model_array
(** Creates constant array with all indices equal to the parameter value. *)

54 55
val array_add_element :
  array : model_array ->
56
  index : string      ->
57
  value : model_value ->
58
  model_array
59
(** Adds an element to the array.
60
    @param array : the array to that the element will be added
61

62 63 64 65 66 67 68 69
    @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

70 71

(*
72
***************************************************************
73 74 75
**  Model elements
***************************************************************
*)
76

77
type model_element_kind =
78 79 80
| Result
  (* Result of a function call (if the counter-example is for postcondition)  *)
| Old
81 82 83 84
  (* 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.*)
85 86
| Other

87 88 89 90 91 92 93
(** 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. *)
}
94

95 96
(** Counter-example model elements. Each element represents
    a counter-example for a single source-code element.*)
97
type model_element = {
98 99
  me_name     : model_element_name;
    (** Information about the name of the model element  *)
100 101 102 103
  me_value    : model_value;
    (** Counter-example value for the element. *)
  me_location : Loc.position option;
    (** Source-code location of the element. *)
104 105
  me_term     : Term.term option;
    (** Why term corresponding to the element.  *)
106 107
}

108 109 110 111
val create_model_element :
  name     : string ->
  value    : model_value ->
  ?location : Loc.position ->
112 113
  ?term     : Term.term ->
  unit ->
114
  model_element
115
(** Creates a counter-example model element.
116 117 118 119
    @param name : the name of the source-code element

    @param value  : counter-example value for the element

120 121
    @param location : source-code location of the element

122
    @param term : why term corresponding to the element *)
123

124
(*
125
***************************************************************
126 127
**  Model definitions
***************************************************************
128 129
*)
type model
130

131 132
val is_model_empty : model -> bool
val default_model : model
133 134

(*
135
***************************************************************
136 137 138
**  Quering the model
***************************************************************
*)
139

140
val print_model :
141
  ?me_name_trans:(model_element_name -> string) ->
142
  Format.formatter ->
143
  model ->
144 145 146 147
  unit
(** Prints the counter-example model

    @param me_name_trans the transformation of the model elements
148 149
      names. The input is information about model element name. The
      output is the name of the model element that should be displayed.
150 151 152
    @param model the counter-example model to print
*)

153 154 155 156 157 158 159 160 161 162
val print_model_human :
  ?me_name_trans:(model_element_name -> string) ->
  Format.formatter ->
  model ->
  unit
(** Same as print_model but is intended to be human readable.

*)


163
val model_to_string :
164
  ?me_name_trans:(model_element_name -> string) ->
165 166 167
  model ->
  string
(** See print_model  *)
168

169
val print_model_vc_term :
170
  ?me_name_trans: (model_element_name -> string) ->
171 172 173 174 175 176 177 178 179 180 181 182
  ?sep: string ->
  Format.formatter ->
  model ->
  unit
(** Prints counter-example model elements related to term that
    triggers VC.

    @param sep separator of counter-example model elements
    @param me_name_trans see print_model
    @model the counter-example model.
*)

183
val model_vc_term_to_string :
184
  ?me_name_trans: (model_element_name -> string) ->
185 186 187 188 189 190 191 192
  ?sep: string ->
  model ->
  string
(** Gets string with counter-example model elements related to term that
    triggers VC.
    See print_model_vc_term
*)

193
val print_model_json :
194
  ?me_name_trans:(model_element_name -> string) ->
195
  ?vc_line_trans:(int -> string) ->
196
  Format.formatter ->
197
  model ->
198 199
  unit
(** Prints counter-example model to json format.
200

201
    @param me_name_trans see print_model
202 203 204 205 206 207 208 209 210 211
    @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.
212 213
    @model the counter-example model to print.

214 215 216 217 218 219 220 221 222 223 224 225
    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)
226
        - "old": Old value of function argument (if the counter-example is for postcondition)
227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247
        - "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"
            }
          ]
      }
    }
248
*)
249

250
val model_to_string_json :
251
  ?me_name_trans:(model_element_name -> string) ->
252
  ?vc_line_trans:(int -> string) ->
253 254 255
  model ->
  string
(** See print_model_json *)
256

257
val interleave_with_source :
258 259
  ?start_comment:string ->
  ?end_comment:string ->
260
  ?me_name_trans:(model_element_name -> string) ->
261
  model ->
262 263
  filename:string ->
  source_code:string ->
264
  string
265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280
(** 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
    @param filename the file name of the source
    @param source_code the input source code

    @return the source code with added comments with information
    about counter-example model
*)
281 282

(*
283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302
***************************************************************
**  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.
*)

(*
***************************************************************
303 304 305 306
** Registering model parser
***************************************************************
*)
type model_parser =  string -> Printer.printer_mapping -> model
307 308
(** Parses the input string into model elements, estabilishes
    a mapping between these elements and mapping from printer
309 310
    and builds model data structure.
*)
311

312 313 314 315
type raw_model_parser =  Stdlib.Sstr.t -> string -> model_element list
(** Parses the input string into model elements. It contains the list of
    projections that are collected in the task.
 *)
316

317
val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit
318 319 320 321

val lookup_model_parser : string -> model_parser

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